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