Modulbeschreibung

Modul: Softwareverifikation

Lehrveranstaltungen:

TitelTypSWSZeitraum
SoftwareverifikationVorlesung2Wintersemester
SoftwareverifikationGruppenübung2Wintersemester

Modulverantwortlich:

Prof. Sibylle Schupp

Zulassungsvoraussetzungen:

Keine

Empfohlene Vorkenntnisse:

  • Automatentheorie und formale Sprachen
  • Computational logic
  • Objekt-orientiere Programmierung, Algorithmen und Datenstrukturen
  • Funktionales Programmieren oder Prozedurales Programmieren
  • Nebenläufigkeit

Modulziele / angestrebte Lernergebnisse:

Fachkompetenz

Wissen

Students apply the major verification techniques in model checking and deductive verification. They explain in formal terms syntax and semantics of the underlying logics, and assess the expressivity of different logics as well as their limitations. They classify formal properties of software systems. They find flaws in formal arguments, arising from modeling artifacts or underspecification. 

Fertigkeiten

Students formulate provable properties of a software system in a formal language. They develop logic-based models that properly abstract from the software under verification and, where necessary, adapt model or property. They construct proofs and property checks by hand or using tools for model checking or deductive verification, and reflect on the scope of the results. Presented with a verification problem in natural language, they select the appropriate verification technique and justify their choice.   

Personale Kompetenzen

Sozialkompetenz

Students discuss relevant topics in class. They defend their solutions orally. They communicate in English. 

Selbstständigkeit

Using accompanying on-line material for self study, students can assess their level of knowledge continuously and adjust it appropriately.  Working on exercise problems, they receive additional feedback. Within limits, they can set their own learning goals. Upon successful completion, students can identify and precisely formulate new problems in academic or applied research in the field of software verification. Within this field, they can conduct independent studies to acquire the necessary competencies and compile their findings in academic reports. They can devise plans to arrive at new solutions or assess existing ones. 

Leistungspunkte Modul:

6 LP

Studienleistung:

Klausur

Arbeitsaufwand in Stunden:

Eigenstudium: 124, Präsenzstudium: 56


Lehrveranstaltung: Softwareverifikation

Dozent:

Sibylle Schupp

Sprache:

Englisch

Zeitraum:

Wintersemester

Inhalt:

  • Syntax and semantics of logic-based systems
  • Deductive verification
    • Specification
    • Proof obligations
    • Program properties
    • Automated vs. interactive theorem proving
  • Model checking
    • Foundations
    • Property languages
    • Tool support
  • Timed automata
  • Recent developments of verification techniques and applications

Literatur:

  • C. Baier and J-P. Katoen, Principles of Model Checking, MIT Press 2007.
  • M. Huth and M. Bryan, Logic in Computer Science. Modelling and Reasoning about Systems, 2nd Edition, 2004.
  • Selected Research Papers