Formal verification of an executable LTL model checker with partial order reduction

DOI10.1007/s10817-017-9418-4zbMath1426.68162OpenAlexW2671604182MaRDI QIDQ682350

Julian Brunner, Peter Lammich

Publication date: 2 February 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://www.research.manchester.ac.uk/portal/en/publications/formal-verification-of-an-executable-ltl-model-checker-with-partial-order-reduction(a99dc6b6-0529-4ae7-860e-fd64f74c9912).html

zbMATH Keywords

formal verificationmodel checkingpartial order reduction

Mathematics Subject Classification ID

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

Related Items

Automated Verification of Parallel Nested DFS ⋮ Verified Certification of Reachability Checking for Timed Automata ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Verified Compositional Algorithm for AI Planning ⋮ Formal verification of an executable LTL model checker with partial order reduction ⋮ Certifying emptiness of timed Büchi automata ⋮ From LCF to Isabelle/HOL ⋮ Efficient verified (UN)SAT certificate checking

Uses Software

• Isabelle
• Isabelle/HOL
• SPIN
• PROMELA
• Coinductive
• Refinement Monadic
• CAVA Automata Library
• CAVA
• Stuttering Equivalence
• Collections
• Archive Formal Proofs
• CAVA LTL Modelchecker
• Gabow SCC
• Imperative Refinement

Cites Work

• Unnamed Item
• Unnamed Item
• Stutter-invariant temporal properties are expressible without the next-time operator
• Formal verification of an executable LTL model checker with partial order reduction
• Combining partial-order reductions with on-the-fly model-checking.
• Isabelle/HOL. A proof assistant for higher-order logic
• Truly Modular (Co)datatypes for Isabelle/HOL
• Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Refinement to Imperative/HOL
• Comprehending monads
• Refinement Calculus
• The Isabelle Collections Framework