Posts

Why might we teach "Formal Methods" informally? And to whom? And when? Carroll Morgan

 BCS-FACS Online SeminarDate and time Thursday 25 June, 11:00 am - 1:00 pm Location Online Free registration < https://www.bcs.org/events-calendar/2026/june/hybrid-why-might-we-teach-formal-methods-informally-and-to-whom-and-when/ > Note that this event is online only. Timetable 11:00 am - Talk 12:00 pm - Questions and answers 1:00 pm - Event closes Seminar Details Title: Why might we teach "Formal Methods" informally? And to whom? And when? Speaker: Carroll Morgan Abstract: Formal Methods (for computing) was enabled by Hoare's “An axiomatic basis for computer programming” in 1969, where Formal meant “in the sense of formal logic”, i.e. reasoning based on manipulation of symbols which themselves had no intrinsic meaning (in the sense of Hilbert). Hoare's paper had itself been enabled by Floyd's “Assigning meanings to programs” just two years earlier, whose informal message might well have been -- in retrospect at least -- “Don...
Post a Comment
Read more

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