Temporal property verification as a program analysis task |
| |
Authors: | Byron Cook Eric Koskinen Moshe Vardi |
| |
Affiliation: | 1. Microsoft Research and University College London, London, UK 2. New York University, New York, NY, USA 3. Rice University, Houston, TX, USA
|
| |
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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|