J. Barnes, Programming in Ada 2012, 2014.
DOI : 10.1017/CBO9781139696616

C. Barrett, A. Stump, and C. Tinelli, The SMT-LIB Standard: Version 2.0, Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, 2010.

J. Christian-blanchette and T. Nipkow, Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder, Interactive Theorem Proving, First International Conference, pp.131-146, 2010.
DOI : 10.1007/978-3-642-14052-5_11

F. Bobot, S. Conchon, É. Contejean, M. Iguernelala, S. Lescuyer et al., The Alt-Ergo automated theorem prover, 2008.

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Why3: Shepherd your herd of provers, Boogie 2011: First International Workshop on Intermediate Verification Languages, pp.53-64, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Let???s verify this with Why3, International Journal on Software Tools for Technology Transfer, vol.7, issue.5, pp.709-727, 2015.
DOI : 10.1007/s10009-014-0314-5

R. Chapman and F. Schanda, Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK, Interactive Theorem Proving -5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 Proceedings, volume 8558 of Lecture Notes in Computer Science, pp.17-26, 2014.
DOI : 10.1007/978-3-319-08970-6_2

M. Christakis, K. Rustan, M. Leino, P. Müller, and V. Wüstholz, Integrated Environment for Diagnosing Verification Errors, 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16, 2016.
DOI : 10.1007/978-3-662-49674-9_25

E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal et al., VCC: A Practical System for Verifying Concurrent C, Theorem Proving in Higher Order Logics (TPHOLs), 2009.
DOI : 10.1007/978-3-540-74591-4_15

R. David and . Cok, Openjml: Software verification for java 7 using jml, openjdk, and eclipse, Proceedings 1st Workshop on Formal Integrated Development Environment, pp.79-92, 2014.

L. De, M. , and N. Bjørner, Z3, an efficient SMT solver, TACAS, pp.337-340, 2008.

J. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, 19th International Conference on Computer Aided Verification, pp.173-177, 2007.
DOI : 10.1007/978-3-540-73368-3_21

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

A. Groce, D. Kroening, and F. Lerda, Understanding Counterexamples with explain, Lecture Notes in Computer Science, vol.3114, pp.453-456, 2004.
DOI : 10.1007/978-3-540-27813-9_35
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.5767

B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx et al., VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java, NASA Formal Methods, pp.41-55, 2011.
DOI : 10.1007/11691372_19

C. Le-goues, K. Rustan, M. Leino, and M. Moskal, The Boogie Verification Debugger (Tool Paper), Software Engineering and Formal Methods -9th International Conference, pp.407-414, 2011.
DOI : 10.1007/978-3-642-21437-0_8

K. Rustan, M. Leino, and V. Wüstholz, The Dafny integrated development environment, Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014 of Electronic Proceedings in Theoretical Computer Science, pp.3-15, 2014.

W. John, P. C. Mccormick, and . Chapin, Building High Integrity Applications with SPARK, 2015.

P. Müller and J. N. Ruskiewicz, Using Debuggers to Understand Failed Verification Attempts, 17th International Symposium on Formal Methods, pp.73-87, 2011.
DOI : 10.1145/249094.249108