The International Competition on Software Verification (SV-COMP) is a driving force for the invention of new methods, technologies, and tools for the automated verification of computer software. Software verification is an unarguably-important research area as society becomes more and more dependent on its correct functionality: software bugs can cost lives and great monetary loss. Though the goal of verified software has existed since the dawn of computer science, the technology enabling widespread use of software verifiers has been extremely challenging to develop, due to fundamental philosophical limitations, practical engineering obstacles, and the challenge in surmounting both simultaneously. SV-COMP aims to advance software verification technology by bringing together the top international minds.
This year marks the 4th annual installment of an increasingly-competitive event, in which 22 entries from top research institutions including New York University, Ecole Normale Supérieure (ENS) of Paris, University of Freiburg, Tsinghua University, Microsoft Research, and IMDEA Software Institute compete across 13 categories of software verification problems.
Each competition entry is a computer program called a “verifier”, and each “problem” is a computer program whose correctness must be verified by the verifier. The verifiers are submitted as executable code, and the problems are provided as source code written in the C programming language. The verifiers classify problems either as “correct”, “incorrect”, or “unknown”, within a time limit of 900 seconds per problem. Points are awarded according to the accuracy of classification. In each problem category, the three highest-scoring verifiers are awarded medals: gold, silver, and bronze.
In collaboration with the University of Utah and Microsoft Research, the IMDEA Software Institute’s competition entry, named SMACK+Corral, was awarded medals in four categories — two gold, one silver, and one bronze — placing it among the top-performing verifiers. Only one entry earned more gold medals, and only three entries earned more medals total.
Technically, SMACK+Corral is the fusion of two programs. SMACK is an open-source project led by Zvonimir Rakamaric of the University of Utah, and Michael Emmi of the IMDEA Software Institute. The role of SMACK is to translate the C-language verification problems into mathematical representations which can be more-easily processed by automated logical-reasoning engines known as “theorem provers”. Corral, developed by Microsoft Research, applies novel reasoning algorithms to decide whether the given mathematical representation should be classified as “correct”. Combined, the two function as a powerful verifier of C-language programs.
The SV-COMP 2015 post-competition event is being held on the week of April 13th, 2015, as part of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), in London, UK. The event includes a short presentation by the authors of each entry, and an official announcement of the competition results.
More information at SV-COMP 2015.
