Compiling higher-order specifications to SMT solvers: how to deal with rejection ...
summary
Claims a verified pipeline that compiles higher-order Vehicle specifications to SMT while giving pinpointed rejections, implemented for Marabou-style backends and formalized in Agda. It uses type-class resolution plus implicit linearity and polarity annotations to detect unsupported features (nonlinearities, mixed quantifiers, nested higher-order uses), records provenance annotations to locate offending source constructs, and performs codegen via normalization by evaluation that separates linear constraints, ifs and uninterpreted functions into SMT-friendly formulas.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:44Vehicle language motivation
- 4:55Challenges in SMT translation
- 9:08Target language design
- 16:32Handling rejection
- 18:18Normalization by evaluation
- 22:28Conclusion
- 23:57Q&A
related talks
22mCounterexample-Guided Inference of Modular Specifications
35mThe Mastermind behind Refinement Types
30mAnalyzing Programs with SMT Solvers
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
19mAutomated Verification of Fundamental Algebraic Laws
46mRefinement Types from Light to Deep Verification
15mClosing Remarks