The Design and Implementation of an Abstract Interpreter for OCaml Programs: A Preliminary Report on the Salto Analyser
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.
Slides (2023-09-07_ML_workshop_Seattle.pdf) | 1.86MiB |
Fri 8 SepDisplayed time zone: Pacific Time (US & Canada) change
16:00 - 17:30 | ML Workshop: Session 4Higher-order, Typed, Inferred, Strict: ML Family Workshop at Grand Crescent Chair(s): Oleg Kiselyov Tohoku University | ||
16:00 30mTalk | Flambda 2 Types: An abstract domain for static analysis of functional programs (moved from OCaml workshop) Higher-order, Typed, Inferred, Strict: ML Family Workshop | ||
16:30 30mTalk | The Design and Implementation of an Abstract Interpreter for OCaml Programs: A Preliminary Report on the Salto Analyser Higher-order, Typed, Inferred, Strict: ML Family Workshop Benoît Montagu Inria Pre-print Media Attached File Attached |