ABSTRACT. Large Language Models (LLMs) have made significant progress in assisting users to query databases in natural language. While LLM-based techniques provide state-of-the-art results on many standard benchmarks, a number of challenging problems remain unresolved, which we discuss in this talk. First, we provide an overview of the Text-to-SQL problem and its interactive version, where the agent can ask the user clarification questions. Second, we consider the main challenges that the agent faces in solving this problem, including complex relationships, multi-turn conversations, ambiguous user queries, and weak evaluation procedures. Third, we explore formal verification–driven solutions for improving and evaluating Text-to-SQL. For example, a verification-driven performance evaluation of ten Text-to-SQL methods on the high-profile BIRD dataset suggests that existing methods often overlook differences between the generated query and the ground truth, leading to incorrect evaluation results. Finally, we discuss the possible logical formalization of the interactive Text-to-SQL problem and outline its remaining challenges.

ABSTRACT. Hyperproperties, which express system behaviors that relate multiple execution traces, cover a variety of important safety and secu- rity properties. Among these, hyperproperties of the form ∀∃.φ, where φ is an invariant or a SafetyLTL formula, capture many practically rele- vant specifications including noninterference, symmetry, and robust path planning. Despite their importance, efficient verification algorithms for such properties remain limited. In this paper, we propose novel verifica- tion algorithms for such ∀∃-hyperproperties. Our approach extends classical induction and k-induction techniques, widely used in single-trace verification, to the hyperproperty setting. We develop hyper-inductive reasoning principles that generalize the base and step cases of induction to sets of traces, refinement techniques to strengthen the property, and incremental approaches to increasing the bound of the k-induction. As a byproduct, we introduce hyper-(k)-inductive invariants, as certificates to witness satisfaction of ∀∃-hyperproperties over transition systems. We evaluate our approach on various bench- marks, demonstrating that our methods are complementary to state-of- the-art hyperproperty model checkers, and we analyze in which cases one option prevails over the others.

ABSTRACT. We present a benchmark suite and an accompanying experimental study that assesses the capabilities of modern Automated Theorem Provers (ATPs) for hyperproperty reasoning. Existing tools for reasoning about hyperproperties typically rely on specialised model checkers or a custom encoding to satisfiability modulo theories (SMT) solvers or first-order provers. Our suite constitutes the first systematic collection of SMT-LIB encodings spanning hyperproperty satisfiability, model checking, and software verification via Constrained Horn Clauses (CHCs). Using this suite, we evaluate state-of-the-art ATPs, including SMT solvers and first-order theorem provers, that support both arithmetic and quantified reasoning. Beyond measuring how different solvers perform, we summarize lessons we learned on what makes a good encoding and solver configuration for hyperproperties. The benchmark suite, translation scripts, and experimental setup are released as an open artifact, enabling reproducible evaluation and providing a foundation for future improvements in automated reasoning about hyperproperties.

ABSTRACT. Control invariance validates that dynamical systems have a control input that preserves a given property at all times. This paper introduces a set of sound axioms and proof rules in differential dynamic logic (dL) that enable verification of control invariance. First, the scalar and vector comparison principles, relating a system of differential equations to a comparison system such that invariance properties can be established more easily, are axiomatized in dL. This axiomatization primarily utilizes differential ghosts, which are proof-theoretic generalizations of comparison systems. Next, with the comparison principles serving as the basis, comparison invariants are introduced, and sound axioms and proof rules are developed. Comparison invariants reduce the question of control invariance to a functional inequality on its Lie derivative for a suitable class of functions, moreover, the right choice of function can result in decidable arithmetic. Furthermore, the perennially popular control barrier functions (CBFs) used in safety-critical control are shown to be a special instance of comparison invariants. This yields an axiomatization of CBFs that leads to a dedicated set of proof rules. The rules allow for the verification of CBFs, which are traditionally used for synthesizing safe controllers without verification. Lastly, comparison invariants are shown to unify several other safety verification techniques, including Darboux invariants and differential invariants, further cementing their versatility.

ABSTRACT. Proofs of UNSAT are a standard primitive in formal verification and software assurance. In many real-world settings, the proof itself encodes proprietary or security-sensitive information, making public disclosure undesirable. Zero-knowledge certification of UNSAT addresses this tension: it enables a prover to convince a verifier that no satisfying assignment exists, without revealing anything about the underlying proof beyond its validity. Luo et al. recently introduced ZKUNSAT, a protocol that achieves this goal by proving the validity of a weakened resolution proof in zero knowledge. ZKUNSAT demonstrates the feasibility of zero-knowledge certification; however, its scalability to larger, real-world instances is constrained by substantial prover memory overhead, limiting its real-world applicability.

Motivated by advances in UNSAT proof formats such as LRAT, which enable efficient plain-text verification, we present a preprocessing technique that improves the efficiency of ZKUNSAT without introducing additional leakage. Our approach normalizes the proof so that each derived clause is justified by a resolution chain of fixed public length k. This eliminates chain-length leakage and reduces prover memory usage. With k = 16, our method certifies roughly 62% more instances than baseline ZKUNSAT on the SAT 2002 competition benchmarks. Furthermore, for an equivalent number of certified instances, the memory footprint drops to under 25% of that required by the baseline.

