業績(成果発表)

in English

  1. 学術論文
  2. 国際会議(査読ありProceedings)
  3. 国際学会(査読あり概要・発表)
  4. 国内学会(査読ありProceedings)
  5. 国内学会(査読なしProceedings)
  6. 国内学会(発表のみ)
  7. 解説記事

学術論文

article_jp
[1] 田中 哲, Reynald Affeldt, and Jacques Garrigue. Safe low-level code generation in Coq using monomorphization and monadification. Journal of Information Processing, 2017. [ bib ]
To appear プロジェクト ページ

[2] Reynald Affeldt and 坂口 和彦. 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. [ bib ]
pdf preprint オープンアクセス doi プロジェクト ページ

[3] Reynald Affeldt, 萩原 学, and Jonas Sénizergues. Formalization of Shannon's theorems. Journal of Automated Reasoning, 53(1):63--103, 2014. [ bib ]
pdf preprint doi プロジェクト ページ

[4] 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. [ bib ]
NASA/Springer pdf preprint doi プロジェクト ページ

[5] Reynald Affeldt, David Nowak, and 山田 聖. Certifying assembly with formal security proofs: the case of BBS. Science of Computer Programming, 77(10--11):1058--1074, 2012. [ bib ]
pdf preprint doi プロジェクト ページ

[6] 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. [ bib ]
pdf preprint doi プロジェクト ページ

[7] Nicolas Marti and Reynald Affeldt. A certified verifier for a fragment of separation logic. Computer Software, 25(3):135--147, 2008. [ bib ]
Japan Society for Software Science and Technology. Iwanami Shoten pdf preprint オープンアクセス doi プロジェクト ページ Reprinted to Information and Media Technologies 4(2):304--316, 2009 doi

[8] Reynald Affeldt, 小林 直樹, and 米澤 明憲. Verification of concurrent programs using the Coq proof assistant: a case study. IPSJ Transactions on Programming, 46(1):110--120, 2005. [ bib ]
pdf preprint Information Processing Society of Japan. Reprinted to IPSJ Digital Courier 1:117--127, 2005 オープンアクセス doi プロジェクト ページ

国際会議(査読ありProceedings)

intinproceedings_jp
[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), Paris, France, January 16--17, 2017, pages 30--42. ACM Press, Jan 2017. [ bib ]
pdf preprint doi プロジェクト ページ スライド

[2] 田中 哲, 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), Tokyo, Japan, November 14--18, 2016, volume 10009 of Lecture Notes in Computer Science, pages 243--260. Springer, Nov 2016. [ bib ]
pdf preprint doi プロジェクト ページ

[3] Reynald Affeldt, Jacques Garrigue, and 才川 隆文. Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. In International Symposium on Information Theory and Its Applications (ISITA 2016), Monterey, California, USA, October 30--November 2, 2016, pages 537--541. IEICE. IEEE Xplore, Oct 2016. [ bib ]
pdf preprint プロジェクト ページ

[4] 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), Nanjing, China, August 24--27, 2015, volume 9236 of Lecture Notes in Computer Science, pages 17--33. Springer, Aug 2015. [ bib ]
pdf preprint doi プロジェクト ページ

[5] 小尾 良介, 萩原 学, and Reynald Affeldt. Formalization of variable-length source coding theorem: Direct part. In International Symposium on Information Theory and Its Applications (ISITA 2014), Melbourne, Australia, October 26--29, 2014, pages 201--205. IEICE. IEEE Xplore, Oct 2014. [ bib ]

[6] 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), Rome, Italy, January 22, 2013, pages 35--46. ACM Press, Jan 2013. [ bib ]
pdf preprint doi

[7] Reynald Affeldt and 萩原 学. Formalization of Shannon's theorems in SSReflect-Coq. In 3rd Conference on Interactive Theorem Proving (ITP 2012), Princeton, New Jersey, USA, August 13--15, 2012, volume 7406 of Lecture Notes in Computer Science, pages 233--249. Springer, Aug 2012. [ bib ]
pdf preprint doi プロジェクト ページ スライド

