4 ms·
Non trivial example projects https://model-checking.github.io/cbmc-training/projects.html https://model-checking.github.io/cbmc-training/projects.html Some cryp
by philzook 3y ago
Non trivial example projects https://model-checking.github.io/cbmc-training/projects.html https://model-checking.github.io/cbmc-training/projects.html
Some crypto, AWS common C, FreeRTOS. Other interesting applications https://www.cprover.org/cbmc/applications/ https://www.cprover.org/cbmc/applications/
- philzook 3y agoFrama-C is also very cool. Also Coq VST and however seL4 does it. I think out of all of these, CBMC requires the least expertise / has highest automation. I also don't see how it can scale beyond the unit test level, or patch together verification conditions into global properties. Perhaps this could be done by some meta framework plugging together calls to CBMC. Given the level of penetration of formal methods generally, I think the relatively low ambition of CBMC compared to these higher ceiling techniques is good.
- rwmj 3y agoThanks, very interesting stuff!