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 praktični deo ispit. Podrazumeva se da je pre uzimanja teme za praktični seminarski rad položena teorija (ili barem njen deo).

Odbrane praktičnih projekata

Odbrana praktičnog projekta može i ne mora da prethodi izlasku na praktični deo ispita. 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.
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). 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 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

Upis ocena

Mole se studneti koji su položili ispit u nekom od prethodnih rokova i žele da upišu ocenu u indeks da se prijave putem naredne ankete do ponedeljka 28. septembra u 12h, kako bi napravili odgovarajući plan upisa ocena (kako bi se izbegle gužve po hodnicima i čekanje).

Upis ocena biće organizovan u sredu, 30. septembra, a tačni termini biće objavljeni nakon isteka roka za popunjavanje ankete. Ako nekome 30. septembar ne odgovara, nije problem, biće i drugih termina za upis (javite se mejlom nakon 05. oktobra).

24.09.2020.

Rezultati

Ovde možete pratiti tekuće rezultate.

Svi rezultati su uneti u Hipatiju. Proverite i ukoliko uočite neku neregularnost, javite što pre. Spiskovi će biti zaključeni 30. septembra.

23. 08. 2020.

Prijava za ispit u Septembar 3

Molimo studente koji izlaze na ispit u ispitnom roku Septembar3 da popune sledeći upitnik.

13. 09. 2020.

Rezultati nakon Septembra 1 2020

Ovde možete pratiti tekuće rezultate.

Uvid u radove je putem mejla.

23. 08. 2020.

Prijava za ispit u Septembar 1

Molimo studente koji izlaze na ispit u ispitnom roku Septembar1 da popune sledeći upitnik.

17. 08. 2020.

Rezultati nakon Jun1 2020

Ovde možete pratiti tekuće rezultate.

Izvinite što ste duže čekali na rezulate od obećanog. Hvala Vam na strpljenju i razumevanju.

Uvid u radove je putem mejla.

07. 06. 2020.

Prijava za ispit u Jun 1

Molimo studente koji izlaze na ispit u ispitnom roku Jun1 da popune sledeći upitnik.

04. 06. 2020.

Teorijski deo ispita

Studenti zainteresovani za polaganje teorije mogu se javiti mejlom radi dogovora termina za online ispitivanje.

16. 04. 2020.

Polaganje ispita

U skladu sa tekućom situacijom, pozivaju se studenti da ako su u mogućnosti što pre završavaju svoje praktične seminarske radove. Konsultacije su moguće online, kao i odbrana.

Što se tiče rokova za odbranu seminarskih radova, oni se ukidaju i možete završiti i odbraniti seminarski rad i u kasnijim terminima. Sa normalizacijom stanja, dogovaramo se preciznije za dalje korake.

Svi koji su položili deo ispita do sada (teorijski, praktični, seminarski), poeni će im se računati i naredne godine (ukoliko, iz bilo kog razloga, ne uspeju da završe svoje obaveze regularno u ovoj školskoj godini).

21. 03. 2020.

Teorijski deo ispita

Ispit se otkazuje do daljnjeg.
Teorijski deo ispita biće organizovan u sredu 18. marta u 17h. Ukoliko se neko od prijavljenih studenata predomisli, obavezno neka se javi mejlom do 16. marta. Ukoliko neko od studenata želi da se naknadno prijavi, to je takođe u redu do ponedeljka 16. marta.

09. 03. 2020.

Predavanje na Argo seminaru, u oblasti verifikacije softvera

U četvrtak 12.3.2020. sa početkom od 18:15 u sali 718 održaće se sastanak Argo seminara sa narednim programom:

Predavač: Pavle Subotić, Amazon

Naslov: "Rinser: Concise Explanations in Static Analysis Driven Code Reviews"

Apstrakt: We consider the problem of producing efficiently actionable evidence from a static analyzer. That is, we seek to close the gap between static analyzers and their human users by providing precisely the right evidence that enables users to accept or dismiss potential bugs reported by the analyzer. In this talk, I present Rinser, a tool used at Amazon to improve the evidence developers receive from static analyzers. Specifically, Rinser provides an on-demand method to check the realdizability of potential bugs reported by the static analyzer Infer. We have developed an initial version of Rinser as a post-analysis automated-reasoning pass based on refutation reasoning. On industrial code bases, our tool is able to surface possible bugs to developers with evidence traces on average 4x steps shorter than standard Infer traces. Foremost, our tool has eased the adaption of static analyzers at Amazon and driven additional dialogue between engineers on the quality of the code. As a bonus, it has also provided a means to soundly remove many trivial false-positive warnings, thereby also reducing the subsequent triaging effort.

09. 03. 2020.

