Characterizing the Typical Case Complexity of Formal Verification and Synthesis

on YouTube ↗51m

" summary

Three research threads: graph-based SAT structure, SMT encodings, and invariant synthesis. Shows that common modularity metrics can be embedded to make SAT instances NP-hard for PCM and that a community-attachment random model yields an exponential resolution lower bound for CDCL when communities are small (≤ n^0.1). For SMT, identifies heavy use of difference‑bounds and octagons and small‑domain encodings that explain practical solvability. For learning invariants, gives a combinatorial bound — teaching dimension 2d + 2d^2 for octagon templates — explaining why few tests suffice.

AI-written summary · about

" chapters (16)

1. 0:00Intro
2. 2:04Industrial Use of Formal Verification
3. 6:10Toy Example
4. 9:20Topics Covered in this Talk: "Typical-Case" Structure in Three Steps of the Verification Process
5. 11:13Community Structure
6. 17:57Graph-related Definitions
7. 19:09Modularity
8. 23:03Generalized Reduction
9. 24:11Polynomial Clique Metrics
10. 29:17Community Attachment Model
11. 36:22Integer Linear Arithmetic (LIA)
12. 39:39Special Case 1: Equality Logic
13. 44:34Invariant Synthesis
14. 46:00Teaching a 2-dimensional Box
15. 47:17Theorem: TDC is lower bound on number of tests for invariant inference
16. 47:54Teaching Dimension of Octagons