Open AccessTemporal property verification as a program analysis task
Author(s) -
Byron Cook,
Eric Koskinen,
Moshe Y. Vardi
Publication year - 2012
Publication title -
formal methods in system design
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.334
H-Index - 54
eISSN - 1572-8102
pISSN - 0925-9856
DOI - 10.1007/s10703-012-0153-5
Subject(s) - computer science , backtracking , model checking , theoretical computer science , programming language , property (philosophy) , soundness , temporal logic , abstraction , kernel (algebra) , mathematics , discrete mathematics , philosophy , epistemology
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.
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom