Deductive verification in decidable fragments with Ivy

DOI10.1007/978-3-319-99725-4_4MaRDI QIDQ6041167zbMATH OpenFDO

Authors K. L. McMillan, Oded Padon

Publication date 26 May 2023

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-99725-4_4

zbMATH Keywords

cache coherencedecidable logicsdeductive verificationdistributed systemseffectively propositional logicliveness verificationmodel checkingPaxossafety verificationspecification-based testing

Mathematics Subject Classification ID

Logic in computer science (03B70) Distributed systems (68M14) 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

• Verifying programs in the calculus of inductive constructions
• Decidability of parameterized verification
• Loop-free verification of termination of derivation for a fragment of dynamic logic
• Verification from Declarative Specifications Using Logic Programming
• \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages
• scientific article; zbMATH DE number 1722694
• scientific article; zbMATH DE number 1701752
• Assertion based inductive verification methods for logic programs

Cited in

(6)

• Temporal prophecy for proving temporal properties of infinite-state systems
• Stratified guarded first-order transition systems
• scientific article; zbMATH DE number 1614710 (Why is no real title available?)
• Tight polynomial worst-case bounds for loop programs
• What's decidable about program verification modulo axioms?
• Stratified guarded first-order transition systems

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

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