References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. S. Etalle & M. Gabbrielli (1996): Transformations of CLP Modules. Theoretical Computer Science 166, pp. 101–146, doi:10.1016/0304-3975(95)00148-4.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. 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.
  21. C. A. R. Hoare (1961): Algorithm 64: Quicksort. Commun. ACM 4(7), pp. 321, doi:10.1145/366622.366644.
  22. C.A.R. Hoare (1969): An Axiomatic Basis for Computer Programming. CACM 12(10), pp. 576–580, 583, doi:10.1145/363235.363259.
  23. C. J. Hogger (1981): Derivation of Logic Programs. Journal of the ACM 28(2), pp. 372–392, doi:10.1145/322248.322258.
  24. 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.
  25. 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.
  26. 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.
  27. 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.
  28. 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.
  29. 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.
  30. 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.
  31. 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.
  32. 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.
  33. M. Odersky, L. Spoon & B. Venners (2011): Programming in Scala: A Comprehensive Step-by-Step Guide, 2nd edition. Artima Incorporation, Sunnyvale, CA, USA.
  34. 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.
  35. 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.
  36. 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.
  37. 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.
  38. 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.
  39. 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.
  40. 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.
  41. 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.
  42. 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.
  43. 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.
  44. 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.
  45. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org