Re:Software Foundations by Benjamin Pierce et al.
by cmrx64 on Sunday December 13, 2015 @09:42PM
(#10729137)
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!
I think I disagree a bit wrt model checking, which is very useful in some specialized domains. I have had quite a lot of success with it when verifying complex real time systems, specified as timed automata. We then generated code from this specifications. It'd be challenging to use any other technique to achieve such an exhaustive verification.
Both [1-2] can be found online, and [2] is particularly enlightening! I followed a course by the authors, and implemented a big chunk of the book. It's really awesome to implement static analyzers by interpreting programs with a more abstract set of types.