Korat: automated testing based on Java predicates

By Chandrasekhar Boyapati, Sarfraz Khurshid, Darko Marinov. International Symposium on Software Testing and Analysis, 2002

778 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/d293bbbb004f5fce0d328341e0b8cfc922e3e536

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

In Software

Citations in the corpus

DART: directed automated random testing (2005, methodology): “Korat [5] is a tool that can analyze a Java method’s precondition on its input and automatically generate all possible non-isomorphic inputs up to a given (small) size.”
Compositional dynamic test generation (2007, neutral): “Recently, there has been a renewed interest on automated test generation from program analysis (e.g., [ BKM02 , BCH + 04, VPK04, CS05, GKS05, CE05]).”
Grammar-based whitebox fuzzing (2008, methodology): “In systematic approaches, test inputs are created from a specification, given either a special piece of code (e.g., Korat [ 5 ]) or a logic formula (e.g., TestEra [19]).”
Evolutionary testing of classes (2004, methodology): “While the generation procedure used in [4] builds complex data structure directly, by satisfying the related class invariants, in this paper only elementary data types are built through generators, while complex data structures are obtained from the execution of (part of) the chromosome, by means of”
Generalized Symbolic Execution for Model Checking and Testing (2003, methodology): “Following [2], we could systematically initialize array length when an array field is first accessed, and then treat each array component as a field.”
The software model checker Blast (2007, background): “Therefore, most research on symbolic execution-based test generation curtails the search by bounding, e.g., the number of iterations of loops, the depth of the search, or the size of the input domain [ 15 ,36,55,58].”
Test input generation with java PathFinder (2004, methodology): “The lazy initialization of repOk that we use for black-box test input generation can be compared to the approach taken by Korat [10].”
JCrasher: an automatic robustness tester for Java (2004, background): “A recent piece of work on generating test inputs automatically from specifications in the Java setting is the Korat system [23].”
Statistical Debugging: A Hypothesis Testing-Based Approach (2006, background): “can help expedite the generation of test cases [26], [27], [28],”
CUTE: a concolic unit testing engine for C (2005, methodology): “, generate only the input memory graphs for which repOk returns true [5, 27].”
Android permissions demystified (2011, methodology): “Korat [7] requires formal specifications of methods as input, which is infeasible for post-facto testing of the Android API.”
Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution (2005, methodology): “The first six classes were previously used in evaluating Rostra [34], and the last five classes were used in evaluating Korat [8].”