Cesare Tinelli

Many real applications problems can be encoded easily as quantified formulas in SMT. However, this simplicity comes at the cost of difficulty during solving by SMT solvers. Different strategies and quantifier instantiation techniques have been developed to tackle this. However, SMT solvers still struggle with quantified formulas generated by some applications. In this paper, we discuss the use of set-bounded quantifiers, quantifiers whose variable ranges over a finite set. These quantifiers can be implemented using quantifier-free fragment of the theory of finite relations with a filter operator, a form of restricted comprehension, that constructs a subset from a finite set using a predicate. We show that this approach outperforms other quantification techniques in satisfiable problems generated by the SLEEC tool, and is very competitive on unsatisfiable benchmarks compared to LEGOS, a specialized solver for SLEEC. We also identify a decidable class of constraints with restricted applications of the filter operator, while showing that unrestricted applications lead to undecidability.

Lean is an increasingly popular proof assistant based on dependent type theory. Despite its success, it still lacks important automation features present in more seasoned proof assistants, such as the Sledgehammer tactic in Isabelle/HOL. A key aspect of Sledgehammer is the use of proof-producing SMT solvers to prove a translated proof goal and the reconstruction of the resulting proof into valid justifications for the original goal. We present Lean-SMT, a tactic providing this functionality in Lean. We detail how the tactic converts Lean goals into SMT problems and, more importantly, how it reconstructs SMT proofs into native Lean proofs. We evaluate the tactic on established benchmarks used to evaluate Sledgehammer's SMT integration, with promising results. We also evaluate Lean-SMT as a standalone proof checker for proofs of SMT-LIB problems. We show that Lean-SMT offers a smaller trusted core without sacrificing too much performance.

In many applications, SMT solvers are used to solve similar or identical tasks over time. When the performance of the solver varies significantly despite only small changes, this leads to frustration for users. This has been called the stability problem, and it represents an important usability challenge for SMT solvers. In this paper, we introduce an approach for mitigating the stability problem based on normalizing solver inputs. We show that a perfect normalizing algorithm exists but is computationally expensive. We then describe an approximate algorithm and evaluate it on a set of benchmarks from related work, as well as a large set of benchmarks sampled from SMT-LIB. Our evaluation shows that our approximate normalizer reduces runtime variability with minimal overhead and is able to normalize a large class of mutated benchmarks to a unique normal form.

We present a number of first- and second-order extensions to SMT theories
specifically aimed at representing and analyzing SQL queries with join,
projection, and selection operations. We support reasoning about SQL queries
with either bag or set semantics for database tables. We provide the former via
an extension of a theory of finite bags and the latter via an extension of the
theory of finite relations. Furthermore, we add the ability to reason about
tables with null values by introducing a theory of nullable sorts based on an
extension of the theory of algebraic datatypes. We implemented solvers for
these theories in the SMT solver cvc5 and evaluated them on a set of benchmarks
derived from public sets of SQL equivalence problems.

Optimization Modulo Theories (OMT) has emerged as an important extension of
the highly successful Satisfiability Modulo Theories (SMT) paradigm. The OMT
problem requires solving an SMT problem with the restriction that the solution
must be optimal with respect to a given objective function. We introduce a
generalization of the OMT problem where, in particular, objective functions can
range over partially ordered sets. We provide a formalization of and an
abstract calculus for the generalized OMT problem and prove their key
correctness properties. Generalized OMT extends previous work on OMT in several
ways. First, in contrast to many current OMT solvers, our calculus is
theory-agnostic, enabling the optimization of queries over any theories or
combinations thereof. Second, our formalization unifies both single- and
multi-objective optimization problems, allowing us to study them both in a
single framework and facilitating the use of objective functions that are not
supported by existing OMT approaches. Finally, our calculus is sufficiently
general to fully capture a wide variety of current OMT approaches (each of
which can be realized as a specific strategy for rule application in the
calculus) and to support the exploration of new search strategies. Much like
the original abstract DPLL(T) calculus for SMT, our Generalized OMT calculus is
designed to establish a theoretical foundation for understanding and research
and to serve as a framework for studying variations of and extensions to
existing OMT methodologies.

We present a new feature of the open-source model checker Kind 2 which checks
whether a component contract is realizable; i.e., it is possible to construct a
component such that for any input allowed by the contract assumptions, there is
some output value that the component can produce that satisfies the contract
guarantees. When the contract is proven unrealizable, it provides a deadlocking
computation and a set of conflicting guarantees. This new feature can be used
to detect flaws in component specifications and to ensure the correctness of
Kind 2's compositional proof arguments.

CVC4Sy is a syntax-guided synthesis (SyGuS) solver based on bounded term
enumeration and, for restricted fragments, quantifier elimination. The
enumerative strategies are based on encoding term enumeration as an extension
of the quantifier-free theory of algebraic datatypes and on a highly optimized
brute-force algorithm. The quantifier elimination strategy extracts solutions
from unsatisfiability proofs of the negated form of synthesis conjectures. It
uses recent counterexample-guided techniques for quantifier instantiation that
make finding such proofs practically feasible. CVC4Sy implements these
strategies by extending the satisfiability modulo theories (SMT) solver CVC4.
The strategy to be applied on a given problem is chosen heuristically based on
the problem's structure. This document gives an overview of these techniques
and their implementation in the SyGuS Solver CVC4Sy, an entry for SyGuS-Comp
2019.

We introduce the first program synthesis engine implemented inside an SMT
solver. We present an approach that extracts solution functions from
unsatisfiability proofs of the negated form of synthesis conjectures. We also
discuss novel counterexample-guided techniques for quantifier instantiation
that we use to make finding such proofs practically feasible. A particularly
important class of specifications are single-invocation properties, for which
we present a dedicated algorithm. To support syntax restrictions on generated
solutions, our approach can transform a solution found without restrictions
into the desired syntactic form. As an alternative, we show how to use
evaluation function axioms to embed syntactic restrictions into constraints
over algebraic datatypes, and then use an algebraic datatype decision procedure
to drive synthesis. Our experimental evaluation on syntax-guided synthesis
benchmarks shows that our implementation in the CVC4 SMT solver is competitive
with state-of-the-art tools for synthesis.

The use of formal analysis tools on models or source code often requires the
availability of auxiliary invariants about the studied system. Abstract
interpretation is currently one of the best approaches to discover useful
invariants, especially numerical ones. However, its application is limited by
two orthogonal issues: (i) developing an abstract interpretation is often
non-trivial; each transfer function of the system has to be represented at the
abstract level, depending on the abstract domain used; (ii) with precise but
costly abstract domains, the information computed by the abstract interpreter
can be used only once a post fix point has been reached; something that may
take a long time for very large system analysis or with delayed widening to
improve precision.
This paper proposes a new, completely automatic, method to build abstract
interpreters. One of its nice features is that its produced interpreters can
provide sound invariants of the analyzed system before reaching the end of the
post fix point computation, and so act as on-the-fly invariant generators.