Fourteenth Summer School on Formal Techniques

Techniques based on formal logic, such as model checking, satisfiability, static analysis, and automated theorem proving, are finding a broad range of applications in modeling, analysis, verification, and synthesis. This school, the fourteenth in the series, will focus on the principles and practice of formal techniques, with a strong emphasis on the hands-on use and development of this technology. It primarily targets graduate students and young researchers who are interested in studying and using formal techniques in their research. A prior background in formal methods is helpful but not required. Participants at the school can expect to have a seriously fun time experimenting with the tools and techniques presented in the lectures during laboratory sessions. The main lectures will run from Monday May 26 to Friday May 30. They will be preceded by a background course "Speaking Logic" taught by Natarajan Shankar and Stéphane Graham-Lengrand (SRI CSL) on May 24/25.

The lecturers at the school include:

• Joost-Pieter Katoen - Deductive Verification of Probabilistic Programs with Caesar
• Erika Abraham - Understanding and using SAT and SMT solvers
• Kristin Yvonne Rozier - Runtime Verification with R2U2
• Philippa Gardner - Compositional Verification using the Gillian Platform
• Nate Foster - Programming and Reasoning with Kleene Algebra with Tests

Lectures

• Deductive Verification of Probabilistic Programs with Caesar
  Joost-Pieter Katoen (RWTH Aachen)
  Abstract: Probabilistic programs encode randomized algorithms, robot controllers, learning components, security mechanisms, and much more. They are however hard to grasp. Not only by humans, also by computers: checking elementary properties related to e.g., termination are "more undecidable" than for ordinary programs. The analysis of probabilistic programs requires manipulating irrational or even transcendental numbers.

  Although this all sounds like a no-go for (semi-)automated analysis, I will present a deductive verification technique to analyse probabilistic programs. In contrast to simulation (like MCMC), this analysis yields exact results. Our technique is based on weakest precondition reasoning. We will explain the foundations of this approach, present some proof rules to reason about probabilistic while-loops, and discuss how the analysis can be automated---either fully or with the help of invariants.

  Hands-on experiments will be carried out using the deductive verifier Caesar, see "https://www.caesarverifier.org.

  
  Bio: Joost-Pieter Katoen is a distinguished professor at RWTH Aachen University, leading the Software Modeling and Verification (MOVES) group. He is part-time affiliated to the University of Twente. His main research contributions are in model checking, concurrency theory, probabilistic computation, and formal semantics.

  His book Principles of Model Checking (with Christel Baier) is a bestseller in formal verification. He received numerous best paper awards and other honors, most recently the JCL Award 2023 in Dependable Computing. He is a member of the Academia Europaea, the Royal Holland Society of Sciences and Humanities (KHMW) and the German Academy of Sciences (2024). He received an honorary doctorate from Aalborg University (2017) and is an ACM Fellow (2020).

  
  
