Workshop

Engineering of Software Verification, Validation, and Certification

Kiel, June 26, 1998

  
           

 
Background

   It becomes more and more apparent, that software testing is not sufficient to  guarantee correctness.  More rigorous arguments  are necessary in order to  convince users  of correct  functioning  and reliability of software and  software components of computer  based systems.  Recently,  we realize  major efforts  in verification and  formal  treatment  of  software,  both for safety and  for security reasons. Software becomes a major topic in systems certification.

   On the other hand, the state of the art in software verification is not as promising  yet:  In many  cases, the  effort of  proving the correctness of large software  systems seems not to be justifiable. More modular approaches are  needed  in order  to guarantee and  to establish  software  correctness. ``Correctness Engineering''   needs various  compositional  and modular specification  and verification techniques, mechanical support  for  correct  design, verification, proof  documentation,  and of course,  we  need  to bridge the  gap between  source  level  verification   and  correct  implementation (integration), a major goal of the Verifix project.  While  showing some  recent  ideas and  results, the  workshop mainly serves  as a discussion forum on these topics.


 
Program
 
8.50 - 9.00  Welcome 
Hans Langmaack and Wolfgang Goerigk
 
9.00 - 9.45 Invited Lecture: 
Wolfgang Reif  (Univ. of Ulm, Germany):
Software Verification with KIV.
 
9.45 - 10.15 Wolfgang Goerigk (Univ. of Kiel, Germany):
A Checker-Based Approach to Program Verification and Certification.
 
10.15 - 10.45  Thilo Gaul (Univ. of Karlsruhe, Germany):
Correctness of Generator-Based Compiler Implementations.
 

*** Coffee Break ***
 
11.15 - 11.45  Wolf Zimmermann (Univ. of Karlsruhe, Germany):
Correctness issues in Object Oriented Libraries.
 
11.45 - 12.15  Axel Dold (Univ. of Ulm, Germany):
Formal Software Development using PVS.
 

*** Lunch ***
 
13.15 - 13.45 Stephan Pfab (Univ. of Ulm, Germany):
Animation of PVS Specifications.
 
13.45 - 14.30 Markus Müller-Olm (Univ. of Dortmund, Germany):
Preservation of Partial and Total Correctness:  Refinement-Algebra Can Prove Both.
 

*** Coffee Break***
 
15.15 - 16.15 Invited Lecture and Informatik-Kolloquium:
J Strother Moore (Univ of Texas, Austin):
A Mechanically Checked Proof of a Multiprocessor Resultvia a Uniprocessor View.
 

*** Break***
 
16.45 - 17.15 Michael Siegel (Weizmann Institute of Science, Israel):
Transformation Validation
 

Organisation and Contact


   The workshop will take place at

   Institut für Informatik und Praktische Mathematik
   Christian-Albrechts-Universität zu Kiel
   Merkurhaus
   Seminar Room 223 (Ho1), 2nd floor
   Preusserstr. 1-9
   D-24105 Kiel, Germany

 
Contact:

   Dr. Wolfgang Goerigk
   Institut für Informatik und Praktische Mathematik
   Christian-Albrechts-Universität zu Kiel
   Preusserstr. 1-9,   D-24105 Kiel, Germany
   phone: (0431) 5604-24
   fax  : (0431) 566143
   email: wg@informatik.uni-kiel.de,  wg@acm.org