[Prev][Next][Index]

Program proving question

Dave, Greg,

I plan to suggest that he contact you, even though he's tackling a more
difficult problem in a more challenging language...

Jim H.

------- Forwarded Message

From: Poetzsch-Heffter <poetzsch@informatik.tu-muenchen.de>
Date: 	Wed, 9 Feb 1994 09:56:29 +0100
To: larch-interest
Subject: Proving Interface Specifications Correct.


I am interested in proving that procedures/program modules
satisfy their interface specifications. We plan to start 
with a subset of LSL/LCL and to develop an interactive tool
that allows to prove that C-programs satisfy their specification.
The project has two main aspects:
  (a) The development of programming logics based on formal 
      operational semantics. 
  (b) The tool support.

Is there already work done in this direction? Any comments?

Thanks for answers.

 Best,       
        Arnd.


=================================================================
 Arnd Poetzsch-Heffter           phone:  ++49 89 2105 8188
   Fakultaet fuer Informatik     fax  :  ++49 89 2105 8180
   Technische Universitaet       email:  poetzsch@informatik.
   D-80290 Muenchen                              tu-muenchen.de
   Germany


------- End of Forwarded Message