Polynomial Analysis of Modular Arithmetic

on YouTube ↗38m

" summary

Proposes the modular polynomial abstract domain (MPAD) whose invariants are polynomial equations modulo 2^k, implements closure via coverings, Groebner bases and null polynomials, and reduces negative guards to positive ones by shifting bits. MPAD satisfies the ascending chain condition, so an SMT-guided iterative algorithm computes best transformer via SMT loop for low bitwidths; prototype handles up to 32-bit examples in under a second on the showcased inverse and bitwise-and cases.

AI-written summary · about

" chapters (16)

1. 0:00Modular arithmetic analysis
2. 1:14Hacker's Delight motivation
3. 2:59Modular arithmetic history
4. 4:05Negative guards challenges
5. 6:33Polynomial systems richness
6. 8:00Microcontroller analysis
7. 10:11Transformer via SAT solvers
8. 12:16Abstract domain construction
9. 15:48Groebner bases for systems
10. 17:14Program operations analysis
11. 18:18Groebner basis fundamentals
12. 21:49Covering operation
13. 25:50Null polynomials
14. 29:19Handling assumptions
15. 31:09Contributions and future work
16. 32:34Q&A