Credits

Citing SMT-LIB

To cite SMT-LIB as a whole the best would be to use something like the following:

Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB), www.SMT-LIB.org. 2016. [BibTeX entry]

To cite a publication on the the SMT-LIB format specifically, please use:

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]

Major Players

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, Pascal Fontaine, and Cesare Tinelli. Previous coordinators include Silvio Ranise and Aaron Stump.

The SMT-LIB benchmark repository on StarExec is co-managed by Clark Barrett, Martin Brain, Pascal Fontaine, Leonardo de Moura, and Christoph Wintersteiger. Until 2013, it was co-managed by Clark Barrett and Morgan Deters. The querying and browsing interface for that repository was developed and 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, David Cok, Sylvain Conchon, David Deharbe, Morgan Deters, Alberto Griggio, Leonardo de Moura, Albert Oliveras, and Tjark Weber.

Suggestions and Feedback

The following additional people have contributed to the initiative over the years with their suggestions and feedback on the SMT-LIB format, the library, or the solver competition (we apologize in advance for any omissions):

Peter Andrews, Alessandro Armando, Domagoj Babić, François Bobot, Adrian Bock, Sergey Berezin, Nikolaj Bjørner, Maria Paola Bonacina, Sascha Boehme, Alessandro Cimatti, Adrien Champion, Jürgen Christ, David Cok, Christopher Conway, David Deharbe, Morgan Deters, Bruno Dutertre, Levent Erkok, Kousha Etessami, Pascal Fontaine, Anders Franzen, Andrew Gacek, Vijay Ganesh, Amit Goel, Alberto Griggio, Jim Grundy, John Harrison, Matthias Heizmann, Jochen Hoenicke, Predrag Janičić, Paul Jackson, Tim King, Joseph Kiniry, Daniel Kröning, Sava Krstić, Viktor Kuncak, Pierre van de Laar, Shuvendu Lahiri, Vincent Langenfeld, Florian Lapschies, Tianyi Liang, Nuno Lopes, Jinpeng Lv, Claude Marchè, Paulo Matos, John Matthews, David Monniaux, Michał Moskal, Jose Meseguer, Leonardo de Moura, Greg Nelson, Ilkka Niemela, Aina Niemetz, Robert Nieuwenhuis, Albert Oliveras, Frank Pfenning, Gabriele Paganelli, Andrew Reynolds, Cody Roux, Philipp Rümmer, Harald Rueß, James Saxe, Florian Schanda, Roberto Sebastiani, Sanjit Seshia, Natarajan Shankar, Eli Singerman, Fabio Somenzi, Ofer Strichman, Geoff Sutcliffe, Moshe Vardi, Margus Veanes, Andrei Voronkov, Johannes Waldmann, Tjark Weber, Georg Weissenbacher, Christoph Wintersteiger.

Benchmarks

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 (we apologize in advance for any omissions):

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 Filliâtre, Bernd Fischer, Pascal Fontaine, Malay Ganai, Vijay Ganesh, Yeting Ge, Patrice Godefroid, Gert-Martin Greuel, Alberto Griggio, Sumit Gulwani, Trevor Hansen, Matthias Heizmann, Keijo Heljanko, Andre Henning, Julien Henry, Paul Jackson, Ivan Jager, Tomi Janhunen, Dejan Jovanović, Gergely Kovasznai, Hyondeuk Kim, Tim King, Daniel Kröning, Wolfgang Kunz, Stefan Kupferschmid, Shuvendu Lahiri, Rustan Leino, Rhishikesh Limaye, Fred Maris, John Matthews, Claude Marchè, David Molnar, Panagiotis Manolios, Michał Moskal, Leonardo de Moura, Ilkka Niemela, Robert Nieuwenhuis, Kazuhiro Ogata, Albert Oliveras, Hristina Palikareva, Lee Pike, Lorenzo Platania, Andre Platzer, Florian Pigorsch, Shaz Qaader, Jan-David Quesel, Zvonimir Rakamaric, Andrew Reynolds, 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, Christoph Sticksel, Aaron Stump, Geoff Sutcliffe, Naoyuki Tamura, Aaron Tomb, Miroslav Velev, Ramarathnam Venkatesan, Johannes Waldmann, Angela Wallenburg, Markus Wedler, Philipp Wendler, Oliver Wienand, Christoph Wintersteiger, Harald Roman Zankl, the Averest team, Calypto Design Systems, the CVC Lite team, the CVC4 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.

Funding

The work on SMT-LIB has been partially supported over the years by the following companies and institutions:

Web Site

This site was developed and is currently maintained by Cesare Tinelli, with contributions from Clark Barrett and Pascal Fontaine.

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.