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:

• prof. dr Milena Vujošević Janičić

Asistent:

• Ivan Ristović

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.

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

• Uvod: o kursu i obavezama na kursu. Slajdovi
• Kratak pregled kursa. Briga o kvalitetu softvera. Slajdovi. Tekst.
  Primer - standardi u automobilskoj industriji: AutoSar
  Video: Extending Clang for checking compliance with automotive coding standards
• Dinamička verifikacija softvera. Tehnike testiranja. Slajdovi. Tekst.
  
• Dinamička verifikacija softvera. Debagovanje. Profajliranje. Analiza binarnog koda.
  Slajdovi. Tekst.
  
• Statička analiza softvera. Pregledi koda. Slajdovi. Tekst.
  
• Simboličko izvršavanje. Slajdovi. Tekst.
  
  • A Survey of Symbolic Execution Techniques ACM Computing Surveys (CSUR), Volume 51 Issue 3, July 2018
    Besplatno dostupna verzija rada
    
  • A Systematic Review of Search Strategies in Dynamic Symbolic Execution, Arash Sabbaghi, Mohammad Reza Keyvanpour. Computer Standards & Interfaces. 2020 Oct 1;72:103444.
• Semantika programskih jezika. Slajdovi. Tekst.
  
• Proveravanje modela. Slajdovi. Tekst.
  
• Apstraktna interpretacija. Slajdovi. Tekst.
  

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

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

Dodatni materijali za predavanja

