These lectures will also be live-streamed: click on the dates below for the Teams links.

External participants required to register.

Maude is a high-performance (up to 50 million rewrites per second) declarative programming language based on rewriting logic, with contains equational logic as a sublogic. A Maude program is either an equational theory (called a functional module), or a rewrite theory (called a system module). Since those theories define initial models in each logic, Maude programming is exactly mathematical modeling. Besides making Maude a very succinct ultra-high-level language, this makes verification of Maude programs much easier than in conventional languages. What makes all this particularly attractive is that Maude is also a very expressive multi-paradigm programming language supporting:

1. Functional programming (in functional modules)

2. Concurrent programming (in system modules)

3. Concurrent object-oriented programming (in object-oriented modules)

4. Constraint programming (for both functional and system modules).

The Leverhulme Lectures at KCL will introduce the main ideas about Maude programming and verification in a series of six lectures as follows:

30 June, 14.00-16.00, Bush House (SE) 1.08

• Lecture 1, 14.00-15.00: Programming Deterministic Systems in Equational Logic
• Lecture 2, 15.00-16.00: Constraint Solving in Maude

7 July, 14.00-16.00, Bush House (SE) 2.02

• Lecture 3, 14.00-15.00: Verifying Maude Functional Modules with Maude's NuITP
• Lecture 4, 15.00-16.00: Programming Concurrent Systems in Rewriting Logic

14 July, 14.00-16.00, Bush House (SE) 1.08

• Lecture 5, 14.00-15.00: Modal Logic Properties of Concurrent Systems and their Model Checking Verification in Maude

• Lecture 6, 15.00-16.00: Symbolic Model Checking and Theorem Proving Verification of Invariants

 

Speaker

Jose Meseguer received his 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). Currently, he is also Leverhulme Visiting Professor at King's College London. Prior to moving to UIUC he was a Principal Scientist as the Stanford Research Institute (SRI), after having held a postdoctoral position at the University of California at Berkeley and a visiting faculty position at IBM Research. He was also an Initiator Member of Stanford University's Center for the Study of Language and Information (CSLI).

Meseguer has made fundamental contributions in the frontier between mathematical logic, executable formal specification and verification, declarative programming languages, programming methodology, programming language semantics, concurrency, and security. His work in all these areas, comprising over 400 publications, is highly cited. His contributions to security include fundamental concepts such as nointerference, browser security verification (including uncovering 12 types of unknown spoofing attacks in Internet Explorer, and full verification of the IBOS Browser), new algorithms and verification techniques to defend systems against Distributed Denial of Service (DDoS) attacks, and new symbolic techniques to analyze cryptographic protocols modulo complex algebraic properties that have been embodied in the Maude-NPA Protocol Analyzer. He is the creator of rewriting logic, a very flexible computational logic to specify both concurrent systems and logics. He is also the main designer of the Maude rewriting logic language, one of the most advanced and efficient rule-based programming languages worldwide.

Maude is also an advanced declarative concurrent programming language with sophisticated object-oriented and constrain solving features and powerful module composition and reflective meta-programming capabilities. Maude and its Formal Environment support a wide range of formal analyses, including symbolic simulation, search, explicit-state and symbolic model checking, and theorem proving. Meseguer, his collaborators, and other researchers have used Maude and its formal environment to build sophisticated systems and tools, and to specify and analyze many systems, including cryptographic protocols, network protocols, web browsers, cloud computing data stores, real-time and cyber-physical systems, models of cell biology, executable formal semantics of programming languages and of hardware and software modeling languages, formal analyzers for conventional code, theorem provers, logics, and tools for interoperating different formal systems.