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

This paper presents a program analysis method that generates program invariants involving polynomial arithmetic. Our approach builds on prior techniques that use solvable polynomial maps for summarizing loops. Such techniques are able to generate all polynomial invariants for a restricted class of programs. However, there currently lacks approaches to apply prior complete methods to the case of general programs with nested loops, conditional branching, unstructured control flow, etc. This paper bridges that gap. Our approach works uniformly for every loop, regardless of whether the loop is within the class of programs prior methods can solve or not. Instead of restricting the kinds of programs we can handle, our method abstracts every loop into a model that can be solved with prior techniques. Our uniform approach to loops gives us a method that brings to bear prior work on solvable polynomial maps to general programs. While no method can generate all polynomial invariants for arbitrary programs, our method establishes its merit through a monotonicty result. We have implemented our techniques, and tested them on a suite of benchmarks from the literature. Our experiments indicate our techniques show promise on challenging verification tasks requiring powerful non-linear reasoning.

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