# What exactly is Symbolic Model Checking?

I know that Symbolic Model Checking is state space traversal based on representations of states sets and transition relations as formulas like in CTL using models like Kripke Model. I know the theory. But I'm finding it hard to understand the actual application. Where exactly is it used? What exactly does it do and how does it work?

Can someone explain with a real example and relate theory to practice?

• This seems to broad to me. The "what does it do?" part may be reasonable scoped (or not), but "where is it used?" is a) another question entirely and b) probably too broad. Commented Mar 22, 2015 at 11:06
• But an example can be taken and explained based on that. That is not too broad. Commented Mar 22, 2015 at 11:17
• Why are you not satisfied with the description of Symbolic Model Checking in standard textbook, e.g., "Principles of Model Checking" by Christel Baier and Joost-Pieter Katoen? Which parts are you confused about? Commented Mar 22, 2015 at 11:53
• They speak about 'how it is supposed to be done' but not 'how exactly it is done'. I'm trying to relate the theory and the practical implementation. I'm still new to this and I need an example. Commented Mar 22, 2015 at 11:56
• You may be on the wrong site then. Computer science is about the concepts ("how it should be done"), you'll have to ask practitioners about the "how it's done" part. Commented Mar 22, 2015 at 16:11

Symbolic Model Checking is Model Checking that works on symbolic states. That is, they encode the states into symbolic representations, typically Ordered Binary Decision Diagrams (OBDDs).

The question is what do they do and how do they work.

You first have your source code for some application. You then transform your source code into some state-transition graph like a Kripke Structure. The states are filled with atomic propositions which describe what is true in that particular state. In Symbolic Model Checking the atomic propositions are encoded as OBDDs to save on space and improve performance.

The Model Checker then starts at some initial state, and explores the states, looking for errors in the state-transition graph. If it finds an error it will often generate a test case demonstrating the error. It uses the symbolic OBDDs to somewhat optimally navigate the state space. Wish I could explain more there but still learning.

But that's basically it. You have a program converted into a formal model (state-transition graph), and then you use symbolic optimizations to navigate the state space to look for errors (by comparing it against an LTL/CTL specification). And if an error is found, the Model Checker gives you some stuff to help document and solve it.

Symbolic model checking can be very useful for verifying the correctness of communications and security protocols. For example:

• A symbolic model of an OAUTH2 implementation could help check for unintended consequences where an adversary obtains secret authentication tokens or related circumstantial data that could help them contravene the process.
• A symbolic model of a cryptographic protocol, such as a TLS handshake, could help verify that the cryptographic design doesn't have any unintended consequences.

This works by writing a symbolic description of all the primitive functions and protocol algorithms, and then having a symbolic model checker, such as ProVerif, traverse the state space and attempt to detect state combinations that produce unfavorable results. In the case of ProVerif, symbolic models are described using the applied Pi calculus as the modeling language. This allows the description of protocols in a functional, ML-like syntax.