[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Generalizing Types as Provable Invariants

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:
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.
Adam Langley

Attachment: pgp19005.pgp
Description: PGP signature