Property-directed incremental invariant generation

Armoni R, Fix L, Fraer R, Huddleston S, Piterman N, Vardi M (2004) SAT-based induction for temporal safety properties. In: BMC Aiken A (1999) Introduction to set constraint-based program analysis. Sci Comput Program 35: 79–111 Awedh M, Somenzi F (2006) Automatic invariant strengthening to prove properties in bounded model checking. In: DAC. ACM Press, New York, pp 1073–1076 Avis D (1998) LRS: a revised implementation of the reverse search vertex enumeration algorithm. Technical Report, McGill Aiken A, Wimmers E (1992) Solving systems of set constraints. In: LICS, pp 329–340 Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without bdds. In: TACAS, London, UK. Springer, Berlin, pp 193–207 Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inform Comput 98(2): 142–170 Bradley AR, Manna Z (2006) Verification constraint problems with strengthening In: ICTAC, Lecture Notes in Computer Science, vol 3722. Springer, Berlin Bradley AR, Manna Z (2007) The calculus of computation: decision procedures with applications to verification. Springer, Berlin Bradley AR, Manna Z (2007) Checking safety by inductive generalization of counterexamples to induction. In: FMCAD Bradley AR, Manna Z, Sipma HB (2005) Linear ranking with reachability. In: CAV, Lecture Notes in Computer Science, vol 3576. Springer, Berlin, pp 491–504 Boyd S, Yang Q (1989) Structured and simultaneous Lyapunov functions for system stability problems. Int J Control 49(6): 2215–2240 Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of programming languages. ACM Press, New York, pp 238–252 Clarke EM, Allen Emerson E (1982) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of programs. Springer, Berlin, pp 52–71 Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Allan Emerson E, Sistla P (eds) CAV, Lecture Notes in Computer Science, vol 1855, Chicago, July 2000. Springer, Berlin, pp 154–169 Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50(5): 752–794 Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among the variables of a program. In: Principles of programming languages. ACM Press, New York, pp 84–96 Collins GE (1975) Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage H (eds) Automata theory and formal languages, Lecture Notes in Computer Science, vol 33. Springer, Berlin, pp 134–183 Cousot P (2005) Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: VMCAI, pp 1–24 Colón M, Sipma HB (2001) Synthesis of linear ranking functions. In: TACAS, Lecture Notes in Computer Science, vol 2031. Springer, Berlin, pp 67–81 Colón M, Sipma HB (2002) Practical methods for proving program termination. In: CAV, Lecture Notes in Computer Science, vol 2404. Springer, Berlin, pp 442–454 Colón M, Sankaranarayanan S, Sipma HB (2003) Linear invariant generation using non-linear constraint solving. In: CAV, Lecture Notes in Computer Science, vol 2725. Springer, Berlin, pp 420–433 de Moura L, Ruess H, Sorea M (2003) Bounded model checking and induction: from refutation to verification. In: CAV, Lecture Notes in Computer Science. Springer, Berlin Floyd RW (1967) Assigning meanings to programs. In: Symposia in applied mathematics, vol 19. American Mathematical Society, pp 19–32 Graf S, Saidi H (1997) Construction of abstract state graphs with PVS. In: CAV, Lecture Notes in Computer Science, vol 1254. Springer, Berlin, pp 72–83 Hardware model checking competition 2007 (HWMCC’07) Jain H, Kroening D, Sharygina N, Clarke EM (2005) Word level predicate abstraction and refinement for verifying RTL verilog. In: DAC Jin H, Somenzi F (2005) Prime clauses for fast enumeration of satisfying assignments to boolean circuits. In: DAC. ACM Press, New York, pp 750–753 Conflict detection for arbitrary constraint propagation algorithms. In: IJCAI Workshop on Modelling and Solving Problems with Constraints Karr M (1976) Affine relationships among variables of a program. Acta Inform 6: 133–151 Katz SM, Manna Z (1975) A closer look at termination. Acta Inform 5(4): 333–352 Knaster B (1928) Un the̠ore̠me sur les fonctions d’ensembles. Ann Soc Polon Math 6: 133–134 McMillan KL, Amla N (2003) Automatic abstraction without counterexamples. In: TACAS, pp 2–17 McMillan KL (2002) Applying SAT methods in unbounded symbolic model checking. In: CAV, Lecture Notes in Computer Science, vol 2404. Springer, Berlin, pp 250–264 McMillan KL (2003) Interpolation and SAT-based model checking. In: CAV, Lecture Notes in Computer Science, vol 2725. Springer, Berlin, pp 1–13 McMillan KL (2005) Applications of craig interpolants in model checking. In: TACAS, Lecture Notes in Computer Science, vol 3440. Springer, Berlin, pp 1–12 Miné A (2001) The octagon abstract domain. In: Analysis, Slicing and Transformation (part of Working Conference on Reverse Engineering), IEEE. IEEE Computer Society, pp 310–319 Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: DAC Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, Berlin Prajna S, Jadbabaie A (2004) Safety verification of hybrid systems using barrier certificates. In: HSCC, Lecture Notes in Computer Science, vol 2993. Springer, Berlin Papachristodoulou A, Prajna S (2002) On the construction of lyapunov functions using the sum of squares decomposition. In: CDC Podelski A, Rybalchenko A (2004) A complete method for the synthesis of linear ranking functions. In: VMCAI, pp 239–251 Schrijver A (1986) Theory of Linear and Integer Programming. Wiley, New York Sankaranarayanan S, Sipma HB, Manna Z (2003) Petri net analysis using invariant generation. In: Verification: theory and practice, Lecture Notes in Computer Science, vol 2772. Springer, Berlin, pp 682–701 Sankaranarayanan S, Sipma HB, Manna Z (2004) Constraint-based linear relations analysis. In: 11th Static Analysis Symposium (SAS’2004), Lecture Notes in Computer Science, vol 3148. Springer, Berlin, pp 53–68 Sankaranarayanan S, Sipma HB, Manna Z (2005) Scalable analysis of linear systems using mathematical programming. In: VMCAI, Lecture Notes in Computer Science, vol 3385. Springer, Berlin Sheeran M, Singh S, Stalmarck G (2000) Checking safety properties using induction and a SAT-solver. In: FMCAD, Lecture Notes in Computer Science, vol 1954. Springer, Berlin Tarski A (1951) A decision method for elementary algebra and geometry. University of California Press, California Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5(2): 285–309 Vimjam VC, Hsiao MS (2006) Fast illegal state identification for improving SAT-based induction. In: DAC. ACM Press, New York, pp 241–246 VIS (http://visi.colorado.edu/~vis) Inc. Wolfram Research. Mathematica, Version 5.2, 2005 Wilhelm R, Sagiv S, Reps TW (2002) Parametric shape analysis via 3-valued logic. Trans Program Languages Syst 24(3): 217–298 Zeller A (1999) Yesterday, my program worked. Today, it does not. Why? In: ESEC/SIGSOFT FSE, pp 253–267