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


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.


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.


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


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.