Department of Information and Computing Sciences

Departement Informatica Onderwijs
Bachelor Informatica Informatiekunde Kunstmatige intelligentie Master Computing Science Game&Media Technology Artifical Intelligence 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 2 (week 46 through 5, i.e., 14-11-2016 through 3-2-2017; retake week 16)
Timeslot:C12+B4
Participants:up till now 7 subscriptions
Schedule:Official schedule representation can be found in Osiris
Teachers:Dit is een oud rooster!
formgrouptimeweekroomteacher
lab session group 1 Mon 15.15-17.0046-51 UNNIK-103
2-4 UNNIK-103
lecture   Mon 13.15-15.0046-51 UNNIK-313 Wishnu Prasetya
 
2-4 UNNIK-313
Thu 15.15-17.0046-47 ANDRO-C019
48-51 BBG-020
2-4 BBG-020
Exam:
week: 41Wed 11-10-20178.30-10.30 uurroom: BBG-001
week: 45Wed 8-11-20179.00-12.00 uurroom: BBG-001
week: 1Tue 2-1-201817.00-20.00 uurroom: UNNIK-220retake exam
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. We will discuss several common ways to define the semantic of programs, from which correctness can be defined and proven. We will discuss the predicate transformation technique, which you can use to symbolically execute a program to calculate its range of input or output. We will discuss several model checking techniques, that can be used to fully verify the model of a program, even if the number of possible executions is infinite. We will also discuss higher order theorem proving. Verification in this setting is usually not fully automatic, but it is very expressive, and thus provides at least an alternative when a verification problem cannot be suitably mapped to one of the above solutions.

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

  • program semantics: operational, denotational, axiomatic.
  • formalisms to express programs' correctness: Hoare-style, LTL, CTL, higher order logic, CSP.
  • automated verification techniques: predicate transformer, model checking (LTL,, CTL, symbolic), tactic-based theorem proving, refinement checking.
Additionally, to acquire hands-on experience with :
  • using a verification tool to model a problem and conduct a verification of its solution.
  • implementing a verification technique.
  • embedding a simple programming language in a higher order theorem prover, and to use it to prove the correctness of some example programs.
Literature:Lecture notes, on-line documentation, and papers.
Course form:Lectures.
Exam form:In principle 40% projects, 60% 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:As in the Education and Examinations Regulation (EER/OER). Additionally participation in the projects and assignments are mandatory.
wijzigen?