Temporal property verification as a program analysis task: Extended Version

Byron Cook, Eric Koskinen, Moshe Vardi

Research output: Contribution to journalArticlepeer-review

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.

Original languageEnglish
Pages (from-to)66-82
Number of pages17
JournalFormal Methods in System Design
Volume41
Issue number1
DOIs
StatePublished - Aug 2012

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture

Keywords

  • Automatic software verification
  • Formal verification
  • Model checking
  • Program analysis
  • Temporal logic
  • Termination

Cite this