Automatically inferring loop invariants via algorithmic learning
DOI10.1017/S0960129513000078zbMATH Open1361.68067OpenAlexW2167120274MaRDI QIDQ5740643FDOQ5740643
Authors: Yungbum Jung, Soonho Kong, Cristina David, 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
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
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 (10)
- Inferring Loop Invariants Using Postconditions
- Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction
- Efficiently learning safety proofs from appearance as well as behaviours
- Automatic generation of non-linear loop invariants
- Mechanical inference of invariants for FOR-loops
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- Invariant inference with provable complexity from the monotone theory
- Programming Languages and Systems
- \textsc{Sorcar}: property-driven algorithms for learning conjunctive invariants
- Predicate generation for learning-based quantifier-free loop invariant inference
Uses Software
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)
