Efficient Directionless Weakest Preconditions (CMU-CyLab-10-002)
Explore this paper's citation graph
Summary
This work reconciles the differences between FSE and WP by proposing a new directionless weakest precondition that can be run in both the forward and backward direction, and provides the more attractive O(M) VC generation time and predicate size while allowing VC generation in execution order, which is what makes FSE attractive in practice.
- Type
- article
- Published
- 2010-01-01
- Cited by
- 1
- References
- 25
- Access
- Open access
- OpenAlex
- https://openalex.org/W27509964
- Semantic Scholar
- https://api.semanticscholar.org/CorpusID:59778657
Keywords
Computer science, Correctness, Predicate transformer semantics, Symbolic execution, Mathematical proof
References
- EXE: A system for automatically generating inputs of death using symbolic execution
- Automated Whitebox Fuzz Testing
- KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs
- Avoiding exponential explosion: generating compact verification conditions
- CUTE: a concolic unit testing engine for C
- A generalization of Dijkstra's calculus
- Proof-carrying code
- Grammar-based whitebox fuzzing
- An efficient method of computing static single assignment form
- A survey of new trends in symbolic execution for software testing and analysis
- DART: directed automated random testing
- A Discipline of Programming
- Hybrid Concolic Testing
- Dynamic test input generation for database applications
- Snugglebug: a powerful approach to weakest preconditions
- Compositional dynamic test generation
- Abstraction-guided Test Generation: A Case Study
- Bouncer: securing software by blocking bad input
- Creating Vulnerability Signatures Using Weakest Preconditions
- Efficient weakest preconditions
Cited by
Related papers
- Efficient Directionless Weakest Preconditions
- On the Correctness and Efficiency of Independent And-Parallelism in Logic Programs
- Compiling equational programs into efficient machine code
- Transformational programming: applications to algorithms and systems
- Logic Program Termination Analysis Using Atom Sizes
- Automatic program analysis using Max-SMT
- Improving Reachability Analysis in Ltsmin
- Staging with delimited control