Incrementally Closing Octagons

摘要: The octagon abstract domain is a widely used numeric expressing relational information between variables whilst being both computationally efficient and simple to implement. Each element of the system constraints where each constraint takes restricted form $\pm x_i \pm x_j \leq d$. A key family operations for are closure algorithms, which check satisfiability provide normal octagonal systems. We present new quadratic incremental algorithms closure, strong integer proofs their correctness. highlight benefits measure performance these algorithms.