Suzette Person
Matthew B. Dwyer
ABSTRACT
Detecting and characterizing the effects of software changes is a fundamental component of software maintenance. Version differencing information can be used to perform version merging, infer change characteristics, produce program documentation, and guide program re-validation. Existing techniques for characterizing code changes, however, are imprecise leading to unnecessary maintenance efforts.
In this paper, we introduce a novel extension and application of symbolic execution techniques that computes a precise behavioral characterization of a program change. This technique, which we call differential symbolic execution (DSE), exploits the fact that program versions are largely similar to reduce cost and improve the quality of analysis results. We define the foundational concepts of DSE, describe cost-effective tool support for DSE, and illustrate its potential benefit through an exploratory study that considers version histories of two Java code bases.
- S. Anand, P. Godefroid, and N. Tillmann. Demand-driven compositional symbolic execution. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008. Google Scholar
Digital Library
- T. Apiwattanapong, A. Orso, and M. J. Harrold. Jdiff: A differencing technique and tool for object-oriented programs. Automated Software Engineering, 14(1):3--36, 2007. Google ScholarDigital Library
- T. Apiwattanapong, R. Santelices, P. K. Chittimalli, A. Orso, and M. J. Harrold. Matrix: Maintenance-oriented testing requirements identifier and examiner. In Proceedings of the Testing: Academic and Industrial Conference - Practice and Research Techniques, pages 137--146, 2006. Google ScholarDigital Library
- R. E. Bryant, S. German, and M. N. Velev. Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Transactions Computational Logic, 2(1):93--134, 2001. Google ScholarDigital Library
- Choco. Main-page Choco. http://choco-solver.net, 2008.Google Scholar
- D. Currie, X. Feng, M. Fujita, A. J. Hu, M. Kwan, and S. Rajan. Embedded software verification using symbolic execution and uninterpreted functions. International Journal of Parallel Programming, 34(1):61--91, 2006. Google ScholarDigital Library
- CVC3. CVC3 page. http://www.cs.nyu.edu/acsys/cvc3, 2008.Google Scholar
- B. Daniel, D. Dig, K. Garcia, and D. Marinov. Automated testing of refactoring engines. In Proceedings of the the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 185--194, 2007. Google ScholarDigital Library
- Diffutils. Comparing and merging files. http://www.gnu.org/software/diffutils, 2002.Google Scholar
- M. Fowler. Refactoring home page. http://refactoring.org, 2007.Google Scholar
- P. Godefroid. Compositional dynamic test generation. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages 47--54, 2007. Google ScholarDigital Library
- D. Jackson and D. A. Ladd. Semantic Diff: A tool for summarizing the effects of modifications. In Proceedings of the International Conference on Software Maintenance, pages 243--252, 1994. Google ScholarDigital Library
- JMeter. Jmeter-Apache JMeter. http://jakarta.apache.org/jmeter/, 2008. Google ScholarDigital Library
- J. C. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385--394, 1976. Google ScholarDigital Library
- D. Notkin. Longitudinal program analysis. In Proceedings of the ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2002. Google ScholarDigital Library
- C. S. Pǎsǎreanu, P. C. Mehlitz, D. H. Bushnell, K. Gundy-Burlet, M. Lowry, S. Person, and M. Pape. Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In Proceedings of the International Symposium on Software Testing and Analysis, pages 15--25, 2008. Google ScholarDigital Library
- S. Raghavan, R. Rohana, D. Leon, A. Podgurski, and V. Augustine. Dex: a semantic-graph differencing tool for studying changes in large code bases. In Proceedings of the International Software Maintenance Conference, pages 188--197, 2004. Google ScholarDigital Library
- V. P. Ranganath and J. Hatcliff. Slicing concurrent Java programs using Indus and Kaveri. Software Tools for Technology Transfer, 9(5--6):489--504, 2007.Google Scholar
- X. Ren, B. G. Ryder, M. Stoerzer, and F. Tip. Chianti: a change impact analysis tool for Java programs. In Proceedings of the 27th International Conference on Software Engineering, pages 664--665, 2005. Google ScholarDigital Library
- G. Rothermel and M. J. Harrold. A safe, efficient regression test selection technique. ACM Transactions on Software Engineering and Methodology, 6(2):173--210, 1997. Google ScholarDigital Library
- S. F. Siegel. MPIN-SPIN page. http://vsl.cis.udel.edu/mpi-spin/, 2008.Google Scholar
- S. F. Siegel, A. Mironova, G. S. Avrunin, and L. A. Clarke. Using model checking with symbolic execution to verify parallel numerical programs. In Proceedings of the 2006 International Symposium on Software Testing and Analysis, pages 157--168, 2006. Google ScholarDigital Library
- S. F. Siegel, S. E. Moelius, and L. F. Rossi. A case study in the use of model checking to verify parallel scientific software. Technical Report UDEL-CIS 2007/343, Department of Computer and Information Sciences, University of Delaware, Nov. 2007.Google Scholar
- S. F. Siegel and L. F. Rossi. Analyzing BlobFlow: A case study using model checking to verify parallel scientific software. In Recent Advances in Parallel Virtual Machine and Message Passing Interface, 15th European PVM/MPI User's Group Meeting, Proceedings, volume 5205 of LNCS. Springer, 2008. To appear. Google ScholarDigital Library
- Siena. Siena: A wide-area event notification service. http://serl.cs.colorado.edu/~serl/dot/siena.html, 2008.Google Scholar
- SIR. Software-artifact infrastructure repository: Home. http://sir.unl.edu, 2008.Google Scholar
- W. Visser, C. S. Pǎsǎreanu, and S. Khurshid. Test input generation with Java PathFinder. In Proceedings of the International Symposium on Software Testing and Analysis, pages 97--107, 2004. Google ScholarDigital Library
- W. Visser, C. S. Pǎsǎreanu?, and R. Pelánek. Test input generation for Java containers using state matching. In Proceedings of the International Symposium on Software Testing and Analysis, pages 37--48, 2006. Google ScholarDigital Library
- J. Winstead and D. Evans. Towards differential program analysis. In Proceedings of the ICSE Workshop on Dynamic Analysis, 2003. Google ScholarDigital Library
Index Terms
- Differential symbolic execution
Recommendations
Directed incremental symbolic execution
PLDI '11The last few years have seen a resurgence of interest in the use of symbolic execution -- a program analysis technique developed more than three decades ago to analyze program execution paths. Scaling symbolic execution and other path-sensitive analysis ...
Directed incremental symbolic execution
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and ImplementationThe last few years have seen a resurgence of interest in the use of symbolic execution -- a program analysis technique developed more than three decades ago to analyze program execution paths. Scaling symbolic execution and other path-sensitive analysis ...
Directed Incremental Symbolic Execution
The last few years have seen a resurgence of interest in the use of symbolic execution—a program analysis technique developed more than three decades ago to analyze program execution paths. Scaling symbolic execution to real systems remains challenging ...
Comments