The Daikon dynamic invariant detector uses machine learning to infer likely program invariants and properties. The types of properties inferred by Daikon include “.field > abs(y)”; “y = 2*x+3”; “array a is sorted”; “for all list objects lst, lst.next.prev = lst”; “for all treenode objects n, n.left.value < n.right.value”; “p != null ⇒ p.content in myArray”; and many more.
This project, Celeriac, dynamically instruments a .NET application to produce a Daikon-compatible program trace. Celeriac works directly on binaries, and therefore does not require build modifications.
To start using Celeriac, visit the Getting Started wiki page.
Binaries are available via AppVeyor.