SluitenHelpPrint
Switch to English
Cursus: INFOPV
INFOPV
Programmaverificatie
Cursus informatieRooster
CursuscodeINFOPV
Studiepunten (ECTS)7,5
Categorie / NiveauM (Master)
CursustypeCursorisch onderwijs
VoertaalEngels
Aangeboden doorFaculteit Betawetenschappen; Graduate School of Natural Sciences;
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
3  (08-02-2016 t/m 22-04-2016)
Aanvangsblok
3
TimeslotD: WO-middag, WO-namiddag, Vrijdag
Onderwijsvorm
Voltijd
Opmerkinghttp://www.cs.uu.nl/education/vak.php?vak=INFOPV
Cursusinschrijving geopendvanaf 02-11-2015 t/m 29-11-2015
AanmeldingsprocedureOsiris
Inschrijven via OSIRISJa
Inschrijven voor bijvakkersJa
VoorinschrijvingNee
Na-inschrijvingJa
Na-inschrijving geopendvanaf 18-01-2016 t/m 19-01-2016
WachtlijstJa
Plaatsingsprocedureadministratie onderwijsinstituut
Cursusdoelen
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.
Inhoud
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.
Ingangseisen
Je moet een geldige toelatingsbeschikking hebben
Verplicht materiaal
Software
UA10078 XEmacs 21.4 HOL theorem prover COQ theorem prover SPIN model checker
Aanbevolen materiaal
Internet pagina's
kan veranderen! On-line documentation and articles
Werkvormen (aanwezigheidsplicht)
Hoorcollege

Practicum (Verplicht)

Toetsen
Eindresultaat
Weging100
Minimum cijfer6

SluitenHelpPrint
Switch to English