PaperlayerView exact revision on arXiv

Source-linked AI summary

DueList: A Theory of Lists with Combinators for SMT Solvers

Pierre Goutagny, Aymeric Fromherz, Raphaël Monat

arXiv:2609.29962v1cs.PL

TL;DR

SMT solvers struggle with symbolic reasoning about recursive lists, despite their use in functional programs with higher-order combinators. DueList applies abstraction refinement to arbitrarily sized abstract lists, and evaluation on a diverse benchmark corpus finds that it extends solver reasoning and outperforms existing solvers in most previously supported cases.

  • Problem

    SMT solvers struggle with inductively defined lists and their higher-order operations, making symbolic reasoning about these widely used structures difficult.

    Source: §1 · p. 1, §2 · p. 3

  • Method

    DueList uses abstraction refinement over symbolic, arbitrarily sized abstract lists manipulated through len, map, and fold combinators.

    Source: §1 · p. 1, §9 · p. 25

  • Results

    DueList extends existing solvers’ reasoning capabilities and outperforms them in the vast majority of previously supported list-related problems.

    Source: §9 · p. 25

  • Takeaways & Limitations

    The evaluation demonstrates benefits from DueList’s specialized list theory and solving procedure on a diverse corpus drawn from prior work and real-world programs.

    Source: §9 · p. 25

    Some longer-running benchmarks do not benefit from the optimizations, including indexOf and taxi dropoff problems whose shapes resist the current optimizations.

    Source: §7.3 · p. 18

Abstract

from arXiv · show

Formal verification tools commonly rely on SMT solvers to automatically reason about programs, leveraging a range of logical theories, e.g., linear integer arithmetic, arrays, or strings, to encode program constructs and verification conditions. Despite recent advances, such solvers still struggle when reasoning about recursive data structures such as lists, which are pervasive in modern functional languages. Additionally, lists are commonly used in conjunction with higher-order combinators to, e.g., generically apply a function to all elements of the list. In this work, we provide first-class support for reasoning about lists within SMT solvers. We focus on lists of arbitrary size that, following the map-reduce paradigm, can be manipulated exclusively through a set of abstract combinators. To this end, we introduce DueList, an abstraction-refinement approach geared towards list reasoning, which we implement on top of off-the-shelf SMT solvers. To evaluate the efficiency of our approach, we assemble a diverse set of 752 benchmarks curated from previous works and real-world programs, and compare DueList against state-of-the-art solvers such as Z3 and CVC5. Our experimental evaluation shows that DueList extends reasoning facilities of existing solvers, allowing to conclude about the (un)satisfiability of a larger range of problems, while outperforming existing solvers in the vast majority of previously supported cases.

1 Introduction

DueList targets symbolic lists of arbitrary size by restricting operations to generic combinators and solving constraints through abstraction refinement. Across 752 benchmarks, it extends existing solvers’ reasoning and outperforms them in most previously supported cases.

1 Introduction

  • SMT solvers struggle with inductively defined lists and higher-order operations, while existing approaches trade automation or arbitrary-length reasoning for more restricted encodings.The cited alternatives use annotations or contracts, fixed-size lists, or generic algebraic-datatype procedures that the paper reports do not scale well.Source: §1 · p. 1
  • DueList reasons about symbolic, arbitrarily sized lists by restricting operations to generic combinators rather than exposing list representations.The motivating example uses map to assign custody scores and fold to sum them across children.Source: §1 · pp. 1–2
  • Its abstraction-refinement approach combines over-approximating and under-approximating encodings to decide unsatisfiability, find models, or refine the search space.The prototype builds on off-the-shelf SMT solvers and uses length and list-shape abstractions.Source: §1 · p. 2
  • Across 752 benchmarks, DueList scales on parametric problems and outperforms other solvers in the vast majority of previously supported cases.The corpus draws on prior list-reasoning and functional-synthesis work, plus OCaml and Catala compiler tests.Source: §1 · p. 2

