Static Analysis
Binary ninja (binja) provides a comfortable automated/manual static analysis
platform for binaries due to its api and intermediate language design.
I've had a lot of success using Frama-C to analyze C code with its many plugins such as Eva, WP, and E-ACSL.
Interactively create slices to improve static RE in binja.
Identify common functions within any binary efficiently and accurately.
I use binexport to create protocol buffers from binja that can be consumed by bindiff.
I use bindiff to do patch analysis for understanding how post-exploit code
needs updated and to recover patched vulns.
Sanitizers
The following sanitizers work well with access to C/C++ source code.
After compiling with these sanitizers the resulting executable will log any detected errors.
LLVM supports these sanitizers with gcc support slowly rolling in.
Property Based Testing
Many languages have property based testing support which can be used to specify
correctness then generate test cases in a variety of ways.
This pairs well with sanitizers.
