SymInfer: Inferring Program Invariants using Symbolic States

TL;DR

SymInfer is a novel technique that leverages symbolic execution to automatically infer precise program invariants, improving safety verification and complexity analysis over existing methods.

Contribution

The paper introduces SymInfer, a new invariant inference approach using symbolic states and counterexample-based refinement, outperforming prior systems.

Findings

Effective in generating precise invariants for safety proofs.

Outperforms existing invariant generation systems.

Applicable to complex numerical invariants in Java programs.

Abstract

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.