[Prev][Next][Index]
Proving Interface Specifications Correct.
-
To: larch-interest
-
Subject: Proving Interface Specifications Correct.
-
From: Poetzsch-Heffter <poetzsch@informatik.tu-muenchen.de>
-
Date: Wed, 9 Feb 1994 09:56:29 +0100
-
Delivery-Date: Wed, 09 Feb 94 02:12:14 -0800
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