Lifted Termination Analysis by Abstract Interpretation and its ApplicationsVirtual
Mon 18 Oct 2021 16:10 - 16:25 at Zurich C - SLE/GPCE Session 8 Chair(s): Ran Wei
This paper is focused on proving termination for program families with numerical features by using abstract interpretation. Furthermore, we present an interesting application of the above lifted termination analysis for resolving ``sketches'', i.e. partial programs with missing numerical parameters (holes), such that the resulting complete programs always terminate. To successfully address the above problems, we employ an abstract interpretation-based framework for inferring sufficient preconditions for termination of single programs that synthesizes piecewise-defined ranking functions.
We introduce a novel lifted decision tree domain for termination, in which decision nodes contain linear constraints defined over numerical features and leaf nodes contain piecewise ranking functions defined over program variables. Moreover, we encode a program sketch as a program family, thereby allowing the use of the lifted termination analysis as a program sketcher. In particular, we aim to find the variants (family members) that terminate under all possible inputs, which represent the correct sketch realizations.
We have implemented an experimental lifted termination analyzer, called SPLFuncTion, for proving termination of $\texttt{#if}$-based C program families and for termination-directed resolving of C program sketches. We have evaluated our approach by a set of loop benchmarks from SV-COMP, and experimental results show that our approach is effective and efficient.
Mon 18 OctDisplayed time zone: Central Time (US & Canada) change
07:40 - 09:00 | |||
07:40 15mTalk | Leveraging Relational Concept Analysis for Automated Feature Location in Software Product LinesVirtual GPCE Nicolas Hlad LIRMM, CNRS, Bérénice Lemoine LIRMM, CNRS, Marianne Huchard LIRMM, Abdelhak Seriai LIRMM, CNRS and University of Montpellier | ||
07:55 15mTalk | FIDDLR: Streamlining Reuse with Concern-Specific Modelling LanguagesVirtual SLE Maximilian Schiedermeier McGill University, Jörg Kienzle McGill University, Canada, Bettina Kemme McGill University, Canada | ||
08:10 15mTalk | Lifted Termination Analysis by Abstract Interpretation and its ApplicationsVirtual GPCE Aleksandar S. Dimovski Mother Teresa University, Skopje | ||
08:25 15mTalk | Delta-based Verification of Software Product FamiliesVirtual GPCE Marco Scaletta Technische Universität Darmstadt, Reiner Hähnle Technical University of Darmstadt, Dominic Steinhöfel CISPA Helmholtz Center for Information Security, Richard Bubel Technische Universität Darmstadt | ||
08:40 20mLive Q&A | Discussion, Questions and Answers SLE |
15:40 - 17:00 | |||
15:40 15mTalk | Leveraging Relational Concept Analysis for Automated Feature Location in Software Product LinesVirtual GPCE Nicolas Hlad LIRMM, CNRS, Bérénice Lemoine LIRMM, CNRS, Marianne Huchard LIRMM, Abdelhak Seriai LIRMM, CNRS and University of Montpellier | ||
15:55 15mTalk | FIDDLR: Streamlining Reuse with Concern-Specific Modelling LanguagesVirtual SLE Maximilian Schiedermeier McGill University, Jörg Kienzle McGill University, Canada, Bettina Kemme McGill University, Canada | ||
16:10 15mTalk | Lifted Termination Analysis by Abstract Interpretation and its ApplicationsVirtual GPCE Aleksandar S. Dimovski Mother Teresa University, Skopje | ||
16:25 15mTalk | Delta-based Verification of Software Product FamiliesVirtual GPCE Marco Scaletta Technische Universität Darmstadt, Reiner Hähnle Technical University of Darmstadt, Dominic Steinhöfel CISPA Helmholtz Center for Information Security, Richard Bubel Technische Universität Darmstadt | ||
16:40 20mLive Q&A | Discussion, Questions and Answers SLE |