Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{2335417,
author = {Griggio, Alberto and Jonáš, Martin},
address = {Paříž, Francie},
booktitle = {Computer Aided Verification. CAV 2023},
doi = {http://dx.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 - JOUR
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://dx.doi.org/10.1007/978-3-031-37709-9\_{}20.
|
