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.
Benchmarks
The SMT-LIB benchmark collection is co-managed by
Clark Barrett,
Pascal Fontaine,
Aina Niemetz,
Mathias Preiner, and
Hans-Jörg Schurr.
Previous benchmark managers include
Leonardo de Moura,
and
Christoph Wintersteiger.
Since 2022, new benchmarks are checked for compliance with the Dolmen tool developed by
Guillaume Bury.
The collection is currently hosted on a GitLab server at the University of Iowa.
The server was initially set up and populated by Alain Mebsout.
Until 2013, the benchmark collection was co-managed by
Clark Barrett and Morgan Deters.
The querying and browsing interface for that, now discontinued, collection was developed and maintained by Morgan Deters.
An official copy of the benchmarks is also available on the StarExec solver execution service.
SMT-COMP
A great impulse to the growth of the benchmark collection 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 Haniel Barbosa, Clark Barrett, Roberto Bruttomesso, David Cok, Sylvain Conchon, David Deharbe, Morgan Deters, Alberto Griggio, Liana Hadarean, Matthias Heizmann, Jochen Hoenicke, Antti Hyvarinen, Leonardo de Moura, Aina Niemetz, Albert Oliveras, Giles Reger, Aaron Stump, 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 standard, the library, or the solver competition (we apologize in advance for any omissions):
Peter Andrews, Alessandro Armando, Domagoj Babić, Kshitij Bansal, François Bobot, Adrian Bock, Sergey Berezin, Murphy Berzish, 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, Joxan Jaffar, 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, Anthony Lin, Tianyi Liang, Dan Liew, Nuno Lopes, Jinpeng Lv, Claude Marchè, Paulo Matos, John Matthews, Raphaël Michel, David Monniaux, Michał Moskal, Jose Meseguer, Leonardo de Moura, Greg Nelson, Ilkka Niemela, Aina Niemetz, Robert Nieuwenhuis, Andres Nötzli, 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):
Nicolas Amat, Domagoj Babić, Nicolas Beauger, Armin Biere, Nikolaj Bjørner, Miquel Bofill, Russell Bradford, Aaron Bradley, Brian Brady, Martin Bromberger, Geoffrey Brown, Robert Brummayer, Roberto Bruttomesso, Randy Bryant, Sebastian Buchwald, Thomas Bunk, Rick Butler, Claudio Castellini, Alex Coffin, James Davenport, Morgan Deters, Michael Decoster, David Deharbe, Stefan Disch, Bruno Dutertre, Matthew England, Levent Erkok, Matteo Favaro, Jean-Christophe Filliâtre, Bernd Fischer, Pascal Fontaine, Andreas Fried, Malay Ganai, Vijay Ganesh, Alexandre Gonzalvez, Yeting Ge, Bernhard Gleiss, Patrice Godefroid, Aman Goel, Gert-Martin Greuel, Alberto Griggio, Matthias Güdemann, Sumit Gulwani, Trevor Hansen, Matthias Heizmann, Keijo Heljanko, Andre Henning, Julien Henry, Jochen Hoenicke, Anastasiia Izycheva, Paul Jackson, Ivan Jager, Tomi Janhunen, Fuqi Jia, Jie-Hong Roland Jiang, Andrew Jones, Dejan Jovanović, Johannes Kanig, Gergely Kovasznai, Hyondeuk Kim, Tim King, Daniel Kröning, Wolfgang Kunz, Stefan Kupferschmid, Shuvendu Lahiri, Rustan Leino, Bohan Li, Rhishikesh Limaye, Nuno Lopes, Fred Maris, John Matthews, Claude Marchè, David Molnar, Makai Mann, Panagiotis Manolios, Michał Moskal, Leonardo de Moura, Yannick Moy, Casey Mulligan, Ilkka Niemela, Robert Nieuwenhuis, Andres Nötzli, Alex Ozdemir, Kazuhiro Ogata, Albert Oliveras, Hristina Palikareva, Lee Pike, Lorenzo Platania, Andre Platzer, Florian Pigorsch, Elizabeth Polgreen, Hernán Ponce de Leon, Mathias Preiner, Shaz Qaader, Jan-David Quesel, Zvonimir Rakamaric, Andrew Reynolds, Miguel del Rio Almajano Enric Rodriguez-Carbonell, John Rushby, Johann-Tobias Schäg, Maria Schett, Michael Schidlowsky, Johannes Schoisswohl, Christoph Scholl, Hans-Jörg Schurr, Sanjit Seshia, Hossein Sheini, Da Shen, Jiae Shin, Saurabh Srivastava, Maria Sorea, Volker Sorge, Dominik Stoffel, Ofer Strichman, Christoph Sticksel, Aaron Stump, Geoff Sutcliffe, Naoyuki Tamura, Nestan Tsiskaridze, Aaron Tomb, Zak Tonks, Ali Uncu, Miroslav Velev, Ramarathnam Venkatesan, Alexey Vishnyakov, Johannes Waldmann, Angela Wallenburg, Tjark Weber, Markus Wedler, Philipp Wendler, Oliver Wienand, Christoph Wintersteiger, Clifford Wolf, Dennis Yurichev, Harald Roman Zankl, Yoni Zohar, 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 Rodin 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:
- the National Science Foundation, 2006-2008 (with grants 0551646, 0551645 and 0551697)
- the Obermann Center for Advanced Studies, 2007
- Intel Corporation, 2005, 2006
- Semiconductor Research Corporation, 2008-9 (with grant 2008-TJ-1850)
Web Site
This site was developed and is currently maintained by Cesare Tinelli, with contributions from Clark Barrett, Pascal Fontaine, Matthias Preiner, and Hans-Jörg Schurr.
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.