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

effectively propositional logicinvariant inferenceverificationwell-quasi-order

Mathematics Subject Classification ID

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

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

(16)

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

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)