SMT 2024: 22ND INTERNATIONAL WORKSHOP ON SATISFIABILITY MODULO THEORIES

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

A
Alethe	Reconstruction of SMT proofs with Lambdapi [original paper]
Algorithm Selection and Configuration	Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis [Presentation only]
arithmetic reasoning	An SMT-LIB Theory of Finite Fields [Original Paper]
Arrays	An SMT Theory for n-Indexed Sequences [Extended abstract]
Automated Reasoning	Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis [Presentation only]
automatic theorem provers	Reconstruction of SMT proofs with Lambdapi [original paper]
B
bit-vector	Challenges in Bit-Vector Reasoning
bit-vectors	A Bit-vector to Integer Translation with bv2nat and nat2bv [Extended abstract]
Bitvectors	CSB: A Counting and Sampling tool for Bit-vectors [Extended Abstract]
bv2nat and nat2bv	A Bit-vector to Integer Translation with bv2nat and nat2bv [Extended abstract]
C
Convexity	Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness [Presentation only]
cvc5	Challenges in Bit-Vector Reasoning
D
dolmen	Minimal logic detection and exporting smtlib problems with Dolmen [Extended abstract]
F
Fault Propagation	Efficient SMT-based Analysis of Failure Propagation - presentation only submission
Finite Degradation Structures (FDS)	Efficient SMT-based Analysis of Failure Propagation - presentation only submission
finite fields	An SMT-LIB Theory of Finite Fields [Original Paper]
H
Heuristic Search	Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis [Presentation only]
higher-order logic	The Hows and Whys of Higher-Order SMT
I
Implicit Predicate Abstraction	Verification Modulo Theories - presentation-only submission
Incremental SAT	Certifying Incremental SAT Solving [Presentation only]
int-blasting	A Bit-vector to Integer Translation with bv2nat and nat2bv [Extended abstract]
Invariant Checking	Verification Modulo Theories - presentation-only submission
IPASIR-UP	Certifying Incremental SAT Solving [Presentation only]
L
Lambdapi	Reconstruction of SMT proofs with Lambdapi [original paper]
logic detection	Minimal logic detection and exporting smtlib problems with Dolmen [Extended abstract]
LTL modulo Theories	Verification Modulo Theories - presentation-only submission
M
Machine Learning	Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis [Presentation only]
MCSat	Arrays Reasoning in MCSat [Original Paper]
Model Counting	CSB: A Counting and Sampling tool for Bit-vectors [Extended Abstract]
Model Enumeration	Efficient SMT-based Analysis of Failure Propagation - presentation only submission
N
Nelson Oppen	Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness [Presentation only]
P
Politeness	Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness [Presentation only]
prime fields	An SMT-LIB Theory of Finite Fields [Original Paper]
printing	Minimal logic detection and exporting smtlib problems with Dolmen [Extended abstract]
proof assistants	Reconstruction of SMT proofs with Lambdapi [original paper]
Proof checking	Certifying Incremental SAT Solving [Presentation only]
proof reconstruction	Reconstruction of SMT proofs with Lambdapi [original paper]
proof verification	Reconstruction of SMT proofs with Lambdapi [original paper]
Proofs	Certifying Incremental SAT Solving [Presentation only]
Q
Quantifier Elimination	Efficient SMT-based Analysis of Failure Propagation - presentation only submission
quantifier instantiation	The Hows and Whys of Higher-Order SMT
S
Sampling	CSB: A Counting and Sampling tool for Bit-vectors [Extended Abstract]
Satisfiability Modulo Theories	An SMT Theory for n-Indexed Sequences [Extended abstract]
Sequences	An SMT Theory for n-Indexed Sequences [Extended abstract]
SMT	Arrays Reasoning in MCSat [Original Paper] A Bit-vector to Integer Translation with bv2nat and nat2bv [Extended abstract] Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis [Presentation only] The Hows and Whys of Higher-Order SMT Challenges in Bit-Vector Reasoning SMT-LIB Report SMT-COMP Results and Tool Presentations SMT Business Meeting
SMT Organization	SMT Business Meeting
SMT Tools	SMT-COMP Results and Tool Presentations
SMT Workshop	SMT Business Meeting
SMT-COMP	SMT-COMP Results and Tool Presentations
SMT-LIB	An SMT-LIB Theory of Finite Fields [Original Paper] SMT-LIB Report
SMT-LIB Language	SMT-LIB Report
smtlib	Minimal logic detection and exporting smtlib problems with Dolmen [Extended abstract]
T
Theory Combination	Combining Combination Properties: An Analysis of Stable Infiniteness, Convexity, and Politeness [Presentation only]
Theory of Arrays	Arrays Reasoning in MCSat [Original Paper]
translation	Minimal logic detection and exporting smtlib problems with Dolmen [Extended abstract]
translation from bit-vectors to integers	A Bit-vector to Integer Translation with bv2nat and nat2bv [Extended abstract]
translation of quantified formulas and arrays	A Bit-vector to Integer Translation with bv2nat and nat2bv [Extended abstract]
V
Verification Modulo Theories	Verification Modulo Theories - presentation-only submission
VMT format	Verification Modulo Theories - presentation-only submission
W
Weakly Equivalent Arrays	Arrays Reasoning in MCSat [Original Paper]

Disclaimer | Powered by EasyChair Smart Program