SMT 2025: 23RD INTERNATIONAL WORKSHOP ON SATISFIABILITY MODULO THEORIES

A
Ait-El-Hara, Hichem Rami	Constraint Propagation for Bit-Vectors in Alt-Ergo
B
Barlik, Marcel	Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2
Barrett, Clark	A Catalog of SMT-LIB Benchmarks A Proposal for an OMT Extension to SMT-LIB
Berg, Jeremias	An Optimization Modulo Theories-Based Approach to Cumulative Scheduling with Delays
Bjørner, Nikolaj	A Conjecture Regarding SMT Instability
Blicha, Martin	Space Explanations of Neural Network Classification
Bobot, François	Visualization of Execution Traces in Colibri 2 SMT Solver SMT-COMP Presentation
Brain, Martin	Evaluating Binary Polynomials using Subpolynomials Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2
Bury, Guillaume	Constraint Propagation for Bit-Vectors in Alt-Ergo
C
Candea, George	A Conjecture Regarding SMT Instability
Cebeci, Can	A Conjecture Regarding SMT Instability
Clément, Basile	Constraint Propagation for Bit-Vectors in Alt-Ergo
D
Dančo, Marek	From MBQI to Enumerative Instantiation and Back
Dasnois, Ellen	A Few Exercises on the Complexity of Congruence Closure with Cardinality Constraints
Deharbe, David	SMT-COMP Presentation
F
Fazekas, Katalin	SAT Reasoning in CDCL(T) Solvers
Fedyukovich, Grigory	Space Explanations of Neural Network Classification
Fontaine, Pascal	A Catalog of SMT-LIB Benchmarks A Few Exercises on the Complexity of Congruence Closure with Cardinality Constraints
Frankel, Guy	Syntax-Guided Synthesis with Counterexample-Guided E-graphs: A Work-in-Progress Report
Frohn, Florian	Satisfiability Modulo Exponential Integer Arithmetic
G
Giesl, Jürgen	Satisfiability Modulo Exponential Integer Arithmetic
Graham-Lengrand, Stéphane	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
Gàmez-Montolio, Arnau	Evaluating Binary Polynomials using Subpolynomials
H
Hader, Thomas	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
Heule, Marijn	Instability Track for SMT-COMP
Hoenicke, Jochen	Business Meeting
Howe, Jacob M.	Evaluating Binary Polynomials using Subpolynomials
Hozzová, Petra	From MBQI to Enumerative Instantiation and Back
I
Irfan, Ahmed	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
J
Jakubův, Jan	Quantifier Instantiations: To Mimic or To Revolt?
Janota, Mikoláš	Quantifier Instantiations: To Mimic or To Revolt? From MBQI to Enumerative Instantiation and Back
Jonáš, Martin	SMT-COMP Presentation
Junke, Christophe	Visualization of Execution Traces in Colibri 2 SMT Solver
K
Kasslin, Antton	An Optimization Modulo Theories-Based Approach to Cumulative Scheduling with Delays
Kolárik, Tomáš	Space Explanations of Neural Network Classification
L
Labbaf, Faezeh	Space Explanations of Neural Network Classification
Lipparini, Enrico	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
M
Meel, Kuldeep S.	Approximate SMT Counting Beyond Discrete Domains
N
Niemetz, Aina	A Catalog of SMT-LIB Benchmarks
P
Parno, Bryan	Instability Track for SMT-COMP
Pit-Claudel, Clément	A Conjecture Regarding SMT Instability
Polgreen, Elizabeth	Syntax-Guided Synthesis with Counterexample-Guided E-graphs: A Work-in-Progress Report
Preiner, Mathias	A Catalog of SMT-LIB Benchmarks
Przybocki, Benjamin	Being Polite is Not Enough (and Other Limits of Theory Combination)
R
Reynolds, Andrew	A Proposal for an OMT Extension to SMT-LIB
Ringert, Jan Oliver	On Writing SMT-LIB Scripts: Metrics and a New Dataset
S
Schneider, Rudi	Syntax-Guided Synthesis with Counterexample-Guided E-graphs: A Work-in-Progress Report
Schurr, Hans-Jörg	A Catalog of SMT-LIB Benchmarks
Shah, Amar	Instability Track for SMT-COMP
Sharygina, Natasha	Space Explanations of Neural Network Classification
Shaw, Arijit	Approximate SMT Counting Beyond Discrete Domains
Soaibuzzaman,	On Writing SMT-LIB Scripts: Metrics and a New Dataset
Steuwer, Michel	Syntax-Guided Synthesis with Counterexample-Guided E-graphs: A Work-in-Progress Report
Strejček, Jan	Deciding Satisfiability of Quantified Bitvector Formulae with BDDs
T
Tinelli, Cesare	A Catalog of SMT-LIB Benchmarks A Proposal for an OMT Extension to SMT-LIB SMT-LIB Discussion
Toledo, Guilherme	Being Polite is Not Enough (and Other Limits of Theory Combination)
Tourret, Sophie	Business Meeting
Tsiskaridze, Nestan	A Proposal for an OMT Extension to SMT-LIB
V
Villemot, Pierre	Constraint Propagation for Bit-Vectors in Alt-Ergo
W
Wand, Michael	Space Explanations of Neural Network Classification
Winterer, Dominik	SMT-COMP Presentation
Z
Zhou, Yi	Instability Track for SMT-COMP
Zohar, Yoni	Being Polite is Not Enough (and Other Limits of Theory Combination)

Disclaimer | Powered by EasyChair Smart Program