ABSTRACT. SMT solvers increasingly produce proof certificates to meet the trust requirements of safety-critical applications. However, eagerly justifying learned theory lemmas during solving constitutes a major performance bottleneck. Recent work mitigates this cost by emitting proof skeletons that record only SAT reasoning and unannotated theory lemmas, though existing approaches depend on new proof formats and specialized theory-specific tooling. We present a general approach that restricts SMT proof skeletons to core SMT reasoning: preprocessing, clausification, and unannotated theory lemmas. We develop external tools for SAT reasoning and proof trimming that reduce the number of theory lemmas requiring justification. An experimental evaluation using the SMT solver cvc5 on SMT-LIB benchmarks across the UF, LIA and LRA theories, with and without quantifiers, demonstrates faster solving and competitive checking performance compared to eager proof production, particularly on quantifier-free problems.

ABSTRACT. Eunoia is a logical framework designed for specifying the proofs and proof systems of SMT solvers, namely CVC5. We present a translation from a core fragment of Eunoia to the 𝜆Π-calculus modulo rewriting as implemented by the LambdaPi proof assistant. The translation is implemented by our tool eo2lp, which we use for generating LambdaPi encodings of (a) a large fragment of the Cooperating Proof Calculus (CPC), the Eunoia signature defining CVC5’s proof system, and (b) proofs produced by CVC5 on unsat problems from various fragments of SMT-LIB.

ABSTRACT. cvc5 is a state-of-the-art proof-producing SMT-solver, capable of solving formulas over a myriad of theories, including that of unicode strings. Matching regular expressions against candidate strings is done numerous times during the solving process of string constraints, and forms a bottleneck in proof-checking for unsatisfiable formulas. In this paper, we describe three approaches for checking regular expressions in proofs produced by cvc5. We also describe their implementation in the Eunoia proof-checking framework, and evaluate them on proofs produced by cvc5 for unsatisfiable SMT-LIB benchmarks for quantifier free logics containing strings.

ABSTRACT. SMT solvers are used in many safety critical applications. To provide evidence of the correctness of their answers some SMT solvers generate externally checkable proof certificates. We present a high performance checker for SMT proofs called Ethos. In contrast with other dedicated SMT proof checkers, Ethos does not implement a fixed proof calculus. Instead, it lets users provide their own proof calculi using the declarative language Eunoia which has been designed to make this easy and convenient by extending the familiar SMT-LIB syntax. We give a short overview of Eunoia and then focus on Ethos itself. We describe multiple optimization and implementation details that ensure that Ethos is fast and practical. We also evaluate Ethos on proofs generated by cvc5, showing that the flexibility of Ethos allows us to efficiently check fine-grained proofs, containing no proof holes, over all SMT-LIB logics without floating points.

ABSTRACT. 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 terminates in the presence of length constraints. To do this, we introduce extended word equations, a mathematical model of a word equation with partial information about length constraints. We then define extended Nielsen transformations, which adapt Nielsen transformations to the setting of extended word equations. We provide a partial characterization of when repeatedly applying extended Nielsen transformations to an extended word equation is guaranteed to terminate.

ABSTRACT. We consider the closure of three of the most classical combination properties, namely, stable infiniteness, gentleness and shininess (or, equivalently for decidable theories, strong politeness), under intersection and maximal combinability. Starting with these three properties, we compute every possible intersection, and then compute the maximal sets of theories that can be combined with each resulting intersection. We iterate this process until no new classes are identified. How many properties will we end up with?

ABSTRACT. We present a sequent calculus for Scott's theory of classes founded on positive free logic. Cut elimination, generalised subformula property and consistency are shown to hold, also in the intuitionistic variant. Eventually the calculus is extended to cover the original Zermelo's set theory Z without the axiom of choice by means of (systems of) rules. The calculus for Z preserves cut elimination, moreover, some of its subsystems and extensions are also provably consistent.

ABSTRACT. Word-level verification of arithmetic circuits with large operands typically relies on arbitrary-precision arithmetic, which can lead to significant computational overhead as word sizes grow. In this paper, we present a hybrid algebraic verification technique based on polynomial reasoning that combines linear and nonlinear rewriting. Our approach relies on multimodular reasoning using homomorphic images, where computations are performed in parallel modulo different primes, thereby avoiding any large-integer arithmetic. We implement the proposed method in the verification tool TalisMan2.0 and evaluate it on a suite of multiplier benchmarks. Our results show that hybrid multimodular reasoning significantly improves upon existing approaches.

ABSTRACT. The two-watched literal scheme, a core component of efficient CDCL (Conflict-Driven Clause Learning) implementations for propositional logic, is extended to first-order logic. Given a set of first-order clauses and a set of ground literals, our lifted two-watched literal scheme efficiently detects all propagating and false clauses with respect to the ground literals. We present the algorithm as a system of rules and prove its soundness and completeness. Additionally, we provide an implementation of the two-watched scheme, which outperforms a standard dynamic programming approach for detecting propagatable literals and conflicts, especially when dealing with long clauses.

