VERIFIKACIJA SOFTVERA

Kurs verifikacija softvera je izborni kurs na master studijama za studente R i I smera. U okviru kursa proučavaju se različite tehnike verifikacije softvera, počevši od dinamičkih pristupa verifikaciji do naprednih tehnika statičke analize. Kurs je, u okviru vežbi, praktično orijentisan na savladavanje upotrebe različitih alata za verifikaciju softvera, a na predavanjima se prelaze osnovni koncepti i teorijske osnove oblasti. Neke od tema na kursu:

  • Tehnike testiranja
  • Alati za profajliranje i debagovanje
  • Statička analiza koda kroz preglede
  • Simboličko izvršavanje
  • SMT/SAT u verifikaciji softvera
  • Proveravanje modela
  • Semantika programskih jezika
  • Apstraktna interpretacija

Predmetni nastavnik:

Asistent:

Izborni predmet

  • 8 ESPB bodova
  • 2 časa predavanja
  • 3 časa vežbi

Predispitne obaveze (45 poena):

  • Seminarski rad samostalni (15 poena)
  • Seminarski rad u grupi (30 poena)

Završni ispit (55 poena):

  • Teorija (25+5 poena)
  • Zadaci (30 poena)
Da bi se položio ispit, neophodno je imati 51 poen, pri čemu je neophodno ostvariti bar 40% na teoriji na završnom ispitu (tj.~minimum 12 poena) i bar 40% na zadacima na završnom ispitu (tj. minimum 12 poena) i bar 40% na predispitnim obavezama (tj. minimum 18 poena).

Teorijski deo ispita polaže se pismeno, izvlači se pet ispitnih pitanja sa spiska ispitnih pitanja.
Studenti koji su zainteresovani za dodatnih 5 poena (za ukupan zbir 105) mogu da usmeno odgovaraju još jedno pitanje sa suženog spiska ispitnih pitanja za usmeni deo (u dodatnom terminu po dogovoru, nakon što završe sve druge ispitne obaveze).

Praktični deo ispita polaže se za računarima.

U terminu ispitnog roka možete polagati praktični deo ispita, teorijski deo ispita ili oba. Pred izlazak na ispit potrebno je preko forme u okviru strane kursa prijaviti namere (praktični, teorijski ili oba). Odbrana praktičnog projekta može i ne mora da prethodi izlasku na ispit.

Odbrane praktičnih projekata

Odbrana praktičnog projekta može i ne mora da prethodi izlasku na ispit. Termini odbrane projekata biće dogovoreni sa svakim timom pojedinačno nakon prijave da je projekat završen. Kada završite projekat, potrebno je da pošaljete mejl sa linkom na repozitorijum. Nakon što rad bude pregledan, dobićete informaciju da li ste ispunili tražene zahteve ili je potrebno još nešto da uradite. Kada bude sve ok, onda prelazimo na fazu dogovora termina odbrane.

U okviru projekta, potrebno je da bude napisan detaljan README fajl koji objašnjava
(1) na koji način se projekat može prevesti i pokrenuti (sve neophodne biblioteke, alati i zavisnosti)
(2) na koji način se izvršna verzija koristi (primeri upotrebe)
(3) koji ulazni primeri se mogu koristiti za upotrebu i testiranje programa.

Pored readme fajla, potrebno je da postoji i fajl SystemDescription (pdf ili tekstualni fajl) koji sadrži:
(1) opis problema
(2) opis arhitekture sistema (opis osnovnih modula implementacije),
(3) opis rešenja problema (osnovne ideje, obrazloženja za ključne odluke, opis osnovnog algoritma)

Svi koji prijave da je projekat završen pre

  • 24. 01., ukoliko je sve ok, imaće priliku da brane u nekom (dogovorenom) terminu između 1. i 10. 02.
  • 18. 02., ukoliko je sve ok, imaće priliku da brane u nekom (dogovorenom) terminu između 1. i 10. 03.
  • 20. 03., ukoliko je sve ok, imaće priliku da brane u nekom (dogovorenom) terminu između 1. i 10. 04.
  • 20. 04., ukoliko je sve ok, imaće priliku da brane u nekom (dogovorenom) terminu između 1. i 10. 05.
Kasnija odbrana je, po potrebi, moguća (npr prijava završenog rada u januaru, a odbrana u martu), ali najkasnija prijava je do 20. 04. i ko dotle ne prijavi seminarski smatraće se da je odustao.

Za sve potencijalne nejasnoće, javite se mejlom!

Ispitna pitanja za teorijski deo ispita

Spisak ispitnih pitanja možete naći ovde.

Studenti koji su zainteresovani za dodatnih 5 poena (za ukupan zbir 105) mogu da usmeno odgovaraju još jedno pitanje sa suženog spiska ispitnih pitanja za usmeni deo (u dodatnom terminu po dogovoru, nakon što završe sve druge ispitne obaveze).

Materijali

Virtuelna mašina

1. tročas - Upotreba QtCreator-ovog debagera

2. tročas - Unit testiranje i pokrivenost koda

3. tročas - Unit testiranje - nastavak

4. tročas - Profajliranje. Valgrind (Memcheck, Massif)

5. tročas - Profajliranje. Valgrind (Cachegrind, KCachegrind, Callgrind)

6. tročas - Profajliranje. Valgrind (Helgrind, DRD)

7. tročas - Klee

8. tročas - Klee - nastavak

9. tročas - CBMC

10. tročas - CBMC - nastavak

11. tročas - Clang static analyzer

12. tročas - priprema za ispit

