Re: Formal semantics for C

Forgive the long delay on replying to this message, but I only now have
had the chance to reply properly.

On 22 Dec 2001, Ken Friis Larsen wrote:

> "S.J.Thompson" <S.J.Thompson@ukc.ac.uk> writes:
> > Query about the formal semantics of C:
> > 
> > Are types readers aware of any work on formalizing the semantics
> > of the C programming language?

> Michael Norrish (Computer Lab, University of Cambridge) developed a
> formal model for C and embedded this model into the HOL theorem
> prover.  More information here:
>         http://www.cl.cam.ac.uk/users/mn200/PhD/

Some time ago, Yuri Gurevich and I did a formal semantics of C 
using the Abstract State Machine (ASM) methodology, then called
"evolving algebras".  You can find more information at:


--Jim Huggins (jhuggins@kettering.edu)