=Paper=
{{Paper
|id=Vol-2854/xfrontmatter
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-2854/xfrontmatter.pdf
|volume=Vol-2854
}}
==None==
https://ceur-ws.org/Vol-2854/xfrontmatter.pdf
Satisfiability Modulo Theories —
18th International Workshop,
SMT 2020
Online (initially located in Paris, France)
July 5–6, 2020
Proceedings
Edited by François Bobot and Tjark Weber
Copyright c 2020 for the individual papers by the papers’ authors. Copyright c 2020 for
the volume as a collection by its editors. This volume and its papers are published under the
Creative Commons License Attribution 4.0 International (CC BY 4.0).
Preface
SMT 2020, the 18th International Workshop on Satisfiability Modulo Theories, was held as a
satellite event of IJCAR 2020 and FSCD 2020 on July 5–6, 2020. The workshop was originally
scheduled to take place in Paris, France, but was eventually held online as a virtual meeting
because of the COVID-19 pandemic.
For background on Satisfiability Modulo Theories and the SMT workshop series, we quote
the following description from its website:1
Determining the satisfiability of first-order formulas modulo background theories,
known as the Satisfiability Modulo Theories (SMT) problem, has proved to be an
enabling technology for verification, synthesis, test generation, compiler optimiza-
tion, scheduling, and other areas. The success of SMT techniques depends on the
development of both domain-specific decision procedures for each background the-
ory (e.g., linear arithmetic, the theory of arrays, or the theory of bit-vectors) and
combination methods that allow one to obtain more versatile SMT tools, usually
leveraging Boolean satisfiability (SAT) solvers. These ingredients together make
SMT techniques well-suited for use in larger automated reasoning and verification
efforts.
The aim of the SMT Workshop is to bring together researchers and users of SMT
tools and techniques. Relevant topics include but are not limited to:
• Decision procedures and theories of interest
• Combinations of decision procedures
• Novel implementation techniques
• Benchmarks and evaluation methodologies
• Applications and case studies
• Theoretical results
Papers on pragmatic aspects of implementing and using SMT tools, as well as novel
applications of SMT, are especially encouraged.
SMT 2020 featured invited talks by Philipp Rümmer and Mooly Sagiv, a joint session
with the 5th International Workshop on Satisfiability Checking and Symbolic Computation
(SC2 2020), and presentations of nine peer-reviewed papers. Of these, five papers are published
in this volume, two as regular papers and three as short papers. The other four papers were
submitted to the workshop for presentation only; we are only including their abstracts.
We would like to thank the SMT Steering Committee, the IJCAR/FSCD organisers, the
SMT Program Committee, the authors and speakers, and everyone else who, by supporting and
adapting to the online format of the event, contributed to the workshop’s success in the midst
of a global pandemic.
François Bobot and Tjark Weber
Co-chairs, SMT 2020
1 https://smt-workshop.cs.uiowa.edu/2020/
Program Committee
Haniel Barbosa, Universidade Federal de Minas Gerais
Clark Barrett, Stanford University
Nikolaj Bjorner, Microsoft Research
Simon Cruanes, Aesthetic Integration
Pascal Fontaine, Université de Lorraine
Stéphane Graham-Lengrand, SRI International
Alberto Griggio, Fondazione Bruno Kessler
Antti Hyvärinen, Università della Svizzera italiana
Mohamed Iguernelala, OcamlPro
Dejan Jovanović, SRI International
Chantal Keller, LRI, Université Paris-Sud
Yannick Moy, AdaCore
Aina Niemetz, Stanford University
Marie Pelleau, Université Nice Sophia Antipolis
Mathias Preiner, Stanford University
Giles Reger, University of Manchester
Andrew Reynolds, University of Iowa
Natasha Sharygina, Università della Svizzera italiana
Peter J. Stuckey, Monash University
Cesare Tinelli, University of Iowa
François Bobot, CEA List
Tjark Weber, Uppsala University
Contents
Invited Talks
Solving String Constraints, Starting from the Beginning and from the End . . . . . . . . . . . . . . . . 1
Philipp Rümmer
Harnessing SMT Solvers for Verifying Low Level Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
Mooly Sagiv
Contributed Papers
Lifting congruence closure with free variables to λ-free higher-order logic via SAT encoding 3
Sophie Tourret, Pascal Fontaine, Daniel El-Ouraoui and Haniel Barbosa
An Empirical Evaluation of SAT Solvers on Bit-vector Problems . . . . . . . . . . . . . . . . . . . . . . . . . 15
Bruno Dutertre
Structural Bit-vector Model Counting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
Seonmo Kim and Stephen McCamant
Bayesian Optimisation of Solver Parameters in CBMC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
Chaitanya Mangla, Sean Holden and Lawrence Paulson
Smt-Switch: a solver-agnostic C++ API for SMT solving . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
Makai Mann, Amalee Wilson, Cesare Tinelli and Clark Barrett
Presentation-only Papers (Abstracts)
Abstract: SMT-Friendly Formalization of the Solidity Memory Model . . . . . . . . . . . . . . . . . . . . 59
Ákos Hajdu and Dejan Jovanović
Abstract: Towards an SMT-LIB Theory of Heap . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
Zafer Esen and Philipp Rümmer
Abstract: BanditFuzz: A Reinforcement-Learning based Performance Fuzzer for SMT
Solvers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
Joseph Scott, Federico Mora and Vijay Ganesh
Abstract: MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers . . . . 62
Joseph Scott, Aina Niemetz, Mathias Preiner and Vijay Ganesh