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.
Joubert, F.J.; Pretorius, Leon(Southern African Institute for Industrial Engineering, 2017-08-31)
When introducing quantified risk assessments at a South African state-owned freight company, a skills gap was found during the identification and quantified risk analysis. To help with risk identification, a checklist of ...
Maina, J.W. (James); Denneman, Erik; De Beer, M.(SATC, 2008-07)
Paper presented at the 27th Annual Southern African Transport Conference 7 - 11 July 2008 "Partnership for research and progress in transportation", CSIR International Convention Centre, Pretoria, South Africa. ABSTRACT:Pavement ...
Maina, J.W.; Denneman, E.; De Beer, M.(eng, 2008-07)
Paper presented at the 27th Annual Southern African Transport Conference 7 - 11 July 2008 "Partnership for research and progress in transportation", CSIR International Convention Centre, Pretoria, South Africa.