Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866909179054129152 |
|---|---|
| author | Somorjai, Márk Dobos-Kovács, Mihály Ádám, Zsófia Bajczi, Levente Vörös, András |
| author_facet | Somorjai, Márk Dobos-Kovács, Mihály Ádám, Zsófia Bajczi, Levente Vörös, András |
| contents | Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_15215 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification Somorjai, Márk Dobos-Kovács, Mihály Ádám, Zsófia Bajczi, Levente Vörös, András Logic in Computer Science Software Engineering Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique. |
| title | Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification |
| topic | Logic in Computer Science Software Engineering |
| url | https://arxiv.org/abs/2404.15215 |