Template-Free Dynamic Invariant Detection

Dynamic invariant detectors such as Daikon infer likely program invariants by evaluating candidate properties against execution traces. However, Daikon’s candidates are drawn from a fixed template library, which prevents it from expressing properties that involve project-specific logic or more than three variables. We present Oca, a dynamic invariant detector that uses a large language model (LLM) to propose candidates instead of deriving them from templates. LLM-proposed invariants are more expressive, but their integration into a dynamic analysis pipeline raises non-trivial research challenges involving prompt design, context selection, and safe execution of untrusted candidates. We address these challenges and evaluate Oca on the Defects4J benchmark, showing that it infers invariants beyond Daikon’s expressive reach, with ongoing evaluation of their bug-detection capability in property-based testing.