Technical Report PHD-2010-04

TR#:PHD-2010-04
Class:PHD
Title: New Approaches to Model Checking and 3-Valued Abstraction and Refinement
Authors: Avraham Yadgar
Supervisors: Orna Grumberg Assaf Schuster
PDFPHD-2010-04.pdf
Abstract: Model Checking is the problem of verifying the correctness of a system with respect to temporal logic properties. This is an important problem, which 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. Despite recent advancement in model checking algorithms and tools, efficient model checking remains a critical problem, due to the growing complexity of software and hardware systems.

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 abstraction and 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 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.

CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2010/PHD/PHD-2010-04), rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the PHD technical reports of 2010
To the main CS technical reports page

Computer science department, Technion
admin