Symbolic execution and program testing

DOI10.1145/360248.360252zbMath0329.68018OpenAlexW2101512909MaRDI QIDQ4095837

James C. King

Publication date: 1976

Published in: Communications of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/360248.360252

Mathematics Subject Classification ID

Related Items (73)

A symbolic programming approach to the rendezvous search problem ⋮ Efficient symbolic analysis of programs ⋮ A unified integration and component testing approach from deterministic stream X-machine specifications ⋮ Loop Invariant Symbolic Execution for Parallel Programs ⋮ Algebraic program analysis ⋮ Introduction to Model Checking ⋮ SAT-Based Model Checking ⋮ Combining Model Checking and Testing ⋮ Backward symbolic execution with loop folding ⋮ Gray-box monitoring of hyperproperties with an application to privacy ⋮ Semantic subtyping with an SMT solver ⋮ Correct approximation of IEEE 754 floating-point arithmetic for program verification ⋮ Automatic construction of test sets: Practical approach ⋮ Model Checking MSVL Programs Based on Dynamic Symbolic Execution ⋮ Executing and verifying higher-order functional-imperative programs in Maude ⋮ Purging in an equality data base ⋮ Concolic testing in logic programming ⋮ Quantum symbolic execution ⋮ Stateful Behavioral Types for Active Objects ⋮ Symbolic Analysis of Maude Theories with Narval ⋮ Enhancing active model learning with equivalence checking using simulation relations ⋮ Symbolic runtime verification for monitoring under uncertainties and assumptions ⋮ Sound symbolic execution via abstract interpretation and its application to security ⋮ Automated verification of functional correctness of race-free GPU programs ⋮ A unifying view on SMT-based software verification ⋮ Symbolic execution of Reo circuits using constraint automata ⋮ Formal testing for separation assurance ⋮ TASS: the toolkit for accurate scientific software ⋮ Hierarchical development of programming languages ⋮ Recognizing malicious software behaviors with tree automata inference ⋮ Unnamed Item ⋮ Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning ⋮ Symbolic Execution as DPLL Modulo Theories ⋮ Simple linear string constraints ⋮ A dynamic logic for deductive verification of multi-threaded programs ⋮ Concolic Testing in CLP ⋮ Learning register automata: from languages to program structures ⋮ Unnamed Item ⋮ Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation ⋮ Densities of almost surely terminating probabilistic programs are differentiable almost everywhere ⋮ A CLP heap solver for test case generation ⋮ Calculational design of a regular model checker by abstract interpretation ⋮ Testing data processing-oriented systems from stream X-machine models ⋮ Symbolic execution formally explained ⋮ A generic framework for symbolic execution: a coinductive approach ⋮ Symbolic execution based on language transformation ⋮ Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs ⋮ Scalable and precise refinement of cache timing analysis via path-sensitive verification ⋮ FLIC: Application to Caching of a Dynamic Dependency Analysis for a 3D Oriented CRS ⋮ An efficient method to generate feasible paths for basis path testing ⋮ Test case generation for object-oriented imperative languages in CLP ⋮ Predicate abstraction in a program logic calculus ⋮ Concolic Execution in Functional Programming by Program Instrumentation ⋮ Combining test case generation and runtime verification ⋮ CompoSAT: specification-guided coverage for model finding ⋮ An evaluation of the effectiveness of symbolic testing ⋮ Lindenmayer grammars and symbolic testing ⋮ JMLUnit: The Next Generation ⋮ Test Data Generation of Bytecode by CLP Partial Evaluation ⋮ Path Feasibility Analysis for String-Manipulating Programs ⋮ Unnamed Item ⋮ Precondition Inference from Intermittent Assertions and Application to Contracts on Collections ⋮ Collective Assertions ⋮ Certified abstract cost analysis ⋮ Dashed strings for string constraint solving ⋮ Symbolic Execution Based Model Checking of Open Systems with Unbounded Variables ⋮ A Survey of Satisfiability Modulo Theory ⋮ Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework ⋮ Performance Estimation Using Symbolic Data ⋮ The application of hypergroups in symbolic executions and finite automata ⋮ A formal methodology using attributed grammars for multiprocessing-system software development. II. Validation ⋮ Estimating the volume of solution space for satisfiability modulo linear real arithmetic ⋮ Symbolic computation in Maude: some tapas

This page was built for publication: Symbolic execution and program testing