Higher-Order MSL Horn Constraints
summary
Extends MSL to higher-order Horn constraints and gives a resolution-based decision procedure that preserves decidable satisfiability by introducing nested higher-order atomic constraints to avoid unbounded head instantiation; proves higher-order MSL satisfiability is interreducible with HORS model checking; builds a Haskell prototype applied to verified socket programming as a proof of concept that the procedure works on real verification patterns.
AI-written summary · about
chapters (8)
- 0:00Higher-order MSL Horn intro
- 2:30MSL Horn in verification
- 7:13Satisfiability with automaton resolution
- 9:06MSL to higher-order logic
- 14:07Higher-order automaton in action
- 17:16Intersection types and automata
- 19:00Higher-order logic foundation
- 20:25Q&A
related talks
38mConstrained Horn Clauses Satisfiability via Catamorphic Abstractions
21mBoosting Constrained Horn Solving by Unsat Core Learning
27mCompiling higher-order specifications to SMT solvers: how to deal with rejection ...
28mHigher-Order Property-Directed Reachability
20mA Hierarchy of Supermartingales for ω-Regular Verification
29mADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
30mSemantics-Guided Synthesis
15mHACCLE: Metaprogramming for Secure Multi-Party Computation