Rigorous State-Based Methods

11th International Conference, ABZ 2025, Düsseldorf, Germany, June 10–13, 2025, Proceedings
Erscheinungsjahr 2025
ISBN: 978-3-031-94532-8
Verlag: Springer

Buch, Englisch, 360 Seiten, Format (B × H): 155 mm x 235 mm

Reihe: Lecture Notes in Computer Science

This book constitutes the refereed proceedings of the 11th International Conference on Rigorous State-Based Methods, ABZ 2025, held in Düsseldorf, Germany, during June 10–13, 2025.

The 10 full papers, 4 short papers, 2 PhD Symposium papers and 5 case study papers presented in this book were carefully reviewed and selected from 33 submissions. The proceedings also contain one invited talk in full paper length. 

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

Zielgruppe

Research

Autoren/Hrsg.

Leuschel, Michael

Ishikawa, Fuyuki

Fachgebiete

• Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Compiler
• Mathematik | Informatik EDV | Informatik Technische Informatik
• Mathematik | Informatik EDV | Informatik Informatik Künstliche Intelligenz
• Mathematik | Informatik EDV | Informatik Informatik Mathematik für Informatiker
• Mathematik | Informatik EDV | Informatik Angewandte Informatik

Inhaltsverzeichnis

.- An Invited Talk about B.

.- Neurosymbolic Learning Systems: Artificial Intelligence and Formal Methods.

.- Mathematical Proofs and Moving Trains: The Double Life of Atelier B.

.- Behavioural Theory of Reflective Parallel Algorithms.

.- Using Symbolic Model Execution to Detect Vulnerabilities of Smart Contracts.

.- Safely Encoding B Proof Obligations in SMT-LIB.

.- On Writing Alloy Models: Metrics and a new Dataset.

.- On Quantitative Solution Iteration in QAlloy.

.- Proof Semantics of Railway Interlocking.

.- Translating Event-B models and development proofs to TLA.

.- The Proved Construction of a Protocol with an Example.

.- Insider Threat Simulation Through Ant Colonies and ProB.

.- Developing safe exception recovery mechanisms for CHERI capability hardware using UML-B formal analysis.

.- Case Study: Safety Controller for Autonomous Driving on Highways.

.- Safety enforcement for autonomous driving on a simulated highway using Asmeta [e-mail].

.- Enhancing Decision-making Safety in Autonomous Driving Through Online Model Checking.

.- Polychronous RSS in a Process-Algebraic Framework - A Case Study in Autonomous Driving Safety.

.- On The Road Again (Safely): Modelling and Analysis of Autonomous Driving with \textsc{Stark}.

.- Modelling and Verification of Highway Car Control with KeYmaera X.

.- State-Based Modelling with a Concept DSL.

.- Towards an End-to-End Tool Chain for Traceable and Verifiable Railway Signalling Specifications.

.- A reasoning and explicit algebraic theory for BBSL in Event-B: EB4BBSL framework.

.- Model-Based Testing of Non-Deterministic Systems.

.- Weakening Goals in Logical Specifications.

.- Formal modelling and reasoning on Assurance Cases expressed with GSN in Event-B.