[8] Reynald Affeldt. On construction of a library of formally verified low-level arithmetic functions. In 27th ACM SIGAPP Symposium On Applied Computing (SAC 2012), Riva del Garda (Trento), Italy, March 26--30, 2012, volume 2, pages 1326--1331. ACM Press, Mar 2012. [ bib ]
pdf preprint doi Software Verification and Testing Track プロジェクト ページ

[9] Reynald Affeldt, David Nowak, and 大岩 寛. Formal network packet processing with minimal fuss: Invertible syntax descriptions at work. In 6th ACM SIGPLAN Workshop Programming Languages meets Program Verification (PLPV 2012), Philadelphia, USA, January 24, 2012, pages 27--36. ACM Press, Jan 2012. [ bib ]
pdf preprint doi

[10] Reynald Affeldt, David Nowak, and 山田 聖. Certifying assembly with formal cryptographic proofs: the case of BBS. In Electronic Communications of the EASST, volume 23. European Association of Software Science and Technology, Jan 2010. [ bib ]
pdf preprint doi プロジェクト ページ Proceedings of the 9th International Workshop on Automated Verification of Critical Systems (AVoCS 2009), Swansea University Computer Science, September 23--25, 2009. Preliminary version: Technical Report of Computer Science, Swansea University CSR-2-2009

[11] 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, Jun 2008. [ bib ]
pdf preprint プロジェクト ページ

[12] Reynald Affeldt, 田中 三貴, and Nicolas Marti. Formal proof of provable security by game-playing in a proof assistant. In 1st International Conference on Provable Security (Provsec 2007), Wollongong, NSW, Australia, November 1--2, 2007, volume 4784 of Lecture Notes in Computer Science, pages 151--168. Springer, Nov 2007. [ bib ]
pdf preprint doi

[13] 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, Tokyo, Japan, December 6--8, 2006, volume 4435 of Lecture Notes in Computer Science, pages 346--360. Springer, Jan 2008. [ bib ]
pdf preprint doi プロジェクト ページ

[14] Nicolas Marti, Reynald Affeldt, and 米澤 明憲. 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, Oct 2006. [ bib ]
pdf preprint doi

[15] Reynald Affeldt and 小林 直樹. Partial order reduction for verification of spatial properties of pi-calculus processes. Electronic Notes in Theoretical Computer Science, 128(2):151--168, Apr 2005. [ bib ]
pdf preprint pdf preprint doi Elsevier. Proceedings of the 11th International Workshop on Expressiveness in Concurrency (EXPRESS 2004), London, UK, August 30, 2004

[16] Reynald Affeldt and 小林 直樹. A Coq library for verification of concurrent programs. Electronic Notes in Theoretical Computer Science, 199:17--32, Feb 2008. [ bib ]
pdf preprint doi プロジェクト ページ Elsevier. Proceedings of the 4th International Workshop on Logical Frameworks and Meta-Languages (LFM 2004), Cork, Ireland, July 5, 2004

[17] Reynald Affeldt and 小林 直樹. 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, Feb 2003. [ bib ]
pdf preprint doi スライド

[18] Reynald Affeldt, 増原 英彦, 住井 英二郎, and 米澤 明憲. 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, September 12--14, 2002, pages 50--60. ACM Press, Sep 2002. [ bib ]
pdf preprint doi スライド

国際学会(査読あり概要・発表)

inttalks_jp
[1] Reynald Affeldt and Jacques Garrigue. Formalization of error-correcting codes using SSReflect. The 6th Coq Workshop, Vienna, Austria, July 7, 2014, Jul 2014. [ bib ]
プロジェクト ページ

[2] Reynald Affeldt and 坂口 和彦. First building blocks for implementations of security protocols verified in Coq. The 5th Coq Workshop, Rennes, France, July 22, 2013, Jul 2013. [ bib ]
プロジェクト ページ

国内学会(査読ありProceedings)

dominproceedings_ref_jp
[1] 田中 哲, Reynald Affeldt, and Jacques Garrigue. Formal verification of the rank function for succinct data structures. In 第18 回プログラミングおよびプログラミング言語ワークショップ(PPL2016), 岡山県玉野市, March 7--9, 2016, Mar 2016. [ bib ]
15 pages. 論文賞 conference website プロジェクト ページ

