TY - JOUR
T1 - Reasoning about nondeterminism in programs
AU - Cook, Byron
AU - Koskinen, Eric
PY - 2013/6
Y1 - 2013/6
N2 - Branching-time temporal logics (e.g. CTL, CTL, modal μ- calculus) allow us to ask sophisticated questions about the nondeterminism that appears in systems. Applications of this type of reasoning include planning, games, security analysis, disproving, precondition synthesis, environment synthesis, etc. Unfortunately, existing automatic branching-time verification tools have limitations that have traditionally restricted their applicability (e.g. push-down systems only, universal path quantifiers only, etc). In this paper we introduce an automation strategy that lifts many of these previous restrictions. Our method works reliably for properties with non-trivial mixtures of universal and existential modal operators. Furthermore, our approach is designed to support (possibly infinite-state) programs. The basis of our approach is the observation that existential reasoning can be reduced to universal reasoning if the system's statespace is appropriately restricted. This restriction on the state-space must meet a constraint derived from recent work on proving nontermination. The observation leads to a new route for implementation based on existing tools. To demonstrate the practical viability of our approach, we report on the results applying our preliminary implementation to a set of benchmarks drawn from the Windows operating system, the PostgreSQL database server, Soft- Updates patching system, as well as other hand-crafted examples.
AB - Branching-time temporal logics (e.g. CTL, CTL, modal μ- calculus) allow us to ask sophisticated questions about the nondeterminism that appears in systems. Applications of this type of reasoning include planning, games, security analysis, disproving, precondition synthesis, environment synthesis, etc. Unfortunately, existing automatic branching-time verification tools have limitations that have traditionally restricted their applicability (e.g. push-down systems only, universal path quantifiers only, etc). In this paper we introduce an automation strategy that lifts many of these previous restrictions. Our method works reliably for properties with non-trivial mixtures of universal and existential modal operators. Furthermore, our approach is designed to support (possibly infinite-state) programs. The basis of our approach is the observation that existential reasoning can be reduced to universal reasoning if the system's statespace is appropriately restricted. This restriction on the state-space must meet a constraint derived from recent work on proving nontermination. The observation leads to a new route for implementation based on existing tools. To demonstrate the practical viability of our approach, we report on the results applying our preliminary implementation to a set of benchmarks drawn from the Windows operating system, the PostgreSQL database server, Soft- Updates patching system, as well as other hand-crafted examples.
KW - CTL
KW - Formal verification
KW - Model checking
KW - Program analysis
KW - Temporal logic
KW - Termination
UR - http://www.scopus.com/inward/record.url?scp=84880119840&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84880119840&partnerID=8YFLogxK
U2 - 10.1145/2499370.2491969
DO - 10.1145/2499370.2491969
M3 - Article
AN - SCOPUS:84880119840
SN - 1523-2867
VL - 48
SP - 219
EP - 229
JO - ACM SIGPLAN Notices
JF - ACM SIGPLAN Notices
IS - 6
ER -