Re: Formal semantics for C

• To: Ken Friis Larsen <kfl@it.edu>
• Subject: Re: Formal semantics for C
• From: Jim Huggins <jhuggins@kettering.edu>
• Date: Wed, 6 Mar 2002 15:06:36 -0500 (EST)
• cc: types@cis.upenn.edu, "S.J.Thompson" <S.J.Thompson@ukc.ac.uk>, Michael.Norrish@cl.cam.ac.uk
• In-Reply-To: <200112221624.fBMGOdq04891@saul.cis.upenn.edu>
• Organization: Kettering University

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:

	http://www.eecs.umich.edu/gasm/papers/calgebra.html 

--Jim Huggins (jhuggins@kettering.edu)

• Prev: Special issue on Mechanising and Automating Mathematics
• Next: Re: Formal semantics for C
• Index(es):
  • Main
  • Thread