All times are for Los Angeles, USA, which observes PDT (UTC7).
The CAV21 Platform is now live at http://cav21.org/.
The schedule and all links (Zoom, Slack, Gather) are available on the platform's workshop page.
You will need to activate your conference registration account to login.
Sunday, 20210718
08:00  09:00  Session 1: Invited Talk  chair: Aina Niemetz 
08:00  09:00  Invited Talk: Using SMT and AbstractionRefinement for Neural Network Verification
Deep neural networks are increasingly being used as controllers for
safetycritical systems. Because neural networks are opaque,
certifying their correctness is a significant challenge. To address
this issue, several neural network verification approaches have
recently been proposed, many of them based on SMT solving. However,
these approaches afford limited scalability, and applying them to
large networks can be challenging. In this talk we will discuss a
framework that can enhance neural network verification techniques by
using overapproximation to reduce the size of the network  thus
making it more amenable to verification. This approximation is
performed such that if the property holds for the smaller (abstract)
network, it holds for the original as well. The overapproximation
may be too coarse, in which case the underlying verification tool
might return a spurious counterexample. Under such conditions, we can
perform counterexampleguided refinement to adjust the approximation,
and then repeat the process. This approach is orthogonal to, and can
be integrated with, many existing verification techniques. For
evaluation purposes, we integrate it with the recently proposed
Marabou framework, and observe a significant improvement in Marabou's
performance. Our experiments demonstrate the great potential of
abstractionrefinement for verifying larger neural networks.


09:00  09:30  Session 2: Theory of SMT  chair: Martin Jonas 
09:00  09:15 
The Extended Theory of Trees and Algebraic (Co)datatypes
paper at VPT/HCVS 2020
(presentation only)
video
The firstorder theory of algebraic datatypes (and codatatypes) is
an important theory implemented in many SMT solvers. It is related
to the theory of finite and infinite trees, which has been studied
since the eighties, especially by the logic programming community.
Following Djelloul, Dao and Frühwirth, we consider an extension of
the latter theory with an additional predicate for finiteness of
trees, which is useful for expressing properties about (not just
datatypes but also) codatatypes. Based on their work, we present a
simplification procedure that determines whether any given (not
necessarily closed) formula is satisfiable, returning a simplified
formula which enables one to read off all possible models. Our
extension makes the algorithm usable for algebraic (co)datatypes,
which was impossible in their original work due to restrictive
assumptions. To this end, we clarify the relationship between the
two theories and describe a translation procedure. We find that
trees are in some ways more expressive than (co)datatypes while
preserving decidability, which makes them interesting for SMT
applications. We also provide a prototype implementation of our
simplification procedure and evaluate it on instances from the
SMTLIB.


09:15  09:30 
Politeness and Stable Infiniteness: Stronger Together paper at CADE 2021 (presentation only) video
We make two contributions to the study of polite combination in
satisfiability modulo theories. The first is a separation between
politeness and strong politeness, by presenting a polite theory
that is not strongly polite. This result shows that proving strong
politeness (which is often harder than proving politeness) is
sometimes needed in order to use polite combination. The second
contribution is an optimization to the polite combination method,
obtained by borrowing from the NelsonOppen method. The NelsonOppen
method is based on guessing arrangements over shared variables. In
contrast, polite combination requires an arrangement over all
variables of the shared sorts. We show that when using polite
combination, if the other theory is stably infinite with respect to
a shared sort, only the shared variables of that sort need be
considered in arrangements, as in the NelsonOppen method. The time
of reasoning about arrangements is exponential in the worst case,
so reducing the number of variables considered has the potential to
improve performance significantly. We show preliminary evidence for
this by demonstrating a speedup on a smart contract verification
benchmark.


