Efficient approximate verification of B and Z models via symmetry markers

DOI10.1007/S10472-010-9208-8MaRDI QIDQ622591zbMATH OpenOpenAlexFDO

Authors Michael Leuschel, Thierry Massart

Publication date 3 February 2011

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10472-010-9208-8

zbMATH Keywords

B-Methodformal methodslogic programmingmodel checkingsymmetry

Mathematics Subject Classification ID

Logic in computer science (03B70) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Graph theory (including graph drawing) in computer science (68R10)

Recommendations

• Efficient Approximate Verification of Promela Models Via Symmetry Markers
• scientific article; zbMATH DE number 1796126
• scientific article; zbMATH DE number 1487862
• Efficient symmetry reduction and the use of state symmetries for symbolic model checking
• Symmetry Reduction for Probabilistic Model Checking

Cites work

• Combining symmetry reduction and under-approximation for symbolic model checking
• Efficient Approximate Verification of Promela Models Via Symmetry Markers
• FM 2005: Formal Methods
• Formal Modeling and Analysis of Timed Systems
• Graphs, Algorithms, and Optimization
• scientific article; zbMATH DE number 1265079 (Why is no real title available?)
• In code. A mathematical journey.
• Modeling in Event B. System and software engineering.
• Myths about the mutual exclusion problem
• Principles of the SPIN model checker. Foreword by Gerard J. Holzmann
• The High Road to Formal Validation:
• Z2SAL: a translation-based model checker for Z

Cited in

(2)

• Operation caching and state compression for model checking of high-level models. How to have your cake and eat it
• Efficient Approximate Verification of Promela Models Via Symmetry Markers

Describes a project that uses

Uses Software

• TopSpin
• Uppaal
• Rodin
• SymmSpin
• PROMELA
• jSpin
• nauty
• Z2sal
• ProB
• B4Free
• Atelier B
• SPIN
• Spin-to-Grape

This page was built for publication: Efficient approximate verification of B and Z models via symmetry markers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q622591)