Plan

Read Recent Sym Exec Soundness Works

symbolic execution soundness proof

Another recent

Why3 soundness (same session with VST-A)