POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Fri 19 Jan 2024 11:10 - 11:30 at Kelvin Lecture - Program Analysis Chair(s): Jules Villard

It is widely known that the precision of a program analyzer is closely related to intensional program properties, namely, properties concerning how the program is written. This explains, for instance, the interest in code obfuscation techniques, namely, tools explicitly designed to degrade the results of program analysis by operating syntactic program transformations. Less is known about a possible relation between what the program extensionally computes, namely, its input-output relation, and the precision of a program analyzer. In this paper we explore this potential connection in an effort to isolate program fragments that can be precisely analyzed by abstract interpretation, namely, programs for which there exists a complete abstract interpretation. In the field of static inference of numeric invariants, this happens for programs, or parts of programs, that manifest a monotone (either non-decreasing or non-increasing) behavior. We first formalize the notion of program monotonicity with respect to a given input and a set of numerical variables of interest. A sound proof system is then introduced with judgments specifying whether a program is monotone relatively to a set of variables and a set of inputs. The interest in monotonicity is justified because we prove that the family of monotone programs admits a complete abstract interpretation over a specific class of non-trivial numerical abstractions and inputs. This class includes all non-relational abstract domains that refine interval analysis (i.e., at least as precise as the intervals abstraction) and that satisfy a topological convexity hypothesis.

Fri 19 Jan

Displayed time zone: London change

10:30 - 11:50
Program AnalysisPOPL at Kelvin Lecture
Chair(s): Jules Villard Meta
10:30
20m
Talk
Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis
POPL
John Cyphert University of Wisconsin-Madison, USA, Zachary Kincaid Princeton University
10:50
20m
Talk
On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability
POPL
Shankaranarayanan Krishna IIT Bombay, India, Aniket Lal IIT Bombay, Andreas Pavlogiannis Aarhus University, Omkar Tuppe IIT Bombay
11:10
20m
Talk
Monotonicity and the Precision of Program Analysis
POPL
Marco Campion INRIA & École Normale Supérieure | Université PSL, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Arizona, Caterina Urban Inria & École Normale Supérieure | Université PSL
11:30
20m
Talk
Flan: An Expressive and Efficient Datalog Compiler for Program AnalysisDistinguished PaperRemote
POPL
Supun Abeysinghe Purdue University, Anxhelo Xhebraj Purdue University, Tiark Rompf Purdue University