Program verifiers are complex

I've recently found out that epitome is not only a Romanian word but also an English one. The discovery deserves a blog post.

Programs instruct (virtual) machines what to do. Programs tell type-checkers what to check. Programs can also tell program verifiers what to check. A (static) program verifier is a little like a type-checker on steroids. Unlike type-checkers, they tend to be complex beasts. ACL2, Jahob, and Spec#, all tame the complexity in different ways.

The approach in Jahob is code reuse. The developers chose to rely heavily on the work of others and innovated mainly in the area of "putting things together".

Spec# divides and conquers, much like Microsoft does in general. They broke down the process of verification into multiple simpler phases and built probably the best engineered program verifier.

The old ACL2 encodes complexity in data rather than code. More specifically Moore (yes, the same guy who did the string matching algorithm) notes that there is no need for verification condition generation if you simply tell a prover the operational semantics of the language you are processing.

It's funny how the oldest tool has the slickest approach (and, probably, the smallest number of developers). Here are some references:

• Full functional verification of linked data structures
• Boogie: A Modular Reusable Verifier for Object-Oriented Programs
• Inductive assertions and operational semantics