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

Mathematics Subject Classification ID

Computational learning theory (68Q32) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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

Cites work

• Array Abstractions from Proofs
• Automated Assumption Generation for Compositional Verification
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Constraint-Based Invariant Inference over Predicate Abstraction
• Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction
• Exact learning Boolean functions via the monotone theory
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Learning Minimal Separating DFA’s for Compositional Verification

Cited in

(10)

• Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
• Efficiently learning safety proofs from appearance as well as behaviours
• Inferring Loop Invariants Using Postconditions
• Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction
• Predicate generation for learning-based quantifier-free loop invariant inference
• Automatic generation of non-linear loop invariants
• Mechanical inference of invariants for FOR-loops
• \textsc{Sorcar}: property-driven algorithms for learning conjunctive invariants
• Invariant inference with provable complexity from the monotone theory
• Programming Languages and Systems

Describes a project that uses

Uses Software

• Coq

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)