TDDE34 · 6 hp · Avancerad nivå (A1N) · Informationsteknologi, Datateknik, Datavetenskap
Mjukvaruverifiering
Ges · nästa start VT 2027
55 %
klarade senaste ordinarie tentan
TEN1 · 5 jun 2026 · 22 studenter
76 %
klarade ordinarie tentorna, alla tillfällen de senaste 5 åren
TEN1 · 90 studenter
Ovanligt svår 2025/26
55 % klarade ordinarie tentan läsåret 2025/26 (22 studenter), mot 82 % i snitt åren innan (68 studenter).
Ingår i 5 program
Tentamen
TEN1 Skriftlig tentamen
- 5
- 4
- 3
- U
Ordinarie tentor
76 % godkända · 90 studenter
- 55 %22
- 79 %14
- 87 %23
- 75 %16
- 87 %15
Omtentor
88 % godkända · 8 studenter
- 88 %8
- Klarar omtentan: 88 % (8 studenter), jämfört med 76 % (90 studenter) på ordinarie
- Får 4 eller 5: 37 % (98 studenter)
Visa små tillfällen (8)
Tillfällen med färre än 5 studenter, ofta tillgodoräknanden eller specialtillfällen. De ingår inte i någon siffra på sidan.
- 0 %1
- 33 %3
- 100 %1
- 67 %3
- 100 %4
- 50 %2
- 0 %1
- 100 %1
Övriga moment
Deltentor, inlämningar och laborationer. De ingår inte i siffrorna överst.
Inlämning eller laboration
LAB1 Laborationer
- G
Ordinarie tillfällen
100 % godkända · 76 studenter
- 100 %16
- 100 %18
- 100 %11
- 100 %16
- 100 %15
Senare tillfällen
100 % godkända · 7 studenter
- 100 %7
- Klarar ett senare tillfälle: 100 % (7 studenter), jämfört med 100 % (76 studenter) på ordinarie
Visa små tillfällen (6)
Tillfällen med färre än 5 studenter, ofta tillgodoräknanden eller specialtillfällen. De ingår inte i någon siffra på sidan.
- 100 %1
- 100 %1
- 100 %2
- 100 %2
- 100 %1
- 100 %1
Om kursen
Mål
Kursen är en introduktion till både teorin och utövandet avmjukvaruverifiering. Efter avslutad kurs ska studenten kunna:
- Demonstrera kännedom om de principer som ligger bakom olika mjukvaruverifieringsmetoder som Hoare logik, satisfierbarhet modulo teori (smt) och abstrakt tolkning.
- Tillämpa existerande tekniker för att analysera och verifiera mjukvaran.
- Beskriva fördelar, begränsningar och forskningsutmaningar av mjukvaruverifiering
Innehåll
- Transitionsystem
- Operationell och axiomatisk semantik
- Hoare logik
- Satisfierbarhet modulo teori (SMT)
- Invariant generering
- Abstrakt tolkning
- Examinator
- Ahmed Rezine
- Schemalagd tid
- 48 h
- Huvudområde
- Informationsteknologi, Datateknik, Datavetenskap