טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentOshman Rotem
SubjectBounded Model - Checking for Branching-Time
Logic
DepartmentDepartment of Computer Science
Supervisor Professor Orna Grumberg
Full Thesis textFull thesis text - English Version


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. One method that has gained industrial acceptance due to its ability to handle large designs is bounded model-checking (BMC), a technique for finding bugs with respect to a given specification through the use of a SAT solver.


BMC is typically applied only to the class of linear-time specifications, which talk about distinct computations of the program. However, many 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 only had to assign 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 a dynamic completeness criterion which can be used to halt the bounded model-checking when it becomes clear that no counter-example to the specification can exist in the model. Thus, in addition to finding bugs (if they exist), our technique can also verify that the specification is satisfied (if no bugs exist).