Rigorous State-Based Methods by Leuschel, Michael; Ishikawa, Fuyuki;

Hosszú leírás:

"

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.

Tartalomjegyzék:

"

.- 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 models@run.time.

.- 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.