Symbiotic: finding bugs in C programs
summary
Symbiotic is an open‑source C bug finder that translates code to LLVM bitcode via clang, applies optimizations and program slicing, then runs symbolic execution (KLEE) to prove or produce counterexamples. Examples show it finds assertion violations, integer overflows and a real memory leak in a linked‑list example; it reports the offending path and concrete values. Current limits: no C++ exceptions, no parallel programs, and scalability depends on slicing and abstraction choices.
AI-written summary · about
chapters (12)
- 0:00Symbiotic introduction
- 1:08Symbolic execution basics
- 6:03Live demo of Symbiotic
- 7:32Symbolic execution challenges
- 8:13Program slicing optimization
- 12:09Automatic symbolic variables
- 13:39Assertion violations detection
- 15:08Memory safety errors
- 16:14Valgrind case study
- 18:28Optimizations impact
- 19:32Future plans
- 21:18Q&A
related talks
01h 12mFinding Bugs with Clang at Compile and Run Time
24mQSYM : A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing
01h 04mCompiler Bugs And Bug Compilers
29mFinding real bugs in big programs with incorrectness logic
24mInception: System-Wide Security Testing of Real-World Embedded Systems Software
30mLet's Build a Symbolic Analyser And Automatically Find Bugs
59mUnder-approximation for Scalable Bug Detection
52mStructure aware fuzzing