References

  1. 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.
  2. Christel Baier & Cesare Tinelli (2015): TACAS . Proceedings. LNCS 9035. Springer, doi:10.1007/978-3-662-46681-0.
  3. 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.
  4. Nikolaj Bjørner, Fabio Fioravanti, Andrey Rybalchenko & Valerio Senni (2014): Proceedings First Workshop on Horn Clauses for Verification and Synthesis, HCVS 2014, Vienna, Austria, 17 July 2014. EPTCS 169, doi:10.4204/EPTCS.169.
  5. Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan & Andrey Rybalchenko (2015): Horn Clause Solvers for Program Verification. In: Lev D. Beklemishev, Andreas Blass, Nachum Dershowitz, Bernd Finkbeiner & Wolfram Schulte: Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, LNCS 9300. Springer, pp. 24–51, doi:10.1007/978-3-319-23534-9_2.
  6. 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.
  7. H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison & M. Tommasi (2007): Tree Automata Techniques and Applications. Available on: http://www.grappa.univ-lille3.fr/tata. Release October, 12th 2007.
  8. P. Cousot & N. Halbwachs (1978): Automatic Discovery of Linear Restraints Among Variables of a Program. In: Proceedings of the 5th Annual ACM Symposium on Principles of Programming Languages, pp. 84–96, doi:10.1145/512760.512770.
  9. 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.
  10. William Craig (1957): Linear Reasoning. A New Form of the Herbrand-Gentzen Theorem. J. Symb. Log. 22(3), pp. 250–268, doi:10.2307/2963593.
  11. 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.
  12. 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.
  13. J. P. Gallagher & L. Lafave (1996): Regular Approximation of Computation Paths in Logic and Functional Languages. In: O. Danvy, R. Glück & P. Thiemann: Partial Evaluation, Springer-Verlag LNCS 1110, pp. 115–136. Available at http://dx.doi.org/10.1007/3-540-61580-6_7.
  14. John P. Gallagher, Mai Ajspur & Bishoksan Kafle (2015): An Optimised Algorithm for Determinisation and Completion of Finite Tree Automata. CoRR abs/1511.03595. Available at http://arxiv.org/abs/1511.03595.
  15. John P. Gallagher & Bishoksan Kafle (2014): Analysis and Transformation Tools for Constrained Horn Clause Verification. TPLP 14(4-5 (additional materials in online edition)), pp. 90–101. Available at http://journals.cambridge.org/action/displaySuppMaterial?cupCode=1&type=4&jid=TLP&volumeId=14&issueId=4-5&aid=9303163.
  16. 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 Conference on Programming Language Design and Implementation, PLDI '12, Beijing, China - June 11 - 16, 2012. ACM, pp. 405–416, doi:10.1145/2254064.2254112. Available at http://dl.acm.org/citation.cfm?id=2254064.
  17. Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli & Jorge A. Navas (2015): The SeaHorn Verification Framework. In: Daniel Kroening & Corina S. Pasareanu: CAV , Proceedings, Part I, LNCS 9206. Springer, pp. 343–361, doi:10.1007/978-3-319-21690-4_20.
  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. Matthias Heizmann, Jochen Hoenicke & Andreas Podelski (2009): Refinement of Trace Abstraction.. In: Jens Palsberg & Zhendong Su: Static Analysis, 16th International Symposium, SAS 2009, LNCS 5673. Springer, pp. 69–85, doi:10.1007/978-3-642-03237-0_7.
  20. Matthias Heizmann, Jochen Hoenicke & Andreas Podelski (2010): Nested interpolants. In: Manuel V. Hermenegildo & Jens Palsberg: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. ACM, pp. 471–482, doi:10.1145/1706299.1706353. Available at http://dl.acm.org/citation.cfm?id=1706299.
  21. Matthias Heizmann, Jochen Hoenicke & Andreas Podelski (2013): Software Model Checking for People Who Love Automata. In: Sharygina & Veith, pp. 36–52, doi:10.1007/978-3-642-39799-8_2.
  22. 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.
  23. 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 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, LNCS 7436. Springer, pp. 247–251, doi:10.1007/978-3-642-32759-9_21.
  24. Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas & Andrew E. Santosa (2012): TRACER: A Symbolic Execution Tool for Verification. In: P. Madhusudan & Sanjit A. Seshia: CAV, LNCS 7358. Springer, pp. 758–766. Available at http://dx.doi.org/10.1007/978-3-642-31424-7_61.
  25. Ranjit Jhala & Kenneth L. McMillan (2006): A Practical and Complete Approach to Predicate Refinement. In: Holger Hermanns & Jens Palsberg: TACAS, LNCS 3920. Springer, pp. 459–473. Available at http://dx.doi.org/10.1007/11691372_33.
  26. Bishoksan Kafle & John P. Gallagher (2015): Constraint Specialisation in Horn Clause Verification. In: Kenichi Asai & Kostis Sagonas: Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM, Mumbai, India, January 15-17, 2015. ACM, pp. 85–90, doi:10.1145/2678015.2682544. Available at http://dl.acm.org/citation.cfm?id=2678015.
  27. 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.
  28. Kenneth L. McMillan & Andrey Rybalchenko (2013): Solving Constrained Horn Clauses using Interpolation. Technical Report. Microsoft Research.
  29. Philipp Rümmer, Hossein Hojjat & Viktor Kuncak (2013): Disjunctive Interpolants for Horn-Clause Verification. In: Sharygina & Veith, pp. 347–363, doi:10.1007/978-3-642-39799-8_24.
  30. Andrey Rybalchenko & Viorica Sofronie-Stokkermans (2010): Constraint solving for interpolation. J. Symb. Comput. 45(11), pp. 1212–1233. Available at http://dx.doi.org/10.1016/j.jsc.2010.06.005.
  31. Natasha Sharygina & Helmut Veith (2013): Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. LNCS 8044. Springer, doi:10.1007/978-3-642-39799-8.
  32. Robert F. Stärk (1989): A Direct Proof for the Completeness of SLD-Resolution. In: Egon Börger, Hans Kleine Büning & Michael M. Richter: CSL '89, 3rd Workshop on Computer Science Logic, Kaiserslautern, Germany, October 2-6, 1989, Proceedings, LNCS 440. Springer, pp. 382–383.
  33. Weifeng Wang & Li Jiao (2015): Trace abstraction refinement for solving Horn clauses. Technical Report ISCAS-SKLCS-15-19. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences. Available on: http://lcs.ios.ac.cn/~wangwf/TechReportISCAS-SKLCS-15-19.pdf.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org