Skip to main content.
Advanced search >
<< Back to previous page Print

<< Thursday, May 09, 2013 >>


Remind me

Tell a friend

Add to my Google calendar (bCal)

Download to my calendar

Bookmark and ShareShare


[Dissertation Talk] Scalable Model Checking Beyond Safety

Presentation: Departmental | May 9 | 4-5 p.m. | 521 Cory Hall


Sayak Ray, UC Berkeley

Electrical Engineering and Computer Sciences (EECS)


Liveness is an extremely important but challenging issue in design verification. It is one of the two major categories of formal property specification. The other category, which is relatively simpler than liveness, is called safety. Safety properties specify that something bad will never happen. For example, the property of mutual exclusion, which specifies that two concurrent processes will never access a critical section simultaneously, is a safety property. Liveness properties, on the other hand, specify that something good will eventually happen. Scenarios like deadlock-freedom, livelock-freedom, stabilization etc. are modeled using liveness properties. Unfortunately, traditional algorithms for liveness verification are very inefficient in practice. We need domain-specific, smart heuristics to solve real-life, industrially-relevant problems.

In this research, we have developed symbolic algorithms and their
open-source implementations that effectively solve liveness verification problem for many industrially relevant hardware systems. In principle, our tool-suite works on any sequential hardware circuit and for the whole family of omega-regular properties. Practicality and effectiveness of our tool-suite have been demonstrated in the context of proving response property (a very common and important liveness property) of on-chip communication fabrics. In this talk, I will discuss two techniques - k-liveness with disjunctive stabilizing constraints, and liveness-to-safety conversion technique for stabilization properties. The former one is effective for proving, and the latter one is effective for disproving liveness properties.


sayak@eecs.berkeley.edu, 510-409-8687