symbolic execution and model-checking

Question

What is the difference between symbolic execution and model checking (for example in model transformation)? I don't understand difference of them. Are they the same?!

Cholecyst

Many programs may do both. If you need to specify everything in an alternate language, the model checker is most likely the technology. It is good for verifying high level designs. It requires little expertise. Symbolic execution can work on existing code. It typically uses some SAT/SMT solver to validate constraints on execution. For example, this is what 'klee' does. Most of these require annotations or alteration of the code to prove/disprove some property. – Immovable

Here is one definition of symbolic execution from CPAChecker, "The symbolic execution analysis is similar to the value analysis. But instead of overapproximating variable values to the top element, it can introduce symbolic values and track constraints over these." Value analysis (like Frama-C EVA) will use ranges to evaluate under/over flow. With Klee, it also uses UBSan, which triggers over/underflow. 'Model checking' is usually equivalent to a Kripke structure (FSM with propositions). But many programs will be inspired by one, but often have elements of each (and theorem provers). – Immovable

Answer 1

In model checking, you have to encode your system as a Finite State Machine and provide that FSM to the model checker as well as a specification. The model checker will then make sure that the specification always holds in that system.

In symbolic execution you only provide your program and the symbolic execution engine will examine all the feasible paths to generate test inputs or check assertions.

A simple example of their difference: concurrency. Model checking can handle multi-thread systems because it is specified in the FSM provided as input, however, symbolic execution cannot handle more than one thread.

Pythagorean

Thanks for your kind help. Java Path Finder is model checking tool or symbolic execution tool or both?! Is there any symbolic execution tool that doesn't use model checking? – Cholecyst

Why can't symbolic execution handle more than one thread? – Bouilli

@StevenShaw Symbolic execution is based on 'logic'. Logic has only one flow and is 'timeless'. You need 'computational timed logic' (CTL), which is what all model checkers are based on. The underlying CTL mathematics has a notion of 'path' or evolution. – Immovable

@artlessnoise, Maybe you meant "Computational Tree Logic" – Matabele

@SuraajKS Yes, confusing as LTL is Linear Temporal Logic, where I replace with temporal with time. In reality most tools are fusing both concepts. Also the concepts are based on Temporal logic. You can see that most of the time logics use temporal. – Immovable

Answer 2

Model Checking: A method to formally verify that a program satisfies a specification. The specification is usually given in a temporal logic formula like: "if input is x output must be y - holds for all executions (globally) of the program" (see e.g. Edward A Lee).

Symbolic model checking versus explicit state checking: Programs can be finite state machines (FSM). Here explicit state checking is sufficient. But luckily model-checkers exist also for extended FSM's, concurrent, probabilistic, real-time applications. To help prevent state explosion in those systems with very large (infinite) number of states, symbolic model checking is used. In symbolic model checking the states and inputs etc. are treated as symbols and as propositional formulas (or sets of states, set operations etc.). To perform model checking a reachability analysis is needed and to do this the program transitions are executed symbolically. These checkers can't make use of the normal execution of instrumented native code.

Symbolic execution: There exist different methods of encoding during symbolic execution. Some are very specific to model checking and some are modular and used in a stand-alone symbolic execution framework, as it was defined by the inventors of symbolic execution. A symbolic execution framework often uses also some elements (exploration, search) of symbolic model checking to be usable for testing etc.

Finally some examples:

JPF, Java-Pathfinder: Model-checker, explicit state checking, input: java byte code

SPF, Symbolic Pathfinder: Symbolic execution, extension of JPF

JCBMC: Bounded Model Checker, extension of JPF, SPF

XRTs: Exploration and symbolic execution, input: CIL byte code

IntelliTest: Parameterized Unit Tests uses XRTs

Spec Explorer: Model-based Testing uses XRTs

Intercolumniation