Introduction to automatic verification 2014VT Status Archive School Computer and Information Science (CIS) Division Owner Ahmed Rezine

Log in

---

Course plan

8 lectures

lectures, reading assignments and an examination seminar

Recommended for

The course was last given

Goals

After the course, the students will be able to:
* model computer algorithms, protocols, components or systems as (possibly augmented) labeled transition systems
* specify safety and liveness correctness criteria using a (probabilistic) temporal logic
* understand what it means for a model to verify a correctness property
* understand the advantages and limitations of automatic verification
* apply a representative tool for plain, timed and probabilistic transition systems

Prerequisites

Basic notions in automata theory and logic

Organization

lectures, reading assignments and examination seminar

Contents

Introduction to model checking and temporal logic. Discussion and application of explicit, symbolic (bdd, sat based, predicate abstraction, counter example guided abstraction), timed, probabilistic and statistical model checking.

Literature

* Lecture material
* Model Checking Clarke, Grumberg & Peled, The MIT Press, 0262032708, 978-0262032704

Lecturers

Ahmed Rezine

Examiner

Ahmed Rezine

Examination

Modelling and verification of a case study, preferably from the student research, and discussion in a seminar session.

Credit

6pt

Comments

Page responsible: Anne Moe