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:
Obaveze studenata uključuju predispitne obaveze i 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 obaveze se sastoje od obaveznog praktičnog seminarskog rada (samostalnog ili grupnog). Praktični seminarski rad je neophodno prijaviti do 1. decembra tekuće godine. 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:
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.
Ciljevi i uslovi izrade praktičnog seminarskog rada:
U okviru repozitorijuma za izradu seminarskog rada, potrebno je da bude napisan README fajl koji sadrži:
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:
.
├── .github // CI konfiguracija:
│ └── workflows // preuzeti sa: {{site.projects-ci}}
│ ├── gate.yml
│ └── tickets.yml
├── git-submodul-of-project-to-analyze @ commit-hash
├── custom.patch // changes to the original project
├── unit_tests
│ ├── run_tests.py
│ ├── RunningTests.md
│ ├── RunningTests.pdf
│ └── tests
│ ├── MyUnitTests1.cpp
│ └── MyUnitTests2.cpp
├── klee
│ ├── run_klee.sh
│ ├── failed-tests
│ │ ├── test00001.ktest
│ │ └── ...
| └── klee-test-corpus.zip
├── cbmc
│ ├── run_cbmc.sh
│ ├── cbmc-outputs
│ │ ├── run1.stdout
│ │ ├── run2.stdout
│ │ ├── run3.stdout
│ │ ├── run3.stderr
│ │ └── ...
│ └── counterexamples
│ ├── counterexample1
│ ├── counterexample2
│ ├── counterexample3
│ └── ...
├── valgrind
│ ├── callgrind
│ │ ├── callgrind.out.12312
│ │ ├── callgrind.out.12313
│ │ ├── callgrind.out.12314
│ │ ├── callgrind.out.12315
│ │ ├── kcachegrind_12315_1.png
│ │ ├── kcachegrind_12315_2.png
│ │ ├── kcachegrind_12315_3.png
│ │ ├── kcachegrind_12315_4.png
│ │ └── run_callgrind.sh
│ └── massif
│ ├── massif.out.12312
│ ├── massif.out.12313
│ ├── massif.out.12314
│ ├── massif.out.12315
│ └── run_massif.sh
├── .gitignore
├── .gitmodules
├── README
├── ProjectAnalysisReport.md
└── ProjectAnalysisReport.pdf
Napomena: Repozitorijumi koji ne prate strukturu prikazanu iznad 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
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:
Pored README fajla, potrebno je da postoji i fajl SystemDescription (PDF ili markdown fajl) koji sadrži:
Forma za prijavu samostalnih seminarskih radova se može naći na sledećem linku (ignorisati pitanja vezana za samostalne seminarske radove).
Polaže se pismeno, izvlači se pet ispitnih pitanja sa spiska ispitnih pitanja.
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 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!
Spisak ispitnih pitanja je redukovan u delu za koji nije držana nastava. Pokrivene su sve oblasti, ali se očekuje manji nivo detaljnosti u odgovorima za poslednjih 7 pitanja.
Novi spisak ispitnih pitanja možete da nađete ovde. Umesto odgovaranja na 5 ispitnih pitanja po 10 poena, odgovaraćete na 4 ispitna pitanja po 12.5 poena. Studentima koji su radili testove poeni su skalirani u tabeli. Raspodela ispitnih pitanja:
Za praktični deo ispita, neophodni broj alata je smanjen sa 5 na 4, a broj poena za svaki alat je adekvatno skaliran.
Za sve nejasnoće, javite se mejlom.
02.02.2025.
U skladu sa tekućim dešavanjima, do daljnjeg nećemo imati nikakve aktivnosti, pa ni testove.
08.12.2024.
Molimo studente koji nisu prihvatili pozivnice na GitHub-u da to urade do subote, 7. decembra u 20h. Pozivnice se mogu prihvatiti tako što sa ulogovanim nalogom posetite glavnu stranicu GitHub organizacije za kurs. Alternativno, moguće je naći pozivnicu unutar "Your organizations" menija (uputstvo).
U subotu uveče će biti automatski kreirani timovi i repozitorijumi za izradu seminarskih radova, i dodaljene odgovarajuće permisije prijavljenim GitHub nalozima. GitHub nalozi koji nisu članovi organizaciju nemaju pristup repozitorijumima za izradu seminarskih radova. Uputstva za organizaciju i izradu seminarskih radova se mogu naći unutar kartice sa obavezama studenata.
05. 12. 2024.
U skladu sa tekućim dešavanjima i kako bismo izbegli potencijalne neprijatnosti, test koji je zakazan za četvrtak 5. decembar ćemo odložiti za četvrtak 12. decembar. Za sva obaveštenja, pratite stranu kursa.
04.12.2024.
Po zvaničnim informacijama, nastava se obustavlja do kraja ove nedelje. Zbog toga nećemo imati časove predavanja. Kako test nije nastava, smatram da test koji je zakazan za četvrtak 5. decembar treba da se održi. Time se ne remeti blokada nastave.
Dakle, u četvrtak 5. decembra ćemo imati treći test u učionici 718 u 10h. Ko želi, može da radi dva pitanja po izboru. Specijalno, pošto nemamo nastavu posle toga, možete da radite i sva tri pitanja. Test nije obavezan.
04.12.2024.
Svim studentima koji su prijavili projekat poslate su pozivnice za pristup organizaciji. Poziv je neophodno prihvatiti kako bi kasnije bili kreirani odgovarajući repozitorijumi.
Ukoliko ste prijavili projekat a niste dobili pozivnicu, javite se na mejl predmetnom asistentu.
01. 12. 2024.
Vežbe će se održavati u jednom terminu i to:
18. 11. 2024.
U četvrtak 21. novembra ćemo imati drugi test u učionici 718 u 10h. Ko želi, može da radi i samo prvo ispitno pitanje, prvo i drugo ispitno pitanje, ili samo drugo ispitno pitanje. Test nije obavezan.
18. 11. 2024.
Vežbe za grupu 5IB će se održavati po rasporedu časova u učionici N252 umesto u učionici JAG1.
05. 11. 2024.
Anketa za prijavu praktičnog seminarskog rada se nalazi na linku. Anketa važi i za grupne i za samostalne radove.
Praktični radovi iz prethodnih školskih godina se mogu naći ovde.
Rok za prijavu teme je 1. decembar.
05. 11. 2024.
U četvrtak 7. novembra ćemo imati četiri časa predavanja na kursu Verifikacija softvera (od 9h do 13h), pošto časovi kursa Konstrukcija i analiza algoritama 2 neće biti držani. Neke naredne nedelje imaćete Konstrukciju i analizu algoritama 2 umesto Verifikacije softvera (bićete na tu temu blagovremeno obavešteni). Prva dva časa biće održana u 718, a druga dva u 704.
Imaćemo najpre jedan čas predavanja, završićemo temu testiranja softvera i onda ćemo imati test u 718, sa poćetkom u 10h. I naredne testove verovatno ćemo organizovati u 718. u 10h (o čemu ćete biti svaki put obavešteni na vreme). Nakon testa, nastavićemo dalje sa gradivom. Moguće je da će biti potrebno i da vas podelim u dve grupe za test, ali to ćemo odlučiti na licu mesta (kako trenutno stoje stvari po broju prijavljenih, na granici smo za dve grupe).
05. 11. 2024.
Studenti su podeljeni na dve grupe za vežbe. Obratite pažnju na izmene u rasporedu časova i proverite u Hipatiji u kojoj ste grupi.
29. 10. 2024.
Studenti zainteresovani da deo teorije polože u terminima predavanja u toku semestra mogu da rade ispitna pitanja okvirno u narednim terminima (proveravajte termine u toku godine):
Možete izaći na jedno ili više ispitnih pitanja, nezavisno. U jednom terminu možete polagati i više ispitnih pitanja (npr nadoknaditi ako niste polagali neko prethodno pitanje). U slučaju polaganja više ispitnih pitanja, nije zagarantovana tišina (predavanje može da bude u toku).
Ako izađete, poeni su konačni i ne možete ponovo da polažete to ispitno pitanje na ispitu. Ako ne izađete, onda ćete to polagati u regularnom terminu ispita. Za sve nejasnoće, javite se mejlom. Ako izvučete ispitno pitanje koje niste spremili, možete da izvučete drugo ispitno pitanje, ali onda je maksimalni broj poena 6.
25. 10. 2024.
U prvoj nedelji neće biti održane vežbe (sreda 09.10.2024).
Predavanja će se održati po rasporedu časova, u četvrtak od 11h.
Zbog upisa studenata na master studije koji se poklapa sa terminom predavanja, ni predavanja u prvoj nedelji neće biti održana.
08. 10. 2024.
27. 09. 2024.