Abstract
The verification of real-world applications is a continuous challenge which yielded numerous different methods and approaches. However, scalability of precise analysis methods on large programs is still limited. We thus propose a formal definition of modules that allows a partitioning of the program into smaller code fragments suitable for verification by bounded model checking. We consider programs written in C/C++ and use LLVM as an intermediate representation. A formal trace semantics for LLVM program runs is defined that also takes modularization into account. Using different abstractions and a selection of fragments of a program for each module, we describe four different modularization approaches. We define desirable properties of modularizations, and show how a bounded model checking approach can be adapted for modularization. Two modularization approaches are implemented within the tool QPR-Verify, which is based on the bounded model checker LLBMC. We evaluate our approach on a medium-sized embedded system software encompassing approximately 160 KLoC.
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.
For brevity, we use getelptr instead of LLVM’s name getelementptr.
- 2.
For simplicity, we assume that integer and pointer variables have the same bit-width, and that all program variables are of type integer. We also identify pointer values with integers, such that \(Val = Adr\). A more refined model would differentiate between different data types stored in memory (including floating-point). In practice, a byte-oriented memory model is often used [17].
References
Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: static driver verification with under 4% false alarms. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, pp. 35–42. FMCAD Inc. (2010)
Balyo, T., Heule, M.J., Järvisalo, M. (eds.): Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions. University of Helsinki (2017)
Beckert, B., Hähnle, R., Schmitt, P.H.: Verification of Object-Oriented Software: The KeY Approach. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-69061-0
BMW CarIT GmbH: Open Source ConnMan (2019). http://www.bmw-carit.de/open-source/connman.php. Accessed 10 June 2019
Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: Fourth Annual Symposium on Logic in Computer Science, pp. 353–362 (1989)
Cobleigh, J.M., Giannakopoulou, D., PĂsĂreanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36577-X_24
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th Annual Symposium on Principles of Programming Languages, pp. 238–252 (1977)
Giannakopoulou, D., Pasareanu, C.S., Cobleigh, J.M.: Assume-guarantee verification of source code with design-level assumptions. In: Proceedings of 26th International Conference on Software Engineering, pp. 211–220. IEEE (2004)
Grumberg, O., Long, D.E.: Model checking and modular verification. In: Baeten, J.C.M., Groote, J.F. (eds.) CONCUR 1991. LNCS, vol. 527, pp. 250–265. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-54430-5_93
Hardekopf, B., Lin, C.: Flow-sensitive pointer analysis for millions of lines of code. In: Proceedings of the 9th Annual IEEE/ACM International Symposium on Code Generation and Optimization, pp. 289–298. IEEE Computer Society (2011)
Hawblitzel, C., et al.: Ironclad apps: end-to-end security via automated full-system verification. In: 11th Symposium on Operating Systems Design and Implementation, pp. 165–181 (2014)
Henzinger, T.A., Qadeer, S., Rajamani, S.K.: You assume, we guarantee: methodology and case studies. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 440–451. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028765
Intel Corporation: Connection Manager (2019). https://git.kernel.org/pub/scm/network/connman/connman.git/tag/?h=1.36. Accessed 10 June 2019
Kaiser, J.O., Dang, H.H., Dreyer, D., Lahav, O., Vafeiadis, V.: Strong logic for weak memory: reasoning about release-acquire consistency in Iris. In: 31st European Conference on Object-Oriented Programming (2017)
Koopman, P.: A case study of Toyota unintended acceleration and software safety. Carnegie Mellon University Presentation, September 2014
Le Lann, G.: An analysis of the Ariane 5 flight 501 failure-a system engineering perspective. In: Proceedings of International Conference and Workshop on Engineering of Computer-Based Systems, pp. 339–346 (1997)
Merz, F., Falke, S., Sinz, C.: LLBMC: bounded model checking of C and C++ programs using a compiler IR. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 146–161. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27705-4_12
Müller, P.: Modular Specification and Verification of Object-Oriented Programs. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45651-1
Müller, P.: The binomial heap verification challenge in Viper. In: Müller, P., Schaefer, I. (eds.) Principled Software Development, pp. 203–219. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98047-8_13
Westland, J.C.: The cost of errors in software development: evidence from industry. J. Syst. Softw. 62(1), 1–9 (2002)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Kleine Büning, M., Sinz, C. (2019). Automatic Modularization of Large Programs for Bounded Model Checking. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-030-32409-4_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-32408-7
Online ISBN: 978-3-030-32409-4
eBook Packages: Computer ScienceComputer Science (R0)