October 5-7, 2010
Organized by IBM R&D Labs in Israel

HVC Award

The HVC Award recognizes the most promising contribution to fields of software and hardware verification and test in the last five years.

HVC Award committee:

Ofer Strichman - Technion (Chair)

Patrice Godefroid - Microsoft Research

Roderick Bloem - Graz University of Technology

Kerstin Eder - University of Bristol

Mooly Sagiv - Tel-Aviv University

The HVC 2010 award 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 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.

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 committee recognizes the fact that the development of the SMT community, as any other community, is a joint effort of many people, but nevertheless decided to limit the award to no more than five people, and accordingly selected (alphabetically) Clark Barrett, Leonardo De Moura, Silvio Ranise, Aaron Stump, and Cesare Tinelli, for their major role in developing the SMT-LIB standard, the SMT-LIB repository, the SMT-COMP competition, the web-based server farm for SMT solvers' developers SMT-EXEC, and more generally for bringing SMT, together with others, to the place it is in today in the industry and in the academia.

The academic impact of this community can be measured by the number of articles it produces. The term "Satisfiability modulo theories", which was born less than 10 years ago, has 1180 hits in Google Scholar as of Aug. 2010, and there are probably hundreds of other papers that are associated with SMT but do not use this term explicitly. The impact of this field on the industry can be measured by its 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, Dassault Aviation, … and the list continues. 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 initiative (SMT-LIB for short). 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-solvers' developers. Developers submit their executables through a web interface, and get detailed results comparing 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 and hence the benchmarks could not be migrated without translation; moreover, there was no good way to compare tools and methods. These problems have been solved because of the above initiative, and consequently, the number of tools and research papers dedicated to this field is now steadily growing as indicated above.

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.