Generalized Symbolic Execution for Model Checking and Testing

By Sarfraz Khurshid, Corina S. Pasareanu, Willem Visser. International Conference on Tools and Algorithms for Construction and Analysis of Systems, 2003

664 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/0860cc74c766c2d52b28d90bead2ee6cea3f3e89

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

Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution (2005, methodology): “[19, 33] proposed an approach for generating tests for Java classes based on symbolic execution.”
KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs (2008, neutral): “However, the approaches are somewhat complementary to KLEE : the tests KLEE generates can be used to drive the model checked code, similar to the approach embraced by Java PathFinder [31,37].”
The software model checker Blast (2007, background): “, 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): “While [30] describes in detail how symbolic execution and lazy initialization are used during model checking, we high-light here the use of complex preconditions during lazy initialization, to initialize the inputs only with valid values.”
Differential symbolic execution (2008, background): “3 Lazy symbolic execution algorithm [39] .”
A NICE Way to Test OpenFlow Applications (2012, neutral): “[23] enable a model checker to perform symbolic execution.”
Combining unit-level symbolic execution and system-level concrete execution for testing nasa software (2008, methodology): “Moreover, the approach in [27] requires an (approximate) type-based static analysis [4] to determine if a program bytecode needs to be executed symbolically, and therefore needs to be instrumented.”
CUTE: a concolic unit testing engine for C (2005, methodology): “The classic approach is to use depth first exploration of the paths by backtracking [14].”
Symbolic Execution with Separation Logic (2005, background): “Red-black trees are a form of balanced search trees which can be easily implemented (see [11, 5]).”
Relational Symbolic Execution (2017, methodology): “Traditionally, symbolic execution has been used more for bug finding and testing [Khurshid et al. 2003; King 1976] than for proving.”
Using Frankencerts for Automated Adversarial Testing of Certificate Validation in SSL/TLS Implementations (2014, background): “We discuss the latter vulnerability in more detail in Section VIII.”
Symbolic execution for software testing in practice: preliminary assessment (2011, background): “Modern approaches, such as generalized symbolic execution (GSE) [33] and jCUTE [51], address multi-threaded programs with complex data structures as inputs.”