ABSTRACT. Many digital systems are designed as collections of asynchronous processes orchestrated by a domain-specific scheduler. The verification of such scheduler-restricted asynchronous systems (SRA) is challenging due to process-process and process-scheduler interactions. In this paper, we tackle the problem of verifying configurable SRA. A configurable SRA describes an unbounded family of possible SRA, each resulting from an instantiation satisfying given configuration constraints; our goal is proving at once that every legal instantiation of a configurable SRA is correct. We propose a contract-based, deductive verification approach that combines (i) compositional proof rules that abstract the scheduler to prove top-level invariant properties, (ii) automatic summarizations of the methods invoked by the scheduler, (iii) simplification with respect to the nature of the space of configurations. The approach is grounded in (object-oriented) first order logic, requires reasoning over quantified statements, and leverages the Dafny software verifier as a backend. An experimental evaluation on industrial case studies demonstrates that the framework scales effectively and enables practical reasoning about complex parameterized behaviors.

ABSTRACT. We introduce proof nets for PiL, an extension of first-order multiplicative additive linear logic with new operators allowing a shallow encoding of processes in the 𝜋-calculus as formulas. We provide correctness criterion, sequentialization procedure, and a proof translation algorithm. We show that proof nets provide a canonical representation of sequent calculus derivations modulo rule permutations.

ABSTRACT. Ordered logics and type systems have been used in a variety of applications including computational linguistics, memory allocation, stream processing, logical frameworks, parametricity, and enforcing security protocols. In most formulations, ordered types are also linear, requiring each resource to be used exactly once. Prior work by Kanovich et al. has investigated calculi that relax this constraint through subexponentials within a linear ordered logic. We generalize their work by using adjoint modalities to combine logics with varying fine-grained structural properties, including weakening, left contraction, right contraction, left mobility, and right mobility. We show that the resulting sequent calculus admits cut elimination. We further provide a natural deduction formulation in which structural rules are implicit, and show that proof checking for this system is decidable. This makes it a suitable foundation for an expressive adjoint programming language or logical framework.

ABSTRACT. HyperLTL extends Linear Temporal Logic (LTL) by introducing trace variables that range over a domain of traces, and quantification over traces, making it possible to relate the assignments of propositional variables along multiple traces. This leads to HyperLTL becoming a predominant specification logic for hyperproperties, which are properties of sets of traces as opposed to individual traces. Satisfiability of HyperLTL is not recursively enumerable. Hence algorithmic methods cannot take the role of deduction for establishing validity. Furthermore, quantification over traces is restricted to be outside the scope of temporal operators in HyperLTL. In this paper, we consider HyperLTL∗, which is the generalization of HyperLTL by dropping this restriction. We pro- pose a proof system for HyperLTL∗, where completeness is achieved by allowing an ω-rule. Weaker finitary rules such as what can be useful for interactive theorem proving can be derived using the ω-rule. We give examples of the use of the proof system on complicated HyperLTL for- mulas which would be hard to derive automatically. We also discuss the expressiveness of HyperLTL∗ and the potential for using first-order logic theorem provers based on it. theorem provers based on it.

ABSTRACT. Hyperproperties specify the behavior of a system across multiple executions, and are an important extension of regular temporal properties. Most algorithms for deciding if a given system satisfy a given hyperproperty rely on a user-specified abstraction of the system. In this paper, we suggest a novel automatic abstraction-refinement algorithm for hyperproperties verification. Our approach is based on predicate abstraction and the recently introduced reduction of hyperproperties verification to satisfiability of Constrained Horn Clauses (CHCs). Moreover, it formalizes and uses CHC-based refinement for counterexamples in the shape of a directed acyclic graph. We implemented our new algorithm on top of the SMT solver Z3. Our experimental evaluation shows our automatic abstraction refinement algorithm can solve a variaty of hyperproperty verification problems, completely automatically. This is in contrast to other existing techniques that require a user-given abstraction.

ABSTRACT. Uniform interpolation is a strong form of interpolation providing an interpretation of propositional quantifiers within a propositional logic. Pitts’ seminal work establishes this property for intuitionistic propositional logic relying on a sequent calculus in which naïve backward proof-search terminates. This constructive approach has been adapted to a wide range of logics, including intuitionistic modal logics. Surprisingly, no intuitionistic modal logic with independent box and diamond has yet been shown to satisfy uniform interpolation. We fill in this gap by proving the uniform interpolation property for Constructive K (CK) and Wijesekera's K (WK). We build on Pitts' technique by exploiting existing terminating calculi for CK and WK, which we prove to eliminate cut, and formalise all our results in the proof assistant Rocq. Together, our results constitute the first positive uniform interpolation results for intuitionistic modal logics with diamond.

ABSTRACT. We study the problem of synthesizing programs from non-linear real arithmetic (NRA) specifications. Existing techniques, such as syntax-guided synthesis (SyGuS), fail to synthesize programs when the specification is unrealizable. We argue this is unsatisfactory in many situations, and aim to synthesize programs from arbitrary NRA specifications, such that for any input, the synthesized program either produces outputs satisfying the specification or correctly reports non-existence of any such output. To avoid rounding errors inherent in floating-point arithmetic, we restrict our programs to operate on rational inputs and outputs, thereby strictly generalizing beyond programs that work with floating-point numbers. We first show that our variant of the synthesis problem is as hard as a long-standing open problem in number theory, and that synthesizing loop-free programs from arbitrary NRA specifications with rational inputs and outputs is impossible in general. Second, we present a sound and complete synthesis algorithm for the case where the specification involves a single output variable. We also show that for realizable specifications, a program generated by SyGuS for NRA (treating inputs and outputs as reals) serves as a solution to our problem, where inputs and outputs are rationals. Third, we provide a sound (but necessarily incomplete) synthesis algorithm for the general case of specifications in NRA. We have implemented our approach in a prototype tool that solves many benchmarks beyond the reach of state-of-the-art SyGuS tools, even when we render the specification realizable.