Automatically inferring loop invariants via algorithmic learning
DOI10.1017/S0960129513000078zbMATH Open1361.68067OpenAlexW2167120274MaRDI QIDQ5740643FDOQ5740643
Soonho Kong, Cristina David, Yungbum Jung, Bow-Yaw Wang, Kwangkeun Yi
Publication date: 27 July 2016
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129513000078
Computational learning theory (68Q32) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Learning Minimal Separating DFA’s for Compositional Verification
- Exact learning Boolean functions via the monotone theory
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Array Abstractions from Proofs
- Constraint-Based Invariant Inference over Predicate Abstraction
- Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction
- Automated Assumption Generation for Compositional Verification
Cited In (5)
- Inferring Loop Invariants Using Postconditions
- Efficiently learning safety proofs from appearance as well as behaviours
- Automatic generation of non-linear loop invariants
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- Invariant inference with provable complexity from the monotone theory
Uses Software
Recommendations
- Automatic generation of non-linear loop invariants 👍 👎
- Inferring Loop Invariants Using Postconditions 👍 👎
- Mechanical inference of invariants for FOR-loops 👍 👎
- A data driven approach for algebraic loop invariants 👍 👎
- An iterative method for generating loop invariants 👍 👎
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference 👍 👎
- Predicate generation for learning-based quantifier-free loop invariant inference 👍 👎
- Ilinva: using abduction to generate loop invariants 👍 👎
This page was built for publication: Automatically inferring loop invariants via algorithmic learning
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5740643)