2 Extending SMT-LIB with abstract lists and combinators

This section motivates a restricted theory of abstract lists and introduces its combinators and SMT-LIB syntax. The theory avoids recursive list definitions while retaining operations useful for collection programs.

2 Extending SMT-LIB with abstract lists and combinators

  • An SMT-LIB extension adds a parameterized List datatype and list combinators, using existing sorts, non-recursive definitions, and lambda expressions.The extension also provides encodings into standard SMT theories, including arrays and datatypes.Source: §2 · pp. 3–4
  • Recursive list definitions and pattern matching make symbolic reasoning difficult, including reasoning about lengths after operations such as append or filter.Fixed-size case splits are commonly used to work around SMT solvers’ limits on inductive reasoning.Source: §2 · p. 3
  • The proposed theory treats lists as abstract values and exposes len, map, and fold instead of nil/cons construction and pattern matching.fold reduces a list to a scalar by chaining a function over its elements from an initial value.Source: §2 · p. 3
  • The combinators are opaque primitive operations in a quantifier-free theory, and non-recursive datatypes let them implement operations such as exists, for_all, sum, and contains.The paper identifies fold as expressive enough to combine elements while maintaining an accumulator.Source: §2 · p. 3

3 DueList: An Overview

DueList extends existing SMT solvers with list-specific abstraction refinement, then illustrates the solver interaction on a running example. Its architecture combines sound over-approximation with restricted concrete checks and feedback.

3.1 Architecture

  • DueList takes constraints over lists and other supported theories, translates them into constraints for an existing SMT solver, and lifts returned models to the input list variables.Its core procedure refines list-specific constraints into the underlying solver’s theory; it does not interact directly with DPLL’s algorithm.Source: §3.1 · pp. 4–6
  • The over-approximating solver uses sound length and shape abstractions to prove unsatisfiability; the under-approximating solver checks a hinted subset and supplies feedback when it cannot establish satisfiability.The architecture first rewrites constraints to remove intermediate lists, then repeats refinement until a conclusion or timeout.Source: §3.1 · pp. 5–6

3.2 DueList by Example

  • In the example, a length abstraction yields a candidate list length of one, but its concrete check rules that length out; refinement then finds length two, where the under-approximating solver establishes satisfiability.The approach passes the resulting model back as a model for the list variable.Source: §3.2 · pp. 6–8

4 Reasoning through Length Abstractions

DueList uses length abstractions to reason about list constraints, then concretizes candidate lengths into SMT queries and refines the search using solver feedback. Fold-specific abstractions and a feedback loop support reasoning beyond fixed-size list encodings.

4.1 Over-approximation by Length Abstraction

  • Length abstraction replaces symbolic lists with integer lengths, while each fold expression receives a shared unconstrained symbolic value to preserve relationships between identical folds.The translation recursively handles list expressions and leaves non-list variables and literals unchanged.Source: §4.1 · pp. 8–9
  • A sound over-approximation makes UNSAT results conclusive; SAT models instead provide length hints for the under-approximating solver.Soundness is established by showing that satisfiable inputs have satisfiable translated problems.Source: §4.1 · p. 9

4.2 Fixed-Length Under-approximations

  • Fixed-length rules instantiate each list as symbolic elements, rewrite its combinators, and remove list values from the resulting SMT query.Map applies its function pointwise, fold is unfolded, and length becomes a constant; the figure presents selected translation rules.Source: §4.2 · p. 10, Figure 5

4.3 Feedback Loop

  • When a fixed-length query is UNSAT, DueList excludes that length and repeats the search until it decides satisfiability or unsatisfiability, or times out with UNKNOWN.The feedback loop adds excluded lengths to the over-approximating query before generating another length model.Source: §4.3 · pp. 10–11
  • Length exploration leaves ordering to the SMT solver; forcing increasing lengths guarantees shortest-list models for satisfiable instances, while binary search requires monotonicity analysis.Binary search strategies are left as future work.Source: §4.3 · p. 11

