References

  1. The MAP transformation system. Available at www.iasi.cnr.it/~proietti/system.html.
  2. Aws Albarghouthi, Arie Gurfinkel & Marsha Chechik (2012): Craig Interpretation. In: Proceedings of SAS, pp. 300–316, doi:10.1007/978-3-642-33125-1_21.
  3. Aws Albarghouthi, Arie Gurfinkel & Marsha Chechik (2012): From Under-Approximations to Over-Approximations and Back. In: Proceedings of TACAS, pp. 157–172, doi:10.1007/978-3-642-28756-5_12.
  4. Aws Albarghouthi, Yi Li, Arie Gurfinkel & Marsha Chechik (2012): Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification. In: Proceedings of CAV, pp. 672–678, doi:10.1007/978-3-642-31424-7_48.
  5. Elvira Albert, Miguel Gómez-Zamalloa, Laurent Hubert & Germán Puebla (2007): Verification of Java Bytecode Using Analysis and Transformation of Logic Programs. In: Proceedings of PADL, pp. 124–139, doi:10.1007/978-3-540-69611-7_8.
  6. Roberto Bagnara, Patricia M. Hill & E.nea Zaffanella (2008): The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming 72(1-2), pp. 3–21, doi:10.1016/j.scico.2007.08.001.
  7. Dirk Beyer (2013): Competition on Software Verification - (SV-COMP). In: Proceedings of TACAS, pp. 594–609, doi:10.1007/978-3-642-36742-7_43.
  8. Nikolaj Bjørner, Kenneth McMillan & Andrey Rybalchenko (2012): Program Verification as Satisfiability Modulo Theories. In: Proceedings of SMT, pp. 3–11.
  9. Aaron R. Bradley (2011): SAT-Based Model Checking without Unrolling. In: Proceedings of VMCAI, LNCS 6538. Springer, pp. 70–87, doi:10.1007/978-3-642-18275-4_7.
  10. P. Chico de Guzmán, M. Carro, M. V. Hermenegildo & P. J. Stuckey (2012): A General Implementation Framework for Tabled CLP. In: Proceedings of FLOPS, pp. 104–119, doi:10.1007/978-3-642-29822-6_11.
  11. Alessandro Cimatti, Alberto Griggio, Bastiaan Schaafsma & Roberto Sebastiani (2013): The MathSAT5 SMT Solver. In: Nir Piterman & Scott Smolka: Proceedings of TACAS, LNCS 7795. Springer, doi:10.1007/978-3-642-36742-7_7.
  12. Philippe Codognet (1995): A Tabulation Method for Constraint Logic Programming. In: Symposium and Exhibition on Industrial Applications of Prolog.
  13. Patrick Cousot & Radhia Cousot (1977): Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proceedings of POPL. ACM, pp. 238–252, doi:10.1145/512950.512973.
  14. W. Craig (1957): Linear Reasoning: A New Form of the Herbrand-Gentzen Theorem. Journal of Symbolic Logic 22(3), pp. 250–268, doi:10.2307/2963593.
  15. Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2013): Specialization with Constrained Generalization for Software Model Checking. In: Proceedings of LOPSTR, LNCS 7844. Springer, pp. 51–70, doi:10.1007/978-3-642-38197-3_5.
  16. Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2014): Program Verification via Iterated Specialization. Science of Computer Programming (Special Issue on PEPM 2013), doi:10.1016/j.scico.2014.05.017.
  17. Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2014): VeriMAP: A Tool for Verifying Programs through Transformations. In: Proceedings of TACAS, pp. 568–574, doi:10.1007/978-3-642-54862-8_47.
  18. Gregory J. Duck, Joxan Jaffar & Nicolas C. H. Koh (2013): Constraint-Based Program Reasoning with Heaps and Separation. In: Proceedings of CP, LNCS 8124. Springer, pp. 282–298, doi:10.1007/978-3-642-40627-0_24.
  19. Sandro Etalle & Maurizio Gabbrielli (1996): Transformations of CLP Modules. Theoretical Computer Science 166(1&2), pp. 101–146, doi:10.1016/0304-3975(95)00148-4.
  20. Fabio Fioravanti, Alberto Pettorossi & Maurizio Proietti (2000): Automated strategies for specializing constraint logic programs. In: Proceedings of LOPSTR, doi:10.1007/3-540-45142-0_8.
  21. Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti & Valerio Senni (2013): Generalization Strategies for the Verification of Infinite State Systems. Theory and Practice of Logic Programming 13(2), pp. 175–199, doi:10.1017/S1471068411000627.
  22. John P. Gallagher & Bishoksan Kafle (2014): Analysis and Transformation Tools for Constrained Horn Clause Verification. In: Proceedings of ICLP (to appear).
  23. Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard & Peter J. Stuckey (2013): Failure tabled constraint logic programming by interpolation. Theory and Practice of Logic Programming 13(4-5), pp. 593–607, doi:10.1017/S1471068413000379.
  24. Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea & Andrey Rybalchenko (2012): Synthesizing Software Verifiers from Proof Rules. In: Proceedings of PLDI, pp. 405–416, doi:10.1145/2254064.2254112.
  25. Bhargav S. Gulavani, Supratik Chakraborty, Aditya V. Nori & Sriram K. Rajamani (2008): Automatically Refining Abstract Interpretations. In: Proceedings of TACAS, pp. 443–458, doi:10.1007/978-3-540-78800-3_33.
  26. Bhargav S. Gulavani & Sriram K. Rajamani (2006): Counterexample Driven Refinement for Abstract Interpretation. In: Proceedings of TACAS, pp. 474–488, doi:10.1007/11691372_34.
  27. Ashutosh Gupta & Andrey Rybalchenko (2009): InvGen: An Efficient Invariant Generator. In: Proceedings of CAV, pp. 634–640, doi:10.1007/978-3-642-02658-4_48.
  28. Nicolas Halbwachs, Yann-Erick Proy & Patrick Roumanoff (1997): Verification of Real-Time Systems using Linear Relation Analysis. Formal Methods in System Design 11(2), pp. 157–185, doi:10.1023/A:1008678014487.
  29. Krystof Hoder, Nikolaj Bjørner & Leonardo Mendonça de Moura (2011): μZ - An Efficient Engine for Fixed Points with Constraints. In: Proceedings of CAV, pp. 457–462, doi:10.1007/978-3-642-22110-1_36.
  30. J. Jaffar & J. Lassez (1987): Constraint Logic Programming. In: Proceedings of POPL, pp. 111–119, doi:10.1145/41625.41635.
  31. J. Jaffar, A. E. Santosa & R. Voicu (2009): An Interpolation Method for CLP Traversal. In: Proceedings of CP, pp. 454–469, doi:10.1007/978-3-642-04244-7_37.
  32. Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas & Andrew E. Santosa (2012): TRACER: A Symbolic Execution Tool for Verification. In: Proceedings of CAV, pp. 758–766, doi:10.1007/978-3-642-31424-7_61.
  33. Kenneth McMillan & Andrey Rybalchenko (2013): Computing Relational Fixed Points using Interpolation. Technical Report. MSR-TR-2013-6.
  34. Kenneth L. McMillan (2010): Lazy Annotation for Program Testing and Verification. In: Proceedings of CAV, pp. 104–118, doi:10.1007/978-3-642-14295-6_10.
  35. Leonardo Mendonça de Moura & Nikolaj Bjørner (2008): Z3: An Efficient SMT Solver. In: Proceedings of TACAS, pp. 337–340, doi:10.1007/978-3-540-78800-3_24.
  36. George C. Necula, Scott McPeak, Shree Prakash Rahul & Westley Weimer (2002): CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In: Proceedings of CC, pp. 213–228, doi:10.1007/3-540-45937-5_16.
  37. J. C. Peralta, J. P. Gallagher & H. Saglam (1998): Analysis of Imperative Programs through Analysis of Constraint Logic Programs. In: 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.
  38. Germán Puebla, Elvira Albert & Manuel V. Hermenegildo (2006): Abstract Interpretation with Specialized Definitions. In: Proceedings of SAS, pp. 107–126, doi:10.1007/11823230_8.
  39. Philipp Rümmer, Hossein Hojjat & Viktor Kuncak (2013): Disjunctive Interpolants for Horn-Clause Verification. In: Proceedings of CAV, pp. 347–363, doi:10.1007/978-3-642-39799-8_24.
  40. Yakir Vizel & Arie Gurfinkel (2014): Interpolating Property Directed Reachability. In: Proceedings of CAV, doi:10.1007/978-3-319-08867-9_17.
  41. Chao Wang, Zijiang Yang, Aarti Gupta & Franjo Ivancic (2007): Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra. In: Proceedings of CAV, pp. 352–365, doi:10.1007/978-3-540-73368-3_40.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org