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:

U toku godine, sve rezultate možete da pratite preko naredne tabele.

Izborni predmet

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

Obaveze studenata uključuju predispitne (praktične) obaveze i završni (teorijski) ispit. Predispitne obaveze se mogu ispuniti u formi praktičnog seminarskog rada. Praktični seminarski rad može, po izboru, biti samostalni ili grupni. Da bi se uspesno položio ispit, neophodno je ispuniti prag na predispitnim obavezama i ispitu. Više detalja u nastavku.

Predispitne (praktične) obaveze (od 50 do 55 poena):

Predispitne obaveze se sastoje od obaveznog praktičnog seminarskog rada (samostalnog ili grupnog). Praktični seminarski rad je neophodno prijaviti u toku semestra. Pratiti obaveštenja radi blagovremenog izbora teme. Da bi se položio ispit minimalni broj poena na predispitnim obavezama je 20.

Praktični seminarski radovi se brane uz prisustvo nastavnika u terminu ispita sa prethodnom prijavom koja se obično objavljuje nedelju dana pred ispit. Očekuje se da student dođe pripremljen za prezentovanje seminarskog rada u svom okruženju (npr. tako što će doneti laptop), predstaviti projekat i odgovoriti na pitanja. Pitanja mogu uključiti i pokretanje alata korišćenih za izradu seminarskog rada ili korišćenih na vežbama, kao i pisanje dodatnih testova tokom odbrane ukoliko su testovi deo seminarskog rada. Praktični seminarski radovi se moraju raditi u repozitorijumima u okviru GitHub organizacije za kurs.

Praktični seminarski rad može biti:

  • Analiza projekta otvorenog koda (samostalni rad) (50 poena)
  • Istraživački projekat (preporuka 2+ člana) (55 poena)

Analiza projekta otvorenog koda (50 poena)

Izrada podrazumeva pokretanje alata za verifikaciju softvera ili pisanje testova nad jednim projektom otvorenog koda. Prilikom odabira projekta, uveriti se da je projekat u dobrom stanju za analizu (prevodi se, kod je citljiv i modularan itd.). Konsultovati FAQ repozitorijum prilikom odabira projekta, kao i za upoznavanje sa čestim problemima tokom analize. Nakon isteka roka za odabir projekta, biće kreirani repozitorijumi za izradu seminarskih radova.

Odbrana je praktična, uz reprodukciju delova seminarskog rada. Neophodno je da sve što se nalazi u repozitorijumu student ume da objasni i reprodukuje na odbrani. Upotreba AI alata je dozvoljena, ali ukoliko student ne ume da objasni bilo koji deo skripti, izveštaja, i drugih artifakata unutar repozitorijuma, mora iznova da radi analizu nad drugim projektom, pri čemu je onda maksimalni broj osvojivih poena umanjen za 10 poena. Zbog toga, vodite računa da unutar repozitorijuma ne ubacite bilo šta što niste dobro proučili i razumeli.

Ciljevi i uslovi izrade praktičnog seminarskog rada:

  • Projekat koji se analizira mora biti otvorenog koda. Popularni kandidati su studentski projekti, u kom slučaju oni moraju biti projekti ranijih generacija (dakle, nije moguće odabrati svoj projekat) koji nisu već bili tema seminarskog rada iz ovog kursa. Spisak analiziranih projekata je dostupan ovde. Preporučuje se odabir nestudentskih projekata.
  • Cilj projekta je pronalazak bagova ili uskih grla programa. Nije neophodno da se zapravo pronađu bagovi kako bi seminarski rad bio uspešan - analiza i izveštaji čine seminarski rad.
  • Neophodno je iskoristiti barem 6 alata/tehnika u okviru seminarskog rada. Pritom:
    • Testovi se zajedno broje kao jedna stavka, i mogu se pisati u bilo kom radnom okviru. Kategorije testova (jedinični, integracioni, i sl.) se računaju kao zasebni alati. Uz testove je neophodno pratiti pokrivenost koda proizvoljnim alatom, pri čemu je alat za pokrivenost deo podrške za testiranje i ne broji se kao zasebni alat. Praćenje pokrivenosti koda bez testova nema smisla i nije validna metrika.
    • Dozvoljeno je koristiti maksimalno 1 Valgrind alat.
    • Maksimalno jedan od alata mora biti alat za formatiranje izvornog koda i stilske provere (npr. clang-format ili clang-tidy).
    • Dva alata moraju biti alati koji nisu rađeni na vežbama.
  • Za svaki korišćeni alat treba da budu dodate i skripte koje reprodukuju dobijene rezultate.

