1. Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. CUP (1996)

   Google Scholar 

2. Abrial, J.-R.: Event based sequential program development: Application to constructing a pointer program. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 51–74. Springer, Heidelberg (2003)

   Chapter  Google Scholar 

3. Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006)

   Chapter  Google Scholar 

4. Abrial, J.-R., Cansell, D.: Click’n’Prove: Interactive Proofs within Set Theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 1–24. Springer, Heidelberg (2003)

   Chapter  Google Scholar 

5. Abrial, J.-R., Cansell, D., Méry, D.: A mechanically proved and incremental development of IEEE 1394 tree identify protocol. FAC 14(3), 215–227 (2003)

   Article  Google Scholar 

6. Abrial, J.-R., Hallerstede, S.: Refinement, Decomposition and Instantiation of Discrete Models: Application to Event-B. Fundamentae Informatica (2006)

   Google Scholar 

7. Abrial, J.-R., Mussat, L.: On using conditional definitions in formal theories. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 242–269. Springer, Heidelberg (2002)

   Chapter  Google Scholar 

8. Abrial, J.-R.: Event driven system construction (1999)

   Google Scholar 

9. Astesiano, E., Bidoit, M., Krieg-Brückner, B., Kirchner, H., Mosses, P.D., Sannella, D., Tarlecki, A.: CASL - the common algebraic specification language. TCS 286, 153–196 (2002) Special issue on Abstract Data Types

   Article MATH  Google Scholar 

10. Back, R.-J.: Refinement Calculus II: Parallel and Reactive Programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol. 430, pp. 67–93. Springer, Heidelberg (1990)

    Google Scholar 

11. Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, Springer, Heidelberg (2006)

    Chapter  Google Scholar 

12. Behm, P., Burdy, L., Meynadier, J.-M.: Well defined B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 29–45. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

13. Butler, M.: csp2B: A practical approach to combining CSP and B. FAC 12(3), 182–198 (2000)

    Article MATH  Google Scholar 

14. Dijkstra, E.W.: The notational conventions I adopted, and why. Technical Report EWD1300, University of Texas (2000)

    Google Scholar 

15. Hallerstede, S.: Parallel hardware design in B. In: Bert, D., P. Bowen, J., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 101–102. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

16. Morgan, C.: Programming from Specifications, 2nd edn. PHI (1994)

    Google Scholar 

17. Morgan, C., Hoang, T., Abrial, J.: The Challenge of Probabilistic Event B. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 162–171. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

18. Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: Predicate subtyping in PVS. IEEE Trans. Soft. Eng. 24(9), 709–720 (1998)

    Article  Google Scholar 

19. Schneider, S., Treharne, H.: CSP theorems for communicating B machines. FAC 17(4), 390–422 (2005)

    Article MATH  Google Scholar 

20. Spivey, J.M.: The Z Notation: A Reference Manual. PHI, 2nd edn. (1992)

    Google Scholar 

21. Taft, S.T., Duff, R.A. (eds.): Ada 95 Reference Manual. Springer, Heidelberg (1997)

    Google Scholar 

22. Woodcock, J., Davies, J.: Using Z. Specification, Refinement, and Proof. PH (1996)

    Google Scholar 

Download references