CAV 2018 Award for BMC and CBMC

Here is a local copy of the official nomination text. See also out BMC page for more information.

CAV Award

The recipients of the 2018 CAV Award are:

• Armin Biere
• Alessandro Cimatti
• Edmund M. Clarke
• Daniel Kroening
• Flavio Lerda
• Yunshan Zhu

Bounded Model Checking has revolutionized the way model checking is used and perceived. It has increased the capabilities of model checkers by orders of magnitude, turning them into a standard tool for hardware verification and a very important component of the toolkit available for software verification.

BMC changed the focus of model checking from full verification to bug-finding. The BMC problem is defined as follows: Given a bound k, is there an erroneous computation of the system of length k? This problem is transformed to a Boolean formula that is satisfiable if and only if the system includes a computation of length k, which violates the specification.

Focusing on the bounded problem enabled the authors to exploit the progress that was made in SAT solving around the same time, and simultaneously to bootstrap the tremendous progress in satisfiability solving that we have seen since.

While early implementation of BMC focused on hardware, CBMC has demonstrated how it can be applied to realistic programs written in C. The ability to apply verification directly to C programs gave an enormous boost to a very large spectrum of applications in hardware and software industry and in academic research. The application areas include error explanation and localization, concurrent programs, equivalence checking, cyber-physical systems and control systems, test vector generation, worst-case execution time, security, and many other practical applications.

For previous winners of the award, please see the main CAV award page.

2018 Award Committee

• Kim G. Larsen (Chair), Aalborg University
• Natarajan Shankar, SRI International
• Pierre Wolper, Liege University
• Somesh Jha, University of Wisconsin