×

zbMATH — the first resource for mathematics

Temporal property verification as a program analysis task. (English) Zbl 1284.68171
Summary: We describe a reduction from temporal property verification to a program analysis problem. First we present a proof system that, unlike the standard formulation, is more amenable to reasoning about infinite-state systems: disjunction is treated by partitioning, rather than enumerating, the state space and temporal operators are characterized with special sets of states called frontiers. We then describe a transformation that, with the use of procedures and nondeterminism, enables off-the-shelf program analysis tools to naturally perform the reasoning necessary for proving temporal properties (e.g. backtracking, eventuality checking, tree counterexamples for branching-time properties, abstraction refinement, etc.). Using examples drawn from the PostgreSQL database server, Apache web server, and Windows OS kernel, we demonstrate the practical viability of our work.

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Cadence SMV, http://www.kenmcmil.com/smv.html · Zbl 1119.68033
[2] Ball T, Bounimova E, Cook B, Levin V, Lichtenberg J, McGarvey C, Ondrusek B, Rajamani SK, Ustuner A (2006) Thorough static analysis of device drivers. SIGOPS Oper Syst Rev 40:73–85 · doi:10.1145/1218063.1217943
[3] Berdine J, Chawdhary A, Cook B, Distefano D, O’Hearn PW (2007) Variance analyses from invariance analyses. In: Hofmann M, Felleisen M (eds) Proceedings of the 34th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL 2007). ACM, New York, pp 211–224 · Zbl 1295.68076
[4] Bernholtz O, Vardi MY, Wolper P (1994) An automata-theoretic approach to branching-time model checking (extended abstract). In: Dill DL (ed) Proceedings of the 6th international conference on computer aided verification (CAV ’94). Lecture notes in computer science, vol 818. Springer, Berlin, pp 142–155
[5] Beyer D, Henzinger TA, Jhala R, Majumdar R (2007) The software model checker blast. Int J Softw Tools Technol Transf 9(5–6):505–525 · Zbl 05536156 · doi:10.1007/s10009-007-0044-z
[6] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2003) A static analyzer for large safety-critical software. In: Proceedings of the ACM SIGPLAN 2003 conference on programming language design and implementation (PLDI’03). ACM, New York, pp 196–207 · Zbl 1026.68514
[7] Bradley A, Manna Z, Sipma H (2005) The polyranking principle. Autom Lang Program, 1349–1361 · Zbl 1081.68568
[8] Burch J Clarke E et al. (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142–170 · Zbl 0753.68066 · doi:10.1016/0890-5401(92)90017-A
[9] Calcagno C, Distefano D, O’Hearn PW, Yang H (2009) Compositional shape analysis by means of bi-abduction. In: Shao Z, Pierce BC (eds) Proceedings of the 36th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL 2009). ACM, New York, pp 289–300 · Zbl 1315.68085
[10] Chaki S, Clarke EM, Grumberg O, Ouaknine J, Sharygina N, Touili T, Veith H (2005) State/event software verification for branching-time specifications. In: Romijn J, Smith G, van de Pol J (eds) Proceedings of the 5th international conference on integrated formal methods (IFM 2005), vol 3771, pp 53–69 · Zbl 1137.68432
[11] Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) Nusmv 2: an opensource tool for symbolic model checking. In: Brinksma E, Larsen KG (eds) Proceedings of the 14th international conference on computer aided verification (CAV’02), vol 2404. Springer, Berlin, pp 359–364 · Zbl 1010.68766
[12] Clarke E, Grumberg O, Peled D (1999) Model checking
[13] Clarke E, Jha S, Lu Y, Veith H (2002) Tree-like counterexamples in model checking. In: Proceedings of the symposium on logic in computer science (LICS’02), pp 19–29
[14] Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8:244–263 · Zbl 0591.68027 · doi:10.1145/5397.5399
[15] Cook B, Gotsman A, Podelski A, Rybalchenko A, Vardi MY (2007) Proving that programs eventually do something good. In: Proceedings of the 34th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL 2007), pp 265–276 · Zbl 1295.68083
[16] Cook B, Koskinen E (2011) Making prophecies with decision predicates. In: Ball T, Sagiv M (eds) Proceedings of the 38th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL’11). ACM, New York, pp 399–410 · Zbl 1284.68389
[17] Cook B, Koskinen E, Vardi MY (2011) Temporal property verification as a program analysis task. In: Gopalakrishnan G, Qadeer S (eds) Proceedings of the 23rd international conference on computer aided verification (CAV’11), vol 6806. Springer, Berlin, pp 333–348
[18] Cook B, Podelski A, Rybalchenko A (2006) Termination proofs for systems code. In: Schwartzbach MI, Ball T (eds) Proceedings of the ACM SIGPLAN 2006 conference on programming language design and implementation, Ottawa, Ontario, Canada, June 11–14, 2006 ACM, New York, pp 415–426
[19] Delzanno G, Podelski A (1999) Model checking in CLP. In: Cleaveland R (ed) Proceedings of the 5th international conference on tools and algorithms for construction and analysis of systems (TACAS ’99). Lecture notes in computer science, vol 1579. Springer, Berlin, pp 223–239 · Zbl 0947.68028
[20] Emerson EA, Namjoshi KS (1996) Automatic verification of parameterized synchronous systems (extended abstract). In: Alur R, Henzinger TA (eds) Proceedings of the 8th international conference on computer aided verification (CAV ’96), vol 1102. Springer, Berlin, pp 87–98
[21] Fioravanti F, Pettorossi A, Proietti M, Senni V (2010) Program specialization for verifying infinite state systems: an experimental evaluation. In: Alpuente M (ed) Proceedings of the 20th international symposium on logic-based program synthesis and transformation (LOPSTR’10), vol 6564. Springer, Berlin, pp 164–183 · Zbl 1326.68184
[22] Gastin P, Oddoux D (2001) Fast ltl to büchi automata translation. In: Berry G, Comon H, Finkel A (eds) Proceedings of the 13th international conference on computer aided verification (CAV 2001), vol 2102. Springer Berlin, pp 53–65 · Zbl 0991.68044
[23] Gurfinkel A (2010) Personal communication
[24] Gurfinkel A, Wei O, Chechik, M (2006) Yasm: a software model-checker for verification and refutation. In: Ball T, Jones RB (eds) Proceedings of the 18th international conference on computer aided verification (CAV’06), vol 4144, pp 170–174
[25] Koskinen E (2012) Temporal verification of programs. PhD thesis, University of Cambridge. To appear · Zbl 1284.68171
[26] Kupferman O, Vardi M, Wolper P (2000) An automata-theoretic approach to branching-time model checking. J ACM 47(2):312–360 · Zbl 1133.68376 · doi:10.1145/333979.333987
[27] Magill S, Berdine J, Clarke EM, Cook B (2007) Arithmetic strengthening for shape analysis. In: Nielson HR, Filé G (eds) Proceedings of the 14th international static analysis symposium (SAS 2007), vol 4634. Springer, Berlin, pp 419–436 · Zbl 1211.68094
[28] O’Hearn P, Reynolds J, Yang H (2001) Local reasoning about programs that alter data structures. In: Computer science logic, pp 1–19 · Zbl 0999.68045
[29] Podelski A, Rybalchenko A (2004) A complete method for the synthesis of linear ranking functions. In: Steffen B, Levi G (eds) Proceedings of the 5th international conference on verification, model checking, and abstract interpretation (VMCAI’04), vol 2937. Springer, Berlin, pp 239–251 · Zbl 1202.68109
[30] Podelski A, Rybalchenko A (2004) Transition invariants. In: Proceedings of the 19th IEEE symposium on logic in computer science (LICS 2004). IEEE Computer Society, New York, pp 32–41 · Zbl 1315.68104
[31] Podelski A, Rybalchenko A (2005) Transition predicate abstraction and fair termination. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL 2005) · Zbl 1315.68104
[32] Reps T, Horwitz S, Sagiv M (1995) Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL’95), pp 49–61
[33] Schmidt DA, Steffen B (1998) Program analysis as model checking of abstract interpretations. In: Levi G (ed) Proceedings of the 5th international static analysis symposium (SAS ’98), vol 1503. Springer, Berlin, pp 351–380
[34] Stirling C (1996) Games and modal mu-calculus. In: Margaria T, Steffen B (eds) Proceedings of the second international workshop on tools and algorithms for construction and analysis of systems (TACAS ’96), vol 1055, pp 298–312
[35] Vardi MY (1995) An automata-theoretic approach to linear temporal logic. In: Banff Higher order workshop, pp 238–266
[36] Walukiewicz I (1996) Pushdown processes: games and model checking. In: Alur R, Henzinger TA (eds) Proceedings of the 8th international conference on computer aided verification. Lecture notes in computer science, vol 1102. Springer, Berlin, pp 62–74
[37] Walukiewicz I (2000) Model checking CTL properties of pushdown systems. In: Kapoor S, Prasad S (eds) Proceedings of the 20th conference on foundations of software technology and theoretical computer science (FST TCS 2000). Springer, Berlin, pp 127–138. 1974 · Zbl 1044.68111
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.