Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle & Christian Herde (2011):
Parallel SAT solving in bounded model checking 21(1),
pp. 5–21,
doi:10.1093/logcom/exp002.
J. Barnat, L. Brim, M. Češka & P. Ročkai (2010):
DiVinE: Parallel Distributed Model Checker (Tool paper).
In: HiBi/PDMC 2010.
IEEE,
doi:10.1109/PDMC-HiBi.2010.9.
Clark Barrett & Cesare Tinelli (2007):
CVC3.
In: W. Damm & H. Hermanns: CAV'07,
LNCS.
Springer,
doi:10.1007/978-3-540-73368-3_34.
Bruno Dutertre & Leonardo de Moura (2006):
The YICES SMT Solver.
Technical Report.
SRI International.
Available at http://yices.csl.sri.com/.
Niklas Eén & Niklas Sörensson (2003):
Temporal induction by incremental SAT solving.
Electr. Notes Theor. Comput. Sci. 89(4),
doi:10.1016/S1571-0661(05)82542-3.
George Hagen & Cesare Tinelli (2008):
Scaling up the formal verification of Lustre programs with SMT-based techniques.
In: FMCAD '08,
Piscataway, NJ, USA,
pp. 1–9,
doi:10.1109/FMCAD.2008.ECP.19.
N. Halbwachs, P. Caspi, P. Raymond & D. Pilaud (1991):
The synchronous data-flow programming language Lustre.
Proceedings of the IEEE 79(9),
pp. 1305–1320,
doi:10.1109/5.97300.
Temesghen Kahsai, Yeting Ge & Cesare Tinelli (2011):
Instantiation-Based Invariant Discovery.
In: NFM 2011,
LNCS 6617.
Springer,
pp. 192–207.
Available at http://dl.acm.org/citation.cfm?id=1986308.1986326.
Leonardo de Moura, Harald Rueß & Maria Sorea (2003):
Bounded Model Checking and Induction: From Refutation to Verification.
In: CAV 2003,
LNCS 2725.
Springer,
doi:10.1007/978-3-540-70952-7_21.
Peter S. Pacheco (1997):
Parallel programming with MPI.
Morgan Kaufmann Publishers Inc..
Mary Sheeran, Satnam Singh & Gunnar Stålmarck (2000):
Checking Safety Properties Using Induction and a SAT-Solver.
In: FMCAD '00.
Springer-Verlag,
London, UK,
pp. 108–125,
doi:10.1007/3-540-40922-X_8.
Siert Wieringa, Matti Niemenmaa & Keijo Heljanko (2009):
Tarmo: A Framework for Parallelized Bounded Model Checking.
In: PDMC '09,
pp. 62–76,
doi:10.4204/EPTCS.14.5.
eptcs@eptcs.org