Teorijski deo ispita

Sredinom marta biće organizovan još jedan termin za polaganje teorijskog dela ispita. Zainteresovani studenti potrebno je da se jave mejlom između prvog i petog marta.

15. 02. 2020.

Teorijski deo ispita

Termin polaganja teorije: petak 14. februar u 10:40 u učionici 821 (po rasporedu je ova učionica prazna, ako slučajno ne bude bila, onda neka druga učionica koja bude prazna ili kabinet 716).

07. 02. 2020.

Rezultati nakon Februara 2020

Ovde možete pratiti tekuće rezultate.

Izvinite što ste duže čekali na rezulate od obećanog. Hvala Vam na strpljenju i razumevanju.

Uvid u radove sa praktičnog dela ispita biće u subotu 8.2.2020 u 12:30 na Studentskom trgu.

07. 02. 2020.

Rezultati praktičnog dela ispita

Rezultati praktičnog dela ispita biće objavljeni nakon nedelje, zbog bolesti asistenta (grip). Polaganje praktičnog i teorijskog dela ispita nije povezano (tj jednom osvojeni poeni se unose u tabelu i važe i u narednom ispitnom roku).

31. 01. 2020.

Компанија Vtool

Компанија Vtool бави се паметном верификацијом софтвера. Они су отворили конкурс за запошљавање студената који можете видети овде.

27. 01. 2020.

Obaveštenje

Pored termina u nedelju 26. januara, teorijski deo ispita možete da polažete i u još jednom roku, tj 2. februara u 9h (na Trgu). Za to polaganje potrebno je da mi se javite mejlom do petka 31. januara u 12h. Studenti koji taj dan polažu neki drugi ispit, a žele da izađu na teoriju, takođe treba da mi se jave mejlom radi dogovora.

24. 01. 2020.

Prijava za ispit u Februaru

Molimo studente koji izlaze na ispit u februarskombroku da popune sledeći upitnik.

24. 01. 2020.

Rezultati nakon Januara 2020

Ovde možete pratiti tekuće rezultate.

21. 01. 2020.

Teorijski seminarski rad

Teorijski seminarski rad možete predati preko naredne forme. Rok za predaju seminarskog rada je 15. januar u 23:59. Ukoliko imate neke nedoumice ili pitanja, javite se mejlom.

08. 01. 2020.

Prijava za ispit u Januaru 1

Molimo studente koji izlaze na ispit u Januaru 1 da popune sledeći upitnik.

06. 01. 2020.

Praktični seminarski radovi

Predlog tema za praktične seminarske radove se može pogledati ovde. Kada izaberete temu, potrebno je da se javite mejlom (i nastavniku i asistentu, istovremeno) radi preciziranja same teme (i radi, u nekim situacijama, uklanjanja teme sa spiska raspoloživih tema). Studenti se pozivaju da i sami predlože neku temu, ukoliko imaju ideju, a koja bi bila u skladu sa gradivom koje se radi na kursu.

05. 01. 2020.

Promena termina vežbi

Umesto časa vežbi u utorak 24.12.2019. imaćemo vežbe u četvrtak 26.12.2019. od 12-15h u učionici JAG2.

18. 12. 2019.

Predavanja na Argo seminaru

Pozivaju se studenti da prisustvuju narednim predavanjima iz oblasti verifikacije softvera/programski jezici.

U četvrtak 26.12.2019. sa početkom u 18:15h u sali 718 odrzaće se sastanak Argo seminara sa narednim programom:

  1. Alen Arslanagić, University of Groningen: Lightweight Typestate Analysis
  2. Marija Selaković, Huawei Research: Dynamic Analysis and Test Generation for JavaScript
  3. Pavle Subotić, Amazon: Towards Verification of React Applications
  4. Stefan Jakšić, Austrian Institute of Technology: Monitoring of Cyber-Physical Systems for Correctness and Robustness
Apstrakte predavanja mozete videti ovde: http://argo.matf.bg.ac.rs/?content=seminar_sr_lat

