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. Title TBD

Kuldeep Meel, National University of Singapore

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)

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.