Title:  Automated Program Analysis for Scientific Software
Author: Jacob Laurel

Abstract:

Program Analysis has successfully solved a variety of problems across
multiple areas including software engineering, compilers, security,
and most recently machine learning. Despite these successes, the
application of program analysis to scientific computing remains
understudied. Further, the few existing techniques that analyze
scientific software focus mainly on lower-level concerns such as
floating-point stability. While those issues remain important,
scientific programs must also obey higher-level mathematical
properties for which there do not exist any automated program
analyses. Despite this need, a gap exists between the scientific
computing community and the programming languages and formal methods
community.

As a step towards bridging this gap, this talk describes why automated
program analysis, in particular abstract interpretation, offers a
natural way to reason about the programs encountered in scientific
computing. I will also discuss how one can cleanly formalize new
domain-specific properties from scientific computing in the language
of abstract interpretation and focus on applications found in
Automatic Differentiation and Bayesian inference. Beyond abstract
interpretation, this talk will highlight why the entire program
analysis, testing, and formal methods toolkit offers new opportunities
to ensure safe and correct scientific software.