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, 2010.

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

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

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

F. Bobot, J. C. 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, pp.17-26, 2014.
DOI : 10.1007/978-3-319-08970-6_2

M. Christakis, K. R. Leino, P. Müller, and V. Wüstholz, Integrated Environment for Diagnosing Verification Errors, 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, 2009.
DOI : 10.1007/978-3-540-74591-4_15

D. R. Cok, Improved usability and performance of SMT solvers for debugging specifications, International Journal on Software Tools for Technology Transfer, vol.45, issue.3, pp.467-481, 2010.
DOI : 10.1007/s10009-010-0138-x

D. R. Cok, OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse, Electronic Proceedings in Theoretical Computer Science, vol.149, pp.79-92, 2014.
DOI : 10.4204/EPTCS.149.8

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

J. C. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, 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, Computer Aided Verification, pp.453-456, 2004.
DOI : 10.1007/978-3-540-27813-9_35

D. Hauzar, C. Marché, and Y. Moy, Counterexamples from proof failures in the SPARK program verifier, Research Report Inria, vol.8854, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01271174

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

L. Goues, C. Leino, K. R. Moskal, and M. , The Boogie Verification Debugger, Software Engineering and Formal Methods, pp.407-414, 2011.

K. R. Leino, T. Millstein, and J. B. Saxe, Generating error traces from verification-condition counterexamples, Science of Computer Programming, vol.55, issue.1-3, pp.1-3, 2005.
DOI : 10.1016/j.scico.2004.05.016

K. R. Leino and V. Wüstholz, The Dafny Integrated Development Environment, Electronic Proceedings in Theoretical Computer Science, vol.149, pp.3-15, 2014.
DOI : 10.4204/EPTCS.149.2

J. W. Mccormick and P. C. Chapin, Building High Integrity Applications with SPARK, 2015.
DOI : 10.1017/CBO9781139629294

L. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, LNCS, vol.4963, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

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

G. Petiot, N. Kosmatov, B. Botella, A. Giorgetti, and J. Julliand, Your Proof Fails? Testing Helps to Find the Reason, 2015.
DOI : 10.1007/978-3-662-49674-9_25

F. Schanda and M. Brain, Using Answer Set Programming in the Development of Verified Software, Technical Communications of the 28th Int. Conf. on Logic Programming. LIPIcs, pp.72-85, 2012.

E. Torlak and D. Jackson, Kodkod: A Relational Model Finder, pp.632-647, 2007.
DOI : 10.1007/978-3-540-71209-1_49