Informace o publikaci
Kratos2: An SMT-Based Model Checker for Imperative Programs
| Autoři | |
|---|---|
| Rok publikování | 2023 |
| Druh | Článek ve sborníku |
| Konference | Computer Aided Verification. CAV 2023 |
| Fakulta / Pracoviště MU | |
| Citace | |
| Doi | http://dx.doi.org/10.1007/978-3-031-37709-9_20 |
| Klíčová slova | Model checking |
| Popis | 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. |