Local symmetry and compositional verification

DOI10.1007/978-3-642-27940-9_23MaRDI QIDQ2891426zbMATH OpenOpenAlexFDO

Authors Kedar S. Namjoshi, Richard Trefler

Publication date 15 June 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-27940-9_23

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) 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

• Symmetry reduction for the local mu-calculus
• Uncovering symmetries in irregular process networks
• scientific article; zbMATH DE number 1796126
• scientific article; zbMATH DE number 1487862
• Extending symmetry reduction techniques to a realistic model of computation

Cites work

• Concurrency verification. Introduction to compositional and noncompositional methods
• From Groups to Groupoids: a Brief Survey
• Groupoids: unifying internal and external symmetry. A tour through some examples.
• scientific article; zbMATH DE number 1956591 (Why is no real title available?)
• scientific article; zbMATH DE number 1973986 (Why is no real title available?)
• scientific article; zbMATH DE number 1982207 (Why is no real title available?)
• scientific article; zbMATH DE number 1796136 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• Local proofs for global safety properties
• Local Proofs for Global Safety Properties
• Local Proofs for Linear-Time Properties of Concurrent Programs
• Nonlinear dynamics of networks: the groupoid formalism
• On Reasoning About Rings
• On the completeness of compositional reasoning methods
• Predicate abstraction and refinement for verifying multi-threaded programs
• Proofs of Networks of Processes
• Proving the Correctness of Multiprocess Programs
• Symmetry and Completeness in the Analysis of Parameterized Systems
• Tentative steps toward a development method for interfering programs
• The ``Hoare Logic of CSP, and All That
• Verifying properties of parallel programs

Cited in

(10)

• Local proofs for global safety properties
• Symmetry reduction for the local mu-calculus
• Unifying Local and Nonlocal Modelling of Respective and Symmetrical Predicates
• Uncovering symmetries in irregular process networks
• Compositional reasoning
• A scheme for symmetrization verification
• Local Proofs for Global Safety Properties
• Correct Hardware Design and Verification Methods
• Cut-off theorems for the \textit{PV}-model
• Choose your proofs: commutativity and symmetry for smarter reasoning

This page was built for publication: Local symmetry and compositional verification

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