Property preserving abstractions for the verification of concurrent systems

DOI10.1007/BF01384313zbMath0829.68053OpenAlexW1987073197MaRDI QIDQ1346649

C. Loiseaux, Joseph Sifakis, Susanne Graf, Ahmed Bouajjani, Saddek Bensalem

Publication date: 10 April 1995

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01384313

zbMATH Keywords

verification methodreactive systems

Mathematics Subject Classification ID

Related Items (44)

Consistent Consequence for Boolean Equation Systems ⋮ On the universal and existential fragments of the \(\mu\)-calculus ⋮ Counterexample-guided predicate abstraction of hybrid systems ⋮ Combining static analysis and case-based search space partitioning for reducing peak memory in model checking ⋮ Applicability of fair simulation ⋮ Abstraction and Abstraction Refinement ⋮ Algebraic simulations ⋮ Simple proof techniques for property preservation via simulation ⋮ Refinement preserving approximations for the design and verification of heterogeneous systems ⋮ When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus ⋮ \(\text{DELFIN}^+\): an efficient deadlock detection tool for CCS processes ⋮ Towards the hierarchical verification of reactive systems ⋮ Combining Predicate Abstraction with Fixpoint Approximations ⋮ On using data abstractions for model checking refinements ⋮ Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols ⋮ Simulation relations and applications in formal methods ⋮ Unfolding Graph Transformation Systems: Theory and Applications to Verification ⋮ Approximating Behaviors in Embedded System Design ⋮ Temporal-logic property preservation under Z refinement ⋮ Inverse-limit and topological aspects of abstract interpretation ⋮ Complete Abstractions and Subclassical Modal Logics ⋮ On the preservation of properties when changing communication models ⋮ Correcting a Space-Efficient Simulation Algorithm ⋮ Abstract model repair for probabilistic systems ⋮ A framework for the verification of infinite-state graph transformation systems ⋮ Combining search space partition and abstraction for LTL model checking ⋮ Networks of Processes with Parameterized State Space ⋮ Feedback in Synchronous Relational Interfaces ⋮ Competent predicate abstraction in model checking ⋮ Generating models of infinite-state communication protocols using regular inference with abstraction ⋮ Verification by augmented abstraction: The automata-theoretic view ⋮ Smaller Abstractions for ∀CTL* without Next ⋮ Partial predicate abstraction and counter-example guided refinement ⋮ Design and Verification of Fault-Tolerant Components ⋮ Abstraction for non-ground answer set programs ⋮ Compositional minimisation of finite state systems using interface specifications ⋮ An efficient simulation algorithm based on abstract interpretation ⋮ Using heuristic search for finding deadlocks in concurrent systems ⋮ A semantic framework for the abstract model checking of tccp programs ⋮ Algorithmic analysis of programs with well quasi-ordered domains. ⋮ Verification by augmented finitary abstraction ⋮ Extracting Program Logics From Abstract Interpretations Defined by Logical Relations ⋮ Narrowing and Rewriting Logic: from Foundations to Applications ⋮ Reduced models for efficient CCS verification

Uses Software

• UNITY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Results on the propositional \(\mu\)-calculus
• The existence of refinement mappings
• A calculus of communicating systems
• Constructive versions of Tarski's fixed point theorems
• Temporal logic can be more expressive
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• A Theory of Communicating Sequential Processes
• “Sometimes” and “not never” revisited
• A galois connection calculus for abstract interpretation
• Galois Connexions

This page was built for publication: Property preserving abstractions for the verification of concurrent systems