Goal of the course is
-
To introduce typical formalisms to express the correctness of programs. This covers: a Hoare style formalism, LTL and CTL temporal formalisms, and CSP formalism. Students are expected to be able to capture and express specifications in these formalisms.
-
To learn a number of basic model-checking algorithms. These include LTL model checking, CTL model checking, and CSP refinement checking. Students are expected to understand the algorithms.
-
To give students some experience in using model-checking technology. This includes using model checking tools like SPIN. Students are expected to become familiar with some model checkers.
-
To expose students to typical problems in the application of model checking, e.g. modelling and dealing with state explosion. Students are expected to be able to identify which modelling constructs can be used to model various concurrency situations, and to circumvent state explosion.
-
To introduce students to higher order theorem proving. Students are expected to be able to understand the underlying principle of modelling in a higher order logic (HOL), to be able to express program verification problems in the HOL notation, and to write proofs in HOL.
|
 |
|
|
The most widely used approach to verify software is still by conducting ad-hoc testing, which is not a realiable and scalable way to safeguard against fatal and costly errors. Over the years various clever technologies for validation and verification have been developed that go far beyond this primitive form of testing. This course introduces some of these advanced technologies, in particular some fully automatic technologies (such as model checking and test generation) and a higher-order based technique, called theorem proving. In addition to discussing techniques a range of tools implementing the techniques is covered.
|
|