article_en.bib

@article{tanaka2017jip,
  author = {Akira Tanaka and Reynald Affeldt and Jacques Garrigue},
  title = {Safe Low-level Code Generation in {Coq} using Monomorphization and Monadification},
  journal = {\href{http://www.ipsj.or.jp/english/jip/}{Journal of Information Processing}},
  year = {2017},
  volume = {},
  number = {},
  pages = {},
  abstract = {To appear \href{https://staff.aist.go.jp/tanaka-akira/succinct/}{project page}}
}
@article{affeldt2014jfr,
  author = {Reynald Affeldt and Kazuhiko Sakaguchi},
  title = {An Intrinsic Encoding of a Subset of {C} and its Application to {TLS} Network Packet Processing},
  journal = {\href{https://jfr.unibo.it/index}{Journal of Formalized Reasoning}},
  year = {2014},
  volume = {7},
  number = {1},
  pages = {63--104},
  abstract = {\href{http://staff.aist.go.jp/reynald.affeldt/documents/vtls-long.pdf}{pdf preprint} \href{https://jfr.unibo.it/article/download/4317/3950}{open access} \href{http://dx.doi.org/10.6092/issn.1972-5787/4317}{doi} \href{https://staff.aist.go.jp/reynald.affeldt/seplog/}{project page}}
}
@article{affeldt2014jar,
  author = {Reynald Affeldt and Manabu Hagiwara and Jonas S\'enizergues},
  title = {Formalization of {Shannon}'s Theorems},
  journal = {\href{https://link.springer.com/journal/10817}{Journal of Automated Reasoning}},
  year = {2014},
  volume = {53},
  number = {1},
  pages = {63--103},
  abstract = {\href{http://staff.aist.go.jp/reynald.affeldt/documents/shannon_theorems.pdf}{pdf preprint} \href{http://dx.doi.org/10.1007/s10817-013-9298-1}{doi}  \href{https://staff.aist.go.jp/reynald.affeldt/shannon/}{project page}}
}
@article{affeldt2013isse,
  author = {Reynald Affeldt},
  title = {On Construction of a Library of Formally Verified Low-level Arithmetic Functions},
  journal = {\href{http://www.springer.com/computer/swe/journal/11334}{Innovations in Systems and Software Engineering}},
  year = {2013},
  volume = {9},
  number = {2},
  pages = {59--77},
  abstract = {NASA/Springer \href{http://staff.aist.go.jp/reynald.affeldt/documents/arilib-affeldt-long.pdf}{pdf preprint} \href{http://dx.doi.org/10.1007/s11334-013-0195-x}{doi} \href{https://staff.aist.go.jp/reynald.affeldt/seplog/}{project page}}
}
@article{affeldt2012scp,
  author = {Reynald Affeldt and David Nowak and Kiyoshi Yamada},
  title = {Certifying Assembly with Formal Security Proofs: the Case of {BBS}},
  journal = {\href{https://www.journals.elsevier.com/science-of-computer-programming/}{Science of Computer Programming}},
  year = {2012},
  volume = {77},
  number = {10--11},
  pages = {1058--1074},
  abstract = {\href{http://staff.aist.go.jp/reynald.affeldt/documents/affeldt-bbs.pdf}{pdf preprint} \href{http://dx.doi.org/10.1016/j.scico.2011.07.003}{doi}  \href{https://staff.aist.go.jp/reynald.affeldt/bbs/}{project page}}
}
@inproceedings{affeldt2009rigid,
  author = {Reynald Affeldt and Hubert Comon-Lundh},
  title = {Verification of Security Protocols with a Bounded Number of Sessions based on Resolution for Rigid Variables},
  booktitle = {Formal to Practical Security},
  year = {2009},
  editor = {},
  volume = {5458},
  series = {Lecture Notes in Computer Science, State-of-the-Art Survey},
  pages = {1--20},
  month = {May},
  publisher = {Springer},
  abstract = {\href{http://staff.aist.go.jp/reynald.affeldt/documents/rigid.pdf}{pdf preprint} \href{http://dx.doi.org/10.1007/978-3-642-02002-5_1}{doi} \href{https://staff.aist.go.jp/reynald.affeldt/rigid/}{project page}}
}
@article{marti2008compsoft,
  author = {Nicolas Marti and Reynald Affeldt},
  title = {A Certified Verifier for a Fragment of Separation Logic},
  journal = {\href{https://www.jstage.jst.go.jp/browse/jssst}{Computer Software}},
  year = {2008},
  volume = {25},
  number = {3},
  pages = {135--147},
  abstract = {Japan Society for Software Science and Technology. Iwanami Shoten \href{http://staff.aist.go.jp/reynald.affeldt/documents/cs2007.pdf}{pdf preprint} \href{https://www.jstage.jst.go.jp/article/jssst/25/3/25_3_3_135/_pdf}{open access} \href{http://dx.doi.org/10.11309/jssst.25.3_135}{doi} \href{https://staff.aist.go.jp/reynald.affeldt/seplog/}{project page} Reprinted to \href{https://www.jstage.jst.go.jp/browse/imt}{Information and Media Technologies} 4(2):304--316, 2009 \href{http://dx.doi.org/10.11185/imt.4.304}{doi}}
}
@article{affeldt2005ipsj,
  author = {Reynald Affeldt and Naoki Kobayashi and Akinori Yonezawa},
  title = {Verification of concurrent programs using the {Coq} proof assistant: a case study},
  journal = {IPSJ Transactions on Programming},
  year = {2005},
  volume = {46},
  number = {1},
  pages = {110--120},
  abstract = {\href{http://staff.aist.go.jp/reynald.affeldt/documents/swopp04.pdf}{pdf preprint} Information Processing Society of Japan. Reprinted to \href{https://www.jstage.jst.go.jp/browse/imt}{IPSJ Digital Courier} 1:117--127, 2005 \href{https://www.jstage.jst.go.jp/article/ipsjdc/1/0/1_0_117/_pdf}{open access} \href{http://dx.doi.org/10.2197/ipsjdc.1.117}{doi} \href{https://staff.aist.go.jp/reynald.affeldt/applpi/}{project page}}
}

This file was generated by bibtex2html 1.98.