日本語(解説記事等) ↓

Research Bibliography

  1. Reynald Affeldt and Cyril Cohen. Formal Foundations of 3D Geometry to Model Robot Manipulators. In 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), January 16-17, 2017, Paris, France, pages 30-42. pdf preprint.
    ACM, (2017). http://dx.doi.org/10.1145/3018610.3018629. ACM Digital Library proceedings version
  2. Akira Tanaka, Reynald Affeldt, and Jacques Garrigue. Formal Verification of the rank Algorithm for Succinct Data Structures. In 18th International Conference on Formal Engineering Methods (ICFEM 2016), November 14-18, 2016, Tokyo, Japan, volume 10009 of Lecture Notes in Computer Science, pages 243-260. Springer, 2016. pdf.
    ©Springer. Springer Link. An early version of this paper was presented at the 18th JSSST Workshop on Programming and Programming Languages (PPL 2016), March 7-9, 2016, where it received the PPL2016 Best Paper Award. Source code.
  3. Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. In The 2016 International Symposium on Information Theory and Its Applications (ISITA 2016), October 30-November 2, 2016, Monterey, California, USA, pages 537-541. IEICE, 2016. pdf preprint.
    Organized session. ©IEICE. Source code.
  4. Reynald Affeldt and Cyril Cohen. Formal Foundations for Rigid Body Transformation. In 33rd Workshop of the Japan Society for Software Science and Technology (JSSST 2016), September 6-9, 2016, Sendai, Japan.
    Not reviewed. 11 pages.
  5. Reynald Affeldt and Jacques Garrigue. Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory. In 6th Conference on Interactive Theorem Proving (ITP 2015), August 24-27, 2015, Nanjing, China, volume 9236 of Lecture Notes in Computer Science, pages 17-33. Springer, August 2015. pdf.
    ©Springer. Springer Link.
  6. Reynald Affeldt, Kazuhiko Sakaguchi. An Intrinsic Encoding of a Subset of C and its Application to TLS Network Packet Processing. Journal of Formalized Reasoning, 7(1):63-104, 2014. pdf.
    Online Access (doi). Extended version of this paper.
  7. Reynald Affeldt, Manabu Hagiwara, and Jonas Sénizergues. Formalization of Shannon's Theorems. Journal of Automated Reasoning, 53(1):63-103, 2014. Springer. pdf.
    ©Springer. Springer Link. Extended version of this paper.
  8. Reynald Affeldt. On Construction of a Library of Formally Verified Low-level Arithmetic Functions. Innovations in Systems and Software Engineering, 9(2):59-77, 2013. NASA/Springer. pdf.
    ©Springer. Springer Link. Extended version of this paper. Latest Coq Documentation.
  9. Reynald Affeldt and Nicolas Marti. Towards Formal Verification of TLS Network Packet Processing Written in C. In 7th ACM SIGPLAN Workshop on Programming Languages meets Program Verification (PLPV 2013), January 22, 2013, Rome, Italy, pages 35-46. ACM, January 2013. pdf.
    ACM, (2013). This is the authors version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 2013 ACM SIGPLAN Workshop on Programming Languages meets Program Verification. http://doi.acm.org/10.1145/2428116.2428124. ACM Digital Library. Latest Coq Documentation.
  10. Reynald Affeldt and Manabu Hagiwara. Formalization of Shannon's Theorems in SSReflect-Coq. In 3rd Conference on Interactive Theorem Proving (ITP 2012), August 13-15, 2012, Princeton, New Jersey, USA, volume 7406 of Lecture Notes in Computer Science, pages 233-249. Springer, August 2012. pdf.
    ©Springer. Springer Link. Latest Coq documentation. slides. Extended version of the first part used as a support for a lecture at the meeting From Modern Coding Theory To Postmodern Coding Theory, March 4-7, 2013, Fukuoka, Japan (volume 44 of Math-for-Industry Lecture, pages 86-94, Kyushu University, 01/30/2013). An overview of the formalization of the channel coding theorem appeared in Suugaku seminar 618:74-79 (Nippon Hyoron Sha, 2013).
  11. Reynald Affeldt. On Construction of a Library of Formally Verified Low-level Arithmetic Functions. In 27th ACM SIGAPP Symposium On Applied Computing (SAC 2012), March 26-30, 2012, Riva del Garda (Trento), Italy, pages 1326-1331 (vol. 2). Software Verification and Testing Track. ACM, 2012. pdf.
    ACM, (2012). This is the authors version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the ACM Symposium on Applied Computing 2012. http://doi.acm.org/10.1145/2245276.2231986. ACM Digital Library. Latest Coq Documentation. Superseded by this article.
  12. Reynald Affeldt, David Nowak, and Yutaka Oiwa. Formal Network Packet Processing with Minimal Fuss: Invertible Syntax Descriptions at Work. In 6th ACM SIGPLAN Workshop Programming Languages meets Program Verification (PLPV 2012), January 24, 2012, Philadelphia, USA, pages 27-36. ACM Press, 2012. pdf.
    ACM, (2012). This is the authors version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in PLPV'12 Proceedings, (Jan. 2012) http://doi.acm.org/10.1145/2103776.2103780. ACM Digital Library.
  13. Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying Assembly with Formal Security Proofs: the Case of BBS. Science of Computer Programming, 77(10-11):1058-1074, 2012. Elsevier. pdf.
    ScienceDirect. Extended version of this paper. Coq scripts (as of January 2011). Latest Coq Documentation
  14. Reynald Affeldt and Kiyoshi Yamada. A Coq Starter Kit to Verify TLS Packet Processing in C. Draft. pdf.
    Superseded by this paper. This is a revised version of a non-reviewed paper that was presented at the 28th Workshop of the Japan Society for Software Science and Technology (JSSST 2011), Naha, September 27-28, 2011.
  15. Reynald Affeldt. Toward Formal Construction of Assembly Arithmetic Functions from Pseudo-code. In 12th JSSST Workshop on Programming and Programming Languages (PPL 2010), March 3-5, 2010. pdf.
    15 pages. Informal proceedings. Superseded by this paper and this article. Latest Coq Documentation
  16. Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS. Electronic Communications of the EASST, 23, January 2010. European Association of Software Science and Technology. pdf.
    Superseded by this paper. Proceedings of the 9th International Workshop on Automated Verification of Critical Systems (AVoCS 2009), Swansea University Computer Science, September 23-25, 2009. Electronic Communications of the EASST online. An extended abstract in Japanese (2 pages) was presented in September 2009 at the annual meeting of the Japan Society for Industrial and Applied Mathematics. Preliminary versions: Technical Report of Computer Science, Swansea University CSR-2-2009 (pdf); Cryptology ePrint Archive: Report 2009/322, July 2009. Coq scripts (as of January 2011).
  17. Reynald Affeldt and Hubert Comon-Lundh. Verification of Security Protocols with a Bounded Number of Sessions based on Resolution for Rigid Variables. In Formal to Practical Security, volume 5458 of Lecture Notes in Computer Science, State-of-the-Art Survey, pages 1-20. Springer, May 2009. preprint.
    ©Springer. Springer Link.
  18. Reynald Affeldt and Hubert Comon-Lundh. A Note on First-order Logic and Security Protocols. In Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS 2008), Pittsburgh, PA, USA, June 21-22, 2008, pages 11-20. pdf.
    Superseded by this paper. Informal proceedings. An extended abstract (2 pages, slides) was presented in September 2008 at the annual meeting of the Japan Society for Industrial and Applied Mathematics.
  19. Reynald Affeldt, Miki Tanaka, and Nicolas Marti. Formal Proof of Provable Security by Game-playing in a Proof Assistant. In 1st International Conference on Provable Security (Provsec 2007), November 1-2, 2007, Wollongong, NSW, Australia, volume 4784 of Lecture Notes in Computer Science, pages 151-168. Springer, October 2007. preprint.
    ©Springer. Springer Link. An extended abstract in Japanese (2 pages) was presented in September 2007 at the annual meeting of the Japan Society for Industrial and Applied Mathematics.
  20. Nicolas Marti and Reynald Affeldt. A Certified Verifier for a Fragment of Separation Logic. Computer Software, 25(3):135-147, 2008. Iwanami Shoten. pdf.
    J-Stage. Coq Documentation of an up-to-date version. Reprinted to Information and Media Technologies 4(2):304-316, 2009. Japan Society for Software Science and Technology. J-Stage. An early version of this article was presented at the 9th JSSST Workshop on Programming and Programming Languages (PPL 2007), March 8-10, 2007, where it received the PPL2007 Best Paper Award. Coq scripts (as of 2007). Interactive Demo.
  21. Reynald Affeldt and Nicolas Marti. An Approach to Formal Verification of Arithmetic Functions in Assembly. In 11th Annual Asian Computing Science Conference (ASIAN 2006), Focusing on Secure Software and Related Issues, December 6-8, 2006, Tokyo, Japan, volume 4435 of Lecture Notes in Computer Science, pages 346-360. Springer, January 2008. preprint.
    ©Springer. Springer Link. Up-to-date Coq Documentation.
  22. Reynald Affeldt and David Nowak. Application of Formal Verification to Software Security. Information Security Summer School (ISSS 2006), Taipei, Taiwan. August 2006. Presentation material.
    Organized by the Taiwan Information Security Center (TWISC). 90 minutes presentation.
  23. Reynald Affeldt and Nicolas Marti. Formal Verification of Arithmetic Functions in SmartMIPS Assembly. In 23rd Workshop of the Japan Society for Software Science and Technology, University of Tokyo, Tokyo, Japan, September 13-15, 2006. 6 pages. Japan Society for Software Science and Technology. pdf.
    Not reviewed. Superseded by this paper. Electronic proceedings.
  24. Nicolas Marti, Reynald Affeldt and Akinori Yonezawa. Model-checking of a Multi-threaded Operating System. In 23rd Workshop of the Japan Society for Software Science and Technology, University of Tokyo, Tokyo, Japan, September 13-15, 2006. 6 pages. Japan Society for Software Science and Technology. pdf.
    Not reviewed. Electronic proceedings. Spin model.
  25. Nicolas Marti, Reynald Affeldt and Akinori Yonezawa. Formal Verification of the Heap Manager of an Operating System using Separation Logic. In 8th International Conference on Formal Engineering Methods (ICFEM 2006), Macao SAR, China, October 29-November 3, 2006, volume 4260 of Lecture Notes in Computer Science, pages 400-419. Springer, October 2006. preprint.
    ©Springer. Springer Link. Coq scripts. Coq Documentation of an up-to-date version.
  26. Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa. Verification of the Heap Manager of an Operating System using Separation Logic. In 3rd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE 2006), Charleston SC, USA, January 14, 2006, pages 61-72. pdf.
    Superseded by this paper. Sponsored by ACM SIGPLAN. Informal proceedings. Slides.
  27. Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa. Towards Formal Verification of Memory Properties using Separation Logic. In 22nd Workshop of the Japan Society for Software Science and Technology, Tohoku University, Sendai, Japan, September 13-15, 2005. 6 pages. Japan Society for Software Science and Technology. pdf.
    Electronic proceedings. Nicolas received the Takahashi Award for his presentation. Slides.
  28. Reynald Affeldt, Naoki Kobayashi, and Akinori Yonezawa. Verification of concurrent programs using the Coq proof assistant: a case study. IPSJ Transactions on Programming, 46(1):110-120. Information Processing Society of Japan, 2005. pdf.
    Reprinted to IPSJ Digital Courier, 1:117-127, January 2005. J-Stage. A preliminary version of this article was presented at the Summer United Workshops on Parallel, Distributed and Cooperative Processing (SWoPP 2004), Aomori, Japan, July 30-August 1, 2004.
  29. Reynald Affeldt and Naoki Kobayashi. Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes. November 2004. 21 pages. Draft. pdf.
    Extended version of this paper.
  30. Reynald Affeldt. Verification of Concurrent Programs using Proof Assistants. Ph.D. thesis. September 2004. The University of Tokyo, Graduate School of Information Science and Technology, Department of Computer Science, 7-3-1 Hongo, Bunkyo-ku, 113-0033 Japan.
  31. Reynald Affeldt and Naoki Kobayashi. Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes. Electronic Notes in Theoretical Computer Science, 128(2):151-168, April 2005. Elsevier. pdf.
    Proceedings of the 11th International Workshop on Expressiveness in Concurrency (EXPRESS 2004), London, UK, August 30, 2004. Elsevier Science direct. Extended version here.
  32. Reynald Affeldt and Naoki Kobayashi. A Coq Library for Verification of Concurrent Programs. Electronic Notes in Theoretical Computer Science, 199:17-32, February 2008. Elsevier. pdf.
    Proceedings of the 4th International Workshop on Logical Frameworks and Meta-Languages (LFM 2004), Cork, Ireland, July 5, 2004. Elsevier Science direct. Coq documentation.
  33. Reynald Affeldt and Naoki Kobayashi. Formalization and Verification of a Mail Server in Coq. In International Symposium on Software Security, Tokyo, Japan, November 8-10, 2002, volume 2609 of Lecture Notes in Computer Science, Hot Topics, pages 217-233. Springer, February 2003. preprint.
  34. Reynald Affeldt, Hidehiko Masuhara, Eijiro Sumii, Akinori Yonezawa. Supporting Objects in Run-Time Bytecode Specialization. In ACM SIGPLAN Asian Symposium on Partial Evaluation and Semantics-based Program Manipulation (ASIA-PEPM 2002), Aizu, Japan, pages 50-60. ACM Press, September 2002. pdf.
  35. Reynald Affeldt. Supporting Object-Oriented Features in Run-time Bytecode Specialization. Master's thesis. September 2001. The University of Tokyo, Graduate School of Science, Department of Information Science, 7-3-1 Hongo, Bunkyo-ku, 113-0033 Japan.
  36. Reynald Affeldt, Hidehiko Masuhara, Eijiro Sumii, and Akinori Yonezawa. Supporting Objects in Run-time Bytecode Specialization. In 18th Workshop of the Japan Society for Software Science and Technology (JSSST 2001), Future University, Hakodate, September 18-20, 2001, 4 pages. Japan Society for Software Science and Technology. pdf.
    Electronic proceedings. Not reviewed. Superseded by this paper.

