FO-Complete Program Verification for Heap Logics
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866912814678933504 |
|---|---|
| author | Murali, Adithya Balakrishnan, Hrishikesh Councilman, Aaron Madhusudan, P. |
| author_facet | Murali, Adithya Balakrishnan, Hrishikesh Councilman, Aaron Madhusudan, P. |
| contents | We develop the first two heap logics that have implicit heaplets and that admit FO-complete program verification. The notion of FO-completeness is a theoretical guarantee that all theorems that are valid when recursive definitions are interpreted as fixpoint definitions (instead of least fixpoint) are guaranteed to be eventually proven by the system. The logics we develop are a frame logic ($\textit{FL}$) and a separation logic ($\textit{SL-FL}$) that has an alternate semantics inspired by frame logic. We show verification condition generation for FL that is amenable to FO-complete reasoning using quantifier instantiation and SMT solvers. We show $\textit{SL-FL}$ can be translated to FL in order to obtain FO-complete reasoning. We implement tools that realize our technique and show the expressiveness of our logics and the efficacy of the verification technique on a suite of benchmarks that manipulate data structures. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_06719 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | FO-Complete Program Verification for Heap Logics Murali, Adithya Balakrishnan, Hrishikesh Councilman, Aaron Madhusudan, P. Logic in Computer Science Programming Languages We develop the first two heap logics that have implicit heaplets and that admit FO-complete program verification. The notion of FO-completeness is a theoretical guarantee that all theorems that are valid when recursive definitions are interpreted as fixpoint definitions (instead of least fixpoint) are guaranteed to be eventually proven by the system. The logics we develop are a frame logic ($\textit{FL}$) and a separation logic ($\textit{SL-FL}$) that has an alternate semantics inspired by frame logic. We show verification condition generation for FL that is amenable to FO-complete reasoning using quantifier instantiation and SMT solvers. We show $\textit{SL-FL}$ can be translated to FL in order to obtain FO-complete reasoning. We implement tools that realize our technique and show the expressiveness of our logics and the efficacy of the verification technique on a suite of benchmarks that manipulate data structures. |
| title | FO-Complete Program Verification for Heap Logics |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2601.06719 |