Abstract
In this paper we present a new approach to verification of multi-threaded C/C++ programs. Our solution effectively chains the parallel and distributed-memory model checker DiVinE with CLang and the LLVM bitcode interpreter. This combination offers full LTL, distributed-memory model checking of virtually unmodified C/C++ source code and is supported by a newly introduced path-reduction technique. We demonstrate the efficiency of the reduction and also the capacity to produce human-readable counter-examples in two small case studies: a C implementation of the Peterson’s mutual exclusion protocol and a C++ implementation of a shared-memory, lock-free FIFO data structure designed for fast inter-thread communication.
This work has been partially supported by the Czech Science Foundation grant No. GAP202/11/0312 and by ARTEMIS-IA iFEST project grant No. 100203.
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
Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: A Model Checker for Concurrent Software. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 484–487. Springer, Heidelberg (2004)
Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004)
Barnat, J., Brim, L., Češka, M., Ročkai, P.: DiVinE: Parallel Distributed Model Checker (Tool paper). In: Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi/PDMC), pp. 4–7. IEEE (2010)
Bingham, B., Bingham, J., de Paula, F.M., Erickson, J., Singh, G., Reitblatt, M.: Industrial Strength Distributed Explicit State Model Checking. In: Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi/PDMC), pp. 28–36. IEEE (2010)
Chaki, S., Clarke, E., Groce, A.: Modular verification of software components in C. IEEE Transactions on Software Engineering, 385–395 (2003)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Zheng, H.: Bandera: Extracting Finite-state Models from Java Source Code. In: International Conference on Software Engineering, p. 439 (2000)
Aan de Brugh, N.H.M., Nguyen, V.Y., Ruys, T.C.: MoonWalker: Verification of.NET Programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 170–173. Springer, Heidelberg (2009)
DeMartini, C., Iosif, R., Sisto, R.: A Deadlock Detection Tool for Concurrent Java Programs. Software Practice and Experience 29(7), 577–603 (1999)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software Verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Holzmann, G.J.: Logic Verification of ANSI-C Code with SPIN. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 131–147. Springer, Heidelberg (2000)
Holzmann, G.J.: The SPIN model checker: primer and reference manual, 1st edn. Addison-Wesley Professional (2003)
Holzmann, G.J., Smith, M.H.: Software Model Checking: Extracting Verification Models from Source Code. Software Testing, Verification and Reliability 11(2), 65–79 (2001)
Lattner, C., Adve, V.: LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In: International Symposium on Code Generation and Optimization (CGO), Palo Alto, California (March 2004)
Linden, A., Wolper, P.: An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 212–226. Springer, Heidelberg (2010)
Musuvathi, M.S., Park, D., Chou, A., Engler, D.R., Dill, D.L.: CMC: A Pragmatic Approach to Model Checking Real Code. In: The Fifth Symposium on Operating Systems Design and Implementation (2002)
Peled, D.: Ten Years of Partial Order Reduction. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 17–28. Springer, Heidelberg (1998)
Brat, G., Thompson, S., Schimpf, K.: The MCP Model Checker (2008), Submitted to PEPM 2008
Thompson, S., Brat, G.: Verification of C++ Flight Software with the MCP Model Checker. In: 2008 IEEE Aerospace Conference, pp. 1–9 (March 2008)
Thompson, S., Brat, G., Venet, A.: Software model checking of ARINC-653 flight code with MCP. In: Muñoz, C. (ed.) Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), NASA/CP-2010-216215, Langley Research Center, Hampton VA 23681-2199, USA, pp. 171–181. NASA (April 2010)
Visser, W., Havelund, K., Brat, G.P., Park, S.: Model Checking Programs. In: ASE, pp. 3–12 (2000)
Yorav, K., Grumberg, O.: Static Analysis for State-Space Reductions Preserving Temporal Logics. Formal Methods in System Design 25(1), 67–96 (2004)
Zaks, A., Joshi, R.: Verifying Multi-threaded C Programs with SPIN. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 325–342. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barnat, J., Brim, L., Ročkai, P. (2012). Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. In: Goodloe, A.E., Person, S. (eds) NASA Formal Methods. NFM 2012. Lecture Notes in Computer Science, vol 7226. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28891-3_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-28891-3_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28890-6
Online ISBN: 978-3-642-28891-3
eBook Packages: Computer ScienceComputer Science (R0)