日本語(解説記事等)

  1. アフェルト レナルド. チュートリアル:定理証明支援系Coq入門. 日本ソフトウェア科学会 第31回大会. 2014.09.07. 日本ソフトウェア科学会. イベントサイト. スライド等.
  2. アフェルト レナルド. 定理証明支援系に基づく形式検証---近年の実例の紹介とCoq入門--- 情報処理, 55:482-491, 2014.05. 情報処理学会. pdf.
  3. アフェルト レナルド. 形式的な符号理論に向けて. 数学セミナー, 618:74-79, 2013.04. 日本評論社.
  4. アフェルト レナルド. SSReflectによる符号理論の形式化に関するー考察. 日本応用数理学会研究部会連合発表会. 2010.03. 日本応用数理学会. slides.
  5. アフェルト レナルド, ノヴァック ダウ゛ィッド, 山田 聖. 形式的な暗号学的安全性証明によるアセンブリプログラムの安全性検証:BBSの事例. 日本応用数理学会2009年度年会講演予稿集, p. 53-54. 2009.09. 日本応用数理学会. pdf. 英語版.
  6. アフェルト レナルド. 実用的な暗号の形式的証明に向けて:アセンブリでの多倍長整数アルゴリズムの形式的検証. 平成20年度研究成果発表会 (RCIS Workshop 2009). poster.
  7. アフェルト レナルド, 田中 三貴, マーティ ニコラ. 証明可能安全性の形式的証明:定理証明ツールによるゲームの手法. 日本応用数理学会2007年度年会講演予稿集, p. 44-45. 2007.09. 日本応用数理学会. pdf. 英語版.