Invited Talks and Tutorials

Invited Talks:

1. Reasoning about quantifiers in SMT: the QSMA algorithm

Maria Paola Bonacina, Università degli Studi di Verona

ABSTRACT: Automated reasoning is a key enabling technology for formal methods. Automated theorem provers (ATP) for first-order and lately higher-order logic and solvers for satisfiability modulo theories (SMT) showcase impressive power and amazing sophistication. However, ATP systems reason well about formulas with arbitrary quantification and free symbols, while SMT solvers reason well about ground formulas with defined symbols. Since formulas from applications involve both quantifiers and defined symbols, a hiatus remains open. QSMA is a new algorithm for quantifiers in SMT. QSMA stands for Quantified Satisfiability Modulo theory and Assignment. Currently, QSMA works for one theory with a unique intended model, so that models differ only in the assignment of values to variables. QSMA accepts arbitrary formulas, viewing all quantifiers as existential by double negation. Since QSMA operates a recursive descent over the tree structure of the formula, peeling off quantifiers and instantiating variables, each call works modulo an assignment. By building under- and over- approximations of the formula, QSMA zooms in on a model or finds that none exists. The implementation of QSMA in the YicesQS solver built on top of the Yices 2 solver exhibited excellent performances in linear rational arithmetic and nonlinear arithmetic. Integrating QSMA in the CDSAT framework for conflict-driven satisfiability in a union of theories is the next challenge.

(QSMA is joint work with Stéphane Graham-Lengrand and Christophe Vauthier. YicesQS is the work of Stéphane Graham-Lengrand. Yices 2 is the work of Bruno Dutertre and Dejan Jovanovic. CDSAT is joint work with Stéphane Graham-Lengrand and Natarajan Shankar.)

BIO: Maria Paola Bonacina is Professor of Computer Science at the Università degli Studi di Verona, where she conducts research in automated reasoning, including theorem proving, SMT, and their applications. Her many contributions include the CDSAT framework for SMT and the SGGS method for first-order theorem proving. Her research has been funded by Italian and EU agencies, and lately by an Amazon Research Award. Maria Paola visits regularly SRI International, and she was Visiting Research Scholar at the Isaac Newton Institute (University of Cambridge) and at Microsoft Research Redmond. She was also Visiting Professor at the University of Manchester and at TU Dresden. Prior to joining U. Verona, Maria Paola was first Assistant Professor and then Associate Professor at the University of Iowa, where she received NSF RIA and CAREER Awards and a Dean Scholar Award. Her education includes Laurea and Doctorate from the Università degli Studi di Milano, then a PhD from the State University of New York at Stony Brook, followed by postdoc’s at the Argonne National Laboratory and at INRIA Lorraine. Maria Paola loves reading the classics and history, listening to early and baroque music, going to theatres and museums, and travelling.

2. Distribution Testing: The New Frontier for Formal Methods

Kuldeep Meel, University of Toronto

ABSTRACT: The dominant guiding philosophy in the first sixty years of Computer Science was for designers to design systems that were always correct, and to accept nothing less as users. But times have changed: Users and designers are accustomed to systems with statistical components and behaviors. What does it mean for the formal methods community?

In this talk, we argue that such a dramatic change in the acceptance and design of systems presents exciting opportunities to make fundamental contributions: we need to rethink the notions and techniques for the design of specifications and verification methodologies. In particular, we will focus on the systems whose behaviors are not naturally captured by symbolic relations but rather require reliance on probability distributions. We will discuss our recent efforts in designing formal methodologies for testing whether a sampling subroutine generates a desired distribution. We will showcase the challenges, opportunities, and rewards in our journey.

