Vol-2854
urn:nbn:de:0074-2854-1

Copyright © 2020 for the individual papers by the papers' authors. Copyright © 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).

SMT 2020
Satisfiability Modulo Theories 2020

Proceedings of the 18th International Workshop on Satisfiability Modulo Theories
co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020)

Online (initially located in Paris, France), July 5-6, 2020.

Edited by

François Bobot *
Tjark Weber **

* CEA List, Palaiseau, France
** Uppsala University, Uppsala, Sweden

Table of Contents

Front Matter
Summary: There were 9 papers submitted for peer-review to this workshop. Out of these, 5 papers are published in this volume, 2 as regular papers and 3 as extended abstracts. Also included in this volume are abstracts for the workshop's 2 invited talks, and for 4 papers that were submitted for presentation only.

Invited Talks

Invited Talk: Solving String Constraints, Starting from the Beginning and from the End 1
Philipp Rümmer
Invited Talk: 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 (extended abstract) 3-14
Sophie Tourret, Pascal Fontaine, Daniel El-Ouraoui, Haniel Barbosa
An Empirical Evaluation of SAT Solvers on Bit-vector Problems 15-25
Bruno Dutertre
Structural Bit-vector Model Counting (extended abstract) 26-36
Seonmo Kim, Stephen McCamant
Bayesian Optimisation of Solver Parameters in CBMC 37-47
Chaitanya Mangla, Sean Holden, Lawrence Paulson
Smt-Switch: A Solver-agnostic C++ API for SMT Solving (extended abstract) 48-58
Makai Mann, Amalee Wilson, Cesare Tinelli, Clark Barrett

Presentation-only Papers (Abstracts)

Abstract: SMT-Friendly Formalization of the Solidity Memory Model 59
Ákos Hajdu, Dejan Jovanović
Abstract: Towards an SMT-LIB Theory of Heap 60
Zafer Esen, Philipp Rümmer
Abstract: BanditFuzz: A Reinforcement-Learning based Performance Fuzzer for SMT Solvers 61
Joseph Scott, Federico Mora, Vijay Ganesh
Abstract: MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers 62
Joseph Scott, Aina Niemetz, Mathias Preiner, Vijay Ganesh

2021-04-13: submitted by Tjark Weber, metadata incl. bibliographic data published under Creative Commons CC0
2021-04-23: published on CEUR Workshop Proceedings (CEUR-WS.org, ISSN 1613-0073) |valid HTML5|