An erstwhile corollary of “thinking in C” was that we felt the specification and the program to be one and the same. Decades of collective suffering led us to realize the value of abstracting high-level models of the design and applying such methods to ensure pre-implementation consistency, correctness, and other desiderata for our designs.
This paper tells us that we can finally eat our cake and have it too: “The code of the application is now executed as is by the model checker. ... [This] allows us to verify implementation level code ... for ... safety and liveness properties.”
The paper begins with clear examples of SPIN/Promela-based “classical,” that is, high-level, model checking and also of SPIN as enhanced by new primitives that enable embedding of C code fragments into Promela text. Section 4, “The use of abstraction,” explains how to “define abstractions that can optimize ... exploration” of the enormous state-space that implementation-level C code engenders. Section 4.3 points out the price to be paid: “Not all user-defined abstractions will necessarily preserve ... logical soundness” in such code checking. The authors cite two conditions that are sufficient for an abstraction to be sound [1]. Section 6 states it simply: “We no longer attempt to extract models from the C code, we directly embed the ... C code into the verification model.”
This is an excellent, state-of-the-art paper that will benefit practitioners and students alike.