Clicky

Harry R. Schwartz

Software engineer, nominal scientist, gentleman of the internet. Member, ←Hotline Webring→.

1B41 8F2C 23DE DD9C 807E A74F 841B 3DAE 25AE 721B

Verified, Validated, or Certified?

Published 17 Feb 2017. Tags: computer-science, formal-methods.

What’s the difference between a verifying compiler, a validating compiler, and a certifying compiler?

All three of these strategies accomplish the same goal: given source code , we should be able to prove that a compiler generates target code such that and satisfy the same specification. We write this as , which indicates that and are semantically equivalent.

I didn’t understand the difference between these strategies—I think I thought they were all vaguely synonymous?—but §2 of Leroy’s Formal Verification of a Realistic Compiler1 clarifies the distinctions.

A verified compiler is accompanied by a proof that, for any , it’ll either throw an error2 or generate code such that . This is the direct approach that usually manifests as “write it in Coq and export it to OCaml.” A verified compiler is correct by construction.

A validated compiler has two components: an unverified compiler and a verified validator. The validator is a Boolean function that takes and and returns true if and only if . In other words:

Note that the general problem of determining whether for any and is undecidable, so most validators would probably conservatively return false if couldn’t be determined.

A certified compiler passes the verification buck to its users. Given source code , it’ll either fail to compile or produce code and certificate , where is a proof that . The user (or, more likely, a client library) can then check that is correct with a verified proof checker.

The compiler itself doesn’t need to be verified, since users can ascertain for themselves (using the certificate) that the compiled code has the same specification as the source.

To sum up, these three approaches all guarantee that :

If you want to prove that your compiler preserves semantics, then, you’d probably want to pick one of these three strategies. You could also structure your compiler as a series of passes, each of which would use one of these. Passes compose trivially, so a chain of correct passes would yield a correct compiler.

Now entering the realm of speculation…

Since all three of these strategies make the same guarantees, could we automatically change strategies? For example, given a validating compiler, could we automatically construct an equivalent verified compiler for the same specification? Leroy notes that it’s theoretically possible to construct a certifying compiler from a verified compiler, but I wonder if that’s true more generally. Do these form an equivalence class? If so, what’s the name of that class, and what else is in it? Have any of those constructions been implemented? Gotta do more reading!

  1. Xavier Leroy, Formal verification of a realistic compiler. Communications of the ACM 52(7), July 2009.

  2. Note that a compiler that only throws errors satisfies this definition. I was delighted to learn that I’ve successfully (if unknowingly) written a verified compiler!