Optimising the ProB model checker for B using partial order reduction

DOI10.1007/S00165-015-0351-1zbMATH Open1342.68208OpenAlexW2295263482MaRDI QIDQ736463FDOQ736463

Michael Leuschel, Ivaylo Dobrikov

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

zbMATH Keywords

model checkingstatic analysisEvent-BLTLpartial order reduction

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• 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
• 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
• Optimising the ProB model checker for B using partial order reduction
• Derivation of concurrent programs by stepwise scheduling of Event-B models

Cited In (3)

• Title not available (Why is that?)
• Optimising the ProB model checker for B using partial order reduction
• Title not available (Why is that?)

Uses Software

• Isabelle/HOL
• SPIN
• DiVinE
• Rodin
• ProB
• LTSmin
• CAVA LTL Modelchecker

Recommendations

• Dynamic partial-order reduction for model checking software 👍 👎
• Combining partial-order reductions with on-the-fly model-checking. 👍 👎
• Formal verification of a partial-order reduction technique for model checking 👍 👎
• Formal verification of an executable LTL model checker with partial order reduction 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎

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)