HVC Award

The HVC award is given to the most influential work in the last five years in formal verification, simulation, and testing. The award is not limited to influential articles; it can also be a system or a collection of activities that promote the area.

The HVC award committee has decided to give the award this year to Prof. Cristian Cadar (Imperial College London) for his contributions to dynamic symbolic execution and the KLEE symbolic execution infrastructure.

Dynamic symbolic execution is a technique for automatically exploring feasible paths through a program by using a constraint solver. It involves generating a concrete input triggering each path and checking if there are any values that can cause an error on the path. KLEE consists of a compiler frontend, mixed symbolic/explicit interpreter, search engine for path exploration, constraint solving optimizer, and constraint solving backend. KLEE is an extensible platform that is used and extended by many groups in academia and industry, in the areas such as bug finding, test generation, exploit generation, automated debugging.

By awarding Prof. Cristian Cadar, the committee recognizes his outstanding contributions to program verification, bug finding, test generation and, more generally, to software reliability.

HVC Award Committee

• Andrey Rybalchenko, Chair (Microsoft Research)
• Hana Chockler (King's College London)
• Kerstin Eder (University of Bristol)
• Marta Kwiatkowska (University of Oxford)
• Leonardo Mariani (University of Milano Bicocca)