263-2812-00L  Program Verification

SemesterFrühjahrssemester 2019
DozierendeA. J. Summers
Periodizitätjährlich wiederkehrende Veranstaltung
LehrspracheEnglisch
KommentarMaximale Teilnehmerzahl: 30.



Lehrveranstaltungen

NummerTitelUmfangDozierende
263-2812-00 VProgram Verification2 Std.
Mi09:15-11:00CAB G 52 »
A. J. Summers
263-2812-00 UProgram Verification1 Std.
Mi11:15-12:00CAB G 52 »
A. J. Summers
263-2812-00 AProgram Verification1 Std.A. J. Summers

Katalogdaten

KurzbeschreibungA hands-on introduction to the theory and construction of deductive software verifiers, covering both cutting-edge methodologies for formal program reasoning, and a perspective over the broad tool stacks making up modern verification tools.
LernzielStudents will earn the necessary skills for designing and developing deductive verification tools which can be applied to modularly analyse 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.

Students will be gain practical experience with reasoning tools at various levels of abstraction, from SAT and SMT solvers at the lowest level, up through intermediate verification languages and tools, to verifiers which target front-end code in executable languages.

By the end of the course, students should have a good working understanding and experience of the issues and decisions involved with designing and building practical verification tools, and the theoretical techniques which underpin them.
InhaltThe course will be organized around building up a "tool stack", starting at the lowest-level with background on SAT and SMT solving techniques, and working upwards through tools at progressively-higher levels of abstraction. The notion of intermediate verification languages will be explored, and the Boogie (Microsoft Research) and Viper (ETH) languages will be used in depth to tackle increasingly ambitious verification tasks.

The course will intermix technical content with hands-on experience; at each level of abstraction, we will understand who to build and use tools which can tackle specific program correctness problems, starting from simple puzzle solvers (Soduko) at the SAT level, and working upwards to full functional correctness of application-level code. This practical work will include three projects (typically worked on in pairs) spread throughout the course, which count towards the final grade. The graded projects are worth 40% in total, individually weighted at 14%, 13% and 13% respectively. The projects are a compulsory performance assessment; in this case, they need not be passed on their own, but will count 40% in all cases towards the final grading. An oral examination (worth the remaining 60% of the final grade) will examine the full technical content covered in the course.
SkriptHandouts (complementing the lecture material) and other materials will be available online.
LiteraturBackground reading material and links to tools will be published on the course website.
Voraussetzungen / BesonderesSome programming experience is essential, as the course contains several practical assignments. A 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üfendeA. J. Summers
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üfungsmodusmündlich 30 Minuten
Zusatzinformation zum PrüfungsmodusThe course includes three projects (typically worked on in pairs) spread throughout the course, which count towards the final grade. The graded projects are worth 40% in total, individually weighted at 14%, 13% and 13%, respectively. The projects are a compulsory performance assessment; in this case, they need not be passed on their own, but will count 40% in the same way in all cases towards the final grading. An oral examination (worth the remaining 60% of the final grade) will examine the full technical content covered in the course. The oral examination timetable includes 10 minutes spare for organisation/preparation between students - the actual discussion questions and answers will last for 20 minutes for each student.
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

PlätzeMaximal 30
VorrangDie Belegung der Lerneinheit ist nur durch die primäre Zielgruppe möglich
Primäre ZielgruppeInformatik MSc (263000)
WartelisteBis 21.02.2019

Angeboten in

StudiengangBereichTyp
CAS in InformatikFokusfächer und WahlfächerWInformation
Doktorat Departement InformatikLehrangebot Doktorat und PostdoktoratWInformation
Informatik MasterWahlfächer der Vertiefung General StudiesWInformation
Informatik MasterWahlfächer der Vertiefung in Software EngineeringWInformation