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 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).

Materijali

Teorijski deo ispita

Teorijski deo ispita sastoji se od 5 pitanja. Svako pitanje vredi 5 poena. Prva četiri pitanja su iz oblasti koje su pokrivane predavanjima, a poslednje pitanje je sa spiska dodatnih pitanja. Iz skupa dodatnih pitanja dobijate tri pitanja (od kojih birate da odgovarate na jedno, pri čemu to jedno ne može biti vezano za temu koju ste Vi obrađivali za samostalni seminarski rad).

Odgovore na većinu dodatnih pitanja možete naći u okviru samostalnih seminarskih radova. Neke odgovore smo diskutovali na časovima prilikom prezentacija (i nisu direktno uključena u materijale). Neki odgovori se prostiru kroz više samostalnih seminarskih radova. Neke odgovore treba samostalno da istražite. Svi dodatni materijali su dostupni ovde.

Samostalni seminarski rad

Samostalni seminarski rad sastoji se od obrade i odbrane izabranog naučnog rada iz oblasti kursa.

Obrada rada obuhvata razumevanje osnovnih ideja predstavljenih u radu i sažimanje tih ideja u tekst dužine od oko četiri strane (a najviše 5 strana) u latex formatu (šablon za format možete skinuti ovde, razlike u odnosu na taj šablon su što tekst ne mora da sadrži slike i tabele, kao i što nije potrebno da se uključuje sadržaj na prvu stranu).

Link na formu za predavanje samostalnog seminarskog možete naći ovde. Bodovanje: 10 poena tekst i 5 pena odbrana.

Odbrana rada obuhvata prezentaciju rada na času predavnja u trajanju od 4 do 5 minuta.

Svi seminarski radovi moraju da budu odbranjeni do kraja semestra.

Potrebno je da samostalno izaberete i predložite rad. Kada izaberete rad, potrebno je da se javite mejlom radi potvrde da je izabrani rad prihvatljiv (po oblasti i temi, kao i da ga niko drugi nije prijavio). Poslednji rok za prijavu teme je 15. april 2018.

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. Neki predlozi radova se mogu naći ovde. Takođe, može se izabrati i neki rad koji je citiran u okviru pregleda simboličkog izvršavanja ovde. Rad može da bude i iz oblasti dinamičke verifikacije softvera. Ukoliko niste sigurni kako da izaberete rad, možemo se konsultovati na tu temu u pauzi između predavanja. Dobro je da izaberete rad koji je citiran veći broj puta (jer to pokazuje njegovu važnost).

VerifikacijaSoftvera_v1.0.3

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, Callgrind, KCachegrind)

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

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 i slajdovi sa 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.
  • 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

Rezultati i upis ocena

Finalni rezultati. Ocene su unete u Hipatiju, proverite! Upis ocena u indeks: petak 28. 09. u 9:15h.

26. 09. 2018.

Rezultati pismenog dela u Septembar 2

Rezultati sa pismenog dela ispita u Septembru 2.

23. 09. 2018.

Odbrane seminarskih radova

Prvi termin odbrane seminarskog rada je ponedeljak 17.09. u jutarnjim časovima (dogovor mejlom). Naredni termin za odbranu je 28. septembar. Tacno vreme bice objavljeno naknadno.
Nakon predavanja seminarskog rada obavezno prijavite (mejlom na milena@...) koji termin Vam više odgovara. Odbrana seminarskog zahteva da svi članovi grupe budu prisutni i obuhvata prikaz rada seminarskog i objašnjenja o odlukama i strukturi implementacije.
U periodu između predavanja seminarskog rada i dobrane, dozvoljene su sitnije izmene i poboljšanja rada, ali ne i drastične izmene.

14. 09. 2018.

Ispit - Septembar 2

Prijava za izlazak na praktični deo ispita 14.09.2018. u 9h se vrši preko forme (do 13.09.2018. u 16:59).

11. 09. 2018.

Rezultati pismenog dela u Septembar 2

Ovde možete pratiti tekuće rezultate.

10. 09. 2018.

Ispit - Septembar 1

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

26. 08. 2018.

Rezultati pismenog dela u Junu 2

Ovde mozete pratiti tekuće rezultate.

10. 07. 2018.

Ispit - jun 2

