ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
Tue 14 Oct 2025 16:00 - 16:25 at Peony West - Analyze This Chair(s): Jens Palsberg

Static analysis aims at computing semantic properties of programs. Abstract interpretation provides a framework to design static analyses and allows one to divide the construction of a static analysis into the definition of abstract domains that describe families of logical predicates with operations to reason on them, and the semantic-guided formalisation of abstract interpreters. The latter relies on the abstract domains, that describe semantic properties, and on the concrete semantics. A large part of the research on static analysis focuses on the design of novel abstract domains, with ever more expressive and/or efficient computer representation for semantic properties. In this short paper, we consider more specifically the core of the abstract interpreters (also called the abstract iterators) and discuss several techniques to build them, that are inspired by functional programming. First, we briefly discuss common iteration techniques based on control flow graphs, which have often been used for program analyses aimed at computing state properties. Second, we consider iteration techniques that borrow principles from denotational semantics and are typically defined by induction over the syntax of programs. Last, we extend the latter family of techniques to relational abstractions that capture relations between program inputs and outputs.

Tue 14 Oct

Displayed time zone: Perth change

16:00 - 17:45
Analyze ThisOlivierFest at Peony West
Chair(s): Jens Palsberg University of California, Los Angeles (UCLA)
16:00
25m
Talk
On the Structure of Abstract Interpretersfestschrift
OlivierFest
Wonyeol Lee POSTECH, Matthieu Lemerre Université Paris-Saclay - CEA List, Xavier Rival Inria - CNRS - Ecole Normale Superieure de Paris - PSL University, Hongseok Yang KAIST
DOI
16:25
25m
Talk
Understanding Linux Kernel Code through Formal Verification: A Case Study of the Task-Scheduler Function select_idle_corefestschrift
OlivierFest
DOI
16:50
25m
Talk
Simple Closure Analysis Revisitedfestschrift
OlivierFest
Fritz Henglein University of Copenhagen
DOI
17:15
15m
Talk
Mixing transformation and symbolic execution with continuation for WebAssembly
OlivierFest
Guannan Wei Tufts University
17:30
15m
Talk
Data-Centric Functional Programming with First-Class Finite Maps and Tabulated Abstractions
OlivierFest
Tiark Rompf Purdue University