VSL Publications

Verifying Properties of Differentiable Programs

Cite
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 11002, pp. 205-222. Springer, Cham, 2018.
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.
Downloads
  1. Preprint
Related Links
  1. Published version (Springer)
  2. Experimental Archive page
BibTeX 
@inproceedings{huckelheim-etal:2018:sas,
  author = {Jan H\"uckelheim and Ziqing Luo and
            Sri Hari Krishna Narayanan and
            Stephen Siegel and Paul D. Hovland},
  title = {Verifying Properties of Differentiable Programs},
  booktitle = {Static Analysis: 25th International Symposium, SAS 2018, Proceedings},
  editor = {Andreas Podelski},
  series = {Lecture Notes in Computer Science},
  volume = {11002},
  pages = {205--222},
  publisher = {Springer},
  doi = {10.1007/978-3-319-99725-4_14},
  year = {2018}
}
VSL | Publications