Seminartermin

Folien mit Terminen und Hinweisen

Contents

Today's software as well as hardware designs are getting more and more involved. Verification efficiency or even decidability strongly depends on the complexity of a given system model. One of the most promising techniques to handle complex systems is the application of different abstraction methods. Abstraction permits a great reduction in verification effort or even allows to verify systems that otherwise could not be analyzed (e.g. many infinite--state systems).

We will discuss different models, e.g. formal models, concurrent or pointer--manipulating programs and probabilistic systems, as well as different abstraction techniques. Based on the abstracted model's verification one tries to derive the validity of the desired properties in the actual system. In some cases the abstraction may be too coarse making refinement necessary.

Requirements

• Vordiplom Informatik or Bachelor in Computer Science
• The written exposition and the presentation must be done in either german or english.
• At least one of the following lectures:
  • Model Checking
  • Advanced Model Checking
  • Semantics and Verification of Software
• LTL and CTL are well-known

Topics (Papers)

Contact