Research Bibliography

日本語版

  1. Academic Journals
  2. International Conferences (refereed proceedings)
  3. International Workshops (refereed talks)
  4. Domestic Conferences (refereed proceedings)
  5. Domestic Conferences (non-refereed proceedings)
  6. Domestic Conferences (presentation only)
  7. Outreach

Academic Journals

article_en
[1] Reynald Affeldt and 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. [ bib ]
pdf preprint open access doi project page

[2] Reynald Affeldt, Manabu Hagiwara, and Jonas Sénizergues. Formalization of Shannon's theorems. Journal of Automated Reasoning, 53(1):63--103, 2014. [ bib ]
pdf preprint doi project page

[3] 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 ]
pdf preprint doi project page NASA/Springer

[4] 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. [ bib ]
pdf preprint doi project page

[5] 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 project page

[6] Nicolas Marti and Reynald Affeldt. A certified verifier for a fragment of separation logic. Computer Software, 25(3):135--147, 2008. [ bib ]
pdf preprint open access doi Japan Society for Software Science and Technology. Iwanami Shoten. project page Reprinted to Information and Media Technologies 4(2):304--316, 2009 doi

[7] 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, 2005. [ bib ]
pdf preprint Information Processing Society of Japan. project page Reprinted to IPSJ Digital Courier 1:117--127, 2005 open access doi

International Conferences (refereed proceedings)