Prijava za izlazak na praktični deo ispita 30.06.2018 u 9h se vrši preko forme (do 27. 06. u 23:59).

19. 06. 2018.

Rezultati pismenog dela u Junu 1

Ovde mozete pratiti tekuće rezultate.

18. 06. 2018.

Anketa o pomeranju termina ispita - jun 2

Molimo Vas da popunite anketu o pomeranju ispita iz Verifikacije softvera na 30.06. u 9h. Anketu je moguće popuniti do 17.06.2018.

14. 06. 2018.

Ispit - jun 1

Prijava za izlazak na praktični deo ispita 07.06.2018 u 9h se vrši preko forme (do srede 06. 06. u 17:00).
Prijava za polaganje teorije: poslati mejl do 06. 06. u 14h.

30. 05. 2018.

Teorijski deo ispita - predrok

Predrok za teorijski deo ispita biće održan u petak 1. juna u 10:30h. U okviru predroka polaže se deo teorijskog ispita: studenti koji su polagali teoriju na kolokvijumu, mogu da polažu drugi deo teorije. Studenti koji nisu izlazili na kolokvijum, mogu da polažu prvi deo teorije (granica je kod simboličkog izvršavanja, tj rad sa simboličkom memorijom).

28. 05. 2018.

Odbrane projekata

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 (tako da odgovara svima).

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

  • 28. 06., ukoliko je sve ok, imaće priliku da brane u nekom (dogovorenom) terminu između 1. i 10. 07.
  • 28. 08., ukoliko je sve ok, imaće priliku da brane u nekom (dogovorenom) terminu između 1. i 10. 09.
  • 10. 09., ukoliko je sve ok, imaće priliku da brane u nekom (dogovorenom) terminu između 15. i 25. 09.
  • 15. 09., ukoliko je sve ok, imaće priliku da brane u nekom (dogovorenom) terminu između 20. i 30. 09.
Kasnija odbrana je, po potrebi, moguća (npr prijava u avgustu, a odbrana sredinom septembra), ali najkasnija prijava je do 15. 09. i ko dotle ne prijavi seminarski smatraće se da je odustao.

Za sve potencijalne nejasnoće, javite se mejlom!

27. 05. 2018.

Najbolji master rad za 2017. godinu

Danas su u okviru galerije Srpske akademije nauka i umetnosti dodeljene nagrade za najbolje doktorske i master radove u oblastima matematike i računarstva. Objavu možete naći na strani Matematičkog instituta ovde.

U oblasti računarstva, Branislava Živković dobila je nagradu za svoj master rad pod imenom ,,Paralelizacija statičke verifikacije softvera''. Rad možete pogledati ovde. Rezultati rada prikazani su i na konferenciji: 23rd International Conference on Types for Proofs and Programs, (maj, 2017). Čestitamo!

23. 05. 2018.

Informacije o ispitu

Ispit možete polagati u redosledu koji Vam odgovara (posebno teoriju, posebno zadatke, istovremeno teorija i zadaci). Jedino je potrebno prijaviti ispit i nameru redoslda polaganja (preko forme za prijavljivanje koja će biti dostupna uskoro).

U okviru materijala sa predavanja okačeni su i do sada odbranjeni seminarski radovi.

22. 05. 2018.

Nadoknada vežbi

Nadoknada 10.časa vežbi će biti 15.05.2018 od 9h u Jag2.

13. 05. 2018.

Rezultati

Ovde mozete pratiti tekuće rezultate.

27. 04. 2018.

Odbrana samostalnih seminarskih radova

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

Bodovanje: 10 poena tekst i 5 pena odbrana.

Rok za predaju seminarskog rada je najkasnije u poslednji petak u podne pre termina odbrane. Redosled odbrane seminarskih radova može se videti ovde. Na odbrani možete i ne morate koristiti slajdove. Važno je da se držite vremenskih ograničenja.

26. 04. 2018.

Vežbe

U četvrtak 26.04.2018 nećemo imati vežbe. Nadoknada će biti u nekom terminu posle praznika u dogovoru sa studentima.

26. 04. 2018.

Grupni seminarski rad

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

08. 04. 2018.

Test

Prijavite se ukoliko želite da radite test! Forma za prijavljivanje. Raspored polaganja testa.

