> 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. not everybody believes in PCC so much, apparently: http://www.cs.virginia.edu/~evans/talks/horses.ppt sincerely.