The spring semester 2021 will certainly take place online until Easter. Exceptions: Courses that can only be carried out with on-site presence. Please note the information provided by the lecturers.

263-2812-00L  Program Verification

SemesterSpring Semester 2021
LecturersP. Müller, C. Matheja
Periodicityyearly recurring course
Language of instructionEnglish
CommentNumber of participants limited to 30.



Catalogue data

AbstractA 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.
ObjectiveStudents 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.
ContentThe 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.
Lecture notesThe slides will be available online.
LiteratureWill be announced in the lecture.
Prerequisites / NoticeA 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.

Performance assessment

Performance assessment information (valid until the course unit is held again)
Performance assessment as a semester course
ECTS credits5 credits
ExaminersP. Müller, C. Matheja
Typegraded semester performance
Language of examinationEnglish
RepetitionRepetition only possible after re-enrolling for the course unit.
Additional information on mode of examinationThe 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.

Learning materials

 
Main linkInformation
Only public learning materials are listed.

Courses

NumberTitleHoursLecturers
263-2812-00 GProgram Verification3 hrs
Wed09-12CAB G 56 »
P. Müller, C. Matheja
263-2812-00 AProgram Verification1 hrsP. Müller, C. Matheja

Groups

No information on groups available.

Restrictions

Places30 at the most
PriorityRegistration for the course unit is only possible for the primary target group
Primary target groupComputer Science MSc (263000)
Waiting listuntil 25.02.2021

Offered in

ProgrammeSectionType
CAS in Computer ScienceFocus Courses and ElectivesWInformation
Cyber Security MasterElective CoursesWInformation
Computer Science MasterElective Focus Courses General StudiesWInformation
Computer Science MasterElective CoursesWInformation
Computer Science MasterFocus Elective Courses Software EngineeringWInformation
Computer Science MasterMinor in Programming Languages and Software EngineeringWInformation