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

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.
C++ SystemC

Links

Project page: http://www.cprover.org/scoot/

Last commit date

- (latest download available on the project website is from October 2009)

Related papers

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.