SUMMARY: Rewriting modulo SMT is a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze reachability properties of infinite-state open systems, i.e., systems that interact with a nondeterministic environment. Such systems exhibit both internal nondeterminism, which is proper to the system, and external nondeterminism, which is due to the environment. In a reflective formalism, such as rewriting logic, rewriting modulo SMT can be reduced to standard rewriting. Hence, rewriting modulo SMT naturally extends rewriting-based reachability analysis techniques, which are available for closed systems, to open systems. In this talk, I will be discussing the main conceptual and technical ideas behind rewriting modulo SMT, its state of implementation in the Maude system, and some research challenges to be tackled during the next few years.
SHORT BIO: Camilo Rocha is an Associate Professor in the Department of Electronics and Computer Science at the Pontificia Universidad Javeriana (Cali, Colombia). He earned a B.Sc. and a M.Sc. degree in Informatics from the Universidad de los Andes (Bogotá, Colombia), and a M.Sc. degree in Mathematics and a Ph.D. degree in Computer Science from the University of Illinois (Urbana, USA). He is currently working on developing symbolic techniques and tools for reachability analysis in rewriting logic. Overall, his research interests are in formal methods, algorithms, and software engineering, more specifically on techniques for building reliable software systems. Details and more information about his research can be found at his personal web page: http://camilorocha.info.