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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Constraint Based Invariant Generation with Modular Operations

  • Yuchen Li,
  • Hongfei Fu,
  • Haowen Long,
  • Guoqiang Li

摘要

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.