J. Abrial, Extending B without changing it (for developing distributed systems), st Conference on the B method, pp.169-190, 1996.

J. Abrial, Event driven distributed program construction. Internal note, Consultant, 2001.

J. Abrial, Event driven distributed program construction, Consultant, 2001.

J. Abrial, Event driven electronic circuit construction. Internal note, Consultant, 2001.

J. Abrial, Event driven sequential program construction. Internal note, Consultant, 2001.

J. Abrial, Formal construction of proved circuits, Consultant, 2001.

J. Abrial, Discrete system models. Internal note, Consultant, 2002.

J. Abrial, B#: Toward a Synthesis between Z and B, 3nd International Conference of B and Z Users -ZB 2003, 2003.
DOI : 10.1007/3-540-44880-2_12

J. Abrial, D. Cansell, and G. Laffitte, ???Higher-Order??? Mathematics in B, Lecture Notes in Computer Science, vol.2272, pp.370-393, 2002.
DOI : 10.1007/3-540-45648-1_19

J. Abrial, D. Cansell, and D. Méry, A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol, Formal Aspects of Computing, vol.14, issue.3, 2001.
DOI : 10.1007/s001650300002
URL : https://hal.archives-ouvertes.fr/inria-00099531

J. Abrial, D. Cansell, and D. Méry, Formal Derivation of Spanning Trees Algorithms, 3nd International Conference of B and Z Users -ZB 2003, 2003.
DOI : 10.1007/3-540-44880-2_27
URL : https://hal.archives-ouvertes.fr/inria-00099793

J. Abrial, D. Cansell, and D. Méry, A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol, Formal Aspects of Computing, vol.14, issue.3, 2003.
DOI : 10.1007/s001650300002
URL : https://hal.archives-ouvertes.fr/inria-00099531

J. Abrial and L. Mussat, Introducing dynamic constraints in B98 :Recent Advances in the Development and Use of the B Method, volume 1393 of Lecture Notes in Computer Science, 1998.

J. B. Abrial, B#: Toward a Synthesis between Z and B, Lecture Notes in Computer Science, vol.2651, pp.168-177, 2003.
DOI : 10.1007/3-540-44880-2_12

J. Abrial, Event Based Sequential Program Development: Application to Constructing a Pointer Program, Lecture Notes in Computer Science, vol.2805, pp.51-74, 2003.
DOI : 10.1007/978-3-540-45236-2_5

J. Abrial, Formal methods in industry, Proceeding of the 28th international conference on Software engineering , ICSE '06, pp.761-768, 2006.
DOI : 10.1145/1134285.1134406

