|
|
|
|
|
|
by rurban
4453 days ago
|
|
|
Klee, EXE, Forensic, cbmc, BAP all mix symbolic analysis with SAT solvers into the C parse tree, and can come up with input to contradict the assertions. (automatic testcases or exploits)
Frama-C still beats all with it's interface, but Forensic is so nice that it even tells how the fix should look like. https://en.wikipedia.org/wiki/Model_checking |
|
|