The state explosion problem is becoming less of an issue in software nowadays because of the massive improvement in SAT/SMT solvers. The topic of this post is not about model checking, but I believe still interesting.

One big improvement when it came to verification came from symbolic execution [1], in which the verifier looks for assertion violations by representing variables as a set of constraints. At each assertion, the constraints are checked to see if they can be negatively satisfied, giving a counterexample for the error. We run the program in a special interpreter (or using some interesting metaprogramming and a compiler frontend etc) and at each conditional statement a new constraint is added, leading to a tree. By cleverly picking branches etc we hopefully drastically reduce the search space.

This reduced the state explosion problem in many cases, but obviously there's now an explosion on the control flow. A more recent improvement has been to unwind loops a bound number of times, encoding the whole program as a logical statement that is only satisfied by input that will trigger an assertion error. The hypothesis is that the structure of such formulas is well simplified by SAT solvers, and this has been borne out empirically from what I know. We can further improve by natively executing that code which is not constrained, which is a further boon - in principle we could instrument a program to simply return the formula that (if satisfied) produces counterexamples.

This sort of approach is very useful in practice because it's very understandable to software engineers - in the ideal case where a large company produces a product based on it, one might reasonably expect to be able to pass the software their source code and be presented with a series of counterexamples. It's all very interesting.

(I'm not an expert on this, take what I say with a pinch of salt).

[1] https://klee.github.io/klee/

> A more recent improvement has been to unwind loops a bound number of times, encoding the whole program as a logical statement that is only satisfied by input that will trigger an assertion error.

The technical term for this is bounded model checking (BMC).

I get what you're saying about the state explosion problem, but the article specifically calls out the idea of proving a lack of negative behaviors. It seems to me it might be quite useful to be able to prove, for example, that a program never reads memory at random, or that it never exceeds the bounds of any allocated buffer.

That's a different problem scale than "prove the whole thing works as specified".

Model checking deals with two kinds of properties - safety and liveness. Safety properties effectively say nothing bad ever happens while liveness properties say that something good will eventually happen. For example, "my program will never crash due to a null point dereference" is a safety property. "My arbiter module will output a grant for every input request" is a liveness property.

It is true that model checkers are much better are proving safety properties than liveness properties. I think it's not too far from the truth to say that model checkers are no good at proving liveness properties in real designs and that only safety properties work (somewhat well) in practice.

An alternative here is to abandon model checking altogether and focus on a powerful static analysis. I think the main challenge here is coming up with effective property specification schemes. A powerful type system like Haskell does in fact enable you to prove quite strong statements about your program. But you are inherently limited in terms of what you can prove to whatever it is that the type system can express. To me, it seems that model checkers allow more flexibility in specifying your property, especially when you take into account the fact that you can do your model checking on an augmented/instrumented version of your design.

> That's a different problem scale than "prove the whole thing works as specified".

On a vaguely related note, equivalence checking between designs, especially in the hardware context, is one thing that formal tools have had a lot of success with.

> you are inherently limited in terms of what you can prove to whatever it is that the type system can express

Does that actually limit you? E.g. I can imagine using a monad-like structure in Haskell to construct things like "procedure guaranteed to terminate in <k primitive steps".

Well, considering that the article talks about Coq, which is completely built around a type system (plus a termination checker), it's not that limiting.

It's not just about whether it is possible in theory though. I'm sure it is, but if it's too complicated, it won't see adoption. The point I was making is that expressibility isn't just important in your programming language, it's important for your verification scheme as well.

Sadly, it's not a different problem scale — the typical model is something similar to "for each state, does the property P hold?". Hence no matter the property (or complexity thereof), one must still enumerate all states.

Of course, one will attempt to also find equivalence classes for the states! The code

    long x = user_input();
    if (x == 0) {
        violate_model();
    } else {
        do_something();
    }

you would expect by any reasonable implementation to collapse the system into just two equivalent states that can be tested.

Ah, but finding equivalence classes of states is quite tricky! Obviously the naive approach of enumerating states and assigning them to equivalence classes is dead on arrival. You might be hinting at examining control flow predicates with your example. This technique is called predicate abstraction and underlies a lot of the SLAM effort. It works in certain scenarios - A statement which more or less captures the state of the field itself.

What I'm personally hinting at is symbolic/concolic execution. Essentially, each variable has a set of constraints associated with it - initially left blank for an input variable, for example. Then, the program can be executed, with assignments producing new constraints and replacing old ones. At each point in control flow, the executor chooses a path, and adds new constraints. When a dangerous statement (assertion, pointer dereference etc) is reached, the constraints can be solved by z3 or some other SMT solver, and if it can find a satisfying result you automatically have a test case that will produce erroneous or undefined behaviour.

It works quite well for short programs, actually - the KLEE people (or maybe it was DART) found bugs in busybox, GNU Coreutils etc.

The current approach is to instead of traversing your control flow tree explicitly (which means you're doing a tree search over a potentially infinite tree), converting the program such that it produces a logical statement that can be solved by an SMT solver, that is satisfiable iff there is an input that leads to a bug within that bounded number of loop unwindings.

With fun C++ metaprogramming, you can actually get this to happen natively (i.e. the parts that aren't reliant on input get run natively) which leads to a massive speedup o

I don't believe it to be model checking, although it might use model checking techniques. I could be wrong, I'm only familiar with a few aspects.

I'd love to use proofs that my software is good; but after reading the 43 page "coq in a hurry" document, I still have no idea how to prove that "print 2 + 2" prints out "4", let alone how to apply it to any of my real world apps :(

Mostly it seems formal proof stuff looks a lot like my memories of the functional programming world -- lots of one-letter variable names and unicode symbols, no code comments, any word that isn't an abbreviation is in Latin; all emphasis on the abstract, no mention of how to make this wonderful formula interact with the real world... Is there some fundamental reason that a proof language can't be as readable and practical as Python?

I presume I got downvotes for people interpreting my memories of functional programming class at university as an insult? Gah :<

But still, I would really like to know to apply formal proofs to even the simplest of real-world code bases, and the documentation that I've found on the website doesn't seem to offer that information (or if it does, it does so in a language I don't understand) -- does anyone have any links to more useful tutorials?