252-0058-00L  Formal Methods and Functional Programming

SemesterFrühjahrssemester 2018
DozierendeD. Basin, P. Müller
Periodizitätjährlich wiederkehrende Veranstaltung
LehrspracheEnglisch



Lehrveranstaltungen

NummerTitelUmfangDozierende
252-0058-00 VFormal Methods and Functional Programming4 Std.
Di10:15-12:00HG G 5 »
Do10:15-12:00HG G 5 »
13.03.10:15-11:00HG E 3 »
D. Basin, P. Müller
252-0058-00 UFormal Methods and Functional Programming2 Std.
Di13:15-15:00CAB G 52 »
13:15-15:00CHN D 46 »
13:15-15:00NO D 11 »
13:15-15:00NO E 11 »
Mi15:15-17:00CHN D 42 »
16:15-18:00NO C 6 »
11.07.10:15-12:00HG F 5 »
D. Basin, P. Müller

Katalogdaten

KurzbeschreibungIn this course, participants will learn about new ways of specifying, reasoning about, and developing programs and computer systems. The first half will focus on using functional programs to express and reason about computation. The second half presents methods for developing and verifying programs represented as discrete transition systems.
LernzielIn this course, participants will learn about new ways of specifying,
reasoning about, and developing programs and computer systems. Our objective is to help students raise their level of abstraction in modeling and implementing systems.
InhaltThe first part of the course will focus on designing and reasoning
about functional programs. Functional programs are mathematical
expressions that are evaluated and reasoned about much like ordinary
mathematical functions. As a result, these expressions are simple to
analyze and compose to implement large-scale programs. We will cover the mathematical foundations of functional programming, the lambda calculus, as well as higher-order programming, typing, and proofs of correctness.

The second part of the course will focus on deductive and algorithmic validation of programs modeled as transition systems. As an example of deductive verification, students will learn how to formalize the semantics of imperative programming languages and how to use a formal semantics to prove properties of languages and programs. As an example of algorithmic validation, the course will introduce model checking and apply it to programs and program designs.

Leistungskontrolle

Information zur Leistungskontrolle (gültig bis die Lerneinheit neu gelesen wird)
Leistungskontrolle als Semesterkurs
ECTS Kreditpunkte7 KP
PrüfendeP. Müller, D. Basin
FormSessionsprüfung
PrüfungsspracheEnglisch
RepetitionDie Leistungskontrolle wird nur in der Session nach der Lerneinheit angeboten. Die Repetition ist nur nach erneuter Belegung möglich.
Prüfungsmodusschriftlich 180 Minuten
Zusatzinformation zum PrüfungsmodusWe offer 2 graded quizzes, in the first and second half.
Each quiz will be 30 minutes and each will count 10% of the total grade.
Hilfsmittel schriftlichKeine
Diese Angaben können noch zu Semesterbeginn aktualisiert werden; verbindlich sind die Angaben auf dem Prüfungsplan.

Lernmaterialien

 
HauptlinkInformation
Es werden nur die öffentlichen Lernmaterialien aufgeführt.

Gruppen

Keine Informationen zu Gruppen vorhanden.

Einschränkungen

Keine zusätzlichen Belegungseinschränkungen vorhanden.

Angeboten in

StudiengangBereichTyp
Informatik BachelorObligatorische Fächer (4. Sem.)OInformation
Informatik BachelorGrundlagenfächerOInformation