3 papers
cs.LO2026
Parallel SMT Solving via Dynamic Partitioning, Core-Guided Pruning, and Backbone Detection
Ilana Shapiro, Sorin Lerner, Nikolaj Bjørner
Exploiting parallelism in modern CPU architectures remains a longstanding challenge in optimizing SMT solvers. We introduce a novel framework for parallel SMT solving that uses fee…
cs.LO2025
Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
Petra Hozzová, Nikolaj Bjørner
Program synthesis is the task of automatically constructing a program conforming to a given specification. In this paper we focus on synthesis of single-invocation recursion-free f…
cs.NI2025
LLM-Based Config Synthesis requires Disambiguation
Rajdeep Mondal, Nikolaj Bjorner, Todd Millstein +2
Beyond hallucinations, another problem in program synthesis using LLMs is ambiguity in user intent. We illustrate the ambiguity problem in a networking context for LLM-based increm…