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 thirteenth 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 27 to Friday
May 31. They will be preceded by a background course "Speaking
Logic" taught by Natarajan Shankar and Stéphane
Graham-Lengrand (SRI CSL) on May 25/26. The summer school will be
immediately followed by a two-day Bootcamp to reinforce some of the
skills acquired during the school. Participants in the Bootcamp
will employ formal tools and techniques (including those taught in
this and prior summer school editions) under the supervision of the
Bootcamp faculty to create verified artifacts.
The lecturers at the school include:
- Josef Urban - Combining Machine Learning and Theorem Proving
- Marsha Chechik - Elicitation and Formal Reasoning about Normative Requirements
- Leonardo de Moura and David Thrane Christiansen - The Lean 4 programming language and theorem prover
- Cesare Tinelli - Modeling and analyzing reactive systems with logic-based symbolic model checkers
- Armando Solar-Lezama - Neurosymbolic Programming for Better Learning
Lectures
-
Combining Machine Learning and Theorem Proving
Josef Urban (CIIRC)
Abstract: The lectures will introduce the main approaches
that combine machine learning with automated theorem proving. This
includes learning to choose relevant facts in large theories,
learning to guide the proof search in automated provers, guiding
the application of tactics in interactive tactical systems,
various forms of conjecturing, and feedback loops interleaving
learning, proving and conjecturing. I will also show some demos of
the systems and mention related tasks such as autoformalization.
Bio: Dr. Josef Urban is a Distinguished Researcher at Czech
Institute of Informatics, Robotics and Cybernetics (CIIRC),
heading its AI department and formerly also the ERC project
AI4REASON. His main interests are in combining inductive/learning
and deductive/reasoning AI methods over large formal knowledge
bases. His systems have won several theorem proving competitions,
and the methods today assist formal verification in proof
assistants. He received his MSc in Mathematics and PhD in Computer
Science from Charles University in Prague, worked as an assistant
professor in Prague, and as a researcher at University of Miami
and Radboud University Nijmegen. He has also co-founded the
conference on Artificial Intelligence and Theorem Proving (AITP)
and co-organized it since 2016.
-
Elicitation and Formal Reasoning about Normative Requirements
Prof. Marsha Chechik (U. Toronto)
Abstract: As software and cyber-physical systems
interacting with humans become prevalent in domains such as
healthcare, education and customer service, software engineers
need to consider normative (i.e., social, legal, ethical,
empathetic and cultural) requirements. However, their elicitation
is challenging, as they must reflect the often conflicting or
redundant views of stakeholders ranging from users and operators
to lawyers, ethicists and regulators. I will describe a
tool-supported framework for normative requirements elicitation.
Built on top of LEGOS-a custom bounded satisfiability checker for
first order logic with transitive closure, our framework allows
specification of normative rules for a software system in an
intuitive high-level language called SLEEC, and provides automated
analysis to identify rule conflicts, redundancies, and other
well-formedness concerns. It also synthesizes feedback enabling
users to understand and resolve problems.
Our approach has been successfully applied to over a dozen of
realistic case studies from assistive-care robots and tree-disease
detection drones to manufacturing collaborative robots, and
supported teams of ethicists, lawyers, philosophers,
psychologists, safety analysts, and engineers.
Bio: Dr. Marsha Chechik is a Professor and Bell University Labs
Chair in Software Engineering the Department of Computer Science
at the University of Toronto, where she has been a faculty member
since 1996. She has served as Chair of the Department in 2019-22
and Acting Dean of Faculty of Information in 2022. Her research
interests are in the application of formal methods to improve the
quality of software. She has (co)-authored numerous papers in
formal methods, software specification and verification, computer
safety and security and requirements engineering. She is a member of
IFIP WG 2.9 on Requirements Engineering and an Associate Editor in
Chief of IEEE Transactions on Software Engineering and Journal on
Software and Systems Modeling. She has been Program Committee
Co-Chair of numerous conferences including the 2018 International
Conference in Software Engineering (ICSE18), the 2016
International Conference on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS'16), the 2014
International Conference on Automated Software Engineering
(ASE'14), and the ACM Joint European Software Engineering
Conference and Symposium on the Foundations of Software
Engineering (ESEC/FSE’21), International Conference on Formal
Methods (FM’22), International Conference on Modeling
(MODELS’24). She is an ASE Faculty Fellow and Distinguished Member of
ACM. Over a dozen Ph.D. students completed their degrees under her
supervision and obtained positions in some of the best
universities and research labs in the world.
-
The Lean 4 programming language and theorem prover
Leonardo de Moura and David Thrane Christiansen
Abstract: This course offers a hands-on approach to
learning functional programming and formal
verification. Participants will gain practical experience in
writing and proving properties of functional programs using Lean,
a modern functional programming language and theorem prover. For
more information about Lean, please visit lean-lang.org. The
course is designed for both beginners and those with some
functional programming background.
Lean Installation: To prepare for the Lean lectures, please
install Lean using the official instructions at
https://lean-lang.org/lean4/doc/quickstart.html. This
will set up everything you need for the summer school.
If for some reason you can't follow these instructions, please
make sure that the way you install Lean ends up with an
installation of elan, the Lean toolchain version manager, rather
than a specific version of Lean itself (e.g. from nixpkgs). The
installation of elan worked if you can type "lean +4.7.0
--version" in your home directory, and it prints out "Lean
(version 4.7.0, ...)", and typing lean +nightly-2024-05-19
--version" prints something like "Lean (version
4.9.0-nightly-2024-04-19, ...)".
The presentation will mostly be interactive, rather than
slide-based.
Bio: Leo is a Senior Principal Applied Scientist in the
Automated Reasoning Group at AWS. In his spare time, he dedicates
himself to serving as the Chief Architect of the Lean FRO, a
non-profit organization that he proudly co-founded alongside
Sebastian Ullrich. He is also honored to hold a position on the
Board of Directors at the Lean FRO, where he actively contributes
to its growth and development. Before joining AWS in 2023, he was
a Senior Principal Researcher in the RiSE group at Microsoft
Research, where he worked for 17 years starting in 2006. Prior to
that, he worked as a Computer Scientist at SRI International. His
research areas are automated reasoning, theorem proving, decision
procedures, SAT and SMT. He is the main architect of several
automated reasoning tools: Lean, Z3, Yices 1.0 and SAL. Leo’s work
in automated reasoning has been acknowledged with a series of
prestigious awards, including the CAV, Haifa, and Herbrand awards,
as well as the Programming Languages Software Award by the
ACM. Leo’s work has also been reported in the New York Times and
many popular science magazines such as Wired, Quanta, and Nature
News.
Bio: David Thrane Christiansen has worked with functional
programming and dependent types in both academia and industry,
with a particular interest in metaprogramming and domain-specific
languages. He is the author of Functional Programming in Lean and,
together with Daniel P. Friedman, The Little Typer. David works
full-time at the Lean FRO on making the process of writing and
maintaining documentation as easy as possible. Before working at
the Lean FRO, he was the Executive Director of the Haskell
Foundation, and he has multiple years of industrial experience
with functional programming and verification at both Deon Digital
and Galois. Before that, David contributed extensively to the
first version of Idris.
-
Modeling and analyzing reactive systems with logic-based symbolic model checkers
Cesare Tinelli (U. Iowa)
Abstract: The lectures will introduce a language and
verification environment for modeling and statically analyzing a
variety of reactive computational systems such as embedded
systems. The language is an extension of Lustre, a declarative and
synchronous dataflow programming language for reactive
systems. The verification environment is built around the Kind 2
model checker and supports high-level modeling features such as
assume-guaranteed contracts and mode-based specifications, which
enable the modular and compositional verification of
multi-component systems. The lectures will focus on the
specification and verification of safety properties but discuss
also additional kinds of analysis important in industrial
applications such as contract realizability checking, merit
analysis and blame analysis. They will conclude with a general
description of the main automated reasoning techniques used under
the hood to enable such analyses. The labs will provide
opportunities to acquire hands-on experience in modeling and
verifying systems in Kind 2 through a number of exercises of
increasing complexity.
Resources: Kind 2 is open-source software and is available
both in source and precompiled from its
website. The
website includes an online user manual and many example modelss
that can be executed and analyzed online. Additional resources on
the website include a Kind 2 extension for Visual Studio code,
which will be used in the labs, and several technical publications
on the reasoning techniques Kind 2 is based on, or on applications
of Kind 2. Additional materials will be available at the school.
Bio: Cesare Tinelli received a Ph.D. in Computer Science
from the University of Illinois at Urbana-Champaign in 1999 and is
currently a F. Wendell Miller Professor of Computer Science at the
University of Iowa. He is best known for his work in automated
reasoning and verification, in particular in or based on
Satisfiability Modulo Theories (SMT), a field he helped establish
through his research and service activities. He received an NSF
CAREER award in 2003, a Haifa Verification Conference award in
2010 for his role in building and promoting the SMT community, and
a CAV Award in 2021 for his pioneering contributions to the
foundations of the theory and practice of SMT. He is an associate
editor of the Journal of Automated Reasoning and has served in the
program committee of more than 80 automated reasoning and formal
methods conferences and workshops, as well as the steering
committee of CADE, ETAPS, FTP, FroCoS, IJCAR, and SMT. He was the
PC chair of FroCoS'11 and a PC co-chair of TACAS'15 and
CADE-29. He is a founder and coordinator of the SMT-LIB
initiative, an international effort aimed at standardizing
benchmarks and I/O formats for SMT solvers. He has led the
development of the award-winning Darwin theorem prover and the
Kind 1 and Kind 2 model checkers. He has co-led the development of
the widely used and award-winning CVC3 and CVC4 SMT solvers, and
co-leads the development of their successor cvc5.
-
Neurosymbolic Programming for Better Learning
Armando Solar-Lezama (MIT)
Abstract: For decades, programming has been the way we get
computers to do what we want, but in recent years, data driven
approaches have started to provide a different path, the ability
to achieve complex functionality through large data-sets of
examples. But data-driven approaches have a number of limitations
compared to more traditional forms of programming. In particular,
several aspects that make programming so useful: modularity, the
ability to develop software incrementally, or the ability to
establish its correctness for inputs beyond those that were used
to develop it and test it.
In this lecture, I will describe Neurosymbolic Programming, a set
of techniques that combine ideas from programming systems and deep
learning to develop learning systems that combine the benefits of
data-driven learning with some of the features of programming
systems that modern software development relies on.
Bio: Armando Solar-Lezama is Distinguished Professor of
Computing at the MIT Schwarzman College of Computing. He is the
associate director and COO in the Computer Science and Artificial
Intelligence Laboratory, where he leads the Computer Assisted
Programming Group. Solar-Lezama and his research group focus on
program synthesis, a research area at the intersection of
programming systems and artificial intelligence. Solar-Lezama
earned a PhD from University of California, Berkeley.
-
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.
The Formal Methods in the Field Bootcamp will be held following the
summer school from May 29 to the morning of June 2, 2024. This
edition of the FMiTF Bootcamp will be taught by SRI staff with
expertise spanning a range of tools covering static and dynamic
analyzers, code verifiers, SAT/SMT solvers, interactive proof
assistants, and model checkers.
Invited Speakers
-
Applied Category Theory for All?
Valeria de Paiva (Topos Institute, Berkeley)
Abstract: Some might say that Applied Category Theory is a
contradiction in terms. Category Theory is one of the most
abstract branches of pure mathematics, even called by some
mathematicians "abstract nonsense". But exactly because the theory
is so abstract, it can and has been applied in different areas and
from the beginning: math, logic, computer science and many other
subjects. I want to discuss applications to logic and computer
science, some old, some new. This survey is not meant to be
comprehensive, but instead to follow my personal tastes and
interests.
-
Invited Fireside Chat
Chris Lattner
Bio: Chris Lattner is a co-founder and the CEO of
Modular, which is building an innovative new developer platform
for AI and heterogenous compute. Modular provides an AI engine
that accelerates PyTorch and TensorFlow inference, as well as
the Mojo🔥 language, which extends Python into systems and
accelerator programming domains. He has also co-founded the LLVM
Compiler infrastructure project, the Clang C++ compiler, the
Swift programming language, the MLIR compiler infrastructure,
the CIRCT project, and has contributed to many other commercial
and open source projects at Apple, Tesla, Google and SiFive.
Zoom Links
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/
Registration for in-person participation with SSFT24 is now closed.
Applicants are welcome to register for virtual participation.
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 2024 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 April 30,
2024, 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.