SluitenHelpPrint
Switch to English
Cursus: INFOPV
INFOPV
Programmaverificatie
Cursus informatieRooster
CursuscodeINFOPV
Studiepunten (ECTS)7,5
Categorie / NiveauM (Master)
CursustypeCursorisch onderwijs
VoertaalEngels
Aangeboden doorFaculteit Betawetenschappen; Onderwijsinstituut Informatica;
Contactpersoondr. S.W.B. Prasetya
Telefoon+31 30 2534090
E-mailS.W.B.Prasetya@uu.nl
Docenten
Docent
dr. S.W.B. Prasetya
Feedback en bereikbaarheid
Overige cursussen docent
Blok
1  (06-09-2010 t/m 12-11-2010)
Aanvangsblok
1
TimeslotB: DI-ochtend, DO-middag, DO-namiddag
Onderwijsvorm
Voltijd
Opmerkinghttp://www.cs.uu.nl/education/vak.php?vak=INFOPV
Cursusinschrijving geopendvanaf 21-06-2010 t/m 17-09-2010
Aanmeldingsprocedureadministratie onderwijsinstituut
Inschrijven via OSIRISJa
Inschrijven voor bijvakkersJa
VoorinschrijvingNee
WachtlijstNee
Plaatsingsprocedureadministratie onderwijsinstituut
Cursusdoelen
-
Inhoud

Er 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 state programs.

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 applications.

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 tools.

http://www.cs.uu.nl/education/vak.php?vak=INFOPV&jaar=2010

 

 

Ingangseisen
Je moet een geldige toelatingsbeschikking hebben
Verplicht materiaal
-
Aanbevolen materiaal
Internet pagina's
kan veranderen! On-line documentation and articles
Werkvormen (aanwezigheidsplicht)
Hoorcollege

Practicum (Verplicht)

Toetsen
Tentamen
Weging100
Minimum cijfer6

Beoordeling
70% assignments, 20% seminars, 10% participation. This may change depending on the number of participants.

SluitenHelpPrint
Switch to English