Home • Intro • Tools • Specs • Thanks • SMT-LIB • Previous

SMT-COMP 2014 Participants

These solvers have expressed intention to participate in SMT-COMP 2014.
Solver main track application track Preliminary version solver id Final version solver id Seed System description Contacts
4Simp X - 916 1228 (4-Simp 2014)
config 1720 default		 20324 ? thansen@csse.unimelb.edu.au
abziz_portfolio_all_features X - 912 1275 abziz_portfolio_all_features
config 1803 default		 21381 ? Mohammad Abdul Aziz <mohammad.abdulaziz8@gmail.com>
abziz_portfolio_min_features X - 950 1273 abziz_portfolio_min_features
config 1801 default		 21381 ? Mohammad Abdul Aziz <mohammad.abdulaziz8@gmail.com>
AProVE X - 865 1229
config 1721 default		 2094937 AProVE Carsten Fuhs <c.fuhs@cs.ucl.ac.uk>
Boolector X - 911 : config 1136: 1218
config 1703 boolector		 42 Boolector Mathias Preiner <mathias.preiner@jku.at>; Aina Niemetz <aina.niemetz@jku.at>; Armin Biere <biere@jku.at>
Boolector (dual propagation) X - 911 : config 1134 1218
config 1701 boolectord		 42 Boolector Mathias Preiner <mathias.preiner@jku.at>; Aina Niemetz <aina.niemetz@jku.at>; Armin Biere <biere@jku.at>
Boolector (justification) X - 911 : config 1135 1218
config 1702 boolectorj		 42 Boolector Mathias Preiner <mathias.preiner@jku.at>; Aina Niemetz <aina.niemetz@jku.at>; Armin Biere <biere@jku.at>
CVC3 X X 900 1262
config 1785 default		 33333 CVC3 Clark Barrett <barrett@cs.nyu.edu>;Morgan Deters <mdeters@cs.nyu.edu>
CVC4 X X 898; application track=899 1257 CVC4 f7118b2:
config 1778
app config 1779 application		 44444 CVC4 Clark Barrett <barrett@cs.nyu.edu>;Morgan Deters <mdeters@cs.nyu.edu>
Kleaver-STP X - 893 1196 Kleaver-indie-more-typed
config 1738 kleaver_indie_1		 12739 Kleaver Hristina Palikareva <h.palikareva@imperial.ac.uk>; Cristian Cadar <c.cadar@imperial.ac.uk>
Kleaver-portfolio X - 894 1196 Kleaver-indie-more-typed
config 1740 kleaver_portfolio		 12739 Kleaver Hristina Palikareva <h.palikareva@imperial.ac.uk>; Cristian Cadar <c.cadar@imperial.ac.uk>
OpenSMT2 X - 921 1204 OpenSMT2-2014-06-14b
config 1789 default		 1984 OpenSMT antti.hyvarinen@gmail.com
raSAT X - 922 1199 raSAT-main-track-final
config 1654 default.sh		 18643 raSAT Tung Vu Xuan <tungvx@jaist.ac.jp>
SMTInterpol X X 1075 smtinterpol-2.1-118-g3dada2f 1075 smtinterpol-2.1-118-g3dada2f
config 1375 default		 3154861623 SMTInterpol hoenicke@informatik.uni-freiburg.de;christj@informatik.uni-freiburg.de
sonolar (sonolar_smtcomp-2014) X - 938 938
config 1173 default		 4 SONOLAR florian@informatik.uni-bremen.de
STP-CryptoMiniSat4 X - 968 1240 stp-cryptominisat4
config 1750 default		 1337 STP-CryptoMiniSat4 soos.mate@gmail.com
veriT X - 860 1269 veriT-smtcomp2014
config 1797 default		 1027 veriT david.deharbe@loria.fr; Pascal.Fontaine@inria.fr
Yices2 X X 1095 (config=default); app track config=incremental 1259 Yices-2.2.1-smtcomp2014
config 1781 default
app config 1782 incremental		 22908 Yices bruno@csl.sri.com
MathSAT 5 (non-competitive) X ? 174 1079
config 1384 default		 - - -
Z3 (non-competitive) X X 1286 config 1815 default;
app ?		 - - -
These are the logic divisions in which each solver is competing.
Solver ALIA AUFLIA AUFLIRA AUFNIRA BV LIA LRA NIA NRA QF_ABV QF_ALIA QF_AUFBV QF_AUFLIA QF_AX QF_BV QF_IDL QF_LIA QF_LRA QF_NIA QF_NRA QF_RDL QF_UF QF_UFBV QF_UFIDL QF_UFLIA QF_UFLRA QF_UFNIA QF_UFNRA UF UFBV UFIDL UFLIA UFLRA UFNIA
4Simp X
Abziz X
Abziz2 X
AProVE X
Boolector X
Boolector-d X
Boolector-j X
CVC3 X X X X X X X X X X X X X X X X X X X
CVC4 X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X
Kleaver-STP X
Kleaver-portfolio X
OpenSMT2 X
raSAT X
SMTInterpol X X X X X X X X
SONOLAR X X
STP-CryptoMiniSat4 X
veriT X X X X X X X X X X X X X X X X X
Yices2 X X X X X X X X X X X X X X X
MathSAT5 (non-competitive) X X X X X X X X X X X X
Z3 (non-competitive) X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X

These are the solvers participating in the Separation Logic competition. This is a separate competition being conducted with SMT-like solvers that solve encodings of separation logic problems. It is separate from SMT-COMP, though it is using the same infrastructure and being conducted by the same organizing committee. The relationship of the associated logic to SMT-LIB is currently under discussion.
Solver Preliminary version solver id Final version solver id System description Contacts
Cyclist-SL 1136 1136
config 1487 default
pre: 113 SL-CYCLIST3		 Cyclist-SL Nikos Gorogiannis <nikos.gorogiannis@gmail.com>
SLSAT 1137 1137
config 1488 default
pre: 117 SL-SAT3		 SLSAT Nikos Gorogiannis <nikos.gorogiannis@gmail.com>
Asterix 986 986
config 1233 default.sh
pre: none		 Asterix Juan A. Navarro Perez <juan.navarro@ucl.ac.uk>; Andrey Rybalchenko <rybal@microsoft.com>
SLEEK 1084 (default configuration) 1277 sleek-05
config 1806 default
pre: 115 SL-SLEEK3;
late correction for output format: 1297 sleek-06, config 1834 default		 SLEEK Le Quang Loc <locle@comp.nus.edu.sg>; Chin Wei Ngan <chinwn@comp.nus.edu.sg>
SLIDE 920 1255 (SLIDE-final)
config 1775 SLD_Input
pre: 116 SL-SLIDE3		 SLIDE Adam Rogalewicz <rogalew@fit.vutbr.cz>Radu IOSIF <; Radu.Iosif@imag.fr>; Tomas Vojnar <vojnar@fit.vutbr.cz>
SPEN 971 1280 SPEN 1.09
config 1809 spen.sh
pre: 118 SL-SPEN3		 SPEN Mihaela Sighireanu <mihaela.sighireanu@gmail.com>
These are the benchmark divisions in which each solver is competing.
Solver UDB_sat UDB_entl sll0a_sat sll0a_entl FDB_entl
Asterix X X
Cyclist-SL X X X
SLSAT X X
SLEEK X X X X X
SLIDE X X
SPEN X X X
Home • Intro • Tools • Specs • Thanks • SMT-LIB • Previous

Last modified: Tue 17 Feb 2015 15:00 UTC
 Valid XHTML 1.0 Valid CSS!