The DOI matches its Crossref record; 28 of the 28 references it cites were found in a registry or an index.
Korat: automated testing based on Java predicates
Abstract
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.
Overview
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Integrity signals
Registry
Cites
Statistics
Verification
Claims the paper makes
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
The self-check needs the paper’s full text.
Citations
Cites
(1994) · Cited by 21,711
Rayward-Smith, V. J. (1991) · Journal of the Operational Research Society · doi:10.1057/jors.1991.155 · Cited by 16,821
The Unified Modeling Language reference manual
Rumbaugh, J. E., Booch, G., & Jacobson, I. (1999) · CERN Document Server (European Organization for Nuclear Research) · Cited by 4,175
Holzmann, G. J. (1997) · IEEE Transactions on Software Engineering · doi:10.1109/32.588521 · Cited by 3,803
Clarke, E., McMillan, K., Campos, S., & Hartonas-Garmhausen, V. (1996) · Lecture Notes in Computer Science · doi:10.1007/3-540-61474-5_93 · Cited by 2,839
(1998) · PDCA/Test · doi:10.1201/9781420048131.axh · Cited by 1,900
McMillan, K. L. (1993) · Springer eBooks · doi:10.1007/978-1-4615-3190-6 · Cited by 1,677
Visser, W., Havelund, K., Brat, G., Park, S., & Lerda, F. (2003) · Automated Software Engineering · doi:10.1023/a:1022920129859 · Cited by 1,343
Coward, P. D. (1990) · The Software Life Cycle · doi:10.1016/b978-0-408-03741-9.50028-3 · Cited by 1,290
Bandera: extracting finite-state models from Java source code
Corbett, J. C., Dwyer, M. B., Hatcliff, J., Laubach, S., Păsăreanu, C. S., Robby, & Zheng, H. (2000) · Proceedings of the 22nd international conference on Software engineering - ICSE '00 · doi:10.1145/337180.337234 · Cited by 1,059
Cited by
DART: directed automated random testing
Godefroid, P., Klarlund, N., & Sen, K. (2005) · ACM SIGPLAN Notices · doi:10.1145/1064978.1065036 · Cited by 2,067
The software model checker Blast: Applications to software engineering
Beyer, D., Henzinger, T. A., Jhala, R., & Majumdar, R. (2007) · International Journal on Software Tools for Technology Transfer · doi:10.1007/s10009-007-0044-z · Cited by 585
Grammar-based whitebox fuzzing
Godefroid, P., Kiezun, A., & Levin, M. Y. (2008) · Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation · doi:10.1145/1375581.1375607 · Cited by 462
JCrasher: an automatic robustness tester for Java
Csallner, C., & Smaragdakis, Y. (2004) · Software: Practice and Experience · doi:10.1002/spe.602 · Cited by 426
Evolutionary testing of classes
Tonella, P. (2004) · Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis · doi:10.1145/1007512.1007528 · Cited by 410
Metadata
- Authors
- Boyapati, C., Khurshid, S., & Marinov, D.
- Venue
- ACM SIGSOFT Software Engineering Notes
- Published
- 2002-07
- Volume
- 27
- Issue
- 4
- Pages
- 123-133
- ISSN
- 0163-5948 (ISSN-L)
- OpenAlex
- W2162120832
- Cited by
- 593
- References
- 28
- FWCI
- 95.56
- Type
- journal article
- Language
- en
- Open access
- closed
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
How to cite
Cite CoChat for the checks on this page, and the paper for its own findings.
- This page
- CoChat. (2026). Citation check: Korat: automated testing based on Java predicates. https://app.cochat.ai/papers/10.1145/566171.566191
- The paper
- Boyapati, C., Khurshid, S., & Marinov, D. (2002). Korat: automated testing based on Java predicates. ACM SIGSOFT Software Engineering Notes. https://doi.org/10.1145/566171.566191
Data sources
Bibliographic data: Semantic Scholar, OpenAlex, Crossref.
Contains information from the Semantic Scholar Academic Graph Datasets, made available under the ODC Attribution License (ODC-BY 1.0).
Semantic Scholar’s data is described in: Kinney, R., et al. (2023). The Semantic Scholar Open Data Platform. arXiv:2301.10140.
