On Fri, May 31, 2002 at 03:17:30PM -0700, Waldemar Horwat wrote:
> How much work has been done on generalizing the notion of a static
> type system into a more complete framework for proving interesting
> invariants about a program? In essence, I'd like the source code of
> a program to consist of two interweaved parts:
<snip>
You may wish to read some of Dawson Engler's papers on metacompilaion (also
known as the Stanford Checker). It's not a generalisation of a type-system so
much as a separate language for expressing assertions about the program (such
as "the interrupts flag should be set upon return of this function"). The
implementation has been used `in anger' to find many problems in the Linux
kernel source.
http://www.stanford.edu/~engler/
Adam Langley
Attachment:
pgp19005.pgp
Description: PGP signature