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.


 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