Please use this identifier to cite or link to this item:
https://research.matf.bg.ac.rs/handle/123456789/783
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Vujošević Janičić, Milena | en_US |
dc.date.accessioned | 2022-08-15T15:37:16Z | - |
dc.date.available | 2022-08-15T15:37:16Z | - |
dc.date.issued | 2020-05-01 | - |
dc.identifier.issn | 02181940 | en |
dc.identifier.uri | https://research.matf.bg.ac.rs/handle/123456789/783 | - |
dc.description.abstract | Automated and reliable software verification is of crucial importance for development of high-quality software. Formal methods can be used for finding different kinds of bugs without executing the software, for example, for finding possible run-time errors. The methods like model checking and symbolic execution offer very precise static analysis but on real world programs do not always scale well. One way to tackle the scalability problem is to apply new concurrent and sequential approaches to complex algorithms used in these kinds of software analysis. In this paper, we compare different variants of bounded model checking and propose two concurrent approaches: concurrency of intra-procedural analysis and concurrency of inter-procedural analysis. We implemented these approaches in a software verification tool LAV, a tool that is based on bounded model checking and symbolic execution. For assessing the improvements gained, we experimentally compared the concurrent approaches with the standard bounded model checking approach (where all correctness conditions are put into a single compound formula) and with a sequential approach (where correctness conditions are checked separately, one after the other). The results show that, in many cases, the proposed concurrent approaches give significant improvements. | en |
dc.relation.ispartof | International Journal of Software Engineering and Knowledge Engineering | en |
dc.subject | automated bug finding | en |
dc.subject | bounded model checking | en |
dc.subject | parallel and concurrent approaches | en |
dc.subject | Software verification | en |
dc.title | Concurrent Bug Finding Based on Bounded Model Checking | en_US |
dc.type | Article | en_US |
dc.identifier.doi | 10.1142/S0218194020500242 | - |
dc.identifier.scopus | 2-s2.0-85087326651 | - |
dc.identifier.url | https://api.elsevier.com/content/abstract/scopus_id/85087326651 | - |
dc.contributor.affiliation | Informatics and Computer Science | en_US |
dc.relation.firstpage | 669 | en |
dc.relation.lastpage | 694 | en |
dc.relation.volume | 30 | en |
dc.relation.issue | 5 | en |
item.fulltext | No Fulltext | - |
item.openairecristype | http://purl.org/coar/resource_type/c_18cf | - |
item.cerifentitytype | Publications | - |
item.grantfulltext | none | - |
item.openairetype | Article | - |
crisitem.author.dept | Informatics and Computer Science | - |
crisitem.author.orcid | 0000-0001-5396-0644 | - |
Appears in Collections: | Research outputs |
SCOPUSTM
Citations
1
checked on Dec 21, 2024
Page view(s)
12
checked on Dec 24, 2024
Google ScholarTM
Check
Altmetric
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.