Abstract
The correctness of parallel and reactive programs is often easier specified using formulae of temporal logics. Yet verifying that a system satisfies such specifications is more difficult than verifying safety properties: the recurrence of a specific program state has to be detected. This paper reports on the development of a generic framework for automatic verification of linear temporal logic specifications for programs in LLVM bitcode. Our method searches explicitly through all possible interleavings of parallel threads (control non-determinism) but represents symbolically the variable evaluations (data non-determinism), guided by the specification in order to prove the correctness. To evaluate the framework we compare our method with state-of-the-art tools on a set of unmodified C programs.
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
Preview
Unable to display preview. Download preview PDF.
References
Alglave, J., Donaldson, A.F., Kroening, D., Tautschnig, M.: Making software verification tools really work. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 28–42. Springer, Heidelberg (2011)
Barnat, J., Bauch, P., Havel, V.: Model checking parallel programs with inputs. In: Proc. of PDP, pp. 756–759 (2014)
Barnat, J., Bauch, P., Havel, V.: Temporal verification of simulink diagrams. In: Proc. of HASE, pp. 81–88 (2014)
Barnat, J., Brim, L., Havel, V., Havlíček, J., Kriho, J., Lenčo, M., Ročkai, P., Štill, V., Weiser, J.: Divine 3.0 – Explicit-state Model-checker for Multithreaded C/C++ Programs. In: CAV, pp. 863–868 (2013)
Barnat, J., Brim, L., Ročkai, P.: Towards LTL model checking of unmodified thread-based c&c++programs. In: NFM, pp. 252–266 (2012)
Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011)
Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. In: Proc. of FMICS, pp. 160–177 (2002)
Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011)
Bradley, A., Somenzi, F., Hassan, Z., Yan, Z.: An incremental approach to model checking progress properties. In: Proc. of FMCAD, pp. 144–153 (2011)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Verifying LTL properties of hybrid systems with K-liveness. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 424–440. Springer, Heidelberg (2014)
Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.: proving that programs eventually do something good. In: Proc. of POPL, pp. 265–276 (2007)
Cook, B., Koskinen, E.: Making prophecies with decision predicates. In: Proc. of POPL, pp. 399–410 (2011)
Duret-Lutz, A.: LTL Translation Improvements in SPOT 1.0. IJCCBS 5(1), 31–54 (2014)
Havel, V.: Generic Platform for Explicit-Symbolic Verification. Master’s thesis, Masaryk University (2014)
Holzmann, G.: The Model Checker SPIN. IEEE T. Software Eng. 23(5), 279–295 (1997)
Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis transformation. In: Proc. of CGO, pp. 75–86 (2004)
Manna, Z., Pnueli, A.: Verification of Concurrent Programs, Part I: The Temporal Framework. Stanford University, Technical report (1981)
McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)
Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: Proc. of POPL, pp. 132–144 (2005)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Bauch, P., Havel, V., Barnat, J. (2014). LTL Model Checking of LLVM Bitcode with Symbolic Data. In: Hliněný, P., et al. Mathematical and Engineering Methods in Computer Science. MEMICS 2014. Lecture Notes in Computer Science(), vol 8934. Springer, Cham. https://doi.org/10.1007/978-3-319-14896-0_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-14896-0_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-14895-3
Online ISBN: 978-3-319-14896-0
eBook Packages: Computer ScienceComputer Science (R0)