Description
Book Synopsis.- 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 extsc{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.
