Kratos2: An SMT-Based Model Checker for Imperative Programs

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 a Martin JONÁŠ

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

https://doi.org/10.1007/978-3-031-37709-9_20

UT WoS

001310805600020

EID Scopus

2-s2.0-85169473274

Klíčová slova anglicky

Model checking

Štítky

core_A, firank_1

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 13. 8. 2025 18:04, Mgr. Petra Trembecká, 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.

Citovat

GRIGGIO, Alberto a Martin JONÁŠ. Kratos2: An SMT-Based Model Checker for Imperative Programs. In Constantin Enea, Akash Lal. Computer Aided Verification. CAV 2023. Paříž, Francie: Springer, 2023, s. 429-436. ISBN 978-3-031-37708-2. Dostupné z: https://doi.org/10.1007/978-3-031-37709-9_20.

@inproceedings{2335417,
   author = {Griggio, Alberto and Jonáš, Martin},
   address = {Paříž, Francie},
   booktitle = {Computer Aided Verification. CAV 2023},
   doi = {https://doi.org/10.1007/978-3-031-37709-9_20},
   editor = {Constantin Enea, Akash Lal},
   keywords = {Model checking},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Paříž, Francie},
   isbn = {978-3-031-37708-2},
   pages = {429-436},
   publisher = {Springer},
   title = {Kratos2: An SMT-Based Model Checker for Imperative Programs},
   year = {2023}
}

TY  - CONF
ID  - 2335417
AU  - Griggio, Alberto - Jonáš, Martin
PY  - 2023
TI  - Kratos2: An SMT-Based Model Checker for Imperative Programs
PB  - Springer
CY  - Paříž, Francie
SN  - 9783031377082
KW  - Model checking
N2  - 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.
ER  -

GRIGGIO, Alberto a Martin JONÁŠ. Kratos2: An SMT-Based Model Checker for Imperative Programs. In Constantin Enea, Akash Lal. \textit{Computer Aided Verification. CAV 2023}. Paříž, Francie: Springer, 2023, s.~429-436. ISBN~978-3-031-37708-2. Dostupné z: https://doi.org/10.1007/978-3-031-37709-9\_{}20.

Přehled o publikaci