SMT 2025: 23RD INTERNATIONAL WORKSHOP ON SATISFIABILITY MODULO THEORIES

This page contains an index consisting of author-provided keywords.

A
Alt-Ergo	Constraint Propagation for Bit-Vectors in Alt-Ergo
automated reasoning	A Catalog of SMT-LIB Benchmarks
B
benchmarks	A Catalog of SMT-LIB Benchmarks
Bit-Vectors	Constraint Propagation for Bit-Vectors in Alt-Ergo
bit-width reduction	Deciding Satisfiability of Quantified Bitvector Formulae with BDDs
C
cardinality constraints	A Few Exercises on the Complexity of Congruence Closure with Cardinality Constraints
case studies	A Conjecture Regarding SMT Instability
competition	SMT-COMP presentation
congruence closure	A Few Exercises on the Complexity of Congruence Closure with Cardinality Constraints
Constraint Propagation	Constraint Propagation for Bit-Vectors in Alt-Ergo
Cryptographic Hash Function	Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2
D
Dafny	Instability Track for SMT-COMP
data integration	A Catalog of SMT-LIB Benchmarks
database	A Catalog of SMT-LIB Benchmarks
dataset	On Writing SMT-LIB Scripts: Metrics and a new Dataset
debugging	A Conjecture Regarding SMT Instability Visualization of execution traces in Colibri 2 SMT solver
Differential Cryptanalysis	Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2
directions	Business Meeting
discussions	Business Meeting
discussions	SMT-LIB discussion
disequality propagation	A Few Exercises on the Complexity of Congruence Closure with Cardinality Constraints
E
e-graphs	Syntax-Guided Synthesis with CounterExample Guided E-graphs: A Work-In-Progress Report
enumerative	From MBQI to Enumerative Instantiation and Back
EUF	A Few Exercises on the Complexity of Congruence Closure with Cardinality Constraints
EUF + FCC	A Few Exercises on the Complexity of Congruence Closure with Cardinality Constraints
evolution	On Writing SMT-LIB Scripts: Metrics and a new Dataset
Exponentiation	Satisfiability Modulo Exponential Integer Arithmetic
F
F*	Instability Track for SMT-COMP
finite domains	A Few Exercises on the Complexity of Congruence Closure with Cardinality Constraints
finite rings	Evaluating Binary Polynomials using Subpolynomials
Flow Allocation	An Optimization Modulo Theories-based Approach to Cumulative Scheduling with Delays
Flow Evenness	An Optimization Modulo Theories-based Approach to Cumulative Scheduling with Delays
G
Gentleness	Being polite is not enough (and other limits of theory combination)
H
Hybrid SMT Formulas	Approximate SMT Counting Beyond Discrete Domains
I
incremental SAT	SAT Reasoning in CDCL(T) Solvers
Instability	A Conjecture Regarding SMT Instability Instability Track for SMT-COMP
Integer	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
Integer Arithmetic	Satisfiability Modulo Exponential Integer Arithmetic
interface	SAT Reasoning in CDCL(T) Solvers
IPASIR-UP	SAT Reasoning in CDCL(T) Solvers
L
Local Search	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
logging	Visualization of execution traces in Colibri 2 SMT solver
M
MBQI	From MBQI to Enumerative Instantiation and Back
MCSAT	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
MILP	An Optimization Modulo Theories-based Approach to Cumulative Scheduling with Delays
Model Counting	Approximate SMT Counting Beyond Discrete Domains
modulo arithemetic	Evaluating Binary Polynomials using Subpolynomials
N
Nelson-Oppen	Being polite is not enough (and other limits of theory combination)
neural networks	Space Explanations of Neural Network Classification
Nonlinear Arithmetic	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
novices	On Writing SMT-LIB Scripts: Metrics and a new Dataset
NP-completeness	A Few Exercises on the Complexity of Congruence Closure with Cardinality Constraints
O
observability	Visualization of execution traces in Colibri 2 SMT solver
observational equivalence	Syntax-Guided Synthesis with CounterExample Guided E-graphs: A Work-In-Progress Report
OMT	A Proposal for an OMT Extension to SMT-LIB An Optimization Modulo Theories-based Approach to Cumulative Scheduling with Delays
operation abstraction	Deciding Satisfiability of Quantified Bitvector Formulae with BDDs
Optimization Modulo Theories	A Proposal for an OMT Extension to SMT-LIB
P
Politeness	Being polite is not enough (and other limits of theory combination)
Polynomials	Evaluating Binary Polynomials using Subpolynomials
Probabilistic Term Generation	Quantifier Instantiations: To Mimic or To Revolt?
program synthesis	Syntax-Guided Synthesis with CounterExample Guided E-graphs: A Work-In-Progress Report
Program Verification	Instability Track for SMT-COMP
Projected Counting	Approximate SMT Counting Beyond Discrete Domains
Q
quantified bitvector	Deciding Satisfiability of Quantified Bitvector Formulae with BDDs
Quantifier Instantiation	Instability Track for SMT-COMP From MBQI to Enumerative Instantiation and Back Quantifier Instantiations: To Mimic or To Revolt?
R
Resource-Constrained Cumulative Scheduling	An Optimization Modulo Theories-based Approach to Cumulative Scheduling with Delays
S
Satisfiability Modulo Theories	Quantifier Instantiations: To Mimic or To Revolt?
Satisfiability Modulo Theory	Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2
SHA-2	Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2
Shininess	Being polite is not enough (and other limits of theory combination)
SMT	Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search A Catalog of SMT-LIB Benchmarks Visualization of execution traces in Colibri 2 SMT solver From MBQI to Enumerative Instantiation and Back Space Explanations of Neural Network Classification Satisfiability Modulo Exponential Integer Arithmetic Evaluating Binary Polynomials using Subpolynomials Business Meeting
SMT	SAT Reasoning in CDCL(T) Solvers Deciding Satisfiability of Quantified Bitvector Formulae with BDDs SMT-LIB discussion
SMT-COMP	Instability Track for SMT-COMP
SMT-COMP	SMT-COMP presentation
SMT-LIB	Constraint Propagation for Bit-Vectors in Alt-Ergo On Writing SMT-LIB Scripts: Metrics and a new Dataset A Proposal for an OMT Extension to SMT-LIB
SMT-LIB	SMT-LIB discussion
solvers	SMT-COMP presentation
SQLite	A Catalog of SMT-LIB Benchmarks
syntax-guided synthesis	Syntax-Guided Synthesis with CounterExample Guided E-graphs: A Work-In-Progress Report
T
Theory combination	Being polite is not enough (and other limits of theory combination)
theory of bit-vectors	Evaluating Binary Polynomials using Subpolynomials
Theory of BitVectors	Comparative Analysis of SMT Solvers for Differential Cryptanalysis of SHA-2
U
user interface	Visualization of execution traces in Colibri 2 SMT solver
V
Verus	Instability Track for SMT-COMP
vizualization	Visualization of execution traces in Colibri 2 SMT solver
X
XAI	Space Explanations of Neural Network Classification

Disclaimer | Powered by EasyChair Smart Program