PV4 Symbioticcan detect assertion violations and memory-related bugs in C programs

Symbiotic implements an approach of combining instrumentation, slicing, and symbolic execution to detect errors in (sequential) C programs

Application domain/field

Type of tool

Bug detector

Expected input

Format:

Expected output

Symbiotic will report any assertion or property violations that it finds. It can also generate a violation witness if a property/assertion is violated.

Internals

Symbiotic can be used to check safety properties such as assertion violations, invalid pointer dereference, double free, memory leaks, etc. Uses KLEE for symbolic execution. Uses Z3 for SMT solving.

Comments

Symbiotic has participated in SV-COMP (verification competition) in 2016-2021.

Links

Related papers

Last publication date

18 May 2020

Related tools

ProVerB specific

Markdown description: view/edit



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