Decidability of inferring inductive invariants
DOI10.1145/2837614.2837640zbMATH Open1347.68234OpenAlexW2296031223MaRDI QIDQ2828258FDOQ2828258
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
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
Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70)
Cited In (15)
- Title not available (Why is that?)
- When Is Reachability Intrinsically Decidable?
- Inferring inductive invariants from phase structures
- Stratified guarded first-order transition systems
- On invariant synthesis for parametric systems
- On the decidability of the existence of polyhedral invariants in transition systems
- Title not available (Why is that?)
- Invariant Checking for Programs with Procedure Calls
- Invariant inference with provable complexity from the monotone theory
- Title not available (Why is that?)
- Invariant checking for SMT-based systems with quantifiers
- Deciding the Inductive Validity of ∀ ∃ * Queries
- On the Monniaux problem in abstract interpretation
- Title not available (Why is that?)
- What's decidable about program verification modulo axioms?
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)
