TY - GEN
T1 - Temporal property verification as a program analysis task
AU - Cook, Byron
AU - Koskinen, Eric
AU - Vardi, Moshe
PY - 2011
Y1 - 2011
N2 - We describe a reduction from temporal property verification to a program analysis problem. We produce an encoding which, with the use of recursion 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. We produce an encoding which, with the use of recursion 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.
UR - https://www.scopus.com/pages/publications/79960341516
UR - https://www.scopus.com/pages/publications/79960341516#tab=citedBy
U2 - 10.1007/978-3-642-22110-1_26
DO - 10.1007/978-3-642-22110-1_26
M3 - Conference contribution
AN - SCOPUS:79960341516
SN - 9783642221095
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 333
EP - 348
BT - Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings
ER -