• Dinamička verifikacija softvera. Tehnike testiranja.
  • Seminarski rad, Jelena Mitrović: Uloga QA testera u razvoju softvera: tehnologije, alati i izazovi
    
  • Seminarski rad, Rastko Đorđević: Metamorfno testiranje.
    
  • Seminarski rad, Lazar Vasović: Metamorfno testiranje: primena kod kompajlera.
    
  • Seminarski rad, Lazar Mrkela, Ivan Milić: Pregled osnovnih tehnika testiranja
    
  • Master rad, Ana Đorđević: Automatsko generisanje test primera uz pomoć statičke analize i rešavača Z3
    
  • Master rad, Ana Mitrović: Primena jezila Scala u paralelizaciji rasplinutog testiranja
    
  • Seminarski rad, Petar Mićić: Automatsko generisanje test primera korišćenjem genetskog algoritma
    
  • Seminarski rad, Lazar Mladenović: JUnit
    
  • Seminarski rad, Dalma Beara: Selenium – alat za testiranje veb aplikacija
    
  • Seminarski rad, Stefan Pantić: CppUnit - Biblioteka za testiranje C++ koda
    
  • Seminarski rad, David Gavrilović: Komponentno i integraciono testiranje u programskom jeziku C++
    
  • Seminarski rad, Dijana Zulfikarić: Biblioteka PyTest
    
  • Seminarski rad, Nikola Dimić: WebdriverIO - savremen alat za testiranje
    
  • Seminarski rad, Luka Milošević: Fuzz testiranje
    
  • Seminarski rad, Filip Jovašević: Testiranje metodama klase ekvivalencije i graničnih vrednosti
    
  • Seminarski rad, Stefan Stanišić: Razvojni okvir Jasmine
    
  • Seminarski rad, Nikola Kovačević: Jedinično testiranje pomoću xUnit alata (u C#.NET aplikacijama)
    
• Dinamička verifikacija softvera. Debagovanje. Profajliranje. Analiza binarnog koda.
  
  • Master rad, Đorđe Todorović: Podrška za naprednu analizu promenljivih lokalnih za niti pomoću alata Gnu Gdb
    
  • Master rad, Nikola Prica: Podrška za profajliranje softvera uređaja sa ugrađenim računarom
    
  • Master rad, Aleksandra Karadžić: Alat Valgrind - implementacija konvencije FPXX za arhitekturu MIPS
    
  • Seminarski rad, Nevena Nikolić: Profajleri - Knutov algoritam
    
  • Seminarski rad, Luka Kalinić: Kako rade debageri?
    
  • Seminarski rad, Nikola Dimitrijević: Sistemski poziv ptrace
    
  • Seminarski rad, Srdan Lazarević: Alat komandne linije strace
    
  • Seminarski rad, Vladimir Bošković: Profajleri - Uzimanje uzoraka
    
  • Seminarski rad, Nikola Nestorović: Sanitajzeri
    
  • Seminarski rad, Vladimir Batoćanin, Stefan Stefanović, Jovan Ležaja, Đorđe Jovanović: Debagovanje Haskela - GHCi i alternative
    
  • Seminarski rad, Dimitrije Sekulić, Sandra Radojević, Maja Gavrilović, Matija Pejić: Načini debagovanja u programskom jeziku Python
    
  • Seminarski rad, Ivan Vranković, Andela Karakaš, Ivan Mihajlović, Kristina Petrović: Debagovanje Java Programa
    
  • Seminarski rad, Kristina Pantelić, Ivana Cvetkoski, Bojana Ristanović, Nikola Stamenić: Tačka prekida: GNU debager
    
  • Seminarski rad, Momir Adžemović, Miloš Miković, Marko Spasić, Mladen Dobrašinović: Debagovanje sa LLDB-om
    
  • Seminarski rad, Jovana Bošković, Ana Jakovljević, Nikola Perić, Mateja Trtica: Profajliranje Haskell programa
    
  • Seminarski rad, Andelka Milovanović, David Popov, Jelisaveta Smiljanić, Petar Zečević: Profajleri i njihova vizualizacija za jezik Python
    
  • Seminarski rad, Jelena Živović, Tomislav Janković, Jelena Jeremić, Milica Marić: Profajleri za programe napisane u programskom jeziku Java
    
  • Seminarski rad, Marko Spasić: Debagovanje i profajliranje GLSL šejder programa
    
• Statička analiza softvera. Pregledi koda.
  • Seminarski rad, Nikola Janković, Andela Milićević, Katarina Savičić, Dunja Spasić: Metode za pregled kôda i njihov značaj
  • Seminarski rad, Jovana Pejkić: ESLint - alat za statičku analizu koda u JavaScript-u
• Simboličko izvršavanje.
  • A Survey of Symbolic Execution Techniques ACM Computing Surveys (CSUR), Volume 51 Issue 3, July 2018
    Besplatno dostupna verzija rada
    
  • A Systematic Review of Search Strategies in Dynamic Symbolic Execution, Arash Sabbaghi, Mohammad Reza Keyvanpour. Computer Standards & Interfaces. 2020 Oct 1;72:103444.
  • Seminarski rad, Aleksandar Anžel: Simboličko izvršavanje - Konkoličko izvršavanje.
    
  • Seminarski rad, Nikola Stojević: Simboličko izvršavanje - Modelovanje okoline.
    
  • Seminarski rad, Filip Lazić: Simboličko izvršavanje - Eksplozija putanja i regulisanje broja putanja (1).
    
  • Seminarski rad, Saša Cvetković: Simboličko izvršavanje - Eksplozija putanja i regulisanje broja putanja (2).
    
  • Seminarski rad, Lazar Ranković: Simboličko izvršavanje - Rešavanje uslova (1).
    
  • Seminarski rad, Vido Mladenović: Simboličko izvršavanje - Rešavanje uslova (2).
    
  • Seminarski rad, Nemanja Mićović: Simboličko izvršavanje - Strategije obilaska puteva.
    
  • Seminarski rad, Irena Blagojević, Gorana Vučić: Simboličko izvršavanje - Selektivno simboličko izvršavanje.
    
  • Simboličko izvršavanje - sve prethodne teme.
  • Seminarski rad, Tatjana Radovanović: EXE: Pronalaženje test primera koji dovode do pada sistema.
    
  • Seminarski rad, Ognjen Plavišić: Kako vršiti statičku analizu u okviru LLVM projekta.
    
• Semantika programskih jezika.
  • Seminarski rad, Uroš Ševkušič: Denotaciona semantika - primeri .
  • Seminarski rad, Aleksandra Kovačević: Prirodna semantika.
  • Seminarski rad, Jana Milutinović: Strukturna semantika.
    
  • Seminarski rad, Kristina Stanojević: Denotaciona semantika.
    
  • Seminarski rad, Nikola Katić: Aksiomatska semantika.
    
  • Seminarski rad, Mirko Brkušanin: Primena semantike programskih jezika (VELLVM).
    
  • Seminarski rad, Jovan Dmitrović: Pojam invarijante.
• Proveravanje modela.
  • Seminarski rad, Uroš Ševkušič: Proveravanje modela kvantnih programa korišćenjem kvantnih Markovljevih lanaca.
  • Seminarski rad, Nikola Grulović: CTL i primeri svojstava koji se mogu izraziti u CTL-u
    
  • Seminarski rad, Tomislav Milovanović: Verifikacija hardvera. Primeri. Jezici Verilog i VHDL.
    
  • Seminarski rad, Tatjana Damnjanović: Modelovanje sistema sa Kripke strukturama
    
  • Seminarski rad, Nadežda Bogdanović: Apstrakcija predikata
    
  • Seminarski rad, Ivona Jurošević: LTL i primeri svojstava koji se mogu izraziti u LTL-u
    
  • Proveravanje modela - razne teme.
    
• Apstraktna interpretacija.
  • Seminarski rad, Milan Čugurović: Intuicija - preciznije.
    
  • Seminarski rad, Dimitrije Špadijer: Teorija - preciznije.
• Primene tehnika verifikacije softvera u biologiji i u sintezi koda.
• Dodatni materijali za učenje (deo 1), (deo 2), (deo 3).

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