Please be advised that the site will be down for maintenance on Sunday, September 1, 2024, from 08:00 to 18:00, and again on Monday, September 2, 2024, from 08:00 to 09:00. We apologize for any inconvenience this may cause.
dc.contributor.author | Timm, Nils![]() |
|
dc.contributor.author | Gruner, Stefan![]() |
|
dc.date.accessioned | 2020-08-26T15:23:07Z | |
dc.date.available | 2020-08-26T15:23:07Z | |
dc.date.issued | 2019-04 | |
dc.description.abstract | We present a technique for verifying concurrent software systems via SAT-based three-valued bounded model checking. It is based on a direct transfer of the system to be analysed and a temporal logic property into a propositional logic formula that encodes the corresponding model checking problem. In our approach we first employ three-valued abstraction which gives us an abstract system defined over predicates with the possible truth values true, false and unknown. The state space of the abstract system is then logically encoded. The verification result of the encoded three-valued model checking problem can be obtained via two satisfiability checks, one for an over-approximation of the encoding and one for an under-approximation. True and false results can be immediately transferred to the system under consideration. In case of an unknown result, the current abstraction is too imprecise for a definite outcome. In order to achieve the necessary precision, we have developed a novel cause-guided abstraction refinement procedure. An unknown result always entails a truth assignment that only satisfies the over-approximation, but not the under-approximation. We determine the propositional logic clauses of the under-approximation that are not satisfied under the assignment. These clauses contain unknown as a constant. Each unknown is associated with a cause of uncertainty that refers to missing predicates that are required for a definite model checking result. Our procedure adds these predicates to the abstraction and constructs the encoding corresponding to the refined model checking problem. The procedure is iteratively applied until a definite result can be obtained. We have integrated our novel refinement approach into a SAT-based three-valued bounded model checker. In an experimental evaluation, we show that our approach allows to automatically and quickly reach the right level of abstraction for solving software verification tasks. | en_ZA |
dc.description.department | Computer Science | en_ZA |
dc.description.librarian | hj2020 | en_ZA |
dc.description.uri | http://www.elsevier.com/locate/scico | en_ZA |
dc.identifier.citation | Timm, N. & Gruner, S. 2019, 'Three-valued bounded model checking with cause-guided abstraction refinement', Science of Computer Programming, vol. 175, pp. 37-62. | en_ZA |
dc.identifier.issn | 0167-6423 (print) | |
dc.identifier.issn | 1872-7964 (online) | |
dc.identifier.other | 10.1016/j.scico.2019.02.002 | |
dc.identifier.uri | http://hdl.handle.net/2263/75921 | |
dc.language.iso | en | en_ZA |
dc.publisher | Elsevier | en_ZA |
dc.rights | © 2019 Elsevier B.V. All rights reserved. Notice : this is the author’s version of a work that was accepted for publication in Science of Computer Programming. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. A definitive version was subsequently published in Science of Computer Programming, vol. 175, pp. 37-62, 2019. doi : 10.1016/j.scico.2019.02.002. | en_ZA |
dc.subject | Bounded model checking | en_ZA |
dc.subject | Cause-guided abstraction refinement | en_ZA |
dc.subject | Concurrent software systems | en_ZA |
dc.subject | Fairness | en_ZA |
dc.subject | Three-valued abstraction (3VA) | en_ZA |
dc.title | Three-valued bounded model checking with cause-guided abstraction refinement | en_ZA |
dc.type | Preprint Article | en_ZA |