Abstract
We present a technique for verifying concurrent software systems via SAT-based bounded model checking. It is based on a direct transfer of the system and an LTL property into a formula that encodes the corresponding model checking problem. In our approach we first employ three-valued abstraction. The state space of the resulting abstract system is then logically encoded, which saves us the expensive construction of an explicit state space model. The verification result can be obtained via two SAT checks. Our work includes the definition of the encoding and a theorem which states that the SAT result for an encoded verification task is equivalent to the result of the corresponding model checking problem. We also introduce an extension of the encoding by fairness constraints, which facilitates the verification of liveness properties. We have implemented our technique in an automatic verification tool that supports bounded LTL model checking under fairness.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Completeness thresholds for checking safety properties are linear in the size of the abstraction, i.e. in the number of abstract states [7].
References
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Handb. Satisf. 185, 457–481 (2009)
Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999). doi:10.1007/3-540-48683-6_25
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. Int. J. Softw. Tools Technol. Transf. 2(4), 410–425 (2000)
Fitting, M.: Kleene’s 3-valued logics and their children. Fund. Inf. 20(1–3), 113–131 (1994)
Grumberg, O.: 3-valued abstraction for (bounded) model checking. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, p. 21. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04761-9_2
Ivančić, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: software verification platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 301–306. Springer, Heidelberg (2005). doi:10.1007/11513988_31
Kroening, D., Ouaknine, J., Strichman, O., Wahl, T., Worrell, J.: Linear completeness thresholds for bounded model checking. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 557–572. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_44
Kroening, D., Tautschnig, M.: CBMC – C bounded model checker. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_26
Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. J. Satisf. Boolean Model. Comput. 7, 59–64 (2010)
Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 82–97. Springer, Heidelberg (2005). doi:10.1007/11513988_9
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
Shoham, S., Grumberg, O.: 3-valued abstraction: more precision at less cost. Inf. Comput. 206(11), 1313–1333 (2008)
Timm, N.: Bounded model checking für partielle systeme. Master’s thesis, University of Paderborn (2009)
Timm, N., Wehrheim, H.: On symmetries and spotlights – verifying parameterised systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 534–548. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16901-4_35
Timm, N., Wehrheim, H., Czech, M.: Heuristic-guided abstraction refinement for concurrent systems. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 348–363. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34281-3_25
Wehrheim, H.: Bounded model checking for partial Kripke structures. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 380–394. Springer, Heidelberg (2008). doi:10.1007/978-3-540-85762-4_26
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Timm, N., Gruner, S., Harvey, M. (2016). A Bounded Model Checker for Three-Valued Abstractions of Concurrent Software Systems. In: Ribeiro, L., Lecomte, T. (eds) Formal Methods: Foundations and Applications. SBMF 2016. Lecture Notes in Computer Science(), vol 10090. Springer, Cham. https://doi.org/10.1007/978-3-319-49815-7_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-49815-7_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-49814-0
Online ISBN: 978-3-319-49815-7
eBook Packages: Computer ScienceComputer Science (R0)