Symbolic execution and program testing

By J. King. 1976

How researchers see this paper

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

Citations in the corpus

Detecting Violations of Differential Privacy (2018, methodology): “Then, the symbolic executor tracks symbolic program states along program execution in the standard way [26].”
Evasion and Hardening of Tree Ensemble Classifiers (2015, methodology): “We call this approach symbolic prediction in reference to symbolic program execution (King, 1976), because we essentially move a symbolic instance ˜ x down the regression tree and keep track of the constraints imposed on ˜ x by all encountered predicates.”
Programming with a Differentiable Forth Interpreter (2016, methodology): “We do this using symbolic execution [11]: we ﬁrst ﬁll the stacks and heap of a standard Forth abstract machine with symbols representing arbitrary values (e.g.”
Machine Learning Testing: Survey, Landscapes and Horizons (2019, methodology): “Symbolic execution is a program analysis technique to test whether certain properties can be violated by the software under test [105].”
The Art, Science, and Engineering of Fuzzing: A Survey (2018, background): “introduced by Godefroid [90] in 2007 and refers to dynamic symbolic execution (DSE), which is a variant of symbolic execution [42], [130], [112].”
SgxPectre Attacks: Leaking Enclave Secrets via Speculative Execution (2018, methodology): “ts before deploying them to the untrusted SGX machines. To this end, we devise a dynamic symbolic execution technique to enable automated identification ofSgxPectre Attack gadgets. Symbolic execution [41] is a program testing and debugging technique in which symbolic inputs are supplied instead of c”
Automated Test Case Generation as a Many-Objective Optimisation Problem with Dynamic Selection of the Targets (2018, methodology): “Other than evolutionary approaches, other techniques have been proposed in the literature for test case and test data generation, such as dynamic symbolic execution [7], [26], [53], [56] and random testing [9], [32], [36], [37].”
NEZHA: Efficient Domain-Independent Differential Testing (2017, methodology): “Symbolic execution: Symbolic execution [43] is a white-box technique that executes a program symbolically , computes constraints along different paths, and uses a constraint solver to generate inputs that satisfy the collected constraints along each path.”
Automated Whitebox Fuzz Testing (2008, background): “Static test generation [19] consists of analyzing a program statically to attempt to compute input values to drive it along speciﬁc program paths without ever executing the program .”
Symbolic Robustness Analysis (2009, methodology): “Our algorithm is based on symbolic execution [3]–[6], which executes the program on symbolic inputs and aggregates symbolic constraints on each execution path.”
ODR: output-deterministic replay for multicore debugging (2009, methodology): “To meet this requirement, FormGen employs symbolic execution [12]–a method for deriving a formula representing the set of all read-traces along a given path.”
Towards automatic generation of vulnerability-based signatures (2006, methodology): “We use many static analysis techniques such as symbolic execution [31], abstract interpretation [18], model checking [15], theorem proving [20], dataflow analysis [29], and program slicing [57].”
Compositional dynamic test generation (2007, background): “Static test generation (e.g., [ Kin76 ]) consists of analyzing the program statically, by exclusively using symbolic execution techniques to attempt to compute inputs to drive along specific execution paths or branches, without ever executing the program.”
Guided GUI testing of android apps with minimal restart and approximate learning (2013, methodology): “To resolve this, we would need to combine existing GUI test generation techniques with symbolic execution [61] or search-based testing techniques [48, 49], in the sense that hybrid concolic testing [72] combines random testing and concolic execution [33].”
Deductive Software Verification – The KeY Book (2016, methodology): “For this reduction we employ the technique of symbolic execution [King, 1976].”
The software model checker Blast (2007, background): “There is a rich literature on test-vector generation using symbolic execution [23, 36, 39, 55, 57, 58, 75].”
A Survey of Symbolic Execution Techniques (2016, background): “Two fundamental approaches, pioneered by King in a seminal article [68], are the following:”
Automated program repair (2019, methodology): “The path condition of a program path is a formula which is true for those inputs which traverse the path [19].”