Directed Model Checking for B: An Evaluation and New Techniques

DOI10.1007/978-3-642-19829-8_1MaRDI QIDQ2999306zbMATH OpenOpenAlexFDO

Authors Michael Leuschel, Jens Bendisposto

Publication date 12 May 2011

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-19829-8_1

zbMATH Keywords

B-methoddirected model checkingindustrial case studiesmodel checkingsearchspintool support

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Survey on Directed Model Checking
• Model Checking Software
• Transition-Based Directed Model Checking
• Higher-order model checking in direct style
• A Direct Algorithm for Multi-valued Bounded Model Checking
• BDD-based symbolic model checking

Cites work

• Directed Model Checking for B: An Evaluation and New Techniques
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 2087625 (Why is no real title available?)
• scientific article; zbMATH DE number 2087636 (Why is no real title available?)
• Model Checking Software
• Model Checking Software
• Principles of the SPIN model checker. Foreword by Gerard J. Holzmann
• Symbolic model checking: \(10^{20}\) states and beyond
• The B-Book
• The High Road to Formal Validation:

Cited in

(8)

• Integrating formal specifications into applications: the ProB Java API
• Directed Model Checking for B: An Evaluation and New Techniques
• Survey on Directed Model Checking
• scientific article; zbMATH DE number 1746648 (Why is no real title available?)
• scientific article; zbMATH DE number 7453192 (Why is no real title available?)
• ZB 2005: Formal Specification and Development in Z and B
• Model Checking Software
• Optimising the ProB model checker for B using partial order reduction

Describes a project that uses

Uses Software

• jSpin
• TLC
• FDR2
• ProB
• SPIN

This page was built for publication: Directed Model Checking for B: An Evaluation and New Techniques

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