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"
}