Proceedings ©2021 Copyright for the individual papers by their authors. Copyright for the volume as a collection by its editors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CPWrEooUrckResehdoinpgs IhStSpN:/c1e6u1r3-w-0s0.o7r3g CEUR Workshop Proceedings (CEUR-WS.org) The 19th International Workshop on Satisfiability Modulo Theories was held on July 18th and 19th in association with the 33rd International Conference on Computer Aided Verification. The workshop had originally been scheduled to take place in Los Angeles, USA, but was held online as a virtual meeting due to the COVID-19 pandemic and its repercussions.
The SMT workshop is an annual event dedicated to Satisfiability Modulo Theories (SMT).
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, test-vector generation, compiler optimization, scheduling, and other areas.
The success of SMT techniques depends on the development of both domain-specific decision procedures for each concrete 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. These two ingredients together make SMT techniques well-suited for use in larger automated reasoning and formal verification eforts.
The workshop aims at bringing 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
SMT 2021 featured invited talks by Guy Katz from the University of Jerusalem and Karem A. Sakallah from the University of Michigan, and the presentation of 14 peer-reviewed papers. The workshop received 16 submissions, out of which 14 were accepted. Each submission was reviewed by three program committee members. Of the 14 accepted submissions, six are published in this volume: two as original papers, and four as extended abstracts. The remaining eight were submitted to the workshop for presentation only. For two of them, the authors agreed to include the paper abstracts in this volume.
We would like to thank the program commitee, the authors, the invited speakers and the SMT Steering Committee for their contributions to the workshop. We would further like to thank the CAV organizers for hosting the workshop, EasyChair for the availability of their conference system, and CEUR for their help to publish these proceedings.
Alexander Nadel and Aina Niemetz Co-chairs, SMT 2021 Program Committee Alexander Nadel, Intel Aina Niemetz, Stanford University