5 Abstracting over Fold Combinators

Length-only abstractions omit list contents, while coarse element summaries can make fold reasoning imprecise. DueList introduces fold-specific abstractions, including list summarization and reasoning about the image of a fold function.

5 Abstracting over Fold Combinators

  • Fold-specific abstractions aim to retain precision because coarse list-element summaries can make fold abstractions imprecise, unlike array operations dominated by element access or updates.Length abstractions alone do not capture list contents.Source: §5 · p. 11

5.1 List Summarization

  • When a fold admits neutral-element padding, a list can be summarized by its length and head; for addition, the sum can occupy the head and zeros pad the remaining positions.This length-independent rewrite avoids many symbolic variables and constraints for large lists.Source: §5.1 · pp. 11–12

5.2 fold Reachability

  • For nonempty lists, DueList over-approximates a fold by the image of its function; if that abstraction is UNSAT, the original problem is UNSAT, while otherwise other heuristics continue.For empty lists, the fold is rewritten as its initial value.Source: §5.2 · p. 13

6 Simplifying and Optimizing SMT Queries

Section 6 reduces SMT-query cost through list-specific rewriting and solver optimizations. Deforestation reduces variables and constraints, while incremental solving and preprocessing target solver overhead.

6.1 SMT Variable Reduction Through Deforestation

  • Inlining map into fold can enlarge the unfolded expression while reducing SMT variables and constraints; the running example falls from |l| + 1 constraints to one.The original encoding creates intermediate variables for the mapped list; inlining removes them.Source: §6.1 · pp. 13–14, Figure 8, Figure 9
  • Nested maps can be composed into one map, while len (map f l) simplifies to len l because map preserves list length.The map-of-map rule is especially useful when maps are nested inside len or fold.Source: §6.1 · p. 14
  • Because DueList's language is pure, rewriting rules can be applied in any order; in practice, it reduces nested maps first, then applies fold-of-map and len-of-map once.After nested maps are reduced, the outer fold or len rule need only be applied once.Source: §6.1 · p. 14

6.2 SMT-Solving Optimizations

  • Incremental solving reuses solver state as refinement adds constraints, while preprocessing removes redundant or spurious constraints and simplifies trivial ones, sometimes avoiding a solver query.The preprocessing pass can detect trivial satisfiable or unsatisfiable cases before querying the solver.Source: §6.2 · p. 15

7 Experimental Evaluation

The evaluation tests DueList on a curated, parameterized corpus, examines its optimizations, and compares it with existing solvers. DueList outperforms existing tools in most evaluated cases, while the comparisons also reveal task-specific limits and solver-encoding differences.

7.1 Implementation

  • DueList is implemented in 4,000 lines of OCaml and uses Z3 4.15.2 as its backend; experiments average four runs with a 30-second query timeout.The experiments ran on an Intel Core i7-12700 with 128GB of DDR5 RAM.Source: §7.1 · p. 15

7.2 A Corpus of List Problems

  • The corpus contains 39 parametric benchmarks—23 satisfiable and 16 unsatisfiable—expanded into 752 files by varying list-length parameters.For satisfiable problems, the parameter lower-bounds list lengths; for unsatisfiable problems, it upper-bounds them.Source: §7.2 · p. 16
  • The benchmarks adapt list-intensive computations from Catala, SyGuS-inspired problems, and OCaml library functions, alongside custom tests of targeted patterns.Examples include social-benefit computations, array-style operations, and folds implementing functions such as exists, nth, and filter.Source: §7.2 · p. 17

