From f1538f102e3596dad0dc86c7a25de694503806d9 Mon Sep 17 00:00:00 2001 From: Justin Hsu Date: Thu, 30 Jun 2022 21:55:43 -0400 Subject: [PATCH] Update bibs. --- bibs/header.bib | 3 + bibs/myrefs.bib | 628 +++++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 620 insertions(+), 11 deletions(-) diff --git a/bibs/header.bib b/bibs/header.bib index 3981c5b..87db72e 100644 --- a/bibs/header.bib +++ b/bibs/header.bib @@ -247,6 +247,7 @@ @STRING{oopsla13 = oopsla # ", Indianapolis, Indiana" } @STRING{oopsla14 = oopsla # ", Portland, Oregon" } @STRING{oopsla16 = oopsla # ", Amsterdam, The Netherlands" } +@STRING{oopsla22 = oopsla # ", Auckland, New Zealand" } % ---- @STRING{lics = "{IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS})" } @STRING{licspost20 = "{ACM/IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS})" } @@ -559,6 +560,7 @@ @STRING{vmcai09 = vmcai # ", Savannah, Georgia" } @STRING{vmcai12 = vmcai # ", Philadelphia, Pennsylvania" } @STRING{vmcai13 = vmcai # ", Rome, Italy" } +@STRING{vmcai16 = vmcai # ", St. Petersburg, Florida" } % ---- @STRING{csf = "{IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium @@ -788,6 +790,7 @@ % --- @STRING{esecfse11 = esecfse # ", Szeged, Hungary" } @STRING{esecfse13 = esecfse # ", Saint Petersburg, Russia" } +@STRING{esecfse19 = esecfse # ", Tallinn, Estonia" } % --- @STRING{esop88 = esop # ", Nancy, France" } @STRING{esop92 = esop # ", Rennes, France" } diff --git a/bibs/myrefs.bib b/bibs/myrefs.bib index f632502..4d196eb 100644 --- a/bibs/myrefs.bib +++ b/bibs/myrefs.bib @@ -11,17 +11,6 @@ jhsite = yes, } -@unpublished{SLHR21, - title = {Symbolic Execution for Randomized Programs}, - author = {Susag, Zachary and - Lahiri, Sumit and - Hsu, Justin and - Roy, Subhajit}, - year = 2022, - jh = yes, - jhsite = yes, -} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% THESIS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @phdthesis{JHThesis, title = {Probabilistic Couplings for Probabilistic Reasoning}, @@ -107,6 +96,23 @@ } %%%%%%%%%%%%%%%%%%%%%%%%%%%% CONFERENCES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +@article{SLHR21, + title = {Symbolic Execution for Randomized Programs}, + author = {Susag, Zachary and + Lahiri, Sumit and + Hsu, Justin and + Roy, Subhajit}, + year = 2022, + month = jan, + journal = pacmpl, + volume = {6}, + number = {OOPSLA}, + reviewed = yes, + jh = yes, + jhsite = yes, + note = "Appeared at " # oopsla22 # ".", +} + @inproceedings{BPHR21, title = {Data-Driven Invariant Learning for Probabilistic Programs}, author = {Bao, Jialu and @@ -8454,6 +8460,27 @@ 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 @@ -9338,3 +9365,582 @@ location = {Nice, France}, biburl = {https://dblp.org/rec/books/sp/Devroye86.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } + +@inproceedings{DBLP:conf/popl/AndersonFGJKSW14, + author = {Carolyn Jane Anderson and + Nate Foster and + Arjun Guha and + Jean{-}Baptiste Jeannin and + Dexter Kozen and + Cole Schlesinger and + David Walker}, + editor = {Suresh Jagannathan and + Peter Sewell}, + title = {{NetKAT}: semantic foundations for networks}, + booktitle = popl14, + pages = {113--126}, + publisher = {{ACM}}, + year = {2014}, + url = {https://doi.org/10.1145/2535838.2535862}, + doi = {10.1145/2535838.2535862}, + timestamp = {Thu, 24 Jun 2021 16:19:31 +0200}, + biburl = {https://dblp.org/rec/conf/popl/AndersonFGJKSW14.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/pldi/0002BC22, + author = {Michael Greenberg and + Ryan Beckett and + Eric Hayden Campbell}, + editor = {Ranjit Jhala and + Isil Dillig}, + title = {Kleene algebra modulo theories: a framework for concrete {KATs}}, + booktitle = pldi22, + pages = {594--608}, + publisher = {{ACM}}, + year = {2022}, + url = {https://doi.org/10.1145/3519939.3523722}, + doi = {10.1145/3519939.3523722}, + timestamp = {Fri, 03 Jun 2022 08:42:34 +0200}, + biburl = {https://dblp.org/rec/conf/pldi/0002BC22.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@book {MR0205854, + AUTHOR = {Robinson, Abraham}, + TITLE = {Non-standard analysis}, + PUBLISHER = {North-Holland Publishing Co., Amsterdam}, + YEAR = {1966}, + PAGES = {xi+293}, + MRCLASS = {02.57}, + MRNUMBER = {0205854}, +MRREVIEWER = {G. Kreisel}, +} + +@book {MR971063, + TITLE = {Nonstandard analysis and its applications}, + SERIES = {London Mathematical Society Student Texts}, + VOLUME = {10}, + EDITOR = {Cutland, Nigel}, + NOTE = {Papers from a conference held at the University of Hull, Hull, + 1986}, + PUBLISHER = {Cambridge University Press, Cambridge}, + YEAR = {1988}, + PAGES = {xiv+346}, + ISBN = {0-521-35109-X; 0-521-35947-3}, + MRCLASS = {03H05 (03-01 03H10 26E35)}, + MRNUMBER = {971063}, +MRREVIEWER = {W. A. J. Luxemburg}, + DOI = {10.1017/CBO9781139172110}, + URL = {https://doi-org.proxy.library.cornell.edu/10.1017/CBO9781139172110}, +} + + + +@book{DBLP:books/sp/Rust05, + author = {Heinrich Rust}, + title = {Operational Semantics for Timed Systems: {A} Non-standard Approach + to Uniform Modeling of Timed and Hybrid Systems}, + series = lncs, + volume = {3456}, + publisher = springer, + year = {2005}, + url = {https://doi.org/10.1007/978-3-540-32008-1}, + doi = {10.1007/978-3-540-32008-1}, + isbn = {3-540-25576-1}, + timestamp = {Tue, 14 May 2019 10:00:35 +0200}, + biburl = {https://dblp.org/rec/books/sp/Rust05.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article {MR464380, + AUTHOR = {Anderson, Robert M.}, + TITLE = {A non-standard representation for {B}rownian motion and {I}t\^{o} + integration}, + JOURNAL = {Israel J. Math.}, + FJOURNAL = {Israel Journal of Mathematics}, + VOLUME = {25}, + YEAR = {1976}, + NUMBER = {1-2}, + PAGES = {15--46}, + ISSN = {0021-2172}, + MRCLASS = {60G05 (02H25 60H05)}, + MRNUMBER = {464380}, +MRREVIEWER = {P. A. Loeb}, + DOI = {10.1007/BF02756559}, + URL = {https://doi-org.proxy.library.cornell.edu/10.1007/BF02756559}, +} + +@inproceedings{DBLP:conf/icalp/SuenagaH11, + author = {Kohei Suenaga and + Ichiro Hasuo}, + editor = {Luca Aceto and + Monika Henzinger and + Jir{\'{\i}} Sgall}, + title = {Programming with Infinitesimals: {A} While-Language for Hybrid System + Modeling}, + booktitle = icalp11, + series = lncs, + volume = {6756}, + pages = {392--403}, + publisher = springer, + year = {2011}, + url = {https://doi.org/10.1007/978-3-642-22012-8\_31}, + doi = {10.1007/978-3-642-22012-8\_31}, + timestamp = {Tue, 14 May 2019 10:00:44 +0200}, + biburl = {https://dblp.org/rec/conf/icalp/SuenagaH11.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/cav/HasuoS12, + author = {Ichiro Hasuo and + Kohei Suenaga}, + editor = {P. Madhusudan and + Sanjit A. Seshia}, + title = {Exercises in Nonstandard Static Analysis of Hybrid Systems}, + booktitle = cav12, + series = lncs, + volume = {7358}, + pages = {462--478}, + publisher = springer, + year = {2012}, + url = {https://doi.org/10.1007/978-3-642-31424-7\_34}, + doi = {10.1007/978-3-642-31424-7\_34}, + timestamp = {Tue, 14 May 2019 10:00:43 +0200}, + biburl = {https://dblp.org/rec/conf/cav/HasuoS12.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/aplas/NakamuraKSI17, + author = {Hirofumi Nakamura and + Kensuke Kojima and + Kohei Suenaga and + Atsushi Igarashi}, + editor = {Bor{-}Yuh Evan Chang}, + title = {A Nonstandard Functional Programming Language}, + booktitle = aplas17, + series = lncs, + volume = {10695}, + pages = {514--533}, + publisher = springer, + year = {2017}, + url = {https://doi.org/10.1007/978-3-319-71237-6\_25}, + doi = {10.1007/978-3-319-71237-6\_25}, + timestamp = {Tue, 14 May 2019 10:00:41 +0200}, + biburl = {https://dblp.org/rec/conf/aplas/NakamuraKSI17.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/vmcai/KidoCH16, + author = {Kengo Kido and + Swarat Chaudhuri and + Ichiro Hasuo}, + editor = {Barbara Jobstmann and + K. Rustan M. Leino}, + title = {Abstract Interpretation with Infinitesimals - Towards Scalability + in Nonstandard Static Analysis}, + booktitle = vmcai16, + series = lncs, + volume = {9583}, + pages = {229--249}, + publisher = springer, + year = {2016}, + url = {https://doi.org/10.1007/978-3-662-49122-5\_11}, + doi = {10.1007/978-3-662-49122-5\_11}, + timestamp = {Tue, 14 May 2019 10:00:43 +0200}, + biburl = {https://dblp.org/rec/conf/vmcai/KidoCH16.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@book{oksendal2003stochastic, + title={Stochastic Differential Equations: An Introduction with Applications}, + author={{\O}ksendal, Bernt}, + isbn={9783540047582}, + lccn={2007923169}, + series={Universitext}, + year={2003}, + publisher=springer +} + +@book {MR3930614, + AUTHOR = {Durrett, Rick}, + TITLE = {Probability---theory and examples}, + SERIES = {Cambridge Series in Statistical and Probabilistic Mathematics}, + VOLUME = {49}, + NOTE = {Fifth edition of [ MR1068527]}, + PUBLISHER = cup, + YEAR = {2019}, + PAGES = {xii+419}, + ISBN = {978-1-108-47368-2}, + MRCLASS = {60-01 (37A30)}, + MRNUMBER = {3930614}, + DOI = {10.1017/9781108591034}, + URL = {https://doi-org.proxy.library.cornell.edu/10.1017/9781108591034}, +} + +@inproceedings{DBLP:conf/pldi/NgoC018, + author = {Van Chan Ngo and + Quentin Carbonneaux and + Jan Hoffmann}, + editor = {Jeffrey S. Foster and + Dan Grossman}, + title = {Bounded expectations: resource analysis for probabilistic programs}, + booktitle = pldi18, + pages = {496--512}, + publisher = {{ACM}}, + year = {2018}, + url = {https://doi.org/10.1145/3192366.3192394}, + doi = {10.1145/3192366.3192394}, + timestamp = {Wed, 23 Jun 2021 15:34:31 +0200}, + biburl = {https://dblp.org/rec/conf/pldi/NgoC018.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + + + +@inproceedings{DBLP:conf/pldi/Wang0R21, + author = {Di Wang and + Jan Hoffmann and + Thomas W. Reps}, + editor = {Stephen N. Freund and + Eran Yahav}, + title = {Central moment analysis for cost accumulators in probabilistic programs}, + booktitle = pldi21, + pages = {559--573}, + publisher = {{ACM}}, + year = {2021}, + url = {https://doi.org/10.1145/3453483.3454062}, + doi = {10.1145/3453483.3454062}, + timestamp = {Thu, 09 Dec 2021 07:39:43 +0100}, + biburl = {https://dblp.org/rec/conf/pldi/Wang0R21.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/popl/FosterKM0T15, + author = {Nate Foster and + Dexter Kozen and + Matthew Milano and + Alexandra Silva and + Laure Thompson}, + editor = {Sriram K. Rajamani and + David Walker}, + title = {A Coalgebraic Decision Procedure for {NetKAT}}, + booktitle = popl15, + pages = {343--355}, + publisher = {{ACM}}, + year = {2015}, + url = {https://doi.org/10.1145/2676726.2677011}, + doi = {10.1145/2676726.2677011}, + timestamp = {Wed, 23 Jun 2021 17:06:05 +0200}, + biburl = {https://dblp.org/rec/conf/popl/FosterKM0T15.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/toplas/Kozen97, + author = {Dexter Kozen}, + title = {Kleene Algebra with Tests}, + journal = toplas, + volume = {19}, + number = {3}, + pages = {427--443}, + year = {1997}, + url = {https://doi.org/10.1145/256167.256195}, + doi = {10.1145/256167.256195}, + timestamp = {Thu, 14 Oct 2021 09:12:21 +0200}, + biburl = {https://dblp.org/rec/journals/toplas/Kozen97.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@Inbook{Kozen2017, +author="Kozen, Dexter", +editor="Ba{\c{s}}kent, Can +and Moss, Lawrence S. +and Ramanujam, Ramaswamy", +title={On the Coalgebraic Theory of {Kleene} {Algebra} with {Tests}}, +bookTitle={{Rohit Parikh} on Logic, Language and Society}, +year="2017", +publisher=springer, +address="Cham", +pages="279--298", +isbn="978-3-319-47843-2", +doi="10.1007/978-3-319-47843-2_15", +url="https://doi.org/10.1007/978-3-319-47843-2_15" +} + +@inproceedings{DBLP:conf/sigsoft/NejatiGMBFW19, + author = {Shiva Nejati and + Khouloud Gaaloul and + Claudio Menghi and + Lionel C. Briand and + Stephen Foster and + David Wolfe}, + editor = {Marlon Dumas and + Dietmar Pfahl and + Sven Apel and + Alessandra Russo}, + title = {Evaluating model testing and model checking for finding requirements + violations in Simulink models}, + booktitle = esecfse19, + pages = {1015--1025}, + publisher = {{ACM}}, + year = {2019}, + url = {https://doi.org/10.1145/3338906.3340444}, + doi = {10.1145/3338906.3340444}, + timestamp = {Sat, 09 Apr 2022 12:47:21 +0200}, + biburl = {https://dblp.org/rec/conf/sigsoft/NejatiGMBFW19.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@misc{FB:infer, + author = {O'Hearn, Peter and + Distefano, Dino and + Calcagno, Cristiano}, + title = {Open-sourcing {Facebook Infer}: Identify bugs before you ship}, + year = 2015, + url = {https://engineering.fb.com/2015/06/11/developer-tools/open-sourcing-facebook-infer-identify-bugs-before-you-ship/}, + institution = {Facebook Engineering}, +} + +@ARTICLE{tsividis-analog, + author={Tsividis, Yannis}, + journal={IEEE Spectrum}, + title={Not your Father's analog computer}, + year={2018}, + volume={55}, + number={2}, + pages={38-43}, + doi={10.1109/MSPEC.2018.8278135} +} + + + +@article{DBLP:journals/ccr/CampbellMKMVV99, + author = {Andrew T. Campbell and + Hermann de Meer and + Michael E. Kounavis and + Kazuho Miki and + John B. Vicente and + Daniel A. M. Villela}, + title = {A survey of programmable networks}, + journal = {Comput. Commun. Rev.}, + volume = {29}, + number = {2}, + pages = {7--23}, + year = {1999}, + url = {https://doi.org/10.1145/505733.505735}, + doi = {10.1145/505733.505735}, + timestamp = {Sun, 06 Sep 2020 18:03:59 +0200}, + biburl = {https://dblp.org/rec/journals/ccr/CampbellMKMVV99.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@book{DBLP:books/sp/Platzer18, + author = {Andr{\'{e}} Platzer}, + title = {Logical Foundations of Cyber-Physical Systems}, + publisher = springer, + year = {2018}, + url = {https://doi.org/10.1007/978-3-319-63588-0}, + doi = {10.1007/978-3-319-63588-0}, + isbn = {978-3-319-63587-3}, + timestamp = {Fri, 02 Nov 2018 09:27:05 +0100}, + biburl = {https://dblp.org/rec/books/sp/Platzer18.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article {MR390154, + AUTHOR = {Loeb, Peter A.}, + TITLE = {Conversion from nonstandard to standard measure spaces and + applications in probability theory}, + JOURNAL = {Trans. Amer. Math. Soc.}, + FJOURNAL = {Transactions of the American Mathematical Society}, + VOLUME = {211}, + YEAR = {1975}, + PAGES = {113--122}, + ISSN = {0002-9947}, + MRCLASS = {28A10 (02H25 60J99)}, + MRNUMBER = {390154}, +MRREVIEWER = {R. B. Kirk}, + DOI = {10.2307/1997222}, + URL = {https://doi-org.proxy.library.cornell.edu/10.2307/1997222}, +} + +@inproceedings{DBLP:conf/popl/SuenagaSH13, + author = {Kohei Suenaga and + Hiroyoshi Sekine and + Ichiro Hasuo}, + editor = {Roberto Giacobazzi and + Radhia Cousot}, + title = {Hyperstream processing systems: nonstandard modeling of continuous-time + signals}, + booktitle = popl13, + pages = {417--430}, + publisher = {{ACM}}, + year = {2013}, + url = {https://doi.org/10.1145/2429069.2429120}, + doi = {10.1145/2429069.2429120}, + timestamp = {Thu, 14 Oct 2021 09:53:20 +0200}, + biburl = {https://dblp.org/rec/conf/popl/SuenagaSH13.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/popl/KumarMNO14, + author = {Ramana Kumar and + Magnus O. Myreen and + Michael Norrish and + Scott Owens}, + editor = {Suresh Jagannathan and + Peter Sewell}, + title = {{CakeML}: a verified implementation of {ML}}, + booktitle = popl14, + pages = {179--192}, + publisher = {{ACM}}, + year = {2014}, + url = {https://doi.org/10.1145/2535838.2535841}, + doi = {10.1145/2535838.2535841}, + timestamp = {Thu, 24 Jun 2021 16:19:31 +0200}, + biburl = {https://dblp.org/rec/conf/popl/KumarMNO14.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/cacm/KleinAEHCDEEKNSTW10, + author = {Gerwin Klein and + June Andronick and + Kevin Elphinstone and + Gernot Heiser and + David Cock and + Philip Derrin and + Dhammika Elkaduwe and + Kai Engelhardt and + Rafal Kolanski and + Michael Norrish and + Thomas Sewell and + Harvey Tuch and + Simon Winwood}, + title = {{seL4}: formal verification of an operating-system kernel}, + journal = cacm, + volume = {53}, + number = {6}, + pages = {107--115}, + year = {2010}, + url = {https://doi.org/10.1145/1743546.1743574}, + doi = {10.1145/1743546.1743574}, + timestamp = {Wed, 25 Sep 2019 17:48:13 +0200}, + biburl = {https://dblp.org/rec/journals/cacm/KleinAEHCDEEKNSTW10.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/emsoft/BajajEFP19, + author = {Viren Bajaj and + Karim Elmaaroufi and + Nathan Fulton and + Andr{\'{e}} Platzer}, + title = {Verifiably safe {SCUBA} diving using commodity sensors: work-in-progress}, + booktitle = {Proceedings of the International Conference on Embedded Software + Companion ({EMSOFT}), New York, NY}, + pages = {8}, + publisher = {{ACM}}, + year = {2019}, + url = {https://doi.org/10.1145/3349568.3351554}, + doi = {10.1145/3349568.3351554}, + timestamp = {Mon, 09 Aug 2021 14:53:48 +0200}, + biburl = {https://dblp.org/rec/conf/emsoft/BajajEFP19.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@Article{pmid19414839, + Author="Levey, A. S. and Stevens, L. A. and Schmid, C. H. and Zhang, Y. L. and Castro, A. F. and Feldman, H. I. and Kusek, J. W. and Eggers, P. and Van Lente, F. and Greene, T. and Coresh, J. ", + Title="{{A} new equation to estimate glomerular filtration rate}", + Journal="Ann. Intern. Med.", + Year="2009", + Volume="150", + Number="9", + Pages="604--612", + Month="May" +} + +@incollection{DBLP:reference/mc/0001FPP18, + author = {Laurent Doyen and + Goran Frehse and + George J. Pappas and + Andr{\'{e}} Platzer}, + editor = {Edmund M. Clarke and + Thomas A. Henzinger and + Helmut Veith and + Roderick Bloem}, + title = {Verification of Hybrid Systems}, + booktitle = {Handbook of Model Checking}, + pages = {1047--1110}, + publisher = {Springer}, + year = {2018}, + url = {https://doi.org/10.1007/978-3-319-10575-8\_30}, + doi = {10.1007/978-3-319-10575-8\_30}, + timestamp = {Mon, 03 Jan 2022 22:13:30 +0100}, + biburl = {https://dblp.org/rec/reference/mc/0001FPP18.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/itp/FultonMBP17, + author = {Nathan Fulton and + Stefan Mitsch and + Rose Bohrer and + Andr{\'{e}} Platzer}, + editor = {Mauricio Ayala{-}Rinc{\'{o}}n and + C{\'{e}}sar A. Mu{\~{n}}oz}, + title = {Bellerophon: Tactical Theorem Proving for Hybrid Systems}, + booktitle = {International Conference on Interactive Theorem Proving ({ITP}), + Bras{\'{\i}}lia, Brazil}, + series = {Lecture Notes in Computer Science}, + volume = {10499}, + pages = {207--224}, + publisher = {Springer}, + year = {2017}, + url = {https://doi.org/10.1007/978-3-319-66107-0\_14}, + doi = {10.1007/978-3-319-66107-0\_14}, + timestamp = {Tue, 10 May 2022 14:16:41 +0200}, + biburl = {https://dblp.org/rec/conf/itp/FultonMBP17.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@book{DBLP:books/daglib/0025392, + author = {Andr{\'{e}} Platzer}, + title = {Logical Analysis of Hybrid Systems - Proving Theorems for Complex + Dynamics}, + publisher = {Springer}, + year = {2010}, + url = {https://doi.org/10.1007/978-3-642-14509-4}, + doi = {10.1007/978-3-642-14509-4}, + isbn = {978-3-642-14508-7}, + timestamp = {Mon, 29 May 2017 13:41:04 +0200}, + biburl = {https://dblp.org/rec/books/daglib/0025392.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@phdthesis{DBLP:phd/dnb/Platzer12, + author = {Andr{\'{e}} Platzer}, + title = {Differential dynamic logics - automated theorem proving for hybrid systems}, + school = {Carl von Ossietzky University of Oldenburg}, + year = {2008}, + url = {http://oops.uni-oldenburg.de/1403/}, + urn = {urn:nbn:de:gbv:715-oops-14833}, + timestamp = {Sat, 17 Jul 2021 09:07:29 +0200}, + biburl = {https://dblp.org/rec/phd/dnb/Platzer12.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/cade/Platzer11, + author = {Andr{\'{e}} Platzer}, + editor = {Nikolaj S. Bj{\o}rner and + Viorica Sofronie{-}Stokkermans}, + title = {Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs}, + booktitle = {International Conference on Automated Deduction ({CADE}), Wroclaw, Poland}, + series = {Lecture Notes in Computer Science}, + volume = {6803}, + pages = {446--460}, + publisher = {Springer}, + year = {2011}, + url = {https://doi.org/10.1007/978-3-642-22438-6\_34}, + doi = {10.1007/978-3-642-22438-6\_34}, + timestamp = {Thu, 14 Apr 2022 20:26:15 +0200}, + biburl = {https://dblp.org/rec/conf/cade/Platzer11.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +}