An invariant-based approach to the verification of asynchronous parameterized networks

DOI10.1016/J.JSC.2008.11.006MaRDI QIDQ604385zbMATHOpenAlexFDO

Authors Sumit K. Garg

Publication date 10 November 2010

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jsc.2008.11.006

zbMATH Keywords

simulationmodel checkinginductionprogram verificationinvariant generationasynchronous networks

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification of parameterized protocols
• Automatic verification of parameterized networks of processes
• scientific article; zbMATH DE number 1232244
• Inferring Network Invariants Automatically
• scientific article; zbMATH DE number 1670786

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1693448 (Why is no real title available?)
• scientific article; zbMATH DE number 1232244 (Why is no real title available?)
• scientific article; zbMATH DE number 1032897 (Why is no real title available?)
• scientific article; zbMATH DE number 1982210 (Why is no real title available?)
• scientific article; zbMATH DE number 1515293 (Why is no real title available?)
• scientific article; zbMATH DE number 1746449 (Why is no real title available?)
• scientific article; zbMATH DE number 1754630 (Why is no real title available?)
• A minimized automaton representation of reachable states
• A structural induction theorem for processes
• An approach to the verification of symmetric parameterized distributed systems
• CONCUR 2004 - Concurrency Theory
• Characterizing finite Kripke structures in propositional temporal logic
• Computer Science Logic
• Equivalence and preorder checking for finite-state systems
• Exact and efficient verification of parameterized cache coherence protocols
• FM 2005: Formal Methods
• On Reasoning About Rings
• Reasoning about systems with many processes
• Verification by augmented finitary abstraction

Cited in

(3)

• Game-theoretic simulation checking tool
• Weak Invariant Simulation and Its Application to Analysis of Parameterized Networks
• Parameterised verification of publish/subscribe networks with exception handling

Describes a project that uses

Uses Software

• BLAST
• SPIN

This page was built for publication: An invariant-based approach to the verification of asynchronous parameterized networks

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