4 papers
A Deeper Look at Depth: Stable Generation Accounting for Quantifier Reasoning
Can Cebeci, Nikolaj Bjørner, George Candea +1
SMT solvers make automated verification convenient. At the same time, solvers suffer from instability, whereby seemingly inconsequential changes to the input may cause a previously…
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…
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…
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…