D 2023

Kratos2: An SMT-Based Model Checker for Imperative Programs

GRIGGIO, Alberto a Martin JONÁŠ

Základní údaje

Originální název

Kratos2: An SMT-Based Model Checker for Imperative Programs

Autoři

GRIGGIO, Alberto (380 Itálie) a Martin JONÁŠ (203 Česká republika, garant, domácí)

Vydání

Paříž, Francie, Computer Aided Verification. CAV 2023, od s. 429-436, 8 s. 2023

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/23:00132160

Organizační jednotka

Fakulta informatiky

ISBN

978-3-031-37708-2

ISSN

DOI

Klíčová slova anglicky

Model checking

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 8. 4. 2024 17:08, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

This paper describes Kratos2, a tool for the verification of imperative programs. Kratos2 operates on an intermediate verification language called K2, with a formally-specified semantics based on smt, allowing the specification of both reachability and liveness properties. It integrates several state-of-the-art verification engines based on sat and smt. Moreover, it provides additional functionalities such as a flexible Python api, a customizable C front-end, generation of counterexamples, support for simulation and symbolic execution, and translation into multiple low-level verification formalisms. Our experimental analysis shows that Kratos2 is competitive with state-of-the-art software verifiers on a large range of programs. Thanks to its flexibility, Kratos2 has already been used in various industrial projects and academic publications, both as a verification back-end and as a benchmark generator.