Optimising the ProB model checker for B using partial order reduction

DOI10.1007/s00165-015-0351-1zbMath1342.68208OpenAlexW2295263482MaRDI QIDQ736463

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)

Related Items

Optimising the ProB model checker for B using partial order reduction, Unnamed Item

Uses Software

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

Cites Work

• Stutter-invariant temporal properties are expressible without the next-time operator
• Optimising the ProB model checker for B using partial order reduction
• Derivation of concurrent programs by stepwise scheduling of Event-B models
• Isabelle/HOL. A proof assistant for higher-order logic
• Using partial orders for the efficient verification of deadlock freedom and safety properties
• State space reduction using partial order techniques
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• State Space Reduction for Sensor Networks Using Two-Level Partial Order Reduction
• Directed Model Checking for B: An Evaluation and New Techniques
• The High Road to Formal Validation:
• Partial Order Reduction for State/Event LTL
• The B-Book
• Depth-First Search and Linear Graph Algorithms
• Model Checking Software
• Integrated Formal Methods
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item