E. Albert, M. Gómez-Zamalloa, L. Hubert & G. Puebla (2007):
Verification of Java Bytecode Using Analysis and Transformation of Logic Programs.
In: M. Hanus: Practical Aspects of Declarative Languages,
Lecture Notes in Computer Science 4354.
Springer,
pp. 124–139,
doi:10.1007/978-3-540-69611-7_8.
K. R. Apt, F. S. de Boer & E.-R. Olderog (2009):
Verification of Sequential and Concurrent Programs,
Third edition.
Springer,
doi:10.1007/978-1-84882-745-5.
G. Banda & J. P. Gallagher (2009):
Analysis of Linear Hybrid Systems in CLP.
In: Michael Hanus: Logic-Based Program Synthesis and Transformation, 18th International Symposium, LOPSTR 2008, Valencia, Spain, July 17–18, 2008, Revised Selected Papers,
Lecture Notes in Computer Science 5438.
Springer,
pp. 55–70,
doi:10.1007/978-3-642-00515-2_5.
N. Bjørner, A. Gurfinkel, K. L. McMillan & A. Rybalchenko (2015):
Horn Clause Solvers for Program Verification.
In: L. D. Beklemishev, A. Blass, N. Dershowitz, B. Finkbeiner & W. Schulte: Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday,
Lecture Notes in Computer Science 9300.
Springer,
pp. 24–51,
doi:10.1007/978-3-319-23534-9_2.
M. Bruynooghe, M. Codish, J. P. Gallagher, S. Genaim & W. Vanhoof (2007):
Termination analysis of logic programs through combination of type-based norms.
ACM Trans. Program. Lang. Syst. 29(2),
pp. 10–es,
doi:10.1145/1216374.1216378.
A. Bundy (2001):
The Automation of Proof by Mathematical Induction.
In: A. Robinson & A. Voronkov: Handbook of Automated Reasoning I.
North Holland,
pp. 845–911,
doi:10.1016/B978-044450813-3/50015-1.
R. M. Burstall & J. Darlington (1977):
A Transformation System for Developing Recursive Programs.
Journal of the ACM 24(1),
pp. 44–67,
doi:10.1145/321992.321996.
R. Certezeanu, S. Drossopoulou, B. Egelund-Müller, K. R. M. Leino, S. Sivarajan & M. J. Wheelhouse (2016):
Quicksort Revisited - Verifying Alternative Versions of Quicksort.
In: E. Ábrahám, M. M. Bonsangue & E. Broch Johnsen: Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday,
Lecture Notes in Computer Science 9660.
Springer,
pp. 407–426,
doi:10.1007/978-3-319-30734-3_27.
E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014):
Program Verification via Iterated Specialization.
Science of Computer Programming 95, Part 2,
pp. 149–175,
doi:10.1016/j.scico.2014.05.017.
E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014):
VeriMAP: A Tool for Verifying Programs through Transformations.
In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS '14,
Lecture Notes in Computer Science 8413.
Springer,
pp. 568–574,
doi:10.1007/978-3-642-54862-8_47.
Available at http://www.map.uniroma2.it/VeriMAP.
E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2017):
Semantics-based generation of verification conditions via program specialization.
Science of Computer Programming 147,
pp. 78–108,
doi:10.1016/j.scico.2016.11.002.
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.
Special Issue onıt ICLP '18.
E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2020):
Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates.
In: Proceedings of the International Joint Conference on Automated Reasoning, IJCAR '20,
Lecture Notes in Computer Science 12166.
Springer, Cham,
pp. 83–102,
doi:10.1007/978-3-030-51074-9_6.
G. Delzanno & A. Podelski (1999):
Model Checking in CLP.
In: R. Cleaveland: 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS '99,
Lecture Notes in Computer Science 1579.
Springer-Verlag,
pp. 223–239,
doi:10.1007/3-540-49059-0_16.
S. Etalle & M. Gabbrielli (1996):
Transformations of CLP Modules.
Theoretical Computer Science 166,
pp. 101–146,
doi:10.1016/0304-3975(95)00148-4.
F. Fioravanti, A. Pettorossi & M. Proietti (2001):
Verifying CTL Properties of Infinite State Systems by Specializing Constraint Logic Programs.
In: Proceedings of the ACM SIGPLAN Workshop on Verification and Computational Logic VCL'01, Florence (Italy),
Technical Report DSSE-TR-2001-3.
University of Southampton, UK,
pp. 85–96.
M. Foley & C. A. R. Hoare (1971):
Proof of a Recursive Program: Quicksort.
Comput. J. 14(4),
pp. 391–395,
doi:10.1093/comjnl/14.4.391.
L. Fribourg & H. Olsén (1997):
A decompositional approach for computing least fixed-points of Datalog programs with Z-counters.
Constraints 2(3/4),
pp. 305–335,
doi:10.1023/A:1009747629591.
S. Grebenshchikov, N. P. Lopes, C. Popeea & A. Rybalchenko (2012):
Synthesizing software verifiers from proof rules.
In: Proceedings of the ACM SIGPLAN Conference on 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.
C. A. R. Hoare (1961):
Algorithm 64: Quicksort.
Commun. ACM 4(7),
pp. 321,
doi:10.1145/366622.366644.
C.A.R. Hoare (1969):
An Axiomatic Basis for Computer Programming.
CACM 12(10),
pp. 576–580, 583,
doi:10.1145/363235.363259.
C. J. Hogger (1981):
Derivation of Logic Programs.
Journal of the ACM 28(2),
pp. 372–392,
doi:10.1145/322248.322258.
H. Hojjat & Ph. Rümmer (2018):
The ELDARICA Horn Solver.
In: N. Bjørner & A. Gurfinkel: 2018 Formal Methods in Computer Aided Design, \voidb@x FMCAD 2018, Austin, TX, USA, October 30 – November 2, 2018.
IEEE,
pp. 1–7,
doi:10.23919/FMCAD.2018.8603013.
B. Kafle & J. P. Gallagher (2017):
Constraint specialisation in Horn clause verification.
Sci. Comput. Program. 137,
pp. 125–140,
doi:10.1016/j.scico.2017.01.002.
A. Komuravelli, A. Gurfinkel, S. Chaki & E. M. Clarke (2013):
Automatic Abstraction in SMT-Based Unbounded Software Model Checking.
In: N. Sharygina & H. Veith: Computer Aided Verification, Proceedings of the 25th International Conference CAV '13, Saint Petersburg, Russia, July 13–19, 2013,
Lecture Notes in Computer Science 8044.
Springer,
pp. 846–862,
doi:10.1007/978-3-642-39799-8_59.
K. R. M. Leino (2013):
Developing Verified Programs with Dafny.
In: Proceedings of the 2013 International Conference on Software Engineering,
ICSE '13.
IEEE Press,
pp. 1488–1490,
doi:10.1109/ICSE.2013.6606754.
M. Leuschel & H. Lehmann (2000):
Coverability of Reset Petri Nets and Other Well-Structured Transition Systems by Partial Deduction..
In: J. W. Lloyd: Proceedings of the First International Conference on Computational Logic (CL 2000), London, UK, 24-28 July,
Lecture Notes in Artificial Intelligence 1861.
Springer-Verlag,
pp. 101–115,
doi:10.1007/3-540-44957-4_7.
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, Proceedings,
Lecture Notes in Computer Science 523.
Springer,
pp. 124–144,
doi:10.1007/3540543961_7.
M. Méndez-Lojo, J. A. Navas & M. V. Hermenegildo (2008):
A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs.
In: 17th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR '07, Kongens Lyngby, Denmark, August 23–24, 2007,
Lecture Notes in Computer Science 4915.
Springer,
pp. 154–168,
doi:10.1007/978-3-540-78769-3_11.
D. Mordvinov & G. Fedyukovich (2017):
Synchronizing Constrained Horn Clauses.
In: T. Eiter & D. Sands: LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017,
EPiC Series in Computing 46.
EasyChair,
pp. 338–355.
Available at http://www.easychair.org/publications/paper/340359.
L. M. de Moura & N. Bjørner (2008):
Z3: An Efficient SMT Solver.
In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 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.
J. C. Peralta, J. P. Gallagher & H. Saglam (1998):
Analysis of Imperative Programs through Analysis of Constraint Logic Programs.
In: G. Levi: Proceedings of the 5th International Symposium on Static Analysis, SAS '98,
Lecture Notes in Computer Science 1503.
Springer,
pp. 246–261,
doi:10.1007/3-540-49727-7_15.
A. Pettorossi & M. Proietti (1989):
Decidability Results and Characterization of Strategies for the Development of Logic Programs.
In: G. Levi & M. Martelli: Proceedings of the Sixth International Conference on Logic Programming, Lisbon, Portugal.
The MIT Press,
pp. 539–553.
Tuan-Hung Pham, Andrew Gacek & Michael W. Whalen (2016):
Reasoning About Algebraic Data Types with Abstractions.
J. Autom. Reason. 57(4),
pp. 281–318,
doi:10.1007/s10817-016-9368-2.
A. Podelski & A. Rybalchenko (2007):
ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement.
In: M. Hanus: Practical Aspects of Declarative Languages, PADL '07,
Lecture Notes in Computer Science 4354.
Springer,
pp. 245–259,
doi:10.1007/978-3-540-69611-7_16.
M. Proietti & A. Pettorossi (1995):
Unfolding-Definition-Folding, in this Order, for Avoiding Unnecessary Variables in Logic Programs.
Theoretical Computer Science 142(1),
pp. 89–124,
doi:10.1016/0304-3975(94)00227-A.
Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. Swift & D. S. Warren (1997):
Efficient Model Checking Using Tabled Resolution.
In: Proceedings of the 9th International Conference on Computer Aided Verification (CAV '97),
Lecture Notes in Computer Science 1254.
Springer-Verlag,
pp. 143–154,
doi:10.1007/3-540-63166-6_16.
S. Renault, A. Pettorossi & M. Proietti (1998):
Design, Implementation, and Use of the MAP Transformation System.
R 491.
IASI-CNR,
Rome, Italy.
Available at http://www.iasi.cnr.it/~proietti/system.html.
A. Reynolds & V. Kuncak (2015):
Induction for SMT Solvers.
In: Deepak D'Souza, Akash Lal & Kim Guldstrand Larsen: Verification, Model Checking, and Abstract Interpretation, Proceedings of the 16th International Conference VMCAI 2015, Mumbai, India, January 12–14, 2015,
Lecture Notes in Computer Science 8931.
Springer,
pp. 80–98,
doi:10.1007/978-3-662-46081-8_5.
Ph. Suter, M. Dotta & V. Kuncak (2010):
Decision procedures for algebraic data types with abstractions.
In: M. V. Hermenegildo & J. Palsberg: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010.
ACM,
pp. 199–210,
doi:10.1145/1706299.1706325.
H. Tamaki & T. Sato (1984):
Unfold/Fold Transformation of Logic Programs.
In: S.-Å. Tärnlund: Proceedings of the Second International Conference on Logic Programming, ICLP '84.
Uppsala University,
Uppsala, Sweden,
pp. 127–138.
H. Unno, S. Torii & H. Sakamoto (2017):
Automating Induction for Solving Horn Clauses.
In: Rupak Majumdar & Viktor Kuncak: Computer Aided Verification, Proceedings of the 29th International Conference CAV '17, Heidelberg, Germany, Part II,
Lecture Notes in Computer Science 10427.
Springer,
pp. 571–591,
doi:10.1007/978-3-319-63390-9_30.
P. L. Wadler (1990):
Deforestation: Transforming Programs to Eliminate Trees.
Theoretical Computer Science 73,
pp. 231–248,
doi:10.1016/0304-3975(90)90147-A.