TY - GEN
T1 - Reasoning about nondeterminism in programs
AU - Cook, Byron
AU - Koskinen, Eric
PY - 2013
Y1 - 2013
N2 - Branching-time temporal logics (e.g. CTL, CTL*, modal μ-calculus) allow us to ask sophisticated questions about the nonde-terminism 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 non-termination. 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 nonde-terminism 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 non-termination. 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=84883091588&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84883091588&partnerID=8YFLogxK
U2 - 10.1145/2491956.2491969
DO - 10.1145/2491956.2491969
M3 - Conference contribution
AN - SCOPUS:84883091588
SN - 9781450320146
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 219
EP - 229
BT - PLDI 2013 - Proceedings of the 2013 ACM SIGPLAN Conference on Programming Language Design and Implementation
T2 - 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013
Y2 - 16 June 2013 through 19 June 2013
ER -