Abstract
Unit test generation tools typically aim at one of two objectives: to explore the program behavior in order to exercise automated oracles, or to produce a representative test set that can be used to manually add oracles or to use as a regression test set. Dynamic symbolic execution (DSE) can efficiently explore all simple paths through a program, exercising automated oracles such as assertions or code contracts. However, its original intention was not to produce representative test sets. Although DSE tools like Pex can retain subsets of the tests seen during the exploration, customer feedback revealed that users expect different values than those produced by Pex, and sometimes also more than one value for a given condition or program path. This 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 with DSE by augmenting path conditions with additional conditions that enforce target criteria such as boundary or mutation adequacy, or logical coverage criteria. Experiments with our Apex prototype demonstrate that the resulting test cases can detect up to 30% more seeded defects than those produced with Pex.
A preliminary version of this paper was published as a short paper discussing the idea for mutation and boundary analysis without evaluation in [15].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ammann, P., Offutt, J.: Introduction to Software Testing, 1st edn. Cambridge University Press (2008)
Anand, S., Păsăreanu, C.S., Visser, W.: JPF-SE: a symbolic execution extension to Java PathFinder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 134–138. Springer, Heidelberg (2007)
Andrews, J.H., Briand, L.C., Labiche, Y.: Is mutation an appropriate tool for testing experiments? In: Proc. ICSE 2005, pp. 402–411. ACM (2005)
Bhattacharya, N., Sakti, A., Antoniol, G., Guéhéneuc, Y.-G., Pesant, G.: Divide-by-zero exception raising via branch coverage. In: Cohen, M.B., Ó Cinnéide, M. (eds.) SSBSE 2011. LNCS, vol. 6956, pp. 204–218. Springer, Heidelberg (2011)
Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82–90 (2013)
Chilenski, J.J., Miller, S.P.: Applicability of modified condition/decision coverage to software testing. Software Engineering Journal, 193–200 (1994)
DeMillo, R.A., Lipton, R.J., Sayward, F.: Hints on test data selection: Help for the practicing programmer. Computer 11(4), 34–41 (1978)
Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: a survey. Softw. Test. Verif. Reliab. 19, 215–261 (2009)
Ghani, K., Clark, J.A.: Strengthening inferred specifications using search based testing. In: Proc. SBST, pp. 187–194. IEEE Computer Society Press (2008)
Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. In: Proc. PLDI, pp. 213–223 (2005)
Godefroid, P., Levin, M.Y., Molnar, D.A.: Active property checking. In: Proc. EMSOFT 2008, pp. 207–216. ACM (2008)
Godefroid, P., Levin, M.Y., Molnar, D.A.: Sage: Whitebox fuzzing for security testing. ACM Queue 10(1), 20 (2012)
Godefroid, P., Luchaup, D.: Automatic partial loop summarization in dynamic test generation. In: Proc. ISSTA 2011, pp. 23–33. ACM (2011)
Howden, W.E.: Weak mutation testing and completeness of test sets. IEEE TSE 8(4), 371–379 (1982)
Jamrozik, K., Fraser, G., Tillmann, N., De Halleux, J.: Augmented dynamic symbolic execution. In: Proc. ASE 2012, pp. 254–257. ACM (2012)
Joebstl, E., Weiglhofer, M., Aichernig, B.K., Wotawa, F.: When bdds fail: Conformance testing with symbolic execution and smt solving. In: Proc. ICST 2010, pp. 479–488. IEEE Computer Society (2010)
Kosmatov, N., Legeard, B., Peureux, F., Utting, M.: Boundary coverage criteria for test generation from formal models. In: Proc. ISSRE, pp. 139–150. IEEE Computer Society (2004)
Pandita, R., Xie, T., Tillmann, N., de Halleux, J.: Guided test generation for coverage criteria. In: Proc. ICSM 2010, pp. 1–10. IEEE Computer Society (2010)
Romano, D., Di Penta, M., Antoniol, G.: An approach for search based testing of null pointer exceptions. In: Proc. ICST 2011, pp. 160–169. IEEE (2011)
Rothermel, G., Harrold, M.J., Ostrin, J., Hong, C.: An empirical study of the effects of minimization on the fault detection capabilities of test suites. In: Proc. ICSM 1998, pp. 34–43. IEEE Computer Society Press (1998)
Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proc. ESEC/FSE-13, pp. 263–272. ACM (2005)
Staats, M., Pǎsǎreanu, C.: Parallel symbolic execution for structural test generation. In: Proc. ISSTA 2010, pp. 183–194. ACM (2010)
Tillmann, N., de Halleux, J.: Pex–white box test generation for.NET. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 134–153. Springer, Heidelberg (2008)
Vilkomir, S.A., Bowen, J.P.: Reinforced condition/decision coverage (rc/dc): A new criterion for software testing. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 291–308. Springer, Heidelberg (2002)
White, L.J., Cohen, E.I.: A domain strategy for computer program testing. IEEE Trans. Softw. Eng. 6, 247–257 (1980)
Zhang, L., Xie, T., Zhang, L., Tillmann, N., de Halleux, J., Mei, H.: Test generation via dynamic symbolic execution for mutation testing. In: Proc. ICSM 2010, pp. 1–10. IEEE Computer Society (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jamrozik, K., Fraser, G., Tillman, N., de Halleux, J. (2013). Generating Test Suites with Augmented Dynamic Symbolic Execution. In: Veanes, M., Viganò, L. (eds) Tests and Proofs. TAP 2013. Lecture Notes in Computer Science, vol 7942. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38916-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-38916-0_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38915-3
Online ISBN: 978-3-642-38916-0
eBook Packages: Computer ScienceComputer Science (R0)