J. R. Abrial, Modeling in Event-B: system and software engineering, 2010.
DOI : 10.1017/CBO9781139195881

J. R. Abrial, M. Butler, S. Hallerstede, T. S. Hoang, F. Mehta et al., Rodin: an open toolset for modelling and reasoning in Event-B. International journal on software tools for technology transfer, pp.447-466, 2010.
DOI : 10.1007/s10009-010-0145-y

J. R. Abrial, M. Butler, S. Hallerstede, and L. Voisin, An Open Extensible Tool Environment for Event-B, Formal Methods and Software Engineering, pp.588-605, 2006.
DOI : 10.1007/11901433_32

M. Butler, Incremental design of distributed systems with Event-B. Engineering Methods and Tools for Software Safety and Security, p.131, 2009.

M. Butler, Mastering System Analysis and Design through Abstraction and Refinement, 2012.

M. Butler and I. Maamria, Practical Theory Extension in Event-B, Theories of Programming and Formal Methods, pp.67-81, 2013.
DOI : 10.1007/978-3-540-87603-8_18

K. R. Leino, Dafny: An Automatic Program Verifier for Functional Correctness, Logic for Programming, Artificial Intelligence, and Reasoning, pp.348-370
DOI : 10.1007/978-3-642-17511-4_20
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.156.9592

D. Moura, L. Bjørner, and N. , Z3: An Efficient SMT Solver, Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

E. W. Dijkstra, A constructive approach to the problem of program correctness, BIT, vol.6, issue.3, pp.174-186, 1968.
DOI : 10.1007/BF01933419

E. M. Clarke and J. M. Wing, Formal methods: state of the art and future directions, ACM Computing Surveys, vol.28, issue.4, pp.626-643, 1996.
DOI : 10.1145/242223.242257
URL : https://hal.archives-ouvertes.fr/hal-00444076

C. A. Hoare, J. Misra, G. T. Leavens, and N. Shankar, The verified software initiative, ACM Computing Surveys, vol.41, issue.4, pp.1-8, 2009.
DOI : 10.1145/1592434.1592439

G. T. Leavens, J. R. Abrial, D. Batory, M. Butler, A. Coglio et al., Roadmap for enhanced languages and methods to aid verification, Proceedings of the 5th international conference on Generative programming and component engineering , GPCE '06, pp.221-236, 2006.
DOI : 10.1145/1173706.1173740
URL : http://archives.cs.iastate.edu/documents/disk0/00/00/04/38/00000438-00/roadmap.pdf

K. R. Leino and R. Monahan, Dafny Meets the Verification Benchmarks Challenge, Verified Software: Theories, Tools, Experiments, pp.112-126, 2010.
DOI : 10.1007/978-3-642-15057-9_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.178.8600

N. Catano, K. R. Leino, and V. Rivera, The EventB2Dafny Rodin plug-in, 2012 Second International Workshop on Developing Tools as Plug-Ins (TOPI), pp.49-54, 2012.
DOI : 10.1109/TOPI.2012.6229810

N. Catano, C. Rueda, and T. Wahls, A Machine-Checked Proof for a Translation of Event-B Machines to JML. arXiv preprint arXiv 1309, p.2339, 2013.

D. Mry and R. Monahan, Transforming Event B Models into Verified C# Implementations, VPT@ CAV, pp.57-73, 2013.

M. Barnett, K. R. Leino, and W. Schulte, The Spec# programming system: An overview. In Construction and analysis of safe, secure, and interoperable smart devices, pp.49-69, 2005.

G. T. Leavens, A. L. Baker, and C. Ruby, Preliminary design of JML, ACM SIGSOFT Software Engineering Notes, vol.31, issue.3, pp.31-32, 2006.
DOI : 10.1145/1127878.1127884

A. Edmunds and M. Butler, Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. Programming Language Approaches to Concurrency and Communication-cEntric Software, p.1, 2011.