Das Herbstsemester 2020 findet in einer gemischten Form aus Online- und Präsenzunterricht statt.
Bitte lesen Sie die publizierten Informationen zu den einzelnen Lehrveranstaltungen genau.

263-4630-00L  Computer-Aided Modelling and Reasoning

SemesterHerbstsemester 2018
DozierendeNoch nicht bekannt
Periodizitätjährlich wiederkehrende Veranstaltung
LehrveranstaltungFindet dieses Semester nicht statt.
LehrspracheEnglisch
KommentarTakes place next spring semester (SS19).

In the Master Programme max. 10 credits can be accounted by Labs on top of the Interfocus Courses. Additional Labs will be listed on the Addendum.



Katalogdaten

KurzbeschreibungThe "computer-aided modelling and reasoning" lab is a hands-on course about using an interactive theorem prover to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The lab has two parts: The first introduces various modelling and proof techniques. The second part consists of a project in which the students apply these techniques
LernzielThe students learn to effectively use a theorem prover to create unambiguous models and rigorously analyse them. They learn how to write precise and concise specifications, to exploit the theorem prover as a tool for checking and analysing such models and for taming their complexity, and to extract certified executable implementations from such specifications.
InhaltThe "computer-aided modelling and reasoning" lab is a hands-on course about using an interactive theorem prover to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The focus is on applying logical methods to concrete problems supported by a theorem prover. The course will demonstrate the challenges of formal rigor, but also the benefits of machine support in modelling, proving and validating.

The lab will have two parts: The first part introduces basic and advanced modelling techniques (functional programs, inductive definitions, modules), the associated proof techniques (term rewriting, resolution, induction, proof automation), and compilation of the models to certified executable code. In the second part, the students work in teams of two on a project assignment in which they apply these techniques: they build a formal model and prove its desired properties. The project lies in the area of programming languages, model checking, or information security.
LiteraturTextbook: Tobias Nipkow, Gerwin Klein. Concrete Semantics, part 1 (www.concrete-semantics.org)

Leistungskontrolle

Information zur Leistungskontrolle (gültig bis die Lerneinheit neu gelesen wird)
Leistungskontrolle als Semesterkurs
ECTS Kreditpunkte8 KP
Prüfende
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üfungsmodusAll participating students will take part in a mandatory longer-term project. The final grade will be composed as follows: 60% exam and 40% project work. Computer-based exam.
Hilfsmittel schriftlichKeine
Online-PrüfungDie Prüfung kann am Computer stattfinden.
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.

Lehrveranstaltungen

NummerTitelUmfangDozierende
263-4630-00 PComputer-Aided Modelling and Reasoning
Findet dieses Semester nicht statt.
7 Std.Noch nicht bekannt

Gruppen

Keine Informationen zu Gruppen vorhanden.

Einschränkungen

Keine zusätzlichen Belegungseinschränkungen vorhanden.

Angeboten in

StudiengangBereichTyp
Informatik MasterWahlfächer der Vertiefung General StudiesWInformation
Informatik MasterWahlfächer der Vertiefung in Software EngineeringWInformation
Informatik MasterWahlfächer der Vertiefung in Information SecurityWInformation