Jose Meseguer: Rewriting Logic Based Semantics and Analysis of Concurrent Programs

 

Abstract: Rewriting logic is a very simple computational logic with good features as a model-independent semantic framework to specify concurrent systems and languages. The semantics of a programming language can be naturally defined as a rewrite theory in a new specification style that combines the best features of structural operational semantics and of algebraic semantics while overcoming their limitations. Thanks to rewriting logic's high performance implementation in the Maude system and to Maude's built-in support for execution, breadth first search, and LTL model checking, one can use the rewriting logic semantics of a concurrent language to build formal analysis tools for that language essentially for free, with a performance competitive with that of more conventional formal analysis tools. If time permits, I will discuss our recent experience at UIUC applying these techniques to Java and the JVM in joint work with A. Farzan, F. Cheng, and G. Rosu.

CV: Dr. Jose Meseguer is Professor of Computer Science at the University of Illinois at Urbana-Champaign. He has made fundamental contributions in the frontier between executable formal specification and verification, declarative programming languages, logical frameworks, and concurrency. His work in all these areas is highly cited. The Maude language, based on rewriting logic, is one of the most advanced and efficient executable specification languages in existence. It supports a wide range of formal analyses, including symbolic simulation, search, model checking, and theorem proving. Maude has been used as a metatool to build other formal tools such as theorem provers, formal analyzers for conventional code, and tools for interoperating different formal systems. It has also been used to specify and analyze many systems, including cryptographic protocols, active network protocols, real-time distributed systems, hardware and software architectures, and to give an executable formal semantics to programming languages.