Automated generation and checking of verification conditions

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