Automated inductive verification of parameterized protocols
From MaRDI portal
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
- An automatic proving approach to parameterized verification
- Program Development in Computational Logic
- ParaVerifier: an automatic framework for proving parameterized cache coherence protocols
- Transformational Verification of Parameterized Protocols Using Array Formulas
- Parameterized verification with automatically computed inductive assertions
Cited in
(16)- Automatic deductive verification with invisible invariants
- Model checking parameterized systems
- Parameterized Verification of Communicating Automata under Context Bounds
- ParaVerifier: an automatic framework for proving parameterized cache coherence protocols
- An automatic proving approach to parameterized verification
- Verification of parametrized systems by dynamic induction on diagrams
- Parametrized invariance for infinite state processes
- scientific article; zbMATH DE number 1418468 (Why is no real title available?)
- Automated Synthesis of Protocol Converters with BALM-II
- Transformational Verification of Parameterized Protocols Using Array Formulas
- Tools and Algorithms for the Construction and Analysis of Systems
- Verification by Parallelization of Parametric Code
- Verifying Parameterized taDOM+ Lock Managers
- Program Development in Computational Logic
- Using induction and rewriting to verify and complete parameterized specifications
- Feature interaction detection by pairwise analysis of LTL properties -- A case study
This page was built for publication: Automated inductive verification of parameterized protocols
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4551131)