bcp.bib

@preamble{{\newcommand{\SortNoop}[1]{}}}
@inproceedings{MysteriesOfDropbox2016,
  author = {John Hughes and Benjamin C. Pierce and Thomas Arts 
                  and Ulf Norell},
  title = {Mysteries of {D}ropbox: {P}roperty-Based Testing 
                  of a Distributed 
                  Synchronization Service},
  year = 2016,
  booktitle = {International Conference on Software Testing, 
                  Verification and Validation (ICST)},
  month = apr,
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/ICST-2015-mysteries.pdf},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/mysteriesofdropbox.pdf}
}
@misc{Pierce:ChalmersDeepspecTalk,
  author = {Benjamin C. Pierce},
  title = {The Age of Deep Specification},
  note = {Honorary doctorate address at Chalmers University},
  year = 2015,
  month = may,
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/chalmers-deepspec-2015.pdf}
}
@inproceedings{TestingNI:ICFP,
  author = {C\u{a}t\u{a}lin Hri\c{t}cu and
                  John Hughes and
                  Benjamin C. Pierce and
                  Antal Spector-Zabusky and
                  Dimitrios Vytiniotis and
                  Arthur Azevedo de Amorim and
                  Leonidas Lampropoulos},
  title = {Testing Noninterference, Quickly},
  booktitle = {18th ACM SIGPLAN International
                  Conference on Functional Programming (ICFP)},
  shortbooktitle = {ICFP},
  year = {2013},
  month = sep,
  url = {http://www.crash-safe.org/node/24},
  bcp = {yes},
  plclub = {yes},
  keys = {verification,security},
  note = {Full version in Journal of Functional Programming, special issue for ICFP 2013, 26:e4 (62 pages), April 2016. Technical Report available as arXiv:1409.0393.}
}
@misc{Pierce:SPLASHTalk2016,
  author = {Benjamin C. Pierce},
  title = {The Science of Deep Specification},
  month = nov,
  year = 2016,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/deepspec-splash2016.pdf},
  note = {Invited keynote at {\em SPLASH / OOPSLA}},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/deepspec-splash2016.pdf},
  video = {https://www.youtube.com/watch?v=IPNdsnRWBkk&t=5s},
  keys = {verification}
}
@inproceedings{Denes:VSL2014,
  author = {Maxime D\'en\`es and Catalin Hritcu and Leonidas Lampropoulos and Zoe Paraskevopoulou and Benjamin C. Pierce},
  title = {{QuickChick}: {P}roperty-Based Testing for {C}oq (abstract)},
  booktitle = {VSL},
  url = {http://www.easychair.org/smart-program/VSL2014/index.html},
  year = 2014,
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification}
}
@inproceedings{Paraskevopoulou:ITP2015,
  author = {Zoe Paraskevopoulou and
                  C\u{a}t\u{a}lin Hri\c{t}cu and
                  Maxime D\'en\`es and
                  Leonidas Lampropoulos and
                  Benjamin C. Pierce},
  title = {Foundational Property-Based Testing},
  booktitle = {International Conference 
                  on Interactive Theorem Proving (ITP)},
  year = 2015,
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification}
}
@misc{Pierce:DeepSpecHCSS2016,
  author = {Benjamin C. Pierce},
  title = {The Science of Deep Specification},
  month = may,
  year = 2016,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/deepspec-hcss2016-slides.pdf},
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification},
  note = {High-Confidence Software Systems (HCSS)}
}
@inproceedings{beginners-luck,
  author = {Leonidas Lampropoulos and
                  Diane Gallois-Wong and
                  C\u{a}t\u{a}lin Hri\c{t}cu and
                  John Hughes and
                  Benjamin C. Pierce and
                  {Li-yao} Xia},
  title = {Beginner's {Luck}: A Language for Random Generators},
  booktitle = {44th ACM SIGPLAN Symposium on Principles of Programming
                  Languages (POPL)},
  year = {2017},
  month = jan,
  url = {https://arxiv.org/abs/1607.05443},
  acceptance = {64/279=0.23},
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification}
}
@misc{beginners-luck-old,
  author = {Leonidas Lampropoulos and
                  Diane Gallois-Wong and
                  C\u{a}t\u{a}lin Hri\c{t}cu and
                  John Hughes and
                  Benjamin C. Pierce and
                  {Li-yao} Xia},
  title = {Beginner's Luck: A Language for Random Generators},
  url = {https://arxiv.org/abs/1607.05443},
  year = {2016},
  month = jul,
  howpublished = {Draft, arXiv:1607.05443},
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification}
}
@misc{AzevedoDeAmorim17,
  author = {Arthur {Azevedo de Amorim} and
                  C\u{a}t\u{a}lin Hri\c{t}cu and
                  Benjamin C. Pierce},
  title = {The Meaning of Memory Safety},
  howpublished = {arXiv:1705.07354},
  url = {https://arxiv.org/abs/1705.07354},
  year = {2017},
  month = may,
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification}
}
@inproceedings{AzevedoDeAmorim17old,
  author = {Arthur Azevedo de Amorim and
                  C\u{a}t\u{a}lin Hri\c{t}cu and
                  Benjamin C. Pierce},
  title = {The Meaning of Memory Safety},
  booktitle = {ACM Conference on Computer and Communications Security (CCS)},
  year = 2017,
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification},
  note = {Under submission}
}
@misc{Pierce:ReleaseInterview,
  author = {Benjamin C. Pierce},
  title = {{Interview with Tijs van der Storm on The Science of Deep Specification for release.nl magazine}},
  month = nov,
  year = 2016,
  transcript = {http://release.nl/293/video.html?video=775966},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security,verification}
}
@misc{Pierce:OmegaTauInterview,
  author = {Benjamin C. Pierce},
  title = {{Interview with Markus V\"olter on The Science of Deep Specification for Omega Tau podcast}},
  month = nov,
  year = 2016,
  transcript = {http://omegataupodcast.net/243-formal-specification-and-proof/},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security,verification}
}
@misc{Pierce:NSFtalk2017,
  author = {Benjamin C. Pierce},
  title = {The Science of Deep Specification},
  month = sep,
  year = 2017,
  note = {WATCH lecture at NSF},
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification}
}
@article{Appel20160331,
  author = {Appel, Andrew W. and Beringer, Lennart and Chlipala, Adam and Pierce, Benjamin C. and Shao, Zhong and Weirich, Stephanie and Zdancewic, Steve},
  title = {Position paper: the science of deep specification},
  volume = {375},
  number = {2104},
  year = {2017},
  doi = {10.1098/rsta.2016.0331},
  publisher = {The Royal Society},
  abstract = {We introduce our efforts within the project
                  {\textquoteleft}The science of deep
                  specification{\textquoteright} to work out the key
                  formal underpinnings of industrial-scale formal
                  specifications of software and hardware components,
                  anticipating a world where large verified systems
                  are routinely built out of smaller verified
                  components that are also used by many other
                  projects. We identify an important class of
                  specification that has already been used in a few
                  experiments that connect strong
                  component-correctness theorems across the work of
                  different teams. To help popularize the unique
                  advantages of that style, we dub it deep
                  specification, and we say that it encompasses
                  specifications that are rich, two-sided, formal and
                  live (terms that we define in the article). Our core
                  team is developing a proof-of-concept system (based
                  on the Coq proof assistant) whose specification and
                  verification work is divided across largely
                  decoupled subteams at our four institutions,
                  encompassing hardware microarchitecture, compilers,
                  operating systems and applications, along with
                  cross-cutting principles and tools for effective
                  specification. We also aim to catalyse interest in
                  the approach, not just by basic researchers but also
                  by users in industry. This article is part of the
                  themed issue {\textquoteleft}Verified trustworthy
                  software systems{\textquoteright}.},
  issn = {1364-503X},
  url = {http://rsta.royalsocietypublishing.org/content/375/2104/20160331},
  eprint = {http://rsta.royalsocietypublishing.org/content/375/2104/20160331.full.pdf},
  journal = {Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security,verification}
}