A Simple Runtime Invariant Miner
9 points by vrthra
9 points by vrthra
This post provides a tutorial of the Daikon framework for inferring dynamic invariants from program execution. Daikon is the dynamic dual of static analysis for invariant inference, and is /a/ whitebox dual of blackbox specification inference.
This is part of my ongoing effort to document various algorithms relating to static and dynamic analysis as well as blackbox and whitebox testing.
I am looking for feedback on structure as well as content as before. The content is oriented toward software engineering students who typically know about basic software development, and some formalism. The implementation prioritizes clarity over speed.
Note: Pyodide takes a little time to initialize, but it should be faster to initialize than spinning up the binder service from Jupyter (but slower to execute).
Really epic content. I don't have time to review it at the moment, but I've bookmarked the thread to come back to it later as this is something I've been meaning to learn regardless. Thanks for putting this together.
I’ve “written” two systems like this in the past 6 months… and where I continue to get stuck is that most software doesn’t have interesting invariants that can be discovered this way. I got stuck.
In both cases, I integrated contracts and tracing with invariant inference into Go. It “works” but it just isn’t compelling for any code bases I’m working on. Very unfortunate. :(
I agree; On its own, it is not very useful. Finding useful invariants that holds across all valid executions of a system, while flagging invalid executions is difficult. What I would suggest is to use a template based input generator in conjunction. i.e. Something that will let you exercise a specific behaviour of the system. Then combine that with other behaviours and find how many of the captured invariants gets violated. This can give you a better signal for buggy executions.