09:30  09:45  Break  
09:45  10:45  Session 3: Proofs and Interpolation  chair: Stéphane GrahamLengrand 
09:45  10:00 
Reliable Reconstruction of FineGrained Proofs in a Proof Assistant paper at CADE 2021 (presentation only) video
We present a fast and reliable reconstruction of proofs generated
by the SMT solver veriT in Isabelle. The finegrained proof format
makes the reconstruction simple and efficient. For typical proof
steps, such as arithmetic reasoning and skolemization, our
reconstruction can avoid expensive search. By skipping proof steps
that are irrelevant for Isabelle, the performance of proof checking
is improved. Our method increases the success rate of Sledgehammer
by halving the failure rate and reduces the checking time by 13%.
We provide a detailed evaluation of the reconstruction time for each
rule. The runtime is influenced by both simple rules that appear
very often and common complex rules.


10:00  10:15 
TheorySpecific Proof Steps Witnessing Correctness of SMT Executions to appear at DAC 2021 (presentation only) video
Ensuring hardware and software correctness increasingly relies on
the use of symbolic logic solvers, in particular for satisfiability
modulo theories (SMT). However, building efficient and correct SMT
solvers is difficult: even stateoftheart solvers disagree on
instance satisfiability. This work presents a system for witnessing
unsatisfiability of instances of NP problems, commonly appearing in
verification, in a way that is natural to SMT solving. Our
implementation of the system seems to often result in significantly
smaller witnesses, lower solving overhead, and faster checking time
in comparison to existing proof formats that can serve a similar
purpose.


10:15  10:30 
Proof Tree Preserving Sequence Interpolation of Quantified Formulas in the Theory of Equality paper (extended abstract) video
Interpolation of SMT formulas is difficult, especially in the
presence of quantifiers since quantifier instantiations introduce
mixed terms, i.e., terms containing symbols that belong to
different partitions of the input formula.
Existing interpolation algorithms for quantified formulas require
proof modifications or syntactical restrictions on the generated
proof trees. We present a nonrestrictive, proof tree preserving
approach to compute inductive sequences of interpolants for
quantified formulas in the theory of equality with uninterpreted
functions using a single proof tree.


10:30  10:45 
AXDInterpolator: a Tool for Computing Interpolants for Arrays with MaxDiff paper (original paper) video
Several approaches toward quantifierfree interpolation algorithms
of theories involving arrays have been proposed by extending the
language using a binary function skolemizing the extensionality
principle. In FoSSaCS 2021, the last three authors studied the
enrichment of the McCarthy’s theory of extensional arrays with
a maxdiff operation. This paper discusses the implementation of
the interpolation algorithm proposed in FoSSaCS 2021 using the
Z3 API. The implementation allows the user to choose Z3, Mathsat,
or SMT Interpol as interpolation engines. The tool returns a
formula in SMTLIB2 format, which allows compatibility with model
checkers and invariant generators using such a format. We compare
our algorithm with stateoftheart interpolation engines. Some
examples reveal that our tool can handle some formulas in our
theory that other solvers cannot. Our experiments using
unsatisfiable formulas extracted with the model checker
UAutomizer show the feasibility of our tool. For that purpose, we
used C programs from the ReachSafetyArrays and MemSafetyArrays
tracks of the SVCOMP.


10:45  11:30  Session 4: Boosting SMT Solving  chair: Andrew Reynolds 
10:45  11:00 
Quantifier Simplification by Unification in SMT to appear at FROCOS 2021 (presentation only) video
Quantifier reasoning in SMT solvers relies on instantiation:
ground instances are generated heuristically from the quantified
formulas until a contradiction is reached at the ground level.
Current instantiation heuristics, however, often fail in presence
of nested quantifiers. To address this issue we introduce a
unificationbased method that augments the problem with shallow
quantified formulas obtained from assertions with nested quantifiers.
These new formulas help unlocking the regular instantiation
techniques, but parsimony is necessary since they might also be
misguiding. To mitigate this, we identify some effective restricting
conditions. The method is implemented in the veriT solver, and tested
on benchmarks from the SMTLIB. It allows the solver to prove more
formulas, faster.


