Milos Gligoric
Viktor Kuncak
ABSTRACT
We present an approach for describing tests using non-deterministic test generation programs. To write such programs, we introduce UDITA, a Java-based language with non-deterministic choice operators and an interface for generating linked structures. We also describe new algorithms that generate concrete tests by efficiently exploring the space of all executions of non-deterministic UDITA programs.
We implemented our approach and incorporated it into the official, publicly available repository of Java PathFinder (JPF), a popular tool for verifying Java programs. We evaluate our technique by generating tests for data structures, refactoring engines, and JPF itself. Our experiments show that test generation using UDITA is faster and leads to test descriptions that are easier to write than in previous frameworks. Moreover, the novel execution mechanism of UDITA is essential for making test generation feasible. Using UDITA, we have discovered a number of bugs in Eclipse, NetBeans, Sun javac, and JPF.
- UDITA website. http://mir.cs.illinois.edu/udita.Google Scholar
- K. Apt and M. G. Wallace. Constraint Logic Programming using Eclipse. CUP, 2006. Google ScholarDigital Library
- T. Ball, D. Hoffman, F. Ruskey, R. Webber, and L. J. White. State generation and automated class testing. STVR, 2000.Google ScholarCross Ref
- N. E. Beckman, A. V. Nori, S. K. Rajamani, and R. J. Simmons. Proofs from tests. In ISSTA, 2008. Google ScholarDigital Library
- C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated testing based on Java predicates. In ISSTA, 2002. Google ScholarDigital Library
- C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: Automatically generating inputs of death. In CCS, 2006. Google ScholarDigital Library
- K. Claessen and J. Hughes. QuickCheck: A lightweight tool for random testing of Haskell programs. In ICFP, 2000. Google ScholarDigital Library
- L. Clarke and D. Richardson. Symbolic evaluation methods for program analysis. In Program Flow Analysis: Theory and Applications, chapter 9. Prentice-Hall, Inc., 1981.Google Scholar
- C. Csallner, N. Tillmann, and Y. Smaragdakis. DySy: Dynamic symbolic execution for invariant inference. In ICSE, 2008. Google ScholarDigital Library
- M. d'Amorim, C. Pacheco, T. Xie, D. Marinov, and M. D. Ernst. An empirical comparison of automated generation and classification techniques for object-oriented unit testing. In ASE, 2006. Google ScholarDigital Library
- B. Daniel, D. Dig, K. Garcia, and D. Marinov. Automated testing of refactoring engines. In ESEC/FSE, 2007. Google ScholarDigital Library
- L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, 2008. Google ScholarDigital Library
- X. Deng, J. Lee, and Robby. Bogor/Kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. In ASE, 2006. Google ScholarDigital Library
- B. Elkarablieh, D. Marinov, and S. Khurshid. Efficient solving of structural constraints. In ISSTA, 2008. Google ScholarDigital Library
- S. Fischer, O. Kiselyov, and C. Shan. Purely functional lazy non-deterministic programming. In ICFP, 2009. Google ScholarDigital Library
- C. Flanagan. Automatic software model checking via constraint logic. J-SCP, 50(1--3), 2004. Google ScholarDigital Library
- M. Gligoric, T. Gvero, V. Jagannath, S. Khurshid, V. Kuncak, and D. Marinov. On test generation through programming in UDITA. Tech. report LARA-REPORT-2009-005, EPFL, 2009.Google Scholar
- M. Gligoric, T. Gvero, S. Lauterburg, D. Marinov, and S. Khurshid. Optimizing generation of object graphs in Java PathFinder. In ICST, 2009. Google ScholarDigital Library
- P. Godefroid, A. Kiezun, and M. Y. Levin. Grammar-based whitebox fuzzing. In PLDI, 2008. Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated random testing. In PLDI, 2005. Google ScholarDigital Library
- W. Grieskamp, X. Qu, X. Wei, N. Kicillof, and M. B. Cohen. Interaction coverage meets path coverage by SMT constraint solving. In TestCom/FATES, 2009. Google ScholarDigital Library
- R. Iosif. Symmetry reduction criteria for software model checking. In SPIN, 2002. Google ScholarDigital Library
- V. Jagannath, Y. Y. Lee, B. Daniel, and D. Marinov. Reducing the costs of bounded-exhaustive testing. In FASE, 2009. Google ScholarDigital Library
- S. Khurshid and D. Marinov. TestEra: Specification-based testing of Java programs using SAT. J-ASE, 11(4), 2004. Google ScholarDigital Library
- S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In TACAS, 2003. Google ScholarDigital Library
- J. C. King. Symbolic execution and program testing. Commun. ACM, 19(7), 1976. Google ScholarDigital Library
- R. Lämmel and W. Schulte. Controllable combinatorial coverage in grammar-based testing. In TestCom, 2006.Google ScholarDigital Library
- D. Marinov. Automatic Testing of Software with Structurally Complex Inputs. PhD thesis, MIT, 2005. Google ScholarDigital Library
- D. Marinov, A. Andoni, D. Daniliuc, S. Khurshid, and M. Rinard. An evaluation of exhaustive testing for data structures. Technical Report MIT-LCS-TR-921, 2003.Google Scholar
- W. M. McKeeman. Differential testing for software. J-DTJ, 10(1), 1998.Google Scholar
- T. Noll and B. Schlich. Delayed nondeterminism in model checking embedded systems assembly code. In HVC, 2007. Google ScholarDigital Library
- W. F. Opdyke and R. E. Johnson. Refactoring: an aid in designing application frameworks and evolving object-oriented systems. In SOOPPA, 1990.Google Scholar
- C. Pasareanu, R. Pelánek, and W. Visser. Predicate abstraction with under-approximation refinement. J-LMCS, 3(1), 2007.Google Scholar
- C. S. Pasareanu, P. C. Mehlitz, D. H. Bushnell, K. Gundy-Burlet, M. R. Lowry, S. Person, and M. Pape. Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In ISSTA, 2008.Google ScholarDigital Library
- K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In ESEC/FSE, 2005. Google ScholarDigital Library
- K. Sullivan, J. Yang, D. Coppit, S. Khurshid, and D. Jackson. Software assurance by bounded exhaustive testing. In ISSTA, 2004. Google ScholarDigital Library
- S. Thummalapenta, T. Xie, N. Tillmann, J. de Halleux, and W. Schulte. MSeqGen: Object-oriented unit-test generation via mining source code. In ESEC/FSE, 2009. Google ScholarDigital Library
- N. Tillmann and J. de Halleux. Pex---White box test generation for .NET. In TAP, 2008. Google ScholarDigital Library
- F. Tip. Refactoring using type constraints. In SAS, 2007. Google ScholarDigital Library
- W. Visser, K. Havelund, G. P. Brat, S. Park, and F. Lerda. Model checking programs. J-ASE, 10(2), 2003. Google ScholarDigital Library
- W. Visser, C. S. Pasareanu, and S. Khurshid. Test input generation with Java PathFinder. In ISSTA, 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 ISSTA, 2006. Google ScholarDigital Library
Recommendations
EvoSuite: automatic test suite generation for object-oriented software
ESEC/FSE '11: Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineeringTo find defects in software, one needs test cases that execute the software systematically, and oracles that assess the correctness of the observed behavior when running these test cases. This paper presents EvoSuite, a tool that automatically generates ...
JQF: coverage-guided property-based testing in Java
ISSTA 2019: Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and AnalysisWe present JQF, a platform for performing coverage-guided fuzz testing in Java. JQF is designed both for practitioners, who wish to find bugs in Java programs, as well as for researchers, who wish to implement new fuzzing algorithms.
Practitioners ...
A Survey of Compiler Testing
Virtually any software running on a computer has been processed by a compiler or a compiler-like tool. Because compilers are such a crucial piece of infrastructure for building software, their correctness is of paramount importance. To validate and ...
Comments