All times are for Europe/Paris, which observes CEST (UTC+2). A calendar is available.
Sunday, 20200705 Live Stream Day 1
10:00  11:00  Session 1: SMT for Program Verification  chair: Stéphane GrahamLengrand 
10:00  10:30  SMTFriendly Formalization of the Solidity Memory Model paper (presentation only) Ákos Hajdu and Dejan Jovanović
Solidity is the dominant programming language for Ethereum
smart contracts. This paper presents a highlevel
formalization of the Solidity language with a focus on the
memory model. The presented formalization covers all
features of the language related to managing state and
memory. In addition, the formalization we provide is
effective: all but few features can be encoded in the
quantifierfree fragment of standard SMT theories. This
enables precise and efficient reasoning about the state of
smart contracts written in Solidity. The formalization is
implemented in the solcverify verifier and we provide an
extensive set of tests that covers the breadth of the
required semantics. We also provide an evaluation on the
test set that validates the semantics and shows the novelty
of the approach compared to other Soliditylevel contract
analysis tools.


10:30  11:00  Towards an SMTLIB Theory of Heap paper (presentation only) Zafer Esen and Philipp Rümmer
Constrained Horn Clauses (CHC) are a convenient intermediate
verification language that can be generated by several
verification tools, and that can be processed by several
mature and efficient Horn solvers. One of the main
challenges when using CHC in verification is the encoding of
program with heapallocated datastructures: such
datastructures are today either represented explicitly
using the theory of arrays, or are transformed away with the
help of invariants or refinement types. Both approaches have
disadvantages: they are lowlevel, do not preserve the
structure of a program well, and leave little design choice
with respect to the handling of heap to the Horn
solver. This abstract presents ongoing work on the
definition of a highlevel SMTLIB theory of heap, which in
the context of CHC gives rise to standard interchange format
for programs with heap datastructures. The abstract
presents the signature and intuition behind the theory. A
preliminary version of the theory axioms can be found in the
appendix. The abstract is meant as a starting point for
discussion, and request for comments.


11:00  11:30  FSCD/IJCAR virtual coffee break  
11:30  13:00  Session 2: SAT and Bit Vectors  chair: François Bobot 
11:30  12:00  Lifting congruence closure with free variables to λfree higherorder logic via SAT encoding extended abstract Sophie Tourret, Pascal Fontaine, Daniel ElOuraoui and Haniel Barbosa
Recent work in extending SMT solvers to higherorder logic
(HOL) has not explored lifting quantifier instantiation
algorithms to perform higherorder unification. As a
consequence, widely used instantiation techniques, such as
trigger and particularly conflictbased, can only be
applied in a limited manner. Congruence closure with free
variables (CCFV) is a decision procedure for the Eground
(dis)unification problem, which is at the heart of these
instantiation techniques. Here, as a first step towards
fully supporting trigger and conflictbased instantiation
in HOL, we define the Eground (dis)unification problem in
λfree higherorder logic (λfHOL), an extension of
firstorder logic where function symbols may be partially
applied and functional variables may occur, and extend CCFV
to solve it. To improve scalability in the context of
handling higherorder variables, we rely on an encoding of
the CCFV search as a propositional formula. We present a
solution reconstruction procedure so that models for the
propositional formula lead to solutions for the Eground
(dis)unification problem. This is instrumental to port
trigger and conflictbased instantiation to be fully
applied in λfHOL.


12:00  12:30  An Empirical Evaluation of SAT Solvers on Bitvector Problems paper Bruno Dutertre
Bit blasting is the main method for solving SMT problems in
the theory of fixed size bit vectors. It converts bitvector
problems to equisatisfiable Boolean satisfiability problems
that are then solved by SAT solvers. We present an empirical
evaluation of stateoftheart SAT solvers on problems
produced by bit blasting with the Yices SMT solver. The
results are quite different from common SAT solver
evaluations such as the SAT races and SAT competitions,
which argues for extending these evaluations to include
benchmarks derived from SMT problems.


12:30  13:00  Structural BitVector Model Counting extended abstract Seonmo Kim and Stephen McCamant Various approximate model counting techniques have been proposed and are used in many applications such as probabilistic inference and quantitative informationflow security. The hashingbased technique is a wellknown approach and can be more scalable than exact model counting techniques. However, its performance is highly dependent on the performance of a decision procedure (SAT or SMT solver) and adding numerous hashing constraints to a formula might cause a solver to perform poorly. We propose a model counting technique which computes lower and upper bounds of the number of solutions to an SMT formula by analyzing the structure of the formula, which means this approach does not rely on a decision procedure. Our algorithm runs in polynomial time and gives firm lower and upper bounds unlike other approximate model counters that compute probabilistic bounds. We compare our algorithm with stateofthe art model counters and our experiments show that our approach is faster than others and provides a tradeoff between computational effort and the precision of results. 

