Generating and Exploiting Automated Reasoning Proof Certificates

Automated reasoning refers to a set of tools and techniques for automatically proving or disproving formulas in mathematical logic.35 It has many applications in computer science--for example, questions about the existence of bugs or security vulnerabilities in hardware or software systems can often be phrased as logical formulas, or verification conditions, whose validity can then be proved or disproved using automated reasoning techniques, a process known as formal verification.15,26 When successful, formal verification can guarantee freedom from certain kinds of design errors, an outcome that is otherwise extremely difficult to achieve. Driven by such potential benefits, the past couple of decades have seen a dramatic improvement in the performance and capabilities of automated reasoning tools, with a corresponding explosion of use cases, including formal verification, automated test-case generation, program analysis, program synthesis, and many more.5,37,38 These applications rely crucially on automated reasoning tools producing correct results.