Verification Techniques

Technische Universität Dresden Institut für Theoretische Informatik Lehrstuhl für Automatentheorie

Dr. Calogero Zarba

Course Description

Verification is the act of convincing oneself that a computer system correctly behaves according to its specification.

In this course we will cover the following verification techniques:

• Testing executes some computational models of the system according to a given coverage scheme. It can show the presence of errors but never the absence of errors.
• Algorithm verification (aka as model checking) consists in exhaustively exploring all the computational models of the system. It can show both the presence and the absence of errors; it is fully automatic but applicable only to finite-state systems.
• Deductive verification uses inference systems in order to formally prove that the system is correct. It can show the absence of errors but not the presence of errors; it can be applied to infinite-state systems but requires user interaction.
• Algorithm-deductive verification combines algorithm verification and deductive verification in order to verify infinite-state systems with reduced user interaction and greater automation degree. It can show both the presence and the absence of errors.

Time and place

Prerequisites

First-order logic.