Korat

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 33 articles )

Showing results 21 to 33 of 33.
Sorted by year (citations)
  1. Chockler, Hana; Kupferman, Orna; Vardi, Moshe: Coverage metrics for formal verification (2006) ioport
  2. Lämmel, Ralf; Schulte, Wolfram: Controllable combinatorial coverage in grammar-based testing (2006)
  3. Xie, Tao; Notkin, David: Tool-assisted unit-test generation and selection based on operational abstractions (2006) ioport
  4. Artho, Cyrille; Barringer, Howard; Goldberg, Allen; Havelund, Klaus; Khurshid, Sarfraz; Lowry, Mike; Pasareanu, Corina; Roşu, Grigore; Sen, Koushik; Visser, Willem; Washington, Rich: Combining test case generation and runtime verification (2005)
  5. Ball, Thomas: A theory of predicate-complete test coverage and generation (2005)
  6. Gaudel, Marie-Claude: Formal methods and testing: Hypotheses, and correctness approximations (2005)
  7. Godefroid, Patrice; Klarlund, Nils: Software model checking: Searching for computations in the abstract or the concrete (2005)
  8. Leavens, Gary T.; Cheon, Yoonsik; Clifton, Curtis; Ruby, Clyde; Cok, David R.: How the design of JML accommodates both runtime assertion checking and formal verification (2005)
  9. Xie, Tao; Marinov, Darko; Schulte, Wolfram; Notkin, David: Symstra: A framework for generating object-oriented unit tests using symbolic execution (2005)
  10. Artho, Cyrille; Drusinksy, Doron; Goldberg, Allen; Havelund, Klaus; Lowry, Mike; Pasareanu, Corina; Rosu, Grigore; Visser, Willem: Experiments with test case generation and runtime analysis (2003)
  11. Grieskamp, Wolfgang; Nachmanson, Lev; Tillmann, Nikolai; Veanes, Margus: Test case generation from AsmL specifications (2003)
  12. Khurshid, Sarfraz; Păsăreanu, Corina S.; Visser, Willem: Generalized symbolic execution for model checking and testing (2003)
  13. Souter, Amie L.; Wong, Tiffany M.; Shindo, Stacey A.; Pollock, Lori L.: TATOO: \textitTestingand \textitAnalysis\textitToolfor \textitObject-\textitOrientedsoftware (2001)