Proceedings 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). SMT 2020, the 18th International Workshop on Satis ability 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 Satis ability Modulo Theories and the SMT workshop series, we quote the following description from its website:1
Determining the satis ability of rst-order formulas modulo background theories, known as the Satis ability Modulo Theories (SMT) problem, has proved to be an enabling technology for veri cation, synthesis, test generation, compiler optimization, scheduling, and other areas. The success of SMT techniques depends on the development of both domain-speci c decision procedures for each background theory (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 satis ability (SAT) solvers. These ingredients together make SMT techniques well-suited for use in larger automated reasoning and veri cation e orts.
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:
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 Rummer and Mooly Sagiv, a joint session with the 5th International Workshop on Satis ability Checking and Symbolic Computation (SC2 2020), and presentations of nine peer-reviewed papers. Of these, ve 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.
Program Committee
Pascal Fontaine, Universite de Lorraine Stephane Graham-Lengrand, SRI International Alberto Griggio, Fondazione Bruno Kessler Antti Hyvarinen, Universita della Svizzera italiana Mohamed Iguernelala, OcamlPro Dejan Jovanovic, SRI International Chantal Keller, LRI, Universite Paris-Sud Yannick Moy, AdaCore Aina Niemetz, Stanford University Marie Pelleau, Universite Nice Sophia Antipolis Mathias Preiner, Stanford University Giles Reger, University of Manchester Andrew Reynolds, University of Iowa Natasha Sharygina, Universita della Svizzera italiana Peter J. Stuckey, Monash University Cesare Tinelli, University of Iowa
Harnessing SMT Solvers for Verifying Low Level Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
Mooly Sagiv
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
Abstract: SMT-Friendly Formalization of the Solidity Memory Model . . . . . . . . . . . . . . . . . . . . 59
Akos Hajdu and Dejan Jovanovic Abstract: Towards an SMT-LIB Theory of Heap . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
Zafer Esen and Philipp Rummer 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