11:00  11:15 
FirstOrder Instantiation using Discriminating Terms paper (extended abstract) video
This paper proposes a technique to limit the number of possible
terms to consider in quantifier instantiation. One of the major
hurdle that SMT solvers face when dealing with quantifiers is that
there are simply too many terms to instantiate with. So even if the
right set of terms is available to the solver, meaning they appear
in the formula, the solver might not have enough resources to come
upon the right combination. This motivates the technique presented
in this paper, which instantiates only by a certain type of terms,
called discriminating terms. The paper introduces a class of
formulas, where the proposed technique has a considerable impact.


11:15  11:30 
Further Steps Down The Wrong Path: Improving the BitBlasting of Multiplication paper (extended abstract) video
Reducing terms in the theory of bitvectors to formulae in
propositional logic, "bitblasting", is a popular and effective
technique. For logical operations, comparisons and even
bitvector addition, it produces circuit or CNF formulae that are
linear in the size of the bitvectors and unit propagation gives
effective bitwise reasoning.
However, it is highly limited when it comes to multiplication.
The formulae produced are at least one order of magnitude larger
than other terms and introduce significant difficulty into the SAT
problem.
Even basic aware of modular (2^{n}) arithmetic and the vast
body of arithmetic, algebraic and cryptographic theorems on it make
it clear that bitblasting is the wrong path for handling
multiplication.
In this workinprogress paper we sketch two further steps along this
wrong path, compacting multiplication by constant and showing the
existence of incremental encodings of multiplication.
It is hoped that these will not only get us closer to "the best
that can be achieved given the limitations" but also that they
might eventually connect to less limited, algebraic techniques.


11:30  11:45  Break  
11:45  12:45  Session 5: SMTCOMP 2021  chair: Alberto Griggio 
11:45  12:45 
SMTCOMP 2021 Report and Tool Presentations 
Monday, 20210719
08:00  09:00  Session 1: Invited Talk  chair: Alexander Nadel 
08:00  09:00  Invited Talk: AVR: WordLevel Verification by
Equality Abstraction of Data State
AVR is, primarily, an IC3/PDRstyle model checker for safety
properties of wordlevel hardware. It scales to large designs by
automatically abstracting the state space of wordlevel variables
such that only equality and disequality among the variables are
preserved regardless of their exact bitprecise assignments. The
abstraction is parameterized by a userspecified bit width threshold
𝑤 which can range from 1 to the largest bit width in the design.
Reachability queries employ EUF logic for word level variables whose
width is larger than 𝑤 and BV logic for variables whose width is less
than or equal to 𝑤. This provides for a range of data abstractions
that enable AVR to successfully handle a diverse set of benchmarks.
AVR produces compact wordlevel inductive invariants for safe designs
or counterexamples for unsafe designs. AVR was the overall winner of
the 2020 Hardware Model Checking Competition. In this talk I will
analyze AVR’s performance on the 2020 HWMCC benchmarks under a
variety of bit width thresholds. I will also compare its IC3/PDR mode
with an option for 𝑘induction and discuss the advantages and
limitations of these approaches for different benchmark families.


09:00  09:30  Session 2: SMT Applications  chair: Mathias Preiner 
09:00  09:15 
On Symmetry and Quantification: A New Approach to Verify Distributed Protocols paper at NFM 2021 (presentation only) video
Proving that an unbounded distributed protocol satisfies a given
safety property amounts to finding a quantified inductive invariant
that implies the property for all possible instance sizes of the
protocol. Existing methods for solving this problem can be described
as search procedures for an invariant whose quantification prefix
fits a particular template. We propose an alternative constructive
approach that does not prescribe, a priori, a specific quantifier
prefix. Instead, the required prefix is automatically inferred
without any search by carefully analyzing the structural symmetries
of the protocol. The key insight underlying this approach is that
symmetry and quantification are closely related concepts that
express protocol invariance under different rearrangements of its
components. We propose symmetric incremental induction, an extension
of the finitedomain IC3/PDR algorithm, that automatically derives
the required quantified inductive invariant by exploiting the
connection between symmetry and quantification. While various
attempts have been made to exploit symmetry in verification
applications, to our knowledge, this is the first demonstration of
a direct link between symmetry and quantification in the context of
clause learning during incremental induction. We also describe a
procedure to automatically find a minimal finite size, the cutoff,
that yields a quantified invariant proving safety for any size.
Our approach is implemented in IC3PO, a new verifier for distributed
protocols that significantly outperforms the stateoftheart,
scales orders of magnitude faster, and robustly derives compact
inductive invariants fully automatically.


