2D5333 Programverifiering, kursuppläggning, 1996 per 4

Första föreläsningen 11 mars 1996 kl 13:15-15:00 i Nadas seminarierum 1537, Osquars Backe 2, plan 5. Föreläsningar och seminarier på svenska denna gång.

Preliminär Disposition

Under introduktionsföreläsningen ska vi hitta två gemensamma dubbeltimmar i undervisningsveckan(dvs v11-13 och v17-20). Den första för föreläsning och diskussion om teoristoffet (hålls till minsta möjliga) och den andra för diskussionsseminarier.
Reviderat schema med aktuell kursadministration.

Förslag: Må 13-15 Föreläsning, Fr 10-12 Redovisning/diskussion under Må 11 mars - fr 29 mars, må 22 april - fr 10 maj. OBS: till fredagstiden bör alla som avser att få poäng för kursen ha läst de artiklar som ska gås igenom.

1F Må 11/3     Introduktion/översikt, Historik. Floyd-Hoare-
  	         metoden. Välgrundade mängder och avslutning. 
1R Fr 15/3     Modellbaserad notation, Z  och Morgan/Dijkstras
                 notation. Förfining. Kod som specialfall av
                 specifikation. Utdelning av hemuppgift 1.
2F Må 18/3     Första ordningens språk. Ekvationer och 
                 omskrivning. Axiom, hypoteser, mekaniserade 
                 bevis. Knuth-Bendix metod.
2R Fr 22/3    Diskussion av Hoare-Wirth, Parnas, Parnas et al.
3F Må 25/3    Larch: LSL/LCL, LP, LCLint. (Inlämning av 
               hemuppgift 1, utdelning av uppgift 2)
3R Fr 29/3    Diskussion av Rosenblum, Sommerville Ch 8, Ch 9,
               Jacky.
4F Må 22/4    Gästföreläsare (industriorienterat)
4R Fr 26/4    Diskussion av Broy, Broy, Wing.
5F Må 29/4    MS- och temporallogiker. Automater på oändliga
  	         strängar och träd. Modellverifiering.
5R Fr 3/5     Diskussion av Ciaccia, Ciaccia, Clarke et al.
6F Må 6/5     Tekniska system med programvara och maskinvara.
                 Markovmodellering
6R Fr 10/5    Diskussion av Klarlund et al, Johnson-Butler.
7F Må 13/5    Realisering av verifieringsmetodik. (Inlämning av 
                 hemuppgift 2).
7R EÖ         Diskussion av Rosenbaum, Musa. Avslutning.

Litteratur.

Liknande Kurser

2G1301: Teori för distribuerade system
Models of Software systems
Methods of Software development
Björn Lispers planerade semantikkurs

Ingång till Nadas kursweb

Stefan