1. Realizability in Semantics-Guided Synthesis Done Eagerly
- Author
-
Meyer, Roland, Tepe, Jakob, and Wolff, Sebastian
- Subjects
Computer Science - Logic in Computer Science ,Computer Science - Programming Languages - Abstract
We present realizability and realization logic, two program logics that jointly address the problem of finding solutions in semantics-guided synthesis. What is new is that we proceed eagerly and not only analyze a single candidate program but a whole set. Realizability logic computes information about the set of candidate programs in a forward fashion. Realization logic uses this information as guidance to identify a suitable candidate in a backward fashion. Realizability logic is able to analyze a set of programs due to a new form of assertions that tracks synthesis alternatives. Realizability logic then picks alternatives to arrive at a program, and we give the guarantee that this process will not need backtracking. We show how to implement the program logics using verification conditions, and report on experiments with a prototype in the context of safe memory reclamation for lock-free data structures., Comment: 47 pages, 16 figures
- Published
- 2024