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

DOI10.1007/978-3-540-78800-3_4MaRDI QIDQ5458319zbMATH OpenOpenAlexFDO

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

• Automata, Languages and Programming
• Computer Aided Verification
• Computer Aided Verification
• Formal Methods in Computer-Aided Design
• 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?)
• Inferring Network Invariants Automatically
• Local Proofs for Global Safety Properties
• Proving properties of a ring of finite-state machines
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• 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)

• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
• Parameterized model checking of networks of timed automata with Boolean guards
• Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
• Parameterised verification for multi-agent systems
• An abstraction technique for parameterized model checking of leader election protocols: application to FTSP
• Parametrized invariance for infinite state processes
• Multi-parameterised compositional verification of safety properties
• 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
• Verification, Model Checking, and Abstract Interpretation

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)