BIO: Kuldeep Meel is an Associate Professor of Computer Science in the Department of Computer Science at the University of Toronto. His research interests lie at the intersection of Formal Methods and Artificial Intelligence. He is a recipient of the 2022 ACP Early Career Researcher Award, IJCAI-21 Early Career Spotlight, the 2019 NRF Fellowship for AI, and was named AI’s 10 to Watch by IEEE Intelligent Systems in 2020. His research program’s recent recognitions include the 2023 CACM Research Highlight Award, CAV-22 Distinguished Paper Award, DATE-23 Best Paper Award Nomination, 2022 ACM SIGMOD Research Highlight, ICCAD-21 Best Paper Award nomination, 1st Place in Model Counting Competition (2020, 2022 and 2023).

3. Formal Methods for Trusted AI

Bettina Könighofer, TU Graz

ABSTRACT: The enormous influence of systems deploying AI is contrasted by the growing concerns about their safety and the relative lack of trust by the society. This talk will focus on a few aspects of trustworthy AI: safety, accountability, and explainability. First, we will discuss recent work on evaluating safety for systems deploying deep learning, and correct-by-construction runtime assurance methods to enforce safety during runtime (aka shielding). For accountability, we outline the potential of formal computing tools to analyse the decisions of autonomous agents and to assign responsibility. Finally, we approach explainability from the automata learning perspective. We will discuss recent automata learning approaches which are able to learn compact probabilistic models for high-dimensional environments and outline how learned environmental models can effectively be used to understand and to evaluate the decisions of the agent.

BIO: Bettina Könighofer is assistant professor of Formal Methods and Machine Learning at Graz University of Technology. Bettina’s research interests lie primarily in the area of reinforcement learning, model checking, and runtime monitoring and enforcement. Bettina’s work on shielding was one of the first that combined correct-by-construction runtime enforcement techniques with AI, bootstrapping the line of research on shielded learning. Bettina received the PhD degree from TU Graz under the supervision of Prof. Roderick Bloem in 2020. Before starting assistant professor in 2023, she led the TurstedAI group at Lamarr Security Research.

Tutorials:

1. Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community

The NSF:CCRI Project Investigators (Rozier, Shankar, Tinelli, Vardi)

ABSTRACT: As model checking becomes more integrated into the standard design and verification process for safety-critical systems, the platforms for model checking research have become more limited. Previous options have become closed-source or industry tools; current research platforms don’t have support for expressive specification languages needed for verifying real systems. Our goal is to fill the current gap in model checking research platforms: building a freely-available, open-source, scalable model checking infrastructure that accepts expressive models and efficiently interfaces with the currently-maintained state-of-the-art back-end algorithms to provide an extensible research and verification tool. With extensive involvement from the research community, we have been creating a community resource with a well-documented intermediate representation to enable extensibility, and a web portal, facilitating new modeling languages and back-end algorithmic advances. To add new modeling languages or algorithms, researchers need only to develop a translator to/from the new intermediate language, and will then be able to integrate each advance with the full state-of-the-art in model checking. This tutorial will include an overview of the model checking intermediate language semantics and demonstrations of (provably correct) translators to and from that representation.

BIO: Though the need for a unifying framework for model-checking algorithms, tools, and future research has been growing for many years, this project was funded by the US National Science Foundation (NSF) in 2020. This tutorial presents the results-so-far from the collaborative effort supported by NSF’s CISE Community Research Infrastructure (CCRI) program, which aims to develop sustainable, robust, and innovative science and engineering infrastructures through research community involvement and leadership.

The NSF grant team consists of Kristin Yvonne Rozier (principal investigator, Iowa State University), Natarajan Shankar (SRI), Cesare Tinelli (University of Iowa), and Moshe Y. Vardi (Rice University). Though the talk will be delivered by three of the proposal’s investigators (Rozier, Tinelli, and Shankar), the materials presented include work by many students, members of the international technical advisory board, and research community members.

2. MiniZinc for Formal Methods

Peter J. Stuckey

