Realizability in Semantics-Guided Synthesis Done Eagerly
<|reference_start|>Realizability in Semantics-Guided Synthesis Done Eagerly: 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.<|reference_end|>
@article{meyer2024realizability,
    title={Realizability in Semantics-Guided Synthesis Done Eagerly},
    author={Roland Meyer, Jakob Tepe, Sebastian Wolff},
    journal={arXiv preprint arXiv:2403.05607},
    year={2024},
    archivePrefix={arXiv},
    eprint={2403.05607},
    primaryClass={cs.LO cs.PL}
}