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:LambdaTA,
author = {Benjamin C. Pierce},
title = {Lambda, The Ultimate {TA}: {U}sing a Proof Assistant to Teach
Programming Language Foundations},
note = {Keynote address at {\em International Conference on
Functional Programming (ICFP)}},
year = 2009,
plclub = {Yes},
month = sep,
bcp = {Yes},
keys = {verification},
slides = {http://www.cis.upenn.edu/~bcpierce/papers/LambdaTA.pdf}
}
@misc{Pierce:LambdaTA-ITP,
author = {Benjamin C. Pierce},
title = {Proof Assistant
as Teaching Assistant: A View from the Trenches},
note = {Keynote address at {\em International Conference
on Interactive Theorem Proving (ITP)}},
year = 2010,
plclub = {Yes},
month = jul,
bcp = {Yes},
keys = {verification},
slides = {http://www.cis.upenn.edu/~bcpierce/papers/LambdaTA-ITP.pdf}
}
@inproceedings{poplmark,
author = {Brian E. Aydemir and Aaron Bohannon and Matthew Fairbairn
and J. Nathan Foster and Benjamin C. Pierce and Peter
Sewell and Dimitrios Vytiniotis and Geoffrey Washburn and
Stephanie Weirich and Steve Zdancewic},
title = {Mechanized metatheory for the masses: {T}he {POPLmark}
Challenge},
booktitle = {International Conference on Theorem Proving in
Higher Order Logics (TPHOLs)},
year = 2005,
month = {August},
ps = {http://www.cis.upenn.edu/~geoffw/research/papers/poplmark.ps},
psgz = {http://www.cis.upenn.edu/~geoffw/research/papers/poplmark.ps.gz},
pdf = {http://www.cis.upenn.edu/~geoffw/research/papers/poplmark.pdf},
plclub = {Yes},
bcp = {Yes},
keys = {verification},
abstract = {How close are we to a world where every paper on
programming languages is accompanied by an electronic
appendix with machine-checked proofs?
We propose a concrete set of benchmarks for measuring
progress in this area. Based on the metatheory of System
F-sub, a typed lambda-calculus with second-order
polymorphism, subtyping, and records, these benchmarks
embody many aspects of programming languages that are
challenging to formalize: variable binding at both the term
and type levels, syntactic forms with variable numbers of
components (including binders), and proofs demanding
complex induction principles. We hope that these benchmarks
will help clarify the current state of the art, provide a
basis for comparing competing technologies, and motivate
further research.}
}
@inproceedings{Aydemir08,
author = {Brian Aydemir and Arthur Chargu\'{e}raud and Benjamin C. Pierce and Randy Pollack and Stephanie Weirich},
title = {Engineering formal metatheory},
pages = {3--15},
publisher = {ACM},
booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL}), San Francisco, California},
year = {2008},
month = jan,
bcp = {Yes},
keys = {verification},
plclub = {Yes},
short = {http://www.cis.upenn.edu/~bcpierce/papers/binders.pdf}
}
@misc{Aydemir07a:old,
author = {Brian Aydemir and Arthur Chargu{{\'e}}raud and Benjamin C. Pierce
and Randy Pollack and Stephanie Weirich},
title = {Engineering Formal Metatheory},
year = {2007},
month = jul,
keys = {verification},
note = {Submitted for publication},
short = {http://www.cis.upenn.edu/~bcpierce/papers/binders.pdf}
}
@misc{Pierce08LambdaTA,
author = {Benjamin C. Pierce},
title = {Using a Proof Assistant to Teach Programming Language Foundations, or,
{L}ambda, the Ultimate {TA}},
year = {2008},
month = apr,
bcp = {Yes},
keys = {verification},
plclub = {Yes},
note = {White paper},
short = {http://www.cis.upenn.edu/~bcpierce/papers/plcurriculum.pdf}
}
@book{Pierce:SFold,
author = {Benjamin C. Pierce and Arthur {Azevedo de Amorim}
and Chris Casinghino and Marco Gaboardi and
Michael Greenberg and C\v{a}t\v{a}lin Hri\c{t}cu
and Vilhelm Sj\"{o}berg and Brent Yorgey},
title = {Software Foundations},
year = {2017},
publisher = {Electronic textbook},
plclub = {Yes},
bcp = {Yes},
keys = {verification,books},
note = {Version 5.0. \URL{http://www.cis.upenn.edu/~bcpierce/sf}},
ebook = {http://www.cis.upenn.edu/~bcpierce/sf},
japanese = {http://proofcafe.org/sf}
}
@book{Pierce:SF1,
author = {Benjamin C. Pierce and Arthur {Azevedo de Amorim}
and Chris Casinghino and Marco Gaboardi and
Michael Greenberg and C\v{a}t\v{a}lin Hri\c{t}cu
and Vilhelm Sj\"{o}berg and Brent Yorgey},
title = {Logical Foundations},
series = {Software Foundations series, volume 1},
month = may,
year = {2018},
publisher = {Electronic textbook},
plclub = {Yes},
bcp = {Yes},
keys = {verification,books},
note = {Version 5.5. \URL{http://www.cis.upenn.edu/~bcpierce/sf}},
ebook = {http://www.cis.upenn.edu/~bcpierce/sf},
japanese = {http://proofcafe.org/sf}
}
@book{Pierce:SF2,
author = {Benjamin C. Pierce and Arthur {Azevedo de Amorim}
and Chris Casinghino and Marco Gaboardi and
Michael Greenberg and C\v{a}t\v{a}lin Hri\c{t}cu
and Vilhelm Sj\"{o}berg and Andrew Tolmach
and Brent Yorgey},
title = {Programming Language Foundations},
series = {Software Foundations series, volume 2},
month = may,
year = {2018},
publisher = {Electronic textbook},
plclub = {Yes},
bcp = {Yes},
keys = {verification,books},
note = {Version 5.5. \URL{http://www.cis.upenn.edu/~bcpierce/sf}},
ebook = {http://www.cis.upenn.edu/~bcpierce/sf},
japanese = {http://proofcafe.org/sf}
}
@book{Pierce:SF4,
author = {Leonidas Lampropoulos and Benjamin C. Pierce},
title = {{QuickChick}: Property-Based Testing in Coq},
series = {Software Foundations series, volume 4},
month = aug,
year = {2018},
publisher = {Electronic textbook},
plclub = {Yes},
bcp = {Yes},
keys = {verification,books},
note = {\URL{http://www.cis.upenn.edu/~bcpierce/sf}},
ebook = {http://www.cis.upenn.edu/~bcpierce/sf}
}
@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,
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}
}
@misc{Pierce:ETAPSTalk2018,
author = {Benjamin C. Pierce},
title = {The Science of Deep Specification},
month = apr,
year = 2018,
slides = {http://www.cis.upenn.edu/~bcpierce/papers/pierce-etaps2018.pdf},
note = {Invited keynote at {\em ETAPS / POST}},
plclub = {Yes},
bcp = {Yes},
video = {https://www.etaps.org/index.php/2018/invited-speakers},
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)}
}
@incollection{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 = {Foundations of Programming and Software systems: Probabilistic Programming},
editor = {Gilles Barthe and Joost-Pieter Katoen and Alexandra Silva},
year = {2020},
url = {https://arxiv.org/abs/1607.05443},
plclub = {Yes},
bcp = {Yes},
keys = {verification},
note = {An earlier version appeared in ACM SIGPLAN Symposium on Principles of Programming
Languages (POPL), Jan 2017}
}
@inproceedings{beginners-luck:popl,
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},
keys = {verification}
}
@inproceedings{AzevedoDeAmorim17,
author = {Arthur Azevedo de Amorim and
Catalin Hritcu and
Benjamin C. Pierce},
editor = {Lujo Bauer and
Ralf K{\"{u}}sters},
title = {The Meaning of Memory Safety},
booktitle = {Principles of Security and Trust - 7th International Conference, {POST}
2018, Held as Part of the European Joint Conferences on Theory and
Practice of Software, {ETAPS} 2018, Thessaloniki, Greece, April 14-20,
2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10804},
pages = {79--105},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-89722-6\_4},
doi = {10.1007/978-3-319-89722-6\_4},
timestamp = {Fri, 31 Jan 2020 21:32:30 +0100},
biburl = {https://dblp.org/rec/conf/post/AmorimHP18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
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}
}
@misc{Pierce:DeepWeb-dsw2018,
author = {Benjamin C. Pierce},
title = {Specifying the {DeepSpec Web Server}},
month = jun,
year = 2018,
note = {Talk at {\it DeepSpec} workshop},
plclub = {Yes},
bcp = {Yes},
slides = {http://www.cis.upenn.edu/~bcpierce/papers/DeepWeb-dsw2018.pdf},
keys = {verification}
}
@misc{Pierce:DeepWeb-dsw2019,
author = {Benjamin C. Pierce},
title = {The Science of Deep Specification},
month = jun,
year = 2019,
note = {Opening talk at {\it DeepSpec} workshop},
plclub = {Yes},
bcp = {Yes},
slides = {http://www.cis.upenn.edu/~bcpierce/papers/DeepSpec-workshop-2019-Intro.pdf},
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: {T}he 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}
}
@article{Lampropoulos&18,
author = {Leonidas Lampropoulos and
Zoe Paraskevopoulou and
Benjamin C. Pierce},
title = {Generating good generators for inductive relations},
journal = {{PACMPL}},
volume = {2},
number = {{POPL}},
pages = {45:1--45:30},
year = {2018},
url = {http://doi.acm.org/10.1145/3158133},
doi = {10.1145/3158133},
timestamp = {Fri, 05 Jan 2018 12:57:30 +0100},
biburl = {https://dblp.org/rec/bib/journals/pacmpl/LampropoulosPP18},
bibsource = {dblp computer science bibliography, https://dblp.org},
plclub = {Yes},
bcp = {Yes},
short = {http://www.cis.upenn.edu/~bcpierce/papers/generating-good.pdf},
keys = {verification}
}
@article{DBLP:journals/pacmpl/Lampropoulos0P19,
author = {Leonidas Lampropoulos and
Michael Hicks and
Benjamin C. Pierce},
title = {Coverage guided, property based testing},
journal = {Proc. {ACM} Program. Lang.},
volume = {3},
number = {{OOPSLA}},
pages = {181:1--181:29},
year = {2019},
url = {https://doi.org/10.1145/3360607},
doi = {10.1145/3360607},
timestamp = {Thu, 16 Apr 2020 13:51:47 +0200},
biburl = {https://dblp.org/rec/journals/pacmpl/Lampropoulos0P19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
bcp = {Yes},
plclub = {Yes},
keys = {verification}
}
@misc{Pierce:POPLMarkRetrospective2020,
author = {Benjamin C. Pierce},
title = {POPLmark 15 Year Retrospective Panel at {\em
Certified Programs and Proofs}},
year = 2020,
url = {https://www.youtube.com/watch?v=2M2ZWNzpzkE},
bcp = {Yes},
plclub = {Yes},
keys = {verification},
note = {Written up in
\URL{https://blog.sigplan.org/2020/01/29/mechanized-proofs-for-pl-past-present-and-future/}}
}
@article{Lehsani2022:newer,
title = {Modular Mechanized Verification of Transactional Predication},
author = {Mohsen Lesani and {Li-Yao} Xia and Anders Kaseorg and
Christian J. Bell and
Adam Chlipala and Benjamin C. Pierce and Steve Zdancewic},
journal = {Proc. {ACM} Program. Lang.},
volume = {6},
number = {{OOPSLA1}},
month = apr,
year = {2022},
bcp = {Yes},
plclub = {Yes},
keys = {verification},
note = {OOPSLA 2022},
pdef = {http://www.cis.upenn.edu/~bcpierce/papers/oopsla22main-p66-p-3e39fed5de-56232-final.pdf}
}
@article{10.1145/3527324,
author = {Lesani, Mohsen and Xia, Li-Yao and Kaseorg, Anders and Bell, Christian J. and Chlipala, Adam and Pierce, Benjamin C. and Zdancewic, Steve},
title = {C4: Verified Transactional Objects},
year = {2022},
issue_date = {April 2022},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {6},
number = {OOPSLA1},
url = {https://doi.org/10.1145/3527324},
doi = {10.1145/3527324},
abstract = {Transactional objects combine the performance of classical concurrent objects with the high-level programmability of transactional memory. However, verifying the correctness of transactional objects is tricky, requiring reasoning simultaneously about classical concurrent objects, which guarantee the atomicity of individual methods—the property known as linearizability—and about software-transactional-memory libraries, which guarantee the atomicity of user-defined sequences of method calls—or serializability. We present a formal-verification framework called C4, built up from the familiar notion of linearizability and its compositional properties, that allows proof of both kinds of libraries, along with composition of theorems from both styles to prove correctness of applications or further libraries. We apply the framework in a significant case study, verifying a transactional set object built out of both classical and transactional components following the technique of transactional predication; the proof is modular, reasoning separately about the transactional and nontransactional parts of the implementation. Central to our approach is the use of syntactic transformers on interaction trees—i.e., transactional libraries that transform client code to enforce particular synchronization disciplines. Our framework and case studies are mechanized in Coq.},
journal = {Proc. ACM Program. Lang.},
month = {apr},
articleno = {80},
numpages = {31},
keywords = {objects, serializability, concurrency, verification, linearizability},
bcp = {Yes},
plclub = {Yes},
keys = {verification}
}
@article{DBLP:journals/pacmpl/XiaZHHMPZ20,
author = {Li{-}yao Xia and
Yannick Zakowski and
Paul He and
Chung{-}Kil Hur and
Gregory Malecha and
Benjamin C. Pierce and
Steve Zdancewic},
title = {Interaction trees: representing recursive and impure programs in Coq},
journal = {Proc. {ACM} Program. Lang.},
volume = {4},
number = {{POPL}},
pages = {51:1--51:32},
year = {2020},
url = {https://doi.org/10.1145/3371119},
doi = {10.1145/3371119},
timestamp = {Thu, 16 Apr 2020 13:51:44 +0200},
biburl = {https://dblp.org/rec/journals/pacmpl/XiaZHHMPZ20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
note = {Distinguished paper award},
bcp = {Yes},
plclub = {Yes},
keys = {verification}
}
@inproceedings{Li2021:MBToNA,
author = {Yishuai Li and
Benjamin C. Pierce and
Steve Zdancewic},
editor = {Cristian Cadar and
Xiangyu Zhang},
title = {Model-based testing of networked applications},
booktitle = {{ISSTA} '21: 30th {ACM} {SIGSOFT} International Symposium on Software
Testing and Analysis, Virtual Event, Denmark, July 11-17, 2021},
pages = {529--539},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3460319.3464798},
doi = {10.1145/3460319.3464798},
timestamp = {Sat, 08 Jan 2022 02:24:32 +0100},
biburl = {https://dblp.org/rec/conf/issta/LiPZ21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
bcp = {Yes},
plclub = {Yes},
keys = {verification}
}
@inproceedings{DBLP:conf/esop/GoldsteinHLP21,
author = {Harrison Goldstein and
John Hughes and
Leonidas Lampropoulos and
Benjamin C. Pierce},
editor = {Nobuko Yoshida},
title = {Do Judge a Test by its Cover: Combining Combinatorial
and Property-Based Testing},
booktitle = {Programming Languages and Systems, 30th European Symposium on Programming,
{ESOP} 2021, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2021, Luxembourg City, Luxembourg,
March 27 - April 1, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12648},
pages = {264--291},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-72019-3\_10},
doi = {10.1007/978-3-030-72019-3\_10},
timestamp = {Wed, 07 Apr 2021 16:01:48 +0200},
biburl = {https://dblp.org/rec/conf/esop/GoldsteinHLP21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
bcp = {Yes},
plclub = {Yes},
keys = {misc,verification}
}
@inproceedings{Anderson2021stack,
author = {Sean Noble Anderson and
Leonidas Lampropoulos and
Roberto Blanco and
Benjamin C. Pierce and
Andrew Tolmach},
title = {Security Properties for Stack Safety},
year = {2021},
booktitle = {Workshop on Foundations of Computer Security (FCS)},
bcp = {Yes},
plclub = {Yes},
keys = {misc,verification}
}
@article{Anderson2021stack:old2,
author = {Sean Noble Anderson and
Leonidas Lampropoulos and
Roberto Blanco and
Benjamin C. Pierce and
Andrew Tolmach},
title = {Security Properties for Stack Safety},
journal = {CoRR},
volume = {abs/2105.00417},
year = {2021},
url = {https://arxiv.org/abs/2105.00417},
eprinttype = {arXiv},
eprint = {2105.00417},
timestamp = {Wed, 12 May 2021 15:54:31 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2105-00417.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
bcp = {Yes},
plclub = {Yes},
keys = {misc,verification}
}
@article{DBLP:journals/corr/abs-2203-00652,
author = {Harrison Goldstein and
Benjamin C. Pierce},
title = {Parsing Randomness: Unifying and Differentiating Parsers and Random
Generators},
journal = {CoRR},
volume = {abs/2203.00652},
year = {2022},
url = {https://doi.org/10.48550/arXiv.2203.00652},
doi = {10.48550/arXiv.2203.00652},
eprinttype = {arXiv},
eprint = {2203.00652},
timestamp = {Wed, 16 Mar 2022 16:39:52 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2203-00652.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
bcp = {Yes},
plclub = {Yes},
keys = {verification}
}
@inproceedings{DBLP:conf/itp/ZhangHK0LXBMPZ21,
author = {Hengchu Zhang and
Wolf Honor{\'{e}} and
Nicolas Koh and
Yao Li and
Yishuai Li and
Li{-}yao Xia and
Lennart Beringer and
William Mansky and
Benjamin C. Pierce and
Steve Zdancewic},
editor = {Liron Cohen and
Cezary Kaliszyk},
title = {Verifying an {HTTP} Key-Value Server with Interaction Trees and {VST}},
booktitle = {12th International Conference on Interactive Theorem Proving, {ITP}
2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
series = {LIPIcs},
volume = {193},
pages = {32:1--32:19},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2021},
url = {https://doi.org/10.4230/LIPIcs.ITP.2021.32},
doi = {10.4230/LIPIcs.ITP.2021.32},
timestamp = {Sat, 09 Apr 2022 12:45:06 +0200},
biburl = {https://dblp.org/rec/conf/itp/ZhangHK0LXBMPZ21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org},
bcp = {Yes},
plclub = {Yes},
keys = {verification}
}
@misc{Holey2022,
author = {Joseph Cutler and Harrison Goldstein and Koen Claessen
and John Hughes and Benjamin C. Pierce },
title = {Functional Pearl: Holey Generators!},
year = 2022,
month = may,
note = {Draft},
bcp = {Yes},
plclub = {Yes},
keys = {verification}
}
@misc{Frohlich2023old,
author = {Harrison Goldstein and Samantha Frohlich and
Benjamin C. Pierce and Meng Wang},
title = {Reflecting on Random Generation},
year = 2023,
month = feb,
note = {Under submission},
bcp = {Yes},
plclub = {Yes},
keys = {verification}
}
@article{goldstein2023reflecting,
title = {Reflecting on Random Generation},
author = {Goldstein, Harrison and Frohlich, Samantha and
Wang, Meng and Pierce, Benjamin C},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
pages = {322--355},
year = {2023},
bcp = {Yes},
plclub = {Yes},
keys = {verification},
publisher = {ACM New York, NY, USA}
}
@misc{GoldsteinChoices2022,
author = {Harrison Goldstein and
Benjamin C. Pierce},
title = {Making Better Choices: {G}uiding Random Generators with Derivatives},
year = 2022,
note = {Draft},
bcp = {Yes},
plclub = {Yes},
keys = {verification}
}
@misc{Pierce:Yow22,
author = {Benjamin C. Pierce},
title = {({W}hen) Will Property-Based Testing Rule The World?},
month = may,
year = 2022,
note = {Keynote at {\it Yow! Lambda Jam} Conference},
plclub = {Yes},
bcp = {Yes},
slides = {http://www.cis.upenn.edu/~bcpierce/papers/Yow2022-Pierce.pdf},
keys = {verification}
}
@misc{Pierce:2.8:2022,
author = {Benjamin C. Pierce},
title = {Understanding Property-Based Testing by Talking to People},
month = may,
year = 2022,
note = {Short talk at {\it Working Group 2.8}},
plclub = {Yes},
bcp = {Yes},
slides = {http://www.cis.upenn.edu/~bcpierce/papers/Pierce-WG2.8-2022.pdf},
keys = {verification}
}
@article{10.1145/3527324-duplicate,
author = {Lesani, Mohsen and Xia, Li-yao and Kaseorg, Anders and Bell, Christian J. and Chlipala, Adam and Pierce, Benjamin C. and Zdancewic, Steve},
title = {C4: Verified Transactional Objects},
year = {2022},
issue_date = {April 2022},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {6},
number = {OOPSLA1},
url = {https://doi.org/10.1145/3527324},
doi = {10.1145/3527324},
abstract = {Transactional objects combine the performance of classical concurrent objects with the high-level programmability of transactional memory. However, verifying the correctness of transactional objects is tricky, requiring reasoning simultaneously about classical concurrent objects, which guarantee the atomicity of individual methods—the property known as linearizability—and about software-transactional-memory libraries, which guarantee the atomicity of user-defined sequences of method calls—or serializability. We present a formal-verification framework called C4, built up from the familiar notion of linearizability and its compositional properties, that allows proof of both kinds of libraries, along with composition of theorems from both styles to prove correctness of applications or further libraries. We apply the framework in a significant case study, verifying a transactional set object built out of both classical and transactional components following the technique of transactional predication; the proof is modular, reasoning separately about the transactional and nontransactional parts of the implementation. Central to our approach is the use of syntactic transformers on interaction trees—i.e., transactional libraries that transform client code to enforce particular synchronization disciplines. Our framework and case studies are mechanized in Coq.},
journal = {Proc. ACM Program. Lang.},
month = {apr},
articleno = {80},
numpages = {31},
keywords = {concurrency, serializability, linearizability, verification, objects},
plclub = {Yes},
bcp = {Yes},
keys = {verification}
}
@article{GoldsteinOOPSLA2022,
author = {Goldstein, Harrison and Pierce, Benjamin C.},
title = {Parsing Randomness},
year = {2022},
issue_date = {October 2022},
number = {OOPSLA},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
journal = {Proc. ACM Program. Lang.},
plclub = {Yes},
bcp = {Yes},
paper = {http://www.cis.upenn.edu/~bcpierce/papers/oopsla22.pdf},
keys = {verification}
}
@misc{Pierce:LambdaTA2022,
author = {Benjamin C. Pierce},
title = {Software Foundations, 15 years on},
day = 20,
month = jul,
year = 2022,
note = {Talk at Newton Institute workshop on Formal Education},
plclub = {Yes},
bcp = {Yes},
slides = {http://www.cis.upenn.edu/~bcpierce/papers/LambdaTA-Newton.pdf},
keys = {verification}
}
@inproceedings{Shi2023,
author = {Jessica Shi and Benjamin Pierce and Andrew Head},
title = {Towards a Science of Interactive Proof Reading},
year = {2023},
booktitle = {13th annual workshop on the intersection of HCI and PL (PLATEAU)},
bcp = {Yes},
plclub = {Yes},
keys = {misc,verification}
}
@phdthesis{LiYishuaiThesis,
author = {Yishuai Li},
title = {Testing By Dualization},
year = {2022},
school = {University of Pennsylvania},
url = {https://repository.upenn.edu/edissertations/5376/},
bcp = {Yes},
plclub = {Yes},
keys = {verification}
}
@phdthesis{XiaLiYao,
author = {Li-Yao Xia},
title = {Executable Semantics with Interaction Trees},
year = {2022},
school = {University of Pennsylvania},
url = {https://repository.upenn.edu/edissertations/5348/},
bcp = {Yes},
plclub = {Yes},
keys = {verification}
}