ABSTRACT. Model-theoretic semantics comes with a computational counterpart: to check validity is to search for a countermodel, and tableaux, resolution, and satisfiability solvers make the semantics something one can run. Proof-theoretic semantics --- the younger paradigm in which meaning is given by inferential role rather than by denotation --- has no established counterpart. This paper proposes one: logic programming. We show that Sandqvist's base-extension semantics for intuitionistic propositional logic is executable in a precise sense. Bases are logic programs, and to each formula $\varphi$ we assign a goal $[[\varphi]]$ of a second-order hereditary Harrop language such that $\varphi$ is supported in a base $\mathcal{B}$ exactly when $[[\varphi]]$ is operationally derivable from $\mathcal{B}$ read as a program. The encoding is the Russell--Prawitz translation of the connectives with quantification restricted to atoms, and this restriction is not a limitation but the point: it is what the support clauses themselves demand. The correspondence is exact base by base, not merely at the level of validity, so that intuitionistic validity becomes the success of a single query against the empty program. Logic programming stands to proof-theoretic semantics as tableaux and satisfiability solvers stand to model-theoretic semantics.

ABSTRACT. In The Art of Computer Programming, Knuth benchmarked 10 encoding techniques for computing the chromatic number of the queen’s graph: the minimum number of colors needed to color the squares of an NxN chessboard so that no two squares sharing a row, column, or diagonal receive the same color. In this paper, we extend his analysis much further by comparing thousands of encodings for the same problem, which allows us to identify additional factors that are important for solver performance. We obtain 1584 encodings for this problem by varying (a) the constraints that encode which color is assigned to each cell, (b) the constraints that forbid the same color appearing in a row, column, or diagonal line, and (c) the symmetry-breaking constraints. We find that the three most impactful encoding factors are (i) the choice of symmetry-breaking constraints, (ii) enabling so-called clique hints, and (iii) enforcing that each cell is assigned exactly one color through blocked clauses. Furthermore, while Knuth proposed clique hints as an advantage of the order encoding, we show in fact that they can be effectively employed for the one-hot encoding as well.

ABSTRACT. Tarski's high school algebra problem asks whether every true identity concerning addition, multiplication, and exponentiation of positive integers follows from a list of 11 elementary identities. Surprisingly, Wilkie showed that the following identity is valid over the positive integers and yet does not follow from Tarski's axioms: \begin{align*} &\left((1+x)^y + (1+x+x^2)^y\right)^x \cdot \left((1+x^3)^x + (1+x^2+x^4)^x\right)^y = \\&\left((1+x)^x + (1+x+x^2)^x\right)^y \cdot \left((1+x^3)^y + (1+x^2+x^4)^y\right)^x. \end{align*} Gurevič gave an algebra on 59 elements that satisfies Tarski's axioms but not Wilkie's identity, and over the years several authors whittled down the size of such a countermodel, culminating in a countermodel of size 12 due to Burris and Yeats. On the other hand, Zhang proved that there is no countermodel with fewer than 11 elements. Using SAT, we prove that the smallest countermodels are of size 12, as conjectured by Burris and Yeats. Moreover, we show that there are exactly 8,957,952 countermodels on 12 elements up to isomorphism and provide a simple classification of them. Our SAT approach outperforms dedicated tools for finding countermodels in equational theories, namely Mace4 and SEM. Furthermore, using autoformalization, we prove the correctness of our main result in Lean.

ABSTRACT. Quantifier instantiation is currently the main approach to non-ground SMT solving: solvers generate ground instances and solve the resulting ground SMT problems with CDCL(T)-style reasoning. When a conflict is found, conflict analysis learns only a ground clause, even though the conflict comes from instances of non-ground clauses. Yet non-ground reasoning can give exponentially shorter proofs than purely ground reasoning. We propose a calculus that consists of ground instantiations, CDCL(T)-style rules, and non-ground conflict analysis. The solver reasons on ground instances, but the resolution steps of conflict analysis are performed on their original non-ground clauses. This produces learned clauses that are typically more general than the ground conflict. With a suitable strategy, the learned clauses are even non-redundant. We also show how chronological backtracking can be included in SMT solving. Our calculus gives a common setting for CDCL(T)-style SMT solving, a range of instantiation-based procedures, and non-ground clause learning, and we prove that it simulates CDCL, SCL(FOL), SCL(T), and even Resolution.

ABSTRACT. Symmetry breaking in graph search problems remains challenging: complete symmetry breaking constraints are typically exponential in size, while partial approaches trade pruning strength for scalability.

We introduce a strength-driven, redundancy-aware methodology for constructing compact partial symmetry breaking constraints based on graph patterns. Each pattern corresponds to a simple clause over equality literals and can be integrated directly into CP or SAT models.

Our approach incrementally selects strong, non-redundant patterns, yielding partial symmetry breaks that achieve substantial pruning while remaining compact. This provides a principled framework for deriving lightweight symmetry breaking constraints beyond previously studied constructions.

We evaluate the proposed constraints on graph instances with up to 25 vertices using a redundancy ratio metric. The resulting partial symmetry breaks constitute only a small fraction of the size of complete symmetry breaking constraints, while delivering significant performance improvements across several graph search benchmarks compared to previously defined partial symmetry breaking methods.

ABSTRACT. We present RTEC_rct, an interval-based stream reasoning system. RTEC_rct inherits from its predecessor RTEC_s a compositional and associative sequencing operator. RTEC_rct extends RTEC_s with `Reasoning Cut-off Tuples' (RCTs), a mechanism allowing for monotonic output given a monotonic input. RTEC_rct is also equipped with a bookkeeping policy, guided by RCTs, that identifies the minimal information for correct reasoning. Our empirical, reproducible evaluation on real and synthetic data from three application domains demonstrates the efficacy of RTEC_rct.

ABSTRACT. The calculus ALASCA extends superposition-based saturation proving with reasoning in Uninterpreted Functions and Linear Real Arithmetic (UFLRA). As efficiency of saturation algorithms depend on literal selection, simplification, and redundancy elimination, this paper improves reasoning in Uflra by introducing theory-specific notions and methods for all of these techniques. The implementation of these methods in the first-order theorem prover Vampire shows substantial gains in every tested benchmark category, solving a number of problems previously unsolved by any system.