Wednesday, July 5th
| 09:00 - 10:00 | Session 1: Invited Talk | chair: Mathias Preiner |
| 09:00 - 10:00 | Invited Talk: Deductive Verification of Distributed Protocols in Decidable Logics
Verification of distributed protocols and systems, where both the
number of nodes in the systems and the state-space of each node are
unbounded, is a long-standing research goal. In recent years, efforts
around the Ivy verification tool have pushed a strategy of modeling
distributed protocols and systems in a new way that enables decidable
deductive verification, i.e., given a candidate inductive invariant,
it is possible to automatically check if it is inductive, and to
produce a finite counterexample to induction in case it is not
inductive. Complex protocols require quantifiers in both models and
their invariants, including forall-exists quantifier
alternations. Still, it is possible to obtain decidability by
enforcing a stratification structure on quantifier alternations, often
achieved using modular decomposition techniques. Stratified
quantifiers lead not only to theoretical decidability, but to reliable
solver performance in practice, which is in contrast to the typical
instability of SMT solvers over formulas with complex
quantification. Moreover, reliable automation of invariant checking
and finite counterexamples open the path to automating invariant
inference. Recently, several invariant inference algorithms have been
developed that can find complex quantified invariants for challenging
distributed protocols.
In this talk I will provide an overview of Ivy's principles and
techniques for modeling distributed protocols in a decidable fragment
of first-order logic. I will also draw on the experience with Ivy and
related tools to offer some lessons learned and open questions
relevant to the SMT community.
|
|
| 10:00 - 10:30 | Coffee Break | |
| 10:30 - 12:30 | Session 2: Quantifiers, SAT, OMT | chair: Sophie Tourret |
| 10:30 - 11:00 |
Complete Trigger Selection in Satisfiability modulo First Order Theories
(original paper)
[slides]
Let T be an SMT solver with no theory solvers except for Quantifier
Instantiation. Given a set of first order clauses S saturated by
Resolution (with a valid literal selection rule) we show that T is
complete if its Trigger function is the same as the literal selection
rule. So if T halts with a ground model G, then G is a model in the
theory of S. In addition for a suitable ordering, if all maximal
literals are selected in each clause, then T will halt on G, so it is
a decision procedure for the theory S. Also, for a suitable ordering,
if all clauses are Horn, or all clauses are 2SAT, then T solves the
theory S in polynomial time.
|
|
| 11:00 - 11:30 |
Selecting Quantifiers for Instantiation in SMT (extended abstract) [slides]
This work attempts to choose quantifiers to instantiate based on
feedback from the SMT solver. This tackles the challenge that if a
problem contains many quantifiers ex- impressions, it eventually gets
flooded by too many generated ground terms. Therefore, we instantiate
only some of the quantifiers but the question is, which are the
useful ones?
The SMT solver is modeled as a multi-armed bandit, where each
quantifier is a lever producing a positive reward if an instantiation
of the quantifier is useful. The issue is that we do not know whether
an instantiation was useful or not until the given problem instance
is actually proven (and then it’s too late). In this paper, we
explore several heuristics that attempt to assess the usefulness of
quantifier instantiations.
|
|
| 11:30 - 12:00 |
IPASIR-UP: User Propagators for CDCL (presentation only)
Modern SAT solvers are frequently embedded as sub-reasoning engines
into more complex tools for addressing problems beyond the Boolean
satisfiability problem. Examples include solvers for Satisfiability
Modulo Theories (SMT), combinatorial optimization, model enumeration
and counting. In such use cases, the SAT solver is often able to
provide relevant information beyond the satisfiability answer.
Further, domain knowledge of the embedding system (e.g., symmetry
properties or theory axioms) can be beneficial for the CDCL search,
but cannot be efficiently represented in clausal form.
In this paper, we propose a general interface to inspect and
influence the internal behaviour of CDCL SAT solvers. Our goal is to
capture the most essential functionalities that are sufficient to
simplify and improve use cases that require a more fine-grained
interaction with the SAT solver than provided via the standard IPASIR
interface. For our experiments, we extend CaDiCaL with our interface
and evaluate it on two representative use cases: enumerating graphs
within the SAT modulo Symmetries framework (SMS), and as the main
CDCL(T) SAT engine of the SMT solver cvc5.
|
|
| 12:00 - 12:30 |
An Abstract Calculus for Optimization Modulo Theories (presentation only)
Optimization Modulo Theories (OMT) has emerged as an important
extension of the highly-successful Satisfiability Modulo Theories
(SMT) paradigm. An OMT problem solves an SMT problem, but with the
addition of an objective function that must be optimized. We
introduce a novel abstract calculus for the OMT problem and prove its
correctness. The calculus generalizes previous approaches in several
ways. First, it is not specific to any theory or optimization
technique, making it easily applicable to new theories or objective
functions. Second, it unifies single- and multi-objective
optimization problems, allowing both to be managed within a single
framework. Finally, it is sufficiently general to capture a variety
of heuristics (e.g., linear search, binary search). Such heuristics
are realized as specific strategies for applying the rules in the
calculus.
|
|
| 12:30 - 14:00 | Lunch Break | |
| 14:00 - 15:30 | Session 3: SMT Applications and SMT-COMP | chair: Aina Niemetz |
| 14:00 - 14:30 |
Automated Analysis of Halo2 Circuits (original paper) [slides]
Zero-knowledge proof systems are becoming increasingly prevalent and
being widely used to secure decentralized financial systems and
protect the privacy of users. Given the sensitivity of these
applications, zero-knowledge proof systems are a natural target for
formal verification methods. We describe methods for checking one
such proof system: Halo2. We use abstract interpretation and an SMT
solver to check various properties of Halo2 circuits. Using abstract
interpretation, we can detect unused gates, unconstrained cells, and
unused columns. Using an SMT solver, we can detect under-constrained
(in the sense that for the same public input they have two satisfying
assignments) circuits. This is the first work we are aware of that
applies lightweight formal methods to PLONKish arithmetization and
Halo2 circuits. We conclude by outlining future directions for
researc
|
|
| 14:30 - 15:00 |
Application of SMT in a Meta-Compiler: A Logic DSL for Specifying Type Systems (extended abstract) [slides]
Building a compiler for a programming language is a notoriously hard
task, especially when starting from scratch. That’s why we developed
Langkit, a meta-compiler which allows language designers to focus on
the high-level aspects of their language. In particular, the
specification of type systems is done in a declarative manner by
writing equations in a high-level logic DSL. Those equations are then
resolved by a custom solver embedded in the generated compiler
front-end whenever a code fragment of the target language needs to be
analyzed. This framework is successfully used at AdaCore to implement
name and type resolution of Ada, powering navigation in IDEs and
enabling development of deep static analysis tools.
We discuss the implementation of our solver, and how a recent switch
to using a DPLL(T) solver backend with a custom theory allowed us
both to address long-standing combinatorial explosion problems we had
with our previous approach, but also to gain new insights in how to
emit human-readable diagnostics for type errors.
|
|
| 15:00 - 15:30 | Discussion on Future of SMT-COMP | |
| 15:30 - 16:00 | Coffee Break | |
| 16:00 - 17:45 | Session 4: SMT-LIB and SMT Business Meeting | chair: Mathias Preiner |
| 16:00 - 16:45 |
SMT-LIB Report |
|
| 16:45 - 17:45 | Business Meeting | |
Thursday, July 6th
| 09:00 - 10:00 | Session 1: Invited Talk | chair: Stéphane Graham-Lengrand |
| 09:00 - 10:00 | Invited Talk: SAT and SMT solving at Cloud Scale
Amazon Web Services (AWS) is a cloud computing services provider that
has made significant investments in automated reasoning to check the
correctness of its internal systems and to provide assurances to
customers. We are using SAT and SMT solvers more than one billion
times a day, both for "real-time" queries in customer security
(checking security policies and verifying network protections), and
also for large queries involving code and hardware reasoning that are
at the limits of what can be feasibly solved by current solvers.
Supporting reasoning at this scale and volume requires careful
examination of the problems to be solved and a clear focus on
operations to ensure our analyses are consistently trustworthy and
performant. I will describe some lessons learned and offer some
directions for the community that should allow us to scale further,
increase trust, and solve the next billion queries a day.
|
|
| 10:00 - 10:30 | Coffee Break | |
| 10:30 - 12:30 | Session 2: SMT Theories and Solving | chair: Jochen Hoenicke |
| 10:30 - 11:00 |
Satisfiability Modulo Finite Fields (presentation only)
We study satisfiability modulo the theory of finite fields and give a
decision procedure for this theory. We implement our procedure for
prime fields inside the cvc5 SMT solver. Using this theory, we
construct SMT queries that encode translation validation for various
zero knowledge proof compilers applied to Boolean computations. We
evaluate our procedure on these benchmarks. Our experiments show that
our implementation is superior to previous approaches (which encode
field arithmetic using integers or bit-vectors).
|
|
| 11:00 - 11:30 |
Exploiting Strict Constraints in the Cylindrical Algebraic Covering (original paper) [slides]
One of the few available complete methods for checking the
satisfiability of sets of polynomial constraints over the reals is
the cylindrical algebraic covering (CAlC) method. In this paper, we
propose an extension for this method to exploit the strictness of
input constraints for reducing the computational effort. We
illustrate the concepts on a multidimensional example and provide
experimental results to evaluate the usefulness of our proposed
extension.
|
|
| 11:30 - 12:00 |
Reasoning About Vectors using an SMT Theory of Sequences (presentation only) [slides]
Dynamic arrays, also referred to as vectors, are fundamental data
structures used in many programs. Modeling their semantics
efficiently is crucial when reasoning about such programs. The theory
of arrays is widely supported but is not ideal, because the number of
elements is fixed (determined by its index sort) and cannot be
adjusted, which is a problem, given that the length of vectors often
plays an important role when reasoning about vector programs.
In this paper, we propose reasoning about vectors using a theory of
sequences. We introduce the theory, propose a basic calculus adapted
from one for the theory of strings, and extend it to efficiently
handle common vector operations. We prove that our calculus is sound
and show how to construct a model when it terminates with a saturated
configuration. Finally, we describe an implementation of the calculus
in cvc5 and demonstrate its efficacy by evaluating it on verification
conditions for smart contracts and benchmarks derived from existing
array benchmarks.
|
|
| 12:00 - 12:30 |
Partitioning Strategies and Partitioning Portfolios for Parallel SMT Solving (presentation only)
For many users of Satisfiability Modulo Theories (SMT) solvers, the
solver's performance is the main bottleneck in their application. One
promising approach for improving performance is to leverage the
increasing availability of parallel and cloud computing. However,
despite many efforts, the best parallel approach to date consists of
running a portfolio of sequential solvers, meaning that performance
is still limited by the best possible sequential performance. In this
paper, we revisit divide-and-conquer approaches to parallel SMT, in
which a challenging problem is partitioned into several subproblems.
We introduce several new algorithms for partitioning and evaluate
them, as well as portfolios including them, on a large set of
difficult SMT benchmarks. We show that mixed portfolios including our
new divide-and-conquer approaches can significantly outperform
traditional portfolios for parallel SMT.
|
|
| 12:30 - 14:00 | Lunch Break | |
| 14:00 - 15:30 | Session 3: Proofs, Certificates, and Models | chair: Yoni Zohar |
| 14:00 - 14:30 |
Automatic Verification of SMT Rewrites in Isabelle/HOL (presentation only) [slides]
Satisfiability modulo theories (SMT) solvers are widely used to
ensure the correctness of safety- and security- critical
applications. Therefore, being able to trust a solver’s results is
crucial. One way to increase trust is to generate proof certificates,
which record the reasoning steps the solver has done. These proof
certificates can be given to a proof checker which determines whether
the steps in the proof are correct. One key challenge with this
approach is that it is difficult to efficiently and accurately
produce proofs for reasoning steps involving term rewriting rules (of
which there are many in modern SMT solvers). Previous work showed how
a domain-specific language, RARE, can be used to capture rewriting
rules for the purposes of proof production. However, the RARE rules
were trusted—i.e., the correctness of the rules themselves was not
checked by the proof checker. In this paper, we present IsaRARE, a
tool that can automatically generate lemmas in the interactive
theorem prover Isabelle/HOL corresponding to RARE rewrite rules. The
correctness of the rules can then be verified by proving the lemmas.
We evaluate our approach by verifying an extensive set of rewrite
rules used by the cvc5 SMT solver.
|
|
| 14:30 - 15:00 |
Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem (presentation only)
For typical first-order logical theories, satisfying assignments have
a straightforward finite representation that can directly serve as a
certificate that a given assignment satisfies the given formula. For
non-linear real arithmetic with transcendental functions, however, no
general finite representation of satisfying assignments is available.
Hence, in this paper, we introduce a different form of satisfiability
certificate for this theory, formulate the satisfiability
verification problem as the problem of searching for such a
certificate, and show how to perform this search in a systematic
fashion. This does not only ease the independent verification of
results, but also allows the systematic design of new, efficient
search techniques. Computational experiments document that the
resulting method is able to prove satisfiability of a substantially
higher number of benchmark problems than existing methods.
|
|
| 15:00 - 15:30 |
Verifying Models with Dolmen (extended abstract)
Dolmen provides tools to parse, type, and validate input files used
in automated deduction, and in particular problems from the SMT-LIB.
We present here an extension of Dolmen which makes it capable of
verifying ground models for quantifier-free SMT-LIB problems. While
most of the extension was a straightforward implementation of an
evaluator for ground expressions, there were some challenges, related
to corner cases of the semantics (division by zero, partial
functions, ...), as well as order of evaluation of statements,
most of which could be solved by improvements to the SMT-LIB standard
for models.
|
|
| 15:30 - 16:00 | Coffee Break | |
| 16:00 - 17:00 | Session 4: SMT-COMP | chair: Stéphane Graham-Lengrand |
| 16:00 - 17:00 | SMT-COMP Results and Tool Presentations [slides] | |