At the 11th Haifa Verification Conference 2015 (HVC'15) taking place from November 17 - 19, 2015, at the IBM research labs in Haifa, Israel, the HVC'15 award was given to Armin Biere. The award certificate was handed over before the award talk on November 19. The following award text was announced at the HVC'15 award page.
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.
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