Data-Driven Abductive Inference of Library Specifications
summary
Tool named Elrond infers specifications for black‑box OCaml libraries by combining random testing, SMT counterexample-guided refinement, and an abduction loop; it produces minimal “maximal” specs that enable client verification and the team verifies all results manually in Coq. The pipeline runs on 27 benchmarks, completes inference and strengthening within minutes and finishes abduction for 87% of safe clients within a one‑hour bound, reporting learned predicates like hd and mem.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:14Verifying Clients of a Library
- 3:49Data-Driven Specification Inference
- 6:47Elrond Pipeline Specifications are too overapproximate to prove the client assertions...
- 6:59Overapproximation Example
- 8:12Overcoming Overapproximation: Strengthening
- 9:34Elrond Pipeline Specifications could be too overfitted to be consistent with the black box library implementation.
- 9:44Overfitting Example
- 11:03Overcoming Overfitting: Abduction
- 11:45Overcoming Overfitting: Data-Driven Abduction
- 12:24Evaluation
- 13:52Conclusion Problem: how to infer specifications for block box library implementations to enable verification involving rich datatypes?
related talks
36mSpecification-Guided Component-Based Synthesis from Effectful Libraries
23mSpecifying and Verifying Future Conditions
18mInference of Resource Management Specifications
20mOn Extending Incorrectness Logic with Backwards Reasoning
20mAutomatic and Incremental Repair for Speculative Information Leaks
21mExact Loop Bound Analysis
14mQuantified Underapproximation via Labeled Bunches
14mSynthesizing Implication Lemmas for Interactive Theorem Proving