Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
DOI10.1007/978-3-540-78800-3_4zbMATH Open1134.68403OpenAlexW1546036076MaRDI QIDQ5458319FDOQ5458319
Authors: Muralidhar Talupur, Helmut Veith, Edmund 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
Recommendations
- Verification, Model Checking, and Abstract Interpretation
- Model checking and abstraction to the aid of parameterized systems (a survey)
- MONOTONIC ABSTRACTION: ON EFFICIENT VERIFICATION OF PARAMETERIZED SYSTEMS
- Parameterized model checking of synchronous distributed algorithms by abstraction
- View abstraction -- a tutorial (invited paper)
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- Reasoning about systems with many processes
- Title not available (Why is that?)
- Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
- Verification, Model Checking, and Abstract Interpretation
- Reasoning about networks with many identical finite state processes
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Verifying safety properties of concurrent Java programs using 3-valued logic
- Inferring Network Invariants Automatically
- Computer Aided Verification
- Proving properties of a ring of finite-state machines
- Title not available (Why is that?)
- Computer Aided Verification
- Title not available (Why is that?)
- Title not available (Why is that?)
- Formal Methods in Computer-Aided Design
- Title not available (Why is that?)
- Local Proofs for Global Safety Properties
- Automata, Languages and Programming
Cited In (11)
- Parameterised verification for multi-agent systems
- Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
- Verification, Model Checking, and Abstract Interpretation
- Tutorial on parameterized model checking of fault-tolerant distributed algorithms
- Parameterized model checking of networks of timed automata with Boolean guards
- Monotonic Abstraction in Action
- Parametrized invariance for infinite state processes
- Multi-parameterised compositional verification of safety properties
- 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
- An abstraction technique for parameterized model checking of leader election protocols: application to FTSP
Uses Software
This page was built for publication: Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5458319)
