References

  1. R. Bagnara, P. M. Hill & E. 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. Available at http://dx.doi.org/10.1016/j.scico.2007.08.001.
  2. T. Ball, V. Levin & S. K. Rajamani (2011): A decade of software model checking with SLAM. Commun. ACM 54(7), pp. 68–76. Available at http://doi.acm.org/10.1145/1965724.1965743.
  3. F. Bancilhon, D. Maier, Y. Sagiv & J. Ullman (1986): Magic Sets and other strange ways to implement logic programs. In: Proceedings of the 5th ACM SIGMOD-SIGACT Symposium on Principles of Database Systems. Available at http://dx.doi.org/10.1145/6012.15399.
  4. F. Benoy & A. King (1996): Inferring Argument Size Relationships with CLP(R). In: J. P. Gallagher: Logic-Based Program Synthesis and Transformation (LOPSTR'96), Springer-Verlag Lecture Notes in Computer Science 1207, pp. 204–223. Available at http://dx.doi.org/10.1007/3-540-62718-9_12.
  5. D. Beyer (2013): Second Competition on Software Verification - (Summary of SV-COMP 2013). In: N. Piterman & S. A. Smolka: TACAS, Lecture Notes in Computer Science 7795. Springer, pp. 594–609. Available at http://dx.doi.org/10.1007/978-3-642-36742-7_43.
  6. D. Beyer, T. A. Henzinger, R. Majumdar & A. Rybalchenko (2007): Path invariants. In: J. Ferrante & K. S. McKinley: PLDI. ACM, pp. 300–309. Available at http://doi.acm.org/10.1145/1250734.1250769.
  7. N. Bjørner, K. L. McMillan & A. Rybalchenko (2013): On Solving Universally Quantified Horn Clauses. In: F. Logozzo & M. Fähndrich: SAS, Lecture Notes in Computer Science 7935. Springer, pp. 105–125. Available at http://dx.doi.org/10.1007/978-3-642-38856-9_8.
  8. R. Blanc, A. Gupta, L. Kovács & B. Kragl (2013): Tree Interpolation in Vampire. In: K. L. McMillan, A. Middeldorp & A. Voronkov: LPAR, Lecture Notes in Computer Science 8312. Springer, pp. 173–181. Available at http://dx.doi.org/10.1007/978-3-642-45221-5_13.
  9. F. Bueno, D. Cabeza, M. Carro, M. Hermenegildo, P. López-García & G. Puebla (1997): The Ciao Prolog system. Reference manual. Technical Report CLIP3/97.1. School of Computer Science, Technical University of Madrid (UPM). Available from http://www.clip.dia.fi.upm.es/.
  10. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu & H. Veith (2003): Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), pp. 752–794. Available at http://doi.acm.org/10.1145/876638.876643.
  11. P. Cousot & R. Cousot (1977): Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: R. M. Graham, M. A. Harrison & R. Sethi: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977. ACM, pp. 238–252. Available at http://dl.acm.org/citation.cfm?id=512950.
  12. P. Cousot & N. Halbwachs (1978): Automatic Discovery of Linear Restraints Among Variables of a Program. In: A. V. Aho, S. N. Zilles & T. G. Szymanski: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978. ACM Press, pp. 84–96. Available at http://dl.acm.org/citation.cfm?id=512760.
  13. E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014): Program verification via iterated specialization. Sci. Comput. Program. 95, pp. 149–175. Available at http://dx.doi.org/10.1016/j.scico.2014.05.017.
  14. E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014): VeriMAP: A Tool for Verifying Programs through Transformations. In: E. Ábrahám & K. Havelund: TACAS, Lecture Notes in Computer Science 8413. Springer, pp. 568–574. Available at http://dx.doi.org/10.1007/978-3-642-54862-8_47.
  15. S. Debray & R. Ramakrishnan (1994): Abstract Interpretation of Logic Programs Using Magic Transformations. Journal of Logic Programming 18, pp. 149–176. Available at http://dx.doi.org/10.1016/0743-1066(94)90050-7.
  16. F. Fioravanti, A. Pettorossi & M. Proietti (2002): Specialization with Clause Splitting for Deriving Deterministic Constraint Logic Programs. In: In Proc. IEEE Conference on Systems, Man and Cybernetics, Hammamet. IEEE Press. Available at http://dx.doi.org/10.1109/ICSMC.2002.1167971.
  17. F. Fioravanti, A. Pettorossi, M. Proietti & V. Senni (2013): Controlling Polyvariance for Specialization-based Verification. Fundam. Inform. 124(4), pp. 483–502. Available at http://dx.doi.org/10.3233/FI-2013-845.
  18. 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 Lecture Notes in Computer Science 1110, pp. 115–136. Available at http://dx.doi.org/10.1007/3-540-61580-6_7.
  19. G. Gange, J. A. Navas, P. Schachte, H. Søndergaard & P. J. Stuckey (2013): Failure tabled constraint logic programming by interpolation. TPLP 13(4-5), pp. 593–607. Available at http://dx.doi.org/10.1017/S1471068413000379.
  20. S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea & A. Rybalchenko (2012): HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution). In: C. Flanagan & B. König: TACAS, LNCS 7214. Springer, pp. 549–551. Available at http://dx.doi.org/10.1007/978-3-642-28756-5_46.
  21. A. Gupta, C. Popeea & A. Rybalchenko (2011): Solving Recursion-Free Horn Clauses over LI+UIF. In: H. Yang: APLAS, Lecture Notes in Computer Science 7078. Springer, pp. 188–203. Available at http://dx.doi.org/10.1007/978-3-642-25318-8_16.
  22. A. Gupta & A. Rybalchenko (2009): InvGen: An Efficient Invariant Generator. In: A. Bouajjani & O. Maler: CAV, Lecture Notes in Computer Science 5643. Springer, pp. 634–640. Available at http://dx.doi.org/10.1007/978-3-642-02658-4_48.
  23. N. Halbwachs, Y. E. Proy & P. Raymound (1994): Verification of Linear hybrid systems by means of convex approximations. In: Proceedings of the First Symposium on Static Analysis, LNCS 864, pp. 223–237. Available at http://dx.doi.org/10.1007/3-540-58485-4_43.
  24. J. Jaffar & M. Maher (1994): Constraint Logic Programming: A Survey. Journal of Logic Programming 19/20, pp. 503–581. Available at http://dx.doi.org/10.1016/0743-1066(94)90033-7.
  25. J. Jaffar, V. Murali, J. A. Navas & A. E. Santosa (2012): TRACER: A Symbolic Execution Tool for Verification. In: P. Madhusudan & S. A. Seshia: CAV, Lecture Notes in Computer Science 7358. Springer, pp. 758–766. Available at http://dx.doi.org/10.1007/978-3-642-31424-7_61.
  26. J. Jaffar, J. A. Navas & A. E. Santosa (2011): Unbounded Symbolic Execution for Program Verification. In: S. Khurshid & K. Sen: RV, Lecture Notes in Computer Science 7186. Springer, pp. 396–411. Available at http://dx.doi.org/10.1007/978-3-642-29860-8_32.
  27. L. Lakhdar-Chaouch, B. Jeannet & A. Girault (2011): Widening with Thresholds for Programs with Complex Control Graphs. In: T. Bultan & P.-A. Hsiung: ATVA 2011, Lecture Notes in Computer Science 6996. Springer, pp. 492–502. Available at http://dx.doi.org/10.1007/978-3-642-24372-1_38.
  28. M. Leuschel & T. Massart (1999): Infinite State Model Checking by Abstract Interpretation and Program Specialisation. In: A. Bossi: LOPSTR'99, Lecture Notes in Computer Science 1817. Springer, pp. 62–81. Available at http://dx.doi.org/10.1007/10720327_5.
  29. G. Levi (2000): Abstract Interpretation Based Verification of Logic Programs. Electr. Notes Theor. Comput. Sci. 40, pp. 243. Available at http://dx.doi.org/10.1016/S1571-0661(05)80052-0.
  30. A. Pettorossi & M. Proietti (2000): Perfect Model Checking via Unfold/Fold Transformations. In: J. W. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.-K. Lau, C. Palamidessi, L. M. Pereira, Y. Sagiv & P. J. Stuckey: Computational Logic, Lecture Notes in Computer Science 1861. Springer, pp. 613–628. Available at http://dx.doi.org/10.1007/3-540-44957-4_41.
  31. A. Rybalchenko & V. 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.
  32. W. H. Winsborough (1989): Path-Dependent Reachability Analysis for Multiple Specialization.. In: E. L. Lusk & R. A. Overbeek: NACLP. MIT Press, pp. 133–153. Available at http://dblp.uni-trier.de/db/conf/slp/slp89.html#Winsborough89.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org