12 citations · 13 across the 8 of their papers we have counts for
11 papers
Automated Reasoning with Nested Datatypes
Tomer Hakak, Yoni Zohar, Andrew Reynolds +2
We introduce a theory of nested datatypes. The theory is obtained by restricting the naive combination of datatypes and arrays, so as to prevent non-standard models from emerging.…
CSLib: The Lean Computer Science Library
Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi +5
We introduce CSLib, an open-source framework for proving computer-science-related theorems and writing formally verified code in the Lean proof assistant. CSLib aims to be for comp…
Self-Supervised Bootstrapping of Action-Predictive Embodied Reasoning
Milan Ganai, Katie Luo, Jonas Frey +2
Embodied Chain-of-Thought (CoT) reasoning has significantly enhanced Vision-Language-Action (VLA) models, yet current methods rely on rigid templates to specify reasoning primitive…
Solving Set Constraints with Comprehensions and Bounded Quantifiers
Mudathir Mohamed, Nick Feng, Andrew Reynolds +3
Many real applications problems can be encoded easily as quantified formulas in SMT. However, this simplicity comes at the cost of difficulty during solving by SMT solvers. Differe…
Integer Reasoning Modulo Different Constants in SMT
Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor +4
This paper presents a new refutation procedure for multimodular systems of integer constraints that commonly arise when verifying cryptographic protocols. These systems, involving…
The termination of Nielsen transformations applied to word equations with length constraints
Benjamin Przybocki, Clark Barrett
Nielsen transformations form the basis of a simple and widely used procedure for solving word equations. We make progress on the problem of determining when this procedure terminat…
Towards SMT Solver Stability via Input Normalization
Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz +4
In many applications, SMT solvers are utilized to solve similar or identical tasks over time. Significant variations in performance due to small changes in the input are not uncomm…
The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems
Benjamin Przybocki, Guilherme Toledo, Yoni Zohar +1
Stable infiniteness, strong finite witnessability, and smoothness are model-theoretic properties relevant to theory combination in satisfiability modulo theories. Theories that are…
Verifying SQL Queries using Theories of Tables and Relations
Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli +1
We present a number of first- and second-order extensions to SMT theories specifically aimed at representing and analyzing SQL queries with join, projection, and selection operatio…
Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems
David "davidad" Dalrymple, Joar Skalse, Yoshua Bengio +14
Ensuring that AI systems reliably and robustly avoid harmful or dangerous behaviours is a crucial challenge, especially for AI systems with a high degree of autonomy and general in…
Generalized Optimization Modulo Theories
Nestan Tsiskaridze, Clark Barrett, Cesare Tinelli
Optimization Modulo Theories (OMT) has emerged as an important extension of the highly successful Satisfiability Modulo Theories (SMT) paradigm. The OMT problem requires solving an…