Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2403.05607 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Table of Contents:
- 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.