0
$\begingroup$

I have started reading some textbooks and papers on Model Checking, and have run into the closely related but different Symbolic Execution. I have a few open questions on StackOverflow about the "symbolic" aspect of Symbolic Model Checking and Symbolic Execution. At first I thought they meant the same thing but now I am starting to think they are mostly unrelated and incompatible. But I can't quite tell yet.

My question here is how to combine Symbolic Model Checking with Symbolic Execution.

Here is my understanding so far. In regards to Symbolic Model Checking, they keep on saying sets of states are manipulated rather than individual states. And states are encoded in boolean variables. You then represent boolean formulas over these variables using Binary Decision Diagrams (BDDs). They mentioned "every finite set can be represented as a Boolean function." but I'm not sure what that means. They go on to say "each state $s$ is bit-string comprising values of state variables". "Transition is a state pair (s, s’)." And "compute $S_0, S_1, S_2, \dots$ where $S_i$ is the set of states reachable from some initial state." Finally, from here, "the main idea behind symbolic model checking is to represent and manipulate a finite state-transition system symbolically as a Boolean function."

So from that information, which is similar in textbooks, here's what I gather. In Symbolic Model Checking, "symbolic states" are just sets of boolean variables. A transition is also just a set of boolean variables but between two states (but I think only the current state and next state, I'm not sure if it includes jumping over states). The model of the program then is a state-transition graph. So it's just boolean variables everywhere. This gets me wondering how this is actually encoded, but will save that for a later question perhaps. It seems like this:

[s1(v1, v2 && v3), s2(v1, v2 || v3), t1(s1, s2), ...]

Essentially just a big matrix of boolean variables somehow. That's what I'm gathering. But I am left confused as to how they "compute next states" in Symbolic Model Checking. There's still a disconnect there. And not sure how the boolean variables got there in the first place.

Then there is Symbolic Execution. In this one, states are propositional formulas rather than sets of boolean variables. Close but not quite the same (I think). A way that it is similar to Symbolic Model Checking is that you have to "explore the state space" by progressively generating the next state. I am not sure the details of how the two systems differ because I don't yet know exactly how to "calculate" the Symbolic Model Checking states. But the Symbolic Execution states are all the branching points you made in the code to get from the initial state to the current state. And by "symbolic", Symbolic Execution means we are actually passing symbols around in the code (in a layer of abstraction above the code, somehow) instead of "values". I am starting to understand how this works. But I don't see how you could combine it with Symbolic Model Checking, since it would be like combining boolean state variables with symbolic states. There's a disconnect for me there.

The paper linked to above combines Symbolic Model Checking with Symbolic Execution, however. They say they made something "which enables standard model checkers to perform symbolic execution of the program". But they don't really explain how it works. What the model checker is doing in the Symbolic Execution environment. And how the "states as boolean variables" can work alongside symbolic variables and symbolic states.

To summarize, my question is how to combine Symbolic Model Checking with Symbolic Execution, so the BDDs (from symbolic states in Symbolic Model Checking) are somehow working alongside the symbolic states and symbolic variables (from Symbolic Execution).

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.