Optimising the ProB model checker for B using partial order reduction
From MaRDI portal
Publication:736463
DOI10.1007/S00165-015-0351-1zbMATH Open1342.68208OpenAlexW2295263482MaRDI QIDQ736463FDOQ736463
Authors: Ivaylo Dobrikov, Michael Leuschel
Publication date: 4 August 2016
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-015-0351-1
Recommendations
- scientific article; zbMATH DE number 2087625
- Formal verification of a partial-order reduction technique for model checking
- Dynamic partial-order reduction for model checking software
- Combining partial-order reductions with on-the-fly model-checking.
- Formal verification of an executable LTL model checker with partial order reduction
- scientific article; zbMATH DE number 1361136
Cites Work
- Depth-First Search and Linear Graph Algorithms
- Isabelle/HOL. A proof assistant for higher-order logic
- Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
- Title not available (Why is that?)
- Modeling in Event B. System and software engineering.
- The B-Book
- Stutter-invariant temporal properties are expressible without the next-time operator
- The High Road to Formal Validation:
- State space reduction using partial order techniques
- Title not available (Why is that?)
- Integrated Formal Methods
- Model Checking Software
- Using partial orders for the efficient verification of deadlock freedom and safety properties
- State space reduction for sensor networks using two-level partial order reduction
- Directed Model Checking for B: An Evaluation and New Techniques
- Partial Order Reduction for State/Event LTL
- Title not available (Why is that?)
- Title not available (Why is that?)
- Optimising the ProB model checker for B using partial order reduction
- Derivation of concurrent programs by stepwise scheduling of Event-B models
Cited In (5)
- Formal verification of an executable LTL model checker with partial order reduction
- Title not available (Why is that?)
- Optimising the ProB model checker for B using partial order reduction
- Title not available (Why is that?)
- Operation caching and state compression for model checking of high-level models. How to have your cake and eat it
Uses Software
This page was built for publication: Optimising the ProB model checker for B using partial order reduction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q736463)