Advertisement

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

  • Nils TimmEmail author
  • Stefan Gruner
  • Prince Sibanda
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10522)

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.

References

  1. 1.
    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. In: Handbook of Satisfiability, pp. 457–481 (2009)Google Scholar
  2. 2.
    Biere, A., Heule, M., van Maaren, H., Walsh, T.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, pp. 131–153 (2009)Google Scholar
  3. 3.
    Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005). doi: 10.1007/978-3-540-31980-1_40 CrossRefGoogle Scholar
  4. 4.
    Edelkamp, S., Lafuente, A.L., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 57–79. Springer, Heidelberg (2001). doi: 10.1007/3-540-45139-0_5 CrossRefGoogle Scholar
  5. 5.
    Edelkamp, S., Schuppan, V., Bošnački, D., Wijs, A., Fehnker, A., Aljazzar, H.: Survey on directed model checking. In: Peled, D.A., Wooldridge, M.J. (eds.) MoChArt 2008. LNCS (LNAI), vol. 5348, pp. 65–89. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-00431-5_5 CrossRefGoogle Scholar
  6. 6.
    le Berre, D., Parrain, A.: The Sat4J library, release 2.2. J. Satisfiability Boolean Modeling Comput. 7, 59–64 (2010)Google Scholar
  7. 7.
    Reffe, F., Edelkamp, S.: Error detection with directed symbolic model checking. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 195–211. Springer, Heidelberg (1999). doi: 10.1007/3-540-48119-2_13 Google Scholar
  8. 8.
    Shtrichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 480–494. Springer, Heidelberg (2000). doi: 10.1007/10722167_36 CrossRefGoogle Scholar
  9. 9.
    Wang, C., Jin, H., Hachtel, G.D., Somenzi, F.: Refining the SAT decision ordering for bounded model checking. In: DAC, pp. 535–538. ACM (2004)Google Scholar
  10. 10.
    Demsky, B., Lam, P.: SATCheck: SAT-directed stateless model checking for SC and TSO. In: ACM SIGPLAN Notices, pp. 20–36. ACM (2015)Google Scholar
  11. 11.
    Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI, pp. 399–404 (2009)Google Scholar
  12. 12.
    Andisha, A.S., Wehrle, M., Westphal, B.: Directed model checking for PROMELA with relaxation-based distance functions. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 153–159. Springer, Cham (2015). doi: 10.1007/978-3-319-23404-5_11 CrossRefGoogle Scholar
  13. 13.
    Maeoka, J., Tanabe, Y., Ishikawa, F.: Depth-first heuristic search for software model checking. In: Lee, R. (ed.) Computer and Information Science 2015. SCI, vol. 614, pp. 75–96. Springer, Cham (2016). doi: 10.1007/978-3-319-23467-0_6 CrossRefGoogle Scholar
  14. 14.
    Schrieb, J., Wehrheim, H., Wonisch, D.: Three-valued spotlight abstractions. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 106–122. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-05089-3_8 CrossRefGoogle Scholar
  15. 15.
    Tseytin, G.S.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, pp. 115–125. Steklov Mathematical Institute (1970)Google Scholar
  16. 16.
    Gelder, A.: Improved conflict-clause minimization leads to improved propositional proof traces. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 141–146. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-02777-2_15 CrossRefGoogle Scholar
  17. 17.
    Zhang, H., Stickel, M.: An efficient algorithm for unit-propagation. In: 4th International Symposium on Artificial Intelligence and Mathematics, pp. 166–169 (1996)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2017

Authors and Affiliations

  1. 1.Department of Computer ScienceUniversity of PretoriaPretoriaSouth Africa

Personalised recommendations