Decision Procedures for the Grand Challenge

Abstract. 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 problems.

• Type: Conference
• Year: 2005
• Where: VSTTE
• Authors: Daniel Kroening
• Keywords: Correctness, Possible Choices, Reasoning Engine, Software Engineering, VSTTE 2005