ABSTRACT: MiniZinc is a free and open-source constraint modeling language, designed for solving discrete optimisation problems. You can use MiniZinc to model constraint satisfaction and optimization problems in a high-level, solver-independent way, taking advantage of a large library of pre-defined constraints encapsulting different combinatorial substructures of the problem. Your model is then compiled into FlatZinc, a solver input language that is understood by a wide range of solvers including leading CP solvers such as OR-tools from Google, and CP-optimiser from IBM, and leading MIP solvers such as Gurobi and Cplex.

MiniZinc is useful for Formal Reasoning problems where we reason about a bounded size problem on discrete objects (including integers). In this tutorial we will give an introduction to MiniZinc focusing, at least in the latter part, on where it can be applied to Formal Methods problems. Formal methods modelling through MiniZinc leads to different ways to model things such as state progression, and can take advantage of combinatorial substructures that occur in such problems, such as injective mappings. Overall MiniZinc gives an alternate, and often highly competitive, approach to using SMT for answering some kinds of formal reasoning questions.

BIO: Professor Peter J. Stuckey is a Professor in the Department of Data Science and Artificial Intelligences in the Faculty of Information Technology at Monash University. Peter Stuckey is a pioneer in constraint programming, the science of modelling and solving complex combinatorial problems. His research interests include: discrete optimization; programming languages, in particular declarative programing languages; constraint solving algorithms; path finding; bioinformatics; and constraint-based graphics. He enjoys problem solving in any area, having publications in e.g. databases, election science, system security, and timetabling, and working with companies such as Oracle and Rio Tinto on problems that interest them. In 2019 he was elected as an AAAI Fellow and awarded the Association of Constraint Programming Award for Research Excellence.

3. Local Search and Its Application in CDCL/CDCL(T) solvers for SAT/SMT

Shaowei Cai

ABSTRACT: Modern SAT solvers are based on a paradigm named conflict driven clause learning (CDCL), and CDCL(T) remains the main method for SMT. Local search is an important alternative for satisfiable instances, which has witnessed significant progress in SAT, and has begun to show promising results in SMT. Furthermore, recent techniques integrating local search into CDCL have brought significant improvements, and local search is widely used in state of the art CDCL solvers as an important component. Similar results have also been observed in CDCL(T). This talk will introduce state of the art local search methods for SAT and SMT, and also present the recent techniques of combining local search and CDCL/CDCL(T).

BIO: Shaowei Cai is a Professor at Institute of Software, Chinese Academy of Sciences. He received his PhD degree from Peking University with Distinguished Doctoral Dissertation Award. His research interests include satisfiability solving and combinatorial optimization. Particularly, he developed efficient local search solvers for SAT/SMT/MaxSAT, and proposed a powerful hybrid approach for SAT, which has been used in state of the art CDCL solvers. He has received the Best Paper Award at SAT 2021 conference. He has won more than 10 gold medals in SAT and SMT Competitions, and his solvers were ranked 1st many times in MaxSAT Evaluations.

4. NASA’s core Flight System Framework Overview / Tutorial

David Swartwout

ABSTRACT: The core Flight System (cFS) is a platform and project independent reusable software framework and set of reusable software applications. There are three key aspects to the cFS architecture: a dynamic run-time environment, layered software, and a component-based design. It is the combination of these key aspects that makes it suitable for reuse on any number of flight projects and/or embedded software systems at a significant cost and schedule savings. This tutorial will give a brief overview of the architecture and demonstrate a simple app development and deployment.

BIO: David Swartwout graduated from Texas A&M University with a degree in Computer Engineering and began his career developing Mission Control Center software for NASA. Over the years he has lead teams developing increasingly complex and higher profile software systems for a variety of NASA missions across the International Space Station, the Orion Program, and now the Gateway outpost under the Artemis program. He has twice received the NASA Exception Engineering Achievement Medal for his project leadership. He currently serves as the Gateway Production Software Lead for NASA’s Artemis Gateway Program. Over the years he has led several large core Flight System (CFS) based development programs for NASA, including the Morpheus Lander and the Orion Ascent Abort 2 mission.