Commit 31ca6074 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

apply to collection.bib

parent 4abdb135
......@@ -2,392 +2,501 @@
@STRING{SV = {Springer}}
@article{1969-Hoare,
author = {C. A. R. Hoare},
title = {An Axiomatic Basis for Computer Programming},
journal = {Commun. ACM},
issue_date = {Oct. 1969},
volume = {12},
number = {10},
month = {oct},
year = {1969},
issn = {0001-0782},
pages = {576-580},
numpages = {5},
note = {\url{http://doi.acm.org/10.1145/363235.363259}},
url = {http://doi.acm.org/10.1145/363235.363259},
doi = {10.1145/363235.363259},
acmid = {363259},
publisher = {ACM}
author = {C. A. R. Hoare},
title = {An Axiomatic Basis for Computer Programming},
journal = {Commun. ACM},
year = {1969},
volume = {12},
number = {10},
pages = {576-580},
month = {oct},
note = {\url{http://doi.acm.org/10.1145/363235.363259}},
_acmid = {363259},
_doi = {10.1145/363235.363259},
_issn = {0001-0782},
_issue_date = {Oct. 1969},
_numpages = {5},
_publisher = {ACM},
_url = {http://doi.acm.org/10.1145/363235.363259},
}
@article{2007-Blazy-C-chronique,
author = {Sandrine Blazy},
title = {Comment gagner confiance en {C} ?},
journal = {Technique et Science Informatiques},
year = {2007},
volume = {26},
number = {9},
pages = {1195-1200},
note = {\url{http://hal.inria.fr/inria-00292049/}},
hal = {http://hal.inria.fr/inria-00292049/},
pubkind = {journal-fr-mono}
author = {Sandrine Blazy},
title = {Comment gagner confiance en {C} ?},
journal = {Technique et Science Informatiques},
year = {2007},
volume = {26},
number = {9},
pages = {1195-1200},
note = {\url{http://hal.inria.fr/inria-00292049/}},
_hal = {http://hal.inria.fr/inria-00292049/},
_pubkind = {journal-fr-mono},
}
@inproceedings{2012-Appel,
author = {Andrew W. Appel},
title = {Verified Software Toolchain},
booktitle = {{NASA} Formal Methods - 4th International Symposium, {NFM} 2012, Norfolk,
VA, USA, April 3-5, 2012. Proceedings},
editor = {Alwyn Goodloe and Suzette Person},
publisher = SV,
series = LNCS,
volume = {7226},
year = {2012},
pages = {2},
url = {https://doi.org/10.1007/978-3-642-28891-3_2},
note = {\url{https://doi.org/10.1007/978-3-642-28891-3_2}},
doi = {10.1007/978-3-642-28891-3_2},
author = {Andrew W. Appel},
title = {Verified Software Toolchain},
booktitle = {{NASA} Formal Methods - 4th International Symposium, {NFM} 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings},
year = {2012},
editor = {Alwyn Goodloe and Suzette Person},
pages = {2},
publisher = SV, series = LNCS, volume = {7226},
note = {\url{https://doi.org/10.1007/978-3-642-28891-3_2}},
_doi = {10.1007/978-3-642-28891-3_2},
_url = {https://doi.org/10.1007/978-3-642-28891-3_2},
}
@article{2015-Appel,
author = {Andrew W. Appel},
title = {Verification of a Cryptographic Primitive: SHA-256},
journal = {ACM Trans. Program. Lang. Syst.},
issue_date = {April 2015},
volume = {37},
number = {2},
month = apr,
year = {2015},
issn = {0164-0925},
pages = {7:1--7:31},
articleno = {7},
numpages = {31},
url = {http://doi.acm.org/10.1145/2701415},
note = {\url{http://doi.acm.org/10.1145/2701415}},
doi = {10.1145/2701415},
acmid = {2701415},
publisher = {ACM},
author = {Andrew W. Appel},
title = {Verification of a Cryptographic Primitive: SHA-256},
journal = {ACM Trans. Program. Lang. Syst.},
year = {},
volume = {37},
number = {2},
pages = {7:1--7:31},
month = apr, year = {2015},
note = {\url{http://doi.acm.org/10.1145/2701415}},
_acmid = {2701415},
_articleno = {7},
_doi = {10.1145/2701415},
_issn = {0164-0925},
_issue_date = {April 2015},
_numpages = {31},
_publisher = {ACM},
_url = {http://doi.acm.org/10.1145/2701415},
}
@book{Abrial:1996:BAP:236705,
author = {Jean-Raymond Abrial},
title = {The B-book: Assigning Programs to Meanings},
year = {1996},
isbn = {0-521-49619-5},
publisher = {Cambridge University Press},
address = {New York, NY, USA},
author = {Jean-Raymond Abrial},
title = {The B-book: Assigning Programs to Meanings},
publisher = {Cambridge University Press},
year = {1996},
address = {New York, NY, USA},
_isbn = {0-521-49619-5},
}
@inproceedings{BGJ+15,
author = {Daniel J. Bernstein and
Bernard van Gastel and
Wesley Janssen and
Tanja Lange and
Peter Schwabe and
Sjaak Smetsers},
title = {{TweetNaCl}: A crypto library in 100 tweets},
booktitle = {Progress in Cryptology -- {LATINCRYPT 2014}},
year = {2015},
editor = {Diego Aranha and Alfred Menezes},
pages = {64--83},
publisher = SV, series = LNCS, volume = {8895},
note = {Document ID: c74b5bbf605ba02ad8d9e49f04aca9a2, \url{http://cryptojedi.org/papers/\#tweetnacl}},
}
@inproceedings{BLS12,
author = {Daniel J. Bernstein and
Tanja Lange and
Peter Schwabe},
title = {The security impact of a new cryptographic library},
booktitle = {Progress in Cryptology -- {LATINCRYPT 2012}},
year = {2012},
editor = {Alejandro Hevia and Gregory Neven},
pages = {159--176},
publisher = SV, series = LNCS, volume = {7533},
note = {Document ID: 5f6fc69cc5a319aecba43760c56fab04, \url{http://cryptojedi.org/papers/\#coolnacl}},
}
note = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=onepage&q&f=false}}
@inproceedings{Ber06,
author = {Daniel J. Bernstein},
title = {Curve25519: new {D}iffie-{H}ellman speed records},
booktitle = {Public Key Cryptography -- {PKC 2006}},
editor = {Moti Yung and Yevgeniy Dodis and Aggelos Kiayias and Tal Malkin},
publisher = SV,
series = LNCS,
volume = {3958},
year = {2006},
pages = {207--228},
note = {\url{http://cr.yp.to/papers.html\#curve25519}},
author = {Daniel J. Bernstein},
title = {Curve25519: new {D}iffie-{H}ellman speed records},
booktitle = {Public Key Cryptography -- {PKC 2006}},
year = {2006},
editor = {Moti Yung and Yevgeniy Dodis and Aggelos Kiayias and Tal Malkin},
pages = {207--228},
publisher = SV, series = LNCS, volume = {3958},
note = {\url{http://cr.yp.to/papers.html\#curve25519}},
}
@misc{Ber14,
title = {25519 naming, Posting to the CFRG mailing list},
author = {Daniel J. Bernstein},
year = {2008},
note = {\url{https://www.ietf.org/mail-archive/web/cfrg/current/msg04996.html}}
author = {Daniel J. Bernstein},
title = {25519 naming, Posting to the CFRG mailing list},
year = {2008},
note = {\url{https://www.ietf.org/mail-archive/web/cfrg/current/msg04996.html}},
}
@inproceedings{Beringer2015VerifiedCA,
title = {Verified Correctness and Security of OpenSSL HMAC},
author = {Lennart Beringer and Adam Petcher and Katherine Q. Ye and Andrew W. Appel},
booktitle = {USENIX Security Symposium},
year = {2015},
note = {\url{https://www.cs.cmu.edu/~kqy/resources/verified-hmac.pdf}}
}
@inproceedings{BGJ+15,
author = {Daniel J. Bernstein and Bernard van Gastel and Wesley Janssen and Tanja Lange and Peter Schwabe and Sjaak Smetsers},
title = {{TweetNaCl}: A crypto library in 100 tweets},
booktitle = {Progress in Cryptology -- {LATINCRYPT 2014}},
editor = {Diego Aranha and Alfred Menezes},
publisher = SV,
series = LNCS,
volume = {8895},
year = {2015},
pages = {64--83},
note = {Document ID: c74b5bbf605ba02ad8d9e49f04aca9a2, \url{http://cryptojedi.org/papers/\#tweetnacl}},
author = {Lennart Beringer and
Adam Petcher and
Katherine Q. Ye and
Andrew W. Appel},
title = {Verified Correctness and Security of OpenSSL HMAC},
booktitle = {USENIX Security Symposium},
year = {2015},
note = {\url{https://www.cs.cmu.edu/~kqy/resources/verified-hmac.pdf}},
}
@article{Blazy-Leroy-Clight-09,
author = {Sandrine Blazy and Xavier Leroy},
title = {Mechanized semantics for the {Clight}
subset of the {C} language},
year = {2009},
journal = {Journal of Automated Reasoning},
volume = {43},
number = {3},
pages = {263-288},
note = {\url{http://gallium.inria.fr/~xleroy/publi/Clight.pdf}},
hal = {http://hal.inria.fr/inria-00352524/},
urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9148-3}
}
@inproceedings{BLS12,
author = {Daniel J. Bernstein and Tanja Lange and Peter Schwabe},
title = {The security impact of a new cryptographic library},
booktitle = {Progress in Cryptology -- {LATINCRYPT 2012}},
editor = {Alejandro Hevia and Gregory Neven},
publisher = SV,
series = LNCS,
volume = {7533},
year = {2012},
pages = {159--176},
note = {Document ID: 5f6fc69cc5a319aecba43760c56fab04, \url{http://cryptojedi.org/papers/\#coolnacl}},
}
author = {Sandrine Blazy and
Xavier Leroy},
title = {Mechanized semantics for the {Clight} subset of the {C} language},
journal = {Journal of Automated Reasoning},
year = {2009},
@article{cao2018vst-floyd,
author = {Qinxiang Cao and Lennart Beringer and Samuel Gruetter and Josiah Dodds and Andrew W. Appel},
year = {2018},
title = {VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs},
journal = {Journal of Automated Reasoning},
issn = {0168-7433},
doi = {10.1007/s10817-018-9457-5},
volume = {61},
month = {6},
pages = {367--422},
number = {1-4},
url = {https://doi.org/10.1007/s10817-018-9457-5},
abstract = {The Verified Software Toolchain builds foundational machine-checked proofs of the functional correctness of C programs. Its program logic, Verifiable C, is a shallowly embedded higher-order separation Hoare logic which is proved sound in Coq with respect to the operational semantics of CompCert Clight. This paper introduces VST-Floyd, a verification assistant which offers a set of semiautomatic tactics helping users build functional correctness proofs for C programs using Verifiable C.}
volume = {43},
number = {3},
pages = {263-288},
note = {\url{http://gallium.inria.fr/~xleroy/publi/Clight.pdf}},
_hal = {http://hal.inria.fr/inria-00352524/},
_urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9148-3},
}
@inproceedings{Chen2014VerifyingCS,
title = {Verifying Curve25519 Software},
author = {Yu-Fang Chen and Chang-Hong Hsu and Hsin-Hung Lin and Peter Schwabe and Ming-Hsien Tsai and Bow-Yaw Wang and Bo-Yin Yang and Shang-Yi Yang},
booktitle = {ACM Conference on Computer and Communications Security},
year = {2014},
note = {\url{https://cryptojedi.org/papers/verify25519-20140428.pdf}}
}
@misc{coq-faq,
title = {{The Coq Proof Assistant} -- {Frequently Asked Questions}},
author = {},
note = {\url{https://coq.inria.fr/faq}},
}
author = {Yu-Fang Chen and
Chang-Hong Hsu and
Hsin-Hung Lin and
Peter Schwabe and
Ming-Hsien Tsai and
Bow-Yaw Wang and
Bo-Yin Yang and
Shang-Yi Yang},
title = {Verifying Curve25519 Software},
booktitle = {ACM Conference on Computer and Communications Security},
year = {2014},
@Article{CpdtJFR,
author = {Adam Chlipala},
title = {An Introduction to Programming and Proving with Dependent Types in Coq},
volume = {3(2)},
pages = {1-93},
year = {2010},
journal = {Journal of Formalized Reasoning},
url = {http://adam.chlipala.net/papers/CpdtJFR/},
note = {\url{http://adam.chlipala.net/papers/CpdtJFR/}}
note = {\url{https://cryptojedi.org/papers/verify25519-20140428.pdf}},
}
@misc{cryptoeprint:2011:646,
author = {Daniel J. Bernstein and Tanja Lange and Peter Schwabe},
title = {The security impact of a new cryptographic library},
howpublished = {Cryptology ePrint Archive, Report 2011/646},
year = {2011},
note = {\url{https://eprint.iacr.org/2011/646}},
@article{CpdtJFR,
author = {Adam Chlipala},
title = {An Introduction to Programming and Proving with Dependent Types in Coq},
journal = {Journal of Formalized Reasoning},
year = {2010},
volume = {3(2)},
pages = {1-93},
note = {\url{http://adam.chlipala.net/papers/CpdtJFR/}},
_url = {http://adam.chlipala.net/papers/CpdtJFR/},
}
@inproceedings{DBLP:conf/itp/BartziaS14,
author = {Evmorfia-Iro Bartzia and Pierre-Yves Strub},
title = {A Formal Library for Elliptic Curves in the Coq Proof Assistant},
booktitle = {Interactive Theorem Proving},
editor = {Gerwin Klein and Ruben Gamboa},
publisher = SV,
series = LNCS,
volume = {8558},
year = {2014},
pages = {77-92},
note = {\url{https://hal.inria.fr/hal-01102288}}
author = {Evmorfia-Iro Bartzia and
Pierre-Yves Strub},
title = {A Formal Library for Elliptic Curves in the Coq Proof Assistant},
booktitle = {Interactive Theorem Proving},
year = {2014},
editor = {Gerwin Klein and Ruben Gamboa},
pages = {77-92},
publisher = SV, series = LNCS, volume = {8558},
note = {\url{https://hal.inria.fr/hal-01102288}},
}
@article{DBLP:journals/corr/BhargavanDFHPRR17,
author = {Karthikeyan Bhargavan and
Antoine Delignat{-}Lavaud and
C{\'{e}}dric Fournet and
Catalin Hritcu and
Jonathan Protzenko and
Tahina Ramananandro and
Aseem Rastogi and
Nikhil Swamy and
Peng Wang and
Santiago Zanella B{\'{e}}guelin and
Jean Karim Zinzindohou{\'{e}}},
title = {Verified Low-Level Programming Embedded in {F}},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
pages = {17},
year = {2017},
publisher = {ACM},
url = {http://arxiv.org/abs/1703.00053},
note = {\url{http://arxiv.org/abs/1703.00053}},
eprint = {1703.00053},
timestamp = {Mon, 13 Aug 2018 16:46:57 +0200},
author = {Karthikeyan Bhargavan and
Antoine Delignat{-}Lavaud and
C{\'{e}}dric Fournet and
Catalin Hritcu and
Jonathan Protzenko and
Tahina Ramananandro and
Aseem Rastogi and
Nikhil Swamy and
Peng Wang and
Santiago Zanella B{\'{e}}guelin and
Jean Karim Zinzindohou{\'{e}}},
title = {Verified Low-Level Programming Embedded in {F}},
journal = {Proceedings of the ACM on Programming Languages},
year = {2017},
volume = {1},
number = {ICFP},
pages = {17},
note = {\url{http://arxiv.org/abs/1703.00053}},
_eprint = {1703.00053},
_publisher = {ACM},
_timestamp = {Mon, 13 Aug 2018 16:46:57 +0200},
_url = {http://arxiv.org/abs/1703.00053},
}
@inproceedings{Erbsen2016SystematicSO,
title = {Systematic Synthesis of Elliptic Curve Cryptography Implementations},
author = {Andres Erbsen and Jason Gross and Adam Chlipala},
year = {2016},
note = {\url{https://people.csail.mit.edu/jgross/personal-website/papers/2017-fiat-crypto-pldi-draft.pdf}}
author = {Andres Erbsen and
Jason Gross and
Adam Chlipala},
title = {Systematic Synthesis of Elliptic Curve Cryptography Implementations},
booktitle = {},
year = {2016},
note = {\url{https://people.csail.mit.edu/jgross/personal-website/papers/2017-fiat-crypto-pldi-draft.pdf}},
}
@inproceedings{Erbsen2017CraftingCE,
title = {Crafting certified elliptic curve cryptography implementations in Coq},
author = {Andres Erbsen},
year = {2017},
note = {\url{http://adam.chlipala.net/theses/andreser_meng.pdf}}
}
@inproceedings{fiat-crypto,
title = {Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises},
author = {Andres Erbsen and Jade Philipoom and Jason Gross and Robert Sloan and Adam Chlipala},
booktitle = {Proceedings of the \href{https://www.ieee-security.org/TC/SP2019/}{40th IEEE Symposium on Security and Privacy (S\&P'19)}},
year = {2019},
month = {May},
code-github = {https://github.com/mit-plv/fiat-crypto},
owner = {jgross},
timestamp = {2018.06.01},
url = {https://people.csail.mit.edu/jgross/personal-website/papers/2019-fiat-crypto-ieee-sp.pdf},
note = {\url{https://people.csail.mit.edu/jgross/personal-website/papers/2019-fiat-crypto-ieee-sp.pdf}}
}
author = {Andres Erbsen},
title = {Crafting certified elliptic curve cryptography implementations in Coq},
booktitle = {},
year = {2017},
@article{gonthier2008formal,
title = {Formal proof--the four-color theorem},
author = {Georges Gonthier},
journal = {Notices of the AMS},
volume = {55},
number = {11},
pages = {1382--1393},
year = {2008},
note = {\url{https://www.ams.org/notices/200811/tx081101382p.pdf}}
note = {\url{http://adam.chlipala.net/theses/andreser_meng.pdf}},
}
@incollection{Howard1995-HOWTFN,
title = {The Formul\ae-as-Types Notion of Construction},
author = {W. A. Howard},
booktitle = {The Curry-Howard Isomorphism},
year = {1995},
editor = {Philippe De Groote},
publisher = {Academia},
note = {\url{https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf}}
author = {W. A. Howard},
title = {The Formul\ae-as-Types Notion of Construction},
booktitle = {The Curry-Howard Isomorphism},
publisher = {Academia},
year = {1995},
editor = {Philippe De Groote},
note = {\url{https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf}},
}
@techreport{ISO:C99,
title = {ISO C Standard 1999},
author = {ISO},
editor = {WG14},
note = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1124.pdf}},
year = {1999}
author = {ISO},
title = {ISO C Standard 1999},
institution = {},
year = {1999},
note = {\url{http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1124.pdf}},
_editor = {WG14},
}
@article{Leroy-backend,
author = {Xavier Leroy},
title = {A formally verified compiler back-end},
journal = {Journal of Automated Reasoning},
volume = {43},
number = {4},
pages = {363--446},
year = {2009},
note = {\url{http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf}},
urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9155-4},
hal = {http://hal.inria.fr/inria-00360768/},
pubkind = {journal-int-mono}
author = {Xavier Leroy},
title = {A formally verified compiler back-end},
journal = {Journal of Automated Reasoning},
year = {2009},
volume = {43},
number = {4},
pages = {363--446},
note = {\url{http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf}},
_hal = {http://hal.inria.fr/inria-00360768/},
_pubkind = {journal-int-mono},
_urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9155-4},
}
@article{Mon85,
author = {Peter L. Montgomery},
title = {Modular Multiplication Without Trial Division},
journal = {Mathematics of Computation},
publisher = {American Mathematical Society},
year = {1985},
volume = {44},
number = {170},
pages = {519--521},
note = {\url{http://www.ams.org/journals/mcom/1985-44-170/S0025-5718-1985-0777282-X/S0025-5718-1985-0777282-X.pdf}},
author = {Peter L. Montgomery},
title = {Modular Multiplication Without Trial Division},
journal = {Mathematics of Computation},
year = {1985},
volume = {44},
number = {170},
pages = {519--521},
note = {\url{http://www.ams.org/journals/mcom/1985-44-170/S0025-5718-1985-0777282-X/S0025-5718-1985-0777282-X.pdf}},
_publisher = {American Mathematical Society},
}
@article{MontgomerySpeeding,
author = {Peter L. Montgomery},
title = {Speeding the Pollard and Elliptic Curve Methods of Factorization. Math. Comp. 48, 243-264},
month = {01},
volume = {48},
year = {1987},
pages = {243-243},
journal = {Mathematics of Computation - Math. Comput.},
doi = {10.1090/S0025-5718-1987-0866113-7},
note = {\url{http://links.jstor.org/sici?sici=0025-5718(198701)48:177<243:STPAEC>2.0.CO;2-3}}
author = {Peter L. Montgomery},
title = {Speeding the Pollard and Elliptic Curve Methods of Factorization. Math. Comp. 48, 243-264},
journal = {Mathematics of Computation - Math. Comput.},
year = {1987},
volume = {48},
pages = {243-243},
month = {01},
note = {\url{http://links.jstor.org/sici?sici=0025-5718(198701)48:177<243:STPAEC>2.0.CO;2-3}},
_doi = {10.1090/S0025-5718-1987-0866113-7},
}
@inproceedings{Philipoom2018CorrectbyconstructionFF,
title = {Correct-by-construction finite field arithmetic in Coq},
author = {Jade Philipoom},
year = {2018},
note = {\url{http://adam.chlipala.net/theses/jadep_meng.pdf}}
author = {Jade Philipoom},
title = {Correct-by-construction finite field arithmetic in Coq},
booktitle = {},
year = {2018},
note = {\url{http://adam.chlipala.net/theses/jadep_meng.pdf}},
}
@article{Reynolds02separationlogic,
author = {John C. Reynolds},
title = {Separation Logic: A Logic for Shared Mutable Data Structures},
journal = {LICS},
volume = {17},
year = {2002},
pages = {55-74},