Kratke biografije predavača:

  • Alen is a PhD student at the University of Groningen under Jorge Perez. He completed his masters studies at the University of Novi Sad. Alen recently completed a research internship with the Amazon Automated Reasoning Group (ARG).
  • Dr. Marija Selaković je senior inzenjer u Huawei istraživačkom centru u Dresdenu. Pre dolaska u Huawei, Marija je bila asistent na tehnickom univerzitetu u Darmstadtu, gde je i završila doktorske studije u oblasti analize koda i automatskog testiranja. Tokom doktorskih studija Marija je dva puta bila praktikant u istraživačkom centru Microsofta u Redmondu. Master studije je završila na VU univerzitetu u Amsterdamu i univerzitetu L’Aquila u Italiji. Osnovne studije je završila na Fakultetu organizacionih nauka u Beogradu.
  • Dr. Pavle Subotic is an Applied Scientist at the Amazon Automated Reasoning Group (ARG). Previously he worked on R&D projects at AWS, Oracle, and Toshiba. He completed his PhD at University College London (UCL) under Prof. Byron Cook and is a co-founder of the Souffle open source compiler project.
  • Dr. Stefan Jaksic is a Scientist at AIT Austrian Institute of Technology GmbH, in the Center for Digital Safety and Security. Stefan obtained his PhD degree from TU Wien in 2018, successfully defending his thesis ‘Real-time Monitoring for Correctness and Robustness'. He is co-author of several peer-reviewed conference papers in the field of Runtime Verification. He is involved in national and European research projects in the field of verification of mixed-signal systems such as Internet of Things (IoT) and Cyber-Physical Systems (CPSs). He is also lecturing Model-Based System and Software Engineering at FH Campus Wien.

17. 12. 2019.

Prijava za praktični seminarski rad

Ukoliko ste stekli uslov za izradu praktičnog seminarskog rada, potrebno je da prijavite putem sledeće ankete. Ako imate svoj tim, prijavljujete ceo tim jednim popunjavanjem. Ukoliko nemate svoj tim, prijavite se samostalno, pa ćemo Vam dodeliti tim.

02. 12. 2019.

Prijava teorijskog seminarskog

Zbog izmena u pravilima upisa na predmete na master studijama, rok za prijavu teorijskog seminarskog se pomera na 6. decembar.

01. 12. 2019.

Nadoknada vežbi do kraja semestra

Na osnovu odgovora većine (67%), nadoknada propuštenih vežbi biće četvrtkom u učionici JAG2 od 12-15h, i to 28.11, 5.12, 12.12, 19.12.

26. 11. 2019.

Rezultati

Ovde možete pratiti tekuće rezultate.

26. 11. 2019.

Nadoknada vežbi do kraja semestra

Molim Vas da mi popunite anketu i odaberete način organizacije nadoknade časova vežbi. Anketa

26. 11. 2019.

Master radovi

Kao odgovor na pitanje koje mi je nezavisno postavilo nekoliko studenata, na narednoj adresi mogu se naći odbranjeni master radovi kojima sam bila mentor. Većina je u oblastima verifikacije softvera, programskih jezika i kompajlera, ali ima i drugih oblasti (uz svaki rad navedene su oblasti kojima rad pripada).

16. 11. 2019.

Ispit u kolokvijumskoj nedelji

Teorijski ispit u kolokvijumskoj nedelji mogu da polažu svi studenti (tj i oni koji prenose poene od prošle godine i kojima je rok za polaganje najkasnije januar 2020).

13. 11. 2019.

Teorijski seminarski rad

Prijava za izradu teorijskog seminarskog rada vrši se preko naredne forme. Prijava za izradu seminarskog rada je otvorena do 01.12.2019. Rok za predaju teorijskog seminarskog rada je 15. januar. Teorijski seminarski rad se radi samostalno.

Uz prijavu predlažete temu na kojoj želite da radite i njeno kratko obrazloženje (tj podteme koje bi bile pokrivene i početna literatura). Nakon prijave, dobićete potvrdu da li se tema u potpunosti prihvata ili su potrebne nekakve dodatne modifikacije. Spisak izabranih i odobrenih tema biće ažuriran na svaka 2-3 dana i moći će da se prati ovde. Ukoliko Vaša tema nije na spisku duže od dva dana nakon njenog prijavljivanja, pošaljite mi mejl.

Teme koje je moguće izabrati vezane su za oblasti koje se obrađuju na predavanjima ili za naučne radove iz tih oblasti. U prvom slučaju, rad treba da pokrije ili proširi neku temu sa predavanja za koju već ne postoji dodatni materijal (za neke teme postoje dodatni materijali koje možete naći u okviru kartice za predavanja) ili ukoliko postoji dodatni materijal, onda da to bude nekakvo proširenje tog materijala. Na primer, tema može da bude neka specificna vrsta terstiranja koja se ne obrađuje detaljno, ili neki alat/algoritam za testiranje/profajliranje/debagovanje, ili neki interesantan algoritam ili primena simboličkog izvršavanja/proveravanju modela/apstraktne interpretacije, ili opis nekog alata koji se zasniva na simboličkom izvršavanju/proveravanju modelu/apstraktnoj interpretaciji, ili neki detalji vezani za neki teorijski koncept (npr nacini izražavanja nekih interesantnih svojstava kroz LTL, detalji vezani za CTL/CTL*)... Tema može da bude i nešto što ovde nije nabrojano kroz primere, sve dok se uklapa ili dok dopunjuje osnovne koncepte koji se obrađuju na predavanjima.

