AUTOMATSKO GENERISANJE I PROVERAVANJE USLOVA ISPRAVNOSTI PROGRAMA

eBibliothek Repositorium

 
 

AUTOMATSKO GENERISANJE I PROVERAVANJE USLOVA ISPRAVNOSTI PROGRAMA

Zur Kurzanzeige

dc.contributor.advisor Tošić, Dušan
dc.contributor.author Vujošević Janičić, Milena
dc.date.accessioned 2016-06-22T16:42:11Z
dc.date.available 2016-06-22T16:42:11Z
dc.date.issued 2013
dc.identifier.uri http://hdl.handle.net/123456789/4231
dc.description.abstract 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 Ñ++, 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. en_US
dc.description.provenance Submitted by Slavisha Milisavljevic (slavisha) on 2016-06-22T16:42:11Z No. of bitstreams: 1 phdVujosevicJanicicMilena.pdf: 1748120 bytes, checksum: 986921cf0c70e8d15e1f2a3d346be776 (MD5) en
dc.description.provenance Made available in DSpace on 2016-06-22T16:42:11Z (GMT). No. of bitstreams: 1 phdVujosevicJanicicMilena.pdf: 1748120 bytes, checksum: 986921cf0c70e8d15e1f2a3d346be776 (MD5) Previous issue date: 2013 en
dc.language.iso sr en_US
dc.publisher Beograd en_US
dc.title AUTOMATSKO GENERISANJE I PROVERAVANJE USLOVA ISPRAVNOSTI PROGRAMA en_US
mf.author.birth-date 1980-06-03
mf.author.birth-place Beograd en_US
mf.author.birth-country Srbija en_US
mf.author.residence-state Srbija en_US
mf.author.citizenship Srpsko en_US
mf.author.nationality Srpkinja en_US
mf.contributor.committee Kunčak, Viktor
mf.contributor.committee Marić, Filip
mf.university.faculty Mathematical Faculty en_US
mf.document.references 181 en_US
mf.document.pages 145 en_US
mf.document.location Beograd en_US
mf.document.genealogy-project No en_US
mf.university Belgrade University en_US

Dateien zu dieser Ressource

Dateien Größe Format Anzeige
phdVujosevicJanicicMilena.pdf 1.748Mb PDF Öffnen

Das Dokument erscheint in:

Zur Kurzanzeige