Publication details

Kratos2: An SMT-Based Model Checker for Imperative Programs


GRIGGIO Alberto JONÁŠ Martin

Year of publication 2023
Type Article in Proceedings
Conference Computer Aided Verification. CAV 2023
MU Faculty or unit

Faculty of Informatics

Keywords Model checking
Description 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.

You are running an old browser version. We recommend updating your browser to its latest version.

More info