U okviru repozitorijuma za izradu seminarskog rada, potrebno je da bude napisan README fajl koji sadrži:

  • Informacije o autoru seminarskog rada.
  • Opis projekta koji je analiziran i odgovarajući linkovi do izvornog koda projekta - grana koja je analizirana i heš kod commit-a.
  • Spisak alata koji su korišćeni za analizu i uputstva za reprodukciju rezultata.
  • Spisak zaključaka.

Pored README fajla, potrebno je da postoji i (markdown ili PDF) fajl ProjectAnalysisReport koji sadrži detaljan opis analize projekta i zaključcima koji su napravljeni. Referencu na projekat koji se analizira dodati kao git submodul. Svaki alat koji je korišćen treba da ima poseban direktorijum u kome se nalaze rezultati rada alata kao i opcione skripte za pokretanje.

Primer korektne organizacije repozitorijuma se može naći u okviru FAQ repozitorijuma. epozitorijumi koji ne prate navedeni šablon ili nemaju tražene informacije u README fajlu neće biti prihvaćeni! Svi repozitorijumi moraju imati instaliranu CI konfiguraciju.

Forma za prijavu samostalnih seminarskih radova se može naći na sledećem linku (odabrati opciju samostalni seminarski rad). Repozitorijumi koji su već bili tema za samostalni seminarski rad iz ovog kursa se mogu naći na sledećem linku (spisak se automatski ažurira i uključuje real-time izmene u formi za prijavu).

Istraživački projekat (55 poena)

Napomena: Iako zamišljen da se radi timski, moguće je ovaj tip seminarskog rada raditi samostalno ali pritom se obim projekta ne smanjuje.

Većeg obima, istraživačkog tipa. Teme za projekat su dostupne unapred. Izuzetno, ukoliko imate neku ideju možete da je predložite. Izrada podrazumeva kreiranje novih ili nadograđivanje postojećih alata za verifikaciju softvera, kao i njihovu verifikaciju koristeći barem alate pomenute na vežbama. Nakon odabira projekta, i odgovarajućeg odobrenja od strane nastavnika, biće kreirani repozitorijumi za izradu seminarskih radova. Odbrana je usmena, uz prikaz rada. Nakon odbrane istraživačkog seminarskog rada biće sa profesorkom dogovoren termin za prezentovanje rada.

Spisak predviđenih tema se može naći ovde.

U okviru repozitorijuma za izradu seminarskog rada, potrebno je da bude napisan detaljan README fajl koji sadrži:

  • Informacije o autorima
  • Na koji način se projekat može prevesti i pokrenuti (sve neophodne biblioteke, alati i zavisnosti)
  • Na koji način se izvršna verzija koristi (primeri upotrebe)
  • Koji ulazni primeri se mogu koristiti za upotrebu i testiranje programa.
  • Spisak alata koji su korišćeni za analizu.
  • Ukoliko su testovi deo projekta, testovi treba da bude unutar repozitorijuma zajedno sa opisom kako se pokreću. Uključiti potencijalne skripte za pokretanje testova ukoliko su korišćene.

Pored README fajla, potrebno je da postoji i fajl SystemDescription (PDF ili markdown fajl) koji sadrži:

  • imena autora
  • opis problema
  • opis arhitekture sistema (opis osnovnih modula implementacije),
  • opis rešenja problema (osnovne ideje, obrazloženja za ključne odluke, opis osnovnog algoritma)

