References

  1. F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise & N. Sharygina (2012): SAFARI: SMT-based Abstraction For Arrays with Interpolants. In: Proceedings of the 24th International Conference on Computer Aided Verification, CAV '12, Lecture Notes in Computer Science 7358. Springer, pp. 679–685, doi:10.1007/978-3-642-31424-7_49.
  2. D. Beyer, T. A. Henzinger, R. Majumdar & A. Rybalchenko (2007): Invariant Synthesis for Combined Theories. In: Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI '07, Lecture Notes in Computer Science 4349. Springer, pp. 378–394, doi:10.1007/978-3-540-69738-1_27.
  3. B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux & X. Rival (2002): Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software. In: The Essence of Computation, Lecture Notes in Computer Science 2566. Springer, pp. 85–108, doi:10.1007/3-540-36377-7_5.
  4. Aaron R. Bradley, Zohar Manna & Henny B. Sipma (2006): What's decidable about arrays?. In: Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI '06, Lecture Notes in Computer Science 3855. Springer, pp. 427–442, doi:10.1007/11609773_28.
  5. M. Bravenboer & Y. Smaragdakis (2009): Strictly declarative specification of sophisticated points-to analyses. In: S. Arora & G. T. Leavens: Proceedings of the 24th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA '09. ACM, pp. 243–262, doi:10.1145/1640089.1640108.
  6. 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.
  7. P. Cousot & R. Cousot (1977): Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction of Approximation of Fixpoints. In: Proceedings of the 4th ACM-SIGPLAN Symposium on Principles of Programming Languages, POPL '77. ACM, pp. 238–252, doi:10.1145/512950.512973.
  8. P. Cousot, R. Cousot & F. Logozzo (2011): A parametric segmentation functor for fully automatic and scalable array content analysis. In: Proceedings of the 38th ACM Symposium on Principles of programming languages, POPL '11. ACM, pp. 105–118, doi:10.1145/1926385.1926399.
  9. P. Cousot & N. Halbwachs (1978): Automatic Discovery of Linear Restraints among Variables of a Program. In: Proceedings of the Fifth ACM Symposium on Principles of Programming Languages, POPL '78. ACM, pp. 84–96, doi:10.1145/512760.512770.
  10. B. Cui & D. S. Warren (2000): A System for Tabled Constraint Logic Programming. In: J. W. Lloyd: Proceedings of the First International Conference on Computational Logic, CL 2000, London, UK, July 24-28, 2000, Lecture Notes in Artificial Intelligence 1861. Springer-Verlag, pp. 478–492, doi:10.1007/3-540-44957-4_32.
  11. E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2013): Specialization with Constrained Generalization for Software Model Checking. In: Proceedings of the 22nd International Symposium Logic-Based Program Synthesis and Transformation, LOPSTR '12, Lecture Notes in Computer Science 7844, pp. 51–70, doi:10.1007/978-3-642-38197-3_5.
  12. E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2013): Verifying Programs via Iterated Specialization. In: Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM '13. ACM, pp. 43–52, doi:10.1145/2426890.2426899.
  13. D. De Schreye, R. Glück, J. Jørgensen, M. Leuschel, B. Martens & M. H. Sørensen (1999): Conjunctive Partial Deduction: Foundations, Control, Algorithms, and Experiments. Journal of Logic Programming 41(2–3), pp. 231–277, doi:10.1016/S0743-1066(99)00030-8.
  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. F. Fioravanti, A. Pettorossi & M. Proietti (2004): Transformation Rules for Locally Stratified Constraint Logic Programs. In: K.-K. Lau & M. Bruynooghe: Program Development in Computational Logic, Lecture Notes in Computer Science 3049. Springer-Verlag, pp. 292–340, doi:10.1007/978-3-540-25951-0_10.
  18. F. Fioravanti, A. Pettorossi, M. Proietti & V. Senni (2011): Improving Reachability Analysis of Infinite State Systems by Specialization. In: G. Delzanno & I. Potapov: Proceedings of the 5th International Workshop on Reachability Problems, RP '11, September 28-30, 2011, Genova, Italy, Lecture Notes in Computer Science 6945. Springer, pp. 165–179, doi:10.1007/978-3-642-24288-5_15.
  19. F. Fioravanti, A. Pettorossi, M. Proietti & V. Senni (2013): Generalization Strategies for the Verification of Infinite State Systems. Theory and Practice of Logic Programming. Special Issue on the 25th Annual GULP Conference 13(2), pp. 175–199, doi:10.1017/S1471068411000627.
  20. C. Flanagan (2004): Automatic software model checking via constraint logic. Sci. Comput. Program. 50(1–3), pp. 253–270, doi:10.1016/j.scico.2004.01.006.
  21. C. Flanagan & S. Qadeer (2002): Predicate abstraction for software verification. In: Proceedings of the 29th ACM Symposium on Principles of programming languages, POPL '02. ACM, pp. 191–202, doi:10.1145/503272.503291.
  22. D. Gopan, T. W. Reps & S. Sagiv (2005): A framework for numeric analysis of array operations. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of programming languages, POPL '05. ACM, pp. 338–350, doi:10.1145/1047659.1040333.
  23. S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea & A. Rybalchenko (2012): HSF(C): A Software Verifier based on Horn Clauses. In: C. Flanagan & B. König: Proc. of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS '12, Lecture Notes in Computer Science 7214. Springer, pp. 549–551, doi:10.1007/978-3-642-28756-5_46.
  24. 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. ACM, pp. 405–416, doi:10.1145/2345156.2254112.
  25. B. S. Gulavani, S. Chakraborty, A. V. Nori & S. K. Rajamani (2008): Automatically Refining Abstract Interpretations. In: Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS '08, Lecture Notes in Computer Science 4963. Springer, pp. 443–458, doi:10.1007/978-3-540-78800-3_33.
  26. N. Halbwachs & M. Péron (2008): Discovering properties about arrays in simple programs. In: Proceedings of the ACM Conference on Programming language design and implementation, PLDI '08. ACM, pp. 339–348, doi:10.1145/1375581.1375623.
  27. K. S. Henriksen & J. P. Gallagher (2006): Abstract Interpretation of PIC Programs through Logic Programming. In: Proceedings of the 6th IEEE International Workshop on Source Code Analysis and Manipulation, SCAM '06. IEEE, pp. 103 – 179, doi:10.1016/0743-1066(92)90030-7.
  28. J. Jaffar & M. Maher (1994): Constraint Logic Programming: A Survey. Journal of Logic Programming 19/20, pp. 503–581, doi:10.1016/0743-1066(94)90033-7.
  29. J. Jaffar, J. A. Navas & A. E. Santosa (2012): TRACER: A Symbolic Execution Tool for Verification, doi:10.1007/978-3-642-31424-7_61.
  30. J. Jaffar, J. A. Navas & A. E. Santosa (2012): Unbounded Symbolic Execution for Program Verification. In: Proceedings of the 2nd International Conference on Runtime Verification, RV '11, Lecture Notes in Computer Science 7186. Springer, pp. 396–411, doi:10.1007/978-3-642-29860-8_32.
  31. R. Jhala & R. Majumdar (2009): Software model checking. ACM Computing Surveys 41(4), pp. 21:1–21:54, doi:10.1145/1592434.1592438.
  32. R. Jhala & K. L. McMillan (2007): Array abstractions from proofs. In: Proceedings of the 19th International Conference on Computer Aided Verification, CAV '07, Lecture Notes in Computer Science 4590. Springer, pp. 193–206, doi:10.1007/978-3-540-73368-3_23.
  33. N. D. Jones, C. K. Gomard & P. Sestoft (1993): Partial Evaluation and Automatic Program Generation. Prentice Hall.
  34. L. Kovács & A. Voronkov (2009): Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. In: Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering, FASE '09, Lecture Notes in Computer Science 5503. Springer, pp. 470–485, doi:10.1007/978-3-642-00593-0_33.
  35. S. K. Lahiri & R. E. Bryant (2007): Predicate abstraction with indexed predicates. ACM Trans. Comput. Log. 9(1). ACM, doi:10.1145/1297658.1297662.
  36. D. Larraz, E. Rodríguez-Carbonell & A. Rubio (2013): SMT-Based Array Invariant Generation. In: 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI '13, Rome, Italy, January 20-22, 2013, Lecture Notes in Computer Science 7737. Springer, pp. 169–188, doi:10.1007/978-3-642-35873-9_12.
  37. M. Leuschel & M. Bruynooghe (2002): Logic program specialisation through partial deduction: Control issues. Theory and Practice of Logic Programming 2(4&5), pp. 461–515, doi:10.1017/S147106840200145X.
  38. MAP: The MAP transformation system.
  39. K. L. McMillan (2008): Quantified invariant generation using an interpolating saturation prover. In: Proceedings of 14th international conference on Tools and algorithms for the construction and analysis of systems, TACAS '08, Lecture Notes in Computer Science 4963. Springer, pp. 413–427, doi:10.1007/978-3-540-78800-3_31.
  40. S. P. Miller, M. W. Whalen & D. D. Cofer (2010): Software model checking takes off. Commun. ACM 53(2). ACM, pp. 58–64, doi:10.1145/1646353.1646372.
  41. U. Nilsson & J. Lübcke (2000): Constraint Logic Programming for Local and Symbolic Model-Checking. In: J. W. Lloyd: Proceedings of the First International Conference on Computational Logic, CL 2000, London, UK, July 24-28, 2000, Lecture Notes in Artificial Intelligence 1861. Springer-Verlag, pp. 384–398, doi:10.1007/3-540-44957-4_26.
  42. J. C. Peralta & J. P. Gallagher (2003): Convex Hull Abstractions in Specialization of CLP Programs. In: M. Leuschel: Logic Based Program Synthesis and Tranformation, 12th International Workshop, LOPSTR '02, Madrid, Spain, September 17–20, 2002, Revised Selected Papers, Lecture Notes in Computer Science 2664. Springer, pp. 90–108, doi:10.1007/3-540-45013-0_8.
  43. 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.
  44. 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.
  45. T. W. Reps (1998): Program analysis via graph reachability. Information and Software Technology 40(11–12), pp. 701–726, doi:10.1016/S0950-5849(98)00093-7.
  46. A. Rybalchenko (2010): Constraint Solving for Program Verification: Theory and Practice by Example. In: T. Touili, B. Cook & P. Jackson: Proceedings of the 22nd International Conference on Computer Aided Verification, CAV '10, Lecture Notes in Computer Science 6174. Springer, pp. 57–71, doi:10.1007/978-3-642-14295-6_7.
  47. A. Rybalchenko & V. Sofronie-Stokkermans (2010): Constraint solving for interpolation. Journal of Symbolic Computation 45(11), pp. 1212–1233, doi:10.1007/978-3-540-69738-1_25.
  48. D. A. Schmidt (1998): Data flow analysis is model checking of abstract interpretations. In: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '98. ACM, pp. 38–48, doi:10.1145/268946.268950.
  49. M. N. Seghir, A. Podelski & T. Wies (2009): Abstraction Refinement for Quantified Array Assertions. In: Proceeding of the 16th International Symposium on Static Analysis, SAS '09, Lecture Notes in Computer Science 5673. Springer, pp. 3–18, doi:10.1007/978-3-642-03237-0_3.
  50. 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.
  51. H. Tamaki & T. Sato (1986): A Generalized Correctness Proof of the Unfold/Fold Logic Program Transformation. Technical Report 86-4. Ibaraki University, Japan.
  52. J. Whaley & M. S. Lam (2004): Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In: Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, PLDI '04. ACM, pp. 131–144, doi:10.1145/996841.996859.

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