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. Armin Biere from Johannes Kepler University in Austria.

Since Biere's PhD graduation in 1997, he made pivotal contributions in formal verification, one of which --- bounded model checking --- was recently selected as the most influential article in the 20 years of TACAS. This technique is still being used in numerous EDA companies, and also led to similar ideas in verification of software. In addition, he is the developer of numerous award-winning SAT, bitvector, arrays and QBF solvers. Such solvers developed by him or under his guidance rank at the top of many international competitions and were awarded 42 medals including 24 gold medals.

Biere is one of the editors of the 980-pages "Handbook of Satisfiability", the chair of the SAT association, the founder and organizer of the Hardware Model Checking Competition (HWMCC), the inventor of the now ubiquitous AIG format for model-checking, and also has served in the last two years as an informal advisor of D. Knuth for SAT-related issues.

By awarding Prof. Biere, the committee recognizes his major contributions to the formal verification and computational logic communities.

HVC award committee

• Hana Chockler (King's College London) - chair
• Kerstin Eder (University of Bristol)
• Leonardo Mariani (University of Milano-Bicocca)
• Andrey Rybalchenko (Microsoft Research UK)
• Shaz Qadeer (Microsoft Research US)
• Ofer Strichman (Technion)