Eleventh Summer School on Formal Techniques
May 30 - June 5, 2022
Table of Contents
Lecturers
Speaking Logic
Bootcamp
Invited Speakers
Schedule
Logistics
Previous SSFTs
Registration
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 eleventh 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.
Lectures
-
Symbolic Analysis and its Application to Machine Learning Models
Corina Pasareanu (NASA Ames/CMU West)
Slides:
Symbolic Execution and Probabilistic Reasoning,
SafeDNN
Videos:
Lecture 1,
Lecture 2,
Lecture 3,
Lecture 4,
NeuroSPF Video
Lab Materials:
NeoruSPF Github,
Lab Problem Slides
Abstract: In this lecture we focus on symbolic execution, a systematic
program analysis technique which explores multiple program behaviors by
solving symbolic constraints collected from conditions in the program. The
obtained solutions can be used as test inputs that execute feasible program
paths. Symbolic execution has been used to uncover subtle errors and unknown
vulnerabilities in many software systems. Furthermore, symbolic execution
has been extended with probabilistic reasoning enabling quantitative
checking of software. This probabilistic information can be used for example
to compute the reliability of a controller under different environment
conditions or to quantify information leakage a software system. In this
lecture we review newer applications of symbolic execution and its
probabilistic variant, to the analysis of machine learning models, with
respect to safety, robustness, and fairness properties.
Bio: Corina Pasareanu is doing research in software engineering at NASA
Ames, in the Robust Software Engineering group. She is employed by KBR,
where she is Technical Professional Leader - Data Science. She is also
affiliated with Carnegie Mellon University (CMU), CMU CyLab, CMU Silicon
Valley, and CMU ECE. Her research interests are in formal methods, software
testing, security and machine learning
Abstract: -->
-
Trustworthy Boolean Reasoning
Randy Bryant (CMU)
Lecture 1A: (Un)Satisfiability -
Video 1A,
Lecture 1B: Unsatisfiability Proofs -
Video 1B,
Lecture 2A: Introduction to BDDs -
Video 2A,
Lecture 2B: Proof Generation with BDDs -
Video 2B
Abstract: Like all complex software systems, automated reasoning tools are
prone to bugs. In seeking to maximize their performance, developers may
attempt optimizations that are either unsound or are incorrectly
implemented. These bugs presents challenges for both the developers and the
users, especially when the tools are used for formal verification or to
support mathematical proofs. Some tools have been developed within formal
frameworks that ensure their trustworthiness, but these must often operate
with lower capacity and speed than can be achieved by those implemented with
conventional programming methods. An alternative is to ensure the
trustworthiness of individual executions of the tool by having it produce a
checkable proof of each result. Such a proof provides a detailed,
step-by-step justification expressed in a standard proof framework. A much
simpler proof checker, possibly one that has been formally verified, can
then validate the outcome.
Proof generation has become a standard capability for Boolean
satisfiability (SAT) solvers when they encounter unsatisfiable
formulas. Proof frameworks have been developed to support SAT
solvers based using conflict-driven, clause-learning (CDCL)
algorithms. Recent work has shown that these frameworks can also
be used for proof generation by solvers using ordered binary
decision diagrams (OBDDs) and pseudo-Boolean reasoning. These
approaches can handle classes of problems for which CDCL performs
poorly. We have also incorporated proof generation into an
OBDD-based quantified Boolean formula (QBF) solver, enabling it to
prove that the formula is either true or false.
Bio: Randal E. Bryant is the Founders University Professor of Computer
Science Emeritus at Carnegie Mellon University. He has been on the faculty
there since 1984. Prior to that he received his PhD from MIT and was an
assistant professor at Caltech. He is best known for the development of
Boolean reasoning methods based on Ordered Binary Decision Diagrams (OBDDs).
These have found widespread use in formal verification, design automation,
and reliability analysis. He is a fellow of the IEEE and ACM, and a member
of the National Academy of Engineering.
-
Formal Modeling, Verification, Synthesis, and Learning with UCLID5
Sanjit Seshia (UC Berkeley)
UCLID5
Abstract: The field of formal methods is being impacted by
the confluence of three interesting trends. First, certain classes
of systems, such as trusted hardware-software platforms, motivate
a heterogeneous approach to formal modeling and
specification. Second, algorithmic methods for verification are
being transformed by advances in algorithmic synthesis. Third,
dramatic advances in machine learning are fueling their
integration with more traditional, deductive reasoning
engines. This lecture series will address the challenges and
opportunities presented by this confluence. Specifically, we will
cover approaches to multi-modal modeling of systems, verification
by reduction to synthesis, and integration of inductive learning
with deductive reasoning. These ideas have been implemented in
the open source UCLID5 toolkit, and the tutorial will include
several exercises in UCLID5.
Bio: Sanjit A. Seshia is a Professor in the Department of
Electrical Engineering and Computer Sciences at the University of
California, Berkeley. His research interests are in formal methods
for dependable and secure computing, with a current focus on the
areas of cyber-physical systems, computer security, machine
learning, and robotics. He has made pioneering contributions to
the areas of satisfiability modulo theories (SMT), SMT-based
verification, and inductive program synthesis. He is co-author of
a widely-used textbook on embedded, cyber-physical systems and has
led the development of technologies for cyber-physical systems
education based on formal methods. His awards and honors include a
Presidential Early Career Award for Scientists and Engineers
(PECASE), an Alfred P. Sloan Research Fellowship, the Frederick
Emmons Terman Award for contributions to electrical engineering
and computer science education, the Donald O. Pederson Best Paper
Award for the IEEE Transactions on CAD, the IEEE Technical
Committee on Cyber-Physical Systems (TCCPS) Mid-Career Award, and
the Computer-Aided Verification (CAV) Award for pioneering
contributions to the foundations of SMT solving. He is a Fellow of
the ACM and the IEEE.
-
SMT-based Verification of Heap-manipulating Programs
Ruzica Piskac (Yale University)
Slides:
Lecture 1
Lecture 2 (new)
Videos:
Video 1
Video 2
Video 3
Video 4
Homework
cs454-master.zip
Abstract: The goal of this course is to introduce the
students to the theory and practice of program analysis and
software verification. We will introduce the basic vocabulary of
program verification; students will become familiar with
assertions, pre- and post-conditions, and inductive
invariants. They will learn how to derive mathematical formulas
from the code and annotations (so called "verification
conditions"). We will explore some state-of-the art tools used for
program verification and we will provide more detailed insights
into algorithms and paradigms on which those tools are based such
as SMT solvers and decision procedures. Finally, we will discuss
how to reason about programs that manipulate dynamically allocated
data structures, such as lists or trees.
Bio: Ruzica Piskac is an associate professor of computer
science at Yale University. Her research interests span the areas
of programming languages, software verification, automated
reasoning, and code synthesis. A common thread in Ruzica's
research is improving software reliability and trustworthiness
using formal techniques. Ruzica joined Yale in 2013 as an
assistant professor and professor, and prior to that she was an
independent research group leader at the Max Planck Institute for
Software Systems in Germany. Ruzica has received various
recognitions for research and teaching, including the Patrick
Denantes Prize for her PhD thesis, a CACM Research Highlight
paper, an NSF CAREER award, the Facebook Communications and
Networking award, the Microsoft Research Award for the Software
Engineering Innovation Foundation (SEIF), the Amazon Research
Award, and the 2019 Ackerman Award for Teaching and Mentoring.
-
Neurosymbolic Programming
Mayur Naik (U. of Pennsylvania)
Scallop @SSFT22
Abstract: While deep learning approaches continue to make
strides in domains such as vision and natural language processing,
the logical reasoning ability of such models remains a fundamental
open problem. On the other hand, formal methods and symbolic
reasoning tools are appealing for their completeness and
generalizability. Neurosymbolic methods combine the best of both
worlds by connecting neural models and logical reasoning
programs. In this tutorial, we will introduce a Datalog-based
differentiable logical reasoning engine, Scallop, that can be
integrated with deep neural models like convolutional neural
networks (CNN) and transformers. We will describe how to write
neurosymbolic programs with Scallop that can facilitate better
learning for tasks that involve both perception and reasoning.
Bio: Mayur Naik is Professor and Graduate Chair in the
department of Computer and Information Science at the University
of Pennsylvania. He conducts research in programming languages
and machine learning, with a current focus on programming
abstractions and tools for integrating deep learning and symbolic
reasoning. His past research contributions span the areas of
program analysis, program synthesis, and testing. He holds a
Ph.D. in Computer Science from Stanford University in 2008.
Speaking Logic: Background Course
The main lectures in the summer school will be preceded by a background course on logic
Bootcamp
Bootcamp Problems
Scallop @SSFT22 Bootcamp
SSFT '22: UCLID5 Lab
warm-up.vpr
advanced.vpr
Invited Speakers
-
Reasoning Principles for Verifying Concurrent Search Structures
Thomas Wies (New York University, Courant Institute of
Mathematical Sciences)
Abstract: Search structures support the fundamental data
storage primitives on key-value pairs: insert a pair, delete by
key, search by key, and update the value associated with a
key. Concurrent search structures are parallel algorithms to speed
access to search structures on multicore and distributed
servers. These sophisticated algorithms perform fine-grained
synchronization between threads, making them notoriously difficult
to design correctly. In this talk, I will present a framework for
obtaining correctness proofs for concurrent search structures that
are modular, reusable, and amenable to automation. The framework
takes advantage of recent advances in local reasoning techniques
based on concurrent separation logic. I will provide an overview
of these techniques and demonstrate there use for verifying
realistic search structures such as concurrent B-link trees and
log-structured merge trees.
Bio: Thomas Wies is an Associate Professor in the Computer
Science Department at New York University and a member of the
Analysis of Computer Systems Group in the Courant Institute of
Mathematical Sciences. He is recipient of an NSF CAREER Award, an
OOPSLA 2014 Best Paper Award, and an ISSRE 2019 Distinguished
Paper Award. His research interests are in Programming Languages
and Formal Methods.
-
Computational Social Choice and Incomplete Information
Phokion G. Kolaitis (University of California Santa Cruz and IBM Research)
:
Abstract: Computational social choice is an
interdisciplinary field that studies collective decision making
from an algorithmic perspective. Determining the winners under
various voting rules is a mainstream area of research in
computational social choice. Many such rules assume that the
voters provide complete information about their preferences, an
assumption that is often unrealistic because typically only
partial preference information is available. This situation has
motivated the study of the notions of the necessary winners and
the possible winners with respect to a variety of voting rules.
The main aim of this talk is to present an overview of winner
determination under incomplete information and to highlight some
recent advances in this area, including the development of a
framework that aims to create bridges between computational social
choice and data management. This framework infuses relational
database context into social choice and allows for the formulation
of sophisticated queries about voting rules, candidates, winners,
issues, and positions on issues. We will introduce the necessary
answer semantics and the possible answer semantics to queries and
will explore the computational complexity of query evaluation
under these semantics.
Bio: Phokion Kolaitis is a Distinguished Research Professor
at UC Santa Cruz and a Principal Research Staff Member at the IBM
Almaden Research Center. His research interests include principles
of database systems, logic in computer science, and computational
complexity.
Kolaitis is a Fellow of the American Association for the
Advancement of Science, a Fellow of the Association for Computing
Machinery, and the recipient of a 1993 Guggenheim Fellowship. He
is also a co-winner of both the 2008 and the 2014 ACM PODS Alberto
O. Mendelzon Test-of-Time Award, the 2013 International Conference
on Database Theory Test-of-Time Award, and the 2020 Alonzo Church
Award for Outstanding Contributions to Logic and Computation. At
present, Kolaitis serves as President of the Association for
Symbolic Logic.
-
Set of Support, Demodulation, and Paramodulation: Fundamental
Concepts in Theorem Proving
Maria Paola Bonacina (Università degli Studi di Verona)
Abstract: The ability of distinguishing assumptions and
conjecture, the ability of replacing equals by equals, and the
ability of generating equations from equations, are essential in
theorem proving. By one of those turns in the history of science,
the investigation of these problems began in a short time interval
at the Argonne National Laboratory, around the charismatic figure
of an unsighted scientist, the late Larry Wos, one of the founders
of the field of automated reasoning. Starting from the origins of
these concepts in Larry’s papers, this talk traces their
evolution, unearthing the often forgotten trails that connect
Larry’s original definitions to those that are implemented in
state-of-the-art theorem provers. Along the way, one of the most
fascinating journeys in the history of computer science will
unfold under our eyes.
Bio: Maria Paola Bonacina is Professor of Computer Science
at the Università degli Studi di Verona and International Fellow
at the Computer Science Laboratory of SRI International. Maria
Paola received a Laurea and a Doctorate from the Università degli
Studi di Milano, and a PhD from the State University of New York
at Stony Brook. After postdoc's at the Argonne National Laboratory
and INRIA Lorraine, she started her career at the University of
Iowa, where she was first Assistant Professor and then Associate
Professor of Computer Science, receiving NSF RIA and CAREER awards
and a Dean Scholar Award. She was Visiting Professor at the
Technische Universität Dresden and at the University of
Manchester. Her research area is automated reasoning, including
theorem proving, satisfiability modulo theories, and their
applications. Maria Paola serves regularly on the program
committees of the most important conferences in automated
reasoning. She was elected twice president of the board of
trustees of the Conference on Automated Deduction. Maria Paola
loves reading the classics and history, listening to early and
baroque music, going to theatres and museums, and travelling.
-
Building Trustworthy, Resilient, and Interpretable AI
Susmit Jha (SRI International):
Slides
Abstract: This tutorial will discuss methods for building
trustworthy, resilient, and interpretable AI models by combining
symbolic methods developed for automated reasoning with deep
learning models. The increasing adoption of artificial
intelligence and machine learning in systems, including
safety-critical systems, has created a pressing need for
developing scalable techniques that can be used to establish trust
over their safe behavior, resilience to adversarial attacks, and
interpretability to enable human audits. The tutorial comprises
three components: a review of the techniques for trustworthy deep
learning in formal methods and machine learning literature, a
summary of key challenges and open research problems, and an
overview of the TRINITY-AI system being developed an SRI to
address some of these challenges. Time permitting, we will also
discuss the connection between trustworthy machine learning and
creative AI, and how we can use these techniques to generate the
designs of new cyber-physical systems such as air taxis, UUVs, and
underwater vehicles.
Bio: Susmit Jha is a Principal Scientist in Computer
Science Laboratory at SRI International. His research (
https://nusci.csl.sri.com/ ) focusses on high assurance machine
learning and automatic synthesis of systems. Before joining SRI,
Susmit was a researcher at Raytheon (UTRC) and Intel, and finished
his PhD at UC Berkeley in 2011.
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
Registration for SSFT22 is now closed - check back next year
This year, the school 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. On-site Covid testing will be available. We
have funding from NSF to cover transportation/food/lodging expenses
for selected US-based students. Non-student and non-US in-person
participants will be expected to cover their own transportation and
will be charged a fee for the school to cover the cost of food and
lodging.
The nearest airport to the summer school is SFO. Use Supershuttle
for ground transportation to/from SFO - we should have a discount
code shortly.
