263-2812-00L  Program Verification

SemesterFrühjahrssemester 2022
DozierendeP. Müller
Periodizitätjährlich wiederkehrende Veranstaltung
LehrspracheEnglisch
KommentarMaximale Teilnehmerzahl: 30.



Lehrveranstaltungen

NummerTitelUmfangDozierende
263-2812-00 GProgram Verification Für Fachstudierende und Hörer/-innen ist eine Spezialbewilligung der Dozierenden notwendig.3 Std.
Mi09:15-12:00CAB G 56 »
P. Müller
263-2812-00 AProgram Verification Für Fachstudierende und Hörer/-innen ist eine Spezialbewilligung der Dozierenden notwendig.1 Std.P. Müller

Katalogdaten

KurzbeschreibungA hands-on introduction to the theory and construction of deductive program verifiers, covering both powerful techniques for formal program reasoning, and a perspective over the tool stack making up modern verification tools.
LernzielStudents will earn the necessary skills for designing, developing, and applying deductive verification tools that enable the modular verification of complex software, including features challenging for reasoning such as heap-based mutable data and concurrency. Students will learn both a variety of fundamental reasoning principles, and how these reasoning ideas can be made practical via automatic tools.

By the end of the course, students should have a good working understanding and decisions involved with designing and building practical verification tools, including the underlying theory. They will also be able to apply such tools to develop formally-verified programs.
InhaltThe course will cover verification techniques and ways to automate them by introducing a verifier for a small core language and then progressively enriching the language with advanced features such as a mutable heap and concurrency. For each language extension, the course will explain the necessary reasoning principles, specification techniques, and tool support. In particular, it will introduce SMT solvers to prove logical formulas, intermediate verification languages to encode verification problems, and source code verifiers to handle feature-rich languages. The course will intermix technical content with hands-on experience.
SkriptThe slides will be available online.
LiteraturWill be announced in the lecture.
Voraussetzungen / BesonderesA basic familiarity with propositional and first-order logic will be assumed. Courses with an emphasis on formal reasoning about programs (such as Formal Methods and Functional Programming) are advantageous background, but are not a requirement.

Leistungskontrolle

Information zur Leistungskontrolle (gültig bis die Lerneinheit neu gelesen wird)
Leistungskontrolle als Semesterkurs
ECTS Kreditpunkte5 KP
PrüfendeP. Müller
Formbenotete Semesterleistung
PrüfungsspracheEnglisch
RepetitionRepetition nur nach erneuter Belegung der Lerneinheit möglich.
Zusatzinformation zum PrüfungsmodusThe grade for the course is determined by two projects, each with a final presentation. The weight of each project will be announced at the beginning of the course.

Last cancellation/deregistration date for this graded semester performance: end of week 3 of the semester. Please note that after that date, no deregistration will be accepted and a "no show" will appear on your transcript.

Lernmaterialien

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

Gruppen

Keine Informationen zu Gruppen vorhanden.

Einschränkungen

Allgemein : Für Fachstudierende und Hörer/-innen ist eine Spezialbewilligung der Dozierenden notwendig
PlätzeMaximal 30
VorrangDie Belegung der Lerneinheit ist nur durch die primäre Zielgruppe möglich
Primäre ZielgruppeInformatik MSc (263000)
WartelisteBis 24.02.2022

Angeboten in

StudiengangBereichTyp
CAS in InformatikVertiefungsfächer und WahlfächerWInformation
Informatik MasterWahlfächerWInformation
Informatik MasterWahlfächer der Vertiefung General StudiesWInformation
Informatik MasterErgänzung in Programming Languages and Software EngineeringWInformation