nach oben

Formal Methods in System Design

Erschienen in:

01.08.2012

Temporal property verification as a program analysis task

Extended Version

verfasst von: Byron Cook, Eric Koskinen, Moshe Vardi

Erschienen in: Formal Methods in System Design | Ausgabe 1/2012

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

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.

Vorheriger Artikel Unified QBF certification and its applications

Nächster Artikel Forest automata for verification of heap manipulation

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

This is an adaptation of a known technique [18]. However, rather than using assert to check that one of the ranking functions in \(\mathcal {M}\) holds, our encoding instead returns false, allowing other possibilities to be considered (if any exist) in outer disjunctive or AF formulae.

Cadence SMV, http://www.kenmcmil.com/smv.html

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 CrossRef

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 CrossRef

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 CrossRef

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 CrossRef

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 CrossRef

Bradley A, Manna Z, Sipma H (2005) The polyranking principle. Autom Lang Program, 1349–1361

Burch J Clarke E et al. (1992) Symbolic model checking: 10²⁰ states and beyond. Inf Comput 98(2):142–170 MathSciNetMATHCrossRef

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

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

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 CrossRef

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 CrossRef

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 MATHCrossRef

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 CrossRef

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

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 CrossRef

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 CrossRef

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 CrossRef

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 CrossRef

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

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 CrossRef

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 CrossRef

25.

Koskinen E (2012) Temporal verification of programs. PhD thesis, University of Cambridge. To appear

26.

Kupferman O, Vardi M, Wolper P (2000) An automata-theoretic approach to branching-time model checking. J ACM 47(2):312–360 MathSciNetMATHCrossRef

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

28.

O’Hearn P, Reynolds J, Yang H (2001) Local reasoning about programs that alter data structures. In: Computer science logic, pp 1–19 CrossRef

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 CrossRef

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 CrossRef

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)

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 CrossRef

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 CrossRef

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 CrossRef

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 CrossRef

Titel: Temporal property verification as a program analysis task
Extended Version
verfasst von: Byron Cook
Eric Koskinen
Moshe Vardi
Publikationsdatum: 01.08.2012
Verlag: Springer US
Erschienen in: Formal Methods in System Design / Ausgabe 1/2012
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI: https://doi.org/10.1007/s10703-012-0153-5

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 1/2012

Forest automata for verification of heap manipulation

2011 CAV award announcement

Recognizing malicious software behaviors with tree automata inference

Counterexample-guided abstraction refinement for symmetric concurrent programs

Unified QBF certification and its applications

Preface

Premium Partner