Humboldt-Universität zu Berlin - Mathematisch-Naturwissenschaftliche Fakultät - Software Engineering

Softwareverifikation

Das Ziel des Proseminars ist es, theoretisches und praktisches Wissen über die essenziellen Softwareverifikationstechniken zu vermitteln. Speziell werden Verifikationstechniken bezüglich Echtzeiteigenschaften und probabilistischen Eigenschaften vorgestellt. Angewendet werden sollen die Techniken auf realen Source Code. Voraussetzung dafür ist die Kenntnis der notwendigen Verfahren. Die Studenten sollen befähigt werden, eigenständig wissenschaftlich zu arbeiten.

 

 

Wann und Wo

Proseminar: Montag, 11-13 Uhr, RUD 26, 1.308

Wer

Dozent: Dr. Esteban Pavese

Beschreibung und Aufbau der Lehrveranstaltung

Vorsicht: dieser Kurs wird in englischer Sprache gehalten.

 

Software verification and validation (V&V) have been defined as the processes of checking whether a software system meets its needs. The main difference between Validation and Verification is that validation aims at checking that the software meets the stakeholders needs, while verification aims at checking that it complies with its specifications. Since specifications can be written formally, they are good candidates for automatic and exhaustive procedures that can check whether a system meets them successfully.

 

In this seminar, students will be introduced to the basic concepts that make software verification work. Students will also learn about current tools and research activities related to the subject. These include:

  • Software modellling and specification languages;
  • Exhaustive verification approaches (i.e., model checking);
  • Formal semantics of programs;
  • Source-code verification, challenges and approaches;
  • Testing strategies, testing vs. verification;

 

Requirements: the seminar has no initial requirements, no previous knowledge will be assumed. A good grasp of propositional and first-order logic is a plus.

 

Seminar work schedule and calendar:

 

The seminar will involve three distinct parts. The first part will be an introduction to the topics described above. During this first part of the seminar, a collection of research papers and book chapters on the subject will be available for the students. Each student will be required to pick one of these writings, on which a report will be due by the end of the semester.

During the second part of the seminar, we will have group discussions on the chosen report topics. After this discussion, the third part will consist of lectures specifically focused on these topics. In such a way the last part of the seminar will be geared towards the students' specific interests.

As a result, many topics will arise that can easily be turned into a starting point for a B.Sc.  or  M.Sc. thesis.

 

The calendar will be updated shortly.

 

Evaluation: the seminar will only involve a written report turned in by the student.