Karem Sakallah: SAT-Enabled Verification of State Transition Systems

PRACTICALITIES

Lunch is served at 12:00 noon (register at this doodle at the latest the Saturday before, but preferably earlier). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for ca two hours of more technical discussions.

ABSTRACT

Modern conflict-driven clause-learning (CDCL) SAT solvers, introduced twenty years ago, have had a profound impact in many domains by enabling the solution of large-scale problems that were thought to be out of reach. It is now routine for modern SAT and SAT modulo Theories (SMT) solvers to tackle decision problems containing millions of variables and constraints. Verification of complex hardware and software systems is now increasingly facilitated by the automated reasoning capabilities of modern SAT technology.

In this seminar I argue that the CDCL paradigm is now sufficiently mature and attempts to improve it further can only yield incremental gains in performance and capacity. Instead, I propose to combine it with two equally powerful concepts to allow for scalable reasoning about exponentially-large state transition systems. The first concept, pioneered by the IC3 and later PDR incremental induction reachability solvers, culminates a decades-old quest for solving the so-called state explosion problem in model checking. The second concept, CounterExample-Guided Abstraction Refinement (CEGAR for short), provides an adaptive computational framework for managing complexity by a) judicious elimination of irrelevant details (abstraction/over-approximation)  and by b) automatically filtering any false positives/spurious counterexamples (refinement).

After briefly describing the salient features of these two concepts I will illustrate their use, along with an underlying SAT/SMT engine, on two example applications of state transition systems: sequential hardware verification and detection of cross-site scripting (XSS) in PHP web servers. In both cases the goal is to show that all states reachable from a good initial state satisfy a given safety property or to produce a counterexample trace demonstrating violation of the property.