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, 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 organizers 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,
John Harrison,
Predrag Janicic,
Paul Jackson,
Joseph Kiniry,
Daniel Kroening,
Sava Krstic,
Shuvendu Lahiri,
Paulo Matos,
Michal Moskal,
Jose Meseguer,
Greg Nelson,
Ilkka Niemela,
Robert Nieuwenhuis,
Albert Oliveras,
Frank Pfenning,
Philipp Ruemmer,
Harald Ruess,
James Saxe,
Roberto Sebastiani,
Sanjit Seshia,
Natarajan Shankar,
Eli Singerman,
Fabio Somenzi,
Ofer Strichman,
Geoff Sutcliffe,
Moshe Vardi,
Andrei Voronkov,
Tjark Weber,
Georg Weissenbacher,
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,
Nikolaj Bjorner,
Miquel Bofill,
Aaron Bradley,
Brian Brady,
Geoffrey Brown,
Robert Brummayer,
Roberto Bruttomesso,
Randy Bryant,
Rick Butler,
Claudio Castellini,
Morgan Deters,
Michael Decoster,
Stefan Disch,
Bruno Dutertre,
Levent Erkok,
Jean-Christophe Filliatre,
Bernd Fischer,
Pascal Fontaine,
Malay Ganai,
Vijay Ganesh,
Yeting Ge,
Patrice Godefroid,
Alberto Griggio,
Gert-Martin Greuel,
Sumit Gulwani,
Keijo Heljanko,
Andre Henning,
Paul Jackson,
Dejan Jovanovic,
Hyondeuk Kim,
Tim King,
Daniel Kroening,
Wolfgang Kunz,
Stefan Kupferschmid,
Shuvendu Lahiri,
Rustan Leino,
Rhishikesh Limaye,
John Matthews,
Claude Marche,
David Molnar,
Panagiotis Manolios,
Michal Moskal,
Leonardo de Moura,
Robert Nieuwenhuis,
Kazuhiro Ogata,
Albert Oliveras,
Lee Pike,
Lorenzo Platania,
Florian Pigorsch,
Shaz Qaader,
Zvonimir Rakamaric,
Enric Rodriguez-Carbonell,
John Rushby,
Michael Schidlowsky,
Christoph Scholl,
Sanjit Seshia,
Hossein Sheini,
Jiae Shin,
Saurabh Srivastava,
Maria Sorea,
Volker Sorge,
Dominik Stoffel,
Ofer Strichman,
Aaron Stump,
Geoff Sutcliffe,
Naoyuki Tamura,
Miroslav Velev,
Ramarathnam Venkatesan,
Johannes Waldmann,
Angela Wallenburg,
Markus Wedler,
Oliver Wienand,
the Averest team,
Calypto Design Systems,
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 or corporations.