  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.
