points by uecker 4 days ago | 0 comments
C and formal verification is an awesome combination. I tried cmbc on some toy programs, it it fully automatically proved memory safety and all assertions. But for larger programs one has to split up with a contract-like facility.
Can you tell us more how you use cbmc with macros? I am also exploring this.
I also wonder what feature from C++ you miss in C?
[–] nanolith 3 days ago
I did a talk on this at BSDCan 2026:
https://www.bsdcan.org/2026/timetable/timetable-Model-Checki...
That link has the slides and some example code. There's also a live stream on YouTube.
Regarding features I miss from C++, I like the concept of generics. I don't like the implementation in C++. I also find C's _Generic facility to be limited, especially when building containers that perform hygienic type erasure. This feature isn't enough for me to go back to C++ on its own, but it is something I'm exploring in a new language I'm writing.
[–] uecker 2 days ago
Thank you!
[–] Surac 4 days ago