13:00  14:00  Lunch break  
14:00  15:30  Joint SC^{2} session  chair: Konstantin Korovin 
The papers in this session were accepted by the SC^{2} program committee for presentation at the SC^{2} workshop. SMT participants are invited to attend these presentations.  
14:00  14:30  Computing Tropical Prevarieties with Satisfiability Modulo Theory (SMT) Solvers paper Christoph Lüders
A novel way to use SMT (Satisfiability Modulo Theories)
solvers to compute the tropical prevariety
(resp. equilibrium) of a polynomial system is presented. The
new method is benchmarked against a naive approach that uses
purely polyhedral methods. It turns out that the SMT
approach is faster than the polyhedral approach for models
that would otherwise take more than one minute to compute,
in many cases by a factor of 60 or more, and in the worst
case is only slower by a factor of two. Furthermore, the new
approach is an anytime algorithm, thus offering a way to
compute parts of the solution when the polyhedral approach
is infeasible.


14:30  15:00  GeoGebra and the realgeom Reasoning Tool Robert Vajda and Zoltán Kovács
Reasoning tools for geometric equalities based on
elimination methods are already integrated in some dynamic
geometry systems (DGS), in particular in GeoGebra. However,
no reasoning tools in any popular DGS environments for
elementary inequalities exist yet. This paper investigates
if the generic real quantifier elimination (RQE) methods and
their existing implementations are mature enough from the
practical point of view to explore simple elementary
Euclidean triangle inequalities and the best possible
geometric constants occurring in the inequalities. It is
known, that from theoretical point, real geometry inequality
problems can be cast as RQE problems and can be solved by
RQE algorithms. Unfortunately, the computational complexity
of the RQE algorithms are rather high. The practical
question is, if the RQE problem formulations for the
investigated geometric inequality are tractable in a
reasonable time limit. If this is so, an RQE based geometry
inequality prover may be also an integral part of DGS. As a
first experimental step, we also implemented a real
reasoning tool for GeoGebra called realgeom which uses
Wolfram’s Mathematica polyalgorithmic RQE tool as an
external service for solving the semialgebraic problem
associated to the geometric inequality exploration
problem. Finally, we show by an example that parametric real
root counting algorithms may be sufficient to attack certain
inequality exploration problems and they can be later
substitutes/alternatives for the general RQE tool in our
framework.


15:00  15:30  New Opportunities for the Formal Proof of Computational Real Geometry? Erika Abraham, James H. Davenport, Matthew England, Gereon Kremer and Zak Tonks
The purpose of this paper is to explore the question “to
what extent could we produce formal, machineverifiable,
proofs in real algebraic geometry?” The question has been
asked before but as yet the leading algorithms for answering
such questions have not been formalised. We present the
thesis that a new algorithm for ascertaining satisfiability
of formulae over the reals via Cylindrical Algebraic
Coverings might provide a trace and outputs that allow the
results to be more susceptible to machine verification than
those of competing algorithms.


15:30  16:00  FSCD/IJCAR virtual coffee break  
16:00  17:00  Session 3  chair: Haniel Barbosa 
16:00  17:00  Invited talk: Solving String Constraints, Starting from the Beginning and from the End Philipp Rümmer
The recent years have seen a wealth of research on string solvers,
i.e., SMT solvers that can check satisfiability of quantifierfree
formulas over a background theory of strings and regular
expressions. String solvers can be applied in different verification
algorithms, for instance in symbolic execution to check path
feasibility, in software model checking to take care of implication
checks; a prime application area is security analysis for languages
like JavaScript and PHP, for instance to discover vulnerability to
injection attacks. To process constraints from those domains, it is
necessary for string solvers to handle a delicate combination of
(theoretically and practically) challenging operations: concatenation
in word equations, to model assignments in programs; regular
expressions or contextfree grammars, to model properties or attack
patterns; string length, to express string manipulation in programs;
transduction, to express sanitisation, escape operations, and
replacement operations in strings; and others. This talk will give a
general introduction to string solving, and then present a solver
architecture based on the concept of preimage computation that is
simple, yet turns out to be complete for an expressive fragment of
string constraints. The architecture has been implemented in our
solver OSTRICH (and is the result of joint work with many people).

