HVC Award
Granted since 2007, the HVC award recognizes the most promising academic and industrial contribution to the fields of testing and software and hardware verification from the last five years.
The HVC'14 award committee has decided to give this year's award to Andrey Rybalchenko, Corneliu Popeea, Nuno Lopes, and Sergey Grebenshchiko for their PLDI'12 paper called "Synthesizing Software Verifiers from Proof Rules". The key idea underlying this work is to reduce program verification to solving Horn-like clauses involving unknown predicates, where the unknown predicates may correspond to loop invariants or method pre- and post-conditions. Given such a general engine for solving these Horn-like clauses, the arduous task of engineering a program verification tool reduces to coming up with appropriate proof rules. The proposed approach has been used for verifying both safety and liveness properties of sequential as well as multi-threaded programs and has also been successfully applied to program synthesis. In a series of follow-up papers, the authors have explored algorithms for solving quantified recursive Horn clauses and applied these algorithms to a variety of challenging problems in verification and synthesis.
HVC award committee
- Isil Dillig, chair (UT Austin)
- Patrice Godefroid (MSR)
- Mayur Naik (Georgia Tech)
- Darko Marinov (UIUC)
- Corina Pasareanu (CMU and NASA)
- Avi Ziv (IBM)
Keynote Speakers
- Prof. Moshe Vardi, Rice University
- Wolfgang Roesner, Fellow, IBM
- Prof. Martin Vechev, ETH Zürich
- Harry Foster, Chief Verification Scientist, Mentor Graphics
- Ziv Binyamini, Corporate VP & CTO, System and Software Solutions, Cadence
