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.
