Department of Information and Computing Sciences

Departement Informatica Onderwijs
Bachelor Informatica Informatiekunde Kunstmatige intelligentie Master Computing Science Game&Media Technology Artifical Intelligence Human Computer Interaction Business Informatics

Onderwijs Informatica en Informatiekunde

Vak-informatie Informatica en Informatiekunde

Program semantics and verification

Website:website containing additional information
Course code:INFOMPSV
Credits:7.5 ECTS
Period:period 1 (week 36 through 45, i.e., 3-9-2020 through 6-11-2020; retake week 1)
Timeslot:A
Participants:up till now 28 subscriptions
Schedule:Official schedule representation can be found in MyTimetable
Teachers:
formgrouptimeweekroomteacher
lecture          Wishnu Prasetya
Anna-Lena Lamprecht
Contents:Most modern software is quite complex. The most widely used approach to verify them is still by testing, which is inherently incomplete and hard to scale up to cover the complexity. In this course we will discuss a number of advanced validation and verification techniques that go far beyond ad-hoc testing. Exploiting them is an important key towards more reliable complex software. We will in particular focus on techniques that can be automated, or at least partially automated:
  • Predicate transformation technique, which you can use to symbolically execute a program to calculate its range of input or output. This leads to the bounded but symbolic and fully automated verification technique.
  • Common automated theorem proving techniques, used as the back-end of symbolic execution based verification.
  • We will also discuss several common ways to define the semantic of programs, from which correctness can be defined and proven.
  • Model checking techniques, that can be used to either fully verify a model of a program, even if the number of possible executions is infinite, or to boundedly verify the program itself.

Learning goals: to become familiar with, and acquire insight on the underlying concepts of:

  • program semantics: axiomatic and symbolic.
  • formalisms to express programs' correctness: Hoare-style, temporal logic based (LTL and CTL), algebraic (CSP).
  • automated verification techniques: predicate transformation/symbolic execution, automated theorem proving, model checking (LTL, CTL, symbolic), refinement checking.
Additionally, to acquire hands-on experience with :
  • implementing and optimizing a verification technique.
  • using a verification tool to model a problem and conduct a verification of its solution.

Prerequisites: background in predicate logic, experience with a functional programming language, e.g. Haskell or ML.

Literature:Lecture notes, on-line documentation, and papers.
Course form:Lectures.
Exam form:In principle 50% projects, 50% exams. This can be changed depending on the composition of the projects, but in any case the exam-form and grading will be announced and fixed at the start of the course.
Minimum effort to qualify for 2nd chance exam:Eligibility to the resit exam: conform to the University regulation. The most important part of this is that your standing final result should be at least 4. Also note that resit is not possible if you already passed the course.
wijzigen?