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 1 to 20 of 33.
Sorted by year (citations)

1 2 next

  1. Ponzio, Pablo; Godio, Ariel; Rosner, Nicolás; Arroyo, Marcelo; Aguirre, Nazareno; Frias, Marcelo F.: Efficient bounded model checking of heap-manipulating programs using tight field bounds (2021)
  2. Porncharoenwase, Sorawee; Nelson, Tim; Krishnamurthi, Shriram: CompoSAT: specification-guided coverage for model finding (2018)
  3. Claessen, Koen; Duregård, Jonas; Pałka, Michał H.: Generating constrained random data with uniform distribution (2015)
  4. Brucker, Achim D.; Wolff, Burkhart: On theorem prover-based testing (2013)
  5. Bengolea, Valeria; Aguirre, Nazareno; Marinov, Darko; Frias, Marcelo F.: Using coverage criteria on repOK to reduce bounded-exhaustive test suites (2012) ioport
  6. Nokhbeh Zaeem, Razieh; Gopinath, Divya; Khurshid, Sarfraz; McKinley, Kathryn S.: History-aware data structure repair using SAT (2012) ioport
  7. 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) ioport
  8. Giannakopoulou, Dimitra; Bushnell, David H.; Schumann, Johann; Erzberger, Heinz; Heere, Karen: Formal testing for separation assurance (2011)
  9. Huang, J. C.: Software error detection through testing and analysis (2009)
  10. Păsăreanu, Corina S.; Visser, Willem: A survey of new trends in symbolic execution for software testing and analysis (2009) ioport
  11. Arcuri, Andrea; Yao, Xin: Search based software testing of object-oriented containers (2008) ioport
  12. Demakov, A. V.; Zelenov, S. V.; Zelenova, S. A.: Using abstract models for the generation of test data with a complex structure (2008)
  13. Pelánek, Radek; Rosecký, Václav; Moravec, Pavel: Complementarity of error detection techniques (2008) ioport
  14. Zybin, R. S.; Kuliamin, V. V.; Ponomarenko, A. V.; Rubanov, V. V.; Chernov, E. S.: Automation of broad sanity test generation (2008)
  15. Beckert, Bernhard; Gladisch, Christoph: White-box testing by combining deduction-based specification extraction and black-box testing (2007)
  16. Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak: The software model checker blast (2007) ioport
  17. Engel, Christian; Hähnle, Reiner: Generating unit tests from formal proofs (2007)
  18. Simons, Anthony J. H.: Jwalk: a tool for lazy, systematic testing of java classes by design introspection and user interaction (2007) ioport
  19. Simons, Anthony J. H.: Jwalk: a tool for lazy, systematic testing of Java classes by design introspection and user interaction. (2007) ioport
  20. Veanes, Margus; Ernits, Juhan; Campbell, Colin: State isomorphism in model programs with abstract data structures (2007)

1 2 next