Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/782
DC FieldValueLanguage
dc.contributor.authorVujošević Janičić, Milenaen_US
dc.contributor.authorKuncak, Viktoren_US
dc.date.accessioned2022-08-15T15:37:16Z-
dc.date.available2022-08-15T15:37:16Z-
dc.date.issued2012-02-07-
dc.identifier.isbn9783642277047-
dc.identifier.issn03029743en
dc.identifier.urihttps://research.matf.bg.ac.rs/handle/123456789/782-
dc.description.abstractWe present design and evaluation of LAV, a new open-source tool for statically checking program assertions and errors. LAV integrates into the popular LLVM infrastructure for compilation and analysis. LAV uses symbolic execution to construct a first-order logic formula that models the behavior of each basic blocks. It models the relationships between basic blocks using propositional formulas. By combining these two kinds of formulas LAV generates polynomial-sized verification conditions for loop-free code. It uses underapproximating or overapproximating unrolling to handle loops. LAV can pass generated verification conditions to one of the several SMT solvers: Boolector, MathSAT, Yices, and Z3. Our experiments with small 200 benchmarks suggest that LAV is competitive with related tools, so it can be used as an effective alternative for certain verification tasks. The experience also shows that LAV provides significant help in analyzing student programs and providing feedback to students in everyday university practice. © 2012 Springer-Verlag.en
dc.relation.ispartofLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)en_US
dc.titleDevelopment and evaluation of LAV: An SMT-based error finding platform: System descriptionen_US
dc.typeConference Paperen_US
dc.relation.publicationInternational Conference on Verified Software: Tools, Theories, Experiments VSTTE 2012en_US
dc.identifier.doi10.1007/978-3-642-27705-4_9-
dc.identifier.scopus2-s2.0-84856518334-
dc.identifier.urlhttps://api.elsevier.com/content/abstract/scopus_id/84856518334-
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.relation.firstpage98en_US
dc.relation.lastpage113en_US
dc.relation.volume7152 LNCSen_US
item.fulltextNo Fulltext-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.cerifentitytypePublications-
item.grantfulltextnone-
item.openairetypeConference Paper-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.orcid0000-0001-5396-0644-
Appears in Collections:Research outputs
Show simple item record

SCOPUSTM   
Citations

16
checked on Dec 18, 2024

Page view(s)

10
checked on Dec 24, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.