Clark Barrett, Silvio Ranise, Aaron Stump, and Cesare Tinelli.
The Satisfiability Modulo Theories Library (SMT-LIB),
www.SMT-LIB.org.
2008.
BibTeX entry
Silvio Ranise and Cesare Tinelli.
The SMT-LIB Standard: Version 1.2.
Technical Report,
Department of Computer Science,
The University of Iowa, 2006.
(Available at www.SMT-LIB.org .)
BibTeX entry
The SMT-LIB initiative was created by Silvio Ranise and Cesare Tinelli in 2002, after a proposal made at FroCoS 2002 by Alessandro Armando.
The initiative is currently co-ordinated by Clark Barrett, Silvio Ranise, Aaron Stump, and Cesare Tinelli.
The SMT-LIB benchmark repository is co-managed by Clark Barrett and Cesare Tinelli.
A great impulse to the growth of the repository and to SMT-LIB as a whole has been given by the affiliated solver competition SMT-COMP. Past and present organizer of SMT-COMP include Aaron Stump, Clark Barrett, Leonardo de Moura, Morgan Deters, and Albert Oliveras.
The following additional people have contributed to the initiative
with their suggestions and feedback on the SMT-LIB format, the library, or
the solver competition:
Peter Andrews,
Alessandro Armando,
Domagoj Babic,
Sergey Berezin,
Nikolaj Bjorner,
Maria Paola Bonacina,
Alessandro Cimatti,
Bruno Dutertre,
Kousha Etessami,
Vijay Ganesh,
Jim Grundy,
Joseph Kiniry,
Sava Krstic,
Predrag Janicic,
Shuvendu Lahiri,
Paulo Matos,
Michal Moskal,
Jose Meseguer,
Greg Nelson,
Ilkka Niemela,
Robert Nieuwenhuis,
Albert Oliveras,
Frank Pfenning,
Harald Ruess,
James Saxe,
Roberto Sebastiani,
Sanjit Seshia,
Natarajan Shankar,
Eli Singerman,
Fabio Somenzi,
Ofer Strichman,
Geoff Sutcliffe,
Moshe Vardi,
Andrei Voronkov,
Christoph Wintersteiger,
and probably some more people we are now forgetting.
(We apologize in advance for any omissions.)
The following people have also directly or indirectly contributed to SMT-LIB by
providing benchmarks natively in SMT-LIB format, or
translating existing benchmarks for us into SMT-LIB or similar formats, or
more generally making their benchmarks available to the research community:
Domagoj Babic,
Clark Barrett,
Armin Biere,
Aaron Bradley,
Geoffrey Brown,
Robert Brummayer,
Rick Butler,
Claudio Castellini,
Michael Decoster,
Bruno Dutertre,
Jean-Christophe Filliatre,
Bernd Fischer,
Pascal Fontaine,
Malay Ganai,
Vijay Ganesh,
Yeting Ge,
Alberto Griggio,
Keijo Heljanko,
Andre Henning,
Hyondeuk Kim,
Daniel Kroening,
Shuvendu Lahiri,
Rustan Leino,
Rhishikesh Limaye,
Claude Marche,
David Molnar,
Panagiotis Manolios,
Michal Moskal,
Leonardo de Moura,
Robert Nieuwenhuis,
Kazuhiro Ogata,
Albert Oliveras,
Lee Pike,
Lorenzo Platania,
Shaz Qaader,
Enric Rodriguez-Carbonell,
John Rushby,
Michael Schidlowsky,
Sanjit Seshia,
Hossein Sheini,
Jiae Shin,
Maria Sorea,
Volker Sorge,
Ofer Strichman,
Aaron Stump,
Geoff Sutcliffe,
Naoyuki Tamura,
Miroslav Velev,
the Averest team,
the CVC Lite team,
the CSP2SAT team,
the HarVey team,
the MathSAT team,
the MIPLIB team,
the SAL team,
the Simplify team,
the TPTP team,
the UCLID team,
the WiSA team,
and probably some more people we are now forgetting.
(We apologize in advance for any omissions.)
The work on SMT-LIB was partially supported by the following companies and institutions:
This site was developed and is currently maintained by
Cesare Tinelli,
with contributions from Clark Barrett and Silvio Ranise.
Any opinions, findings and conclusions or recommendations expressed in this site are those of the authors and do not necessarily reflect the views of the funding institutions.