Monday, 20200706 Live Stream Day 2
10:00  11:00  Session 1  chair: Pascal Fontaine 
10:00  11:00  Invited talk: Harnessing SMT Solvers for Verifying Low Level Programs Mooly Sagiv Smart contracts are positioned to revolutionize today's business processes by automating financial transactions, digital media distribution, medical record management, property ownership registration, and more. The vast majority of smart contracts are implemented using virtual machines such as EVM and WebAssembly which are very powerful. However, bugs in smart contracts lead to tremendous economic losses. I will describe our ongoing effort to leverage existing SMT solvers for verifying smart contracts and uncovering subtle bugs. We are developing SaaS technology demo.certora.com for smart contract verification. This technology is intended to be used as part of the CI/CD of smart contract development. Safety properties of smart contracts are described in a high level manner to enable reuse across different smart contracts. The EVM code is decompiled into an intermediate representation using static analysis and the SMT formula is generated and fed into SMT solvers. The formulas include nonlinear integer arithmetic with large constants, uninterpreted functions, quantifications. I will also describe some of the high level properties checked and bugs found using the SMT solvers. This is a joint work with Thomas Bernardi, Nurit Dor, Anastasia Fedotov, Shelly Grossman, Alexander Nutz, Lior Oppenheim, Or Pistiner, John A. Toman, and James R. Wilcox. 

11:00  11:30  FSCD/IJCAR virtual coffee break  
11:30  13:00  Session 2: Learning for SMT  chair: Antti Hyvärinen 
11:30  12:00  BanditFuzz: A ReinforcementLearning based Performance Fuzzer for SMT Solvers (presentation only) Joseph Scott, Federico Mora and Vijay Ganesh
In this paper, we present a reinforcementlearning based
fuzzing system, BanditFuzz, that zeroes in on the
grammatical constructs of wellformed inputs that are the
root cause of performance slowdown in SMT
solvers. BanditFuzz takes the following as input: a grammar
G describing wellformed inputs to a set of distinct solvers
(say, a target solver T and a reference solver R) that
implement the same specification, and a fuzzing objective
(e.g., maximize the relative performance difference between
T and R). BanditFuzz outputs a list of grammatical
constructs that are ranked in descending order by how likely
they are to maximize performance differences between solvers
T and R. Using BanditFuzz, we constructed two benchmark
suites (with 400 floating point and 300 string instances)
that expose performance issues in all considered solvers,
namely, Z3, CVC4, Colibri, MathSAT, Z3seq, and Z3str3. We
also performed a comparison of BanditFuzz against random,
mutation, and evolutionary fuzzing methods and observed up
to a 81% improvement based on PAR2 scores used in SAT
competitions.


12:00  12:30  MachSMT: A Machine Learningbased Algorithm Selector for SMT Solvers (presentation only) Joseph Scott, Aina Niemetz, Mathias Preiner and Vijay Ganesh
In this paper, we present MachSMT, an algorithm selection
tool for stateoftheart Satisfiability Modulo Theories
(SMT) solvers. MachSMT supports the entirety of the logics
within the SMTLIB initiative. MachSMT uses machine learning
to learn empirical hardness models (a mapping from SMTLIB
instances to solvers) for stateoftheart SMT solvers to
compute a ranking of which solver is most likely to solve a
particular instance the fastest. We analyzed the performance
of MachSMT on 102 logics/tracks of SMTCOMP 2019 and observe
that it improves on competition winners in 49 logics (with
up to 240% in perfor mance for certain logics). MachSMT is
clearly not a replacement for any particular SMT solver, but
rather a tool that enables users to leverage the collective
strength of the diverse set of algorithms implemented as
part of these sophisticated solvers. Our MachSMT artifact is
available
at https://github.com/j29scott/MachSMT.


12:30  13:00  Bayesian Optimisation of Solver Parameters in CBMC paper Chaitanya Mangla, Sean Holden and Lawrence Paulson
Satisfiability solvers can be embedded in applications to
perform specific formal reasoning tasks. CBMC, for example,
is a bounded model checker for C and C++ that embeds SMT and
SAT solvers to check internally generated formulae. Such
solvers will be solely used to evaluate the class of
formulae generated by the embedding application and
therefore may benefit from domainspecific parameter
tuning. We propose the use of Bayesian optimisation for this
purpose, which offers a principled approach to blackbox
optimisation within limited resources. We demonstrate its
use for optimisation of the solver embedded in CBMC
specifically for a collection of test harnesses in active
industrial use, for which we have achieved a significant
improvement over the default parameters.


13:00  14:00  Lunch break  
14:00  15:30  Session 3: SMT Solvers  chair: Giles Reger 
14:00  14:30  SmtSwitch: a solveragnostic C++ API for SMT solving extended abstract Makai Mann, Amalee Wilson, Cesare Tinelli and Clark Barrett
This extended abstract describes work in progress on
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.


14:30  15:30  SMTCOMP 2020 Report and Tool Presentations Haniel Barbosa, Jochen Hoenicke and Antti Hyvärinen 

15:30  16:00  FSCD/IJCAR virtual coffee break  
16:00  17:30  Session 4  chair: Tjark Weber 
16:00  16:45  SMTLIB Report Cesare Tinelli and Pascal Fontaine 

16:45  17:30  Business meeting of the SMT Steering Committee 