A Rewriting Logic Sampler

  • Jose Meseguer | CS Dept. Univ. of Illinois at Urbana-Champaign

Rewriting logic is a simple computational logic very well suited as a semantic framework within which many different models of computation, systems and languages can be naturally modeled. It is also a flexible logical framework in which many different logical formalisms can be both represented and executed. As the title suggests, the talk does not try to give a comprehensive overview of rewriting logic. Instead, after introducing the basic concepts, it focuses on some recent research directions emphasizing:

  1. Extensions of the logic to model real-time systems and probabilistic systems; and
  2. Some exciting application areas such as: semantics of programming languages, security, and bioinformatics.

Speaker Details

Dr. Jose Meseguer received a Ph.D. in Mathematics from the University of Zaragoza, Spain. He is Professor of Computer Science at the University of Illinois at Urbana-Champaign (UIUC). Prior to moving to UIUC he was a Principal Scientist as the Stanford Research Institute (SRI), after having held postdoctoral positions at the University of California at Berkeley and IBM Research. He was also an Initiator Member of Stanford University’s Center for the Study of Language and Information (CSLI).Dr. Meseguer has made fundamental contributions in the frontier between executable formal specification and verification, declarative programming languages, programming methodology, concurrency, and security. His work in all these areas is highly cited (see http://citeseer.ist.psu.edu/mostcited.html). The Maude language is one of the most advanced and efficient executable specification languages. It supports a wide range of formal analyses, including symbolic simulation, search, model checking, and theorem proving. It is also an advanced declarative concurrent language with sophisticated object-oriented features and powerful module composition and reflective metaprogrammign capabilities. He, his collaborators, and other researchers have used Maude and its tool environment to build sophisticated systems and tools, and to specify and analyze many systems, including criptographic protocols, active network protocols, models of cell biology, executable formal semantics of programming languages, formal analyzers for conventional code, theorem provers, and tools for interoperating different formal systems. He has given numerous invited lectures at international scientific meetings and has taught advanced courses on his research at leading American, British, German, Spanish, Italian, and Japanese universities and research centers. He has also served in numerous program committees of international scientific conferences and as editor of various scientific journals.

Watch Next