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

• Symbolic execution
• Bug detection
• Program slicing
• Safety verification
• Memory safety

Type of tool

Bug detector

Expected 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

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.