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 twelfth 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.
This year, 2023, we celebrate the 60th anniversary of Alan
Robinson's first publication on Resolution, and are delighted to
have a series of lectures devoted to the latest developments in this
important strand of automated reasoning. The summer school will be
immediately followed by a Formal Methods in the Field (FMiTF)
Bootcamp. 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.
Lectures
-
No More Garbage In: Validating Formal Models
Pamela Zave (Princeton) and Tim Nelson (Brown)
References
Lecture 1
Lecture 2
Abstract: One of the oldest and truest maxims about
programming is "Garbage in, garbage out." In this course we apply
the maxim to formal models and verification tools. The goal is to
help students compare their formal models to the real world they
are supposed to describe, and by doing so, ensure that the results
of formal verification also describe the real world. Lectures and
labs explain how verification tools can help this inherently
informal process, and how to avoid mistakes even the experts can
make.
Bio: Pamela Zave is a researcher with the Computer Science
Department of Princeton University, having held previous positions
at the University of Maryland, Bell Labs, and AT&T Labs. She is
an ACM Fellow, an IFIP Fellow, an AT&T Fellow, and the 2017
recipient of the IEEE Harlan D. Mills Award for sustained
contributions to the theory and practice of software engineering.
She now works on the application of formal methods to networking,
and is an author of the forthcoming book "The Real Internet
Architecture: Past, Present, and Future Evolution."
Bio: Tim Nelson is a lecturer at Brown University who works
on human-facing formal methods and formal-methods education.
Among other courses, he teaches Brown University's Logic for
Systems, where students put concrete, logic-based tools (such as
model finders, model checkers, and proof assistants) to work on
problems in their own domain. Tim got his PhD at Worcester
Polytechnic Institute, where he worked on lightweight formal
methods for security policy analysis (the Margrave tool). At
Brown, he has done research on network programming, improving
formal-methods tool output, property-based testing, and
configuration synthesis. He finds any application of formal
methods interesting, and is looking forward to learning a lot
together this summer.
-
First-Order Theorem Proving
Laura Kovacs (TU Wien) and Andrei Voronkov (Manchester)
First-Order Theorem Proving and VAMPIRE
Slides
Exercises
Vampire Cookies
Exercises with Solutions
Abstract: First-order theorem proving is one of the
earliest research areas within artificial intelligence and formal
methods. It is undergoing a rapid development thanks to its
successful use in program analysis and verification, security
analysis, symbolic computation, theorem proving in mathematics,
and other related areas. This tutorial will provide a series of
four lectures introducing the audience to first-order theorem
proving. The workhorse used for a demonstration of concepts
discussed at the tutorial will be our award-winning theorem prover
Vampire.
The tutorial will be split in four lecture. The first lecture
immediately helps the audience place the work in context by
introducing them to an application of theorem proving in Vampire
for validating mathematical theorems. The next three lectures
introduce the core concepts of automating first-order theorem
proving in first-order logic with equality. We will introduce
the saturation principle and present various algorithms
implementing redundancy elimination (lecture two). We will
discuss the resolution and superposition calculus for effective
reasoning in first-order logic with equality (lecture three).
We will then also present practical considerations on using
superposition in practice (lecture four), highlighting also
further challenges in this area.
Bio: Laura Kovacs is a full professor of computer science at
the TU Wien, leading the automated program reasoning (APRe) group
of the Formal Methods in Systems Engineering division. Her
research focuses on the design and development of new theories,
technologies, and tools for program analysis, with a particular
focus on automated assertion generation, symbolic summation,
computer algebra, and automated theorem proving. She is the
co-developer of the Vampire theorem prover and a Wallenberg
Academy Fellow of Sweden. Her research has also been awarded with
a ERC Starting Grant 2014, an ERC Proof of Concept Grant 2018, an
ERC Consolidator Grant 2020, and an Amazon Research Award 2020.
Bio: Andre Voronkov is Professor of Formal Methods at the
University of Manchester and Visiting Professor at Vienna
University of Technology. He is the designer and founder of
EasyChair, the main designer of the theorem prover Vampire, and
the founder of the LPAR conference series. Vampire is the
winner of numerous theorem proving competitions. In 2015,
Andrei received the Herbrand Award for Distinguished
Contributions to Automated Reasoning.
-
The TPTP World - Infrastructure for Automated Reasoning
Geoff Sutcliffe (Miami)
Abstract: The TPTP World is a well known and established
infrastructure that supports research, development, and deployment
of Automated Theorem Proving (ATP) systems for classical
logics. The data, standards, and services provided by the TPTP
World have made it increasingly easy to build, test, and apply ATP
technology. This talk and tutorial reviews the core features of
the TPTP World, describes key service components of the TPTP World
and how to use them, and presents some successful applications.
TPTP
Lecture Notes
Lab Materials
Lecture 1: The TPTP World, TPTP language, TPTP World
infrastructure, SystemOnTPTP
Lab 1: Encoding and solving problems in the TPTP World - propositional,
first-order, typed first-order.
Lecture 2: Inner workings of some of the TPTP tools, ATP applications,
ATP process.
Lab 2: Encoding and solving problems in the TPTP World - typed extended
first-order, higher-order, modal and epistemic.
-
Reactive Systems: A Powerful Paradigm for Modeling and Analysis
from Engineering to Biology
Tom Henzinger (IST Austria)
-
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
PVS Mac (strings branch)
PVS Linux (strings branch)
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, 2023. 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
-
Resolution, Unification, and Subsumption: Fundamental Concepts in
Theorem Proving
Maria Paola Bonacina, Università degli Studi di Verona
Slides
-
Q & A on Paxos
Leslie Lamport
-
Language Model Software and the Future of Verified Programming
Jesse Michael Han (OpenAI)
:
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.
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).
Participants can register separately for the school and the
bootcamp.
Applicants are urged to submit their applications before April 30,
2023, 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.