DIG: Dynamic Invariant Generator

DIG infers program invariants — nonlinear/linear equalities, octagonal inequalities, congruences, and min/max-plus relations — from program code or execution traces. [GitHub] [ROARS Lab]

1. Program input

Load example:

Input type: C program (annotated with vtraceX(...)) CSV traces

2. Options

(optional — click to configure DIG; defaults are used otherwise)

Numeric parameters (leave blank for DIG defaults)

`-maxdeg`		find nonlinear invariants up to this degree
`-maxterm`		autodegree (max number of terms)
`-ideg`		degree for inequalities (1 = linear, 2 = quadratic, ...)
`-iterms`		number of terms for inequalities (2 = octagonal)
`-icoefs`		coefficients for inequalities (1 = [-1,0,1], i.e., oct)
`-iupper`		max upperbound value for inequalities
`-se_maxdepth`		depth limit of symbolic execution
`-nrandinps`		number of random inputs (only with `-noss`)
`-inpMaxV`		max input value
`-seed`		random seed (for reproducibility)
`-log_level`		logger verbosity (0 = error ... 4 = detail)
timeout (s)		wall-clock limit enforced by the web runner (max 300)

Disable / debugging flags -noeqts don't compute equality invariants
-noieqs don't compute inequality/octagonal invariants
-nocongruences don't compute congruence invariants
-noarrays don't compute array relations
-nominmaxplus don't compute min/max-plus invariants
-noss don't use symbolic states (dynamic analysis only)
-noincrdepth don't use incremental depth
-nosimplify don't simplify/remove weaker invariants (debugging)
-nofilter don't filter inequality terms (debugging)
-nomp don't use multiprocessing
-dosolverstats collect solver statistics

Terms / LLM -uterms user-supplied terms, separated by ;
-llm use an LLM to propose invariants, verified by symbolic states + z3 (server needs ANTHROPIC_API_KEY)
-llm_rounds max LLM propose/verify rounds
-llm_no_traces LLM prompt with source only, no concrete traces

Ready.

3. Discovered invariants

(no results yet)

4. Raw execution output

(waiting for execution output)

DIG · ROARS Lab · George Mason University