Teorijski test biće održan u ponedeljak 23. aprila 2018. godine u 16h (u terminu predavanja). Test nije obavezan. Studenti koji polože test su oslobođeni tog dela gradiva na završnom ispitu. Teme na testu: Briga o kvalitetu softvera. Tehnike testiranja. Dinamička verifikacija softvera. Debagovanje. Profajliranje. Binarna analiza koda. Pregledi koda. Simboličko izvršavanje (uključujući simboličko modelovanje memorije).

Pitanja (dva ili tri) će biti u obliku naslova ili podnaslova odgovarajućih lekcija.

29. 03. 2018.

Samostalni seminarski rad

Rok za prijavu izrade samostalnog seminarskog rada je 15. 04. 2018. godine. Detaljnije informacije se mogu naći ovde.

25. 03. 2018.

Agilan pristup studentskim projektima

У термину одржавања предавања на курсу Методологија стручног и научног рада, 26. марта у 14h биће одржано гостујуће предавање (у трајању од око 45 минута) у сарадњи са фирмом PuzzleSoftware.
Позивамо све заинтересоване студенте да присуствују овом предавању. Тема предавања: Agilan pristup studentskim projektima
  • Kako da formirate tim kolega za zajednički projekat?
  • Kako da radite planiranje, organizovanje procesa i tima, i implementaciju?

Na početku svakog projekta postavlja se jedno važno pitanje – koji sastav tima bi bio idealan za realizaciju projekta? Ko učestvuje na projektu – jedna je od najvažnijih odluka. Od ljudi koje izaberete često može da zavisi i sudbina projekta. Da li želite ljude koji su inovativni, energični? Da li ćete raditi odvojeno sa jasnim smernicama za integracijuna kraju, ili ćete imati redovne sastanke i sinhronizaciju? Odabir ljudi za tim zavisi od pojedinačnog slučaja.

Na fakultetu se obično bavimo onim što nazivamo domenskim zanjem - učimo o oblasti u kojoj ćemo raditi, kao i tehnike za razvoj konkretnog projekta iz konkretne oblasti. U poslednje vreme, studenti takođe uče i o takozvanim “soft” tehnikama i o nekim metodologijama rada.

Tokom ove radionice, bavićemo se planiranjem jednog studentskog projekta. To može biti ispit, praktičan zadatak ili realizacija sjajne ideje pojedinca ili grupe (tima). Razgraničićemo šta je to: Tradicionalan “waterfall” način razvoja, tj. rada na projektu, Iterativni, agilni pristup projektu

Zatim, objasnićemo i kako je moguće podeliti ispit po fazama učenja; kako meriti napredak; šta je to “Design Thinking” i zašto je pogodan za projekte gde eksperimentišemo, gde nam unapred nije poznato rešenje.

Predavač: Đorđe Babić. Đorđe Babić se poslednjih pet godina bavi Project Management-om i izgradnjom timova. Ima veliko iskustvo u software development-u i trenutno radi kao Senior Scrum Master za Innovative Gaming Software (IGSoft) u beogradskom studiju za razvoj betting & social igrica, sa akcentom na mobile. Đorđe je sertifikovani Scrum Master, od strane Scrum Alliance (krovne organizacije za Scrum u svetu). Neke od kompanija u kojima je radio su PSTech, Endava, Cisco, Humanity, Puzzle Software, Telenor i Red Lark.

Inspriše ga formiranje timova, pomaganje ljudi koji imaju tehničko znanje da se prilagode na radnu saradnju i rad u dinamičkom okruženju. Takođe, voli da radi na sinhornizaciji između timova u skaliranim sredinama. U slobodno vreme pomaže ljudima koji su na početku karijere u planiranju profesionalnog razvoja.

15.03.2017.

Učionica za vežbe

Vežbe će od sada biti u BIM, umesto u DLAB-u.

23. 02. 2018.

Komunikacija u okviru kursa

Ostavite svoje podatke preko ove forme ukoliko želite da dobijate informacije vezane za kurs.

15. 02. 2018.

Prva nastavna nedelja

Prve nastavne nedelje letenjeg semestra biće održani samo časovi predavanja u terminu predviđenim rasporedom (vežbe neće biti držane).

15. 02. 2018.

Početak semestra

Svim studentima želimo uspešan početak letnjeg semestra školske 2017/18. godine!

15. 02. 2018.

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