Please use this identifier to cite or link to this item:
https://research.matf.bg.ac.rs/handle/123456789/783
Title: | Concurrent Bug Finding Based on Bounded Model Checking | Authors: | Vujošević Janičić, Milena | Affiliations: | Informatics and Computer Science | Keywords: | automated bug finding;bounded model checking;parallel and concurrent approaches;Software verification | Issue Date: | 1-May-2020 | Journal: | International Journal of Software Engineering and Knowledge Engineering | 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. |
URI: | https://research.matf.bg.ac.rs/handle/123456789/783 | ISSN: | 02181940 | DOI: | 10.1142/S0218194020500242 |
Appears in Collections: | Research outputs |
Show full item record
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.