We’re excited to announce that our founders, Peter Schrammel and Daniel Kroening, alongside AWS’s Michael Tautschnig, have been awarded the Rance Cleaveland Test-of-Time Tool Award for their work on the C Bounded Model Checker (CBMC). The award was presented this week at the European Joint Conferences on Theory and Practice of Software (ETAPS) in Hamilton, Ontario.
CBMC is a leading open-source bounded model checker for C programs, designed to verify array bounds, pointer safety, exceptions, and user-specified assertions. Since its inception, CBMC has been widely adopted in both academia and industry, thanks to its precision, performance, and robust analysis capabilities. The open-source tool, which supports C and C++, with variants available for Java (JBMC) and Rust (Kani), is widely accessible via Diffblue’s GitHub repository. Diffblue’s GitHub repository.
The Rance Cleaveland Test-of-Time Tool Award recognizes software tools that have had a sustained and significant impact on the theory and practice of software. Named in memory of Rance Cleaveland, a pioneer in formal methods and model checking, the award honors tools that have stood the test of time in terms of influence, usability, and longevity.
Peter and Daniel’s work on CBMC made a profound impact on the technology that powers Diffblue today. Through the development and usage of the tool, our founders realized what a strong test generation product looked like – maintaining the highest accuracy possible with tremendous scalability. This could only be achieved through reinforcement learning.
The award was presented this week during ETAPS 2025, one of the world’s leading forums for software science research. ETAPS brings together top minds in programming languages, formal methods, and software engineering, and its awards are among the most respected in the field. More information about the award can be found here.
At Diffblue, we’re proud to see CBMC continuing to empower developers to write safer, more reliable code. It truly stood the test of time.
