The Design and Implementation of an Abstract Interpreter for OCaml Programs - A Preliminary Report on the Salto Analyser

Explore the design and implementation of an abstract interpreter for OCaml programs in this 34-minute conference talk from ACM SIGPLAN's ML'23 event. Delve into the ongoing development of the Salto static analyser, which aims to precisely detect potential exceptions in OCaml programs and identify problematic cases involving under-specified or undefined semantics. Learn about the novel abstract domain used to represent inductively defined sets of trees, drawing inspiration from recursive types, tree automata, and Type Graphs. Discover how the analyser employs a dynamic fixpoint solver to implement an iteration strategy for finding post-fixpoints, automatically inserting widening points to ensure convergence and optimize computations. Gain insights into the challenges and progress of creating an effective static analysis tool for OCaml, presented by Benoît Montagu in this preliminary report on the Salto analyser.

[ML'23] The Design and Implementation of an Abstract Interpreter for OCaml Programs: A Pre...