SymInfer: Inferring Program Invariants using Symbolic States
This addresses the challenge of invariant generation for program verification, offering a novel approach that could improve automated analysis tools, though it appears incremental as it builds on existing symbolic execution and invariant inference methods.
The authors tackled the problem of automatically inferring program invariants by introducing SymInfer, a tool that uses symbolic states from symbolic execution to generate and verify invariants, with preliminary results showing it outperforms existing systems in precision and usefulness for safety and complexity analysis.
We introduce a new technique for inferring program invariants that uses symbolic states generated by symbolic execution. Symbolic states, which consist of path conditions and constraints on local variables, are a compact description of sets of concrete program states and they can be used for both invariant inference and invariant verification. Our technique uses a counterexample-based algorithm that creates concrete states from symbolic states, infers candidate invariants from concrete states, and then verifies or refutes candidate invariants using symbolic states. The refutation case produces concrete counterexamples that prevent spurious results and allow the technique to obtain more precise invariants. This process stops when the algorithm reaches a stable set of invariants. We present SymInfer, a tool that implements these ideas to automatically generate invariants at arbitrary locations in a Java program. The tool obtains symbolic states from Symbolic PathFinder and uses existing algorithms to infer complex (potentially nonlinear) numerical invariants. Our preliminary results show that SymInfer is effective in using symbolic states to generate precise and useful invariants for proving program safety and analyzing program runtime complexity. We also show that SymInfer outperforms existing invariant generation systems.