Reputation: 349
How to implement a symbolic execution engine for a particular language?
I'm considering using symbolic execution to test the robustness of programs written in a particular language such as java. I've read some papers introducing the basic concepts of symbolic execution. But I'm not clear about how to get it started.
For example, how can I generate the constraint conditions from a concrete input? So any one can give me some advice on the basics of the implementation of symbolic execution? Furthermore, what about concolic execution(concrete + symbolic) ?
Upvotes: 5
Views: 1270
Answers (1)
Reputation: 6960
how can I generate the constraint conditions from a concrete input?
using symbolic or concolic execution
So any one can give me some advice on the basics of the implementation of symbolic execution?
My advice is the same as Ziming Zhao: use an existent symbolic execution tool. Do not attempt to implement your own, it would be too hard and time-consuming.
Here are the most popular projects (a more complete list here):
Java: JPF + Symbolic Pathfinder, JCute.
Upvotes: -1
Related Questions
- Building a custom language for logic execution
- How is Symbolic Execution different from Whitebox Fuzzing?
- error detection in static analysis and symbolic execution
- Static analysis vs. symbolic execution in implementation
- implement symbolic execution without model-checking
- application of symbolic execution
- symbolic execution and model-checking
- Modern symbolic execution techniques
- How could I generate and execute machine code at runtime?
- Implementing a stack-based interpreter