APLAS 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
co-located with SPLASH 2022
Mon 5 Dec 2022 11:00 - 11:30 at Seminar Room G007 - Semantics and Analysis Chair(s): Julian Mackay

Abstract Interpretation approximates the semantics of a program by mimicking its concrete fixpoint computation on an abstract domain A. The abstract (post-) fixpoint computation is classically divided into two phases: the ascending phase, using widenings as extrapolation operators to enforce termination, is followed by a descending phase, using narrowings as interpolation operators, so as to mitigate the effect of the precision losses introduced by widenings. In this paper we propose a simple variation of this classical approach where, to more effectively recover precision, we decouple the two phases: in particular, before starting the descending phase, we replace the domain A with a more precise abstract domain D. The correctness of the approach is justified by casting it as an instance of the A^2I framework. After demonstrating the new technique on a simple example, we summarize the results of a preliminary experimental evaluation, showing that it is able to obtain significant precision improvements for several choices of the domains A and D.

Mon 5 Dec

Displayed time zone: Auckland, Wellington change

10:30 - 12:00
Semantics and AnalysisAPLAS at Seminar Room G007
Chair(s): Julian Mackay Victoria University of Wellington
10:30
30m
Talk
An Algebraic Theory for Shared-State Concurrency
APLAS
Yotam Dvir Tel Aviv University, Ohad Kammar University of Edinburgh, Ori Lahav Tel Aviv University
File Attached
11:00
30m
Talk
Decoupling the Ascending and Descending Phases in Abstract Interpretation
APLAS
Vincenzo Arceri University of Parma, Italy, Isabella Mastroeni University of Verona, Italy, Enea Zaffanella University of Parma, Italy
11:30
30m
Talk
Inferring Region Types via an Abstract Notion of Environment Transformation
APLAS
Ulrich Schöpp fortiss GmbH, Chuangjie Xu fortiss GmbH