Multi-parameterised compositional verification of safety properties

DOI10.1016/J.IC.2015.08.002MaRDI QIDQ498394zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(5)

• Safety, domain independence and generalized quantification
• scientific article; zbMATH DE number 1956590 (Why is no real title available?)
• Compositional analysis for verification of parameterized systems
• An automata-theoretic approach to the verification of distributed algorithms
• Symmetry and Completeness in the Analysis of Parameterized Systems

Describes a project that uses

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)