← All papers
A Formal Foundation for Symbolic Evaluation with Merging
cs.LO
Jan 12, 2022 · v1
TL;DR
Uses Lean to formally verify the correctness of symbolic evaluation with state merging in Rosette.
Abstract
This paper presents a formal foundation for symbolic evaluation with state merging, as used in tools like Rosette. The authors develop a semantics for symbolic evaluation that supports path merging and prove its correctness. The formalization uses the Lean theorem prover to establish that the symbolic evaluator faithfully represents all concrete executions of a program.
Problem
Symbolic evaluation with state merging (as used in tools like Rosette) lacks a formal semantics with proven correctness guarantees that the symbolic evaluator faithfully represents all concrete executions.
Approach
The authors develop a formal semantics for symbolic evaluation that supports path merging and prove its correctness using the Lean theorem prover. The formalization establishes that the symbolic evaluator faithfully represents all concrete executions of a program.
Results
A verified formal foundation for symbolic evaluation with merging is established in Lean, proving that path-merged symbolic execution is sound with respect to concrete execution semantics.