References

  1. F. Baader & W. Snyder (2001): Unification Theory. In: A. Robinson & A. Voronkov: Handbook of Automated Reasoning I. Elsevier Science, pp. 445–532, doi:10.1016/B978-044450813-3/50010-2.
  2. A. R. Bradley (2011): SAT-Based Model Checking without Unrolling. In: Ranjit Jhala & David A. Schmidt: Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23–25, 2011. Proceedings, Lecture Notes in Computer Science 6538. Springer, pp. 70–87, doi:10.1007/978-3-642-18275-4_7.
  3. 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.
  4. E.M. Clarke, O. Grumberg, S. Jha, Y. Lu & H. Veith (2000): Counterexample-Guided Abstraction Refinement. In: E.A. Emerson & A.P. Sistla: Proceedings of the 12th International Conference on Computer Aided Verification, CAV '00, Lecture Notes in Computer Science 1855. Springer, pp. 154–169, doi:10.1007/10722167_15.
  5. 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.
  6. E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014): VeriMAP: A Tool for Verifying Programs through Transformations. In: E. Ábrahám & K. Havelund: 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.
  7. 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.
  8. 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. Selected and Extended papers from the International Symposium on Principles and Practice of Declarative Programming 2015.
  9. 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.
  10. 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.
  11. E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2019): Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification. In: E. De Angelis, G. Fedyukovich, N. Tzevelekos & M. Ulbrich: Proceedings of HCVS/PERR 2019: 6th Workshop on Horn Clauses for Verification and Synthesis and 3rd Workshop on Program Equivalence and Relational Reasoning, Prague, Czech Republic, April 6–7, 2019, To appear in EPTCS. Available at https://conf.researchr.org/details/etaps-2019/hcvs-2019-papers/3/Proving-Properties-of-Sorting-Programs-A-Case-Study-in-Horn-Clause-Verification.
  12. S. Etalle & M. Gabbrielli (1996): Transformations of CLP Modules. Theoretical Computer Science 166, pp. 101–146, doi:10.1016/0304-3975(95)00148-4.
  13. 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.
  14. K. Hoder & N. Bjørner (2012): Generalized Property Directed Reachability. In: Alessandro Cimatti & Roberto Sebastiani: Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT '12, Lecture Notes in Computer Science 7317. Springer, Berlin, Heidelberg, pp. 157–171, doi:10.1007/978-3-642-31612-8_13.
  15. 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.
  16. B. Kafle, J. P. Gallagher & J. F. Morales (2016): RAHFT: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata. In: S. Chaudhuri & A. Farzan: 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.
  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. K. L. McMillan (2003): Interpolation and SAT-Based Model Checking. In: Warren A. Hunt Jr. & Fabio Somenzi: Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, Lecture Notes in Computer Science 2725. Springer, pp. 1–13, doi:10.1007/978-3-540-45069-6_1.
  19. 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.
  20. L. M. de Moura & N. Bjørner (2008): Z3: An Efficient SMT Solver. In: C.R. Ramakrishnan & J. Rehof: 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.
  21. A. Pettorossi & M. Proietti (2000): Perfect Model Checking via Unfold/Fold Transformations. 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. 613–628, doi:10.1007/3-540-44957-4_41.
  22. 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.
  23. T. Sato & H. Tamaki (1984): Transformational Logic Program Synthesis. In: Proceedings of the International Conference on Fifth Generation Computer Systems. ICOT, pp. 195–201.
  24. 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.
  25. 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