acm-header
Sign In

Communications of the ACM

Research

Generating and Exploiting Automated Reasoning Proof Certificates


checkmark-labeled token amid pieces of metal, illustration

Credit: Tanzim Graphics

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

Back to Top

Key Insights

ins01.gif

These applications rely crucially on automated reasoning tools producing correct results. However, ensuring correctness is a significant challenge. To meet the perpetual demand for better performance, automated reasoning tools have large and complex code bases, are highly optimized, and evolve rapidly, all of which puts their reliability at risk. While conventional software-engineering best practices can help, they are insufficient, especially when the goal is to provide incontrovertible mathematical guarantees. Formal verification of automated reasoning tools themselves requires an enormous effort and would have to be revisited every time the tools change. Fortunately, it is possible to provide strong correctness guarantees for an automated reasoner without having to trust the tool at all. The idea is to separate proof finding from proof checking. In contrast to the complex tools for finding proofs, automated proof checkers can be relatively simple (that is, a few thousand lines of code as opposed to a few hundred-thousand lines of code) and need only be revisited when the proof format changes, a relatively rare event. Because of their relative simplicity, proof checkers can also be vetted by the community when made open source. Even formal verification of simple proof checkers is not out of the question. It is also worth noting that proof checking can often be done offline, reducing the impact on performance.


 

No entries found

Log in to Read the Full Article

Sign In

Sign in using your ACM Web Account username and password to access premium content if you are an ACM member, Communications subscriber or Digital Library subscriber.

Need Access?

Please select one of the options below for access to premium content and features.

Create a Web Account

If you are already an ACM member, Communications subscriber, or Digital Library subscriber, please set up a web account to access premium content on this site.

Join the ACM

Become a member to take full advantage of ACM's outstanding computing information resources, networking opportunities, and other benefits.
  

Subscribe to Communications of the ACM Magazine

Get full access to 50+ years of CACM content and receive the print version of the magazine monthly.

Purchase the Article

Non-members can purchase this article or a copy of the magazine in which it appears.