Title: Programming, Specifying and Verifying in OBJ languages

Abstract:

OBJ is a family of algebraic languages for programming, modeling and verifying. In the past near 40 years, many variants have beed developed, which are based on order-sorted equational logic and enriched with other logics. Maude and CafeOBJ are two successful representatives in this family. In this talk, I will take Maude and CafeOBJ as examples to show how to program, model and verify in OBJ languages.  Specifically, I will show how to program in Maude both at object level and meta level, how to model and specify computer systems in Maude and CafeOBJ and how to do verifications based on the specifications (model checking in Maude and theorem proving CafeOBJ). 

Short biography:

Zhang Min is now a researcher in Japan Advanced Institute of Science and Technology (JAIST). He received his Ph.D in computer science from JAIST in 2011. Then, he worked as a researcher in the Research Center for Software Verification in JAIST until now. His main research interest is symbolic formal methods.