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

model checkingsearchspintool supportB-methoddirected model checkingindustrial case studies

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

• 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?)
• Directed Model Checking for B: An Evaluation and New Techniques
• 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)

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

Describes a project that uses

Uses Software

• SPIN
• ProB
• jSpin
• TLC
• FDR2

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)