×

Property-directed incremental invariant generation. (English) Zbl 1149.68402


MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

Chaff; Mathematica
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Armoni R, Fix L, Fraer R, Huddleston S, Piterman N, Vardi M (2004) SAT-based induction for temporal safety properties. In: BMC · Zbl 1272.68219
[2] Aiken A (1999) Introduction to set constraint-based program analysis. Sci Comput Program 35: 79–111 · Zbl 0940.68031 · doi:10.1016/S0167-6423(99)00007-6
[3] Awedh M, Somenzi F (2006) Automatic invariant strengthening to prove properties in bounded model checking. In: DAC. ACM Press, New York, pp 1073–1076 · Zbl 1272.68221
[4] Avis D (1998) LRS: a revised implementation of the reverse search vertex enumeration algorithm. Technical Report, McGill · Zbl 0947.90077
[5] Aiken A, Wimmers E (1992) Solving systems of set constraints. In: LICS, pp 329–340
[6] Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without bdds. In: TACAS, London, UK. Springer, Berlin, pp 193–207
[7] Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inform Comput 98(2): 142–170 · Zbl 0753.68066 · doi:10.1016/0890-5401(92)90017-A
[8] Bradley AR, Manna Z (2006) Verification constraint problems with strengthening In: ICTAC, Lecture Notes in Computer Science, vol 3722. Springer, Berlin · Zbl 1168.68421
[9] Bradley AR, Manna Z (2007) The calculus of computation: decision procedures with applications to verification. Springer, Berlin · Zbl 1126.03001
[10] Bradley AR, Manna Z (2007) Checking safety by inductive generalization of counterexamples to induction. In: FMCAD
[11] 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 · Zbl 1081.68611
[12] Boyd S, Yang Q (1989) Structured and simultaneous Lyapunov functions for system stability problems. Int J Control 49(6): 2215–2240 · Zbl 0683.93057
[13] 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
[14] 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
[15] 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 · Zbl 0974.68517
[16] 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 · Zbl 0974.68517 · doi:10.1145/876638.876643
[17] 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
[18] 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
[19] Cousot P (2005) Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: VMCAI, pp 1–24 · Zbl 1111.68503
[20] 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 · Zbl 0978.68095
[21] 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 · Zbl 1010.68774
[22] 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 · Zbl 1278.68164
[23] 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 · Zbl 1278.68199
[24] Floyd RW (1967) Assigning meanings to programs. In: Symposia in applied mathematics, vol 19. American Mathematical Society, pp 19–32 · Zbl 0189.50204
[25] 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
[26] Hardware model checking competition 2007 (HWMCC’07)
[27] Jain H, Kroening D, Sharygina N, Clarke EM (2005) Word level predicate abstraction and refinement for verifying RTL verilog. In: DAC
[28] 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
[29] Conflict detection for arbitrary constraint propagation algorithms. In: IJCAI Workshop on Modelling and Solving Problems with Constraints
[30] Karr M (1976) Affine relationships among variables of a program. Acta Inform 6: 133–151 · Zbl 0358.68025 · doi:10.1007/BF00268497
[31] Katz SM, Manna Z (1975) A closer look at termination. Acta Inform 5(4): 333–352 · Zbl 0312.68018 · doi:10.1007/BF00264565
[32] Knaster B (1928) Un theoreme sur les fonctions d’ensembles. Ann Soc Polon Math 6: 133–134 · JFM 54.0091.04
[33] McMillan KL, Amla N (2003) Automatic abstraction without counterexamples. In: TACAS, pp 2–17 · Zbl 1031.68520
[34] 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 · Zbl 1010.68509
[35] McMillan KL (2003) Interpolation and SAT-based model checking. In: CAV, Lecture Notes in Computer Science, vol 2725. Springer, Berlin, pp 1–13 · Zbl 1278.68184
[36] McMillan KL (2005) Applications of craig interpolants in model checking. In: TACAS, Lecture Notes in Computer Science, vol 3440. Springer, Berlin, pp 1–12 · Zbl 1087.68597
[37] 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
[38] Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: DAC
[39] Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, Berlin · Zbl 0844.68079
[40] Prajna S, Jadbabaie A (2004) Safety verification of hybrid systems using barrier certificates. In: HSCC, Lecture Notes in Computer Science, vol 2993. Springer, Berlin · Zbl 1135.93317
[41] Papachristodoulou A, Prajna S (2002) On the construction of lyapunov functions using the sum of squares decomposition. In: CDC · Zbl 1138.93391
[42] Podelski A, Rybalchenko A (2004) A complete method for the synthesis of linear ranking functions. In: VMCAI, pp 239–251 · Zbl 1202.68109
[43] Schrijver A (1986) Theory of Linear and Integer Programming. Wiley, New York · Zbl 0665.90063
[44] 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 · Zbl 1274.68253
[45] Sankaranarayanan S, Sipma HB, Manna Z (2004) Constraint-based linear relations analysis. In: 11 th Static Analysis Symposium (SAS’2004), Lecture Notes in Computer Science, vol 3148. Springer, Berlin, pp 53–68 · Zbl 1104.68023
[46] 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 · Zbl 1111.68514
[47] 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
[48] Tarski A (1951) A decision method for elementary algebra and geometry. University of California Press, California · Zbl 0044.25102
[49] Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5(2): 285–309 · Zbl 0064.26004
[50] Vimjam VC, Hsiao MS (2006) Fast illegal state identification for improving SAT-based induction. In: DAC. ACM Press, New York, pp 241–246
[51] VIS ( http://visi.colorado.edu/\(\sim\)vis ) · Zbl 1174.54017
[52] Inc. Wolfram Research. Mathematica, Version 5.2, 2005
[53] Wilhelm R, Sagiv S, Reps TW (2002) Parametric shape analysis via 3-valued logic. Trans Program Languages Syst 24(3): 217–298 · Zbl 05459332 · doi:10.1145/514188.514190
[54] Zeller A (1999) Yesterday, my program worked. Today, it does not. Why? In: ESEC/SIGSOFT FSE, pp 253–267
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.