7 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.…
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…
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…
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…
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…