• Understanding and using SAT and SMT solvers
  Erika Abraham (RWTH Aachen)
  Abstract: Satisfiability checking is a research area devoted to the development and implementation of algorithms that allow to check the satisfiability of logical formulas.

  For propositional logic formulas, which are Boolean combinations of Boolean variables, we could enumerate and check all possible variable assignments. However, due to its bad average complexity, this exploration approach is not applicable in practice. Alternatively, the proof system of Boolean resolution can be applied, but the applicability of this method is also restricted to rather small problems. In the 90s, an elegant combination of these two methods has been suggested, where the proof construction is guided by an exploration of the assignment space equipped with a smart look-ahead mechanism. This idea allowed to develop impressively powerful SAT solvers, which are able to effectively solve huge problems at industrial scale.

  The effectivity of SAT solvers gave motivation to extend to scope of solver technologies to formulas of quantifier-free first-order logic over different theories. On the one hand, eager SMT solving approaches have been proposed for certain theories to transform their formulas to propositional logic and use SAT solving to check the result for satisfiability. On the other hand, (full/less) lazy SMT solving uses SAT solving to explore the Boolean structure of the formula, and employs theory solvers to check the consistency of Boolean assignments in the theory domains. SMT solvers can be used as general-purpose off-the-shelf tools. Due to their impressive efficiency, they are nowadays frequently used in a wide variety of applications. A typical application encodes real-world problems as logical formulas, whose solutions can be decoded to solutions of the real-world problem.

  Recently, the idea of symbiotic combination of exploration and proof construction has been also generalized to theories, most notably quantifier-free real algebra, in the framework of the model constructing satisfiability calculus (MCSAT). In this approach, exploration-guided proof construction is designed to run both in the Boolean space and in the theory domain, simultaneously in a consistent manner.

  In this unit we give an introduction to the above mechanisms of SAT and SMT solving, discuss some interesting ideas behind recent developments, and illustrate the usage of SMT solvers on some application examples.

  
  Bio: Erika Abraham graduated in Computer Science at the Christian-Albrechts-University Kiel (Germany), and received her PhD from the University of Leiden (The Netherlands) for her work on the verification of concurrent programs. Then she moved to the Albert-Ludwigs-University Freiburg (Germany), where she started to work on the automated solution of arithmetic problems (SAT and SMT solvers). Since 2008 she is professor at RWTH Aachen University (Germany), with main research focus on SMT solving for real and integer arithmetic, and formal methods for probabilistic and hybrid systems.
