Seminars

Speaker: Pierre Lermusiaux (plermusi.github.io/)

Title: Detection of Uncaught Exceptions in Functional Programs by Abstract
Interpretation

Abstract:

Exception handling is a key feature in modern programming languages. Exceptions
can be used to deal with errors, or as a means to control the flow of execution
of a program. Since they might unexpectedly terminate a program, unhandled
exceptions are a serious safety concern. We propose a static analysis to detect
uncaught exceptions in functional programs, that is defined as an abstract
interpreter. It computes a description of the values potentially returned by a
program using a novel abstract domain, that can express inductively defined
sets of values. Simultaneously, the analysis infers the possibly raised
exceptions, by computing in the abstract exception monad. This abstract
interpreter has been implemented as an effective static analyser for a large
subset of OCaml programs, that supports mutable data types, the OCaml module
system, and dynamically extensible data types such as the exception type. The
analyser has been evaluated on several hundreds of OCaml programs.