is geen recente vakbeschrijving beschikbaar.
Onderstaande tekst is een oude vakbeschrijving uit collegejaar 2005/2006.
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
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
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