Dr. Calogero Zarba
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
- 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
THIS LECTURE HAS BEEN CANCELLED!