Multi-parameterised compositional verification of safety properties

DOI10.1016/J.IC.2015.08.002zbMATH Open1329.68173OpenAlexW1649347715MaRDI QIDQ498394FDOQ498394

Authors: Antti Siirtola, Juha Kortelainen 

Publication date: 28 September 2015

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2015.08.002

Recommendations

• Compositional analysis for verification of parameterized systems
• scientific article; zbMATH DE number 1956590
• scientific article; zbMATH DE number 2080051
• All for the price of few (parameterized verification through view abstraction)
• Symmetry and Completeness in the Analysis of Parameterized Systems

zbMATH Keywords

parameterised verificationdecidabilityconcurrency theorycompositional reasoningrefinement checking

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• CONCUR 2004 - Concurrency Theory
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• Verification, Model Checking, and Abstract Interpretation
• Title not available (Why is that?)
• Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
• Well-structured transition systems everywhere!
• Understanding concurrent systems
• On Reasoning About Rings
• Defining liveness
• A symbolic approach to predicate abstraction.
• Title not available (Why is that?)
• Computer Aided Verification
• A structural induction theorem for processes
• Verification of parametric concurrent systems with prioritised FIFO resource management
• Computer Science Logic
• The Spotlight Principle
• Tools and Algorithms for the Construction and Analysis of Systems
• Exact and efficient verification of parameterized cache coherence protocols
• The weakest deadlock-preserving congruence

Cited In (5)

• Safety, domain independence and generalized quantification
• Title not available (Why is that?)
• Compositional analysis for verification of parameterized systems
• Symmetry and Completeness in the Analysis of Parameterized Systems
• An automata-theoretic approach to the verification of distributed algorithms

Uses Software

• nauty

This page was built for publication: Multi-parameterised compositional verification of safety properties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q498394)