2D5333 Programverifiering, kursadministration, 1996 per 4

HANDLEDNING: Kortare frågor svarar jag på när jag inte sitter i sammanträde. Email går också bra. För längre frågor (svar) får vi boka in en tid.

DELTAGARE: Saknas du nedan, maila mig!
johanh,henrik,jbm,gunnar,arve,berg,staffanu,pl, d92-tma@nada.kth.se,d92-ash,d92-mlo,d91-ewi,d91-mti, josev@it.kth.se,fredrik@e.kth.se,gunnaro@it.kth.se, mko@theophys.kth.se,

Presentationer :

Alexander : Parnas: Teaching Programming..(2) 25/3
Jonas : Rosenblum.. (4) 25/3 (?)
Lasse: Parnas et al: Precise Documentation.. 29/3
Mikael : Sommerville, (Jacky?) 29/3
26/4 : Fredrik : Evans et al (LCLint) (Lokal: F24)
26/4 : Gunnar: Johnsson/ Butler
3/5 : Martin : Broy (Lokal: 1537 OB2)
3/5 : Tomas : Ciaccia, m fl.
3/5 : Henrik/Linda : Klarlund/ Arnborg

Föreläsningar


25/3, 1537 Föreläsning + seminariediskussion
29/3 i sal C210A Osquars Backe 9, seminariediskussion och genomgång av hemtalsomgång 2.
22/4 i 1537 OB2:slutet av algebraisk programspecificering och början av metoder för analys av system med ändliga tillståndsmängder; Nitpick och satisfierbarhetsformuleringar.
Fr 26/4 10-12: Föredrag av Fredrik och Gunnar, examinator Henrik. OBS lokal: F24, Sing-Sing.
Må 29/4 13-15, 1537: Connectorer, temporallogiker (Garlan, Clarke)
Fr 3/5, 10-12, 1537: Diskussion av Broy, Ciaccia, Ciaccia, Klarlund/Arnborg
Må 6/5 13-15, 1537: Automater på oändliga strängar och träd.
Fr 10/5 10-12 F24, Sing-Sing:

Gästföreläsning

Må 13/5 kl 13-15 i 1537: Lars-Henrik Eriksson, Logikkonsult NP AB, ger exempel på praktikfall och verktyg som används i specifikation och verifiering av program och system (1537, Osquars Backe 2).

Kurslitteratur mm

KURSBOKEN har kommit 25/3, pris 310:- inkl moms. THS bokhandel Glaskupan.

KURSBUNTEN: 6 delar utdelade: 1: Kursprogram + bunt; 2: Anteckningar om ... 3: Hints for Specifiers, 4: A course on Formal methods 5: Model Checking and abstraction, 6: Operational Profiles...

MANUALER. A Guide to Larch Prover + LSL handbook App a
Nitpick Manual LCLint 1.4 manual (version 2.0 finns på kursdirectory)
ÄNDRINGAR:
15 ersätts av en annan rapport från samma grupp: RS-95-21.
13 (W Thomas om omega-automater) utgar.

Saknar du ngt - säg till!

Labbinfo

Hemuppgift 1

Hemuppgift 2

Hint-tal 2
Hint-tal 3
Hint 2-tal 3

PROGRAMBIBLIOTEK: Program som ska användas i hemtal 2 finns på
/afs/nada.kth.se/misc/tcs/pver (läs README)
På ..../Z finns Z-standard och Z-sammanfattning (2sidor)
På ...../nitpick/npex finns exempel på indata till Nitpick

NEWSGRUPPER med anknytning till kursen: comp.specification.z
comp.specification.larch
comp.specification.misc

Till kurssidan

Stefan