intinproceedings_en
[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 project page slides

[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), Tokyo, Japan, November 14--18, 2016, volume 10009 of Lecture Notes in Computer Science, pages 243--260. Springer, Nov 2016. [ bib ]
pdf preprint doi project page

[3] Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. 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 project page

[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 project page

[5] Ryosuke Obi, Manabu Hagiwara, 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 Manabu Hagiwara. 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 project page slides

[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 project page

[9] 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), Philadelphia, USA, January 24, 2012, pages 27--36. ACM Press, Jan 2012. [ bib ]
pdf preprint doi

[10] Reynald Affeldt, David Nowak, and Kiyoshi Yamada. 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 project page 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 project page

[12] 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), 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 project page

[14] 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, Oct 2006. [ bib ]
pdf preprint doi

[15] 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, 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 Naoki Kobayashi. A Coq library for verification of concurrent programs. Electronic Notes in Theoretical Computer Science, 199:17--32, Feb 2008. [ bib ]
pdf preprint doi project page Elsevier. Proceedings of the 4th International Workshop on Logical Frameworks and Meta-Languages (LFM 2004), Cork, Ireland, July 5, 2004

[17] 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, Feb 2003. [ bib ]
pdf preprint doi slides

[18] Reynald Affeldt, Hidehiko Masuhara, Eijiro Sumii, and 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, September 12--14, 2002, pages 50--60. ACM Press, Sep 2002. [ bib ]
pdf preprint doi slides

International Workshops (refereed talks)

inttalks_en
[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 ]
project page

[2] Reynald Affeldt and Kazuhiko Sakaguchi. First building blocks for implementations of security protocols verified in Coq. The 5th Coq Workshop, Rennes, France, July 22, 2013, Jul 2013. [ bib ]
project page

Domestic Conferences (refereed proceedings)

dominproceedings_ref_en
[1] Akira Tanaka, Reynald Affeldt, and Jacques Garrigue. Formal verification of the rank function for succinct data structures. In 18th Workshop on Programming and Programming Languages (PPL2016), Okayama-ken, Tamano-shi, March 7--9, 2016, Mar 2016. [ bib ]
15 pages. Best paper award conference website project page

[2] Yoichi Hirai 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 12th Workshop on Programming and Programming Languages (PPL2010), Kagawa-ken, Kotohira Onsen, March 3--5, 2010, pages 1--14, Mar 2010. [ bib ]
pdf preprint conference website project page

[4] Nicolas Marti and Reynald Affeldt. A certified verifier for a fragment of separation logic. In 9th Workshop on Programming and Programming Languages (PPL2007), Ishikawa-ken, Kaga-shi, March 8--10, 2007, pages 187--199, Mar 2007. [ bib ]
Best paper award project page

Domestic Conferences (non-refereed proceedings)

dominproceedings_nonref_en
[1] Reynald Affeldt and Cyril Cohen. Formal foundations for rigid body transformation. In the proceedings of the 33rd Meeting of the Japan Society for Software Science and Technology (JSSST 2016), Miyagi-ken, Sendai-shi, September 6--9, 2016, Sep 2016. [ bib ]
11 pages project page

[2] Reynald Affeldt. An intrinsic encoding of a subset of C and its application to TLS network packet processing. In Annual Workshop of the Japan Society for Industrial and Applied Mathematics 2015, Kanazawa University, Kakuma campus, September 9-11, 2015, pages 306--307, Sep 2015. [ bib ]
project page

[3] Reynald Affeldt and Jacques Garrigue. Formalization of error-correcting codes using SSReflect. In MI Lecture Note Workshop on Theorem proving and provers for reliable theory and implementations (TPP2014), Kyushu University, December 3--5, 2014, volume 61, pages 76--78, Dec 2014. [ bib ]
project page

[4] Reynald Affeldt. Formalization of Shannon's theorems using the Coq proof-assistant. In proceedings of the 2013 IEICE General Conference, The Institute of Electronics, Information and Communication Engineers, Fukuoka Institute of Technology, September 17--20, 2013, pages 39--44, Sep 2013. [ bib ]
pdf preprint project page conference website IEICE, Technical Committee on Information Theory

[5] Reynald Affeldt. About the formal verification of Shannon's theorems. In COE Lecture Note Kyushu University Institute of Mathematics for Industry, Workshop of the Joint Research Projects: From Modern Coding Theory To Postmodern Coding Theory, Kyushu University, March 4--7, 2013, volume 44, pages 86--94, Mar 2013. [ bib ]
pdf preprint project page

[6] Reynald Affeldt. Toward a library of verified arithmetic functions. In Annual Workshop of the Japan Society for Industrial and Applied Mathematics 2011, Doshisha University, September 14--16, 2011, pages 377--378, Sep 2011. [ bib ]
project page

[7] Reynald Affeldt and Kiyoshi Yamada. Formal verification of C programs for implementations of communication protocols. In the proceedings of the 28th Meeting of the Japan Society for Software Science and Technology (JSSST 2011), Okinawa-ken, Naha-shi, September 26--29, 2011, Sep 2011. [ bib ]
pdf preprint project page

[8] Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying assembly with formal cryptographic proofs: the case of BBS. In Annual Workshop of the Japan Society for Industrial and Applied Mathematics 2009 (JSIAM 2009), Osaka University, September 28--30, 2009, pages 53--54, Sep 2009. [ bib ]
pdf preprint (in Japanese) project page

[9] Reynald Affeldt and Hubert Comon-Lundh. Towards verification with no false attack of security protocols in first-order logic. In Annual Workshop of the Japan Society for Industrial and Applied Mathematics 2008 (JSIAM 2008), The University of Tokyo, Kashiwa campus, September 17--19, 2008, pages 177--178, Sep 2008. [ bib ]
pdf preprint slides project page

[10] Reynald Affeldt and Yusuke Kawamoto. Report on FCS-ARSPA-WITS, CSF, FCC'08---about automated verification and certification. In Annual Workshop of the Japan Society for Industrial and Applied Mathematics 2008, The University of Tokyo, Kashiwa campus, September 17--19, 2008, pages 187--188, Sep 2008. [ bib ]

[11] Yusuke Kawamoto and Reynald Affeldt. Report on FCS-ARSPA-WITS, CSF, FCC'08---about formalization of security properties. In Annual Workshop of the Japan Society for Industrial and Applied Mathematics 2008, The University of Tokyo, Kashiwa campus, September 17--19, 2008, pages 185--186, Sep 2008. [ bib ]
(in Japanese)

[12] Reynald Affeldt, Miki Tanaka, and Nicolas Marti. Formal proof of provable security by game-playing in a proof assistant. In Annual Workshop of the Japan Society for Industrial and Applied Mathematics 2017 (JSIAM 2007), Hokkaido University, September 15--17, 2007, pages 44--45, Sep 2007. [ bib ]
pdf preprint (in Japanese)

[13] Reynald Affeldt and Nicolas Marti. Formal verification of arithmetic functions in SmartMIPS assembly. In the proceedings of the 23rd Meeting of the Japan Society for Software Science and Technology, The University of Tokyo, Hongo campus, September 13--15, 2006, Sep 2006. [ bib ]
pdf preprint project page

[14] Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa. Model-checking of a multi-threaded operating system. In the proceedings of the 23rd Meeting of the Japan Society for Software Science and Technology, The University of Tokyo, Hongo campus, September 13--15, 2006, Sep 2006. [ bib ]
pdf preprint project page

[15] Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa. Towards formal verification of memory properties using separation logic. In the proceedings of the 22nd Meeting of the Japan Society for Software Science and Technology, Tohoko University, Aobayama campus, September 13--15, 2005, Sep 2005. [ bib ]
pdf preprint slides project page

[16] Reynald Affeldt, Hidehiko Masuhara, Eijiro Sumii, and Akinori Yonezawa. Supporting objects in run-time bytecode specialization. In the proceedings of the 18th Meeting of the Japan Society for Software Science and Technology (JSSST 2011), Future University Hakodate, September 18--20, 2001, Sep 2001. [ bib ]
pdf preprint

Domestic Conferences (presentation only)

domtalks_en
[1] Akira Tanaka, Reynald Affeldt, and Jacques Garrigue. Safe low-level code generation in Coq using monomorphization and monadification. 2017. [ bib ]
The 114th Meeting of the IPSJ SIG on Programming (PRO114), Shizuoka-shi, 2017/06/09

[2] Akira Tanaka, Reynald Affeldt, and Jacques Garrigue. Certified mon{omorphiz|adific}ation of Gallina for low-level code extraction. Mar 2017. [ bib ]
Poster. 19th Workshop on Programming and Programming Languages (PPL2017), Yamanashi-ken, Fuefuki-shi, 2017/03/09, (in Japanese)

[3] Reynald Affeldt. Report on the Coq coding sprint. Sep 2015. [ bib ]
11th Theorem Proving and Provers Meeting (TPP2015), Kanagawa University, Shonan Hiratsuka campus, 2015/09/17, (in Japanese)

[4] Reynald Affeldt and Kazuhiko Sakaguchi. Demo of a Coq library for verification of C programs. Mar 2014. [ bib ]
Poster. 16th Workshop on Programming and Programming Languages (PPL2014), Kumamoto-ken, Aso-shi, 2014/03/05, (in Japanese)

[5] Reynald Affeldt and Kazuhiko Sakaguchi. Presentation of a Coq library for formal verification of C programs. Nov 2013. [ bib ]
9th Theorem Proving and Provers Meeting (TPP2013), Shinshu University, 2013/11/21, (in Japanese)

[6] Reynald Affeldt and Kazuhiko Sakaguchi. First building blocks for implementations of security protocols verified in Coq. Sep 2013. [ bib ]
Poster. 30th Meeting of the Japan Society for Software Science and Technology, The University of Tokyo, Hongo campus, 2013/09/10

[7] Reynald Affeldt, Manabu Hagiwara, and Jonas Sénizergues. Formal verification of Shannon's theorems. Nov 2012. [ bib ]
8th Theorem Proving and Provers Meeting (TPP2012), Chiba University, 2012/11/21

[8] Reynald Affeldt and Manabu Hagiwara. Formalization of Shannon's theorems. Mar 2012. [ bib ]
Annual Spring Meeting of the Japan Society for Industrial and Applied Mathematics 2012, Kyushu University, 2012/03/08, (in Japanese)

[9] Reynald Affeldt. On construction of a library of formally verified low-level arithmetic functions. Nov 2011. [ bib ]
7th Theorem Proving and Provers Meeting (TPP2011), National Institute of Advanced Industrial Science and Technology (AIST), Tsukuba Central, 2011/11/17

[10] Reynald Affeldt and Kiyoshi Yamada. Mechanical verification of C programs using separation logic. Mar 2011. [ bib ]
Poster. 13th Workshop on Programming and Programming Languages (PPL2011), Hokkaido, Sapporo, 2011/03/10

[11] Reynald Affeldt. Instrumenting error-correcting codes with SSReflect. Nov 2010. [ bib ]
6th Theorem Proving and Provers Meeting (TPP2010), Nagoya University, 2010/11/26

[12] Reynald Affeldt. A note about the formalization of error-correcting codes using SSReflect. Mar 2010. [ bib ]
Annual Spring Meeting of the Japan Society for Industrial and Applied Mathematics 2010 (JSIAM Spring 2010), Tsukuba University, 2010/03/08, (in Japanese) slides

[13] Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying assembly with formal cryptographic proofs: the case of BBS. Nov 2009. [ bib ]
5th Theorem Proving and Provers Meeting (TPP2009), Kwansei Gakuin University, 2009/11/21

[14] Reynald Affeldt. Verification in coq of an implementation of modular exponentiation for an embedded system. Mar 2009. [ bib ]
Poster. 11th Workshop on Programming and Programming Languages (PPL2009), Gifu-ken, Takayama-shi, 2009/03/09 poster file

[15] Reynald Affeldt. Verification of security protocols with a bounded number of sessions based on resolution for rigid variables. Nov 2008. [ bib ]
4th Theorem Proving and Provers Meeting (TPP2008), Tohoko University, 2008/11/26

[16] Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa. Tools and experiments for formal verification of operating systems. Mar 2006. [ bib ]
Poster. 8th Workshop on Programming and Programming Languages (PPL2006), Shiga-ken, Ootsu-shi, 2006/03/05

[17] Reynald Affeldt, Naoki Kobayashi, and Akinori Yonezawa. Verification of concurrent programs using the Coq theorem prover: a case study. Jul 2004. [ bib ]
Summer United Workshops on Parallel, Distributed and Cooperative Processing (SWoPP 2004), Aomori, 2004/07/30

Outreach

outreach_en
[1] Reynald Affeldt. Introduction to Mathematical Components. Computer Software, 34:64--74, Apr 2017. [ bib ]
(in Japanese) open access doi Japan Society for Software Science and Technology journal website

[2] Reynald Affeldt. Towards formal coding theory. Chapter 15 of Evolving Theory of Error-correcting Codes, Manabu Hagiwara (editor), pages 171--189, Sep 2016. [ bib ]
(in Japanese) Nippon Hyoronsha book website

[3] Reynald Affeldt. Formal verification using proof-assistants: Recent results and introduction to coq. Information Processing, 55:482--491, May 2014. [ bib ]
(in Japanese) open access Information Processing Society of Japan magazine website

[4] Reynald Affeldt. Towards formal coding theory. Suugaku Seminaa (Mathematical Seminar), 618:74--79, Apr 2013. [ bib ]
(in Japanese) Nippon Hyoron sha co., Ltd journal website


This file was generated by bibtex2html 1.98.