Part of the book series:Lecture Notes in Computer Science ((LNPSE,volume 9681))
Included in the following conference series:
1350Accesses
9Citations
Abstract
Code reviews are a provenly effective technique to find defects in source code as well as to increase its quality. Industrial software production often relies on code reviews as a standard QA mechanism. Surprisingly, though, tool support for reviewing activities is rare. Existing systems help to keep track of the discussion during the review, but do not support the reviewing activity directly. In this paper we argue that such support can be provided by formal analysis tools. Specifically, we use symbolic execution to improve the program understanding subtask during a code review. Tool support is realized by an Eclipse extension called Symbolic Execution Debugger. It allows one to explore visually a symbolic execution tree for the program under inspection. For evaluation we carefully designed a controlled experiment. We provide statistical evidence that with the help of symbolic execution defects are identified in a more effective manner than with a merely code-based view. Our work suggests that there is huge potential for formal methods not only in the production of safety-critical systems, but for any kind of software and as part of a standard development process.
This is a preview of subscription content,log in via an institution to check access.
Access this chapter
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
- Chapter
- JPY 3498
- Price includes VAT (Japan)
- eBook
- JPY 9151
- Price includes VAT (Japan)
- Softcover Book
- JPY 11439
- Price includes VAT (Japan)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
- 3.
- 4.
- 5.
The times measured for three of the participants were invalid and, therefore, excluded.
- 6.
Detailed results are available athttp://www.key-project.org/eclipse/SED/ReviewingCodeEvaluation/results.
References
Fagan, M.E.: Design and code inspections to reduce errors in program development. IBM Syst. J.15(3), 182–211 (1976)
Fagan, M.E.: Advances in software inspections. IEEE Trans. Softw. Eng.12(7), 744–751 (1986)
Humphrey, W.S.: A Discipline for Software Engineering. Addison-Wesley Longman Publishing Co., Inc, Boston (1995)
Humphrey, W.S.: Introduction to the Personal Software Process. Addison-Wesley Longman Publishing Co., Inc, Boston (1997)
Boyer, R.S., Elspas, B., Levitt, K.N.: SELECT–a formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Not.10(6), 234–245 (1975)
Burstall, R.M.: Program proving as hand simulation with a little induction. In: Information Processing 1974. Elsevier/North-Holland (1974)
Katz, S., Manna, Z.: Towards automatic debugging of programs. In: Proceedings of the International Conference on Reliable Software, pp. 143–155. ACM Press, Los Angeles (1975)
King, J.C.: Symbolic execution and program testing. Commun. ACM19(7), 385–394 (1976)
Wohlin, C., Runeson, P., Höst, M., Ohlsson, M.C., Regnell, B.: Experimentation in Software Engineering. Springer, Heidelberg (2012)
Hentschel, M., Bubel, R., Hähnle, R.: Symbolic execution debugger (SED). In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 255–262. Springer, Heidelberg (2014)
Beckert, B., Hähnle, R., Schmitt, P.H.: Verification of Object-Oriented Software: The KeY Approach. LNCS, vol. 4334. Springer, Heidelberg (2007)
Hentschel, M., Hähnle, R., Bubel, R.: Visualizing unbounded symbolic execution. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 82–98. Springer, Heidelberg (2014)
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. Draft Revision 2344, 31, May 2013
Doolan, E.P.: Experience with Fagan’s inspection method. Softw. Pract. Exper.22(2), 173–182 (1992)
Russell, G.W.: Experience with inspection in ultralarge-scale development. IEEE Softw.8(1), 25–31 (1991)
Macdonald, F., Miller, J.: A comparison of computer support systems for software inspection. Autom. Softw. Eng.6(3), 291–313 (1999)
Miller, J., Macdonald, F., Ferguson, J.: Assisting management decisions in the software inspection process. Inf. Technol. Manag.3(1–2), 67–83 (2002)
Nick, M., Denger, C., Willrich, T.: Experience-based support for code inspections. In: Althoff, K.-D., Dengel, A.R., Bergmann, R., Nick, M., Roth-Berghofer, T.R. (eds.) WM 2005. LNCS (LNAI), vol. 3782, pp. 121–126. Springer, Heidelberg (2005)
McConnell, S.: Code Complete, 2nd edn. Microsoft Press, Redmond (2004)
Zeller, A.: Why Programs Fail–A Guide to Systematic Debugging, 2nd edn. Elsevier, San Francisco (2006)
Bloch, J.: Effective Java, 2nd edn. Prentice Hall, Upper Saddle River (2008)
Frigge, M., Hoaglin, D.C., Iglewicz, B.: Some implementations of the boxplot. Am. Stat.43(1), 50–54 (1989)
Acknowledgment
We thank all participants of the evaluation for their valuable time and feedback.
Author information
Authors and Affiliations
Department of Computer Science, TU Darmstadt, Darmstadt, Germany
Martin Hentschel, Reiner Hähnle & Richard Bubel
- Martin Hentschel
Search author on:PubMed Google Scholar
- Reiner Hähnle
Search author on:PubMed Google Scholar
- Richard Bubel
Search author on:PubMed Google Scholar
Corresponding author
Correspondence toReiner Hähnle.
Editor information
Editors and Affiliations
RWTH Aachen University, Aachen, Germany
Erika Ábrahám
University of Twente, Enschede, Overijssel, The Netherlands
Marieke Huisman
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Hentschel, M., Hähnle, R., Bubel, R. (2016). Can Formal Methods Improve the Efficiency of Code Reviews?. In: Ábrahám, E., Huisman, M. (eds) Integrated Formal Methods. IFM 2016. Lecture Notes in Computer Science(), vol 9681. Springer, Cham. https://doi.org/10.1007/978-3-319-33693-0_1
Download citation
Published:
Publisher Name:Springer, Cham
Print ISBN:978-3-319-33692-3
Online ISBN:978-3-319-33693-0
eBook Packages:Computer ScienceComputer Science (R0)
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative