The Verifying Compiler checks the correctness of the program it compiles. The workhorse of such a tool is the reasoning engine, which decides validity of formulae in a suitably chosen logic. This paper discusses possible choices for this logic, and how to solve the resulting decision problems. A framework for reducing decision problems to propositional logic is described, which allows the surprising improvements in the performance of propositional SAT solvers to be exploited. The only assumption the framework makes is that an axiomatization of the desired logic is given. © IFIP International Federation for Information Processing 2008.
CITATION STYLE
Kroening, D. (2008). Decision procedures for the grand challenge. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4171 LNCS, pp. 428–437). https://doi.org/10.1007/978-3-540-69149-5_46
Mendeley helps you to discover research relevant for your work.