263-2812-00L  Program Verification

SemesterSpring Semester 2018
LecturersA. J. Summers
Periodicityyearly recurring course
Language of instructionEnglish
CommentNumber of participants limited to 30.



Courses

NumberTitleHoursLecturers
263-2812-00 VProgram Verification2 hrs
Wed09:15-11:00CAB G 52 »
A. J. Summers
263-2812-00 UProgram Verification1 hrs
Wed11:15-12:00CAB G 52 »
A. J. Summers
263-2812-00 AProgram Verification1 hrsA. J. Summers

Catalogue data

AbstractA 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.
ObjectiveStudents 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.
ContentThe 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 build small tools on top 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 mini-projects (each worth 10% of the final grade) spread throughout the course, which count towards the final grade. An oral examination (worth 70% of the final grade) will cover the technical content covered.
Lecture notesSlides and other materials will be available online.
LiteratureBackground reading material and links to tools will be published on the course website.
Prerequisites / NoticeSome 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.

Performance assessment

Performance assessment information (valid until the course unit is held again)
Performance assessment as a semester course
ECTS credits5 credits
ExaminersA. J. Summers
Typesession examination
Language of examinationEnglish
RepetitionThe performance assessment is only offered in the session after the course unit. Repetition only possible after re-enrolling.
Mode of examinationoral 20 minutes
Additional information on mode of examinationThe course includes three mini-projects (each worth 10% of the final grade) spread throughout the course, which count towards the final grade. An oral examination (worth 70% of the final grade) will cover the technical content covered.
This information can be updated until the beginning of the semester; information on the examination timetable is binding.

Learning materials

 
Main linkInformation
Only public learning materials are listed.

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 22.02.2018

Offered in

ProgrammeSectionType
CAS in Computer ScienceFocus Courses and ElectivesWInformation
Doctoral Department of Computer ScienceDoctoral and Post-Doctoral CoursesWInformation
Computer Science MasterElective Focus Courses General StudiesWInformation
Computer Science MasterFocus Elective Courses Software EngineeringWInformation