We have used a lot of materials from the Internet. And these are an incomplete list of them. We want to say thank you to all those geniuses behind these documentations/papers/reports.
[BaBE11] Barker-Plummer, David; Barwise, Jon; Etchemendy, John: Language, Proof, and Logic. 2. Aufl. : Center for the Study of Language and Inf, 2011 — ISBN 1575866323
[HuRy04] Huth, M.; Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems. 2. Aufl. : Cambridge University Press Cambridge, UK, 2004
[AvBM01] Avellone, A.; Benini, M.; Moscato, U.: How to avoid the formal verification of a theorem prover. In: Logic journal of IGPL 9 (2001), Nr. 1, S. 1–25
[BDOS08] Barrett, Clark; Deters, Morgan; Oliveras, Albert; Stump, Aaron: Design and results of the 4th annual satisfiability modulo theories competition (SMT-COMP 2008). In: To appear 6 (2008)
[BeKL12] Bestavros, Azer; Kfoury, Assaf; Lapets, Andrei: Seamless Composition and Integration: A Perspective on Formal Methods Research (2012)
[BFMP11] Bobot, Franccois; Filliâtre, Jean-Christophe; Marché, Claude; Paskevich, Andrei: The Why3 platform : LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.64 edition, 2011
[BoFi00] Bobot, Franccois; Filliâtre, Jean-Christophe: Separation Predicates: a Taste of Separation Logic in First-Order Logic
[EcPe09] Echenim, M.; Peltier, N.: A New Instantiation Scheme for Satisfiability Modulo Theories (Research Report) (2009)
[GuKM11] Guitton, Jérôme; Kanig, Johannes; Moy, Yannick: Why Hi-Lite Ada? In: Rustan, et al.[32] (2011), S. 27–39
[LaMi00] Lapets, Andrei; Mirzaei, Saber: Towards Lightweight Integration of SMT Solvers
[MoBj09] De Moura, L.; Bjørner, N.: Satisfiability modulo theories: An appetizer. In: Formal Methods: Foundations and Applications (2009), S. 23–36
[Mour00] de Moura, L.: SMT Solvers: Theory and Implementation
[RuSh07] Rushby, John; Shankar, Natarajan: AFM’07: Second Workshop on Automated Formal Methods: November 6, 2007, Atlanta, Georgia : Association for Computing Machinery, 2007