Publication: On Formal Certification of AD Transformations
Introduction
Applications
Tools
Research Groups
Workshops
Publications
   List Publications
   Advanced Search
   Info
   Add Publications
My Account
About

On Formal Certification of AD Transformations

- incollection -
 

Author(s)
Emmanuel M. Tadjouddine

Published in
Advances in Automatic Differentiation

Editor(s)
Christian H. Bischof, H. Martin Bücker, Paul D. Hovland, Uwe Naumann, J. Utke

Year
2008

Publisher
Springer

Abstract
Automatic differentiation (ad) is concerned with the semantics augmentation of an input program representing a function to form a transformed program that computes the function's derivatives. To ensure the correctness of the ad transformed code, particularly for safety critical applications, we propose using the proof-carrying code paradigm: an ad tool must provide a machine checkable certificate for an ad generated code, which can be checked in polynomial time in the size of the certificate by an ad user using a simple and easy to validate program. Using a WHILE-language, we show how such proofs can be constructed. In particular, we show that certain code transformations and static analyses used in ad can be certified using the well-established Hoare logic for program verification.

Cross-References
Bischof2008AiA

AD Theory and Techniques
Certification

BibTeX
@INCOLLECTION{
         Tadjouddine2008OFC,
       title = "On Formal Certification of {AD} Transformations",
       doi = "10.1007/978-3-540-68942-3_3",
       author = "Emmanuel M. Tadjouddine",
       abstract = "Automatic differentiation (AD) is concerned with the semantics augmentation of an
         input program representing a function to form a transformed program that computes the
         function's derivatives. To ensure the correctness of the AD transformed code, particularly for
         safety critical applications, we propose using the proof-carrying code paradigm: an AD tool must
         provide a machine checkable certificate for an AD generated code, which can be checked in polynomial
         time in the size of the certificate by an AD user using a simple and easy to validate program. Using
         a WHILE-language, we show how such proofs can be constructed. In particular, we show that certain
         code transformations and static analyses used in AD can be certified using the well-established
         Hoare logic for program verification.",
       crossref = "Bischof2008AiA",
       pages = "23--33",
       booktitle = "Advances in Automatic Differentiation",
       publisher = "Springer",
       editor = "Christian H. Bischof and H. Martin B{\"u}cker and Paul D. Hovland and Uwe
         Naumann and J. Utke",
       isbn = "978-3-540-68935-5",
       issn = "1439-7358",
       year = "2008",
       ad_theotech = "Certification"
}


back
  

Contact:
autodiff.org
Username:
Password:
(lost password)