Proofs as Relational Invariants of Synthesized Execution Grammars

Caleb Voss, David Heath, William Harris

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 synt…