References
========================

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.

Website Links
-------------------

	.. [Alt-Ergo] http://alt-ergo.lri.fr/
	.. [CVC4] http://cvc4.cs.nyu.edu/web/
	.. [SMTLIB] http://smtlib.org/

Books
-------------------

	.. [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 <http://dl.acm.org/ft_gateway.cfm?id=1086674&type=pdf>`_


Papers/Reports
----------------

	.. [AFGK11] `Armand, Mickaël; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Théry, Laurent; Wener, Benjamin: Verifying SAT and SMT in Coq for a fully automated decision procedure. In: PSATTT’11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, 2011 <http://hal.inria.fr/inria-00614041/>`_
	.. [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 <http://jigpal.oxfordjournals.org/content/9/1/1.short>`_
	.. [BaST10] `Barrett, Clark; Stump, Aaron; Tinelli, Cesare: The smt-lib standard: Version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, England). Bd. 13, 2010 <http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf>`_
	.. [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) <http://cs1.cs.nyu.edu/web/Research/TechReports/TR2010-931/TR2010-931.pdf>`_
	.. [BeKL12] `Bestavros, Azer; Kfoury, Assaf; Lapets, Andrei: Seamless Composition and Integration: A Perspective on Formal Methods Research (2012) <http://www.cs.bu.edu/techreports/pdf/2012-001-mscs-editorial.pdf>`_
	.. [BFMP11] `Bobot, Fran\ccois; Filliâtre, Jean-Christophe; Marché, Claude; Paskevich, Andrei: The Why3 platform : LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.64 edition, 2011 <https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf>`_
	.. [BMBC08] `Barrett, Clark; de Moura, Leonardo; Bjørner, Nikolaj; Cimatti, Alessandro; ITC-IRST, Trento; Dutertre, Bruno; Krstic, Sava; Nieuwenhuis, Robert; u. a.: SMT 2008: 6th International Workshop on Satisfiability Modulo Theories. In: Workshop: July. Bd. 7, 2008, S. 8 <http://research.microsoft.com/en-us/um/people/leonardo/SMT08_proceedings.pdf>`_
	.. [BoFi00] `Bobot, Fran\ccois; Filliâtre, Jean-Christophe: Separation Predicates: a Taste of Separation Logic in First-Order Logic <http://proval.lri.fr/publications/bobot12icfem.pdf>`_
	.. [CoCK06] `Conchon, Sylvain; Contejean, Evelyne; Kanig, Johannes: Ergo: a theorem prover for polymorphic first-order logic modulo theories. In: Artigo sobre o Ergo. Disponível em:< http://ergo. lri. fr/papers/ergo. ps>. Acesso em 17 (2006) <http://ergo.lri.fr/papers/ergo.ps>`_
	.. [EcPe09] `Echenim, M.; Peltier, N.: A New Instantiation Scheme for Satisfiability Modulo Theories (Research Report) (2009) <http://membres-lig.imag.fr/peltier/rr-smt.pdf>`_
	.. [GuKM11] `Guitton, Jérôme; Kanig, Johannes; Moy, Yannick: Why Hi-Lite Ada? In: Rustan, et al.[32] (2011), S. 27–39 <http://research.microsoft.com/en-us/um/people/moskal/boogie2011/proc1.pdf#page=33>`_
	.. [LaMi00] `Lapets, Andrei; Mirzaei, Saber: Towards Lightweight Integration of SMT Solvers <http://www.cs.bu.edu/techreports/pdf/2012-017-smt-integration.pdf>`_
	.. [MoBj09] `De Moura, L.; Bjørner, N.: Satisfiability modulo theories: An appetizer. In: Formal Methods: Foundations and Applications (2009), S. 23–36 <http://www.springerlink.com/index/B4810780418L2M35.pdf>`_
	.. [Mour00] `de Moura, L.: SMT Solvers: Theory and Implementation <http://research.microsoft.com/en-us/um/people/leonardo/files/oregon08.pdf>`_
	.. [PrBG05] `Prasad, M. R.; Biere, A.; Gupta, A.: A survey of recent advances in SAT-based formal verification. In: International Journal on Software Tools for Technology Transfer (STTT) 7 (2005), Nr. 2, S. 156–173 <http://www.springerlink.com/index/ucyjdvmqaquetapx.pdf>`_
	.. [RuSh07] `Rushby, John; Shankar, Natarajan: AFM’07: Second Workshop on Automated Formal Methods: November 6, 2007, Atlanta, Georgia : Association for Computing Machinery, 2007 <http://fm.csl.sri.com/AFM07/afm07-preprint.pdf>`_