E. W. Dijkstra, A discipline of programming, Series in Automatic Computation, 1976.

K. R. 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.
DOI : 10.1007/3-540-57529-4_61
URL : http://arxiv.org/pdf/1404.6602

D. R. Cok, OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse, Proceedings 1st Workshop on Formal Integrated Development Environment, pp.79-92, 2014.
DOI : 10.1007/978-3-642-18070-5_13
URL : http://arxiv.org/pdf/1404.6608

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/978-3-642-02959-2_10

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

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

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

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

N. Kosmatov, C. Marché, Y. Moy, and J. Signoles, Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), pp.461-478, 2016.
DOI : 10.1007/978-3-662-46681-0_53
URL : https://hal.archives-ouvertes.fr/hal-01344110

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

M. Barnett, R. Deline, B. Jacobs, B. E. Chang, and K. R. Leino, Boogie: A Modular Reusable Verifier for Object-Oriented Programs, Formal Methods for Components and Objects: 4th International Symposium, pp.364-387, 2005.
DOI : 10.1007/11804192_17
URL : http://research.microsoft.com/~leino/papers/krml160.pdf

D. Hauzar, C. Marché, and Y. Moy, Counterexamples from Proof Failures in SPARK, pp.215-233, 2016.
DOI : 10.1007/978-3-540-71209-1_49
URL : https://hal.archives-ouvertes.fr/hal-01314885

C. Flanagan and J. B. Saxe, Avoiding exponential explosion: Generating compact verification conditions, Principles Of Programming Languages, pp.193-205, 2001.

K. R. Leino, Efficient weakest preconditions, Information Processing Letters, vol.93, issue.6, pp.281-288, 2005.
DOI : 10.1016/j.ipl.2004.10.015
URL : http://research.microsoft.com/pubs/70052/tr-2004-34.pdf

C. B. Lourenço, M. J. Frade, J. Sousa, and . Pinto, Formalizing singleassignment program verification: An adaptation-complete approach, 25th European Symposium on Programming, pp.41-67, 2016.

C. Dross, S. Conchon, J. Kanig, and A. Paskevich, Adding Decision Procedures to SMT Solvers Using Axioms with Triggers, Journal of Automated Reasoning, vol.53, issue.6, pp.387-457, 2016.
DOI : 10.1007/978-3-642-18275-4_28
URL : https://hal.archives-ouvertes.fr/hal-00915931

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

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

R. Chapman and F. Schanda, Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK, Proceedings Lecture Notes in Computer Science, vol.8558, pp.17-26, 2014.
DOI : 10.1007/978-3-319-08970-6_2

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 of LIPIcs, Leibniz-Zentrum fuer Informatik, pp.72-85, 2012.

A. Groce, D. Kroening, and F. Lerda, Understanding Counterexamples with explain, CAV, pp.453-456, 2004.
DOI : 10.1007/978-3-540-27813-9_35
URL : http://www-2.cs.cmu.edu/~agroce/cav04.pdf

J. C. 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
URL : http://www4.in.tum.de/~blanchet/tap2009-nitpick.pdf

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.209-226, 2005.
DOI : 10.1016/j.scico.2004.05.016
URL : https://doi.org/10.1016/j.scico.2004.05.016

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/978-1-4615-5229-1_12

C. , L. Goues, K. R. Leino, and M. , The Boogie Verification Debugger, Software Engineering and Formal Methods -9th International ConferenceSEFM), pp.407-414, 2011.

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
URL : http://research.microsoft.com/~moskal/pdf/tphol2009.pdf

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

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

M. Hentschel, R. Hähnle, and R. Bubel, Deductive Software Verification ? The KeY Book, Ch. Debugging and Visualization, pp.383-41310, 2016.

M. Christakis, K. R. 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, pp.424-441, 2016.
DOI : 10.1007/978-3-662-49674-9_25
URL : http://kar.kent.ac.uk/58940/1/TACAS-2016.pdf

G. Petiot, N. Kosmatov, B. Botella, A. Giorgetti, and J. Julliand, Your Proof Fails? Testing Helps to Find the Reason, Tests and Proofs -10th International Conference, pp.130-150, 2016.
DOI : 10.1007/11408901_21
URL : http://arxiv.org/pdf/1508.01691