Forma za prijavu samostalnih seminarskih radova se može naći na sledećem linku (ignorisati pitanja vezana za samostalne seminarske radove).

Završni ispit (50 poena)

Polaže se pismeno, izvlače se četiri ispitna pitanja sa spiska ispitnih pitanja (spisak za prva dva ispitna pitanja, ostatak će biti objavljen naknadno).

Da bi se položio ispit, neophodno je imati 51 poen, pri čemu je neophodno ostvariti bar 20 poena na teoriji na završnom ispitu i bar 20 poena na predispitnim (praktičnim) obavezama. Od poena na teoriji, neophodno je imati bar 3 poena po pitanju (tj. nije dozvoljeno preskakati oblasti).

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


Za sve potencijalne nejasnoće, javite se mejlom!

Ispitna pitanja za teorijski deo ispita

Spisak ispitnih pitanja možete naći ovde (spisak za prva dva ispitna pitanja, ostatak će biti objavljen naknadno).

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

Predavanja - video materijali
Predavanja - skripta (21.07.2025)
Dodatni materijali

Materijali sa predavanja

Materijali

[Beleške sa vežbi]
[GitHub organizacija sa materijalima i studentskim projektima]

Oblasti pokrivene vežbama

  • Dijagnoziranje problema
    • Alati za analizu performansi Linux sistema
    • Analiza ponašanja programa metodom crne kutije
  • Debagovanje koristeći alate za debagovanje i razvojna okruženja
  • Testiranje jedinica koda
  • Praćenje pokrivenosti koda testovima
  • Testiranje pomoću objekata imitatora
    • Ručno pisanje imitator klasa (C++)
    • Imitatori baza podataka (C#)
    • Biblioteke za testiranje koristeći objekte imitatore - Mockito (Java), Moq (C#)
  • Fuzz testiranje
  • Profajliranje
  • Statička analiza
  • Alati i jezici za formalnu verifikaciju softvera

Literatura za predavanja

Predavanja - video materijali
Predavanja - skripta (21.07.2025)

Navedeni matarijali su dosutupni besplatno na internetu (potražite):
  • Materijali koji se mogu naći u okviru kartice za predavanja (slajdovi i tekstovi sa predavanja i razni dodatni materijali)
  • Izabrani naučni radovi, seminarski radovi, master radovi (linkovi dostupni u okviru kartice za predavanja)
  • 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.
  • 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.
  • Christel Baier, Joost-Pieter Katoen. Principles of Model Checking.
  • Kolekcija naprednih materijala

Literatura za vežbe

Dodatni materijali za predavanja

Termin prvog testa

Prvi test biće održan u terminu predavanja 12. januara. Pratite obaveštenja na strani kursa, biće potrebno da se prijavite preko forme kako bi test bio organizovan u jednoj ili dve grupe, u zavisnosti od broja prijavljenih.
Na testu se polažu prva dva ispitna pitanja. Spisak ispitnih pitanja za prvi test je dostupan ovde. Pročitajte pažljivo uputstva koja su data uz ispitna pitanja.

6. 12. 2025.

Praktični seminarski radovi

Anketa za prijavu praktičnih seminarskih radova se nalazi ovde. Anketa važi i za samostalne i istraživačke radove. Za sve detalje o seminarskim radovima, pogledati odeljak o obavezama.
Napomena: Obaveze su ažurirane u odnosu na prethodne godine.

Rok za prijavu je 25. decembar. Nakon isteka roka za prijavu, biće poslate pozivnice za pristup GitHub organizaciji i biće kreirani repozitorijumi za izradu radova.

Projekti otvorenog koda koji su već bili tema za samostalne seminarske radove prethodnih godina se mogu naći ovde. Smernice za odabir projekta za analizu se mogu naći ovde.

Spisak tema za istraživački tip seminarskog rada se može naći ovde.

25. 11. 2025.

Početak semestra

Svim studentima želimo uspešan početak godine!

12. 11. 2025.

Matematički fakultet, Univerzitet u Beogradu
školska 2025/26. godina