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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
S. Etalle & M. Gabbrielli (1996):
Transformations of CLP Modules.
Theoretical Computer Science 166,
pp. 101–146,
doi:10.1016/0304-3975(95)00148-4.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
R. Jhala & R. Majumdar (2009):
Software model checking.
ACM Computing Surveys 41(4),
pp. 21:1–21:54,
doi:10.1145/1592434.1592438.
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.
N. D. Jones, C. K. Gomard & P. Sestoft (1993):
Partial Evaluation and Automatic Program Generation.
Prentice Hall.
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.
S. K. Lahiri & R. E. Bryant (2007):
Predicate abstraction with indexed predicates.
ACM Trans. Comput. Log. 9(1).
ACM,
doi:10.1145/1297658.1297662.
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.
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.
MAP:
The MAP transformation system.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
H. Tamaki & T. Sato (1986):
A Generalized Correctness Proof of the Unfold/Fold Logic Program Transformation.
Technical Report 86-4.
Ibaraki University,
Japan.
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.