Witch
A violation witness validator for sequential C programs and witnesses in the format 2.0. The tool utilises the infrastructure of Symbiotic, and uses a validation backend built on top of the symbolic executor JetKlee.
Symbiotic-Witch
A tool for validating violation witnesses in the witness format 1.0 for sequential C programs. It uses parts of the Symbiotic framework with a Klee-based witness validation module as the back-end verifier. The tool decides the validity of witnesses of violations of multiple common safety properties (assertion safety, memory safety, etc.).
Symbiotic
A program analysis framework for C programs. The tool combines static analysis, program slicing, and symbolic execution. It can check common safety properties (such as the absence of assertion violations, memory leaks, overflows, etc.) and termination.
Contribution: Violation witness generation for JetKlee back-end in witness formats 1.0 and 2.0.