The SMT-LIB Initiative and the Rise of SMT: (HVC 2010 Award Talk)

Satisfiability modulo theories (SMT) is a branch of automated reasoning that builds on advances in propositional satisfiability and on decision procedures for first-order reasoning. Its defining feature is the use of reasoning methods specific to logical theories of interest in target applications. Advances in SMT research and technology have led in the last few years to the development of very powerful satisfiability solvers and to an explosion of applications. SMT solvers are now used for processor verification, equivalence checking, bounded and unbounded model checking, predicate abstraction, static analysis, automated test case generation, extended static checking, scheduling and optimization. While the roots of SMT go back to work in the late 1970s and early 1980s on using decision procedures in formal methods, the field was born in the late 1990s with various independent attempts to harness the power of modern SAT solvers, reaching the current level of sophistication with the research and development advances of the last decade. Major enablers for these advances were SMT-LIB, a standardization and benchmark collection initiative supported by a large number of SMT researchers and users world-wide, and its offsprings: the SMT workshop, an international workshop bringing together SMT researchers and users of SMT applications or techniques; SMT-COMP, an international competition for SMT solvers supporting the SMT-LIB input format; and SMT-EXEC, a public execution service allowing researchers to configure and execute benchmarking experiments on SMT solvers. This talk provides historical perspectives on the development of the field and on the SMT-LIB initiative and its offsprings. It highlights the initiative’s milestones and main achievements, and the role of the authors and other major contributors in it. It then concludes with a brief discussion of a few promising directions for future research in SMT.