Matt Kaufmann

The Boyer Moore Theorem Prover is a highly engineered and effective formal methods tool that pioneered the automation of proofs by induction, and now provides fully automatic or human-guided verification of critical computing systems. The latest version of the system, ACL2, is the only simulation/verification system that provides a standard modelling language and industrial strength model simulation in a unified framework. This technology is truly remarkable in that simulation is comparable to C in performance, but runs inside a theorem prover that verifies properties by mathematical proof. ACL2 is used in industry by AMD, IBM and Rockwell-Collins, among others.

Formal verification is of tremendous interest today in safety-critical applications such as embedded medical devices, spacecraft and aircraft control, and autonomous vehicles such as self-driving cars. Because of the Boyer-Moore Theorem Prover, an enormous range of software programs and hardware designs are now amenable to formal verification, leading to safer and more secure software for all.

For use in the prover, Boyer, Moore, and Kaufmann pioneered and engineered many core verification technologies such as the integration of decision procedures, the use of meta-functions (reflection), and the tight integration of logic and programming. The Boyer-Moore specification logic caters for essentially arbitrary correctness properties, including partial and total correctness, safety, liveness, and security properties. Since the 1970s, Boyer, Moore and Kaufmann and the users of the Boyer-Moore theorem prover have continually re-defined the state-of-the-art by verifying actual running code, and demonstrating that theorem proving technology has reached the stage where commercial-scale applications are feasible.