09:15  09:30 
CounterexampleGuided Prophecy for Model Checking Modulo the Theory of Arrays paper at TACAS 2021 (presentation only) video
We develop a framework for model checking infinitestate systems by
automatically augmenting them with auxiliary variables, enabling
quantifierfree induction proofs for systems that would otherwise
require quantified invariants. We combine this mechanism with a
counterexampleguided abstraction refinement scheme for the theory
of arrays. Our framework can thus, in many cases, reduce inductive
reasoning with quantifiers and arrays to quantifierfree and
arrayfree reasoning. We evaluate the approach on a wide set of
benchmarks from the literature. The results show that our
implementation often outperforms stateoftheart tools,
demonstrating its practical potential.


09:30  10:15  Session 3: SMTLIB and API  chair: Andrew V. Jones 
09:30  09:45 
Dolmen: A validator for SMTLIB and much more paper (extended abstract) video
Dolmen provides tools to parse, type, and validate input files used
in automated deduction, such as problems written in the SMTLIB
language, but also other languages commonly used in theorem provers,
such as TPTP. Dolmen is split into three parts: a commandline
binary, an LSP server, and an OCaml API. The command line binary
can not only validate files, but more importantly is built so that
it can provide informative error messages when input files do not
respect their language specification. These capabilities are also
provided as an LSP server, which can connect to all current editors
to provide instantaneous feedback when editing files. Lastly,
Dolmen also provides a flexible API in OCaml so that new projects
in the field of automated deduction do not need to reimplement the
parsing and typing of input files.


09:45  10:00 
Characteristic Subsets of SMTLIB Benchmarks paper (original paper) video
A typical challenge faced when developing a parametrized solver is
to evaluate a set of strategies over a set of benchmarking problems.
When the set of strategies is large, the evaluation is often done
with a restricted time limit and/or on a smaller subset of problems
order to estimate the quality of the strategies in a reasonable
time. Firstly, considering the standard SMTLIB benchmarks, we ask
the question how much the time evaluation limit and benchmark size
can be restricted to still obtain reasonable performance results.
Furthermore, we propose a method to construct a benchmark
characteristic subset which faithfully characterizes all benchmark
problems. To achieve this, we collect problem performance statistics
and employ clustering methods. We evaluate the quality of our
benchmark characteristic subsets on the task of the best cover
construction, and we compare the results with randomly selected
benchmark subsets. We show that our method achieves smaller relative
error than random problem selection.


10:00  10:15 
SmtSwitch: A Solveragnostic C++ API for SMT Solving paper at SAT 2021 (presentation only) video
This paper presents SmtSwitch, an opensource, solveragnostic API
for SMT solving. SmtSwitch provides an abstract interface, which
can be implemented by different SMT solvers. SmtSwitch provides
simple, uniform, and highperformance access to SMT solving for
applications in areas such as automated reasoning, planning, and
formal verification. The interface allows the user to create,
traverse, and manipulate terms, as well as to dynamically dispatch
queries to different underlying SMT solvers.


10:15  10:45  Break  
10:45  12:45  Session 4: SMTLIB and Business Meeting  chair: Cesare Tinelli 
10:45  11:45  SMTLIB Report 

11:45  12:45  Business Meeting of the SMT Steering Committee  