An Automatic Proving Approach to Parameterized Verification

DOI10.1145/3232164zbMath1407.68295OpenAlexW2902518441MaRDI QIDQ4617972

Jun Pang, Yongjian Li, Yi Lv, David N. Jansen, Shaowei Cai, Kaiqiang Duan, Li-jun Zhang

Publication date: 7 February 2019

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: http://orbilu.uni.lu/handle/10993/37865

zbMATH Keywords

theorem provingautomatic verificationinductive methodscache coherence protocolsinvariant and proof generation

Mathematics Subject Classification ID

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

Related Items (2)

Verification of SMT systems with quantifiers ⋮ Universal invariant checking of parametric systems with quantifier-free SMT reasoning

Uses Software

• Isabelle
• Isabelle/HOL
• ParaVerifier
• Cubicle

This page was built for publication: An Automatic Proving Approach to Parameterized Verification