Posts

Jean-Raymond Abrial: A Scientific Biography of a Formal Methods Pioneer

Jonathan Bowen, Henri Habrias Abstract: Jean-Raymond Abrial is one of the central figures in the development of formal methods for software and systems engineering. Over a career spanning more than five decades, he has played a decisive role in the creation of the Z specification notation, the B-Method, and Event-B and in demonstrating their applicability to large-scale industrial systems. This article presents a scholarly biographical account of Abrial’s life and work, tracing the evolution of his ideas from early work on real-time languages and databases, through foundational contributions to formal specification, refinement, and proof, to the development of industrial-strength tool support such as the Atelier B and the Rodin platform. The article situates Abrial’s contributions within their historical, intellectual, and industrial contexts and assesses their lasting impact on software engineering and formal reasoning about programs.   Published in: IEEE Annals of ...
Post a Comment
Read more

Jean-Raymond Abrial in Grenoble, Christian Jullien testimony

  Extract from FACS FACTS Issue 2025-2 July 2025 In memory of Jean-Raymond Abrial (1938–2025) August 31, 2025 https://www.bcs.org/media/yd4ocehl/facs-jul25.pdf   FACS FACTS Issue 2025-2 July 2025 In memory of Jean-Raymond Abrial (1938–2025)      I didn't work directly with Professor Abrial, but I owe him much ! A brilliant and dedicated teacher Firstly, he was my teacher (two years) during computer science master at IMAG Grenoble  (1971/72). In 1971 he gave us a strong basis in data management. The classes were   fascinating; the lecture hall was truly captivated, the examples being "telling"   despite being based on a rigorous theoretical foundation. I still have  hand-written lecture support  for additionnal courses that he gave for   free at university in the evening, after normal hours.  This document (215 pages) was produced with an alcohol duplicator. He used  a lot of  figures,  graphs and e...
Post a Comment
Read more

Inductive Set Construction using Instantiation and Rodin, D. Cansell

  https://wiki.event-b.org/images/202606.pdf All proof obigations of my Rodin workshop  paper  are in Rodin2026 in this  archive You need the context instantiation plugin (pleased asked to Yamine Ait Ameur). Only automatic proofs are green. Have fun! There are no comment then no english then no bad english. For my talk I've presented in this following order DemoListwfix (I've instantated fixpoint). It's Listwithfix. List EquivList: if I've 2 elements in List or on different Lists they are equivalent. SeqIsList (where I've used sequence defined by Jean-Raymond). FrLB to define recursive function on lists ms FrLSB similar then FrLB but with another parameter Lordwithfix insert sort proof_insert proof_sort I left my cave in 2020 for Jean-Raymond. It's time I went back. My Rodin presentation will be the last one. Jean-Raymond today it's the first year without you (May 26 2026). I feel an immense emptiness since you left. I loose my favorite problems dealer....
Post a Comment
Read more

Higman’s lemma using instantiation, Dominique Cansell

  http://dominique.cansell.free.fr/JRAFest_HigmanV2.pdf   http://dominique.cansell.free.fr/RejectedPaperAbrial'sFestschrift.html   https://en.wikipedia.org/wiki/Higman%27s_lemma  
Post a Comment
Read more

Rodin Workshop 2026 13th Rodin User and Developer Workshop,May 18th, 2026, Tokyo

  Rodin Workshop 2026 13th Rodin User and Developer Workshop The 13th Rodin User and Developer Workshop, May 18th, 2026, Tokyo, Japan * Hybrid event * Event-B is a formal method for system-level modelling and analysis. The Rodin Platform is an Eclipse-based toolset for Event-B that provides effective support for modelling and automated proof. The platform is open-source and is further extendable with plug-ins. A range of plug-ins have already been developed. The 13th Rodin workshop will be collocated with the FM 2026 Conference , . The purpose of this workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers. For Rodin users the workshop will provide an opportunity to share tool experiences and to gain an understanding of on-going tool developments. For plug-in developers the workshop will provide an opportunity to showcase their tool...
Post a Comment
Read more

FACS FACTS Issue 2026-1 January 2026 Chronological bibliography of Jean-Raymond Abrial

 FACS FACTS Issue 2026-1 January 2026 Chronological bibliography of Jean-Raymond Abrial Henri Habrias * December 2025 https://www.bcs.org/media/veppnllv/facs-jan26.pdf “The very first paper on Z was published in 1980 (at the time, the name Z was not ‘invented’), then the book on the B method was published in 1996, and, finally, the book on Event-B was published in 2010. So, 30 years separate Z from Event-B. It is thus clear that I spent a significant time of my scientific professional life working with the same kind of subject in mind, roughly speaking specification languages. I do not know whether this kind of addiction is good or bad, but what I know is that I enjoyed it a lot.” — J.-R. Abrial in From Z to B and then Event-B: Assigning Proofs to Meaningful Programs, J.-R. Abrial In: E.B. Johnsen, L. Petre (eds), Integrated Formal Methods (IFM 2013). LNCS, vol. 7940, pp. 1–15. Springer. ISBN: 978-3-642-38612-1. doi:10.1007/978-3-642-38613-8-1   * Aided by Dominique Cansell; e...
Post a Comment
Read more

Memories of Jean-Raymond Abrial in Oxford, the Alps, and Paris, Bernard Sufrin

 Memories of Jean-Raymond Abrial in Oxford, the Alps, and Paris Bernard Sufrin Emeritus Fellow: Worcester College & Departement of Computer Science: Oxford University FACS FACTS Issue 2026-1 January 2006 https://www.bcs.org/media/veppnllv/facs-jan26.pdf   The end : "Au revoir I wrote earlier of Jean-Raymond’s frighteningly fast work rate. And for the first few months of 1981 he worked even more quickly – generating large numbers of drafts of new foundations for the language and its basic library, as well as building the prototype of an extensible proof checker, and writing essays inspired by Cliff Jones’s book[6]. This work would (eventually) become the basis for B and the B tool. The rest of the “Z group” found it impossible to keep up with him, and wanted the notation to stay stable for a while. We had materials to prepare for courses and further collaborations with industrial partners to pursue,10 and a large (5 year) Software Engineering project to prepare for. Then on...
Post a Comment
Read more