[2] 平井 洋一 and Reynald Affeldt. What could Coq do for database software?---a progress report. In 25th Journées Francophones des Langages Applicatifs (JFLA 2014), Fréjus, France, January 8--11, pages 33--48, Jan 2014. [ bib ]

[3] Reynald Affeldt. Toward formal construction of assembly arithmetic functions from pseudo-code. In 第12 回プログラミングおよびプログラミング言語ワークショップ(PPL2010), 香川県琴平温泉, March 3--5, 2010, pages 1--14, Mar 2010. [ bib ]
pdf preprint conference website プロジェクト ページ

[4] Nicolas Marti and Reynald Affeldt. A certified verifier for a fragment of separation logic. In 第9 回プログラミングおよびプログラミング言語ワークショップ(PPL2007), 石川県加賀市, March 8--10, 2007, pages 187--199, Mar 2007. [ bib ]
論文賞 プロジェクト ページ

国内学会(査読なしProceedings)

dominproceedings_nonref_jp
[1] Reynald Affeldt and Cyril Cohen. Formal foundations for rigid body transformation. In 日本ソフトウェア科学会 第33 回大会 講演論文集 (JSSST 2016), 宮城県仙台市, September 6--9, 2016, Sep 2016. [ bib ]
11 pages プロジェクト ページ 日本語でのタイトル: 剛体変換のための形式基礎

[2] Reynald Affeldt. An intrinsic encoding of a subset of C and its application to TLS network packet processing. In 日本応用数理学会 2015 年度年会 講演予稿集, 金沢大学, 角間キャンパス, September 9-11, 2015, pages 306--307, Sep 2015. [ bib ]
プロジェクト ページ

[3] Reynald Affeldt and Jacques Garrigue. Formalization of error-correcting codes using SSReflect. In MI Lecture Note 研究集会 高信頼な理論と実装のための定理証明および定理証明器 (TPP2014), 九州大学, December 3--5, 2014, volume 61, pages 76--78, Dec 2014. [ bib ]
プロジェクト ページ

[4] Reynald Affeldt. Formalization of Shannon's theorems using the Coq proof-assistant. In 2013年電子情報通信学会ソサイエティ大会 基礎・境界 講演論文集, 福岡工業大学, September 17--20, 2013, pages 39--44, Sep 2013. [ bib ]
pdf preprint プロジェクト ページ conference website IEICE, Technical Committee on Information Theory

[5] Reynald Affeldt. About the formal verification of Shannon's theorems. In COE Lecture Note 九州大学 マス・フォア・インダストリ研究所, 共同利用研究集会II:モダン符号理論からポストモダン符号理論への展望, 九州大学, March 4--7, 2013, volume 44, pages 86--94, Mar 2013. [ bib ]
pdf preprint プロジェクト ページ

[6] Reynald Affeldt. Toward a library of verified arithmetic functions. In 日本応用数理学会 2011 年度年会 講演予稿集, 同志社大学, September 14--16, 2011, pages 377--378, Sep 2011. [ bib ]
プロジェクト ページ

[7] Reynald Affeldt and 山田 聖. Formal verification of C programs for implementations of communication protocols. In 日本ソフトウェア科学会 第28 回大会 講演論文集 (JSSST 2011), 沖縄県那覇市, September 26--29, 2011, Sep 2011. [ bib ]
pdf preprint プロジェクト ページ

[8] Reynald Affeldt, David Nowak, and 山田 聖. 形式的な暗号学的安全性証明によるアセンブリプログラムの安全性検証:bbsの事例. In 日本応用数理学会 2009 年度年会 講演予稿集 (JSIAM 2009), 大阪大学, September 28--30, 2009, pages 53--54, Sep 2009. [ bib ]
pdf preprint (日本語) プロジェクト ページ

[9] Reynald Affeldt and Hubert Comon-Lundh. Towards verification with no false attack of security protocols in first-order logic. In 日本応用数理学会 2008 年度年会 講演予稿集 (JSIAM 2008), 東京大学, 柏キャンパス, September 17--19, 2008, pages 177--178, Sep 2008. [ bib ]
pdf preprint スライド プロジェクト ページ

