Konrad Jamrozik
ABSTRACT
Dynamic symbolic execution (DSE) can efficiently explore all simple paths through a program, reliably determining whether there are any program crashes or violations of assertions or code contracts. However, if such automated oracles do not exist, the traditional approach is to present the developer a small and representative set of tests in order to let him/her determine their correctness. Customer feedback on Microsoft's Pex tool revealed that users expect different values and also more values than those produced by Pex, which threatens the applicability of DSE in a scenario without automated oracles. Indeed, even though all paths might be covered by DSE, the resulting tests are usually not sensitive enough to make a good regression test suite. In this paper, we present augmented dynamic symbolic execution, which aims to produce representative test sets by augmenting path conditions with additional conditions that enforce target criteria such as boundary or mutation adequacy, or logical coverage criteria.
- J. H. Andrews, L. C. Briand, and Y. Labiche. Is mutation an appropriate tool for testing experiments? In ICSE ’05: Proceedings of the 27th International Conference on Software Engineering, pages 402–411, New York, NY, USA, 2005. ACM. Google Scholar
Digital Library
- N. Bhattacharya, A. Sakti, G. Antoniol, Y.-G. Guéhéneuc, and G. Pesant. Divide-by-zero exception raising via branch coverage. In Proceedings of the Third international conference on Search based software engineering, SSBSE’11, pages 204–218, Berlin, Heidelberg, 2011. Springer-Verlag. Google ScholarDigital Library
- C. Cadar, P. Godefroid, S. Khurshid, C. S. Păsăreanu, K. Sen, N. Tillmann, and W. Visser. Symbolic execution for software testing in practice: preliminary assessment. In Proceedings of the 33rd International Conference on Software Engineering, ICSE ’11, pages 1066–1071, New York, NY, USA, 2011. ACM. Google ScholarDigital Library
- J. J. Chilenski and S. P. Miller. Applicability of modified condition/decision coverage to software testing. Software Engineering Journal, pages 193–200, September 1994.Google ScholarCross Ref
- R. A. DeMillo, R. J. Lipton, and F. Sayward. Hints on test data selection: Help for the practicing programmer. Computer, 11(4):34–41, 1978. Google ScholarDigital Library
- P. Godefroid, M. Y. Levin, and D. A. Molnar. Active property checking. In Proceedings of the 8th ACM international conference on Embedded software, EMSOFT ’08, pages 207–216. ACM, 2008. Google ScholarDigital Library
- P. Godefroid, M. Y. Levin, and D. A. Molnar. Sage: Whitebox fuzzing for security testing. ACM Queue, 10(1):20, 2012. Google ScholarDigital Library
- P. McMinn. Search-based software test data generation: A survey. Software Testing, Verification and Reliability, 14(2):105–156, 2004. Google ScholarDigital Library
- R. Pandita, T. Xie, N. Tillmann, and J. de Halleux. Guided test generation for coverage criteria. In Proceedings of the IEEE International Conference on Software Maintenance, ICSM ’10, pages 1–10, Washington, DC, USA, 2010. IEEE Computer Society. Google ScholarDigital Library
- D. Romano, M. Di Penta, and G. Antoniol. An approach for search based testing of null pointer exceptions. In Proceedings of the 2011 Fourth IEEE International Conference on Software Testing, Verification and Validation, ICST ’11, pages 160–169, Washington, DC, USA, 2011. IEEE Computer Society. Google ScholarDigital Library
- RTCA Inc. DO-178b: Software Considerations in Airborne Systems and Equipment Certification. Requirements and Technical Concepts for Aviation, Washington, DC, December 1992.Google Scholar
- N. Tillmann and N. J. de Halleux. Pex — white box test generation for .NET. In International Conference on Tests And Proofs (TAP), pages 134–253, 2008. Google ScholarDigital Library
- L. J. White and E. I. Cohen. A domain strategy for computer program testing. IEEE Trans. Softw. Eng., 6:247–257, May 1980. Google ScholarDigital Library
- L. Zhang, T. Xie, L. Zhang, N. Tillmann, J. de Halleux, and H. Mei. Test generation via dynamic symbolic execution for mutation testing. In Proceedings of the IEEE International Conference on Software Maintenance, ICSM ’10, pages 1–10, Washington, DC, USA, 2010. IEEE Computer Society. Google ScholarDigital Library
Index Terms
- Augmented dynamic symbolic execution
Recommendations
Automatic Mutation Test Case Generation via Dynamic Symbolic Execution
ISSRE '10: Proceedings of the 2010 IEEE 21st International Symposium on Software Reliability EngineeringThe automatic test case generation is the principal issue of the software testing activity. Dynamic symbolic execution appears to be a promising approach to this matter as it has been shown to be quite powerful in producing the sought tests. Despite its ...
Extending a search-based test generator with adaptive dynamic symbolic execution
ISSTA 2014: Proceedings of the 2014 International Symposium on Software Testing and AnalysisAutomatic unit test generation aims to support developers by alleviating the burden of test writing. Different techniques have been proposed over the years, each with distinct limitations. To overcome these limitations, we present an extension to the ...
Experience report: how is dynamic symbolic execution different from manual testing? a study on KLEE
ISSTA 2015: Proceedings of the 2015 International Symposium on Software Testing and AnalysisSoftware testing has been the major approach to software quality assurance for decades, but it typically involves intensive manual efforts. To reduce manual efforts, researchers have proposed numerous approaches to automate test-case generation, which ...
Comments