A bug hunting tool co-developed by an EECS researcher, Dr Michael Tautschnig, has won a prestigious award.
The C Bounded Model Checker (CBMC), which helps to detect bugs in software, won the ‘Falsifcation’ category in the TACAS 2017 6th International Competition on Software Verification (SV-COMP’17).
The results of the competition were announced at the European Joint Conferences on Theory and Practice of software (ETAPS) in Uppsala, Sweden on 27 April.
The focus of SV COMP’17 was precision and during the competition, CBMC did not give a single wrong answer in its category.
Dr Michael Tautschnig, from the School of Electronic Engineering and Computer Science (EECS) and the project’s principal researcher on Software Analysis and Verification, said: “The success in SV-COMP’17 shows that CBMC is both the most efficient tool in this space, and also is the most precise tool across a range of several thousand benchmarks.”
He added: “In order to tune CBMC to become as efficient as it is today, a large number of experiments had to be conducted. This has been enabled by infrastructure set up in EECS, funded by a joint research project with QMUL’s Pasquale Malacaria.”
Dr Tautschnig co-developed CBMC with Professor Daniel Kroening from Oxford University and Peter Schrammel from Sussex University.
It is available as open source from GitHub and, notably, several further contestants in SV-COMP’17 used CBMC as part of their submission.
The competition is aimed at providing a snapshot of the state-of-the-art in software verification as a means to compare, independently from particular paper projects and specific techniques, different verification tools in terms of precision and performance.
TACAS also helps increase the visibility and credits that tool developers receive. It assists to provide a forum for presentation of tools and discussion of the latest technologies and to give students the opportunity to publish about the development work that they have done.