Software is being used in all parts of daily life. It controls a multitude of systems such as cars, elevators, mobile phones, or production facilities. Software defects lead to increasing costs and can cause severe damage. In order to detect such bugs as early as possible, formal verification methods are applied. Such methods are able to analyze and verify software.

The topic of this seminar are advanced methods for verifying the quality and correctness of embedded software. Hence, these methods increase safety and reliability of the overall systems.

The seminar covers the following topics:

• Model checking of embedded software
• Architecture description languages
• Automatic generation of software tools
• Abstract interpretation
• Static analysis
• Abstraction techniques for model checking
• Symbolic representation of state spaces
• Constraint-based model checking

• First meeting: 03.08.2009, 10am, room 2323. Compulsory attendance!
• Presentations will be given at four dates: 01.12.2009, 08.12.2009, 15.12.2009, 22.12.2009 from 3pm to 5pm.

• Dr. rer. nat. Jörg Brauer
• Dr. rer. nat. Dominique Marcel Gückel (main contact person)
• Dipl.-Inform. Volker Kamin