Publications related to Kratos2

• Combining Symbolic Execution with Predicate Abstraction and CEGAR, at FMCAD 2024, describes a new verification technique for implemented in Kratos2.

• Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development, at TACAS 2024, describes an industrial application of Kratos2 in the automotive domain.

• Kratos2: an SMT-Based Model Checker for Imperative Programs, at CAV 2023, is a tool paper describing Kratos2.

• EVA: a Tool for the Compositional Verification of AUTOSAR Models, at TACAS 2023. Kratos2 is used as one of the verification backends.

• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays, in Logical Methods in Computer Science, Volume 18, Issue 3. Kratos2 is used as a translator from C to transition systems.