Research Bibliography

1. Reynald Affeldt. On Construction of a Library of Formally Verified Low-level Arithmetic Functions. In 27th Symposium On Applied Computing (SAC 2012), March 26-30, 2012, Riva del Garda (Trento), Italy. 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 PUBLICATION, {VOL\#, ISS\#, (DATE)} http://doi.acm.org/10.1145/{nnnnnn.nnnnnn}. To appear. 6 pages. Latest Coq Documentation
2. 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, {VOL\#, ISS\#, (Jan. 2012)} http://doi.acm.org/10.1145/2103776.2103780. ACM Digital Library.
3. Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying Assembly with Formal Security Proofs: the Case of BBS. Science of Computer Programming, in press, Elsevier, 2012.↵
   doi. Extended version of this paper. Coq scripts (as of January 2011). Latest Coq Documentation
4. Reynald Affeldt and Kiyoshi Yamada. A Coq Starter Kit to Verify TLS Packet Processing in C. Draft. pdf. ↵
   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.
5. 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. Coq Documentation
6. 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. ECEASST 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).
7. 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. pdf. ↵
   ©Springer. Springer online.
8. 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.
9. 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. pdf. ↵
   ©Springer. Springer online. 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.
10. 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 Best Paper Award. Coq scripts (as of 2007). Interactive Demo.
11. 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. pdf. ↵
    ©Springer. Springer online. Up-to-date Coq Documentation.
12. 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.
13. 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.
14. 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.
15. 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. pdf. ↵
    ©Springer. Springer online. Coq scripts. Coq Documentation of an up-to-date version.
16. 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.
17. 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.
18. 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.
19. 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.
20. 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.
21. 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.
22. 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.
23. 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. pdf. ↵
    ©Springer. Springer online. Coq scripts. Slides.
24. 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. ↵
    Copyright notice. ACM Digital library. Slides.
25. 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.
26. 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.