Constraint Based Invariant Generation with Modular Operations
摘要
Invariant generation is a fundamental problem in program verification that targets the automated generation of invariants that capture the set of reachable program states. Modular operations that calculate the remainder of an integer variable against a divisor are common in programs, and therefore the generation of invariants with modular information is indispensible for proving the correctness of such programs. In this paper, we propose a novel approach for generating affine invariants with modular information via constraint solving. Our approach first transforms affine programs with modular operations into affine transition systems, and then applies existing approaches in Farkas’ Lemma to solve the invariants. Experimental results over a suite of benchmarks that involve complex modular operations show that our approach is time efficient and can generate tight or even accurate linear invariants with modular information.