Kratos is a software model checker for sequential and (cooperative) threaded C programs. Kratos verifies safety properties in the form of program assertion.
For analysis of sequential programs, Kratos implements
- Lazy Predicate Abstraction (Blast algorithm) and
- Lazy Abstraction with Interpolants (McMillan/Impact algorithm)
For analysis of threaded programs, Kratos implements
- Explicit-Scheduler/Symbolic-Threads (ESST) and
- Semi-Symbolic-Scheduler/Symbolic-Threads (S3ST) algorithms.
ESST combines explicit-state model checking techniques for analyzing the scheduler and symbolic techniques based on lazy predicate abstraction for analyzing the threads. That is, ESST keeps track of the scheduler states explicitly and orchestrate the whole verification by direct executions of the scheduler (i.e., the scheduler is part of the model checking algorithm, and not part of design under verification). S3ST is built on ESST for handling designs with parametric interactions between the threads and the scheduler. S3ST combines the explicit part of executions with symbolically-represented set of scheduler states.
Both ESST and S3ST have been specialized to SystemC verification. In the sense that ESST and S3ST implements SystemC scheduling policy and (subset of) SystemC synchronization functions. ESST, in particular, has also been specialized to FairThreads verification.
Kratos can also perform translations from sequential programs to Promela or to NuSMV models, and from threaded programs to Promela models. Currently, Kratos only handles a subset of C language. Extending Kratos to handle a large subset of C constructs are in progress.
Info on SystemC2C
Due to a number of requests for SystemC2C, we regret to say that, unfortunately, we no longer develop, maintain, and distribute SystemC2C because it relies on old tools that are no longer maintained/available on our system. In particular SystemC2C relies on Pinapa front-end, that is no longer maintained by its developers, and an old version of GCC, that is no longer installed on our system.
You can still use Kratos to verify sequential and threaded C benchmarks that encode SystemC models. We provide the benchmarks in our download section. Moreover, because Kratos is constantly under development, we have not released a newer version of it. So, we suggest that you try the Kratos executable used in our latest paper that is list in the publication section (the download link is provided in the paper).
