CHC Model Validation with Proof Guarantees

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F24%3A10474845" target="_blank" >RIV/00216208:11320/24:10474845 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-031-47705-8_4" target="_blank" >https://doi.org/10.1007/978-3-031-47705-8_4</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-47705-8_4" target="_blank" >10.1007/978-3-031-47705-8_4</a>

Jazyk výsledku

angličtina

Název v původním jazyce

CHC Model Validation with Proof Guarantees

Popis výsledku v původním jazyce

Formal verification tooling increasingly relies on logic solvers as automated reasoning engines. A point of commonality among these solvers is the high complexity of their codebases, which makes bug occurrence disturbingly frequent. Tool competitions have showcased many examples of state-of-the-art solvers disagreeing on the satisfiability of logic formulas, be them solvers for Boolean satisfiability (SAT), satisfiability modulo theories (SMT), or constrained Horn clauses (CHC). The validation of solvers&apos; results is thus of paramount importance, in order to increase the confidence not only in the solvers themselves, but also in the tooling which they underpin. Among the formalisms commonly used by modern verification tools, CHC is one that has seen, at the same time, extensive practical usage and very little efforts in result validation. As one of the initial steps in addressing this issue, we propose and evaluate a two-layered validation approach for witnesses of CHC satisfiability. Our approach relies, first, on a proof producing SMT solver to validate a CHC model via a series of SMT queries, and, second, on a proof checker to validate the SMT solver&apos;s results. We developed a modular evaluation framework and assessed the approach&apos;s viability via large scale experimentation, comparing three CHC solvers, five SMT solvers, and four proof checkers. Our results indicate that the approach is feasible, with potential to be incorporated into CHC-based tooling, and also confirm the need for validation, with nine bugs being found in the tools used.

Název v anglickém jazyce

CHC Model Validation with Proof Guarantees

Popis výsledku anglicky

Formal verification tooling increasingly relies on logic solvers as automated reasoning engines. A point of commonality among these solvers is the high complexity of their codebases, which makes bug occurrence disturbingly frequent. Tool competitions have showcased many examples of state-of-the-art solvers disagreeing on the satisfiability of logic formulas, be them solvers for Boolean satisfiability (SAT), satisfiability modulo theories (SMT), or constrained Horn clauses (CHC). The validation of solvers&apos; results is thus of paramount importance, in order to increase the confidence not only in the solvers themselves, but also in the tooling which they underpin. Among the formalisms commonly used by modern verification tools, CHC is one that has seen, at the same time, extensive practical usage and very little efforts in result validation. As one of the initial steps in addressing this issue, we propose and evaluate a two-layered validation approach for witnesses of CHC satisfiability. Our approach relies, first, on a proof producing SMT solver to validate a CHC model via a series of SMT queries, and, second, on a proof checker to validate the SMT solver&apos;s results. We developed a modular evaluation framework and assessed the approach&apos;s viability via large scale experimentation, comparing three CHC solvers, five SMT solvers, and four proof checkers. Our results indicate that the approach is feasible, with potential to be incorporated into CHC-based tooling, and also confirm the need for validation, with nine bugs being found in the tools used.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA23-06506S" target="_blank" >GA23-06506S: Pokročilá analýza a verifikace pro pokročilý software</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2024

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ISBN

978-3-031-47704-1

ISSN

—

e-ISSN

—

Počet stran výsledku

20

Strana od-do

62-81

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Leiden, Nizozememsko

Datum konání akce

13. 11. 2023

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001148151200004