Hoppa till huvudinnehållet
Till KTH:s startsida

FDD3457 Programsemantik och programanalys 6,0 hp

Administrera Om kursen

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 FDD3457 (VT 2019–)
Rubriker med innehåll från kursplan FDD3457 (VT 2019–) är markerade med en asterisk ( )

Innehåll och lärandemål

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:

  1. 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.
  2. Relatera de olika semantiska stilarna och jämföra deras styrkor och svagheter.
  3. Använda dessa semantiska stilar för programanalys, optimering och verifiering, både i teorin och som en grund för mjukvaruverktyg.
  4. Utöka ett programmeringsspråk med nya språkfunktioner, och förlänga dess semantik i enlighet därmed.
  5. Bevisa formella egenskaper hos en given semantik.

Kurslitteratur och förberedelser

Särskild behörighet

Ingen information tillagd

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, 6,0 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

Profile picture Dilian Gurov

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

EECS/Teoretisk datalogi

Huvudområde

Denna kurs tillhör inget huvudområde.

Utbildningsnivå

Forskarnivå

Påbyggnad

Ingen information tillagd

Kontaktperson

Dilian Gurov (dilian@kth.se)

Forskarkurs

Forskarkurser på EECS/Teoretisk datalogi