Literatura za predavanja

  • Materijali koji se mogu naći u okviru kartice za predavanja (slajdovi i tekstovi sa predavanja i razni dodatni materijali)
  • J. Laski, W. Stanley: Software Verification and Analysis. Springer - Verlag, London, 2009.
  • J. B. Almeida, M. J. Frade, J. S. Pinto, S. M. de Sousa: Rigorous Software Development (An introduction to Program Verification). Springer - Verlag, London 2011.
  • Izabrani naučni radovi, seminarski radovi, master radovi
  • Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y. Bounded model checking. Advances in computers. 2003 Dec;58(11):117-48.
  • Cristian Cadar, Daniel Dunbar, Dawson Engler. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs, In OSDI, 2008.

Literatura za vežbe

Ispit - Januar 2

Prijava za izlazak na praktični deo ispita 31.01.2019. u 9h vrši se preko forme (do 30.01.2019. u 9:00).

24. 01. 2019.

Januar 1 Rezultati praktičnog dela ispita

Tekući rezultati su vidljivi ovde. Uvid u rezultate je u četvrtak 24.01.2019 u 12:30 na Studentskom trgu.

22. 01. 2019.

Ispit - Januar 1

Prijava za izlazak na praktični deo ispita 17.01.2019. u 9h vrši se preko forme (do 16.01.2019. u 13:00).

12. 01. 2019.

*** Dragi studenti, želimo vam srećne novogodišnje i božićne praznike i puno uspeha u 2019. godini! ***

30.12.2018.

Odbrane praktičnih projekata

Informacije o terminima odbrane praktičnih projekata dat je u okviru kartice "Obaveze studenata". Možete izaći na ispit i pre nego što odbranite praktični projekat.

31. 12. 2018.

Rezultati samostalnog seminarskog rada

Svim studentima koji su predali samostalni seminarski rad upisani su tekući rezultati ovde.
Objašnjenja vezana broj poena za sam rad data su u nastavku vrste za svaki rad pojedinačno. Ukoliko je nešto nejasno, javite se mejlom radi dobijanja preciznijeg objašnjenja.

30. 12. 2018.

Termin vežbi

Čas vežbi predviđen da se održi 09.01.2019. održaće se u petak 21.12.2018 u 14h u učionici JAG2.

08. 12. 2018.

Rezultati

Ovde možete pratiti tekuće rezultate.

3. 12. 2018.

Teorijski test

Teorijski test biće održan u terminu predavanja 3. decembra 2018. Spisak ispitnih pitanja možete naći ovde. Test nije obavezan ali Vas oslobađa tog dela gradiva na završnom ispitu.

06. 11. 2018.

Grupni seminarski rad

Prijavite grupe za izradu grupnog seminarskog rada do 20. 11. 2018. godine. Forma za prijavu se može naći ovde.

06. 11. 2018.

Samostalni teorijski seminarski rad

Link na formu za predavanje samostalnog seminarskog možete naći ovde.

Predlog tema se može pronaći ovde. Pre početka izrade rada, ukoliko bilo šta nije jasno, najbolje je konsultovati se i najpre razrešiti sve nedoumice (mejlom ili u pauzi između predavanja). Krajnji rok za obradu tema je do 11. decembra. Šablon i obim seminarskog rada možete naći ovde.

Teme sa spiska obuhvataju teme koje se obrađuju na predavanjima ali koje je potrebno dodatno istražiti i produbiti. Za neke teme su navedene smernice u vidu linkova i literature od kojih je potrebno krenuti, a za neke nisu. Za neke teme neophodno je da student pročita jedan ili par naučnih radova kako bi mogao da ih obradi. Odgovarajući naučni radovi mogu se naći kao reference u osnovnom tekstu dokumenta koji je dat kao polazna literatura. Za neke teme potrebno je samostalno naći odgovarajuće stručne ili naučne radove.

Ukoliko se pored teme nalazi i ime studenta, znači da je tema već rezervisana. Spisak tema sa rezervacijama biće ažuriran jednom dnevno. Potrebno je da se javite mejlom i da prijavite za koju ste temu zainteresovani. Najbolje je da prijavite odmah prvu i drugu želju, za slučaj da je prva želja već izabrana a spisak nije u međuvremenu ažuriran.

Ukoliko neko želi neku drugu temu koja se uklapa u sadržaj kursa, može to da predloži mejlom. Ukoliko je u pitanju predlog nekog naučnog rada, predlog konferencija (tj konferencija sa kojih je izabrani rad najverovatnije prihvatljiv) uključuje:
  1. VSTTE - Verified Software: Theories, Tools, Experiments
  2. CAV - Computer Aided Verification
  3. POPL - Principles of Programming Languages
  4. PLDI - Programming Language Design and Implementation
  5. FMCAD - Formal Methods in Computer-Aided Design
Izabrani rad ne bi trebalo da bude objavljen pre više od 12 godina (osim u nekim specijalnim situacijama). Rad takođe može da bude i sa neke druge konferencije ili iz časopisa. Dobro je da izaberete rad koji je citiran veći broj puta (jer to pokazuje njegovu važnost).

30. 10. 2018.

Promena učionice za vežbe

Počev od 24.10.2018 vežbe će se održavati u istom terminu, sredom od 9h, u učionici JAG2.

22. 10. 2018.

Teorijski seminarski rad

Studenti zainteresovani za izradu teorijskog seminarskog rada potrebno je da se do 25. oktobra prijave preko ove forme. U okviru teorijskog seminarskog rada biće potrebno detaljno obraditi neku temu sa predavanja ili neki naučni rad (u dogovoru sa nastavnikom).

16. 10. 2018.

Početak kursa

Nastava na master studijama počinje od 08. 10. 2018.

30. 09. 2018.

Matematički fakultet, Univerzitet u Beogradu
školska 2017/18. godina