Abstract
Finding semantic bugs in code is difficult and requires precious expert time. Lacking comprehensive formal specifications, deductive verification is not an option. We propose an incremental specification procedure: With the help of automatic verification tools, a domain expert is guided through program runs and source code locations. The expert validates a run at certain locations and creates lightweight annotations. Formal methods training is not required. We demonstrate by example that this approach is capable to quickly detect different kinds of semantic bugs. We position our approach in the middle ground between fully-fledged deductive verification and bug finding without semantic guidance.
Supported by Deutsche Forschungsgemeinschaft (DFG) - Project number 351097374.
Chapter PDF
Similar content being viewed by others
References
Ayewah, N., Hovemeyer, D., Morgenthaler, J.D., Penix, J., Pugh, W.: Using static analysis to find bugs. IEEE Software 25(5), 22–29 (2008). https://doi.org/10.1109/MS.2008.130
Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification – specification is the new bottleneck. In: Cassez, F., Huuck, R., Klein, G., Schlich, B. (eds.) Proc. 7th Conf. on Systems Software Verification. EPTCS, vol. 102, pp. 18–32 (2012). https://doi.org/10.4204/EPTCS.102.4
Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification, 23rd Intl. Conf., Snowbird, UT, USA. LNCS, vol. 6806, pp. 184–190. Springer (2011). https://doi.org/10.1007/978-3-642-22110-1_16
Christakis, M., Müller, P., Wüstholz, V.: Collaborative verification and testing with explicit assumptions. In: Giannakopoulou, D., Méry, D. (eds.) Formal Methods, 18th Intl. Symp., Paris, France. LNCS, vol. 7436, pp. 132–146. Springer (2012). https://doi.org/10.1007/978-3-642-32759-9_13
Christakis, M., Müller, P., Wüstholz, V.: Guiding dynamic symbolic execution toward unverified program executions. In: Dillon, L.K., Visser, W., Williams, L.A. (eds.) Proc. 38th Intl. Conf. on Software Engineering, Austin, TX, USA. pp. 144–155. ACM (2016). https://doi.org/10.1145/2884781.2884843
Fagan, M.E.: Design and code inspections to reduce errors in program development. IBM Systems Journal 15(3), 182–211 (1976). https://doi.org/10.1147/sj.153.0182
Godefroid, P.: Test generation using symbolic execution. In: D’Souza, D., Kavitha, T., Radhakrishnan, J. (eds.) IARCS Ann. Conf. on Foundations of Software Technology and Theoretical Computer Science, Hyderabad, India. LIPIcs, vol. 18, pp. 24–33. Dagstuhl (2012). https://doi.org/10.4230/LIPIcs.FSTTCS.2012.24
Grätz, L., Hähnle, R., Bubel, R.: Examples for FASE NIER paper “finding semantics bugs fast” (artifact). In: 25th Intl. Conf. on Fundamental Approaches to Software Engineering, Munich, Germany. Zenodo (2022). https://doi.org/10.5281/zenodo.5806351
Hähnle, R., Huisman, M.: Deductive verification: from pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science: State of the Art and Perspectives, LNCS, vol. 10000, pp. 345–373. Springer (2019). https://doi.org/10.1007/978-3-319-91908-9_18
Hentschel, M., Hähnle, R., Bubel, R.: Can formal methods improve the efficiency of code reviews? In: Ábrahám, E., Huisman, M. (eds.) Integrated Formal Methods, 12th Intl. Conf., Reykjavik, Iceland. LNCS, vol. 9681, pp. 3–19. Springer (2016). https://doi.org/10.1007/978-3-319-33693-0_1
The Independent Breast Screening Review 2018, House of Commons, HC, vol. 1799. UK Department of Health and Social Care (Dec 2018), https://www.gov.uk/government/publications/independent-breast-screening-review-report
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P., Zimmerman, D.M., Dietl, W.: JML reference manual (2013), revision: 2344.
Meyer, B.: Applying “design by contract”. Computer 25(10), 40–51 (1992). https://doi.org/10.1109/2.161279
Stucki, L.G., Foshee, G.L.: New assertion concepts for self-metric software validation. In: Proc. Intl. Conf. on Reliable Software, Los Angeles, California, USA. p. 59–71. Association for Computing Machinery (1975). https://doi.org/10.1145/800027.808425
Tan, L., Liu, C., Li, Z., Wang, X., Zhou, Y., Zhai, C.: Bug characteristics in open source software. Empirical Software Engineering 19(6), 1665–1705 (2014). https://doi.org/10.1007/s10664-013-9258-8
Wang, Q., Brun, Y., Orso, A.: Behavioral execution comparison: Are tests representative of field behavior? In: Intl. Conf. on Software Testing, Verification and Validation, Tokyo, Japan. pp. 321–332. IEEE Computer Society (2017). https://doi.org/10.1109/ICST.2017.36
Wang, Q., Orso, A.: Improving testing by mimicking user behavior. In: Intl. Conf. on Software Maintenance and Evolution, Adelaide, Australia. pp. 488–498. IEEE (2020). https://doi.org/10.1109/ICSME46990.2020.00053
Zeller, A.: Why Programs Fail: A Guide to Systematic Debugging. Elsevier, second edn. (2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Grätz, L., Hähnle, R., Bubel, R. (2022). Finding Semantic Bugs Fast. In: Johnsen, E.B., Wimmer, M. (eds) Fundamental Approaches to Software Engineering. FASE 2022. Lecture Notes in Computer Science, vol 13241. Springer, Cham. https://doi.org/10.1007/978-3-030-99429-7_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-99429-7_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99428-0
Online ISBN: 978-3-030-99429-7
eBook Packages: Computer ScienceComputer Science (R0)