| [1] |
Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa.
Towards formal verification of memory properties using separation
logic.
In 22nd Meeting of the Japan Society for Software Science and
Technology, Tohoku University, Sendai, Japan, September 13-15, 2005. Japan
Society for Software Science and Technology, Sep. 2005.
Electronic proceedings (ISSN 1348-0901). Not referred. 6 pages.
Slides:
http://web.yl.is.s.u-tokyo.ac.jp/~affeldt/documents/seplog-jssst.pdf. [ bib | .pdf ] |
| [2] |
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, Jan. 2006.
Informal proceedings.
http://staff.aist.go.jp/reynald.affeldt/documents/nicolas-space06.psSlides. [ bib | .pdf ] |
| [3] |
Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa.
Formal verification of the heap manager of an operating system using
separation logic.
In Zhiming Liu and He Jifeng, editors, 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-Verlag, Oct. 2006.
To appear. http://savannah.nongnu.org/projects/seplogCoq
scripts. Revised and augmented version of [2]. [ bib | .pdf ] |
| [4] |
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. Japan
Society for Software Science and Technology, Sep. 2006.
Electronic proceedings. Not referred. 6 pages.
http://staff.aist.go.jp/reynald.affeldt/seplogSpin model. [ bib | .pdf ] |
| [5] |
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. Japan
Society for Software Science and Technology, Sep. 2006.
Electronic proceedings. Not referred. 6 pages. [ bib | .pdf ] |
| [6] |
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, Dec. 2006.
To appear in Lecture Notes in Computer Science, Springer-Verlag.
http://staff.aist.go.jp/reynald.affeldt/documents/affeldt-asian2006.pdfPreprint. Revised and extended version of [5]. [ bib ] |
| [7] |
Nicolas Marti and Reynald Affeldt.
A certified verifier for a fragment of separation logic.
In 9th JSSST Workshop on Programming and Programming Languages
(PPL 2007). Japan Society for Software Science and Technology, Mar. 2007.
13 pages. Best paper award.
http://savannah.nongnu.org/projects/seplogCoq scripts.
http://web.yl.is.s.u-tokyo.ac.jp/~nicolas/bigtoeInteractive Demo.
Informal proceedings. [ bib | .pdf ] |
| [8] |
Reynald Affeldt, Miki Tanaka, and Nicolas Marti.
Formal proof of provable security by game-playing in a proof
assistant.
In Willy Susilo, Joseph K. Liu, and Yi Mu, editors, 1st
International Conference on Provable Security (Provsec 2007), 2007.
To appear in Lecture Notes in Computer Science, Springer-Verlag.
http://staff.aist.go.jp/reynald.affeldt/documents/abstract_provsec2007.txtAbstract. [ bib ] |
This file has been generated by bibtex2html 1.77