justhsu
/
justin-site
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Add POPL accept.

This commit is contained in:
Justin Hsu 2021-12-01 10:49:14 -05:00
parent 0d374add02
commit b9cc9668c2
3 changed files with 398 additions and 46 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
bibs/header.bib
View File

@ -167,6 +167,7 @@
@STRING{popl04 = popl # ", Venice, Italy" }
@STRING{popl05 = popl # ", Long Beach, California" }
@STRING{popl06 = popl # ", Charleston, South Carolina" }
@STRING{popl07 = popl # ", Nice, France" }
@STRING{popl08 = popl # ", San Francisco, California" }
@STRING{popl09 = popl # ", Savannah, Georgia" }
@STRING{popl10 = popl # ", Madrid, Spain" }
@ -181,6 +182,7 @@
@STRING{popl19 = popl # ", Lisbon, Portugal" }
@STRING{popl20 = popl # ", New Orleans, Louisiana" }
@STRING{popl21 = popl }
@STRING{popl22 = popl # ", Philadelphia, Pennsylvania" }
% ----
@STRING{icfp = "{ACM} {SIGPLAN} {I}nternational {C}onference on
@ -214,6 +216,7 @@
{S}ystems, {L}anguages, and {A}pplications ({OOPSLA})" }
@STRING{ccs = "{ACM} {SIGSAC} Conference on Computer and Communications Security ({CCS})"}
@STRING{ccs12 = ccs # ", Raleigh, North Carolina" }
@STRING{ccs13 = ccs # ", Berlin, Germany" }
@STRING{ccs14 = ccs # ", Scottsdale, Arizona" }
@STRING{ccs15 = ccs # ", Boulder, Colorado" }
@ -570,6 +573,7 @@
@STRING{aplas = {Asian Symposium on Programming Languages and Systems (APLAS)} }
@STRING{asplos = {International Conference on Architectural Support for
Programming Langauages and Operating Systems (ASPLOS)} }
@STRING{ase = {IEEE/ACM International Conference on Automated Software Engineering (ASE)} }
@STRING{atva = {International Symposium on Automated Technology for
Verification and Analysis (ATVA)} }
@STRING{calco = {Conference on Algebra and Coalgebra in Computer Science ({CALCO})}}
@ -606,6 +610,7 @@
@STRING{icalp = {International Colloquium on Automata, Languages and
Programming (ICALP)} }
@STRING{icse = {International Conference on Software Engineering (ICSE)} }
@STRING{issta = {{ACM} {SIGSOFT} International Symposium on Software Testing and Analysis {(ISSTA)}} }
@STRING{ictac = {International Colloquium on Theoretical Aspects of Computing (ICTAC)} }
@STRING{ijcai = {International Joint Conference on Artificial Intelligence (IJCAI)} }
@STRING{ijcar = {International Joint Conference on Automated Reasoning (IJCAR)} }
@ -633,6 +638,8 @@
and Computation (RANDOM)} }
@STRING{rta = {International Conference on Rewriting Techniques and
Applications (RTA)} }
@STRING{rvpre10 = {International Workshop on Runtime Verification (RV)} }
@STRING{rv = {International Conference on Runtime Verification (RV)} }
@STRING{sas = {International Symposium on Static Analysis (SAS)} }
@STRING{sosp = {ACM Symposium on Operating Systems Principles (SOSP)} }
@STRING{sandp = { {IEEE} Symposium on Security and Privacy (S\&P) }}
@ -676,8 +683,11 @@
@STRING{ascrypt15 = ascrypt # ", Auckland, New Zealand" }
@STRING{ascrypt18 = ascrypt # ", Brisbane, Australia" }
%----
@STRING{asplos14 = asplos # ", Salt Lake City, Utah" }
@STRING{asplos06 = asplos # ", San Jose, California" }
@STRING{asplos14 = asplos # ", Salt Lake City, Utah" }
@STRING{asplos21 = asplos}
%----
@STRING{ase17 = ase # ", Urbana, Illinois" }
%----
@STRING{atva19 = atva # ", Taipei City, Taiwan" }
%----
@ -710,6 +720,7 @@
@STRING{cav06 = cav # ", Seattle, Washington" }
@STRING{cav07 = cav # ", Berlin, Germany" }
@STRING{cav08 = cav # ", Princeton, New Jersey" }
@STRING{cav10 = cav # ", Edinburgh, Scotland" }
@STRING{cav11 = cav # ", Snowbird, Utah" }
@STRING{cav12 = cav # ", Berkeley, California" }
@STRING{cav13 = cav # ", Saint Petersburg, Russia" }
@ -808,9 +819,12 @@ STRING{fse08 = fse # ", Atlanta, Georgia" }
@STRING{icalp17 = icalp # ", Warsaw, Poland" }
@STRING{icalp18 = icalp # ", Prague, Czech Republic" }
% ---
@STRING{icse13 = icse # ", San Francisco, California" }
@STRING{icse14 = icse # ", Hyderabad, India" }
@STRING{icse19 = icse # ", Montr{\'e}al, Qu{\'e}bec" }
% ---
@STRING{issta12 = issta # ", Minneapolis, Minnesota" }
% ---
@STRING{ictac18 = ictac # ", Stellenbosch, South Africa" }
% ---
@STRING{ijcai15 = ijcai # ", Buenos Aires, Argentina" }
@ -847,6 +861,7 @@ STRING{fse08 = fse # ", Atlanta, Georgia" }
% ---
@STRING{osdi96 = osdi # ", Seattle, Washington" }
@STRING{osdi00 = osdi # ", San Diego, California" }
@STRING{osdi08 = osdi # ", San Diego, California" }
@STRING{osdi12 = osdi # ", Hollywood, California" }
% ---
@STRING{paste01 = paste # ", Snowbird, Utah" }
@ -862,6 +877,8 @@ STRING{fse08 = fse # ", Atlanta, Georgia" }
% ---
@STRING{randapx13 = randapx # ", Berkeley, California" }
% ---
@STRING{rv09 = rvpre10 # ", Grenoble, France" }
% ---
@STRING{sas95 = sas # ", Glasgow, Scotland" }
@STRING{sas96 = sas # ", Aachen, Germany" }
@STRING{sas97 = sas # ", Paris, France" }
@ -869,6 +886,7 @@ STRING{fse08 = fse # ", Atlanta, Georgia" }
@STRING{sas01 = sas # ", Paris, France" }
@STRING{sas04 = sas # ", Verona, Italy" }
@STRING{sas05 = sas # ", London, England" }
@STRING{sas06 = sas # ", Seoul, Korea" }
@STRING{sas09 = sas # ", Los Angeles, California" }
@STRING{sas10 = sas # ", Perpignan, France" }
@STRING{sas11 = sas # ", Venice, Italy" }

409
bibs/myrefs.bib
View File

@ -1,15 +1,4 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%% UNPUBLISHED %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@unpublished{BGHT21,
title = {A Separation Logic for Negative Dependence},
author = {Bao, Jialu and
Gaboardi, Marco and
Hsu, Justin and
Tassarotti, Joseph},
year = 2021,
jh = yes,
jhsite = no,
}
@unpublished{SLHR21,
title = {Symbolic Execution for Randomized Programs},
author = {Susag, Zachary and
@ -121,6 +110,27 @@
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%% CONFERENCES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@article{BGHT21,
title = {A Separation Logic for Negative Dependence},
author = {Bao, Jialu and
Gaboardi, Marco and
Hsu, Justin and
Tassarotti, Joseph},
url = {https://arxiv.org/abs/2111.14917},
eprint = {2111.14917},
archivePrefix = {arXiv},
primaryClass = {cs.PL},
year = 2022,
month = jan,
journal = pacmpl,
volume = {6},
number = {POPL},
reviewed = yes,
jh = yes,
jhsite = yes,
note = "Appeared at " # popl22 # ".",
}
@inproceedings{BDHS20,
title = {A Bunched Logic for Conditional Independence},
author = {Bao, Jialu and
@ -8395,27 +8405,6 @@ note={Errata and Remarks maintained at:
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/scp/ErnstPGMPTX07,
author = {Michael D. Ernst and
Jeff H. Perkins and
Philip J. Guo and
Stephen McCamant and
Carlos Pacheco and
Matthew S. Tschantz and
Chen Xiao},
title = {The {Daikon} system for dynamic detection of likely invariants},
journal = {Sci. Comput. Program.},
volume = {69},
number = {1-3},
pages = {35--45},
year = {2007},
url = {https://doi.org/10.1016/j.scico.2007.01.015},
doi = {10.1016/j.scico.2007.01.015},
timestamp = {Sat, 27 May 2017 14:22:55 +0200},
biburl = {https://dblp.org/rec/journals/scp/ErnstPGMPTX07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/popl/0001NMR16,
author = {Pranav Garg and
Daniel Neider and
@ -8944,3 +8933,359 @@ keywords = {Machine learning, Probabilistic programming, Program analysis},
biburl = {https://dblp.org/rec/conf/pldi/WangS0CG21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{barthe_katoen_silva_2020,
place={Cambridge},
title={Foundations of Probabilistic Programming},
DOI={10.1017/9781108770750},
publisher=cup,
year={2020}}
@inproceedings{DBLP:conf/ifip/Freivalds77,
author = {Rusins Freivalds},
title = {Probabilistic Machines Can Use Less Running Time},
booktitle = {{IFIP} Congress},
pages = {839--842},
publisher = {North-Holland},
year = {1977}
}
@inproceedings{DBLP:conf/ccs/Mironov12,
author = {Ilya Mironov},
title = {On significance of the least significant bits for differential privacy},
booktitle = ccs12,
pages = {650--661},
publisher = {{ACM}},
year = {2012}
}
@inproceedings{DBLP:conf/issta/GeldenhuysDV12,
author = {Jaco Geldenhuys and
Matthew B. Dwyer and
Willem Visser},
editor = {Mats Per Erik Heimdahl and
Zhendong Su},
title = {Probabilistic symbolic execution},
booktitle = issta,
pages = {166--176},
year = {2012},
url = {https://doi.org/10.1145/2338965.2336773},
doi = {10.1145/2338965.2336773},
timestamp = {Tue, 06 Nov 2018 16:57:30 +0100},
biburl = {https://dblp.org/rec/conf/issta/GeldenhuysDV12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icse/FilieriPV13,
author = {Antonio Filieri and
Corina S. Pasareanu and
Willem Visser},
editor = {David Notkin and
Betty H. C. Cheng and
Klaus Pohl},
title = {Reliability analysis in symbolic pathfinder},
booktitle = icse13,
pages = {622--631},
year = {2013},
url = {https://doi.org/10.1109/ICSE.2013.6606608},
doi = {10.1109/ICSE.2013.6606608},
timestamp = {Wed, 16 Oct 2019 14:14:49 +0200},
biburl = {https://dblp.org/rec/conf/icse/FilieriPV13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/asplos/KangXQC21,
author = {Qiao Kang and
Jiarong Xing and
Yiming Qiu and
Ang Chen},
editor = {Tim Sherwood and
Emery D. Berger and
Christos Kozyrakis},
title = {Probabilistic profiling of stateful data planes for adversarial testing},
booktitle = asplos21,
pages = {286--301},
year = {2021},
url = {https://doi.org/10.1145/3445814.3446764},
doi = {10.1145/3445814.3446764},
timestamp = {Tue, 21 Sep 2021 18:28:10 +0200},
biburl = {https://dblp.org/rec/conf/asplos/KangXQC21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/Ilvento20,
author = {Christina Ilvento},
editor = {Jay Ligatti and
Xinming Ou and
Jonathan Katz and
Giovanni Vigna},
title = {Implementing the Exponential Mechanism with Base-2 Differential Privacy},
booktitle = ccs20,
pages = {717--742},
year = {2020},
url = {https://doi.org/10.1145/3372297.3417269},
doi = {10.1145/3372297.3417269},
timestamp = {Tue, 10 Nov 2020 19:57:25 +0100},
biburl = {https://dblp.org/rec/conf/ccs/Ilvento20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/kbse/LiewSCDZW17,
author = {Daniel Liew and
Daniel Schemmel and
Cristian Cadar and
Alastair F. Donaldson and
Rafael Z{\"{a}}hl and
Klaus Wehrle},
editor = {Grigore Rosu and
Massimiliano Di Penta and
Tien N. Nguyen},
title = {Floating-point symbolic execution: a case study in n-version programming},
booktitle = {Proceedings of the 32nd {IEEE/ACM} International Conference on Automated
Software Engineering, {ASE} 2017, Urbana, IL, USA, October 30 - November
03, 2017},
pages = {601--612},
publisher = {{IEEE} Computer Society},
year = {2017},
url = {https://doi.org/10.1109/ASE.2017.8115670},
doi = {10.1109/ASE.2017.8115670},
timestamp = {Sat, 05 Sep 2020 18:05:11 +0200},
biburl = {https://dblp.org/rec/conf/kbse/LiewSCDZW17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{king1976,
author = {King, James C.},
title = {Symbolic Execution and Program Testing},
year = {1976},
issue_date = {July 1976},
publisher = acm,
address = {New York, NY, USA},
volume = {19},
number = {7},
issn = {0001-0782},
url = {https://doi.org/10.1145/360248.360252},
doi = {10.1145/360248.360252},
journal = cacm,
month = jul,
pages = {385–394},
numpages = {10},
keywords = {program debugging, program proving, symbolic interpretation, program verification, symbolic execution, program testing}
}
@inproceedings{cadar2008,
author = {Cristian Cadar and
Daniel Dunbar and
Dawson R. Engler},
editor = {Richard Draves and
Robbert van Renesse},
title = {{KLEE:} Unassisted and Automatic Generation of High-Coverage Tests
for Complex Systems Programs},
booktitle = osdi08,
pages = {209--224},
year = {2008},
url = {http://www.usenix.org/events/osdi08/tech/full\_papers/cadar/cadar.pdf},
timestamp = {Thu, 12 Mar 2020 11:35:55 +0100},
biburl = {https://dblp.org/rec/conf/osdi/CadarDE08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{10.1145/800027.808445,
author = {Boyer, Robert S. and Elspas, Bernard and Levitt, Karl N.},
title = {{SELECT}---a Formal System for Testing and Debugging Programs by Symbolic Execution},
year = {1975},
isbn = {9781450373852},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/800027.808445},
doi = {10.1145/800027.808445},
booktitle = {International Conference on Reliable Software, Los Angeles, California},
pages = {234--245},
numpages = {12},
keywords = {Solution of systems of inequalities, Program testing, Symbolic execution, Program verification, Program debugging, Test data generation},
}
@ARTICLE{1702443,
author={Howden, W.E.},
journal={{IEEE} Transactions on Software Engineering},
title={Symbolic Testing and the {DISSECT} Symbolic Evaluation System},
year={1977},
volume={SE-3},
number={4},
pages={266-278},
doi={10.1109/TSE.1977.231144}}
@article{DBLP:journals/acta/ChistikovDM17,
author = {Dmitry Chistikov and
Rayna Dimitrova and
Rupak Majumdar},
title = {Approximate counting in {SMT} and value estimation for probabilistic
programs},
journal = {Acta Informatica},
volume = {54},
number = {8},
pages = {729--764},
year = {2017},
url = {https://doi.org/10.1007/s00236-017-0297-2},
doi = {10.1007/s00236-017-0297-2},
timestamp = {Sun, 21 Jun 2020 17:38:08 +0200},
biburl = {https://dblp.org/rec/journals/acta/ChistikovDM17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@INPROCEEDINGS{7102601,
author={Yi, Qiuping and Yang, Zijiang and Guo, Shengjian and Wang, Chao and Liu, Jian and Zhao, Chen},
booktitle={{IEEE} International Conference on Software Testing, Verification and Validation ({ICST})},
title={Postconditioned Symbolic Execution},
year={2015},
pages={1--10},
doi={10.1109/ICST.2015.7102601}}
@inproceedings{DBLP:conf/cav/McMillan10,
author = {Kenneth L. McMillan},
editor = {Tayssir Touili and
Byron Cook and
Paul B. Jackson},
title = {Lazy Annotation for Program Testing and Verification},
booktitle = cav10,
series = lncs,
volume = {6174},
pages = {104--118},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14295-6\_10},
doi = {10.1007/978-3-642-14295-6\_10},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/McMillan10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{10.1145/1190216.1190226,
author = {Godefroid, Patrice},
title = {Compositional Dynamic Test Generation},
year = {2007},
isbn = {1595935754},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/1190216.1190226},
doi = {10.1145/1190216.1190226},
booktitle = popl07,
pages = {47--54},
numpages = {8},
keywords = {compositional program analysis, software testing, program verification, scalability, automatic test generation},
location = {Nice, France},
}
@inproceedings{DBLP:conf/rv/HansenSS09,
author = {Trevor Hansen and
Peter Schachte and
Harald S{\o}ndergaard},
editor = {Saddek Bensalem and
Doron A. Peled},
title = {State Joining and Splitting for the Symbolic Execution of Binaries},
booktitle = rv09,
series = lncs,
volume = {5779},
pages = {76--92},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-04694-0\_6},
doi = {10.1007/978-3-642-04694-0\_6},
timestamp = {Tue, 14 May 2019 10:00:51 +0200},
biburl = {https://dblp.org/rec/conf/rv/HansenSS09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{demoura2008,
author = {de Moura, Leonardo and Bj{\o}rner, Nikolaj},
editor = {Ramakrishnan, C. R. and Rehof, Jakob},
title = {{Z3}: An Efficient {SMT} Solver},
booktitle = tacas08,
year = {2008},
publisher = {Springer Berlin Heidelberg},
address = {Berlin, Heidelberg},
pages = {337--340},
isbn = {978-3-540-78800-3},
}
@article{DBLP:journals/corr/abs-1811-01721,
author = {Jeff Johnson},
title = {Rethinking floating point for deep learning},
journal = {CoRR},
volume = {abs/1811.01721},
year = {2018},
url = {http://arxiv.org/abs/1811.01721},
eprinttype = {arXiv},
eprint = {1811.01721},
timestamp = {Thu, 22 Nov 2018 17:58:30 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1811-01721.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@misc{google-dp,
author = {Google},
title = {Differential Privacy Libraries and Tools},
url = {https://opensource.google/projects/differential-privacy},
year = 2019,
}
@inproceedings{DBLP:conf/pldi/BlanchetCCFMMMR03,
author = {Bruno Blanchet and
Patrick Cousot and
Radhia Cousot and
J{\'{e}}r{\^{o}}me Feret and
Laurent Mauborgne and
Antoine Min{\'{e}} and
David Monniaux and
Xavier Rival},
editor = {Ron Cytron and
Rajiv Gupta},
title = {A static analyzer for large safety-critical software},
booktitle = pldi03,
pages = {196--207},
year = {2003},
url = {https://doi.org/10.1145/781131.781153},
doi = {10.1145/781131.781153},
timestamp = {Fri, 25 Jun 2021 17:17:37 +0200},
biburl = {https://dblp.org/rec/conf/pldi/BlanchetCCFMMMR03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sas/GoubaultP06,
author = {Eric Goubault and
Sylvie Putot},
editor = {Kwangkeun Yi},
title = {Static Analysis of Numerical Algorithms},
booktitle = sas06,
series = lncs,
volume = {4134},
pages = {18--34},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11823230\_3},
doi = {10.1007/11823230\_3},
timestamp = {Tue, 14 May 2019 10:00:52 +0200},
biburl = {https://dblp.org/rec/conf/sas/GoubaultP06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{DBLP:books/sp/Devroye86,
author = {Luc Devroye},
title = {Non-Uniform Random Variate Generation},
publisher = {Springer},
year = {1986},
url = {https://doi.org/10.1007/978-1-4613-8643-8},
doi = {10.1007/978-1-4613-8643-8},
isbn = {978-1-4613-8645-2},
timestamp = {Wed, 24 Jul 2019 16:59:05 +0200},
biburl = {https://dblp.org/rec/books/sp/Devroye86.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

15
content/news.md
View File

@ -1,3 +1,5 @@
+ **11/2021** *A Separation Logic for Negative Dependence** to appear at **POPL
2022**.
+ **08/2021** This fall, I'm teaching a graduate seminar on **Foundations of
Probabilistic Programming (CS 6182)**. Follow along [here](https://www.cs.cornell.edu/courses/cs6182/2021fa/)!
+ **07/2021** I'm happy to serve on the PC of **POPL 2022** and **PLDI 2022**.
@ -18,16 +20,3 @@
been selected as a **Distingiushed Paper** at **POPL 2021**!
+ **12/2020** **Learning Differentially Private Mechanisms** to appear at **S&P
2021**.
+ **10/2020** I was happy to present a tutorial on probabilistic couplings at
[**CMCS 2020**](https://www.coalg.org/cmcs20/). Slides are available
[here](https://justinh.su/files/slides/cmcs20-tutorial.pdf).
+ **10/2020** **A Pre-Expectation Calculus for Probabilistic Sensitivity** to
appear at **POPL 2021**.
+ **09/2020** This fall, I'm teaching a graduate seminar on **Security and
Privacy in Data Science (CS 763)**. Follow along
[here](https://pages.cs.wisc.edu/~justhsu/teaching/current/cs763/)!
+ **07/2020** I was happy to give a talk at the [**Online Worldwide Seminar on
Logic and Semantics: Young Researcher
(OWLS-YR)**](https://www.cs.bham.ac.uk/~vicaryjo/owls/) on probabilistic
separation logic. Slides are available
[here](https://justinh.su/files/slides/owls-yr.pdf).