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:
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 (firstname.lastname@example.org)