Determining upper bounds on the time complexity of a program is
a fundamental problem with a variety of applications, such as performance de-
bugging, resource certification, and compile-time optimizations. Automated tech-
niques for cost analysis excel at bounding the resource complexity of programs
that use integer values and linear arithmetic. Unfortunately, they fall short when
execution traces become more involved, esp. when data dependencies may affect
the termination conditions of loops. In such cases, state-of-the-art analyzers have
shown to produce loose bounds, or even no bound at all.
We propose a novel technique that generalizes the common notion of recurrence
relations based on ranking functions. Existing methods usually unfold one loop
iteration, and examine the resulting relations between variables. These relations
assist in establishing a recurrence that bounds the number of loop iterations. We
propose a different approach, where we derive recurrences by comparing whole
traces with whole traces of a lower rank, avoiding the need to analyze the com-
plexity of intermediate states. We offer a set of global properties, defined with re-
spect to whole traces, that facilitate such a comparison, and show that these prop-
erties can be checked efficiently using a handful of local conditions. To this end,
we adapt state squeezers, an induction mechanism previously used for verifying
safety properties. We demonstrate that this technique encompasses the reasoning
power of bounded unfolding, and more. We present some seemingly innocuous,
yet intricate, examples where previous tools based on cost relations and control
flow analysis fail to solve, and that our squeezer-powered approach succeeds.

Run-time Complexity Bounds Using Squeezers

ETAPS is a confederation of several conferences, each with its own Programme Committee and Steering Committee. ETAPS is the most important and visible annual European event related to software sciences. Altogether, more than 500 researchers participate in this event every year. The confederated conferences cover various aspects of software systems, ranging from theoretical foundations to programming language developments, compiler advancements, analysis tools, formal approaches to software engineering, and security.

A gather.town room will be open during the whole conference, which can be found here:

https://gather.town/app/nSgVv0DDYoCkmdkP/ETAPS2021

Password: Luxembourg2021

This can be used to meet in the coffee breaks.

 PDF's of the papers are available on https://etaps.org/2021/programme