Korat: Automated testing based on Java predicates This paper presents Korat, a novel framework for automated testing of Java programs. Given a formal specification for a method, Korat uses the method precondition to automatically generate all (nonisomorphic) test cases up to a given small size. Korat then executes the method on each test case, and uses the method postcondition as a test oracle to check the correctness of each output.To generate test cases for a method, Korat constructs a Java predicate (i.e., a method that returns a boolean) from the method’s pre-condition. The heart of Korat is a technique for automatic test case generation: given a predicate and a bound on the size of its inputs, Korat generates all (nonisomorphic) inputs for which the predicate returns true. Korat exhaustively explores the bounded input space of the predicate but does so efficiently by monitoring the predicate’s executions and pruning large portions of the search space.This paper illustrates the use of Korat for testing several data structures, including some from the Java Collections Framework. The experimental results show that it is feasible to generate test cases from Java predicates, even when the search space for inputs is very large. This paper also compares Korat with a testing framework based on declarative specifications. Contrary to our initial expectation, the experiments show that Korat generates test cases much faster than the declarative framework.

This software is also peer reviewed by journal TOMS.

References in zbMATH (referenced in 30 articles )

Showing results 1 to 20 of 30.
Sorted by year (citations)

1 2 next

  1. Brucker, Achim D.; Wolff, Burkhart: On theorem prover-based testing (2013)
  2. Bengolea, Valeria; Aguirre, Nazareno; Marinov, Darko; Frias, Marcelo F.: Using coverage criteria on repOK to reduce bounded-exhaustive test suites (2012)
  3. Nokhbeh Zaeem, Razieh; Gopinath, Divya; Khurshid, Sarfraz; McKinley, Kathryn S.: History-aware data structure repair using SAT (2012)
  4. Aguirre, Nazareno M.; Bengolea, Valeria S.; Frias, Marcelo F.; Galeotti, Juan P.: Incorporating coverage criteria in bounded exhaustive black box test generation of structural inputs (2011)
  5. Giannakopoulou, Dimitra; Bushnell, David H.; Schumann, Johann; Erzberger, Heinz; Heere, Karen: Formal testing for separation assurance (2011)
  6. Huang, J. C.: Software error detection through testing and analysis (2009)
  7. Păsăreanu, Corina S.; Visser, Willem: A survey of new trends in symbolic execution for software testing and analysis (2009)
  8. Arcuri, Andrea; Yao, Xin: Search based software testing of object-oriented containers (2008)
  9. Demakov, A.V.; Zelenov, S.V.; Zelenova, S.A.: Using abstract models for the generation of test data with a complex structure (2008)
  10. Pelánek, Radek; Rosecký, Václav; Moravec, Pavel: Complementarity of error detection techniques (2008)
  11. Zybin, R.S.; Kuliamin, V.V.; Ponomarenko, A.V.; Rubanov, V.V.; Chernov, E.S.: Automation of broad sanity test generation (2008)
  12. Beckert, Bernhard; Gladisch, Christoph: White-box testing by combining deduction-based specification extraction and black-box testing (2007)
  13. Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak: The software model checker blast (2007)
  14. Engel, Christian; Hähnle, Reiner: Generating unit tests from formal proofs (2007)
  15. Simons, Anthony J.H.: Jwalk: a tool for lazy, systematic testing of java classes by design introspection and user interaction (2007)
  16. Simons, Anthony J.H.: Jwalk: a tool for lazy, systematic testing of Java classes by design introspection and user interaction. (2007)
  17. Veanes, Margus; Ernits, Juhan; Campbell, Colin: State isomorphism in model programs with abstract data structures (2007)
  18. Chockler, Hana; Kupferman, Orna; Vardi, Moshe: Coverage metrics for formal verification (2006)
  19. Lämmel, Ralf; Schulte, Wolfram: Controllable combinatorial coverage in grammar-based testing (2006)
  20. Xie, Tao; Notkin, David: Tool-assisted unit-test generation and selection based on operational abstractions (2006)

1 2 next