DIG is a numerical invariant generation tool. It infers program invariants or properties over (i) program execution traces or (ii) program source code. DIG supports many forms of numerical invariants, including nonlinear equalities, octagonal and interval properties, min/max-plus relations, and congruence relations.
I pushed the ocaml script for instrumentation.
To run it use command:
./verify.exe
is the source code
is the file to save to
is the location of the invariant. In this case I just used the suffix of vtrace method. for example. vtrace1() loc wold be 1. Note: if there is only one vtrace() method loc is 0
is the invariant to verify
I noticed that Utlimate takes very long to prove properties and I wonder if we can try to disprove the opposite instead because I think it is faster to find counterexamples than proofs. For example, for a property P we can instead instrument the code to verify Not P which would be faster since Not P would have counterexamples.
I pushed the ocaml script for instrumentation. To run it use command: ./verify.exe