ABSTRACT
Software-defect detection is an increasingly important research topic in software engineering. To detect defects in a program, static verification and dynamic test generation are two important proposed techniques. However, both of these techniques face their respective issues. Static verification produces false positives, and on the other hand, dynamic test generation is often time consuming. To address the limitations of static verification and dynamic test generation, we present an automated defect-detection tool, called DyTa, that combines both static verification and dynamic test generation. DyTa consists of a static phase and a dynamic phase. The static phase detects potential defects with a static checker; the dynamic phase generates test inputs through dynamic symbolic execution to confirm these potential defects. DyTa reduces the number of false positives compared to static verification and performs more efficiently compared to dynamic test generation.
- C. Csallner and Y. Smaragdakis. Check 'n' Crash: Combining Static Checking and Testing. In Proc. ICSE, pages 422--431, 2005. Google ScholarDigital Library
- S. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay. Effective Typestate Verification in the Presence of Aliasing. In Proc. ISSTA, pages 133--144, 2006. Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. DART: Directed Automated Random Testing. In Proc. PLDI, pages 213--223, 2005. Google ScholarDigital Library
- hashing algorithms, 2010. http://hashlib.codeplex.com/.Google Scholar
- D. Hovemeyer and W. Pugh. Finding Bugs is Easy. In Proc. OOPSLA, pages 132--136, 2004. Google ScholarDigital Library
- F. Logozzo. Practical Verification for the Working Programmer with Code Contracts and Abstract Interpretation (Invited Talk). In Proc. VMCAI, 2011. Google ScholarDigital Library
- Microsoft Code Contracts, 2010. http://research.microsoft.com/en-us/projects/contracts/.Google Scholar
- K. Sen, D. Marinov, and G. Agha. CUTE: A Concolic Unit Testing Engine for C. In Proc. ESE/FSE, pages 263--272, 2005. Google ScholarDigital Library
- K. Taneja, T. Xie, N. Tillmann, J. de Halleux, and W. Schulte. Guided Path Exploration for Regression Test Generation. In Companion Proc. ICSE, NIER, pages 311--314, 2009.Google Scholar
- N. Tillmann and J. de Halleux. Pex: White Box Test Generation for. NET. In Proc. TAP, pages 134--153, 2008. Google ScholarDigital Library
Index Terms
- DyTa: dynamic symbolic execution guided with static verification results
Recommendations
Check 'n' crash: combining static checking and testing
ICSE '05: Proceedings of the 27th international conference on Software engineeringWe present an automatic error-detection approach that combines static checking and concrete test-case generation. Our approach consists of taking the abstract error conditions inferred using theorem proving techniques by a static checker (ESC/Java), ...
SoftWare IMmunization (SWIM) - A Combination of Static Analysis and Automatic Testing
COMPSAC '11: Proceedings of the 2011 IEEE 35th Annual Computer Software and Applications ConferenceStatic program analysis uses many checkers to discover a very large number of programming issues, but with a high false alarm rate. With the aid of dynamic automatic testing, the actual severe defects can be confirmed by failures of test cases. After ...
Dyta: An Intelligent System for Moving Target Detection
ICIAP '99: Proceedings of the 10th International Conference on Image Analysis and ProcessingIn this paper we present an intelligent system, Dyta (Dynamic Target Analysis), for moving target detection. Dyta consists of two levels of processes. At the first level it attempts to identify possible moving objects and compute the texture feature of ...
Comments