Signature Inference for Functional Property Discovery
summary
Implements a tool called EasySpec that generates QuickSpec signatures from GHC metadata, runs QuickSpec repeatedly on tiny chunks of relevant functions, and unions results to recover properties much faster than a single global run. Claims are several orders of magnitude faster (examples: a 15‑function run that used to take minutes drops to seconds) and produces similar equations. Works on examples; practical gaps remain (C preprocessor, scoping, false positives require manual vetting).
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:16Types of testing
- 3:02QuickSpec
- 4:55EZSpec
- 6:01Generating Signature
- 9:25Relevant Properties
- 11:00Other Methods
- 12:21The Problem
- 13:02Questions
related talks
15mIronSpec: Increasing the Reliability of Formal Specifications
28mMaking property based testing easier
38mLiving with Spec
14mVerify, but test: extracting property-based tests from F* specifications
20mDerivative-Guided Symbolic Execution
17mTesting Specifications In Dafny
47mSpecs2, from starters to dessert and... a look in the kitchen.
28mLanguage Support for Property-Based Testing
