Introduction to bounded model checking that describes model generation

Most of the tutorials I have found on model checking and bounded model checking start with, the model is given as a Kripke Structure M = (S,I,T,L) where S is a set of states, I is a set of initial states, T is a transition relation, and L is a labeling function. Model checking takes a property P and tries to determine if P is true in the model M.

The algorithms for model checking (and bounded model checking) provided for a given Kripke structure are very understandable, and are all quite neat. For example,

An Analysis of SAT-based Model Checking Techniques in an Industrial Environment

and the survey by Prasad et all 2005, are both very readable and understandable.

Now, suppose one wants to take a program and use model checking to determine if the program is correct. As far as I can tell, the hard part is determining a suitable model of the program. I am trying to figure out, for example, how CBMC derives a formula for a plain SAT solver since this would involve constructing a model and then a CNF formula for plain SAT such that if the formula is true then there is a counter example to the predicate. I think they use bit-vector logic, whatever that means.

I have glanced through:

CBMC (C Bounded Model Checker)

Bit-Vectors in Decision Procedures An Algorithmic Point of View

Slides for CBMC: Bounded Model Checking for ANSI-C

These are focused on how a tool works, and lack some of the details I am looking for. I'm curious if there are any more tutorialish writeups on how to build a SAT based model checking tool, and discuss how to develop the model and whether to use plain SAT of SMT solver.

Alternatively, if someone could point me in the direction of producing a model, given a property and a program written in a very simple language with say a single type: 32bit-Integers, functions, assignments, if-then, if-then-else, and optionally while-loops, that would output a formula for a SAT or SMT solver such that the formula is satisfiable iff the property is not true of the program, then I would also be so grateful.

• Have you read the paper from the CBMC authors where they describe CBMC? As I recall, I'm pretty sure their paper describes how they translate from code to a model and to SAT. By the way, are you asking about how to generate a model (a Kripke Structure) given the code of a program, or are you asking how to bit-blast to SAT given a model? You might want to edit your question to clarify. Typically we first define a transition relation $\delta$, then we translate the bounded model checking problem to SAT (which involves a translation of $\delta$ to SAT along the way; see the Tseitin transform). – D.W. Jul 1 '14 at 0:11
• Do you mean this paper: kroening.com/papers/asp-dac2003.pdf If so, I just found it. – Jonathan Gallagher Jul 1 '14 at 1:39
• For the second question, I guess I was asking both. What is the model one gets out? Do systems using this approach translate down to SAT via bit-blasting, (which I guess involves translating arithmetic to a circuit, to a boolean circuit, to a formula), or whether they use some modified SAT + Constraint Solver. But I am more interested in the model. – Jonathan Gallagher Jul 1 '14 at 1:54
• Yes, they basically use bit-blasting. OK, typically they will convert to SMT, not to SAT, so that they can use things like the theory of arrays, and then feed that to a SMT server. But from a conceptual perspective, you can think of what the SMT solver does as itself bit-blasting to SAT (actually, that is indeed how some SMT solvers work). The CBMC papers should give the basic idea -- why don't you spend some time reading those papers, then see if you can frame a more specific question based on that, and edit your question accordingly? – D.W. Jul 1 '14 at 4:27