Text in english

Ausgewählte Themen der Korrektheit und Semantik in Programmiersprachen

Kurs nur in Deutsch

Semesterwochenstunden:

4

Leistungspunkte:

5

Vorkenntnisse:

Programmieren, Programmiersprachen.

Veranstaltungstyp:

Vorlesung mit Laborübungen

Semesterturnus:

Winter- bzw. Sommersemester

Arbeitsaufwand:

150 Stunden, davon
65 Stunden Präsenzzeit
85 Stunden Vor- und Nachbereitung

Beitrag zu den Zielen des Studiengangs:

Vertiefung in Softwareengineering und Technologie der Programmiersprachen. Methoden zum Entwickeln sicherer Softwaresysteme.

Lernziel:

Bei Abschluss des Lernprozesses wird der erfolgreiche Studierende in der Lage sein, Anforderungen an Software mit Mitteln der formalen Logik zu analysieren, zu spezifizieren, korrekte Implementationen zu entwickeln und die Korrektheit gegen die Spezifikation zu beweisen.

Schlüsselqualifikationen:

Abstraktionsvermögen

Lehrinhalte:

Embedded Devices dringen in nahezu jeden Bereich des täglichen Lebens vor. Damit nimmt die Bedeutung der Sicherheit, Zuverlässigkeit und Fehlerfreiheit von Software immer mehr Raum ein. Bei höchsten Anforderungen an die Fehlerfreiheit ist der Einsatz von mathematischen Werkzeugen zum Nachweis der Korrektheit eines Programms heute Stand der Wissenschaft.  

Anhand des Buchs “Software Foundations” von Benjamin Pierce oder "Certified Programming with Dependent Types" von Adam Chlipala, werden die Techniken untersucht mit denen Eigenschaften von Programmen beschrieben und mit Werkzeugunterstützung nachgewiesen werden können:

  • Anwendung von Logik zur Spezifikation und Rechtfertigung von Programmeigenschaften
  • Anwendung von Beweisassistenten im Nachweis von Programmeigenschaften
  • Funktionales Programmieren als Bindeglied zwischen Logik und Programmiersprachen
  • Typen zur Spezifikation von Programmeigenschaften und deren Nachweis durch Typ-Prüfung des Compilers.
Der Schwerpunkt liegt auf praktischen Aspekten: Die erlernten Techniken werden im Labor mit einem Beweisassistenten, z.B. Coq eingeübt. 

Literatur:

  • Benjamin Pierce, et. al., Software Foundations. http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
  • Adam Chlipala, Certified Programming with Dependent Types", The MIT Press, 2013.
  • Andrew Appel, Program Logics for Certified Compilers, Cambridge University Press, 2014.
  • Benjamin Pierce ed., Advanced Topics in Types and Programming Languages, The MIT Press, 2005.
  • Benjamin Pierce, Types and Programming Languages, The MIT Press, 2002.

Bemerkungen:

Der Kurs findet ausschliesslich in deutscher Sprache statt. Fähigkeit Texte in englischer Sprache lesen und verstehen zu können ist Voraussetzung.

Leistungsnachweis:

Mündliche Befragung 20 min.

Zulassungsvoraussetzungen:

 

Hilfsmittel:

 

Modulverantwortliche/r:

Prof. Dr. Trommler





TH Nürnberg
Fakultät Informatik
Webmaster-IN



Root- Zertifikat

© 2019 Fakultät Informatik