TY - GEN
T1 - Making prophecies with decision predicates
AU - Cook, Byron
AU - Koskinen, Eric
PY - 2010
Y1 - 2010
N2 - We describe a new algorithm for proving temporal properties expressed in LTL of infinite-state programs. Our approach takes advantage of the fact that LTL properties can often be proved more efficiently using techniques usually associated with the branchingtime logic CTL than they can with native LTL algorithms. The caveat is that, in certain instances, nondeterminism in the system's transition relation can cause CTL methods to report counterexamples that are spurious with respect to the original LTL formula. To address this problem we describe an algorithm that, as it attempts to apply CTL proof methods, finds and then removes problematic nondeterminism via an analysis on the potentially spurious counterexamples. Problematic nondeterminism is characterized using decision predicates, and removed using a partial, symbolic determinization procedure which introduces new prophecy variables to predict the future outcome of these choices. We demonstrate-using examples taken from the PostgreSQL database server, Apache web server, and Windows OS kernel- that our method can yield enormous performance improvements in comparison to known tools, allowing us to automatically prove properties of programs where we could not prove them before.
AB - We describe a new algorithm for proving temporal properties expressed in LTL of infinite-state programs. Our approach takes advantage of the fact that LTL properties can often be proved more efficiently using techniques usually associated with the branchingtime logic CTL than they can with native LTL algorithms. The caveat is that, in certain instances, nondeterminism in the system's transition relation can cause CTL methods to report counterexamples that are spurious with respect to the original LTL formula. To address this problem we describe an algorithm that, as it attempts to apply CTL proof methods, finds and then removes problematic nondeterminism via an analysis on the potentially spurious counterexamples. Problematic nondeterminism is characterized using decision predicates, and removed using a partial, symbolic determinization procedure which introduces new prophecy variables to predict the future outcome of these choices. We demonstrate-using examples taken from the PostgreSQL database server, Apache web server, and Windows OS kernel- that our method can yield enormous performance improvements in comparison to known tools, allowing us to automatically prove properties of programs where we could not prove them before.
KW - Formal verification
KW - Linear temporal logic
KW - Model checking
KW - Program analysis
KW - Termination
UR - http://www.scopus.com/inward/record.url?scp=79952033879&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=79952033879&partnerID=8YFLogxK
U2 - 10.1145/1926385.1926431
DO - 10.1145/1926385.1926431
M3 - Conference contribution
AN - SCOPUS:79952033879
SN - 9781450304900
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 399
EP - 410
BT - POPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
T2 - 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11
Y2 - 26 January 2011 through 28 January 2011
ER -