Title: Proofs as Relational Invariants of Synthesized Execution Grammars,
Abstract: The automatic verification of programs that maintain unbounded low-level data
structures is a critical and open problem. Analyzers and verifiers developed in
previous work can synthesize invariants that only describe data structures of
heavily restricted forms, or require an analyst to provide predicates over
program data and structure that are used in a synthesized proof of correctness.
In this work, we introduce a novel automatic safety verifier of programs that
maintain low-level data structures, named LTTP. LTTP synthesizes proofs of
program safety represented as a grammar of a given program's control paths,
annotated with invariants that relate program state at distinct points within
its path of execution. LTTP synthesizes such proofs completely automatically,
using a novel inductive-synthesis algorithm.
We have implemented LTTP as a verifier for JVM bytecode and applied it to
verify the safety of a collection of verification benchmarks. Our results
demonstrate that LTTP can be applied to automatically verify the safety of
programs that are beyond the scope of previously-developed verifiers.