0

What is the application of symbolic execution? Do symbolic execution only generate path condition? How can I use symbolic execution to verify contract?

Cactus
  • 27,075
  • 9
  • 69
  • 149
any
  • 325
  • 5
  • 17

1 Answers1

4

The most famous usage of symbolic execution is test input generation. For example, KLEE is a tool that generates test inputs for C programs using symbolic execution.

Another application would be assertion checking. If by contract you mean pre and post conditions, then yes, symbolic execution can also be used for that purpose.

afsafzal
  • 592
  • 5
  • 15
  • thanks a lot. Does symbolic execution generate test input only with aiding constraint solver? Would you please tell me more about how using symbolic execution for checking pre and post conditions? – any Sep 20 '16 at 16:24
  • As far as I know yes, it generates test inputs with the help of constraint solver. Simplest idea: Imagine you have a function with pre and post conditions. By using symbolic execution you find path condition for all the possible paths of that function. If the "post-condition and path-condition" is satisfiable within all paths then post condition holds. – afsafzal Sep 20 '16 at 17:42
  • Thanks for your kind help. if the "post-condition and path-condition" is satisfiable or "pre-condition and path-condition"? – any Sep 20 '16 at 17:50
  • imagine the pre condition is that `a` should be greater than zero. Then symbolic execution would put this constraint in the list of constraints for all paths. So pre-condition is satisfied implicitly. At the end of a path if path condition specifies `a` should be greater than 5 but post-condition specifies it should be less than 4 then there's at least one path that the post-condition is not met. – afsafzal Sep 20 '16 at 18:00
  • Thank you very much indeed. I have another question about implementation of symbolic execution for the specific language with declarative and imperative parts that is posted in http://stackoverflow.com/questions/39490607/implement-symbolic-execution-without-model-checking/39493738?noredirect=1#comment66308462_39493738 link. if you could help me and explain more I thank you. – any Sep 20 '16 at 18:25
  • No problem. I'd appreciate if you could accept the answer. – afsafzal Sep 20 '16 at 19:24
  • Don't you have any idea about the answer of that post? – any Sep 20 '16 at 19:33
  • how can I check satisfaction of post-condition and path-condition? – any Sep 24 '16 at 05:22