Hückelheim J., Luo Z., Narayanan S.H.K., Siegel S.,
Hovland P.D. (2018) Verifying Properties of Differentiable
Programs. In Proceedings of the 25th International Static Analysis Symposium (SAS 2018). Lecture
Notes in Computer Science, vol 11002. Springer, Cham
There is growing demand for formal verification methods in the
scientific and high performance computing communities. For scientific
applications, it is not only necessary to verify the absence of
violations such as out of bounds access or race conditions, but also
to ensure that the results satisfy certain mathematical properties. In
this work, we explore the limits of automated bounded verification in
the verification of these programs by applying the symbolic execution
tool CIVL to some numerical algorithms that are frequently used in
scientific programs, namely a conjugate gradient solver, a finite
difference stencil, and a mesh quality metric. These algorithms
implement differentiable functions, allowing us to use the automatic
differentiation tools Tapenade and ADIC in the creation of their
specifications.
@InProceedings{10.1007/978-3-319-99725-4_14,
author="Hückelheim, Jan
and Luo, Ziqing
and Narayanan, Sri Hari Krishna
and Siegel, Stephen
and Hovland, Paul D.",
editor="Podelski, Andreas",
title="{V}erifying {P}roperties of {D}ifferentiable {P}rograms",
booktitle="Static Analysis",
year="2018",
publisher="Springer International Publishing",
address="Cham",
pages="205--222",
abstract="There is growing demand for formal verification methods in the scientific and high performance computing communities. For scientific applications, it is not only necessary to verify the absence of violations such as out of bounds access or race conditions, but also to ensure that the results satisfy certain mathematical properties. In this work, we explore the limits of automated bounded verification in the verification of these programs by applying the symbolic execution tool CIVL to some numerical algorithms that are frequently used in scientific programs, namely a conjugate gradient solver, a finite difference stencil, and a mesh quality metric. These algorithms implement differentiable functions, allowing us to use the automatic differentiation tools Tapenade and ADIC in the creation of their specifications.",
isbn="978-3-319-99725-4"
}
