Title: Bounded Model-Checking for Universal Branching-Time Logic
Speaker: Rotem Oshman (MIT)
Place:  32-G575
Time:   1-2:30pm
Date:   Friday October 24th 2008

Abstract:
The model-checking problem is the problem of determining, given a design and
a specification, whether the design satisfies the specification or not.
Model-checking is computationally difficult because of the state-space
explosion problem: the number of states in the design increases
exponentially with the number of variables. Bounded model-checking (BMC) is
a method that has gained popularity in the industry due to its ability to
handle large industrial designs. In BMC, a SAT solver is used to find
counter-examples (bugs) with respect to a given specification. Although it
is best suited for "bug hunting", BMC can sometimes be used to prove
properties as well.

Typically, BMC is applied only to linear-time specifications, which treat
the computations of the program as distinct paths. Some interesting
properties cannot be expressed in linear-time logic, and require
branching-time logic, which talks about the computation tree of the program.
Previous attempts to extend the BMC approach to universal branching-time
logic have searched for a counter-example with a pre-determined shape: the
edges of the counter-example were selected based on worst-case analysis of
the specification, and the SAT solver assigned the states.

We suggest a new approach, in which we allow the SAT solver to choose both
the states and the edges of the counter-example. This significantly reduces
the size of the counter-example produced by BMC and allows us to handle more
complex specifications. We also present two termination criteria, which can
be used to halt BMC when it becomes clear that no counter-example can exist
in the model. Thus, in addition to bug hunting, our technique can also
achieve verification of properties (if no bugs exist).

The talk assumes no prior knowledge of model-checking or temporal logic.