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
(Recordings)
-
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).
Materials:
-
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.
Materials: Prior to the start of the lab sessions, please install
Python and Z3 on your computers. Instructions can be found here:
https://github.com/exercism/z3/blob/main/docs/INSTALLATION.md
-
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.
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.
Materials: R2U2 is open-source software, available for download from its website (https://r2u2.temporallogic.org/). There are currently three implementations of R2U2 (hardware/VHDL, C, and embedded Rust); we will use the embedded Rust version. 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 (tool download: https://github.com/zwang271/WEST website: https://west.temporallogic.org). In addition to directly interfacing with R2U2 to configure runtime verification, we will utilize the new R2U2 Playground (https://r2u2.temporallogic.org/playground/), an interactive web-based playground that provides visualization of R2U2 monitors. The R2U2 Playground provides stepwise execution coupled with reactive timeline plotting and visualization of its internal abstract syntax tree architecture.
-
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
Materials: Slides, labs, tools, etc. can be found at https://gillianplatform.github.io/sphinx/labs/ssft25/index.html
References:
- Separation Logic: A Logic for Shared Mutable 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
Materials:
-
Invited Speakers
-
An Enriched Category Theory of Language
Tai-Danae Bradley
Abstract: The success of large language models is striking, especially given that the training data consists of raw, unstructured text. In this talk, we will propose that category theory can provide a natural framework for investigating this passage from texts, and probability distributions on them, to a more semantically meaningful space. Equipped with motivation from an analogy between linear algebra and category theory, we will define a category of expressions in language enriched over the unit interval and afterwards pass to enriched copresheaves on that category. We will see that the latter setting has rich mathematical structure and comes with ready-made tools in which to explore that structure.
Slides
-
On Mechanical Program Verification
Robert Shostak
Slides
-
Formal Verification (FV) In Chip Design
Vigyan Singhal
Slides
Previous Summer Schools on Formal Techniques
Information about previous Summer Schools on Formal Techniques can
be found at
Jay Bosamiya of CMU has blogged about the 2018 Summer School at
https://www.jaybosamiya.com/blog/2018/05/31/ssft/
This year, the school/bootcamp will take place in a hybrid mode:
the lectures and labs will be live-streamed and recorded. We
strongly encourage in-person participation so that you can benefit
from interactions outside the classroom. We have funding from NSF
to cover transportation/food/lodging expenses for selected
US-based students. Non-student and non-US in-person participants
are expected to cover their own transportation and will be charged
a fee (around $150/day) to cover the cost of food and lodging.
The 2025 Summer School on Formal Techniques will be presented in a
hybrid format. We encourage those students who can attend in
person to do so. Those who cannot be there in person can still
participate virtually but they will need to synchronize with the
Pacific Daylight Savings Time. Applications should be submitted
together with names of two references (preferably advisors,
professors, or senior colleagues).
Applicants are urged to submit their applications before March 31,
2025, since there are only a limited number of spaces available.
Those needing invitation letters for visa purposes are encouraged
to complete their applications as early as possible. We strongly
encourage the participation of women and under-represented
minorities in the summer school.
The nearest airport to the summer school is SFO. Use Supershuttle
for ground transportation to/from SFO - we should have a discount
code shortly.