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!
|
| _version_ | 1866913258543251456 |
|---|---|
| author | Meyer, Roland Tepe, Jakob Wolff, Sebastian |
| author_facet | Meyer, Roland Tepe, Jakob Wolff, Sebastian |
| 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_05607 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Realizability in Semantics-Guided Synthesis Done Eagerly Meyer, Roland Tepe, Jakob Wolff, Sebastian Logic in Computer Science Programming Languages 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. |
| title | Realizability in Semantics-Guided Synthesis Done Eagerly |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2403.05607 |