Synthesizing History and Prophecy Variables for Symbolic Model Checking

on YouTube ↗32m

" summary

Presents an automated CEGAR pipeline that introduces prophecy and history variables to remove universal quantifiers over arrays, using counterexample-guided heuristics and Craig interpolation to mine axiom instantiations and loop points. Implements a ~3000-line Python prototype called contest that hooks into IC3IA, evaluates on single- and multi-loop array benchmarks, and reports solving more cases than freck_horn, Q3 and g-spacer; about 30% of solved instances need auxiliary variables and the refinement strategy is the key practical win.

AI-written summary · about

" chapters (24)

1. 0:00Intro
2. 0:37Motivation
3. 1:08Motivating Example
4. 3:35Approach
5. 3:47High-Level Overview
6. 4:45Refinement Generator
7. 5:23Refinement Definition
8. 6:53Auxiliary Variables
9. 7:46Array Scattering Example (cont.)
10. 8:19Array Scattering Trace 1
11. 9:06Instantiating Axiom Instance 1
12. 10:48Array Scattering Trace 2
13. 11:23Instantiating Axiom Instance 2
14. 14:13Solved Array Scattering Example
15. 14:34Symbolic Array Scattering Trace
16. 15:16A More Complex Example
17. 16:24Array Summing Trace
18. 17:09History Condition
19. 18:21Array Summing Solved
20. 19:16Implementation
21. 20:33Full Refinement
22. 22:15Evaluation
23. 23:45Results (Freqhorn Benchmarks)
24. 25:46Future Work