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.

Mon 21 Oct

Displayed time zone: Pacific Time (US & Canada) change

11:00 - 12:30
Verification cost and quantitative analysisSAS at San Gabriel
Chair(s): Sébastien Bardin CEA LIST, University Paris-Saclay
11:00
30m
Full-paper
Verification of programs with ADTs using Shallow Horn Clauses
SAS
Théo Losekoot , Thomas Genet IRISA, Univ Rennes, Thomas P. Jensen INRIA Rennes
Pre-print
11:30
30m
Full-paper
An Order Theory Framework of Recurrence Equations for Static Cost Analysis – Dynamic Inference of Non-Linear Inequality Invariants
SAS
Louis Rustenholz Universidad Politécnica de Madrid (UPM) and IMDEA Software Institute, Pedro López-García IMDEA Software Institute, José Morales IMDEA Software Institute, Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute
Link to publication Pre-print File Attached
12:00
30m
Full-paper
Quantitative Static Timing Analysis
SAS
Denis Mazzucato INRIA & École Normale Supérieure, Marco Campion INRIA & École Normale Supérieure | Université PSL, Caterina Urban Inria - École Normale Supérieure
Pre-print