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

DOI10.1007/978-3-540-78800-3_4MaRDI QIDQ5458319zbMATHOpenAlexFDO

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

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)

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)

Cites work

• scientific article; zbMATH DE number 1670785 (Why is no real title available?)
• scientific article; zbMATH DE number 1701752 (Why is no real title available?)
• scientific article; zbMATH DE number 1538040 (Why is no real title available?)
• scientific article; zbMATH DE number 1796136 (Why is no real title available?)
• scientific article; zbMATH DE number 2086524 (Why is no real title available?)
• scientific article; zbMATH DE number 1852158 (Why is no real title available?)
• scientific article; zbMATH DE number 1903348 (Why is no real title available?)
• scientific article; zbMATH DE number 2102701 (Why is no real title available?)
• Automata, Languages and Programming
• Computer Aided Verification
• Computer Aided Verification
• Formal Methods in Computer-Aided Design
• Inferring Network Invariants Automatically
• Local Proofs for Global Safety Properties
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• Proving properties of a ring of finite-state machines
• Reasoning about networks with many identical finite state processes
• Reasoning about systems with many processes
• Verification, Model Checking, and Abstract Interpretation
• Verifying safety properties of concurrent Java programs using 3-valued logic

Cited in

(11)

• Parametrized invariance for infinite state processes
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
• Verification, Model Checking, and Abstract Interpretation
• Monotonic Abstraction in Action
• Tutorial on parameterized model checking of fault-tolerant distributed algorithms
• Parameterised verification for multi-agent systems
• Parameterized model checking of networks of timed automata with Boolean guards
• An abstraction technique for parameterized model checking of leader election protocols: application to FTSP
• Multi-parameterised compositional verification of safety properties
• Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems

Describes a project that uses

Uses Software

• Cadence SMV

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)