Kursen består av föreläsningar, laborationer, ett seminarium och en skriftlig tentamen. Det finns sex hemtal som kamraträttas under föreläsningarna, och två laborationer.
FDD3557 Programsemantik och programanalys 7,5 hp
Att ge en semantik för ett programspråk betyder att ge en exakt definition av programbeteendet för program skrivna på detta språk. När språkets semantik har beskrivits formellt, kan man börja och bevisa olika programspråkegenskaper, bevisa korrektheten av programimplementeringar baserade på abstrakta maskiner, motivera olika programanalyser som används i syntaxorienterade redaktörer och programtransformationer som används i optimerande kompilatorer, och specificera och bevisa korrektheten hos konkreta program. Detta ger den formella grunden för ett antal olika programverktyg för programanalys, optimering och verifikation.
Information per kursomgång
Kursomgångar saknas för aktuella eller kommande terminer.
Kursplan som PDF
Notera: all information från kursplanen visas i tillgängligt format på denna sida.
Kursplan FDD3557 (VT 2023–)Information för forskarstuderande om när kursen ges
Kursen erbjuds vartannat år under period 4.
Rubriker med innehåll från kursplan FDD3557 (VT 2023–) är markerade med en asterisk ( )
Innehåll och lärandemål
Kursupplägg
Kursinnehåll
Del I. Operationell semantik och språkimplementering: naturlig semantik, strukturell operationell semantik, abstrakta maskiner, korrekt implementering av språk.
Del II. Denotationell semantik and programanalys: denotationell semantik, fixtpunktteori, programanalys och transformation.
Del III. Axiomatisk semantik and programverifikation: axiomatisk semantik, programspecifikation och verifikation, svagaste förutsättningar, generering av verifieringsvillkor.
Lärandemål
Efter avslutad kurs ska den framgångsrika doktoranden kunna:
- Redogöra för de huvudsakliga semantiska stilarna som används för att fånga programmens mening på ett formellt sätt, både i teori och på exempel.
- Relatera de olika semantiska stilarna och jämföra deras styrkor och svagheter.
- Använda dessa semantiska stilar för programanalys, optimering och verifiering, både i teorin och som en grund för mjukvaruverktyg.
- Utöka ett programmeringsspråk med nya språkfunktioner, och förlänga dess semantik i enlighet därmed.
- Bevisa formella egenskaper hos en given semantik.
Kurslitteratur och förberedelser
Särskild behörighet
Ingen information tillagd
Rekommenderade förkunskaper
Kurser i programmering, diskret matematik och matematisk logik.
Utrustning
Ingen information tillagd
Kurslitteratur
Nielson and Nielson "Semantics with Applications: An Appetizer", Springer-Verlag, 2007, ISBN: 978-1-84628-691-9. Research papers.
Examination och slutförande
När kurs inte längre ges har student möjlighet att examineras under ytterligare två läsår.
Betygsskala
P, F
Examination
- EXA1 - Examination, 7,5 hp, betygsskala: P, F
Examinator beslutar, baserat på rekommendation från KTH:s handläggare av stöd till studenter med funktionsnedsättning, om eventuell anpassad examination för studenter med dokumenterad, varaktig funktionsnedsättning.
Examinator får medge annan examinationsform vid omexamination av enstaka studenter.
Övriga krav för slutbetyg
För att klara kursen måste doktorander bli godkända på hemtalen, laborationsuppgifterna, seminariet och den skriftliga tentamen.
Möjlighet till komplettering
Ingen information tillagd
Möjlighet till plussning
Ingen information tillagd
Examinator
Etiskt förhållningssätt
- Vid grupparbete har alla i gruppen ansvar för gruppens arbete.
- Vid examination ska varje student ärligt redovisa hjälp som erhållits och källor som använts.
- Vid muntlig examination ska varje student kunna redogöra för hela uppgiften och hela lösningen.
Ytterligare information
Kursrum i Canvas
Registrerade studenter hittar information för genomförande av kursen i kursrummet i Canvas. En länk till kursrummet finns under fliken Studier i Personliga menyn vid kursstart.
Ges av
Huvudområde
Denna kurs tillhör inget huvudområde.
Utbildningsnivå
Forskarnivå
Påbyggnad
Ingen information tillagd
Kontaktperson
Dilian Gurov (dilian@kth.se)