4 ms·
Lookup what CBMC does. SAT solvers will also be also be applied in traditional compilers soon. The remaining problem with formal verification and compilation
by rurban 5y ago
Lookup what CBMC does.
SAT solvers will also be also be applied in traditional compilers soon.
The remaining problem with formal verification and compilation is proof of termination, which is not a SAT problem.
Running all test cases via cbcm is magnitudes faster than writing 100% coverage (only line cov, not covered values) tests. It's like one day vs one month. And I've never seen code with full value test coverage.
For guaranteed timing you need special tests, not a SAT solvers. The solver just helps with the proofs.
- AnimalMuppet 5y agoEven if everything you say is true, it's true the first time. Then I make a change to the code. Now if I have unit tests, I have to fix a test (maybe minutes, maybe an hour) and re-run the tests (minutes). Or I have to re-run the formal verification (a day).
- rurban 5y agomake verify needs less than a few seconds on my targets. Everything over 30min needs to be fixed, or split up.