Ph.D Thesis

Ph.D StudentYadgar Avraham
SubjectNew Approaches to Model Checking and to 3-Valued Abstraction
and Refinement
DepartmentDepartment of Computer Science
Supervisors PROFESSOR EMERITUS Orna Grumberg
PROF. Assaf Schuster
Full Thesis textFull thesis text - English Version


Model Checking is the problem of verifying the correctness of a system with respect to temporal logic properties . This is problem is constantly becoming more critical, as software and hardware systems are growing rapidly. Complex systems are more prone to implementation errors, thus demanding a thorough validation. The high time and space requirements of the checking makes the verification of large systems hard to perform.

In this work we present new approaches to symbolic model checking of hardware systems. Our approaches are aimed at increasing the performance of model checkers. We address the size of the systems that are being checked, the verification runtime, and its memory requirements. Our work is also aimed at increasing the automatization of model checking methodologies, thus decreasing human effort and required expertise of the verification engineer.

In our work we propose a memory efficient hybrid SAT and BDD based algorithm for model checking of circuits. This algorithm exploits the advantages of both SAT and BDD approaches, while avoiding their drawbacks as much as possible.

We also present a 3-valued-SAT based approach for Symbolic Trajectory Evaluation (STE). In this approach, STE is performed by using a novel 3-valued SAT solver, instead of the conventional, BDD-based, approach.

A common approach for addressing the capacity problem in model checking is using \emph{abstraction} and \emph{refinement}. In this work we present different methods for automatic refinement in STE, instead of the common manual refinement. These methods require less user effort and expertise, and are less error prone.

We also present an automata theoretic approach to 3-Valued model checking, which can be used for explicit and symbolic model checking. We implement this approach in 3-valued \emph{Bounded Model Checking} (BMC). Our BMC abstraction outperforms conventional abstraction in BMC both in the sizes of the systems being checked, and in the runtime of the verification tool. We propose a new methodology for using BMC for very large systems, based on our 3-valued abstraction. Our methodology requires significantly less user effort and expertise than the common methodologies for BMC of large designs, and is less error prone.