A Counterexample-guided Approach to Finding Numerical Invariants

TL;DR

NumInv is a tool that automatically discovers polynomial numerical invariants in programs using a counterexample-guided approach, aiding program analysis and verification, especially for complex arithmetic and complexity bounds.

Contribution

It introduces a novel CEGIR-based method that sacrifices soundness for practical invariant discovery, leveraging KLEE for dynamic verification and outperforming existing tools.

Findings

NumInv successfully finds invariants for complex arithmetic programs.

It captures precise complexity bounds in benchmark programs.

NumInv performs competitively with state-of-the-art tools.

Abstract

Numerical invariants, e.g., relationships among numerical variables in a program, represent a useful class of properties to analyze programs. General polynomial invariants represent more complex numerical relations, but they are often required in many scientific and engineering applications. We present NumInv, a tool that implements a counterexample-guided invariant generation (CEGIR) technique to automatically discover numerical invariants, which are polynomial equality and inequality relations among numerical variables. This CEGIR technique infers candidate invariants from program traces and then checks them against the program source code using the KLEE test-input generation tool. If the invariants are incorrect KLEE returns counterexample traces, which help the dynamic inference obtain better results. Existing CEGIR approaches often require sound invariants, however NumInv sacrifices soundness and produces results that KLEE cannot refute within certain time bounds. This design and the use of KLEE as a verifier allow NumInv to discover useful and important numerical invariants for many challenging programs. Preliminary results show that NumInv generates required invariants for understanding and verifying correctness of programs involving complex arithmetic. We also show that NumInv discovers polynomial invariants that capture precise complexity bounds of programs used to benchmark existing static complexity analysis techniques. Finally, we show that NumInv performs competitively comparing to state of the art numerical invariant analysis tools.