Pattern-based Refinemnt Generation Through Domain Specifi Languages
Inductive Construction in B with the Theory Plugin
Validation of Formal Models by Interactive Simulation
Thread-Local, Step-Local Proof Obligations for Refnement of State-Based Concurrent Systems
Encoding TLA+ Proof Obligations Safely for SMT
Compositional I/O Abstract State Machines
Crucible Tools for Test Generation and Animation of Alloy Models
Modelling an Automotive Software System with TASTD
TASTD a real-time extension for ASTD
Validation by Abstraction and Refiement
Verifying Event-B Hybrid Models using Cyclone
Exploration of Reflectie ASMs for Security
Standalone Event-B models analysis relying on the EB4EB meta-theory
Adding records to Alloy
Designing Secure Systems using Hierarchical STPA and Event-B
Behavioural Theory of Reflectie Algorithms
Specification in the Event-B Institution
Verifying temporal relational models with Pardinus
AMAN Case Study
Analysis of a Safety-critical Interactive System through VOs
Task Model Design and Analysis with Alloy
Modeling and Verifying an Arrival Manager using Event-B
Formal MVC: a Pattern for the Integration of ASM Specification in UI Development
Exploring a methodology for formal verificatio of safety-critical systems
Extending Modelchecking with ProB to Floating-Point Numbers and Hybrid Systems
A framework for formal verificatio and validation of railway systems
Reconstruction of TLAPS proofs solved by veriT in Lambdapi.