SluitenHelpPrint
Switch to English
Cursus: INFOMPSV
INFOMPSV
Programmasemantiek en -verificatie
Cursus informatieRooster
CursuscodeINFOMPSV
Studiepunten (ECTS)7,5
Categorie / NiveauM (Master)
CursustypeCursorisch onderwijs
VoertaalEngels
Aangeboden doorFaculteit Betawetenschappen; Graduate School of Natural Sciences; Graduate School of Natural Sciences;
Contactpersoondr. S.W.B. Prasetya
Telefoon+31 30 2534090
E-mailS.W.B.Prasetya@uu.nl
Docenten
Docent
dr. A.L. Lamprecht
Overige cursussen docent
Docent
dr. S.W.B. Prasetya
Overige cursussen docent
Contactpersoon van de cursus
dr. S.W.B. Prasetya
Overige cursussen docent
Blok
1-GS  (06-09-2021 t/m 12-11-2021)
Aanvangsblok
1-GS
TimeslotA: A (MA-ochtend, DI-namiddag, WO-ochtend)
Onderwijsvorm
Voltijd
Cursusinschrijving geopendvanaf 31-05-2021 t/m 27-06-2021
AanmeldingsprocedureOsiris
Inschrijven via OSIRISJa
Inschrijven voor bijvakkersJa
VoorinschrijvingNee
Na-inschrijvingJa
Na-inschrijving geopendvanaf 23-08-2021 t/m 20-09-2021
WachtlijstJa
Plaatsingsprocedureadministratie onderwijsinstituut
Cursusdoelen

Learning goals: to become familiar with, and acquire insight on the underlying concepts of:

  • program semantics: operational, denotational, axiomatic.
  • formalisms to express programs' correctness: Hoare-style, LTL, CTL, , CSP.
  • automated verification techniques: predicate transformation/symbolic execution, automated theorem proving, model checking (LTL,, CTL, symbolic), refinement checking.
Additionally, to acquire hands-on experience with :
  • implementing and optimizing a verification technique.
  • using a verification tool to model a problem and conduct a verification of its solution.

Assessment
In principle 15% assignments, 40% projects, 45% exams. This distribution can be changed depending on the composition of the projects, but in any case the exam form and grading will be announced and fixed at the start of the course.

To pass the course the average of the tests should be at least 5.0.

To qualify for a repair test, the grade of the original must be at least a 4.

The retake can replace one of the tests. So, the coverage of the retake is the same as the coverage of the test it replaces.


Prerequisites
Background in predicate logic, experience with a functional programming language, e.g. Haskell or ML.

Inhoud
Most modern software is quite complex.
The most widely used approach to verify them is still by testing, which is inherently incomplete and hard to scale up to cover the complexity.
In this course we will discuss a number of advanced validation and verification techniques that go far beyond ad-hoc testing.
Exploiting them is an important key towards more reliable complex software.

We will in particular focus on techniques that can be automated, or at least partially automated:
  • Predicate transformation technique, which you can use to symbolically execute a program to calculate its range of input or output. This leads to the bounded but symbolic and fully automated verification technique.
  • Common automated theorem proving techniques, used as the back-end of symbolic execution based verification.
  • We will also discuss several common ways to define the semantic of programs, from which correctness can be defined and proven.
  • Model checking techniques, that can be used to either fully verify a model of a program, even if the number of possible executions is infinite, or to boundedly verify the program itself.
Course form
Lectures, projects.

Literature
Lecture notes, on-line documentation, and papers.
Competenties
-
Ingangseisen
Je moet voldoen aan de volgende eisen
  • Toelatingsbeschikking voor de master toegekend
Verplicht materiaal
-
Aanbevolen materiaal
Software
Haskell (beschikbaar in MyWorkPlace) HOL (software alleen in CLZ) SPIN (beschikbaar in MyWorkPlace)
Werkvormen
Hoorcollege

Werkcollege

Toetsen
Eindresultaat
Weging100
Minimum cijfer-

SluitenHelpPrint
Switch to English