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

https://hal.inria.fr/hal-01760864
Contributor : Hal Ifip <>
Submitted on : Friday, April 6, 2018 - 5:21:16 PM
Last modification on : Sunday, November 22, 2020 - 12:52:02 PM

File

459025_1_En_16_Chapter.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

369

Files downloads

89