SMT 2023
Satisfiability Modulo Theories 2023

Table of Contents

• Preface
  Summary: There were 14 papers submitted for peer-review to this workshop, 3 as regular papers, 3 as extended abstracts, and 7 as presentation only. Out of these, 7 papers are published in these proceedings, were accepted for this volume, 3 as regular papers and 3 as extended abstracts. Also included in this volume is the abstract for two invited talks and one abstract of a paper that was submitted as presentation-only. For the remaining 6 presentation-only papers we provide the references.

Invited Talks

• Invited Talk: Deductive Verification of Distributed Protocols in Decidable Logics 1
  Oded Padon
• Invited Talk: SAT and SMT Solving at Cloud Scale 2
  Michael Whalen

Regular Papers

• Automated Analysis of Halo2 Circuits 3-17
  Fatemeh Heidari Soureshjani , Mathias Hall-Andersen , Mohammadmahdi Jahanara , Jeffrey Kam , Jan Gorzny , Mohsen Ahmadvand
• Complete Trigger Selection in Satisfiability Modulo First-Order Theories 18-32
  Christopher Lynch , Stephen Miner
• Exploiting Strict Constraints in the Cylindrical Algebraic Covering 33-45
  Philipp Bär , Jasper Nalbach , Erika Ábrahám , Christopher Brown

Extended Abstracts

• Application of SMT in a Meta-Compiler: A Logic DSL for Specifying Type Systems 46-61
  Romain Béguet , Raphaël Amiard
• Verifying Models with Dolmen 62-70
  Guillaume Bury , François Bobot
• Selecting Quantifiers for Instantiation in SMT 71-77
  Jan Jakubův , Mikoláš Janota , Bartosz Piotrowski , Jelle Piepenbrock , Andrew Reynolds

Presentation-Only Papers (Abstracts)

• Automatic Verification of SMT Rewrites in Isabelle/HOL 78
  Hanna Lachnitt , Mathias Fleury , Leni Aniva , Andrew Reynolds , Haniel Barbosa , Andres Noetzli , Clark Barrett , Cesare Tinelli

Presentation-Only Papers (References)

• Reasoning About Vectors using an SMT Theory of Sequences (presentation only) (paper published at IJCAR 2022 , available here )
  Ying Sheng , Andres Noetzli , Andrew Reynolds , Yoni Zohar , David Dill , Wolfgang Grieskamp , Junkil Park , Shaz Qadeer , Clark Barrett , Cesare Tinelli
• Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem (presentation only) (paper published at NFM 2023 , available here )
  Enrico Lipparini , Stefan Ratschan
• IPASIR-UP: User Propagators for CDCL (presentation only) (paper published at SAT 2023 )
  Katalin Fazekas , Aina Niemetz , Mathias Preiner , Markus Kirchweger , Stefan Szeider , Armin Biere
• Satisfiability Modulo Finite Fields (presentation only) (paper published at CAV 2023 )
  Alex Ozdemir , Gereon Kremer , Cesare Tinelli , Clark Barrett
• An Abstract Calculus for Optimization Modulo Theories (presentation only)
  Nestan Tsiskaridze , Cesare Tinelli , Clark Barrett
• Partitioning Strategies and Partitioning Portfolios for Parallel SMT Solving (presentation only)
  Amalee Wilson , Andres Noetzli , Andrew Reynolds , Byron Cook , Clark Barrett , Cesare Tinelli