Using the C Bounded Model Checker as a TLA+
TLA+ and Alloy are lower barrier to entry software verification tools. They are typically used on systems or protocol level models rather than modelling the exact source. There are many bugs that can appear at this level and they are super useful for clarifying your thinking.
CBMC is a tool I’m pretty bullish on. It is a bounded model checker for C code. It more or less unrolls all loops in normal compileable C to some depth and then throws that into a SAT or SMT solver.
What really makes this great is that there is no new language for software engineers to learn or accept. C has already made it in. People accept C as a useful pragmatic language. I found this a fascinating read in terms of how to make formal methods useable in industry Code-level model checking in the software development workflow at Amazon Web Services
Ultimately, there is surprisingly little difference between ordinary programming and a logic if you are trying to see the similarities. A logical spec is not that different writing a programmatic check. CBMC takes it’s specs largely in the form of regular asserts.
