Generation of Violation Witnesses by Under-Approximating Abstract Interpretatio...

on YouTube ↗21m

" summary

Backwards abstract interpretation computes under-approximate sufficient preconditions, implemented as a proof-of-concept analyzer (~10k LOC) that uses a power-set of polyhedra to represent unions, a repeating-input stream abstraction to model user inputs, and a backward integer wrapping back-transfer to handle C integer semantics. The tool generates SV-COMP-style violation witnesses and is evaluated on an SV-COMP23 subset; results show lower analysis coverage than leading tools but notably fewer timeouts, and all reported witnesses validate with external validators.

AI-written summary · about

" chapters (12)

1. 0:00Violation witness generation
2. 1:27Abstract interpretation alarms
3. 2:55Backward analysis for alarms
4. 5:03Under-approximation foundations
5. 6:28Limitations of original approach
6. 7:37Analysis for program inputs
7. 9:50Union in under-approximation
8. 10:55Integer wrapping in polyhedra
9. 12:42Implementation proof of concept
10. 14:07SV-COMP benchmarks results
11. 15:33Future work challenges
12. 16:39Q&A