7.3 Ablation Study

  • Deforestation significantly speeds up composed-combinator problems; summarization can trivialize Checksum, while the combined optimizations make List.filter time out.For unsatisfiable Swap01, the text attributes deforestation’s impact to the large number of constraints generated by the List encoder.Source: §7.3 · p. 18
  • Some long-running benchmarks receive no benefit from the optimizations: indexOf lacks deep combinator composition, and Taxi dropoff resists efficient summarization.The authors describe DueList’s modular architecture as allowing future heuristics to target such issues.Source: §7.3 · p. 18

7.4 Comparison with State-of-the-art Solvers

  • DueList outperforms existing tools in the vast majority of satisfiable and unsatisfiable cases; Z3’s array encoding is more efficient but seldom works.The comparison covers DueList, three Z3 encodings, and CVC5’s datatype encoding; CVC5 times out on all but one benchmark.Source: §7.4 · p. 21, Table 2 · p. 22
  • Within the same time budget, DueList solves unsatisfiable instances at least four times larger than Z3’s sequence encoding, which provides actionable results only through N=70.On satisfiable problems, sequence and datatype encodings require at least an order of magnitude more time than DueList except on the Running example.Source: §7.4 · p. 23

8 Related work

Existing SMT theories offer different trade-offs for representing collections, but none provides the same combination of abstract list operations and symbolic lengths described for DueList. The related work also contrasts DueList’s abstract representation with approaches that analyze low-level data structures.

Arrays

  • Arrays support flexible indexing and element types but lack intrinsic length; DueList offers a higher-level interface while also encoding store and select through fold.The paper notes that nested-list capabilities have not been explored.Source: §8 · p. 24

Strings

  • String theories support symbolic lengths, but their finite alphabet and structure-oriented operations do not provide a fold-like operation over general list contents.The paper notes that Z3str4 handles symbolic-length strings using a Length Abstraction Solver, similar to DueList’s design.Source: §8 · p. 24

Algebraic datatypes

  • Algebraic datatypes encode symbolic-size lists and their contents recursively, but this encoding requires quantifiers and the surveyed solvers usually could not prove UNSAT on bounded-state problems.The passage also describes catamorphism, solvable tuple-pattern, and quantifier-free datatype approaches, each with distinct scope.Source: §8 · p. 24

Other SMT-based approaches

  • Sequence theories generalize strings and arrays, while Rosette supports symbolic elements only at concrete list lengths, leaving users to choose those lengths.The paper also surveys encodings of comprehensions, symbolic widths, and SyGuS problems.Source: §8 · pp. 24–25

Client applications of DueList

  • DueList could support symbolic execution, including concolic execution of Catala programs, and may help symbolic execution for functional languages and larger deductive verification tasks.These are described as potential applications.Source: §8 · p. 25

Program analysis for data structures

  • Unlike program-analysis methods that inspect low-level data-structure representations, DueList trades that representation detail for efficiency by keeping lists abstract and restricting the input language.The passage relates its fold abstraction to data-structure summarization techniques.Source: §8 · p. 25

9 Conclusion

DueList brings abstraction-refinement list reasoning to off-the-shelf SMT solvers through abstract lists and standard combinators. On benchmarks from prior work and real programs, it extends existing solvers’ reasoning capabilities and outperforms them in most previously supported cases.

Conclusion

  • DueList applies an abstraction-refinement loop to solve problems over abstract lists using standard combinators including len, map, and fold.Its over- and under-approximating solvers use length abstractions and conditional fold reductions to translate list constraints into list-free queries for SMT solvers.Source: §9 · p. 25
  • DueList extends existing solvers’ reasoning capabilities and outperforms them in the vast majority of previously supported list-related problems.The paper describes its evaluation as using a diverse corpus of size-parametric benchmarks from prior work and real-world programs.Source: §9 · p. 25
  • The benchmark corpus is intended to evaluate the approach and foster future research on list reasoning.Future work targets unsupported combinators for pairs of lists, technical limits on lists of lists, and support for more SMT solvers.Source: §9 · p. 25
Loading 2609.29962v1…