PV2 SCOOTextracts models from source code for other checkers, generates code that does not rely on SystemC

Tool for the analysis of SystemC systems. It extracts models that can be passed to tools such as SatAbs and CBMC.

Application domain/field

Type of tool

Model extractor?

Expected input

SystemC program


C++ files that use the SystemC header (#include )

Expected output

Formal model or a flat C++ program that does not use the SystemC library anymore.


SCOOT statically analyses systems described using SystemC and extracts models that can be passed to verification tools such as SatAbs or CBMC. It focuses on the scheduling of the SystemC threads. SCOOT can do race analysis.
C++ SystemC


Related papers

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.