WADT'22 - 26th International Workshop on Algebraic Development Techniques 2022

Aveiro, 28 - 30 June 2022

Plenary Talk: Building Correct-by-Construction Systems with Formal Patterns

Formal patterns are formally specified generic solutions to commonly occurring computational problems that are correct by construction. Being generic, a formal pattern applies, not just to a single system, but to a typically infinite class of systems that satisfy some requirements. Application of a formal pattern to a system satisfying the formal pattern's input requirements results in a new system with new functionality that is correct by construction. Such correctness takes the form of an assume-guarantee property: assuming the original system meets the formal pattern's input requirements, then application of the formal pattern to such a system is guaranteed to enjoy specific correctness properties. The notion of formal pattern can be best expressed in the computational logic of a declarative programming language, so that a program is a theory in such a logic. I will use rewriting logic and the Maude language to illustrate the main ideas. Mathematically, a formal pattern is a theory transformation P that transforms the theory T specifying an input system, perhaps with some additional parameters p, into a new theory P(T,p) specifying the new correct-by-construction system generated by P. I will explain the notion of formal pattern and will give examples of formal patterns to build systems in different areas such as: (i) cyber-physical systems, (ii) distributed systems, (iii) secure systems, (iv) theorem proving, and (v) probabilistic verification.

Jose Meseguer (University of Illinois at Urbana-Champaign and Leverhulme Visiting Professor, King's College, London)

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 at 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 very 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 concurrent systems. 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 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, 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, and tools for interoperating different formal systems. Meseguer is a Fellow of the ACM. He received the FME Fellowship Award at the World Congress on Formal Methods in 2019, the Test of Time Award for his paper on Noninterference (with J.A. Goguen) at the Berkeley Security and Privacy Conference in 2019, the IEEE AIAA David Lubkowski Award for Advancement in Digital Avionics for the PALS formal pattern for asynchronous real-time systems (with S.P. Miller, D. Cofer, L. Sha and A. Al-Nayeem) at the 28th DASC in 2009, and several other awards for other research papers. 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, Estonian, Romanian, Colombian, and Japanese universities, research centers, and Summer/Winter Schools. He has also served as Chair or Program Committee member in numerous international scientific conferences and as editor of various scientific books, journals, and journal issues.

Program of WADT'22

New!!! Timetable of WADT'22

Previous Editions

Steering Committee

Program Committee

The conference is supported by CIDMA through the Portuguese Foundation for Science and Technology, reference UIDB/04106/2020