TY - JOUR
T1 - Temporal property verification as a program analysis task
T2 - Extended Version
AU - Cook, Byron
AU - Koskinen, Eric
AU - Vardi, Moshe
PY - 2012/8
Y1 - 2012/8
N2 - 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.
AB - 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.
KW - Automatic software verification
KW - Formal verification
KW - Model checking
KW - Program analysis
KW - Temporal logic
KW - Termination
UR - http://www.scopus.com/inward/record.url?scp=84863186946&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84863186946&partnerID=8YFLogxK
U2 - 10.1007/s10703-012-0153-5
DO - 10.1007/s10703-012-0153-5
M3 - Article
AN - SCOPUS:84863186946
SN - 0925-9856
VL - 41
SP - 66
EP - 82
JO - Formal Methods in System Design
JF - Formal Methods in System Design
IS - 1
ER -