ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Fri 8 Sep 2023 16:30 - 17:00 at Grand Crescent - ML Workshop: Session 4 Chair(s): Oleg Kiselyov

We report on a work in progress that aims at defining an effective static analyser for OCaml programs, by leveraging abstract interpretation techniques. The goal of the Salto static analyser is to detect precisely which exceptions an OCaml program might raise, and to report problematic cases, where a program execution might rely on elements of the OCaml semantics that are deemed under-specified or undefined. The Salto analyser exploits a novel abstract domain to represent inductively defined sets of trees, that draws inspiration from the theory of recursive types, from tree automata, and from the abstract domain of Type Graphs. The analyser itself is defined using a dynamic fixpoint solver, i.e., a generic library that implements an iteration strategy that finds a post-fixpoint. The solver automatically inserts widening points to ensure the convergence of the iteration process, and aims at limiting the unnecessary computations that may be asked by the iteration strategy.

Fri 8 Sep

Displayed time zone: Pacific Time (US & Canada) change