Clark Barrett, Aaron Stump, and Cesare Tinelli.
The Satisfiability Modulo Theories Library (SMT-LIB),
www.SMT-LIB.org.
2010.
BibTeX entry
Clark Barrett, Aaron Stump, and Cesare Tinelli.
The SMT-LIB Standard - Version 2.0.
Proceedings of the 8th International Workshop on Satisfiability Modulo Theories
(Edinburgh, England), 2010.
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 Morgan Deters. The querying and browsing interface for the repository was developed and is maintained by Morgan Deters.
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, Roberto Bruttomesso, Morgan Deters, Alberto Griggio, and Leonardo de Moura, 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 Babić,
Adrian Bock,
Sergey Berezin,
Nikolaj Bjørner,
Maria Paola Bonacina,
Sascha Boehme,
Alessandro Cimatti,
David Cok,
Christopher Conway,
David Deharbe,
Bruno Dutertre,
Kousha Etessami,
Pascal Fontaine,
Anders Franzen,
Vijay Ganesh,
Amit Goel,
Alberto Griggio,
Jim Grundy,
John Harrison,
Jochen Hoenicke,
Predrag Janičić,
Paul Jackson,
Joseph Kiniry,
Daniel Kroening,
Sava Krstić,
Shuvendu Lahiri,
Nuno Lopes,
Jinpeng Lv,
John Matthews,
Paulo Matos,
Michał Moskal,
Jose Meseguer,
Leonardo de Moura,
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,
Johannes Waldmann,
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 Babić,
Armin Biere,
Nikolaj Bjørner,
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,
Gert-Martin Greuel,
Alberto Griggio,
Sumit Gulwani,
Trevor Hansen,
Keijo Heljanko,
Andre Henning,
Paul Jackson,
Ivan Jager,
Tomi Janhunen,
Dejan Jovanović,
Hyondeuk Kim,
Tim King,
Daniel Kroening,
Wolfgang Kunz,
Stefan Kupferschmid,
Shuvendu Lahiri,
Rustan Leino,
Rhishikesh Limaye,
Fred Maris,
John Matthews,
Claude Marche,
David Molnar,
Panagiotis Manolios,
Michał Moskal,
Leonardo de Moura,
Ilkka Niemela,
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,
Christoph Wintersteiger,
Harald Roman Zankl,
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 previous 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.