Symbolic transformation of expressions in modular arithmetic
summary
Formal rewriting rules convert modular integer expressions into sums products or quotients of linear forms with integer coefficients and prove soundness and termination via a deterministic inference system with 30+ rewrite rules. A new convex join operator represents nondeterminism with relational bounds. Methods are implemented in Astrée and a toy analyzer and they successfully expose patterns like linear and bilinear interpolation to interval or octagon domains while sometimes trading precision depending on what underlying domain already captures.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 0:25Motivation
- 1:30Implicit modular in C
- 2:36Modular syntax
- 4:01Rewriting programs
- 5:06Proving properties
- 6:55Simplifying expressions
- 9:05Soundness of rewriting
- 10:12Handling errors
- 12:00Pattern recognition
- 12:22Linear interpolation
- 13:45Convex join operator
- 15:36Bilinear interpolation
- 17:45Implementation details
- 18:47Conclusion
- 19:11Q&A