Verifying Tree-Manipulating Programs via CHCs
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866908372031242240 |
|---|---|
| author | Faella, Marco Parlato, Gennaro |
| author_facet | Faella, Marco Parlato, Gennaro |
| contents | Programs that manipulate tree-shaped data structures often require complex, specialized proofs that are difficult to generalize and automate. This paper introduces a unified, foundational approach to verifying such programs. Central to our approach is the knitted-tree encoding, modeling each program execution as a tree structure capturing input, output, and intermediate states. Leveraging the compositional nature of knitted-trees, we encode these structures as constrained Horn clauses (CHCs), reducing verification to CHC satisfiability task. To illustrate our approach, we focus on memory safety and show how it naturally leads to simple, modular invariants. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_14092 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Verifying Tree-Manipulating Programs via CHCs Faella, Marco Parlato, Gennaro Programming Languages Logic in Computer Science F.3.1; F.4.1 Programs that manipulate tree-shaped data structures often require complex, specialized proofs that are difficult to generalize and automate. This paper introduces a unified, foundational approach to verifying such programs. Central to our approach is the knitted-tree encoding, modeling each program execution as a tree structure capturing input, output, and intermediate states. Leveraging the compositional nature of knitted-trees, we encode these structures as constrained Horn clauses (CHCs), reducing verification to CHC satisfiability task. To illustrate our approach, we focus on memory safety and show how it naturally leads to simple, modular invariants. |
| title | Verifying Tree-Manipulating Programs via CHCs |
| topic | Programming Languages Logic in Computer Science F.3.1; F.4.1 |
| url | https://arxiv.org/abs/2505.14092 |