FASE Invited Speaker José Meseguer
José Meseguer is Professor of Computer Science at UIUC and leads the Formal Methods and Declarative Languages Laboratory. He obtained his Ph.D. in Mathematics at the University of Zaragoza, Spain, in 1975. After post-doctoral stays at the University of Santiago de Compostela, and at the University of California at Berkeley, he joined in 1980 the Computer Science Laboratory at SRI International in Menlo Park, California, where he became a Principal Scientist and Head of the Logic and Declarative Languages Group. He joined the University of Illinois at Urbana-Champaign in 2001.
He has worked on the design and implementation of several declarative languages, including the OBJ and Maude languages, on formal specification and verification techniques, on concurrency theory, on formal approaches to object-oriented specification, on parallel software and architectures for declarative languages, and on the logical foundations of computer science using equational logic, rewriting logic, and the theory of general logics.
Talk
Capturing System Designs with Formal Executable Specifications
Time: TBA
Room: TBA
Basing system designs on informal specifications and applying formal methods after system implementation greatly reduces the benefits that formal methods can provide. Systems of high quality and trust worthiness can be developed in a faster and much more efficient way by capturing system designs with formal executable specifications and subjecting them to automated formal verification from the earliest stages of system design. Even greater benefits can be gained by making such formal designs highly composable and reusable by means of formal patterns. The experience on using the rewriting-logic-based language Maude and its tool environment and formal patterns for all these purposes is presented and illustrated with concrete examples. The benefits of combining model-based design approaches with the one based on formal executable specifications are also discussed and illustrated with examples.