References

  1. 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 inComputer Science 9300. Springer, pp. 24–51, doi:10.1007/978-3-319-23534-9_2.
  2. 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.
  3. 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. Selected and extended papers from Partial Evaluation and Program Manipulation 2013.
  4. 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.
  5. E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2015): Proving correctness of imperative programs by linearizing constrained Horn clauses. Theory and Practice of Logic Programming 15(4–5), pp. 635–650, doi:10.1017/S1471068415000289.
  6. 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. Available at http://www.sciencedirect.com/science/article/pii/S016764231630199X. Selected and Extended papers from the International Symposium on Principles and Practice of Declarative Programming 2015.
  7. E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2018): Predicate Pairing for program verification. TPLP 18(2), pp. 126–166, doi:10.1017/S1471068417000497.
  8. E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2018): Solving Horn Clauses on Inductive Data Types Without Induction. TPLP 18(3-4), pp. 452–469, doi:10.1017/S1471068418000157.
  9. E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2019): Lemma Generation for Horn Clause Satisfiability: A Preliminary Study. In: A. Lisitsa & A. Nemytykh: Proceedings of VPT 2019 Workshop on Program Verification and Program Transformation, Genova, Italy, April 4th, 2019, To appear in EPTCS. Available at http://refal.botik.ru/vpt/vpt2019/VPT2019_paper_9.pdf.
  10. S. Etalle & M. Gabbrielli (1996): Transformations of CLP Modules. Theoretical Computer Science 166, pp. 101–146, doi:10.1016/0304-3975(95)00148-4.
  11. G. Fedyukovich, S. Prabhu, K. Madhukar & A. Gupta (2018): Solving Constrained Horn Clauses Using Syntax and Data. In: N. Bjørner & A. Gurfinkel: 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. IEEE, pp. 1–9, doi:10.23919/FMCAD.2018.8603011.
  12. 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.
  13. H. Hojjat, F. Konecný, F. Garnier, R. Iosif, V. Kuncak & P. Rümmer (2012): A Verification Toolkit for Numerical Transition Systems. In: D. Giannakopoulou & D. Méry: FM '12: Formal Methods, 18th International Symposium, Paris, France, August 27–31, 2012. Proceedings, Lecture Notes in Computer Science 7436. Springer, pp. 247–251, doi:10.1007/978-3-642-32759-9_21.
  14. H. Hojjat & P. Rümmer (2018): The ELDARICA Horn Solver. In: N. Bjørner & A. Gurfinkel: 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. IEEE, pp. 1–7, doi:10.23919/FMCAD.2018.8603013.
  15. B. Kafle, J. P. Gallagher & J. F. Morales (2016): RAHFT: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata. In: Computer Aided Verification, 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, Lecture Notes in Computer Science 9779. Springer, pp. 261–268, doi:10.1007/978-3-319-41528-4_14.
  16. A. Komuravelli, A. Gurfinkel & S. Chaki (2014): SMT-Based Model Checking for Recursive Programs. In: A. Biere & R. Bloem: Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Lecture Notes in Computer Science 8559. Springer, pp. 17–34, doi:10.1007/978-3-319-08867-9_2.
  17. X. Leroy, D. Doligez, A. Frisch, J. Garrigue, D. Rémy & J. Vouillon (2017): The OCaml system, Release 4.06. Documentation and user's manual. Institut National de Recherche en Informatique et en Automatique, France.
  18. 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, doi:10.29007/gr5c. Available at https://easychair.org/publications/paper/LlxW.
  19. 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.
  20. 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,, Lecture Notes in Computer Science 8931. Springer, pp. 80–98, doi:10.1007/978-3-662-46081-8_5.
  21. 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.
  22. H. Unno, S. Torii & H. Sakamoto (2017): Automating Induction for Solving Horn Clauses. In: Rupak Majumdar & Viktor Kuncak: Proc. Computer Aided Verification - 29th Intern. Conf. CAV 2017, Heidelberg, Germany, Part II, Lecture Notes in Computer Science 10427. Springer, pp. 571–591, doi:10.1007/978-3-319-63390-9_30.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org