Up

Efficient State Merging in Symbolic Execution

Efficient State Merging in Symbolic Execution

1 If you have program if (x < 0) x = 0; else x = 5; with X assigned to x you can merge two states (X < 0, [x = 0]) and (X >= 0, [x = 5]) to one state (true, [x = ITE(X < 0, 0, 5)]). So, you can represent whole program with one SMT formula. Or one function as in Veritesting.

12 pages

Sergey Vartanov, 2007–2020