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 Springer-Verlag.
CITATION STYLE
Cook, B., Koskinen, E., & Vardi, M. (2011). Temporal property verification as a program analysis task. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6806 LNCS, pp. 333–348). https://doi.org/10.1007/978-3-642-22110-1_26
Mendeley helps you to discover research relevant for your work.