Overview
Kratos is a software model checker for SystemC . Currently, it only verifies safety properties in the form of program assertion. Kratos provides two different analyses for verifying SystemC designs: sequential and concurrent analyses. The sequential analysis is based on the lazy predicate abstraction and relies on the translation from SystemC designs to sequential C programs. The concurrent analysis is based on the ESST algorithm that combines Explicit state techniques to handle the SystemC Scheduler with Symbolic techniques based on lazy predicate abstraction to handle the Threads.
Downloads
Kratos consists of two executables that run under Linux machine:
- swchecker implements the sequential analysis.
- cswchecker implements the concurrent analysis.
Documents related to Kratos are the following:
- Manual.
- Architecture (a tool paper submitted for publication).
Benchmarks
- Benchmarks for swchecker.
- Benchmarks for cswchecker.
