Temporal property verification as a program analysis task
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.
2011-cav-Temporal property verification as a program analysis task.pdf
—
PDF document,
227 kB (232628 bytes)