Compositional analysis for verification of parameterized systems

DOI10.1016/J.TCS.2005.11.016MaRDI QIDQ2368952zbMATH OpenOpenAlexFDO

Authors Samik Basu, C. R. Ramakrishnan

Publication date 28 April 2006

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2005.11.016

zbMATH Keywords

AccelerationCompositional model checkingFormula equivalenceParameterized systemsWidening

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

• scientific article; zbMATH DE number 1956590
• Multi-parameterised compositional verification of safety properties
• Tools and Algorithms for the Construction and Analysis of Systems
• Parameterized compositional model checking
• Model checking and abstraction to the aid of parameterized systems (a survey)

Cites work

• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Automatic verification of parameterized networks of processes
• Control and data abstraction: The cornerstones of practical formal verification
• Grammar Analysis and Parsing by Abstract Interpretation
• scientific article; zbMATH DE number 1670768 (Why is no real title available?)
• scientific article; zbMATH DE number 1670786 (Why is no real title available?)
• scientific article; zbMATH DE number 1701752 (Why is no real title available?)
• scientific article; zbMATH DE number 1701757 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1956591 (Why is no real title available?)
• scientific article; zbMATH DE number 1796136 (Why is no real title available?)
• scientific article; zbMATH DE number 1392309 (Why is no real title available?)
• scientific article; zbMATH DE number 1406234 (Why is no real title available?)
• Modal logics and mu-calculi: An introduction
• On Reasoning About Rings
• Parameterized verification of linear networks using automata as invariants
• Results on the propositional \(\mu\)-calculus
• The Complexity of Tree Automata and Logics of Programs
• Thread-modular abstraction refinement.
• Type analysis of prolog using type graphs

Cited in

(15)

• Partial specifications and compositional verification
• A compositional approach to the verification of hybrid systems
• Compositional analysis of C/C++ programs with veriSoft
• A framework for compositional verification of multi-valued systems via abstraction-refinement
• Keeping a crowd safe: on the complexity of parameterized verification (invited talk)
• REACHABILITY ANALYSIS IN VERIFICATION VIA SUPERCOMPILATION
• scientific article; zbMATH DE number 1956590 (Why is no real title available?)
• scientific article; zbMATH DE number 1487866 (Why is no real title available?)
• Compositionality in state space verification methods
• scientific article; zbMATH DE number 1418468 (Why is no real title available?)
• Multi-parameterised compositional verification of safety properties
• Symmetry and Completeness in the Analysis of Parameterized Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Compositional reasoning for parametric probabilistic automata
• An automatic abstraction technique for verifying featured, parameterised systems

Describes a project that uses

Uses Software

• CESAR
• SPIN

This page was built for publication: Compositional analysis for verification of parameterized systems

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