[cap-talk] Confessions of a C programmer

[Sandro Magi]

Bill Frantz wrote:
> (Hehe) And probably the easiest "compiler" to verify is an assembler, since
> the output is directly related to the input. Of course you lose portability
> and memory safety, although Norm wrote some ideas for verifying machine
> code in <http://cap-lore.com/Software/CodeProof/>.
> 
> If one could verify some useful static properties of machine code, and run
> the verifier in a way that it could not modify the code being verified, you
> might end up with smallest development system to verify. Just a thought.

This is related to the ultimate goal of "proof carrying code" [1]. They
now have static analyses that can verify concurrent, interrupt-driven
and self-modifying assembly code.

Sandro

[1] http://flint.cs.yale.edu/flint/publications/