LAV is a system for statically verifying program assertions and locating bugs such as buffer overflows, pointer errors and division by zero. LAV is primarily aimed at analyzing programs written in ...the programming language C. Since LAV uses the popular LLVM intermediate code representation, it can also analyze programs written in other procedural languages. Also, the proposed approach can be used with any other similar intermediate low level code representation. System combines symbolic execution, SAT encoding of program’s control-flow, and elements of bounded model checking. LAV represents the program meaning using first-order logic (FOL) formulas and generates final verification conditions as FOL formulas. Each block of the code (blocks have no internal branchings and no loops) is represented by a FOL formula obtained through symbolic execution. Symbolic execution, however, is not performed between different blocks. Instead, relationships between blocks are modeled by propositional variables encoding transitions between blocks. LAV constructs formulas that encode block semantics once for each block. Then, it combines these formulas with propositional formulas encoding the transitions between the blocks. The resulting compound FOL formulas describe correctness and incorrectness conditions of individual instructions. These formulas are checked by an SMT solver which covers suitable combination of theories. Theories that can be used for modeling correctness conditions are: theory of linear arithmetic, theory of bit-vectors, theory of uninterpreted functions, and theory of arrays. Based on the results obtained from the solver, the analyzed command may be given the status safe (the command does not lead to an error), flawed (the command always leads to an error), unsafe (the command may lead to an error) or unreachable (the command will never be executed). If a command cannot be proved to be safe, LAV translates a potential counterexample from the solver into a program trace that exhibits this error. It also extracts the values of relevant program variables along this trace. The proposed system is implemented in the programming language C++, as a publicly available and open source tool named LAV. LAV has support for several SMT solvers (Boolector, MathSAT, Yices, and Z3). Experimental evaluation on a corpus of C programs, which are designed to demonstrate areas of strengths and weaknesses of different verification techniques, suggests that LAV is competitive with related tools. Also, experimental results show a big advantage of the proposed system compared to symbolic execution applied to programs containing a big number of possible execution paths. The proposed approach allows determining status of commands in programs which are beyond the scope of analysis that can be done by symbolic execution tools. LAV is successfully applied in educational context where it was used for finding bugs in programs written by students at introductory programming course. This application showed that in these programs there is a large number of bugs that a verification tool can efficiently find. Experimental results on a corpus of students’ programs showed that LAV can find bugs that cannot be found by commonly used automated testing techniques. Also, it is shown that LAV can improve evaluation of students’s assignments: (i) by providing useful and helpful feedback to students, which is important in the learning process, and (ii) by improving automated grading process, which is especially important to teachers.
LAV je sistem za automatsko generisanje i proveravanje uslova ispravnosti programa. Sistem je namenjen prvenstveno analizi programa napisanih u programskom jeziku S, ali, pošto koristi LLVM međujezik, može se primeniti i za analizu programa napisanih u drugim proceduralnim programskim jezicima. Sistem kombinuje simboličko izvršavanje, opisivanje ponašanja programa iskaznim promenljivama i proveravanje ograničenih modela. Individualni blokovi LLVM međukoda modeluju se formulama logike prvog reda koje se konstruišu simboličkim izvršavanjem. Relacije između blokova se modeluju iskaznim promenljivama. Formule, koje opisuju ponašanja blokova koda zajedno sa relacijama između blokova, kombinuju se i na osnovu njih prave se formule koje opisuju ponašanje programa. Te formule koriste se za formiranje uslova ispravnosti pojedinačnih komandi programa. Uslovi ispravnosti šalju se na proveru SMT rešavaču koji pokriva odgovarajuću kombinaciju teorija. Podržane teorije, u kojima je moguće modelovati uslove ispravnosti programa, su teorija linearne aritmetike, teorija bit vektora, teorija neinterpretiranih funkcija i teorija nizova. Komanda može imati status bezbedne (izvršavanje komande ne dovodi do greške), neispravne (izvršavanje komande sigurno dovodi do greške), nebezbedne (izvršavanje komande može da dovede do greške) i nedostižne (do izvršavanja komande nikada neće doći). Predloženi sistem je implementiran u programskom jeziku C++ kao alat LAV koji je javno dostupan i otvorenog koda. U okviru alata postoji podrška za rad sa nekoliko SMT rešavača (Boolector, MathSAT, Yices i Z3). Eksperimentalni rezultati na korpusu S programa, koji služe za utvrđivanje mogućnosti verifikacijskih alata, pokazuju da je predstavljen pristup uporediv sa postojećim srodnim alatima. Takođe, eksperimentalni rezultati pokazuju prednost predloženog sistema u odnosu na simboličko izvršavanje u programima u kojima postoji veliki broj mogućih putanja. Kompaktno modelovanje mogućih putanja kroz program omogućava utvrđivanje ispravnosti komandi u programima koji su van domašaja alata za simboličko izvršavanje. LAV je uspešno primenjen i u kontekstu obrazovanja gde je korišćen za otkrivanje grešaka u studentskim radovima. Ovom primenom pokazano je da u studentskim radovima uvodnog kursa programiranja postoji veliki broj grešaka koje verifikacijski alat može efikasno da pronađe. Eksperimentalni rezultati pokazali su da je verifikacija efikasnija od trenutno dominantno korišćenih tehnika automatskog testiranja jer može da otkrije greške u studentskim programima koje su van domašaja ovih tehnika. Takođe, pokazano je kako LAV može da unapredi automatsku evaluaciju studentskih radova na polju generisanja kvalitetnih, razumljivih i pouzdanih podataka o rezultatima rada studenta, kao i na polju automatskog ocenjivanja.
Moj cilj nije bio da ispitujem implementaciju svih poznatih metoda za izračunavanje generalisanih metoda. Takođe mi nije bio cilj da poredim direktne i iterativne metode. Ja sam proučavao pojavu ...problema povećanje broja operacija u pokretnom zarezu, tokom iteracije, prouzrokovane ponovnim izračunaranjem pojedinih izraza, u numeričkim izračunavanjima pseudoinverza, kao i vezu proceduralnih i neproceduralnih programskih jezika i njihovu mogućnost u uzračunavanju generalisanih inverza. Predložio sam nove metode i nove algoritme, kao i modifikacije postojećih metoda i algoritama, koji rešavaju pomenute probleme. Sve je bazirano na mogućnostima paketa MATHEMATICA kao tipičnog primera programskog paketa za simboličko izračunavanje, i paketa DELPHI kao predstavnika proceduralnih programskih jezika. Metodi i algoritmi koje sam predložio implementirani su i testirani na numeričkim i racionalnim matricama, polinomijalnim matricama, retkoposednutim matricama i na bazama podataka. Oni su primenljivi na sve proceduralne programske jezike.
Numeričke bioelektromagnetne simulacijske metode prodrlih elektromagnetnih polja koriste se za izračunavanje komponenata polja u biološkim jedinkama. Elektromagnetno polje nije jednako izvan i unutar ...biološkog subjekta. Izračunavanje energije apsorbirane iz poznatog izvora, kao što su mobilni telefoni u području glave, preduvjet je za ispitivanje biološkog utjecaja elektromagnetnog polja. Pri ovim istraživanjima koriste se približni anatomski modeli i na osnovi njih se izračunavaju komponente polja i apsorbirana energija. Nužno je uspostaviti vezu između odgovarajućih približnih anatomskih modela s realnom strukturom, kako bi se mogli istraživati biološki efekti u dijelovima organa i tkiva. Zbog toga se u ovom radu predlaže novi pristup istraživanju bioloških efekata. U osnovi metode je kombinacija dviju različitih tehnika: 1) numeričke elektromagnetne simulacije kojom se izračunavaju komponente polja u približnom anatomskom modelu i 2) MRI metoda (Magnetic resonance imaging) kojom se precizno lociraju mjesta s povišenom apsorpcijom. Kombiniranje se postiže preklapanjem slika dobivenih jednom i drugom metodom, čime se utvrđuje precizna lokacija mjesta s maksimalnim efektima apsorpcije. Na taj način mogu se pronaći mjesta na kojima bi trebao biti najizraženiji biološki učinak. Novi pristup uspješno prevladava ograničenja koja su postojala pri radu s približnim anatomskim modelima.
Naši majstori u mljekarama vrlo često griješe pri izračunavanju i određivanju prosječnog sadržaja masti u mlijeku. Obično uzimaju uzorak mlijeka od svakog vozara i dobivene analize zbroje, razdijele ...s brojem vozara te time smatraju da su dobili ispravan prosjek. Ovakav način određivanja prosječnog sadržaja masti u mlijeku može se primijeniti samo u onom slučaju, kad svi vozari imaju jednaku količinu mlijeka.
Uspoređivane su količine suhe tvari mlijeka određene metodom sušenja pri 102 °C i izračunavanjem, Flajšmanovom (Fleischmann) formulom analizom 94 uzorka. Statističkom obradom, dobivenih vrijednosti ...primjenom T-testa ustanovljena je veoma značajna razlika (p<0,001) između rezultata obje metode. Količine izračunate po Flajšmanovoj formuli imaju uvijek veću vrijednost (t = -8,15) pa se ne mogu koristiti za procjenu kvaliteta mlijeka.
PDF
