# A Counterexample-guided Approach to Finding Numerical Invariants

arXiv: https://arxiv.org/abs/1903.12113 · HTML: https://mlsanity.com/paper/1903.12113/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Mar 2019.

## Built on by (most cited first, 3 of 3)

- [Invalidator: Automated Patch Correctness Assessment via Semantic and Syntactic Reasoning](https://mlsanity.com/paper/2301.01113/) (2023)
- [A Robust Optimisation Perspective on Counterexample-Guided Repair of Neural Networks](https://mlsanity.com/paper/2301.11342/) (2023)
- [Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning](https://mlsanity.com/paper/2305.01206/) (2023)

## Abstract (arXiv)

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.