Concurrency
Q1 2012, 5 ECTS
Kurset vil dække følgende emner:
- concurrency-mekanismer i Java,
- korrekthedsegenskaber (safety og liveness),
- modelbaseret design af concurrent programmer,
- endelige tilstandsmodeller,
- temporal-logik (LTL), og
- verifikation med Büchi-automater.
Deltagerne skal ved afslutningen af kurset kunne
- beskrive og anvende concurrency mekanismer i Java,
- konstruere modeller af concurrent systemer,
- formulere korrekthedsegenskaber,
- beskrive algoritmer for modelverifikation, og
- relatere resultater af modelverifikation til egenskaber ved Java-programmer.
Forelæser
Anders Møller <amoeller@cs.au.dk>
Materiale
Kurset tager udgangspunkt i følgende bog:
 |
[M&K] Jeff Magee og Jeff Kramer |
| Concurrency: State Models & Java Programming | |
| 2. udgave, Wiley, 2006 | |
| ISBN: 0470093560 / 0470093552 / 9780470093559 |
Desuden anvendes de første kapitler af denne:
 |
[B&K] Christel Baier og Joost-Pieter Katoen |
| Principles of Model Checking | |
| MIT Press, 2008 | |
| ISBN: 0-262-02649-X |
Begge bøger kan købes i Stakbogladen Naturfag.
Eksamen
Skriftlig eksamen (2 timer, uden bøger, noter, etc.).
Alle afleveringsopgaver skal være godkendt før man kan komme til eksamen. Hvis du har fået godkendt afleveringsopgaverne et tidligere år, så kontakt forelæseren.
Pensum er kapitlerne angivet i kursusplanen samt forelæsnings-slides og opgaver.