rodin-b-sharp-user Mailing List for RODIN

13th Rodin User and Developer Workshop

The 13th Rodin User and Developer Workshop, May 18th-19th, 2026, Tokyo, Japan

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<https://conf.researchr.org/home/fm-2026>,.

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 tools and to achieve better coordination of tool development effort.

Submission

If you are interested in giving a presentation at the Rodin workshop or have a plug-in to demonstrate, send

a short abstract (1 or 2 pages PDF) to ro...@ec...<mailto:ro...@ec...> by 15th March 2026.

Notification will be send out early April.

We will endeavour to accommodate all submissions that are clearly relevant to Rodin and Event-B.

The proceedings of the workshop will be available as a technical report at the University of Southampton.

Exclusive Opportunity: Special Issue Publication

This year, we are excited to announce that a special issue is in the planning stages, and the selected high-quality submissions will be invited to contribute to a Special Issue.

(Note: The finalisation of the special issue is currently underway.)


Organisers

Asieh Salehi Fathabadi<https://www.southampton.ac.uk/people/5xb2d2/doctor-asieh-salehi-fathabadi>, Lecturer, University of Southampton

Laurent Voisin, R&D Manager, Systerel<https://www.systerel.fr/en/>

Neeraj Kumar Singh<https://sites.google.com/site/singhnne/>, Associate Professor, INPT-ENSEEIHT / IRIT, University of Toulouse

Michael Leuschel<https://www.cs.hhu.de/lehrstuehle-und-arbeitsgruppen/softwaretechnik-und-programmiersprachen/unser-team/team/leuschel>, Professor, Heinrich-Heine-Universität, Germany

Son Hoang<https://www.southampton.ac.uk/people/5xfl2w/doctor-son-hoang>, Associate Professor, University of Southampton

Dear Rodin users, 

We are pleased to announce the plugin chronoEventB that allows augmenting EventB models with timing properties. 