Neki konkretni primeri tema (koje su nuđene prošle godine ali nisu obrađene):
1. Kako napraviti alat za Valgrind
2. CTL i primeri svojstava koji se mogu izraziti u CTL-u.
3. Pojam invarijante. Primeri.

Simboličko izvršavanje:
Početna literatura: A Survey of Symbolic Execution Techniques ACM Computing Surveys (CSUR), Volume 51 Issue 3, July 2018
Besplatno dostupna verzija rada
Za neke teme je dovoljno korisitit ovaj rad i to su teme koje se uglavnom uklapaju u teme sa predavanja. Za neke teme potrebno je uci detaljnije u citiranu literaturu i procitati odgovarajuci rad/radove.
1. Simbolicko izvrsavanje unazad (Symbolic Backward Execution)
2. Eksplozija putanja i regulisanje broja putanji (Path Subsumption and Equivalence, Under-constrained Symbolic Execution)
3. Modelovanje memorije (Fully Symbolic Memory, Address Concretization, Partial Memory Modeling, Lazy Initialization)
4. Buduci pravci simbolickog izvrsavanja (Further directions)

Ukoliko se odlučite za prikaz naučnog rada iz oblasti, potrebno je da rad ili ima više od 100 citata ili ukoliko je novijeg datuma, da je objavljen u nekom pristojnom časopisu ili na nekoj dobroj konferenciji. 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 koje se odnose na radove koji su od izuzetnog značaja za oblast). 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).

Obim seminarskog rada i formu seminarskog rada možete naći u okviru latex šablona ovde.

Za sva dodatna pitanja/nejasnoće, napišite mejl.

05. 11. 2019.

Kolokvijum u kolokvijumskoj nedelji

S obzirom na ukupan broj održanih predavanja u terminima vežbi, predavanja će biti završena pre kolovijumske nedelje. Zbog toga će studenti dobiti priliku da polažu celokupnu teoriju u terminu kolokvijuma. Polaganje teorije je ujedno i preduslov za dobijanje teme za praktični seminarski rad.

U okviru kolokvijumske nedelje, teorija se može polagati kompletno ili parcijanlo. Kompletno znači da se polaže cela teorija (5 pitanja), a parcijalno znači da se polaže deo terorije (3 pitanja - gradivo zaključno sa simboličkim izvršavanjem). U slučaju da izaberete parcijalno polaganje, to znači da je potrebno da izađete ponovo na teorijski deo ispita (u januarskom ili februarskom ispitnom roku) i da tada polažete preostala dva pitanja.

21. 10. 2019.

Vežbe u četvrtoj nedelji

Umesto časova vežbi, u utorak 22.10.2019 biće održana tri časa predavanja (i dalje zbog bolesti asistenta). U sredu u terminu predavanja biće takođe održana predavanja. Nadoknada vežbi će biti dogovorena sa studentima u toku semestra (biće iskorišćeni termini predavanja).

21. 10. 2019.

Anketa

Mole se studenti da popune sledeću anketu radi bolje komunikacije i organizacije nastave.

13. 10. 2019.

Vežbe u trećoj nedelji

Umesto časova vežbi, u utorak 15.10.2019 biće održana tri časa predavanja (zbog bolesti asistenta). U sredu u terminu predavanja biće takođe održana predavanja. Nadoknada vežbi će biti dogovorena sa studentima u toku semestra (biće iskorišćeni termini predavanja).

12. 10. 2019.

Vežbe u drugoj nedelji

Umesto časova vežbi, u utorak 8.10.2019 biće održana tri časa predavanja (zbog bolesti asistenta). U sredu u terminu predavanja biće održan jedan ipo čas predavanja. Nadoknada vežbi će biti dogovorena sa studentima u toku semestra.

06. 10. 2019.

Prenos poena

Studenti koji su ispunili predispitne obaveze prethodne akademske godine a nisu položili ispit, mogu preneti poene u narednu godinu, ali će se ti poeni računati samo ukoliko se ispit polaže u januarskom ispitnom roku. U suprotnom, poeni se poništavaju i da bi se ispit položio potrebno je ponovo da se ostvare poeni na predispitnim obavezama.

03. 10. 2019.

Vežbe u prvoj nedelji

Vežbe neće biti održane u utorak 1.10.2019. zbog bolesti asistenta.

Termin nadoknade biće dogovoren sa studentima na narednim časovima.

30. 09. 2019.

Početak semestra

Svim studentima želimo uspešan početak zimskog semestra školske 2019/20. godine!

29. 09. 2019.

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