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 verification

Te lang geleden voor docent- en roosterinformatie
Website:website containing additional information
Note:No up-to-date course description available.
Text below is from year 2008/2009

Most modern software is quite complex. The most widely used approach to verify them is still by conducting ad-hoc testing, which is not a realiable and scalable way to safeguard against fatal and costly errors. However over the years people have actually invented various clever technologies for validation and verification that go far beyond ad-hoc testing. Exploiting these technologies is the key towards reliable complex software. This course will introduces you to some of these advanced technologies. In particular we will focus on some fully automatic technologies and on a higher-order based technique.

Model checking is an example of a fully automatic technique that we will discuss. Abstractly, it is a very clever way to explore all possible behavior of a program. So, unlike ordinary testing, model checking guarantees complete coverage! However, model checking only works on finite state programs.

We will also discuss test generation, which is also an automated technique ---in particular we will look at techniques to more cleverly generate the test cases (rather than just blindly random them). It is still a testing approach, so it is not as complete as model checking. Still, it is a low-cost approach, which can be a useful complement when model checking cannot be applied.

To handle programs with infinite state space we have to turn to a more generic approach called theorem proving. Modern theorem proving tools are usually based on very expressive logics which make them very versatile. Although in principle theorem proving is not an automated approach, modern tools do come with powerful automation libraries. Because of their versatility they potentially have many applications.

In addition to discussing techniques we will also show a range of tools implementing the techniques, e.g. HOL, SPIN, FDR, ESC/Java ...

The course includes lab sessions and assignments to give you first hand experience with some of those tools.

Literature:May change!
On-line documentation and articles
Course form:Lectures + programming training.
Exam form:40% assignments, 20% seminars, 10% paper review, 30% exam. This may change depending on the number of participants.
Minimum effort to qualify for 2nd chance exam:To qualify for the retake exam, the grade of the original must be at least 4.

Course outline:

  1. Hoare logic, specifying Java programs, and automated testing.
  2. Modelling concurrent systems in Promela and model checking with SPIN
  3. Symbolic model checking, and model checking in SMV
  4. Modelling in Higher Order Logic and theorem proving in HOL
  5. Selected topics in automated software testing