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

• Model checking
• Simulation
• Model extraction
• SystemC
• Concurrency

Type of tool

Model extractor?

Expected input

SystemC program

Format:

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.

Internals

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.