Engineering of Software Verification, Validation, and Certification

Kiel, June 23, 2000

Background

It is apparent that testing is not sufficient for software correctness and reliability.  More rigorous arguments are necessary in order to convince users of correct functioning and reliability of software and software components of computer based systems.  Although we realize major efforts in verification and formal treatment of software, both for safety and for security, state of the art in software verification is not as promising yet.

Software becomes a major topic in systems certification.  In many cases, however, the effort of proving the correctness of large software based systems seems not to be justifiable.  We need modular approaches 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, validation, 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 on correct compilation.
 

Participation and Contribution

The workshop is intended to be a discussion forum, and to show recent ideas, insights and results, both from industry and academia. It will accommodate presentations concerning not only current work but also interests and experience related to the workshop theme. You are invited to submit abstracts of presentations, including title and author name(s) and email, preferably by email to wg@informatik.uni-kiel.de. Abstracts should be at most one page and sent soon, but not later than April 28.

If you want to participate, please contact us as soon as possible preferably by email to wg@informatik.uni-kiel.de or to up@informatik.uni-kiel.de. Please let us know if you need hotel accomodation, and your arrival and departure time.

 

Venue

The date of the workshop is within Kiel Week, which is a famous sailing competition and festival held every summer. Festival activities will run over the weekend following the workshop. The workshop will be held at
 

Institut für Informatik und Praktische Mathematik
Christian-Albrechts-Universität zu Kiel
Seminar Room (Ü2) and Conference Room
Ludewig-Meyn-Straße 2,
D-24098 Kiel, Germany

Program
 

9.00 - 9.15	Welcome  by Wolfgang Goerigk and Michael Hanus
9.15 - 9.45	Wolfgang Goerigk  (University of Kiel,, Germany) Proving Preservation of Partial Correctness with PVS.
9.45 - 10.15	Roy Bartsch (University of Kiel, Germany): Verification through Program Result Checking: Certifying Railway Relay Circuits.
10.15 - 10.45	Andreas Wolf (University of Kiel, Germany): On "correct" Translations - Wicked Reality vs. Elegant Theory.
	*** Coffee Break ***
11.15 - 11.45	Thilo Gaul (University of Karlsruhe, Germany): Runtime Result Verification: A Practical Approach to Compiler Verification.
11.45 - 12.15	Harald Rueß (SRI International, U.S.A.): Protocol-Independent Secrecy.
12.15 - 12.45	Bruno Langenstein, Roland Vogt, Markus Ullmann (DFKI GmbH Saarbrücken, BSI Bonn, Germany) Modelling Trusted Digital Signature Devices Using VSE
	*** Lunch Break ***
14.00 - 14.30	Markus Müller-Olm (University of Dortmund, Germany): On the Complexity of True Liveness and Copy Constants for Parallel Programs.
14.30 - 15.00	Werner Stephan, Georg Rock, Andreas Nonnengart, Bruno Langenstein  (DFKI GmbH Saarbrücken, Germany): Hybrid Systems in VSE-II.
15.00 - 15.30	Serge Autexier, Dieter Hutter (Univ. des Saarlandes and DFKI GmbH, Saarbrücken, Germany): Towards an efficient management of change in an evolutionary formal software development.
	*** Coffee Break***
16.15	Invited Lecture and Informatik-Kolloquium: J Strother Moore (Univ of Texas at Austin, U.S.A.): Recent Results with ACL2.
19:00	***  Farewell Dinner ***

 

Organisation and Contact
 

Contact:
 

Prof. Dr. Michael Hanus, PD Dr. Wolfgang Goerigk, Mrs. Ulrike Poilakowski-Geuther
Institut für Informatik und Praktische Mathematik
Christian-Albrechts-Universität zu Kiel
Olshausenstraße 40,   D-24098 Kiel, Germany
phone: (0431) 880-7271, -7274, -7270
fax  : (0431) 880-7613
email: (mh | wg | up}@informatik.uni-kiel.de,  wg@acm.org