Efficient approximate verification of B and Z models via symmetry markers

DOI10.1007/s10472-010-9208-8zbMath1209.68127OpenAlexW2054273693MaRDI QIDQ622591

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

symmetrymodel checkingformal methodslogic programmingB-Method

Mathematics Subject Classification ID

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

Related Items (1)

Operation caching and state compression for model checking of high-level models. How to have your cake and eat it

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Z2SAL: a translation-based model checker for Z
• Combining symmetry reduction and under-approximation for symbolic model checking
• Myths about the mutual exclusion problem
• Efficient Approximate Verification of Promela Models Via Symmetry Markers
• The High Road to Formal Validation:
• Graphs, Algorithms, and Optimization
• FM 2005: Formal Methods
• Formal Modeling and Analysis of Timed Systems

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