Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems

DOI10.1007/978-3-540-78800-3_4zbMath1134.68403OpenAlexW1546036076MaRDI QIDQ5458319

Muralidhar Talupur, Helmut Veith, Edmund M. Clarke

Publication date: 11 April 2008

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-78800-3_4

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (10)

Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems ⋮ \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms ⋮ Parametrized invariance for infinite state processes ⋮ An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to FTSP ⋮ Multi-parameterised compositional verification of safety properties ⋮ Parameterized model checking of networks of timed automata with Boolean guards ⋮ Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms ⋮ Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems ⋮ Monotonic Abstraction in Action ⋮ Parameterised verification for multi-agent systems

Uses Software

• Cadence SMV

Cites Work

• Reasoning about networks with many identical finite state processes
• Proving properties of a ring of finite-state machines
• Inferring Network Invariants Automatically
• Reasoning about systems with many processes
• Verifying safety properties of concurrent Java programs using 3-valued logic
• Computer Aided Verification
• Computer Aided Verification
• Local Proofs for Global Safety Properties
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• Automata, Languages and Programming
• Formal Methods in Computer-Aided Design
• Verification, Model Checking, and Abstract Interpretation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems