The Haifa Verification Conference (HVC) 2010, slated for October 5-7, is the sixth in the series of annual conferences dedicated to advancing the verification and testing of both hardware and software. The conference, organized by IBM R&D Labs in Israel, provides a forum for academia, industry, and the research and development community to share their work, exchange ideas, and discuss the challenges and future directions of verification for hardware, software, and hybrid systems.

The HVC award is given to the most influential work in the last five years in the scope of HVC itself, namely formal and nonformal verification. The award is not limited to influential articles; it can also be a system or a collection of activities that promote the area, and it recognizes the most promising contribution to fields of software and hardware verification and test in the last five years.

The HVC 2010 award went to key players in promoting Satisfiability Modulo Theories (SMT). The winners are (alphabetically):

• Clark Barrett, New York University
• Leonardo De-Moura, Microsoft Research
• Silvio Ranise, FBK Trento
• Aaron Stump, University of Iowa
• Cesare Tinelli, University of Iowa

The HVC award committee has decided to give the award this year to those who played a pivotal and continuous role in building and promoting the Satisfiability Modulo Theories (SMT) community. The term "Satisfiability modulo theories," was coined less than 10 years ago, but the impact of this field on the industry can be measured by the current use of SMT solvers: Microsoft uses Z3, an SMT solver developed by De-Moura and Bjorner, in at least 10 different program analysis tools; Intel is using SMT solvers such as MathSat and Boolector for processor verification and hardware equivalence checking; other companies that are known to use SMT solvers include Galois Connection, Praxis, GrammaTech, NVIDIA, Synopsys, Mathworks, and Dassault Aviation. SMT solvers are now standard engines in numerous industrial applications, some of which (like scheduling) are outside the scope of deductive reasoning and formal verification — the original home community of most of the award recipients.

The following are some historical notes on the development of the SMT community and the role played by the award recipients and others.

The growing interest and need for powerful decision procedures led to the Satisfiability-Modulo-Theory Library (SMT-LIB) initiative. The main purpose of this initiative was to streamline the research and tool development in the field.

As a first step, Ranise and Tinelli developed the SMT-LIB standard, which defines a common language for benchmarks and formally specifies various theories that attract enough interest in the research community and have a sufficiently large set of publicly available benchmarks. This standard is now supported by dozens of solvers. The standard is an ongoing effort: Recently, Barrett, Stump, and Tinelli published version 2.0 of the standard — an 80-page document — which includes new theories, various simplifications of the grammar, and a command language.

As a second step, the organizers started collecting benchmarks in this format, and today the SMT-LIB repository, which is mostly managed by Barrett, Deters and Tinelli, includes about 94,000 benchmarks in the SMT-LIB format, classified into 22 divisions.

A third step was to initiate the SMT-COMP annual competition for SMT solvers, with a separate track for each division. This competition attracts 10 to 15 solvers every year. Aaron Stump, Clark Barrett, Leonardo de Moura, Morgan Deters, and Albert Oliveras have been the key players in this competition throughout the years.

A fourth step was to initiate SMT-EXEC, led by Deters and Stump, which is a server farm for the use of SMT-solver developers. Developers submit their executables through a web interface, and get detailed results comparing their work to other solvers with respect to the benchmarks in the SMT-lib repository.

These four steps have promoted the field dramatically. Only a few years back, it was very hard to get benchmarks. Every tool had its own language standard; hence, the benchmarks could not be migrated without translation. Moreover, there was no good way to compare tools and methods. Through the aforementioned efforts, these problems have been solved and, consequently, the number of tools and research papers dedicated to this field is now steadily

Given the scope of the award — the most influential work in formal and nonformal verification in the last five years — receiving it is a major compliment to the joint effort of this group and recognition of the great impact that the SMT community in general achieved.