@INPROCEEDINGS{marti05jssst,
AUTHOR = {Nicolas Marti and Reynald Affeldt and Akinori Yonezawa},
TITLE = {Towards Formal Verification of Memory Properties using Separation Logic},
BOOKTITLE = {22nd Meeting of the Japan Society for Software Science and Technology, Tohoku University, Sendai, Japan, September 13--15, 2005},
YEAR = {2005},
MONTH = {Sep.},
PUBLISHER = {Japan Society for Software Science and Technology},
NOTE = {Electronic proceedings (ISSN 1348-0901). Not referred. 6 pages. Slides: \url{http://web.yl.is.s.u-tokyo.ac.jp/~affeldt/documents/seplog-jssst.pdf}},
URL = {http://web.yl.is.s.u-tokyo.ac.jp/%7Eaffeldt/documents/marti-affeldt-yonezawa.pdf}
}
@INPROCEEDINGS{marti06space,
AUTHOR = {Nicolas Marti and Reynald Affeldt and Akinori Yonezawa},
TITLE = {Verification of the Heap Manager of an Operating System using Separation Logic},
BOOKTITLE = {3rd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE 2006), Charleston SC, USA, January 14, 2006},
YEAR = {2006},
PAGES = {61--72},
MONTH = {Jan.},
NOTE = {Informal proceedings. \url{http://staff.aist.go.jp/reynald.affeldt/documents/nicolas-space06.ps}{Slides}.},
URL = {http://staff.aist.go.jp/reynald.affeldt/documents/space06.pdf}
}
@INPROCEEDINGS{marti06icfem,
AUTHOR = {Nicolas Marti and Reynald Affeldt and Akinori Yonezawa},
TITLE = {Formal Verification of the Heap Manager of an Operating System using Separation Logic},
BOOKTITLE = {8th International Conference on Formal Engineering Methods (ICFEM 2006), Macao SAR, China, October 29--November 3, 2006},
PAGES = {400--419},
YEAR = {2006},
EDITOR = {Zhiming Liu and He Jifeng},
VOLUME = {4260},
OPTNUMBER = {},
SERIES = {Lecture Notes in Computer Science},
OPTADDRESS = {},
MONTH = {Oct.},
OPTORGANIZATION = {},
PUBLISHER = {Springer-Verlag},
NOTE = {To appear. \url{http://savannah.nongnu.org/projects/seplog}{Coq scripts}. Revised and augmented version of \cite{marti06space}},
URL = {http://staff.aist.go.jp/reynald.affeldt/documents/icfem06.pdf}
}
@INPROCEEDINGS{marti06jssst,
AUTHOR = {Nicolas Marti and Reynald Affeldt and Akinori Yonezawa},
TITLE = {Model-checking of a Multi-threaded Operating System},
BOOKTITLE = {23rd Workshop of the Japan Society for Software Science and Technology, University of Tokyo, Tokyo, Japan, September 13--15, 2006},
YEAR = {2006},
MONTH = {Sep.},
PUBLISHER = {Japan Society for Software Science and Technology},
NOTE = {Electronic proceedings. Not referred. 6 pages. \url{http://staff.aist.go.jp/reynald.affeldt/seplog}{Spin model}.},
URL = {http://staff.aist.go.jp/reynald.affeldt/documents/marti-jssst2006-en.pdf}
}
@INPROCEEDINGS{affeldt06jssst,
AUTHOR = {Reynald Affeldt and Nicolas Marti},
TITLE = {Formal Verification of Arithmetic Functions in SmartMIPS Assembly},
BOOKTITLE = {23rd Workshop of the Japan Society for Software Science and Technology, University of Tokyo, Tokyo, Japan, September 13--15, 2006},
YEAR = {2006},
MONTH = {Sep.},
PUBLISHER = {Japan Society for Software Science and Technology},
NOTE = {Electronic proceedings. Not referred. 6 pages.},
URL = {http://staff.aist.go.jp/reynald.affeldt/documents/affeldt-jssst2006-en.pdf}
}
@INPROCEEDINGS{affeldt06asian,
AUTHOR = {Reynald Affeldt and Nicolas Marti},
TITLE = {An Approach to Formal Verification of Arithmetic Functions in Assembly},
BOOKTITLE = {11th Annual Asian Computing Science Conference (ASIAN 2006), Focusing on Secure Software and Related Issues},
OPTPAGES = {},
YEAR = {2006},
OPTEDITOR = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {Lecture Notes in Computer Science},
OPTADDRESS = {},
MONTH = {Dec.},
OPTORGANIZATION = {},
OPTPUBLISHER = {Springer-Verlag},
NOTE = {To appear in Lecture Notes in Computer Science, Springer-Verlag. \url{http://staff.aist.go.jp/reynald.affeldt/documents/affeldt-asian2006.pdf}{Preprint}. Revised and extended version of \cite{affeldt06jssst}.},
OPTURL = {http://staff.aist.go.jp/reynald.affeldt/documents/affeldt-asian2006.pdf}
}
@INPROCEEDINGS{marti07ppl,
AUTHOR = {Nicolas Marti and Reynald Affeldt},
TITLE = {A Certified Verifier for a Fragment of Separation Logic},
BOOKTITLE = {9th JSSST Workshop on Programming and Programming Languages (PPL 2007)},
YEAR = {2007},
MONTH = {Mar.},
PUBLISHER = {Japan Society for Software Science and Technology},
NOTE = {13 pages. Best paper award. \url{http://savannah.nongnu.org/projects/seplog}{Coq scripts}. \url{http://web.yl.is.s.u-tokyo.ac.jp/~nicolas/bigtoe}{Interactive Demo}. Informal proceedings.},
URL = {http://staff.aist.go.jp/reynald.affeldt/documents/ppl2007.pdf}
}
@INPROCEEDINGS{affeldt07provsec,
AUTHOR = {Reynald Affeldt and Miki Tanaka and Nicolas Marti},
TITLE = {Formal Proof of Provable Security by Game-playing in a Proof Assistant},
BOOKTITLE = {1st International Conference on Provable Security (Provsec 2007)},
OPTPAGES = {},
YEAR = {2007},
EDITOR = {Willy Susilo and Joseph K.~Liu and Yi Mu},
OPTVOLUME = {},
OPTNUMBER = {},
OPTSERIES = {Lecture Notes in Computer Science},
OPTADDRESS = {},
OPTMONTH = {Oct.},
OPTORGANIZATION = {},
OPTPUBLISHER = {},
NOTE = {To appear in Lecture Notes in Computer Science, Springer-Verlag. \url{http://staff.aist.go.jp/reynald.affeldt/documents/abstract_provsec2007.txt}{Abstract}.},
OPTANNOTE = {}
}
This file has been generated by bibtex2html 1.77