[10] Reynald Affeldt and 川本 裕輔. Report on FCS-ARSPA-WITS, CSF, FCC'08---about automated verification and certification. In 日本応用数理学会 2008 年度年会 講演予稿集, 東京大学, 柏キャンパス, September 17--19, 2008, pages 187--188, Sep 2008. [ bib ]
日本語でのタイトル: FCS-ARSPA-WITS, CSF, FCC'08参加報告---自動検証と形式的証明について

[11] 川本 裕輔 and Reynald Affeldt. FCS-ARSPA-WITS, CSF, FCC'08参加報告---安全性の形式化について. In 日本応用数理学会 2008 年度年会 講演予稿集, 東京大学, 柏キャンパス, September 17--19, 2008, pages 185--186, Sep 2008. [ bib ]
(日本語)

[12] Reynald Affeldt, 田中 三貴, and Nicolas Marti. 証明可能安全性の形式的証明:定理証明ツールによるゲームの手法. In 日本応用数理学会 2017 年度年会 講演予稿集 (JSIAM 2007), 北海道大学, September 15--17, 2007, pages 44--45, Sep 2007. [ bib ]
pdf preprint (日本語)

[13] Reynald Affeldt and Nicolas Marti. Formal verification of arithmetic functions in SmartMIPS assembly. In 日本ソフトウェア科学会 第23 回大会 講演論文集, 東京大学, 本郷キャンパス, September 13--15, 2006, Sep 2006. [ bib ]
pdf preprint プロジェクト ページ

[14] Nicolas Marti, Reynald Affeldt, and 米澤 明憲. Model-checking of a multi-threaded operating system. In 日本ソフトウェア科学会 第23 回大会 講演論文集, 東京大学, 本郷キャンパス, September 13--15, 2006, Sep 2006. [ bib ]
pdf preprint プロジェクト ページ

[15] Nicolas Marti, Reynald Affeldt, and 米澤 明憲. Towards formal verification of memory properties using separation logic. In 日本ソフトウェア科学会 第22 回大会 講演論文集, 東北大学, 青葉山キャンパス, September 13--15, 2005, Sep 2005. [ bib ]
pdf preprint スライド プロジェクト ページ

[16] Reynald Affeldt, 増原 英彦, 住井 英二郎, and 米澤 明憲. Supporting objects in run-time bytecode specialization. In 日本ソフトウェア科学会 第18 回大会 講演論文集 (JSSST 2011), 公立はこだて未来大学, September 18--20, 2001, Sep 2001. [ bib ]
pdf preprint

国内学会(発表のみ)

domtalks_jp
[1] 田中 哲, Reynald Affeldt, and Jacques Garrigue. Safe low-level code generation in Coq using monomorphization and monadification. 2017. [ bib ]
第114 回プログラミング研究発表会 情報処理学会プログラミング研究会, 静岡市, 2017/06/09

[2] 田中 哲, Reynald Affeldt, and Jacques Garrigue. Certified mon{omorphiz|adific}ation of Gallina for low-level code extraction. Mar 2017. [ bib ]
ポスター. 第19 回プログラミングおよびプログラミング言語ワークショップ(PPL2017), 山梨県笛吹市, 2017/03/09, (日本語)

[3] Reynald Affeldt. Coq coding sprint参加報告. Sep 2015. [ bib ]
弟11 回定理証明及び定理証明系ミーティング (TPP2015), 神奈川大学, 湘南ひらつかキャンパス, 2015/09/17, (日本語)

[4] Reynald Affeldt and 坂口 和彦. Coqによるcプログラムの検証基盤のデモ. Mar 2014. [ bib ]
ポスター. 第16 回プログラミングおよびプログラミング言語ワークショップ(PPL2014), 熊本県阿蘇市, 2014/03/05, (日本語)

[5] Reynald Affeldt and 坂口 和彦. C言語プログラムの形式検証のためのcoqライブラリの紹介. Nov 2013. [ bib ]
弟9 回定理証明及び定理証明系ミーティング (TPP2013), 信州大学, 2013/11/21, (日本語)

