All times are for Los Angeles, USA, which observes PDT (UTC-7).
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, 2021-07-18
| 08:00 - 09:00 | Session 1: Invited Talk | chair: Aina Niemetz |
| 08:00 - 09:00 | Invited Talk: Using SMT and Abstraction-Refinement for Neural Network Verification
Deep neural networks are increasingly being used as controllers for
safety-critical 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 over-approximation 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 over-approximation
may be too coarse, in which case the underlying verification tool
might return a spurious counterexample. Under such conditions, we can
perform counterexample-guided 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
abstraction-refinement 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 first-order 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
SMT-LIB.
|
|
| 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 Nelson-Oppen method. The Nelson-Oppen
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 Nelson-Oppen 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 speed-up on a smart contract verification
benchmark.
|
|
| 09:30 - 09:45 | Break | |
| 09:45 - 10:45 | Session 3: Proofs and Interpolation | chair: Stéphane Graham-Lengrand |
| 09:45 - 10:00 |
Reliable Reconstruction of Fine-Grained 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 fine-grained 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 |
Theory-Specific 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 state-of-the-art 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 non-restrictive, 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 quantifier-free 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 state-of-the-art 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 ReachSafety-Arrays and MemSafety-Arrays
tracks of the SV-COMP.
|
|
| 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
unification-based 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 SMT-LIB. It allows the solver to prove more
formulas, faster.
|
|
| 11:00 - 11:15 |
First-Order 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 Bit-Blasting of Multiplication paper (extended abstract) video
Reducing terms in the theory of bit-vectors to formulae in
propositional logic, "bit-blasting", is a popular and effective
technique. For logical operations, comparisons and even
bit-vector addition, it produces circuit or CNF formulae that are
linear in the size of the bit-vectors and unit propagation gives
effective bit-wise 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 (2n) arithmetic and the vast
body of arithmetic, algebraic and cryptographic theorems on it make
it clear that bit-blasting is the wrong path for handling
multiplication.
In this work-in-progress 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: SMT-COMP 2021 | chair: Alberto Griggio |
| 11:45 - 12:45 |
SMT-COMP 2021 Report and Tool Presentations |
|
Monday, 2021-07-19
| 08:00 - 09:00 | Session 1: Invited Talk | chair: Alexander Nadel |
| 08:00 - 09:00 | Invited Talk: AVR: Word-Level Verification by
Equality Abstraction of Data State
AVR is, primarily, an IC3/PDR-style model checker for safety
properties of word-level hardware. It scales to large designs by
automatically abstracting the state space of word-level variables
such that only equality and dis-equality among the variables are
preserved regardless of their exact bit-precise assignments. The
abstraction is parameterized by a user-specified 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 word-level 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 re-arrangements of its
components. We propose symmetric incremental induction, an extension
of the finite-domain 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 state-of-the-art,
scales orders of magnitude faster, and robustly derives compact
inductive invariants fully automatically.
|
|
| 09:15 - 09:30 |
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays paper at TACAS 2021 (presentation only) video
We develop a framework for model checking infinite-state systems by
automatically augmenting them with auxiliary variables, enabling
quantifier-free induction proofs for systems that would otherwise
require quantified invariants. We combine this mechanism with a
counterexample-guided abstraction refinement scheme for the theory
of arrays. Our framework can thus, in many cases, reduce inductive
reasoning with quantifiers and arrays to quantifier-free and
array-free reasoning. We evaluate the approach on a wide set of
benchmarks from the literature. The results show that our
implementation often outperforms state-of-the-art tools,
demonstrating its practical potential.
|
|
| 09:30 - 10:15 | Session 3: SMT-LIB 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 SMT-LIB
language, but also other languages commonly used in theorem provers,
such as TPTP. Dolmen is split into three parts: a command-line
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 re-implement the
parsing and typing of input files.
|
|
| 09:45 - 10:00 |
Characteristic Subsets of SMT-LIB 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 SMT-LIB 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 |
Smt-Switch: A Solver-agnostic C++ API for SMT Solving paper at SAT 2021 (presentation only) video
This paper presents Smt-Switch, an open-source, solver-agnostic API
for SMT solving. Smt-Switch provides an abstract interface, which
can be implemented by different SMT solvers. Smt-Switch provides
simple, uniform, and high-performance 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: SMT-LIB and Business Meeting | chair: Cesare Tinelli |
| 10:45 - 11:45 | SMT-LIB Report |
|
| 11:45 - 12:45 | Business Meeting of the SMT Steering Committee | |