• Runtime Verification with R2U2
  Kristin Yvonne Rozier (Iowa State)
  Abstract: R2U2, the Realizable Responsive Unobtrusive Unit was designed to fill a gap in real-world, and flight-certifiable, runtime verification. It enables realizable verification of an easy, expressive specification language based on Mission-time Linear Temporal Logic (MLTL), with a generic interface that is highly adaptable to a wide range of missions and platforms. System designers can configure R2U2 once, then change the properties under test while the system, and R2U2, are running, without reconfiguration or re-upload, a critical feature for many aerospace applications. R2U2 is real-time responsive, continuously monitoring the system and detecting anomalies in real-time, or even ahead of real time with minimal estimation, to enable effective mitigation or rescue measures. It is also uniquely unobtrusive, designed not to change system behavior, certifiabiity, timing, tolerances, cost, or other mission parameters.

  Today R2U2 is the only space-flight-certified runtime verification engine, and it has launched into space on several missions, including NASA's Lunar Gateway, Robonaut2 on the International Space Station, and a JAXA satellite. Lectures will feature the algorithms and architecture of the tool, while highlighting successful applications. There are multiple implementations of R2U2, and it is highly configurable to the specific needs of the mission under analysis; we will survey the options for specialization and analysis. Labs will offer an opportunity to configure and run R2U2 on realistic case studies, utilizing the human-facing C2PO interface.

  Resources: R2U2 is open-source software, available for download from its website (https://r2u2.temporallogic.org/). There are several support tools for better specification elicitation, validation, and debugging of R2U2's primary specification logic Mission-time Linear Temporal Logic (MLTL); we will use the WEST GUI (link TBD).
  Bio: Professor Kristin Yvonne Rozier heads the Laboratory for Temporal Logic in Aerospace Engineering at Iowa State University; previously she spent 14 years as a Research Scientist at NASA and three semesters as an Assistant Professor at the University of Cincinnati. She earned her Ph.D. from Rice University and B.S. and M.S. degrees from The College of William and Mary. Dr. Rozier's research focuses on automated techniques for the formal specification, validation, and verification of safety critical systems. Her primary research interests include: design-time checking of system logic and system requirements; runtime system health management; and safety and security analysis.

  Her advances in computation for the aerospace domain earned her many awards including: the NSF CAREER Award; the NASA Early Career Faculty Award; American Helicopter Society's Howard Hughes Award; Women in Aerospace Inaugural Initiative-Inspiration-Impact Award; two NASA Group Achievement Awards; two NASA Superior Accomplishment Awards; Lockheed Martin Space Operations Lightning Award; AIAA's Intelligent Systems Distinguished Service Award; Building a World of Difference faculty fellowship. She holds an endowed position as Dennis and Rebecca Muilenburg Professor, is an Associate Fellow of AIAA, and is a Senior Member of IEEE, ACM, and SWE. Dr. Rozier has served on the NASA Formal Methods Symposium Steering Committee since working to found that conference in 2008.

  
  
• Compositional Verification using the Gillian Platform
  Philippa Gardner (Imperial)
  Abstract: One of the main challenges that modern program analysis tools must face is scalability, that is, the ability to tractably analyse large, dynamically changing codebases. Such scalability requires techniques and tools that are functionally compositional (or simply compositional) where the analysis works on functions in isolation, at any point in the codebase, and then records the results in simple function specifications that can be used in broader calling contexts. However, the traditional tools based on first-order logic can only be compositional for functions that manipulate the variable store, but not for functions that manipulate the heap, limiting their usability.

  A key insight is that, to obtain compositionality, the analysis should work with function specifications that are local, in that they should describe the function behaviour only on the partial states or resources that the function accesses or manipulates, and a mechanism for using such specifications when the function is called by code working on a larger state. This insight was first introduced in separation logic (SL, [1]), a modern over-approximating (OX) program logic for compositional verification of correctness properties, which features local function specifications that can be called on larger state with the help of the frame rule. Recently, these ideas have been adapted to under-approximate (UX) reasoning in the context of incorrectness separation logic (ISL, [3,2]) for compositional true bug-finding.

  Ideas from SL and ISL have led to the development of efficient compositional symbolic execution tools and platforms in academia and industry, such as VeriFast, Viper and CN for semi-automatic OX verification based on SL, Meta’s Infer-Pulse for automatic UX true bug-finding based on ISL, and Gillian for both. Gillian [5,6,7,8] is unique in that it is parametric on the memory model of the language and its compositional symbolic execution engine is underpinned by strong mathematical foundations [4]. It has been instantiated to the C, JavaScript and Rust languages, and applied to industrial code.

  Course Outline: This course will provide a whirl-wind tour of separation logic, compositional symbolic execution and Gillian. It is adapted from my MSc course on “Scalable Verified Software: Separation Logic” that I have been teaching at Imperial for many years.

  The lectures will comprise:

  • An introduction to SL and ISL for reasoning about mutable data structures. You will learn how to write program specifications and prove properties of programs, both informally using sketch proofs and formally using rigorous proofs.
  • An introduction to compositional symbolic execution which creates and uses function specifications from underlying separation logics such as SL and ISL, and provides a sound theoretical foundation for, and indeed was partially inspired by, the Gillian platform.

  The labs will concentrate on compositional OX verification based on SL, and will give you hands-on experience of using Gillian. For the last three years, we have had experience holding a lab on Gillian as part of my MSc course, made possible due to the addition of a symbolic debugger for Gillian. The labs will comprise:

  • Experience with using the WiSL tool, a Gillian instantiation to a small while language with a simple block-offset memory model, exploring many exercises to transition from the informal proof sketches introduced in the lectures to the semi-automatic Gillian proofs that sometimes require the insertion of tactics.
  • Experience with using the Gillian-C tool, working with more complex examples from the lectures and (hopefully, it’s a little ambitious) the real-world Collections-C library.
  Before the Course Please install Gillian on your laptops before the course starts; installation instructions for Gillian can be found at the link https://gillianplatform.github.io/sphinx/index.html
  
  References:
  • Separation Logic: A Logic for Shared Mulable Sata Structures, John Reynolds, https:: www.cs.cmu.edu/~jcr/seplogic.pdf
  • Incorrectness Logic, Peter O'Hearn, POPL’20.
  • Local Reasoning about the Presence of Bugs: Incorrectness Separation Logic, Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O'Hearn and Jules Villard, CAV’20.
  • Compositional Symbolic Execution (CSE) for Correctness and Incorrectness Reasoning, Andreas L\"{o}\"{o}w, Daniele Sobrinho, Sacha-Elie Ayoung, Petar Maksimovic and Philippa Gardner, ECOOP'2024, distinguished paper. This paper centred on simple language and memory model. We are currently extending this work to be mechanised and parametric on the memory model, with a submission deadline in November 2024.
  • For the Gillian tool, see my lecture at the College de France: https://vtss.doc.ic.ac.uk/2021/04/15/collegedefrance.html
  • Symbolic Debugging with Gillian, Nat Karmios, Sacha-Elie Ayoun and Philippa Gardner, DEBT 2023.
  • Gillian, Part I: A Multi-language Platform for Symbolic Execution, José Fragoso Santos Petar Maksimovic, Sacha-Élie Ayoun and Philippa Gardner, PLDI 2020.
  • Gillian, Part II: Real-World Verification for JavaScript and C, Petar Maksimovic, Sacha-Élie Ayoun, José Fragoso Santos and Philippa Gardner, CAV 2021.
  
  Bio: Philippa Gardner’s work has brought scientific and mathematical method to the specification and analysis of open software at scale. She has built trustworthy mechanisations of language standards, leading to the correction of definitions and the formal proofs of properties within the W3C WebAssembly formal specification. She has developed compositional analysis techniques and well-engineered tools for both semi-automatic verification and automatic true bug-finding in industrial and open-source software. She has introduced program logics for verifying complex concurrent algorithms, which underpin tools now used by hundreds of specialist users. Her contributions represent over three decades of sustained investment, all focussed on achieving machine-proven guarantees about the safety and correctness of real, deployed software, grounded in mathematical foundations.

  After completing her PhD thesis at Edinburgh in 1992 and holding research positions in both Edinburgh and Cambridge, Gardner became a lecturer at Imperial in 2001 and a professor in 2009. She held fellowships spanning over twenty years, including a UKRI Established Research Fellowship from 2018 to 2023 at Imperial, and was elected a Fellow of the Royal Academy of Engineering in 2020. She won the British Computer Society Lovelace Medal in 2024, and was the founding director of the UK Research Institute of Verified Trustworthy Software Systems, funded by GCHQ and now directed by Azalea Raad and Brijesh Dongol.

  
  
• Programming and Reasoning with Kleene Algebra with Tests
  Nate Foster (Cornell University)
  Abstract: Kleene algebra with tests (KAT) is an algebraic framework that can be used to reason about imperative programs. It has been applied across a wide variety of areas including program transformations, concurrency control, compiler optimizations, cache control, networking, and more. These lectures will provide an overview of Kleene Algebra with Tests, including the syntax, semantics, and the coalgebraic theory underlying decision procedures for program equivalence. We will illustrate how it can be used as a core framework for network verification, including successful extensions and fundamental limitations.
  Bio: here
  Reading:
  • KAT [TOPLAS 19(3), May '97]: https://dl.acm.org/doi/10.1145/256167.256195
  • NetKAT [POPL '14]: https://dl.acm.org/doi/10.1145/2578855.2535862
  
  
• Speaking Logic
  Natarajan Shankar and Stéphane Graham-Lengrand (SRI CSL):
  

  Speaking Logic - Videos: Speaking Logic Part 1 (2021), Propositional Logic
  PVS Tutorial,
  Type Theory,
  VSCode-PVS Tutorial - VSCode-PVS Video
  

  
  Abstract: Formal logic has become the lingua franca of computing. It is used for specifying digital systems, annotating programs with assertions, defining the semantics of programming languages, and proving or refuting claims about software or hardware systems. Familiarity with the language and methods of logic is a foundation for research into formal aspects of computing. This course covers the basics of logic focusing on the use of logic as a medium for formalization and proof.