Publications

2025

1. Preprint

   Abstractions of Sequences, Functions and Operators

   Louis Rustenholz, Pedro Lopez-Garcia, and Manuel V. Hermenegildo

   Jul 2025

   Presented at CSV’25. Under consideration for publication in STTT.

   Abs arXiv Bib PDF Slides

   We present theoretical and practical results on the order theory of lattices of functions, focusing on Galois connections that abstract (sets of) functions – a topic known as higher-order abstract interpretation. We are motivated by the challenge of inferring closed-form bounds on functions which are defined recursively, i.e. as the fixed point of an operator or, equivalently, as the solution to a functional equation. This has multiple applications in program analysis (e.g. cost analysis, loop acceleration, declarative language analysis) and in hybrid systems governed by differential equations. Our main contribution is a new family of constraint-based abstract domains for abstracting numerical functions, B-bound domains, which abstract a function f by a conjunction of bounds from a preselected set of boundary functions. They allow inferring highly non-linear numerical invariants, which classical numerical abstract domains struggle with. We uncover a convexity property in the constraint space that simplifies, and, in some cases, fully automates, transfer function design. We also introduce domain abstraction, a functor that lifts arbitrary mappings in value space to Galois connections in function space. This supports abstraction from symbolic to numerical functions (i.e. size abstraction), and enables dimensionality reduction of equations. We base our constructions of transfer functions on a simple operator language, starting with sequences, and extending to more general functions, including multivariate, piecewise, and non-discrete domains.

   @misc{absfun-preprint,
     author = {Rustenholz, Louis and Lopez-Garcia, Pedro and Hermenegildo, Manuel V.},
     title = {{A}bstractions of {S}equences, {F}unctions and {O}perators},
     year = {2025},
     month = jul,
     eprint = {2507.23151},
     archiveprefix = {arXiv},
     primaryclass = {cs.PL},
     note = {Presented at CSV'25. Under consideration for publication in STTT.}
   }

2024

1. Conference Paper

   An Order Theory Framework of Recurrence Equations for Static Cost Analysis – Dynamic Inference of Non-Linear Inequality Invariants

   Louis Rustenholz, Pedro López-García, José F. Morales, and Manuel V. Hermenegildo

   In Proceedings of the 31st Static Analysis Symposium (SAS 2024) , Oct 2024

   Abs arXiv Bib PDF Video Code Slides

   Recurrence equations have played a central role in static cost analysis, where they can be viewed as abstractions of programs and used to infer resource usage information without actually running the programs with concrete data. Such information is typically represented as functions of input data sizes. More generally, recurrence equations have been increasingly used to automatically obtain non-linear numerical invariants. However, state-of-the-art recurrence solvers and cost analysers suffer from serious limitations when dealing with the (complex) features of recurrences arising from cost analyses. We address this challenge by developing a novel order-theoretical framework where recurrences are viewed as operators and their solutions as fixpoints, which allows leveraging powerful pre/postfixpoint search techniques. We prove useful properties and provide principles and insights that enable us to develop techniques and combine them to design new solvers. We have also implemented and experimentally evaluated an optimisation-based instantiation of the proposed approach. The results are quite promising: our prototype outperforms state-of-the-art cost analysers and recurrence solvers, and can infer tight non-linear lower/upper bounds, in a reasonable time, for complex recurrences representing diverse program behaviours.

   @inproceedings{order-recsolv-sas24,
     author = {Rustenholz, Louis and López-García, Pedro and F.~Morales, José and V.~Hermenegildo, Manuel},
     title = {{A}n {O}rder {T}heory {F}ramework of {R}ecurrence {E}quations for {S}tatic {C}ost {A}nalysis – {D}ynamic {I}nference of {N}on-{L}inear {I}nequality {I}nvariants},
     booktitle = {Proceedings of the 31st Static Analysis Symposium (SAS 2024)},
     year = {2024},
     month = oct,
     publisher = {Springer},
     series = {LNCS},
     volume = {14995},
     doi = {10.1007/978-3-031-74776-2_14},
     paper_presentation_city = {Pasadena, CA},
     paper_presentation_country = {USA}
   }

2. Journal Article

   A Machine Learning-based Approach for Solving Recurrence Relations and its use in Cost Analysis of Logic Programs

   Louis Rustenholz, Maximiliano Klemen, Miguel Ángel Carreira-Perpiñán, and Pedro López-García

   TPLP, 2024

   Abs arXiv Bib HTML PDF

   Automatic static cost analysis infers information about the resources used by programs without actually running them with concrete data, and presents such information as functions of input data sizes. Most of the analysis tools for logic programs (and many for other languages), as CiaoPP, are based on setting up recurrence relations representing (bounds on) the computational cost of predicates, and solving them to find closed-form functions. Such recurrence solving is a bottleneck in current tools: many of the recurrences that arise during the analysis cannot be solved with state-of-the-art solvers, including Computer Algebra Systems (CASs), so that specific methods for different classes of recurrences need to be developed. We address such a challenge by developing a novel, general approach for solving arbitrary, constrained recurrence relations, that uses machine-learning (sparse-linear and symbolic) regression techniques to guess a candidate closed-form function, and a combination of an SMT-solver and a CAS to check if it is actually a solution of the recurrence. Our prototype implementation and its experimental evaluation within the context of the CiaoPP system show quite promising results. Overall, for the considered benchmarks, our approach outperforms state-of-the-art cost analyzers and recurrence solvers, and solves recurrences that cannot be solved by them.

   @article{mlrec-tplp2024,
     title = {{A} {M}achine {L}earning-based {A}pproach for {S}olving {R}ecurrence {R}elations and its use in {C}ost {A}nalysis of {L}ogic {P}rograms},
     author = {Rustenholz, Louis and Klemen, Maximiliano and Carreira-Perpiñán, Miguel Ángel and López-García, Pedro},
     year = {2024},
     journal = {TPLP},
     month = {},
     volume = {24},
     number = {6},
     pages = {1163--1207},
     doi = {10.1017/S1471068424000413},
   }

2021

1. Conference Paper

   Static Analysis of ReLU Neural Networks with Tropical Polyhedra

   Eric Goubault, Sébastien Palumby, Sylvie Putot, Louis Rustenholz, and Sriram Sankaranarayanan

   In Proceedings of the 28th Static Analysis Symposium (SAS 2021) , Oct 2021

   Abs arXiv Bib PDF Video Video (2) Slides

   This paper studies the problem of range analysis for feedforward neural networks, which is a basic primitive for applications such as robustness of neural networks, compliance to specifications and reachability analysis of neural-network feedback systems. Our approach focuses on ReLU (rectified linear unit) feedforward neural nets that present specific difficulties: approaches that exploit derivatives do not apply in general, the number of patterns of neuron activations can be quite large even for small networks, and convex approximations are generally too coarse. In this paper, we employ set-based methods and abstract interpretation that have been very successful in coping with similar difficulties in classical program verification. We present an approach that abstracts ReLU feedforward neural networks using tropical polyhedra. We show that tropical polyhedra can efficiently abstract ReLU activation function, while being able to control the loss of precision due to linear computations. We show how the connection between ReLU networks and tropical rational functions can provide approaches for range analysis of ReLU neural networks. We report on a preliminary evaluation of our approach using a prototype implementation.

   @inproceedings{relunn-by-trop-sas21,
     author = {Goubault, Eric and Palumby, S{\'e}bastien and Putot, Sylvie and Rustenholz, Louis and Sankaranarayanan, Sriram},
     editor = {Dr{\u{a}}goi, Cezara and Mukherjee, Suvam and Namjoshi, Kedar},
     title = {Static Analysis of ReLU Neural Networks with Tropical Polyhedra},
     booktitle = {Proceedings of the 28th Static Analysis Symposium (SAS 2021)},
     year = {2021},
     month = oct,
     publisher = {Springer International Publishing},
     address = {Cham},
     pages = {166--190},
     isbn = {978-3-030-88806-0}
   }

2. Book

   L’équation aux S-unités – Voyage géométrique en théorie des nombres

   Khalil Bendriss, Paul Boisseau, Adam David, Félix Rebotier, and Louis Rustenholz

   Éditions Ellipses, Sep 2021

   Book version of a project on Geometrical and Algebraic Number Theory

   Preface by Diego Izquierdo

   Abs Bib HTML

   Le charme de l’arithmétique vient de la simplicité de ses énoncés jointe à la difficulté de ses preuves. L’équation aux S-unités consiste à trouver les solutions de l’égalité x + y = 1, où x et y sont des nombres entiers dont on a fixé les facteurs premiers. Combien de solutions a-t-elle ? Malgré son apparence élémentaire, cette question fait appel à plusieurs siècles de développement où se sont entrecroisés algèbre, géométrie et analyse. Ce sera finalement dans un article fondateur de 1996 que l’approche audacieuse des mathématiciens Beukers et Schlickewei permettra d’obtenir une réponse.
   
   Dans cet ouvrage, on se propose d’expliquer pas à pas cette fascinante démonstration pour permettre au plus grand nombre de s’approprier les idées qui l’animent. Au cours de cette élucidation, qui constitue le fil rouge du texte, le lecteur découvrira les notions clés qui ont jalonné l’histoire de l’étude des nombres, de Diophante à nos jours. Les outils et concepts fondamentaux de l’arithmétique seront exposés progressivement, avec des exemples qui serviront à les motiver. En plus d’introduire toutes les notions classiques, comme les anneaux de Dedekind, les corps p-adiques, ou encore la théorie des hauteurs, ce livre a vocation à présenter les grands mouvements qui ont forgé la théorie des nombres modernes. Il s’adresse donc à tous ceux, étudiants en troisième année de licence ou curieux de mathématiques, qui veulent découvrir cette discipline telle qu’elle se pratique de nos jours.

   @book{rustenholz-s-unites-ellipses,
     author = {Bendriss, Khalil and Boisseau, Paul and David, Adam and Rebotier, Félix and Rustenholz, Louis},
     editor = {{Éditions Ellipses}},
     title = {{L}’équation aux {S}-unités -- {V}oyage géométrique en théorie des nombres},
     year = {2021},
     month = sep,
     isbn = {9782340056701},
     note = {Book version of a project on Geometrical and Algebraic Number Theory},
     supervisornote = {Preface by Diego Izquierdo},
   }