Eleventh 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 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

• 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.

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.

Schedule

Logistics

Awards Photos

Previous Summer Schools on Formal Techniques

Information about previous Summer Schools on Formal Techniques can be found at

• SSFT21
• SSFT19
• SSFT18
• SSFT17
• SSFT16
• SSFT15
• SSFT14
• SSFT13
• SSFT12
• SSFT11

Jay Bosamiya of CMU has blogged about the 2018 Summer School at https://www.jaybosamiya.com/blog/2018/05/31/ssft/

Registration

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.