Skip to Main content Skip to Navigation
Conference papers

Model Checking of Concurrent Software Systems via Heuristic-Guided SAT Solving

Abstract : An established approach to software verification is SAT-based bounded model checking where a state space model is encoded as a Boolean formula and the exploration is performed via SAT solving. Most existing approaches in SAT-based model checking rely on general-purpose solvers that do not exploit the structural features of the encoding. Aiming at a significantly better runtime performance in such settings, we show in this paper that SAT algorithms can be specifically tailored w.r.t. the structure of the Boolean encoding of the model checking problem to be solved. We define a state space encoding of concurrent software systems that preserves control flow information. This allows to modify the solver such that the number of SAT decision levels can be significantly reduced by assigning a set of atoms at each level. Such set assignment always characterises a location in the control flow of the encoded system. Moreover, we introduce heuristics that guide the SAT search into directions where a violation of the property of interest may be most likely detected. The heuristic approach enables to quickly discover errors while keeping the actually explored part of the state space small.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Friday, April 6, 2018 - 5:21:16 PM
Last modification on : Sunday, November 22, 2020 - 12:52:02 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Nils Timm, Stefan Gruner, Prince Sibanda. Model Checking of Concurrent Software Systems via Heuristic-Guided SAT Solving. 7th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2017, Teheran, Iran. pp.244-259, ⟨10.1007/978-3-319-68972-2_16⟩. ⟨hal-01760864⟩



Record views


Files downloads