Formalizing the Notion of Implementation

Billy Tanksley btanksley@hifn.com
Mon, 14 Jun 1999 10:14:51 -0700


> From:	Francois-Rene Rideau [SMTP:fare@tunes.org]
> 
> PPS: those of you having studied ASM (abstract state machines),
> Abstract Interpretation, or whatever, can you give tell me
> which paper to cite, and whom to contact?
> 
	http://www.eecs.umich.edu/gasm/ has the materiel.  It's a good site,
although you'll want some mathematical sophistication and a bit of patience
to read through the tutorials.  They're not teaching people how to use the
ASMs; instead, they're proving how they work.

	There's also a LOT of good case studies, like a formal description
of C, Oberon, and Prolog, or a proof of several described weaknesses in a
security protocol, together with a proof of the suggested workaround.

> [ "Faré" | VN: Уng-Vû Bân | Join the TUNES project!
> http://www.tunes.org/  ]
> 
	-Billy