J. Abrial and D. Cansell, Click???n Prove: Interactive Proofs within Set Theory, 16th Intl. Conf. Theorem Proving in Higher Order Logics (TPHOLs'2003), pp.1-24, 2003.
DOI : 10.1007/10930755_1
URL : https://hal.archives-ouvertes.fr/inria-00099836

J. Abrial and D. Cansell, Formal construction of a non-blocking concurrent queue algorithm (a case study in atomicity), J. UCS, vol.11, issue.5, pp.744-770, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00000120

J. Abrial, D. Cansell, and D. Méry, A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol, Formal Aspects of Computing, vol.14, issue.3, pp.215-227, 2003.
DOI : 10.1007/s001650300002
URL : https://hal.archives-ouvertes.fr/inria-00099531

J. Abrial, D. Cansell, and D. Méry, Refinement and reachability in event b, Treharne et al. [97], pp.222-241
DOI : 10.1007/11415787_14
URL : https://hal.archives-ouvertes.fr/inria-00001245

R. Back, A calculus of refinements for program derivations, Acta Informatica, vol.14, issue.3, pp.593-624, 1998.
DOI : 10.1007/BF00291051

R. Back and J. Wright, Refinement Calculus, 1998.
DOI : 10.1007/978-1-4612-1674-2

R. J. Back, On correct refinement of programs, Journal of Computer and System Sciences, vol.23, issue.1, pp.49-68, 1979.
DOI : 10.1016/0022-0000(81)90005-2

J. P. Banâtre, A. Coutant, and D. L. Métayer, The gamma model and its discipline of programming, Science of Computer Programming, vol.15, issue.1, pp.55-77, 1990.
DOI : 10.1016/0167-6423(90)90044-E

P. Behm, P. Benoit, A. Faivre, and J. Meynadier, M??t??or: A Successful Application of B in a Large Project, Proceedings of FM'99: World Congress on Formal Methods, pp.369-387, 1999.
DOI : 10.1007/3-540-48119-2_22

F. Bellegarde, C. Darlot, J. Julliand, and O. Kouchnarenko, Reformulate Dynamic Properties during B Refinement and Forget Variants and Loop Invariants, ZB 2000: Formal Specification and Development in Z and B -First International Conference of B and Z Users, 2000.
DOI : 10.1007/3-540-44525-0_14

J. Bicarregui, D. Clutterbuck, G. Finnie, H. Haughton, K. Lano et al., Formal methods into practise: Case studies in the application of the B method, 1995.

J. P. Bowen, S. Dunne, A. Galloway, and S. King, Formal Specification and Development in Z and B -First International Conference of B and Z Users, 2000.

L. Burdy, Traitrement des expressions dépourvues de sens de la théorie des ensembles Application à la méthode B Stepwise refinement of communicating systems, Science of Computer Programming, vol.27, pp.139-173, 1996.

M. Butler, csp2b: A practical approach to combining csp and b. Formal Aspects of Computing, pp.182-196

M. Butler and C. Snook, Verifying dynamic properties of UML models by translation to the B language and toolkit, UML 2000 WORKSHOP Dynamic Behaviour in UML Models: Semantic Questions, 2000.

M. Butler and M. Walden, Parallel Programming with the B Method In Program Development by Refinement Cases Studies Using the B Method, volume [93] of FACIT, pp.183-195, 1998.

E. Börger and R. Stärk, The Abstract State Machines Method for High-Level System Design and Analysis, 2003.
DOI : 10.1007/978-1-84882-736-3_3

M. Büchi and R. Back, Compositional Symmetric Sharing in B, FM'99 Formal Methods, 1999.
DOI : 10.1007/3-540-48119-2_25

D. Cansell, G. Gopalakrishnan, M. Jones, D. Méry, and A. Weinzoepflen, Incremental proof of the producer/consumer property for the PCI protocol Formal Specification and Development in Z and B -ZB', Lecture Notes in Computer Science, vol.2272, 2002.

D. Cansell and D. Méry, Abstraction and refinement of features, Language Constructs for Designing Features, 2000.
DOI : 10.1007/978-1-4471-0287-8_5
URL : https://hal.archives-ouvertes.fr/inria-00099264

D. Cansell and D. Méry, Développement de fonctions définies récursivement en B : Application du B événementiel, 2002.

D. Cansell and D. Méry, Développement de fonctions définies récursivement en B : Application du B événementiel, 2002.

D. Cansell and D. Méry, Formal and incremental construction of distributed algorithms: On the distributed reference counting algorithm, Theoretical Computer Science, vol.364, issue.3, 2006.
DOI : 10.1016/j.tcs.2006.08.015
URL : https://hal.archives-ouvertes.fr/inria-00093164

D. Cansell and D. Méry, Software Specification Methods An Overview Using a Case Study, chapter Event B. Hermès, 2006.

D. Cansell, G. Gopalakrishnan, M. D. Jones, D. Méry, and A. Weinzoepflen, Incremental Proof of the Producer/Consumer Property for the PCI Protocol, Lecture Notes in Computer Science, vol.2272, pp.22-41, 2002.
DOI : 10.1007/3-540-45648-1_2
URL : https://hal.archives-ouvertes.fr/inria-00100888

D. Cansell and D. Méry, Foundations of the b method, Computers and Informatics, vol.22, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099794

D. Cansell and D. Méry, Incremental Parametric Development of Greedy Algorithms, AVOCS'O6 Sixth International Workshop on Automated Verification of Critical Systems, pp.18-19, 2006.
DOI : 10.1016/j.entcs.2007.05.028
URL : https://hal.archives-ouvertes.fr/inria-00594883

N. Cariero and D. Gelernter, How to write parallel programs: a first course, 1990.

J. Chalopin and Y. Métivier, A Bridge Between the Asynchronous Message Passing Model and Local Computations in Graphs, MFCS, pp.212-223, 2005.
DOI : 10.1007/11549345_19
URL : https://hal.archives-ouvertes.fr/hal-00308135

K. M. Chandy and J. Misra, Parallel Program Design A Foundation, 1988.

M. Chaudron, Notions of Refinement for a Coordination Language for GAMMA, 1997.

E. M. Clarke, O. Grumberg, and D. A. , Peled. Model Checking, 2000.

A. Clearsy, Atelier B Version 3.6. [56] ClearSy. Web site b4free set of tools for development of b models, 2002.

H. Thomas, C. E. Cormen, R. L. Leiserson, C. Rivest, and . Stein, Introduction to Algorithms, 2001.

M. Devillers, D. Griffioen, J. Romin, and F. Vaandrager, Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394, Methods in System Design, pp.307-320, 2000.

E. W. Dijkstra, A Discipline of Programming, 1976.

E. W. Dijkstra and C. S. Scholten, Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science, 1990.

H. Ehrig and B. Mahr, Fundamentals of Algebraic Specification 1, Equations and Initial Semantics, EATCS Monographs on Theoretical Computer Science, 1985.

M. Frappier and H. Habrias, Software Specification Methods An Overview Using a Case Study, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00458174

Y. Gurevitch, Specification and Validation Methods, chapterEvolving Algebras 1993: Lipari Guide, pp.9-36, 1995.

H. Habrias, IRIN-IUT de Nantes, First Conference on the B Method, 1996.

H. Habrias, Spécification formelle avec B. Hermès, 2001.

J. Hoare, The use of B in CICS, Applications of Formal Methods, 1995.

C. B. Jones, Sytematic Software Development Using VDM, 1986.

L. Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.872-923, 1994.
DOI : 10.1145/177492.177726

L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, 2002.

K. Lano, The B Language and Method -A Guide to rPactical Formal Development. FACIT, 1996.

H. Ledang and J. Souquières, Formalizing UML behavioral diagrams with B, Tenth OOPSLA Workshop on Behavioral Semantics : Back to Basics, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00107872

H. Ledang and J. Souquières, Modeling class operations in B: Application to UML behavioral diagrams, Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001), 2001.
DOI : 10.1109/ASE.2001.989815
URL : https://hal.archives-ouvertes.fr/inria-00107871

