Vol-2853⫷ Vol-2854 ⫸Vol-2855
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 |