Certifying the Synthesis of Heap-Manipulating Programs
summary
Method translates SuSLik synthesis traces into machine-checkable Coq proofs and produces three certifiers for HTT, Iris and VST, evaluated on 15 benchmarks. Technique relies on SuSLik emitting deductive traces plus two mechanisms—deferred proof steps to reorder postcondition-changing inferences and a proof context accumulator to record existential unifications. Generated proofs are typically under 100 lines; most Coq check times are 2–20s (VST proofs sometimes approach a minute). Certification is fully automated for the benchmark suite.
AI-written summary · about