All times are for Los Angeles, USA, which observes PDT (UTC-7).

The CAV21 Platform is now live at

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  
Guy Katz
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
Fabian Zaiser and Luke Ong
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
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark Barrett and Cesare Tinelli
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
Hans-Jörg Schurr, Mathias Fleury and Martin Desharnais
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
Rodrigo Otoni, Martin Blicha, Patrick Eugster, Antti E. J. Hyvärinen and Natasha Sharygina
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
Elisabeth Henkel, Jochen Hoenicke and Tanja Schindler
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
Jose Abel Castellanos Joo, Silvio Ghilardi, Alessandro Gianola and Deepak Kapur
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
Pascal Fontaine and Hans-Jörg Schurr
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
Chad Brown and Mikoáš Janota
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
Martin Brain
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
Haniel Barbosa, Jochen Hoenicke and Antti Hyvärinen

     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

Karem A. Sakallah
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
Aman Goel and Karem A. Sakallah
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
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon and Clark Barrett
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
Guillaume Bury
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
Jan Jakubův, Mikoláš Janota and Andrew Reynolds
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
Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli and Clark Barrett
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
Clark Barrett, Pascal Fontaine and Cesare Tinelli
11:45 - 12:45 Business Meeting of the SMT Steering Committee