Ah, I see what you mean. Software Foundation hints ever so slightly at more specific approaches. Looking into the other books a little bit more, I'm not so cert

Ah, I see what you mean. Software Foundation hints ever so slightly at more specific approaches. Looking into the other books a little bit more, I'm not so certain Software Foundations would serve as a good introduction to them. The reason being that it focuses very heavily on the theorem-proving aspects. Concrete Semantics, at least its second half, would be an excellent primer. Software Foundations puts more weight on proving properties about languages than it does verifying particular programs. Whereas Concrete Semantics culminates in Hoare logic and abstract interpretation. That sounds like an excellent use of model checking tools. Most approaches I've seen involve creating a model of some system separate from the implementation, which I think is risky. Still better than nothing, by far. I'll definitely have to check those books out now. Thanks for the recommendations!