ABOUT THE CALENDAR
[Dissertation Talk] Scalable Model Checking Beyond Safety
Presentation: Departmental | May 9 | 4-5 p.m. | 521 Cory Hall
Sayak Ray, UC Berkeley
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.
EECS Home | Contact WebTeam |
Copyright © 2013 UC Regents