Decidability of inferring inductive invariants

DOI10.1145/2837614.2837640MaRDI QIDQ2828258zbMATH OpenOpenAlexFDO

Authors Oded Padon, Sharon Shoham, Mooly Sagiv, Aleksandr Karbyshev, Neil Immerman

Publication date 24 October 2016

Published in Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2837614.2837640

zbMATH Keywords

verificationwell-quasi-ordereffectively propositional logicinvariant inference

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70)

Recommendations

• Property-directed inference of universal invariants or proving their absence
• scientific article; zbMATH DE number 1956575
• Computer Aided Verification
• Property-directed inference of universal invariants or proving their absence
• On the decidability of the existence of polyhedral invariants in transition systems

Cited in

(15)

• scientific article; zbMATH DE number 1395882 (Why is no real title available?)
• What's decidable about program verification modulo axioms?
• scientific article; zbMATH DE number 4187777 (Why is no real title available?)
• When Is Reachability Intrinsically Decidable?
• Stratified guarded first-order transition systems
• Inferring inductive invariants from phase structures
• On invariant synthesis for parametric systems
• On the decidability of the existence of polyhedral invariants in transition systems
• scientific article; zbMATH DE number 1956575 (Why is no real title available?)
• Invariant Checking for Programs with Procedure Calls
• Invariant inference with provable complexity from the monotone theory
• scientific article; zbMATH DE number 7559486 (Why is no real title available?)
• Invariant checking for SMT-based systems with quantifiers
• Deciding the Inductive Validity of ∀ ∃ * Queries
• On the Monniaux problem in abstract interpretation

This page was built for publication: Decidability of inferring inductive invariants

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