Deductive verification in decidable fragments with Ivy

DOI10.1007/978-3-319-99725-4_4zbMath1511.68165MaRDI QIDQ6041167

Oded Padon, K. L. McMillan

Publication date: 26 May 2023

Published in: Static Analysis (Search for Journal in Brave)

zbMATH Keywords

distributed systemsmodel checkingsafety verificationcache coherencedeductive verificationspecification-based testingPaxoseffectively propositional logicdecidable logicsliveness verification

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Distributed systems (68M14)

Related Items (4)

Stratified guarded first-order transition systems ⋮ What’s Decidable About Program Verification Modulo Axioms? ⋮ Unnamed Item ⋮ Temporal prophecy for proving temporal properties of infinite-state systems

This page was built for publication: Deductive verification in decidable fragments with Ivy