A description of the plugin and installation instructions are available at [ https://github.com/AmelMammar/chronoEventB | https://github.com/AmelMammar/chronoEventB ] . 

Please feel free to contact us if you have any questions (installation, bugs, etc.). 

Best regards, 
Amel Mammar & Cabrel Feukeng Momo 

[ https://www.telecom-sudparis.eu/ ] 	
Amel MAMMAR 
Professeure 
01 60 76 44 21 
9 rue Charles Fourier 
91011 Évry-Courcouronnes Cedex 
[ https://www.telecom-sudparis.eu/ ] [ https://twitter.com/TelecomSudParis ] [ https://www.facebook.com/TelecomSudParis ] [ https://www.linkedin.com/edu/school?id=42882&trk=tyah&trkInfo=clickedVertical%3Aschool%2Cidx%3A4-1-7%2CtarId%3A1429711678204%2Ctas%3Atelecom%20sud ] [ https://blogrecherche.wp.imt.fr/ ] 
Une école de [ https://www.imt.fr/ | l'IMT ] 

Hi,

I’m not aware of any stable, up to date plug-in for Rodin to model probabilistic systems.

As far as I know, the most recent and developed work on this subject was by M. A. Aouadhi, B. Delahaye and A. Lanoix.
See for instance https://hal.science/hal-01255753/document, which includes a screenshot of their tool.
However, I do not know if there is a recent release of their plug-in available or if they are still working on it.

Best,
Guillaume

> On 6 Oct 2025, at 15:17, Guzmán Llambías - INCO <gl...@fi...> wrote:
> 
> Hi guys!
> 
> Is there any stable extension to model probabilistic systems with event-b? I have been searching and found some papers but wanted to know if there is something official with Rodin
> 
> Thanks in advance
> Best!
> Guzmán

Hi guys!

Is there any stable extension to model probabilistic systems with event-b?
I have been searching and found some papers but wanted to know if there is
something official with Rodin

Thanks in advance
Best!
Guzmán

Dear All,

I am glad to announce that the first release candidate of Rodin 3.10 is available. You can install it from SourceForge (https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.10-RC1/)  This release is based on the latest Eclipse 2024-12 (4.34) and contains numerous bug fixes.
Rodin will work on macOS (both x86_64 and aarch 64 architectures), Linux and Windows 64-bit computers. You need to have a 64-bit Java JRE (version 17 or later) installed on your computer to run Rodin.

We are interested in getting as much feedback as possible, especially about bugs or usage issues, before publishing the final release. Please do not hesitate to report anything that looks strange to you.

Caution: This is a release candidate. This means that it has not been extensively tested and may contain many bugs, some being nasty. Please do not use it for anything important.

macOS caveats
----
The Rodin application is not notarized. This means that when you download it from SourceForge, macOS will quarantine the application and tell you that it is broken. Just run the command "xattr -rc Rodin.app" in a Terminal to remove the quarantine tag.

Note: If you open an existing workspace (set of projects) with this release, this workspace will not work anymore with prior releases of Rodin. We encourage you to duplicate your workspace to avoid any issue.

Best Regards,
--
Idir AIT SADOUNE
Associate Professor 

LMF - Formal Methods Laboratory
CentraleSupelec - Computer Science Department  
Paris-Saclay University
www.idiraitsadoune.com <https://idiraitsadoune.com/>
+33/0 1 75 31 78 46 

Dear Leon,

I had the same error when running Rodin on my Apple Silicon Macbook for 
the first time.
I guess it is due to the mismatch of architectures; Rodin is available 
for x86_64 only, while the OS tries to use Java for the Apple Silicon chip.
I solved it as follows:
(1) installing x86_64 Java runtime
(2) running Rodin with
  $ rodin -vm /path/to/x86_64/java

I hope this helps.


Cheers,
Tsutomu

On 2025/03/24 18:49, Leon Schlößer wrote:
> Hello,
> 
> I am currently having issues while trying to install Rodin on my new 
> Macbook.
> I always get the same error similar to "Library/Java/ 
> JavaVirtualMachines/temurin-17.jdk/Contents/Home/bin/.../lib/server/ 
> libjvm.dylib" does not contain the JNI_CreateJavaVM symbol". I already 
> tried multiple Java and Rodin versions and I also tried to edit the 
> Info.plist file but nothing seems to work.
> 
> Has anyone encountered a similar problem and might be able to help me 
> with the installation?
> 
> Best regards
> Leon
> 
> 
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user

-- 
Tsutomu Kobayashi, Ph.D.
Japan Aerospace Exploration Agency (JAXA)
https://researchmap.jp/tsutomu.kobayashi?lang=en

Hello,

I am currently having issues while trying to install Rodin on my new 
Macbook.
I always get the same error similar to 
"Library/Java/JavaVirtualMachines/temurin-17.jdk/Contents/Home/bin/.../lib/server/libjvm.dylib" 
does not contain the JNI_CreateJavaVM symbol". I already tried multiple 
Java and Rodin versions and I also tried to edit the Info.plist file but 
nothing seems to work.

Has anyone encountered a similar problem and might be able to help me 
with the installation?

Best regards
Leon

Call for Submissions – 12th Rodin User and Developer Workshop

🔹 10th June 2025 | Düsseldorf, Germany
Collocated with the ABZ 2025 Conference<https://abz-conf.org/site/2025/>
We are pleased to invite submissions for the 12th Rodin User and Developer Workshop<https://wiki.event-b.org/index.php/Rodin_Workshop_2025>. This event aims to bring together researchers, developers, and practitioners working with Event-B and the Rodin Platform, fostering a collaborative and vibrant community.


🔹 About the Workshop
Event-B is a formal method for system-level modelling and analysis, supported by the Rodin Platform, an open-source Eclipse-based toolset that provides modelling and automated proof capabilities. A range of plug-ins have been developed to enhance its functionalities.
The Rodin workshop is an excellent opportunity for:

  *   Rodin users to share tool experiences and learn about ongoing tool developments.
  *   Plug-in developers to showcase their tools and coordinate development efforts.


🔹 Submission Guidelines
We invite submissions from both Rodin users and developers who wish to present their work or demonstrate a plug-in. Please submit a short abstract (1–2 pages, PDF) to ro...@ec...<mailto:ro...@ec...> by 10th May 2025.
We will strive to accommodate all submissions that are clearly relevant to Rodin and Event-B. The workshop proceedings will be published as a technical report at the University of Southampton.


🔹 Exclusive Opportunity: Special Issue Publication
This year, we are excited to announce that selected high-quality submissions will be invited to contribute to a Special Issue entitled:
"Formal Methods in Computer Science: Theory and Applications"
https://www.mdpi.com/journal/mathematics/special_issues/8AXPI3T0RZ

This issue will be published in the renowned Mathematics journal (ISSN 2227-7390, IF 2.3, JCR Q1). Authors of accepted submissions will have the exclusive opportunity to submit a manuscript with a special discount (up to 100%) on publication fees, subject to peer review.
Don’t miss this chance to showcase your research on an international platform!


🔹 Organisers
📌 Asieh Salehi Fathabadi – Senior Research Fellow, University of Southampton
📌 Laurent Voisin – R&D Manager, Systerel
📌 Son Hoang – Associate Professor, University of Southampton


We look forward to your participation and contributions!
For inquiries, please contact: ro...@ec...<mailto:ro...@ec...>

Hi Guillaume,

thanks very much for the feedback.
That explains the behaviour; I had probably written the model before installing the Theory Plugin and then got the errors when re-opening the model after installation.
It would be great if the behaviour could also be fixed for symbols like +r or -r.

Greetings,
Michael

> On 27 Feb 2025, at 14:54, Guillaume Verdier <Gui...@ir...> wrote:
> 
> If the problem appeared around Rodin 3.6, I believe that it’s just because it was the oldest version you tried with the Theory plug-in installed.
> 

Dear Michael,

These conversions are not part of Rodin itself.
They are added by the Theory plug-in (https://sourceforge.net/p/rodin-b-sharp/theory/ci/master/tree/org.eventb.theory.keyboard/plugin.xml#l50).
If the problem appeared around Rodin 3.6, I believe that it’s just because it was the oldest version you tried with the Theory plug-in installed.

These kind of problems have been known since at least Rodin 2.7 in 2013, as documented by ticket #701 (https://sourceforge.net/p/rodin-b-sharp/bugs/701/).
This ticket was fixed in Rodin 3.8, but we only modified the behavior for text symbols, not math ones, such as +r or -r.

I’ll discuss with Laurent how we should handle this.

Cheers,
Guillaume

> On 27 Feb 2025, at 13:32, Michael Leuschel <Mic...@un...> wrote:
> 
> Hi,
> 
> I just noticed after re-opening a Rodin project the some of my guards, invariants and axioms now contained syntax errors.
> The reason is that I had a variable named rollback and it was used in formulas like
>  x+rollback.
> The reason is that +r and -r are automatically converted to a Unicode circled-plus, circled-minus operator
> 
> For example, if you type the following text in the Rodin editor or in Camille:
>  1+right
> it gets automatically transformed into:
>  1⊕ight
> which of course causes syntax errors.
> 
> Our students also had issues with that in their project (modelling a Mars rover where some of the variables started with rover and hence any formula with +rover… or -rover led to errors).
> 
> It seems that Rodin does this conversion since 3.6. I could, however, not find a mention of it in the release notes (https://wiki.event-b.org/index.php/Rodin_Platform_3.6_Release_Notes).
> 
> 
> The fix is to surround the + with whitespace to avoid the automatic conversion.
> But I wonder whether we should disable / change this automatic conversion in Rodin.
> Maybe we should only provide a Latex style conversion (\rplus, \rminus) or a shortcut that cannot appear in a valid Rodin formula (++r  or  [+]  or  (+)  or …).
> 
> Greetings,
> Michael
> 
> 
> 
> 
> 
> 
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user

Hi Tsutomu,

it worked! thanks a lot

all the best
Guzmán

El jue, 27 feb 2025 a las 9:07, Tsutomu Kobayashi (<
kob...@ja...>) escribió:

> Hi Guzmán,
>
> Please try modifying the value of "Size of unspecified deferred sets in
> SETS section" setting in Preferences -> ProB to a larger number.
>
>
> Cheers,
> Tsutomu
>
> On 2025/02/24 23:27, Guzmán Llambías - INCO wrote:
> > Hi guys,
> >
> > I'm using Event-B and Rodin Platform to model a system and have an event
> > that receives one parameter. I'm using the animation model to animate
> > the specification and found a limitation in the number of parameters
> > available for an event. Is there a way to add more parameters? For
> > example, the following lock operation receives one parameter and when I
> > try to animate it I have only two options. Is there a way to have more
> > (e.g. SOURCE_TOKEN3, SOURCE_TOKEN4, SOURCE_TOKEN5)?
> >
> > Thanks in advance
> > Guzmán
> >
> > image.png
> >
> >
> > _______________________________________________
> > Rodin-b-sharp-user mailing list
> > Rod...@li...
> > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user
>
> --
> Tsutomu Kobayashi, Ph.D.
> Japan Aerospace Exploration Agency (JAXA)
> https://researchmap.jp/tsutomu.kobayashi?lang=en
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user
>

Hi,

I just noticed after re-opening a Rodin project the some of my guards, invariants and axioms now contained syntax errors.
The reason is that I had a variable named rollback and it was used in formulas like
  x+rollback.
The reason is that +r and -r are automatically converted to a Unicode circled-plus, circled-minus operator

For example, if you type the following text in the Rodin editor or in Camille:
  1+right
it gets automatically transformed into:
  1⊕ight
which of course causes syntax errors.

Our students also had issues with that in their project (modelling a Mars rover where some of the variables started with rover and hence any formula with +rover… or -rover led to errors).

It seems that Rodin does this conversion since 3.6. I could, however, not find a mention of it in the release notes (https://wiki.event-b.org/index.php/Rodin_Platform_3.6_Release_Notes).


The fix is to surround the + with whitespace to avoid the automatic conversion.
But I wonder whether we should disable / change this automatic conversion in Rodin.
Maybe we should only provide a Latex style conversion (\rplus, \rminus) or a shortcut that cannot appear in a valid Rodin formula (++r  or  [+]  or  (+)  or …).

Greetings,
Michael

Hi Guzmán,

Please try modifying the value of "Size of unspecified deferred sets in 
SETS section" setting in Preferences -> ProB to a larger number.


Cheers,
Tsutomu

On 2025/02/24 23:27, Guzmán Llambías - INCO wrote:
> Hi guys,
> 
> I'm using Event-B and Rodin Platform to model a system and have an event 
> that receives one parameter. I'm using the animation model to animate 
> the specification and found a limitation in the number of parameters 
> available for an event. Is there a way to add more parameters? For 
> example, the following lock operation receives one parameter and when I 
> try to animate it I have only two options. Is there a way to have more 
> (e.g. SOURCE_TOKEN3, SOURCE_TOKEN4, SOURCE_TOKEN5)?
> 
> Thanks in advance
> Guzmán
> 
> image.png
> 
> 
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user

-- 
Tsutomu Kobayashi, Ph.D.
Japan Aerospace Exploration Agency (JAXA)
https://researchmap.jp/tsutomu.kobayashi?lang=en

Dear Rodin users,

I am pleased to announce the release of a new version of two plug-ins:
— version 1.4.0 of the Renaming Refactory plug-in
— version 1.1.0 of the Generic Instantiation (Soton) plug-in

These releases fix compatibility issues with recent Rodin releases and are compatible with Rodin 3.8 and 3.9.

They are available in the Rodin Plug-ins update site.

The work on these releases has been supported by the French ANR project Event-B Rodin Plus (EBRP, ANR-19-CE25-0010).

Best regards,
Guillaume Verdier

Dear Michael,

I fully agree with your analysis. Thank you for pointing this out.

I have created ticket https://sourceforge.net/p/rodin-b-sharp/feature-requests/408/ for this purpose.

We will implement the check in the parser of the AST plug-in of Rodin for the coming 3.10 release hopefully.

Cheers,
Laurent.

> Le 25 févr. 2025 à 12:58, Michael Leuschel <Mic...@un...> a écrit :
> 
> Dear Rodin User,
> 
> this weekend I stumbled upon a somewhat surprising aspect of the Rodin formula language.
> Take the following Event-B context in Camille syntax:
> 
> context TestExistImplication
> constants x y
> axioms
> @axm1 x=1
> @axm2 y=2
> theorem @thm3 ∃z·(z∈1‥3 ∧ x=z) ⇒ y=44  
> end
> 
> Before continuing to read, you may reflect and answer the question whether @thm3 is true or not.
> 
> --------------------------------
> 
> In classical B syntax, within Atelier-B, the answer is that @thm3 is false:
>  ∃z·(z∈1‥3 ∧ x=z) is true
>  y=44 is false
> and the implication is thus false.
> However, in Rodin @thm3 is true and is proven by the auto-provers.
> 
> The reason is that in Rodin
>  #x.( P ) => Q
> is parsed as
>  (#x. (P) => Q )
> and Q is in the scope of the existential quantifier (see page 11 of The Event-B Mathematical Language).
> This is quite different from
>  (#x. (P)) => Q 
> where Q is *not* in the scope of the quantifier.
> 
> More details can be found here:
> https://prob.hhu.de/w/index.php?title=Implication_inside_an_Existential_Quantifier
> 
> The nightly version of ProB (which you can obtain from the update-site  https://stups.hhu-hosting.de/rodin/prob1/nightly) now generates a warning for @thm3 above.
> The warning detects suspicious implications inside existential quantifiers. 
> 
> I wonder whether one could introduce a similar warning in Rodin, detecting when one mixes the existential quantifier with an implication without parentheses (similar to the way Rodin disallows mixing conjunction and disjunction without parentheses), since an implication inside an existential quantifier is probably not intended by the user.
> 
> Greetings,
> Michael Leuschel
> 
> 
> 
> 
> 
> 
> 
> 
> 
> 
> _______________________________________________
> Rodin-b-sharp-user mailing list
> Rod...@li...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user

Dear Rodin User,

this weekend I stumbled upon a somewhat surprising aspect of the Rodin formula language.
Take the following Event-B context in Camille syntax:

context TestExistImplication
constants x y
axioms
 @axm1 x=1
 @axm2 y=2
 theorem @thm3 ∃z·(z∈1‥3 ∧ x=z) ⇒ y=44  
end

Before continuing to read, you may reflect and answer the question whether @thm3 is true or not.

--------------------------------

In classical B syntax, within Atelier-B, the answer is that @thm3 is false:
  ∃z·(z∈1‥3 ∧ x=z) is true
  y=44 is false
and the implication is thus false.
However, in Rodin @thm3 is true and is proven by the auto-provers.

The reason is that in Rodin
  #x.( P ) => Q
is parsed as
  (#x. (P) => Q )
and Q is in the scope of the existential quantifier (see page 11 of The Event-B Mathematical Language).
This is quite different from
  (#x. (P)) => Q 
where Q is *not* in the scope of the quantifier.

More details can be found here:
 https://prob.hhu.de/w/index.php?title=Implication_inside_an_Existential_Quantifier

The nightly version of ProB (which you can obtain from the update-site  https://stups.hhu-hosting.de/rodin/prob1/nightly) now generates a warning for @thm3 above.
The warning detects suspicious implications inside existential quantifiers. 

I wonder whether one could introduce a similar warning in Rodin, detecting when one mixes the existential quantifier with an implication without parentheses (similar to the way Rodin disallows mixing conjunction and disjunction without parentheses), since an implication inside an existential quantifier is probably not intended by the user.

Greetings,
Michael Leuschel

Hi guys,

I'm using Event-B and Rodin Platform to model a system and have an event
that receives one parameter. I'm using the animation model to animate the
specification and found a limitation in the number of parameters available
for an event. Is there a way to add more parameters? For example, the
following lock operation receives one parameter and when I try to animate
it I have only two options. Is there a way to have more (e.g.
SOURCE_TOKEN3, SOURCE_TOKEN4, SOURCE_TOKEN5)?

Thanks in advance
Guzmán

[image: image.png]

Dear Rodin users,

I am pleased to announce the release of version 2.4.1 of the Atelier B plug-in.

It fixes a bug related to encoding issues on some Chinese editions of Windows.
It provides the same provers as version 2.4.0 and is also compatible with Rodin 3.8 and 3.9.

Thanks to Li Qin for reporting the bug, helping to identify the issue and testing the patch.

Thanks to Thierry Lecomte at Clearsy for the support to publish this release.

The work on this release has been supported by the French ANR project Event-B Rodin Plus (EBRP, ANR-19-CE25-0010).

Cheers,
Guillaume Verdier

***********************************************************************
Call for Papers

ABZ 2025: 11th International Conference on Rigorous State Based Methods
 co-located with the 12th Rodin User and Developer Workshop

Düsseldorf, Heinrich Heine University Düsseldorf, Germany

June 10-13, 2025

https://abz-conf.org/site/2025/

***********************************************************************

The 11th international conference on rigorous state based methods
will be held June 10th to June 13th in the center of Düsseldorf (https://abz-conf.org/site/2025/venue/),
with easy access to the main railway station and the international airport.
ABZ'2025 will be co-located with the Rodin workshop.

ABZ 2025 deadlines:

Case Study Track
Abstract submission: February 03, 2025
Paper submission: February 10, 2025
Notification: March 29, 2025 
Final version: April 10, 2025

Main Track
Abstract submission: February 03, 2025
Paper submission: February 10, 2025
(including research/short/industry/journal-first papers)
Notification: March 29, 2025 
Final version: April 10, 2025

Doctoral Symposium
Paper submission: February 24, 2025
Notification: March 29, 2025 
Final version: April 10, 2025

----------
About ABZ
----------

The ABZ conference is dedicated to the cross-fertilization of state-based and machine-based formal methods, like Abstract State Machines (ASM), 
Alloy, B, TLA, VDM and Z, etc., that share a common conceptual foundation and  are widely used in both academia and industry for the design and 
analysis of hardware and software systems. 
The conference aims for a vital exchange of knowledge and experience among the research communities around different formal methods.

The name ABZ goes back to the first conference in London in 2008, where the ASM, B and Z conference series were merged into a joint
event. In the following years other formal methods were added, e.g. Alloy in 2010 (Orford, Canada), VDM in 2012 (Pisa, Italy), and
TLA+ in 2014 (Toulouse, France). After the also successful 2016 conferences in Linz, Austria, and 2018 in Southampton, UK, it was
decided to name the conference "ABZ: International Conference on Rigorous State Based Methods", to stress the openness for further
state-based formal methods. We hope to continue many fruitful discussions between representatives of the individual methods in the
past, which will bring us closer to the common goal of this research community: the creation of reliable and safe software and systems.  
ABZ2020 and ABZ2021 were planned in Ulm but virtually organised. With the editions of 2023 in Nancy and 2024 in Bergamo, ABZ conference returned to be a live event.

ABZ 2025 will feature a main conference track, a case study track, a doctoral symposium, tutorials, and workshops.


---------------------
Main Conference Track
---------------------
Contributions are solicited on all aspects of the theory and applications of ASMs, Alloy, B, TLA, VDM, Z and other state-based rigorous 
approaches in software/hardware engineering, including the development of tools and industrial applications. 
The program spans from theoretical and methodological foundations to practical applications, emphasizing system engineering methods 
and tools that are distinguished by mathematical rigor and have proved to be industrially viable. 
The main goal of the conference is to contribute to the integration of accurate state- and machine-based system development methods, 
clarifying their commonalities and differences to better understand how to combine different approaches for accomplishing the various 
tasks in modeling, experimental validation, mathematical verification of reliable high-quality hardware/software systems. 
Although organized to host several formal methods in a single event, editorial control of the joint conference is vested in one 
integrated program committee.


-----------------
Case Study Track
-----------------
As successfully practiced since ABZ 2014, the 11th edition of ABZ will again include special sessions dedicated to an industrial case study.
We explicitly invite you to also submit contributions to case studies from previous conferences, which substantially extend the solutions presented 
there in one aspect or another. Possible enhancements could be new proof techniques, more elegant modeling, generation, verification, or validation 
of executable code, etc.
This year the case study is about a safety controller for autonomous driving on a highway and
there is a particular emphasis on making the exposition convincing and understandable for researchers
from other communities.

See https://abz-conf.org/site/2025/casestudy/ for a detailed description of the new case study and links to the previous ones.


------------
Submissions
------------
We welcome four kinds of contributions:

*  Full research papers: 
   Full research papers which have to be original, unpublished and not submitted elsewhere. 
   A paper of no more than 16 pages (excluding references) in LNCS format is expected and will be reviewed.
    
*  Short papers: 
   Short papers to present and validate a work in progress or tool demonstrations. A paper of no more than 6 pages (excluding references) in LNCS format 
   is expected and will be reviewed.

*  Application in industry papers: 
   Reporting on work or experiences on the application of state based formal methods in industry. A paper of no more than 8 pages (excluding references) 
   in LNCS format is expected and will be reviewed. It is also an interesting option for industrial practitioners who sometimes face too many constraints 
   to prepare a full paper.

*  Journal-First papers: 
   Journal-First papers summarize recently published papers in high-quality journals. The aim of journal-first papers is to further enrich the program of 
   ABZ and to provide more visibility to an already published journal paper in the scope of the ABZ conference. An extended abstract of no more than 6 
   pages (excluding references) in LNCS format is expected and will be reviewed.

*  Case study papers: 
   Full papers reporting on the experiments conducted with any of the state based techniques in the scope of ABZ 2024 case study. 
   A paper of no more than 16 pages (excluding references) in LNCS format is expected and will be reviewed. 
   We also expect a link to a webpage, where the models, proofs, test cases, simulations, etc. models can be downloaded.
   It is expected that authors will make available all the experimental data for the community to validate and reproduce their findings.
 
*  Contribution to doctoral symposium: 
   This is an excellent opportunity for PhD students to present their ongoing work and receive valuable feedback from the ABZ community. 
    A paper of no more than 4 pages (excluding references) in LNCS format is expected and will be reviewed.

Accepted papers will appear in the Springer LNCS proceedings.
The deadlines for the different kinds of contributions appear above.


-------------------
Organization
-------------------
Conference Chairs:
Michael Leuschel (CoChair), Heinrich-Heine-Universität, Düsseldorf, Germany
Fuyuki Ishikawa (CoChair), National Institute of Informatics, Tokyo, Japan

Case Study Chair:
Fabian Vu, Heinrich-Heine-Universität, Düsseldorf, Germany

Doctoral Symposium Chairs
Asieh Salehi Fathabadi, University of Southampton, UK
Philipp Körner, Heinrich-Heine-Universität, Düsseldorf, Germany

Publicity/Social/Web Chairs:
Jan Gruteser, Heinrich-Heine-Universität, Düsseldorf, Germany
Fabian Vu, Heinrich-Heine-Universität, Düsseldorf, Germany

For further questions concerning ABZ 2025, please contact us at ab...@cs...

Program Committee:
* Yamine Ait Ameur, IRIT/INPT-ENSEEIHT, France
* Toshiaki Aoki, JAIST, Japan
* Paolo Arcaini, National Institute of Informatics, Japan
* Richard Banach, University of Manchester, UK
* Silvia Bonfanti, University of Bergramo, Italy
* Chiara Braghin, University of Milan, Italy
* Maximiliano Cristiá, Universidad Nacional de Rosario, Argentina
* Alcino Cunha, University of Minho, Portugal
* Catherine Dubois, ENSIIE, France
* Guillaume Dupont, IRIT/INPT-ENSEEIHT, France
* Marie Farell, University of Manchester, UK
* Flavio Ferrarotti, Software Competence Centre Hagenberg, Austria
* Marc Frappier, Université de Sherbrooke, Canada
* Angelo Gargantini, University of Bergamo, Italy
* Uwe Glässer, Simon Fraser University, Canada
* Stefan Hallerstede, Aarhus University, Denmark
* Thai Son Hoang, University of Southampton, UK
* Akram Idani, 	Univ. Grenoble Alpes, VERIMAG lab, France
* Fuyuki Ishikawa, National Institute of Informatics, Japan
* Ensuk Kang, Carnegie Mellon University, USA
* Tsutomu Kobayashi, Japan Aerospace Exploration Agency, Japan
* Philipp Körner, University of Düsseldorf, Germany
* Igor Konnov, Informal Systems, Austria
* Régine Laleau, Paris Est Creteil University, France
* Thierry Lecomte, CLEARSY, France
* Michael Leuschel, University of Düsseldorf, Germany
* Frederic Mallet, Université Côte d'Azur, France
* Atif Mashkoor, Johannes Kepler University, Austria
* Dominique Mery, Université de Lorraine, LORIA, France
* Stephan Merz, Inria, France
* Alexander Raschke, Ulm University, Germany
* Elvinia Riccobene, University of Milan, Italy
* Asieh	Salehi Fathabadi, University of Southampton, UK
* Patrizia Scandurra, University of Bergamo, Italy
* Gerhard Schellhorn, Universitaet Augsburg, Germany
* Klaus-Dieter Schewe, Zhejiang University, China
* Emil Sekerinski, McMaster University, Canda
* Neeraj Singh, INPT-ENSEEIHT / IRIT, University of Toulouse, France
* Maurice ter Beek, CNR, Italy
* Laurent Voisin, Systerel, France
* Hillel Wayne, USA

Dear Rodin users,

I am pleased to announce the release of version 2.4.0 of the Atelier B plug-in.

It provides the provers from the latest Atelier B release, version 24.04.2.
It is compatible with Rodin 3.8 and 3.9.

Thanks to Thierry Lecomte and David Deharbe at Clearsy for the support to make this release.

The work on this release has been supported by the French ANR project Event-B Rodin Plus (EBRP, ANR-19-CE25-0010).

Cheers,
Guillaume Verdier

Hi everybody, 
in case you are bothered (like myself) about the increase whitespace in Rodin’s Event-B Explorer or ProB’s operation view on macOS, you can add the following line to your rodin.ini file:
-Dorg.eclipse.swt.internal.carbon.smallFonts

Kind regards,
Michael Leuschel

Dear Rodin users,

I am pleased to announce the release of version 0.8 of the B2Latex plug-in.
This version is compatible with Rodin 3.8 and 3.9.

It is available in the Rodin Plug-ins update site. You can update through Help > Check for Updates.

The following changes have been implemented in this version:
- a compatibility issue with Rodin 3.9 has been fixed
- it is now possible to select several elements and generate LaTeX documents for them at once

The work on this release has been supported by the French ANR project Event-B Rodin Plus (EBRP, ANR-19-CE25-0010).

Best regards,
Guillaume Verdier

Dear All,

I am glad to announce that Rodin 3.9 is available. You can either install it from SourceForge (https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.9/) or use the update mechanism of Eclipse.
Rodin 3.9 brings several bug fixes. It also upgrades the underlying Eclipse to 2023-12 (4.30), which can be run by Java 17 Runtimes.
Rodin will work on macOS, Linux and Windows 64-bit computers. You need to have a 64-bit Java JRE (version 17 or later) installed on your computer to run Rodin.

----
macOS caveats
----
The Rodin application is not notarized. This means that when you download it from SourceForge, macOS will quarantine the application and tell you that it is broken. Just run the command "xattr -rc Rodin.app" in a Terminal to remove the quarantine tag.

----
Important information
----
Please read the Rodin Platform release notes before proceeding with an upgrade.

See https://wiki.event-b.org/index.php/Rodin_Platform_3.9_Release_Notes

----
Fixed Bugs and Implemented Features
----
bug #829: Autorewriter generates invalid proof rule
bug #828: Trace debug/rodintypes/verbose doesn't work
bug #827: Post-tactic applied after a tactic failure
bug #826: NullPointerException in hypothesis page UI
bug #824: Exception related to proof tree UI update
bug #823: Do not allow prime in extension symbol
bug #822: Error handling when loading formula extensions
bug #821: Issues with proof tree filtering
bug #819: "Prove Automatically" setting not persisted
bug #818: Hypothesis hiding by eh/he 

Feature Requests
——
FR #403: User provided names for fresh variables
FR #400: Add factory method to check if symbol is valid
FR #398: Rewrite rule for recursive exponentiation
FR #396: New reasoners on inductive types
FR #395: Manual application of compset simplification rules
FR #394: Rule for functional image
FR #393: Simplify set membership of min/max
FR #392: Simplify bool(B=TRUE) to B
FR #385: Better message for syntax errors in set comprehension
FR #383: Additional inference rule for finiteness
FR #368: Better simplification of identity

This release would not have happened without the support from the Event-B Rodin Plus project funded by the French National Research Agency (ANR).

Best Regards,
---
Idir AIT SADOUNE
Associate Professor 

CentraleSupelec - Computer Science Department
LMF - Formal Methods Laboratory  
Paris-Saclay University
www.idiraitsadoune.com <https://www.idiraitsadoune.com/>
+33/0 1 75 31 78 46 

Dear Colin,

> On 24 Apr 2024, at 17:35, Hogben, Colin H <Col...@uk...> wrote:
> 
> - When editing text in the Rodin editor, a mini light bulb icon appears just to the left; the hover text is "Content Assist Available (Ctrl + Space)" but ctrl+space does nothing.  Should it do something?

It should provide some kind of content completion. This is a known bug in that editor; it has not been fixed yet.
https://sourceforge.net/p/rodin-b-sharp/bugs/793/

> - In one project (in 4.7) in the Event-B Explorer, a machine has a mini-icon overlaying the top-left of the "M" icon - looks a bit like some sort of "file" icon.  I guess it's trying to tell me something, but what?


This icon merely indicates that the component (machine, in your case) has a non-empty comment.
It does not indicate any kind of error or warning, but can be helpful to determine at a glance which components are documented and which ones are not.

I can’t provide any help regarding your issues with Camille, sorry.

Best regards,
Guillaume Verdier

Hi,

Having spent some time using Rodin (following examples and tutorials 
etc.) there are number of things I've seen in the Rodin UI which I'd 
like help to understand.

- While editing with Camille, sometimes there is a red cross icon at the 
bottom left by the end of file.  There are no Rodin Problems, and 
hovering over it gets nothing.  Should I worry?

- Sometimes I have seen a warning triangle icon at the top left of the 
edit window; hovering over it gets e.g. "Warnings: 2".  Again no Rodin 
problems, so what are the warnings?

- When editing text in the Rodin editor, a mini light bulb icon appears 
just to the left; the hover text is "Content Assist Available (Ctrl + 
Space)" but ctrl+space does nothing.  Should it do something?

- When I add an event or invariant in Camille and then save, sometimes 
(always?) no Proof Obligations are added.  But if I perform similar 
modifications using the Rodin editor, new POs are added.  I'd expect the 
addition of POs to be a function of the underlying model rather than the 
particular editor being used.

- In one project (in 4.7) in the Event-B Explorer, a machine has a 
mini-icon overlaying the top-left of the "M" icon - looks a bit like 
some sort of "file" icon.  I guess it's trying to tell me something, but 
what?

Any guidance appreciated.
Thanks,
-- 
Colin Hogben
Software/Control Engineer
UK Atomic Energy Authority
Tel: +44 1235 464948