SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Thu 8 Dec 2022 15:30 - 16:00 at Seminar Room LG004 - ICFP Papers Chair(s): Matthieu Lemerre

Automated deductive program synthesis promises to generate executable programs from concise specifications, along with proofs of correctness that can be independently verified using third-party tools. However, an attempt to exercise this promise using existing proof-certification frameworks reveals significant discrepancies in how proof derivations are structured for two different purposes: program synthesis and program verification. These discrepancies make it difficult to use certified verifiers to validate synthesis results, forcing one to write an ad-hoc translation procedure from synthesis proofs to correctness proofs for each verification backend.

In this work, we address this challenge in the context of the synthesis and verification of heap-manipulating programs. We present a technique for principled translation of deductive synthesis derivations (a.k.a. source proofs) into deductive target proofs about the synthesised programs in the logics of interactive program verifiers. We showcase our technique by implementing three different certifiers for programs generated via SuSLik, a Separation Logic-based tool for automated synthesis of programs with pointers, in foundational verification frameworks embedded in Coq: Hoare Type Theory (HTT), Iris, and Verified Software Toolchain (VST), producing concise and efficient machine-checkable proofs for characteristic synthesis benchmarks.

Thu 8 Dec

Displayed time zone: Auckland, Wellington change

15:30 - 17:00
ICFP PapersCOVID Time Papers In Person at Seminar Room LG004
Chair(s): Matthieu Lemerre CEA LIST, France
15:30
30m
Talk
Certifying the Synthesis of Heap-Manipulating Programs
COVID Time Papers In Person
Yasunari Watanabe Ahrefs Research, Kiran Gopinathan National University of Singapore, George Pîrlea National University of Singapore, Singapore, Nadia Polikarpova University of California at San Diego, Ilya Sergey National University of Singapore
Link to publication DOI
16:00
30m
Talk
Kindly Bent to Free Us
COVID Time Papers In Person
Gabriel Radanne Inria, Hannes Saffrich University of Freiburg, Peter Thiemann University of Freiburg, Germany
Link to publication DOI
16:30
30m
Talk
Stable relations and abstract interpretation of higher-order programs
COVID Time Papers In Person
Benoît Montagu Inria, Thomas P. Jensen INRIA Rennes
Link to publication File Attached