Kratos - A Software Model Checker for SystemC

The growing popularity of SystemC has attracted research aimed at the formal verification of SystemC designs. In this paper we present Kratos, a software model checker for SystemC. Kratos verifies safety properties, in the form of program assertions, by allowing users to explore two directions in the verification. First, by relying on the translation from SystemC designs to sequential C programs, Kratos is capable of model checking the resulting C programs using the symbolic lazy predicate abstraction technique. Second, Kratos implements a novel algorithm, called ESST, that combines Explicit state techniques to deal with the SystemC Scheduler, with Symbolic techniques to deal with the Threads. Kratos is built on top of NuSMV and MathSat, and uses state-of-the-art SMT-based techniques for program abstractions and refinements. © 2011 Springer-Verlag.