Template-Free Dynamic Invariant Detection

Erfan Arvan, Michael D. Ernst, Martin Kellogg

A dynamic invariant detector proposes invariants, such as method pre- and postconditions, and rules out those that do not hold at run time. Traditional detectors propose invariants from a fixed library of templates, which limits their expressiveness. A large language model (LLM) can propose invariants instead of, or in addition to, template-derived ones. With the right prompt and context choices, we found that this idea can both improve the invariants' expressiveness and reduce the cost of inferring the invariants. Greater expressiveness brings complications: an LLM-proposed invariant can execute arbitrary code during invariant evaluation, causing side effects or infinite loops. Our novel instrumentation strategies mitigate these problems. We wrap each candidate and evaluate only one invariant per thread at a time, so nested invariant evaluations cannot trigger one another indefinitely. To recover from non-nested hangs, we monitor each run for stalls and retry it under a growing time budget. Because we cannot prove a candidate side-effect-free in advance, we use delta debugging over the invariants evaluated during a failing test to isolate and disable a side-effecting candidate…