CAV
This commit is contained in:
Justin Hsu
parent
9486caf1d0
commit
17eb62542e
|
|
@ -129,6 +129,7 @@
|
|||
jh = yes,
|
||||
jhsite = yes,
|
||||
reviewed = yes,
|
||||
note = "Distinguished Paper Award."
|
||||
}
|
||||
|
||||
@inproceedings{GDH22,
|
||||
|
|
@ -1312,6 +1313,23 @@ inproceedings{HHRRW14,
|
|||
}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% TALKS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
@talk{popl21-talk,
|
||||
title = {A Pre-Expectation Calculus for Probabilistic Sensitivity},
|
||||
organization = pldi22,
|
||||
year = 2022,
|
||||
month = jun,
|
||||
jh = yes,
|
||||
note = "Originally appeared in: " # popl21,
|
||||
}
|
||||
|
||||
@talk{pldg22-talk,
|
||||
title = {A User's Guide to {BI}},
|
||||
organization = {PL Discussion Group, Cornell University},
|
||||
year = 2022,
|
||||
month = mar,
|
||||
jh = yes,
|
||||
}
|
||||
|
||||
@talk{pldg21-talk,
|
||||
title = {How to Read a {PL} Paper (while also doing other things too)},
|
||||
organization = {PL Discussion Group Retreat, Cornell University},
|
||||
|
|
@ -1328,6 +1346,14 @@ inproceedings{HHRRW14,
|
|||
jh = yes,
|
||||
}
|
||||
|
||||
@talk{ll21-talk,
|
||||
title = {{PL} and Verification for Randomized Algorithms},
|
||||
organization = {Lunch and Learn Seminar, Cornell University},
|
||||
year = 2021,
|
||||
month = oct,
|
||||
jh = yes,
|
||||
}
|
||||
|
||||
@talk{ini21-talk,
|
||||
title = {Data-Driven Invariant Learning for Probabilistic Programs},
|
||||
organization = {Verified Software: From Theory to Practice {(VSOW03)}, Isaac
|
||||
|
|
@ -3644,6 +3670,15 @@ year = {2014}
|
|||
year = {2014}
|
||||
}
|
||||
|
||||
@article{OhP99,
|
||||
title = {The logic of bunched implications},
|
||||
author = {O'Hearn, Peter W and Pym, David J},
|
||||
journal = bsl,
|
||||
pages = {215--244},
|
||||
url = {https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.4742&rep=rep1&type=pdf},
|
||||
year = {1999}
|
||||
}
|
||||
|
||||
@article{POhY04,
|
||||
title = {Possible worlds and resources: The semantics of {BI}},
|
||||
author = {Pym, David J and O'Hearn, Peter W and Yang, Hongseok},
|
||||
|
|
@ -4051,7 +4086,7 @@ pages = {197--214},
|
|||
volume = {7961},
|
||||
year = {2013},
|
||||
pages = {200--215},
|
||||
url = {https://dx.doi.org/10.1007/978--3-642--39320--4\_13},
|
||||
url = {https://dx.doi.org/10.1007/978--3-642--39320--4_13},
|
||||
publisher = springer
|
||||
}
|
||||
|
||||
|
|
@ -7226,8 +7261,8 @@ publisher=springer
|
|||
volume=9779,
|
||||
pages="3--22",
|
||||
isbn="978-3-319-41528-4",
|
||||
doi="10.1007/978-3-319-41528-4\_1",
|
||||
url="https://doi.org/10.1007/978-3-319-41528-4\_1"
|
||||
doi="10.1007/978-3-319-41528-4_1",
|
||||
url="https://doi.org/10.1007/978-3-319-41528-4_1"
|
||||
}
|
||||
|
||||
@inproceedings{Chatterjee:2017:SIP:3009837.3009873,
|
||||
|
|
@ -8148,20 +8183,6 @@ url={https://doi.org/10.1007/3-540-48224-5_35}
|
|||
url = {https://www.cs.cmu.edu/~jcr/copenhagen08.pdf},
|
||||
}
|
||||
|
||||
@article{DBLP:journals/bsl/OHearnP99,
|
||||
author = {O'Hearn, Peter W and Pym, David J},
|
||||
journal = bsl,
|
||||
volume = {5},
|
||||
number = {2},
|
||||
pages = {215--244},
|
||||
year = {1999},
|
||||
url = {http://www.math.ucla.edu/\%7Easl/bsl/0502/0502-003.ps},
|
||||
publisher = cup,
|
||||
timestamp = {Fri, 31 Mar 2006 14:53:26 +0200},
|
||||
biburl = {https://dblp.org/rec/bib/journals/bsl/OHearnP99},
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||
}
|
||||
|
||||
@book{PymMono,
|
||||
title={The Semantics and Proof Theory of the Logic of Bunched Implications},
|
||||
author={David J. Pym},
|
||||
|
|
@ -8601,27 +8622,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/fm/FlanaganL01,
|
||||
author = {Cormac Flanagan and
|
||||
K. Rustan M. Leino},
|
||||
|
|
@ -9944,3 +9944,25 @@ MRREVIEWER = {R. B. Kirk},
|
|||
biburl = {https://dblp.org/rec/conf/cade/Platzer11.bib},
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||
}
|
||||
|
||||
@Inbook{Bjorner2015,
|
||||
author="Bj{\o}rner, Nikolaj
|
||||
and Gurfinkel, Arie
|
||||
and McMillan, Ken
|
||||
and Rybalchenko, Andrey",
|
||||
editor="Beklemishev, Lev D.
|
||||
and Blass, Andreas
|
||||
and Dershowitz, Nachum
|
||||
and Finkbeiner, Bernd
|
||||
and Schulte, Wolfram",
|
||||
title="Horn Clause Solvers for Program Verification",
|
||||
bookTitle="Fields of Logic and Computation {II}: Essays Dedicated to {Yuri Gurevich} on the Occasion of His 75th Birthday",
|
||||
year="2015",
|
||||
publisher=springer,
|
||||
address="Cham",
|
||||
pages="24--51",
|
||||
abstract="Automatic program verification and symbolic model checking tools interface with theorem proving technologies that check satisfiability of formulas. A theme pursued in the past years by the authors of this paper has been to encode symbolic model problems directly as Horn clauses and develop dedicated solvers for Horn clauses. Our solvers are called Duality, HSF, SeaHorn, and {\$}{\$}{\backslash}mu {\{}Z{\}}{\$}{\$}and we have devoted considerable attention in recent papers to algorithms for solving Horn clauses. This paper complements these strides as we summarize main useful properties of Horn clauses, illustrate encodings of procedural program verification into Horn clauses and then highlight a number of useful simplification strategies at the level of Horn clauses. Solving Horn clauses amounts to establishing Existential positive Fixed-point Logic formulas, a perspective that was promoted by Blass and Gurevich.",
|
||||
isbn="978-3-319-23534-9",
|
||||
doi="10.1007/978-3-319-23534-9_2",
|
||||
url="https://doi.org/10.1007/978-3-319-23534-9_2"
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,3 +1,5 @@
|
|||
+ **08/2022** Our paper **Data-Driven Invariant Learning for Probabilistic
|
||||
Programs** received a Distinguished Paper at **CAV 2022**!
|
||||
+ **08/2022** This fall, I am teaching [**Category Theory for Computer
|
||||
Scientists (CS 6117)**](https://www.cs.cornell.edu/courses/cs6117/2022fa/)!
|
||||
+ **07/2022** **Symbolic Execution for Randomized Programs** to
|
||||
|
|
|
|||
Loading…
Reference in New Issue