Marsha Chechik: Multi-Valued Model-Checking: Theory, Implementation and Applications

Abstract: In software engineering, one often models with more than just boolean values True and False, e.g., to explicitly represent partiality or disagreement in a system, to assign labels or colors to transitions between states, etc. Such models can be thought of as multi-valued, i.e., described in logics with additional truth values. Reasoning about such models can always be done classically, but usually at the expense of complex translation into two-valued models and not being able to interpret results of the analysis on the original model. Over the past two years, we have developed a theory of performing model-checking directly on multi-valued models and implemented a symbolic multi-valued model-checker XChek. In this talk, I will outline the fundamentals of multi-valued model-checking, discuss some implementation details of XChek, including complexity and the representation of counter-examples, and describe several domains of application of multi-valued model-checking.

Biography: Marsha Chechik received her Ph.D. from the University of Maryland in 1996 and joined the Computer Science department at the University of Toronto. She is now an associate professor of Computer Science, currently on sabbatical at Lucent Technologies in Murray Hill, NJ. Prof. Chechik's research interests are mainly in the paplication of formal methods to improve quality of software. She has authored over 35 papers in formal methods, software specification and verification, and requirements engineering. She is also interested in software engineering education and in computer security.