H. Ledang and J. Souquières, Contributions for Modelling UML State-Charts in B, Third International Conference on Integrated Formal Methods -IFM'2002, 2002.
DOI : 10.1007/3-540-47884-1_7
URL : https://hal.archives-ouvertes.fr/inria-00099403

Z. Manna, Mathematical Theory of Computation, 1974.

A. Mciver, C. Morgan, and T. S. Hoang, Probabilistic Termination in B, ZB 2003: Formal Specification and Development in Z and B -Third International Conference of B and Z Users, 2003.
DOI : 10.1007/3-540-44880-2_15

D. Méry, Requirements for a Temporal B Assigning Temporal Meaning to Abstract Machines??? and to Abstract Systems, IFM'99 Integrated Formal Methods, 1999.
DOI : 10.1007/978-1-4471-0851-1_21

L. Mikhailov and M. Butler, An Approach to Combining B and Alloy, ZB 2002: Formal Specification and Development in Z and B - 2nd International Conference of B and Z Users, 2002.
DOI : 10.1007/3-540-45648-1_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.124.1490

L. Moreau, Distributed directory service and message routing for mobile agents, Science of Computer Programming, vol.39, issue.2-3, pp.249-272, 2001.
DOI : 10.1016/S0167-6423(00)00011-3
URL : http://doi.org/10.1016/s0167-6423(00)00011-3

C. Morgan, Programming from Specifications. Prentice Hall International Series in Computer Science, 1990.

C. Morgan, T. S. Hoang, and J. Abrial, The challenge of probabilistic vent b extended abstract, Treharne et al. [97], pp.162-171

S. Owicki and D. Gries, An axiomatic proof technique for parallel programs I, Acta Informatica, vol.11, issue.4, pp.319-340, 1976.
DOI : 10.1007/BF00268134

A. Papatsaras and B. Stoddart, Global and Communicating State Machine Models in Event Driven B: A Simple Railway Case Study, ZB 2002: Formal Specification and Development in Z and B -2nd International Conference of B and Z Users, 2002.
DOI : 10.1007/3-540-45648-1_24

M. Potet and Y. Rouzeau, Composition and refinement in the B-method, B'98: Recent Advances in the Development and Use of the B Method, 1998.
DOI : 10.1007/BFb0053355

R. C. Prim, Shortest connection and some generalizations [89] project RODIN. Rigorous open development environment for complex systems, Bell Syst. Tech. J, vol.36, 1957.
DOI : 10.1002/j.1538-7305.1957.tb01515.x

H. and J. Rogers, Theory of Recursive Functions and Effective Computability, 1967.

S. Schneider and H. Treharne, Communicating B Machines, ZB 2002: Formal Specification and Development in Z and B -2nd International Conference of B and Z Users, pp.416-435, 2002.
DOI : 10.1007/3-540-45648-1_22
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.5500

E. Sekerinski and K. Sere, Program Development by Refinement -Cases Studies Using the B Method. FACIT, 1998.

J. M. Spivey, The Z notation, A Reference Manual, 1989.

R. Stärk, J. Schmid, and E. Börger, Java and the Java Virtual Machine, 1998.
DOI : 10.1007/978-3-642-59495-3

H. Treharne and S. Schneider, How to Drive a B Machine, ZB 2000: Formal Specification and Development in Z and B -First International Conference of B and Z Users, 2000.
DOI : 10.1007/3-540-44525-0_12