Foundational Certification of Code Transformations Using Automatic Differentiation

• Autorzy: Tadjouddine E. M. , Lv W.

Identyfikatory

DOI

10.7494/csci.2014.15.2.215

• Języki publikacji: EN

Abstrakty

EN

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 aim at certifying the algebraic manipulations at the heart of the AD process. We have considered a WHILE-language, and have shown how such proofs can be constructed by using appropriate relational Hoare logic. In particular, we have shown how such inference rules can be constructed for both the forward- and reverse-mode AD by using an abductive logical reasoning.

Słowa kluczowe

EN

relational Hoare logic; abductive reasoning; certification; automatic differentiation

• Wydawca: Wydawnictwa AGH
• Czasopismo: Computer Science
• Rocznik: 2014
• Tom: Vol. 15 (2)
• Strony: 215--236
• Opis fizyczny: Bibliogr. 28 poz., rys.

Twórcy

autor

Tadjouddine E. M.

• Xi’an Jiaotong-Liverpool University, Department of Computer Science & Software Engineering, 111 Ren Ai Road, Suzhou Industrial Park, Suzhou, P.R. China 215123

autor

Lv W.

• Xi’an Jiaotong-Liverpool University, Department of Computer Science & Software Engineering, 111 Ren Ai Road, Suzhou Industrial Park, Suzhou, P.R. China 215123

Bibliografia

• [1] Aho A., Sethi R., Ullman J., Lam M.: Compilers: principles, techniques, and tools. Addison-Wesley Publishing Company, Boston, USA, Second ed., 2006.
• [2] Araya-Polo M., Hasco ̈et L.: Certification of Directional Derivatives Computed by Automatic Differentiation. WSEAS Transactions on Circuits and Systems, 2005.
• [3] Bai W., Tadjouddine E.M., Payne T., Guan S.: A Proof-Carrying Code Approach to Certificate Auction Mechanisms. In: The 10th International Symposium on Formal Aspects of Component Software. 2013.
• [4] Benton N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL ’04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 14–25. ACM Press, New York, NY, USA, 2004. ISBN 1-58113-729-X.
• [5] Berdine J., Calcagno C., O’Hearn P. W.: Symbolic Execution with Separation Logic. In: In APLAS, pp. 52–68. Springer, 2005.
• [6] Bertot Y., Cast ́eran P.: Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Texts in theoret. comp. science. Springer-Verlag, 2004. ISBN 3-540-20854-2 (hardcover).
• [7] Bischof C.H., Carle A., Khademi P., Mauer A.: ADIFOR 2.0: Automatic Differentiation of Fortran 77 Programs. IEEE Computational Science & Engineering, 3(3):18–32, 1996.
• [8] Calcagno C., Distefano D., O’Hearn P., Yang H.: Compositional shape analysis by means of bi-abduction. In: POPL ’09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on POPL, pp. 289–300. ACM, New York, NY, USA, 2009. ISBN 978-1-60558-379-2.
• [9] Christianson B.: Reverse Accumulation and Attractive Fixed Points. Optimization Methods and Software, 3 311–326, 1994.
• [10] Cytron R., Ferrante J., Rosen B. K., Wegman M. N., Zadeck F. K.: Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM Transactions on Programming Languages and Systems, 13(4): 451–490, 1991.
• [11] Fischer H.: Special Problems in Automatic Differentiation. In: Automatic Differentiation of Algorithms: Theory, Implementation, and Application, A. Griewank, G. F. Corliss, eds., pp. 43–50. SIAM, Philadelphia, PA, 1991. ISBN 0–89871–284–X.
• [12] Forth S. A., Tadjouddine M., Pryce J. D., Reid J. K.: Jacobian Code Generated by Source Transformation and Vertex Elimination can be as Efficient as Hand-Coding. ACM Transactions on Mathematical Software, 30(3): 266–299, 2004.
• [13] Frade M. J., Saabas A., Uustalu T.: Foundational certification of data-flow analyses. In: TASE, pp. 107–116. 2007.
• [14] Gilbert J. C.: Automatic Differentiation and Iterative Processes. Optimization Methods and Software, 1: 13–21, 1992.
• [15] Griewank A., Bischof C., Corliss G., Carle A., Williamson K.: Derivative Convergence for Iterative Equation Solvers. Optimization Methods and Software, 2: 321–355, 1993.
• [16] Griewank A., Walther A.: Evaluating Derivatives: Principles and Techniques of Algorithmic Differentiation. Frontiers in Appl. Math. SIAM, Philadelphia, PA, second ed., 2008.
• [17] Hasco ̈et L., Pascual V.: TAPENADE 2.1 user’s guide. INRIA Sophia Antipolis, 2004, Route des Lucioles, 09902 Sophia Antipolis, France, 2004. See http://www.inria.fr/rrrt/rt-0300.html.
• [18] Huth M. R. A., Ryan M. D.: Logic in Computer Science: Modelling and Reasoning about Systems . Cambridge University Press, Cambridge, England, 2000. ISBN Hardback: ISBN 0521652006, Paperback: ISBN 0521656028.
• [19] Inoue K.: Induction, Abduction, and Consequence-Finding. In: ILP ’01: Proceedings of the 11th Int’ Conf. on Inductive Logic Programming, pp. 65–79. Springer, London, UK, 2001. ISBN 3-540-42538-1.
• [20] Leroy X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Proceedings of POPL’06, pp. 42–54. 2006.
• [21] Mayero M.: Formalisation et automatisation de preuves en analyses r ́elle etnum ́erique. Ph.D. thesis, Universit ́e Paris VI, 2001. ftp://ftp.inria.fr/INRIA/LogiCal/Micaela.Mayero/papers/these-mayero.ps.gz.
• [22] Necula G. C.: Proof-carrying code. In: Proceedings of POPL’97, pp. 106–119. ACM Press, New York, NY, USA, 1997. ISBN 0-89791-853-3.
• [23] Pusch G.D., Bischof C., Carle A.: On Automatic Differentiation of Codes with COMPLEX Arithmetic with Respect to Real Variables. Technical Memorandum ANL/MCS-TM-188, Argonne National Laboratory, Mathematics and Computer Science Division, 9700 South Casss Avenue, Argonne, IL 60439, 1995.
• [24] Reid P., Gamboa R.: Automatic Differentiation in ACL2. In: ITP, M.C.J.D. van Eekelen, H. Geuvers, J. Schmaltz, F. Wiedijk, eds., Lecture Notes in Computer Science, vol. 6898, pp. 312–324. Springer, 2011.
• [25] Ross B. J.: Running Programs Backwards: The Logical Inversion of Imperative Computation. Formal Aspects of Computing, 9: 331–348, 1998.
• [26] Tadjouddine E. M.: On Formal Certification of AD Transformations. In: Advances in Automatic Differentiation, C. Bischof, M. B ̈ucker, P. Hovland, U. Naumann, J. Utke, eds., Lecture Notes in Computational Science and Engineering, vol. 64, pp. 23–34. Springer, Berlin, 2008.
• [27] Tadjouddine E. M., Cao Y.: An Option Price Model Calibration Using Algorithmic Differentiation. In: ISCIS 2011, E. Gelenbe, ed., Computer and Information Sciences, pp. 577–581. Springer, 2011.
• [28] Tadjouddine M., Forth S. A., Keane A. J.: Adjoint differentiation of a Structural Dynamics Solver. In: Automatic Differentiation: Applications, Theory, and Implementations, M. B ̈ucker, G. Corliss, P. Hovland, U. Naumann, B. Norris, eds., LNCSE, pp. 309–319. Springer, Berlin, Germany, 2005.