Michael Leuschel

Latest

• Integrating Formal Specifications into Applications - The ProB Java API
• The First Twenty-Five Years of Industrial Use of the B Method
• Validation and Real-Life Demonstration of ETCS Hybrid Level 3 Principles Using a Formal B Model
• Translating Alloy and Extensions to Classical B
• Embedding SMT-LIB into B for Interactive Proof and Constraint Solving
• Embedding High-Level Formal Specifications into Applications
• The History and Evolution of B and Event-B
• Repair and Generation of Formal Models Using Synthesis
• From Software Specifications to Constraint Programming
• A Translation from Alloy to B
• Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains
• Three is a crowd: SAT, SMT and CLP on a chessboard
• Proof Assisted Bounded and Unbounded Symbolic Model Checking of Software and System Models
• Contraint Logic Programming over Infinite Domains with an Application to Proof
• SMT Solvers for Validation of B and Event-B models
• Interactive Model Repair by Synthesis
• Proof Assisted Symbolic Model Checking for B and Event-B
• Turning Failure into Proof: The ProB Disprover for B and Event-B
• Inferring Physical Units in Formal Models
• From Animation to Data Validation: The ProB Constraint Solver 10 Years On
• Who watches the watchers: Validating the ProB Validation Tool
• Inferring Physical Units in B Models
• Turning Failure into Proof: Evaluating the ProB Disprover
• B constrained