Output details

Making prophecies with decision predicates.

<9>This paper provides a vastly faster alternative to the traditional automata-theoretic construction (due to Vardi/Wolper) that underlies all previously known model checkers for linear temporal logics. Our paper instead shows how one can automatically infer prophecy variables, which then facilitate the use of much higher-performance proof methods that would otherwise not be applicable to linear-time properties. This approach provides many orders of magnitude of speedup over known techniques when applied to the PostgreSQL database server, Apache web server, and Windows OS kernel. This work is a key component of a new extension to the Microsoft Windows Static Driver Verifier product.