Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference

DOI10.1007/978-3-642-19835-9_17zbMath1315.68097arXiv1207.7167OpenAlexW2099316895MaRDI QIDQ5892496

Kwangkeun Yi, Wonchan Lee, Bow-Yaw Wang, Yungbum Jung

Publication date: 19 May 2011

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1207.7167

Mathematics Subject Classification ID

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

Related Items

Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF ⋮ NIL: learning nonlinear interpolants

Uses Software

• Yices
• CSIsat
• FOCI

Cites Work

• Unnamed Item
• Learning regular sets from queries and counterexamples
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Exact learning Boolean functions via the monotone theory
• An interpolating theorem prover
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Abstractions from proofs
• Interpolant Strength
• Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction
• Array Abstractions from Proofs
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• Lazy Abstraction with Interpolants
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems