Model Checking of Concurrent Software Systems via Heuristic-Guided SAT Solving - Fundamentals of Software Engineering Access content directly
Conference Papers Year : 2017

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

Nils Timm
  • Function : Author
  • PersonId : 1030399
Stefan Gruner
  • Function : Author
  • PersonId : 848507

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.
Fichier principal
Vignette du fichier
459025_1_En_16_Chapter.pdf (342.91 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01760864 , version 1 (06-04-2018)

Licence

Attribution

Identifiers

Cite

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⟩
183 View
84 Download

Altmetric

Share

Gmail Facebook X LinkedIn More