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 programsApplication domain/field
- Symbolic execution
- Bug detection
- Program slicing
- Safety verification
- Memory safety
Type of tool
Bug detectorExpected input
- Instrumented C program. It needs to be instrumented with e.g. assertions or
__VERIFIER_error()
. - Optional: This can be used to indicate that Symbiotic should look for certain errors aside from assertion violations, e.g. errors in memory manipulations.
Format:
- Program:
.c
file(s) - Optional property: passed as an argument while calling symbiotic