References

  1. Foto N. Afrati, Manolis Gergatsoulis & Francesca Toni (2003): Linearisability on Datalog programs. Theor. Comput. Sci. 308(1-3), pp. 199–226, doi:10.1016/S0304-3975(02)00730-2.
  2. Roberto Bagnara, Patricia M. Hill & Enea Zaffanella (2008): The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1-2), pp. 3–21, doi:10.1016/j.scico.2007.08.001.
  3. Christel Baier & Cesare Tinelli (2015): Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Lecture Notes in Computer Science 9035. Springer, doi:10.1007/978-3-662-46681-0.
  4. Dirk Beyer (2015): Software Verification and Verifiable Witnesses - (Report on SV-COMP 2015). In: Baier & Tinelli, pp. 401–416, doi:10.1007/978-3-662-46681-0_31.
  5. Nikolaj Bjørner, Kenneth L. McMillan & Andrey Rybalchenko (2013): On Solving Universally Quantified Horn Clauses. In: Francesco Logozzo & Manuel Fähndrich: SAS, LNCS 7935. Springer, pp. 105–125. Available at http://dx.doi.org/10.1007/978-3-642-38856-9_8.
  6. Patrick Cousot & Radhia Cousot (1977): Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Robert M. Graham, Michael A. Harrison & Ravi Sethi: POPL. ACM, pp. 238–252. Available at http://doi.acm.org/10.1145/512950.512973.
  7. Patrick Cousot & Nicolas Halbwachs (1978): POPL. ACM Press, pp. 84–96, doi:10.1145/512760.512770. Available at http://dl.acm.org/citation.cfm?id=512760.
  8. Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2014): VeriMAP: A Tool for Verifying Programs through Transformations. In: Erika Ábrahám & Klaus Havelund: TACAS, LNCS 8413. Springer, pp. 568–574. Available at http://dx.doi.org/10.1007/978-3-642-54862-8_47.
  9. Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2015): Proving correctness of imperative programs by linearizing constrained Horn clauses. TPLP 15(4-5), pp. 635–650, doi:10.1017/S1471068415000289.
  10. Bruno Dutertre (2014): Yices 2.2. In: Armin Biere & Roderick Bloem: Computer-Aided Verification (CAV'2014), Lecture Notes in Computer Science 8559. Springer, pp. 737–744, doi:10.1007/978-3-319-08867-9_49.
  11. Javier Esparza, Pierre Ganty, Stefan Kiefer & Michael Luttenberger (2011): Parikh's theorem: A simple and direct automaton construction. Inf. Process. Lett. 111(12), pp. 614–619, doi:10.1016/j.ipl.2011.03.019.
  12. Javier Esparza, Stefan Kiefer & Michael Luttenberger (2007): On Fixed Point Equations over Commutative Semirings. In: STACS 2007, 24th Annual Symposium on Theoretical Aspects of Computer Science, Proceedings, LNCS 4393. Springer, pp. 296–307, doi:10.1007/978-3-540-70918-3_26.
  13. J. P. Gallagher (1986): Transforming Logic Programs by Specialising Interpreters. In: Proceedings of the 7th European Conference on Artificial Intelligence (ECAI-86), Brighton, pp. 109–122.
  14. John P. Gallagher (1993): Tutorial on Specialisation of Logic Programs. In: David A. Schmidt: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'93, Copenhagen, Denmark, June 14-16, 1993. ACM, pp. 88–98, doi:10.1145/154630.154640. Available at http://dl.acm.org/citation.cfm?id=154630.
  15. Pierre Ganty, Radu Iosif & Filip Konečný (2013): Underapproximation of Procedure Summaries for Integer Programs. In: Nir Piterman & Scott A. Smolka: TACAS 2013. Proceedings, Lecture Notes in Computer Science 7795. Springer, pp. 245–259, doi:10.1007/978-3-642-36742-7_18.
  16. Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea & Andrey Rybalchenko (2012): HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution). In: Cormac Flanagan & Barbara König: TACAS, LNCS 7214. Springer, pp. 549–551. Available at http://dx.doi.org/10.1007/978-3-642-28756-5_46.
  17. Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea & Andrey Rybalchenko (2012): Synthesizing software verifiers from proof rules. In: Jan Vitek, Haibo Lin & Frank Tip: ACM SIGPLAN PLDI. ACM, pp. 405–416, doi:10.1145/2254064.2254112. Available at http://dl.acm.org/citation.cfm?id=2254064.
  18. Arie Gurfinkel, Temesghen Kahsai & Jorge A. Navas (2015): SeaHorn: A Framework for Verifying C Programs (Competition Contribution). In: Baier & Tinelli, pp. 447–450, doi:10.1007/978-3-662-46681-0_41.
  19. Manuel V. Hermenegildo, Francisco Bueno, Manuel Carro, Pedro López-García, Edison Mera, José F. Morales & Germán Puebla (2012): An overview of Ciao and its design philosophy. TPLP 12(1-2), pp. 219–252, doi:10.1017/S1471068411000457.
  20. Hossein Hojjat, Filip Konecný, Florent Garnier, Radu Iosif, Viktor Kuncak & Philipp Rümmer (2012): A Verification Toolkit for Numerical Transition Systems - Tool Paper. In: Dimitra Giannakopoulou & Dominique Méry: FM. Proceedings, Lecture Notes in Computer Science 7436. Springer, pp. 247–251, doi:10.1007/978-3-642-32759-9_21.
  21. N. Jones, C.K. Gomard & P. Sestoft (1993): Partial Evaluation and Automatic Software Generation. Prentice Hall.
  22. Neil D. Jones (2004): Transformation by interpreter specialisation. Sci. Comput. Program. 52, pp. 307–339, doi:10.1016/j.scico.2004.03.010.
  23. Bishoksan Kafle & John P Gallagher (2015): Horn clause verification with convex polyhedral abstraction and tree automata-based refinement. Computer Languages, Systems & Structures, doi:10.1016/j.cl.2015.11.001.
  24. Bishoksan Kafle, John P. Gallagher & Pierre Ganty (2015): Decomposition by tree dimension in Horn clause verification. In: Alexei Lisitsa, Andrei P. Nemytykh & Alberto Pettorossi: VPT., EPTCS 199, pp. 1–14, doi:10.4204/EPTCS.199.1.
  25. Michael Leuschel (1994): Partial Evaluation of the ``Real Thing". In: Laurent Fribourg & Franco Turini: LOPSTR, Proceedings, Lecture Notes in Computer Science 883. Springer, pp. 122–137, doi:10.1007/3-540-58792-6_8.
  26. Michael Leuschel, Daniel Elphick, Mauricio Varea, Stephen-John Craig & Marc Fontaine (2006): The Ecce and Logen partial evaluators and their web interfaces. In: John Hatcliff & Frank Tip: PEPM 2006. ACM, pp. 88–94, doi:10.1145/1111542.1111557.
  27. Michael Leuschel & Germán Vidal (2014): Fast offline partial evaluation of logic programs. Inf. Comput. 235, pp. 70–97, doi:10.1016/j.ic.2014.01.005.
  28. Michael Luttenberger & Maximilian Schlund (2016): Convergence of Newton's Method over Commutative Semirings. Inf. Comput. 246, pp. 43–61, doi:10.1016/j.ic.2015.11.008.
  29. Kenneth L. McMillan & Andrey Rybalchenko (2013): Solving Constrained Horn Clauses using Interpolation. Technical Report. Microsoft Research.
  30. Philipp Rümmer, Hossein Hojjat & Viktor Kuncak (2013): Disjunctive Interpolants for Horn-Clause Verification. In: Natasha Sharygina & Helmut Veith: CAV, Lecture Notes in Computer Science 8044. Springer, pp. 347–363, doi:10.1007/978-3-642-39799-8. Available at 10.1007/978-3-642-39799-8_24.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org