@incollection(Boogie,
 author       = {M.~Barnett and B.-Y.~E. Chang and R.~{De Line} and B.~Jacobs and K.~R.~M. Leino},
 year         = {2006},
 title        = {Boogie: {A} Modular Reusable Verifier for Object-Oriented Programs},
 editor       = {F.~de~Boer and M.~M. Bonsangue and S.~Graf and W.-P. de~Roever},
 booktitle    = {Formal Methods for Components and Objects},
 series       = {Lecture Notes in Computer Science 4111},
 publisher    = {Springer},
 pages        = {364--387},
 doi          = {10.1007/11804192_17},
)
@inproceedings(CVC4,
 author       = {C.~Barrett and C.~L. Conway and M.~Deters and L.~Hadarean and D.~Jovanovic and T.~King and A.~Reynolds and C.~Tinelli},
 year         = {2011},
 title        = {{CVC4}},
 editor       = {Ganesh Gopalakrishnan and Shaz Qadeer},
 booktitle    = {23rd {CAV}~'11},
 series       = {Lecture Notes in Computer Science 6806},
 publisher    = {Springer},
 pages        = {171--177},
 doi          = {10.1007/978-3-642-22110-1_14},
)
@book(BoochB94,
 author       = {Grady Booch and Doug Bryan},
 year         = {1994},
 title        = {Software engineering with Ada {(3.} ed.)},
 series       = {Benjamin/Cummings series in object-oriented software engineering},
 publisher    = {Benjamin/Cummings},
)
@inproceedings(MaS13,
 author       = {Alessandro Cimatti and Alberto Griggio and Bastiaan Schaafsma and Roberto Sebastiani},
 year         = {2013},
 title        = {The {MathSAT5 SMT} solver},
 editor       = {Nir Piterman and Scott Smolka},
 booktitle    = {19th TACAS~'13},
 series       = {Lecture Notes in Computer Science 7795},
 publisher    = {Springer},
 pages        = {93--107},
 doi          = {10.1007/978-3-642-36742-7_7},
)
@article(DeAngelisFGHPP21,
 author       = {E.~{De Angelis} and F.~Fioravanti and J.~P. Gallagher and M.~V. Hermenegildo and A.~Pettorossi and M.~Proietti},
 year         = {2021},
 title        = {Analysis and Transformation of Constrained {H}orn Clauses for Program Verification},
 journal      = {Theory and Practice of Logic Programming},
 pages        = {1--69},
 doi          = {10.1017/S1471068421000211},
)
@article(De&18a,
 author       = {E.~{De Angelis} and F.~Fioravanti and A.~Pettorossi and M.~Proietti},
 year         = {2018},
 title        = {Solving {H}orn Clauses on Inductive Data Types Without Induction},
 journal      = {Theory and Practice of Logic Programming},
 volume       = {18},
 number       = {3-4},
 pages        = {452--469},
 doi          = {10.1017/S1471068418000157},
)
@inproceedings(De&20a,
 author       = {E.~{De Angelis} and F.~Fioravanti and A.~Pettorossi and M.~Proietti},
 year         = {2020},
 title        = {Removing Algebraic Data Types from Constrained {H}orn Clauses Using Difference Predicates},
 editor       = {N.~Peltier and V.~Sofronie-Stokkermans},
 booktitle    = {Proceedings of the International Joint Conference on Automated Reasoning, IJCAR~2020},
 series       = {Lecture Notes in Artificial Intelligence 12166},
 publisher    = {Springer},
 pages        = {83--102},
 doi          = {10.1007/978-3-030-51074-9_6},
)
@article(De&22a,
 author       = {E.~{De Angelis} and F.~Fioravanti and A.~Pettorossi and M.~Proietti},
 year         = {2022a},
 title        = {Satisfiability of constrained {H}orn clauses on algebraic data types: {A} transformation-based approach},
 journal      = {Journal of Logic and Computation},
 volume       = {32},
 pages        = {402--442},
 doi          = {10.1093/logcom/exab090},
)
@article(DeAngelisFPP22,
 author       = {E.~{De Angelis} and M.~Proietti and F.~Fioravanti and A.~Pettorossi},
 year         = {2022},
 title        = {Verifying Catamorphism-Based Contracts using Constrained {H}orn Clauses},
 journal      = {Theory and Practice of Logic Programming},
 volume       = {22},
 number       = {4},
 pages        = {555--572},
 doi          = {10.1017/S1471068422000175},
)
@inproceedings(Why3,
 author       = {J.-C. Filli{\^{a}}tre and A.~Paskevich},
 year         = {2013},
 title        = {Why3 - {W}here Programs Meet Provers},
 editor       = {M.~Felleisen and Ph. Gardner},
 booktitle    = {Programming Languages and Systems, 22nd European Symposium on Programming, {ESOP}'13, Rome, Italy, March 16--24, 2013},
 series       = {Lecture Notes in Computer Science 7792},
 publisher    = {Springer},
 pages        = {125--128},
 doi          = {10.1007/978-3-642-37036-6_8},
)
@inproceedings(Flo67,
 author       = {R.~W. Floyd},
 year         = {1967},
 title        = {Assigning Meanings to Programs},
 editor       = {J.~T. Schwartz},
 booktitle    = {Proceedings of Symposium on Applied Mathematics, Vol. 19},
 publisher    = {American Mathematical Society, Providence, R.I., USA},
 pages        = {19--32},
 doi          = {10.1007/978-94-011-1793-7_4},
)
@article(GovindSG22,
 author       = {H.~{Govind V. K.} and S.~Shoham and A.~Gurfinkel},
 year         = {2022},
 title        = {Solving constrained {H}orn clauses modulo algebraic data types and recursive functions},
 journal      = {Proc. {ACM} Program. Lang.},
 volume       = {6},
 number       = {{POPL}},
 pages        = {1--29},
 doi          = {10.1145/3498722},
)
@inproceedings(Gr&12,
 author       = {S.~Grebenshchikov and N.~P. Lopes and C.~Popeea and A.~Rybalchenko},
 year         = {2012},
 title        = {Synthesizing software verifiers from proof rules},
 booktitle    = {33rd ACM SIGPLAN Conf.~Programming Language Design and Implementation, PLDI~'12},
 pages        = {405--416},
 doi          = {10.1145/2345156.2254112},
)
@article(HamzaVK19,
 author       = {J.~Hamza and N.~Voirol and V.~Kuncak},
 year         = {2019},
 title        = {System {FR:} formalized foundations for the {S}tainless verifier},
 journal      = {Proc. {ACM} Program. Lang.},
 volume       = {3},
 number       = {{OOPSLA}},
 pages        = {166:1--166:30},
 doi          = {10.1145/3360592},
)
@article(Hermenegildo&12,
 author       = {M.~Hermenegildo and F.~Bueno and M.~Carro and P.~L{\'o}pez-Garc{\'i}a and E.~Mera and J.~F. Morales and G.~Puebla},
 year         = {2012},
 title        = {{A}n Overview of {C}iao and its Design Philosophy},
 journal      = {Theory and Practice of Logic Programming},
 volume       = {12},
 number       = {1--2},
 pages        = {219--252},
 doi          = {10.1017/S1471068411000457},
)
@article(Hoa69,
 author       = {C.A.R. Hoare},
 year         = {1969},
 title        = {An {A}xiomatic {B}asis for {C}omputer {P}rogramming},
 journal      = {CACM},
 volume       = {12},
 number       = {10},
 pages        = {576--580, 583},
 doi          = {10.1145/363235.363259},
)
@inproceedings(HoR18,
 author       = {H.~Hojjat and Ph. R{\"{u}}mmer},
 year         = {2018},
 title        = {The {ELDARICA} {H}orn Solver},
 editor       = {N.~Bj{\o}rner and A.~Gurfinkel},
 booktitle    = {Formal Methods in Computer Aided Design, \mbox{FMCAD~2018}},
 publisher    = {{IEEE}},
 pages        = {1--7},
 doi          = {10.23919/FMCAD.2018.8603013},
)
@inproceedings(Ko&14,
 author       = {A.~Komuravelli and A.~Gurfinkel and S.~Chaki},
 year         = {2014},
 title        = {{SMT}-Based Model Checking for Recursive Programs},
 booktitle    = {26th {CAV}~'14},
 series       = {Lecture Notes in Computer Science 8559},
 publisher    = {Springer},
 pages        = {17--34},
 doi          = {10.1007/978-3-319-08867-9_2},
)
@inproceedings(KostyukovMF21,
 author       = {Yurii Kostyukov and Dmitry Mordvinov and Grigory Fedyukovich},
 year         = {2021},
 title        = {Beyond the elementary representations of program invariants over algebraic data types},
 editor       = {Stephen~N. Freund and Eran Yahav},
 booktitle    = {{PLDI} '21: 42nd {ACM} {SIGPLAN} International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021},
 publisher    = {{ACM}},
 pages        = {451--465},
 doi          = {10.1145/3453483.3454055},
)
@inproceedings(Lei13,
 author       = {K.~R.~M. Leino},
 year         = {2013},
 title        = {Developing Verified Programs with {D}afny},
 booktitle    = {Intl. Conf. on Software Engineering~'13},
 publisher    = {IEEE Press},
 pages        = {1488--1490},
 doi          = {10.1109/ICSE.2013.6606754},
)
@inproceedings(MeijerFP91,
 author       = {E.~Meijer and M.~M. Fokkinga and R.~Paterson},
 year         = {1991},
 title        = {Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire},
 editor       = {J.~Hughes},
 booktitle    = {Functional Programming Languages and Computer Architecture, 5th {ACM} Conference, Cambridge, MA, USA, August 26-30, 1991},
 series       = {Lecture Notes in Computer Science 523},
 publisher    = {Springer},
 pages        = {124--144},
 doi          = {10.1007/3540543961\_7},
)
@book(Meyer91,
 author       = {Bertrand Meyer},
 year         = {1991},
 title        = {Eiffel: The Language},
 publisher    = {Prentice-Hall},
)
@inproceedings(DeB08,
 author       = {L.~M. de~Moura and N.~Bj{\o}rner},
 year         = {2008},
 title        = {Z3: {A}n Efficient {SMT} Solver},
 booktitle    = {14th {TACAS}~'08},
 series       = {Lecture Notes in Computer Science 4963},
 publisher    = {Springer},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3\_24},
)
@book(OderskySV11,
 author       = {M.~Odersky and L.~Spoon and B.~Venners},
 year         = {2011},
 title        = {Programming in {S}cala: {A} Comprehensive Step-by-Step Guide},
 edition      = {2nd},
 publisher    = {Artima Incorporation},
 address      = {Sunnyvale, CA, USA},
)
@inproceedings(ReK15,
 author       = {A.~Reynolds and V.~Kuncak},
 year         = {2015},
 title        = {Induction for {SMT} Solvers},
 editor       = {Deepak D'Souza and Akash Lal and Kim~Guldstrand Larsen},
 booktitle    = {16th {VMCAI}},
 series       = {Lecture Notes in Computer Science 8931},
 publisher    = {Springer},
 pages        = {80--98},
 doi          = {10.1007/978-3-662-46081-8_5},
)
@misc(Solidity,
 author       = {Solidity},
 year         = {2022},
 title        = {Solidity v0.8.12 Documentation},
 howpublished = {\url{https://docs.soliditylang.org/}},
)
@incollection(Su&11,
 author       = {{Philippe} Suter and A.~S. K\"{o}ksal and V.~Kuncak},
 year         = {2011},
 title        = {Satisfiability Modulo Recursive Programs},
 editor       = {E.~Yahav},
 booktitle    = {18th {SAS}~'11},
 series       = {Lecture Notes in Computer Science 6887},
 publisher    = {Springer},
 pages        = {298--315},
 doi          = {10.1007/978-3-642-23702-7\_23},
)
@inproceedings(Un&17,
 author       = {H.~Unno and S.~Torii and H.~Sakamoto},
 year         = {2017},
 title        = {Automating Induction for Solving {H}orn Clauses},
 editor       = {Rupak Majumdar and Viktor Kuncak},
 booktitle    = {29th {CAV}~'17, Part {II}},
 series       = {Lecture Notes in Computer Science 10427},
 publisher    = {Springer},
 pages        = {571--591},
 doi          = {10.1007/978-3-319-63390-9_30},
)
@inproceedings(Ya&19,
 author       = {Weikun Yang and Grigory Fedyukovich and Aarti Gupta},
 year         = {2019},
 title        = {Lemma Synthesis for Automating Induction over Algebraic Data Types},
 editor       = {Thomas Schiex and Simon de~Givry},
 booktitle    = {25th Int. Conf. Principles and Practice of Constraint Programming, {CP~2019}},
 series       = {Lecture Notes in Computer Science 11802},
 publisher    = {Springer},
 pages        = {600--617},
 doi          = {10.1007/978-3-030-30048-7\_35},
)