[6] Reynald Affeldt and 坂口 和彦. First building blocks for implementations of security protocols verified in Coq. Sep 2013. [ bib ]
ポスター. 日本ソフトウェア科学会 第30 回大会, 東京大学, 本郷キャンパス, 2013/09/10

[7] Reynald Affeldt, 萩原 学, and Jonas Sénizergues. Formal verification of Shannon's theorems. Nov 2012. [ bib ]
弟8 回定理証明及び定理証明系ミーティング (TPP2012), 千葉大学, 2012/11/21

[8] Reynald Affeldt and 萩原 学. シャノンの定理の形式化. Mar 2012. [ bib ]
日本応用数理学会 2012 年春の研究部会連合発表会, 九州大学, 2012/03/08, (日本語)

[9] Reynald Affeldt. On construction of a library of formally verified low-level arithmetic functions. Nov 2011. [ bib ]
弟7 回定理証明及び定理証明系ミーティング (TPP2011), 産業技術総合研究所 (AIST), つくば中央, 2011/11/17

[10] Reynald Affeldt and 山田 聖. 分離論理を用いた,c言語プログラムの機械的検証. Mar 2011. [ bib ]
ポスター. 第13 回プログラミングおよびプログラミング言語ワークショップ(PPL2011), 北海道札幌市, 2011/03/10

[11] Reynald Affeldt. Instrumenting error-correcting codes with SSReflect. Nov 2010. [ bib ]
弟6 回定理証明及び定理証明系ミーティング (TPP2010), 名古屋大学, 2010/11/26

[12] Reynald Affeldt. SSReflectに よる符号理論の形式化に関する一考察. Mar 2010. [ bib ]
日本応用数理学会 2010 年春の研究部会連合発表会 (JSIAM Spring 2010), 筑波大学, 2010/03/08, (日本語) スライド

[13] Reynald Affeldt, David Nowak, and 山田 聖. Certifying assembly with formal cryptographic proofs: the case of BBS. Nov 2009. [ bib ]
弟5 回定理証明及び定理証明系ミーティング (TPP2009), 関西学院大学, 2009/11/21

[14] Reynald Affeldt. Coq上 での組込み用途の冪剰余の検証. Mar 2009. [ bib ]
ポスター. 第11 回プログラミングおよびプログラミング言語ワークショップ(PPL2009), 岐阜県高山市, 2009/03/09 ポスター ファイル

[15] Reynald Affeldt. Verification of security protocols with a bounded number of sessions based on resolution for rigid variables. Nov 2008. [ bib ]
弟4 回定理証明及び定理証明系ミーティング (TPP2008), 東北大学, 2008/11/26

[16] Nicolas Marti, Reynald Affeldt, and 米澤 明憲. Tools and experiments for formal verification of operating systems. Mar 2006. [ bib ]
ポスター. 第8 回プログラミングおよびプログラミング言語ワークショップ(PPL2006), 滋賀県大津市, 2006/03/05

[17] Reynald Affeldt, 小林 直樹, and 米澤 明憲. Verification of concurrent programs using the Coq theorem prover: a case study. Jul 2004. [ bib ]
並列/分散/協調処理に関するサマー・ワークショップ(SWoPP 2004), 青森, 2004/07/30

解説記事

outreach_jp
[1] Reynald Affeldt. Mathematical components入門. コンピュータソフトウェア, 34:64--74, Apr 2017. [ bib ]
(日本語) オープンアクセス doi 日本ソフトウェア科学会 journal website

[2] Reynald Affeldt. 形式的な符号理論に向けて. 進化する符号理論, 第15章, 萩原 学 (編著), pages 171--189, Sep 2016. [ bib ]
(日本語) 日本評論社 book website

[3] Reynald Affeldt. 定理証明支援系に基づく形式検証---近年の実例の紹介とCoq入門---. 情報処理, 55:482--491, May 2014. [ bib ]
(日本語) オープンアクセス 情報処理学会 magazine website

[4] Reynald Affeldt. 形式的な符号理論に向けて. 数学セミナー, 618:74--79, Apr 2013. [ bib ]
(日本語) 日本評論社 journal website


This file was generated by bibtex2html 1.98.