Automatically inferring loop invariants via algorithmic learning

DOI10.1017/S0960129513000078zbMath1361.68067OpenAlexW2167120274MaRDI QIDQ5740643

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

Mathematics Subject Classification ID

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

Related Items (1)

Invariant inference with provable complexity from the monotone theory

Uses Software

• Coq

Cites Work

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

This page was built for publication: Automatically inferring loop invariants via algorithmic learning