[{"citation":{"apa":"Mciver, A., Morgan, C., Kaminski, B. L., & Katoen, J. P. (2017). A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. Los Angeles, CA, United States: Association for Computing Machinery. https://doi.org/10.1145/3158121","ama":"Mciver A, Morgan C, Kaminski BL, Katoen JP. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2017;2(POPL). doi:10.1145/3158121","ieee":"A. Mciver, C. Morgan, B. L. Kaminski, and J. P. Katoen, “A new proof rule for almost-sure termination,” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL. Association for Computing Machinery, 2017.","short":"A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM on Programming Languages 2 (2017).","mla":"Mciver, Annabelle, et al. “A New Proof Rule for Almost-Sure Termination.” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, 33, Association for Computing Machinery, 2017, doi:10.1145/3158121.","ista":"Mciver A, Morgan C, Kaminski BL, Katoen JP. 2017. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2(POPL), 33.","chicago":"Mciver, Annabelle, Carroll Morgan, Benjamin Lucien Kaminski, and Joost P Katoen. “A New Proof Rule for Almost-Sure Termination.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158121."},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","author":[{"first_name":"Annabelle","full_name":"Mciver, Annabelle","last_name":"Mciver"},{"full_name":"Morgan, Carroll","last_name":"Morgan","first_name":"Carroll"},{"full_name":"Kaminski, Benjamin Lucien","last_name":"Kaminski","first_name":"Benjamin Lucien"},{"id":"4524F760-F248-11E8-B48F-1D18A9856A87","first_name":"Joost P","full_name":"Katoen, Joost P","last_name":"Katoen"}],"external_id":{"arxiv":["1711.03588"]},"article_processing_charge":"No","title":"A new proof rule for almost-sure termination","article_number":"33","year":"2017","day":"07","publication":"Proceedings of the ACM on Programming Languages","date_published":"2017-12-07T00:00:00Z","doi":"10.1145/3158121","date_created":"2021-12-05T23:01:49Z","acknowledgement":"McIver and Morgan are grateful to David Basin and the Information Security Group at ETH Zürich for hosting a six-month stay in Switzerland, during part of which this work began. And thanks particularly to Andreas Lochbihler, who shared with us the probabilistic termination problem that led to it. They acknowledge the support of ARC grant DP140101119. Part of this work was carried out during the Workshop on Probabilistic Programming Semantics\r\nat McGill University’s Bellairs Research Institute on Barbados organised by Alexandra Silva and\r\nPrakash Panangaden. Kaminski and Katoen are grateful to Sebastian Junges for spotting a flaw in §5.4.","quality_controlled":"1","publisher":"Association for Computing Machinery","oa":1,"date_updated":"2021-12-07T08:04:14Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"_id":"10418","article_type":"original","type":"journal_article","conference":{"name":"POPL: Programming Languages","location":"Los Angeles, CA, United States","end_date":"2018-01-13","start_date":"2018-01-07"},"status":"public","publication_identifier":{"eissn":["2475-1421"]},"publication_status":"published","language":[{"iso":"eng"}],"issue":"POPL","volume":2,"abstract":[{"lang":"eng","text":"We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates \"almost surely\". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice. Like others, we use variant functions (a.k.a. \"super-martingales\") that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains."}],"oa_version":"Published Version","scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://dl.acm.org/doi/10.1145/3158121"}],"month":"12","intvolume":" 2"},{"type":"conference","conference":{"start_date":"2017-01-12","end_date":"2017-01-15","location":"Copenhagen, Denmark","name":"FOGA: Foundations of Genetic Algorithms"},"status":"public","_id":"1112","publist_id":"6255","author":[{"last_name":"Paixao","full_name":"Paixao, Tiago","orcid":"0000-0003-2361-3953","id":"2C5658E6-F248-11E8-B48F-1D18A9856A87","first_name":"Tiago"},{"full_name":"Pérez Heredia, Jorge","last_name":"Pérez Heredia","first_name":"Jorge"}],"department":[{"_id":"NiBa"}],"title":"An application of stochastic differential equations to evolutionary algorithms","citation":{"ama":"Paixao T, Pérez Heredia J. An application of stochastic differential equations to evolutionary algorithms. In: Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms. ACM; 2017:3-11. doi:10.1145/3040718.3040729","apa":"Paixao, T., & Pérez Heredia, J. (2017). An application of stochastic differential equations to evolutionary algorithms. In Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms (pp. 3–11). Copenhagen, Denmark: ACM. https://doi.org/10.1145/3040718.3040729","ieee":"T. Paixao and J. Pérez Heredia, “An application of stochastic differential equations to evolutionary algorithms,” in Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms, Copenhagen, Denmark, 2017, pp. 3–11.","short":"T. Paixao, J. Pérez Heredia, in:, Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms, ACM, 2017, pp. 3–11.","mla":"Paixao, Tiago, and Jorge Pérez Heredia. “An Application of Stochastic Differential Equations to Evolutionary Algorithms.” Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms, ACM, 2017, pp. 3–11, doi:10.1145/3040718.3040729.","ista":"Paixao T, Pérez Heredia J. 2017. An application of stochastic differential equations to evolutionary algorithms. Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms. FOGA: Foundations of Genetic Algorithms, 3–11.","chicago":"Paixao, Tiago, and Jorge Pérez Heredia. “An Application of Stochastic Differential Equations to Evolutionary Algorithms.” In Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms, 3–11. ACM, 2017. https://doi.org/10.1145/3040718.3040729."},"date_updated":"2021-01-12T06:48:22Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"ACM","scopus_import":1,"quality_controlled":"1","month":"01","abstract":[{"text":"There has been renewed interest in modelling the behaviour of evolutionary algorithms by more traditional mathematical objects, such as ordinary differential equations or Markov chains. The advantage is that the analysis becomes greatly facilitated due to the existence of well established methods. However, this typically comes at the cost of disregarding information about the process. Here, we introduce the use of stochastic differential equations (SDEs) for the study of EAs. SDEs can produce simple analytical results for the dynamics of stochastic processes, unlike Markov chains which can produce rigorous but unwieldy expressions about the dynamics. On the other hand, unlike ordinary differential equations (ODEs), they do not discard information about the stochasticity of the process. We show that these are especially suitable for the analysis of fixed budget scenarios and present analogs of the additive and multiplicative drift theorems for SDEs. We exemplify the use of these methods for two model algorithms ((1+1) EA and RLS) on two canonical problems(OneMax and LeadingOnes).","lang":"eng"}],"oa_version":"None","page":"3 - 11","doi":"10.1145/3040718.3040729","date_published":"2017-01-12T00:00:00Z","date_created":"2018-12-11T11:50:12Z","publication_identifier":{"isbn":["978-145034651-1"]},"publication_status":"published","year":"2017","day":"12","publication":"Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms","language":[{"iso":"eng"}]},{"oa":1,"quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","year":"2017","has_accepted_license":"1","day":"01","page":"38:1-38-21","date_created":"2018-12-11T11:50:33Z","date_published":"2017-01-01T00:00:00Z","doi":"10.4230/LIPIcs.ITCS.2017.38","citation":{"ista":"Alwen JF, De Rezende S, Nordstrom J, Vinyals M. 2017. Cumulative space in black-white pebbling and resolution. ITCS: Innovations in Theoretical Computer Science, LIPIcs, vol. 67, 38:1-38-21.","chicago":"Alwen, Joel F, Susanna De Rezende, Jakob Nordstrom, and Marc Vinyals. “Cumulative Space in Black-White Pebbling and Resolution.” edited by Christos Papadimitriou, 67:38:1-38-21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.ITCS.2017.38.","short":"J.F. Alwen, S. De Rezende, J. Nordstrom, M. Vinyals, in:, C. Papadimitriou (Ed.), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, p. 38:1-38-21.","ieee":"J. F. Alwen, S. De Rezende, J. Nordstrom, and M. Vinyals, “Cumulative space in black-white pebbling and resolution,” presented at the ITCS: Innovations in Theoretical Computer Science, Berkeley, CA, United States, 2017, vol. 67, p. 38:1-38-21.","ama":"Alwen JF, De Rezende S, Nordstrom J, Vinyals M. Cumulative space in black-white pebbling and resolution. In: Papadimitriou C, ed. Vol 67. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017:38:1-38-21. doi:10.4230/LIPIcs.ITCS.2017.38","apa":"Alwen, J. F., De Rezende, S., Nordstrom, J., & Vinyals, M. (2017). Cumulative space in black-white pebbling and resolution. In C. Papadimitriou (Ed.) (Vol. 67, p. 38:1-38-21). Presented at the ITCS: Innovations in Theoretical Computer Science, Berkeley, CA, United States: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ITCS.2017.38","mla":"Alwen, Joel F., et al. Cumulative Space in Black-White Pebbling and Resolution. Edited by Christos Papadimitriou, vol. 67, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, p. 38:1-38-21, doi:10.4230/LIPIcs.ITCS.2017.38."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"6179","author":[{"id":"2A8DFA8C-F248-11E8-B48F-1D18A9856A87","first_name":"Joel F","full_name":"Alwen, Joel F","last_name":"Alwen"},{"first_name":"Susanna","full_name":"De Rezende, Susanna","last_name":"De Rezende"},{"first_name":"Jakob","last_name":"Nordstrom","full_name":"Nordstrom, Jakob"},{"last_name":"Vinyals","full_name":"Vinyals, Marc","first_name":"Marc"}],"title":"Cumulative space in black-white pebbling and resolution","editor":[{"first_name":"Christos","last_name":"Papadimitriou","full_name":"Papadimitriou, Christos"}],"abstract":[{"text":"We study space complexity and time-space trade-offs with a focus not on peak memory usage but on overall memory consumption throughout the computation. Such a cumulative space measure was introduced for the computational model of parallel black pebbling by [Alwen and Serbinenko ’15] as a tool for obtaining results in cryptography. We consider instead the non- deterministic black-white pebble game and prove optimal cumulative space lower bounds and trade-offs, where in order to minimize pebbling time the space has to remain large during a significant fraction of the pebbling. We also initiate the study of cumulative space in proof complexity, an area where other space complexity measures have been extensively studied during the last 10–15 years. Using and extending the connection between proof complexity and pebble games in [Ben-Sasson and Nordström ’08, ’11] we obtain several strong cumulative space results for (even parallel versions of) the resolution proof system, and outline some possible future directions of study of this, in our opinion, natural and interesting space measure.","lang":"eng"}],"oa_version":"Published Version","alternative_title":["LIPIcs"],"scopus_import":1,"intvolume":" 67","month":"01","publication_status":"published","publication_identifier":{"issn":["18688969"]},"language":[{"iso":"eng"}],"file":[{"creator":"system","file_size":557769,"date_updated":"2020-07-14T12:44:37Z","file_name":"IST-2018-927-v1+1_LIPIcs-ITCS-2017-38.pdf","date_created":"2018-12-12T10:17:11Z","relation":"main_file","access_level":"open_access","content_type":"application/pdf","checksum":"dbc94810be07c2fb1945d5c2a6130e6c","file_id":"5263"}],"volume":67,"_id":"1175","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"name":"ITCS: Innovations in Theoretical Computer Science","start_date":"2017-01-09","end_date":"2017-01-11","location":"Berkeley, CA, United States"},"type":"conference","pubrep_id":"927","status":"public","date_updated":"2021-01-12T06:48:51Z","ddc":["005","600"],"file_date_updated":"2020-07-14T12:44:37Z","department":[{"_id":"KrPi"}]},{"page":"525-559","date_created":"2018-12-11T11:50:38Z","date_published":"2017-03-01T00:00:00Z","doi":"10.1007/s11538-016-0244-3","year":"2017","publication":"Bulletin of Mathematical Biology","day":"01","oa":1,"quality_controlled":"1","publisher":"Springer","acknowledgement":"We thank Nick Barton, Katarína Bod’ová, and Sr\r\n-\r\ndan Sarikas for constructive feed-\r\nback and support. Furthermore, we would like to express our deep gratitude to the anonymous referees (one\r\nof whom, Jimmy Garnier, agreed to reveal his identity) and the editor Max Souza, for very helpful and\r\ndetailed comments and suggestions that significantly helped us to improve the manuscript. This project has\r\nreceived funding from the European Union’s Seventh Framework Programme for research, technological\r\ndevelopment and demonstration under Grant Agreement 618091 Speed of Adaptation in Population Genet-\r\nics and Evolutionary Computation (SAGE) and the European Research Council (ERC) Grant No. 250152\r\n(SN), from the Scientific Grant Agency of the Slovak Republic under the Grant 1/0459/13 and by the Slovak\r\nResearch and Development Agency under the Contract No. APVV-14-0378 (RK). RK would also like to\r\nthank IST Austria for its hospitality during the work on this project.","author":[{"full_name":"Kollár, Richard","last_name":"Kollár","first_name":"Richard"},{"first_name":"Sebastian","id":"461468AE-F248-11E8-B48F-1D18A9856A87","full_name":"Novak, Sebastian","last_name":"Novak"}],"publist_id":"6160","title":"Existence of traveling waves for the generalized F–KPP equation","citation":{"mla":"Kollár, Richard, and Sebastian Novak. “Existence of Traveling Waves for the Generalized F–KPP Equation.” Bulletin of Mathematical Biology, vol. 79, no. 3, Springer, 2017, pp. 525–59, doi:10.1007/s11538-016-0244-3.","ieee":"R. Kollár and S. Novak, “Existence of traveling waves for the generalized F–KPP equation,” Bulletin of Mathematical Biology, vol. 79, no. 3. Springer, pp. 525–559, 2017.","short":"R. Kollár, S. Novak, Bulletin of Mathematical Biology 79 (2017) 525–559.","apa":"Kollár, R., & Novak, S. (2017). Existence of traveling waves for the generalized F–KPP equation. Bulletin of Mathematical Biology. Springer. https://doi.org/10.1007/s11538-016-0244-3","ama":"Kollár R, Novak S. Existence of traveling waves for the generalized F–KPP equation. Bulletin of Mathematical Biology. 2017;79(3):525-559. doi:10.1007/s11538-016-0244-3","chicago":"Kollár, Richard, and Sebastian Novak. “Existence of Traveling Waves for the Generalized F–KPP Equation.” Bulletin of Mathematical Biology. Springer, 2017. https://doi.org/10.1007/s11538-016-0244-3.","ista":"Kollár R, Novak S. 2017. Existence of traveling waves for the generalized F–KPP equation. Bulletin of Mathematical Biology. 79(3), 525–559."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"25B1EC9E-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"618091","name":"Speed of Adaptation in Population Genetics and Evolutionary Computation"},{"_id":"25B07788-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"250152","name":"Limits to selection in biology and in evolutionary computation"}],"ec_funded":1,"volume":79,"issue":"3","publication_status":"published","language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1607.00944"}],"scopus_import":1,"intvolume":" 79","month":"03","abstract":[{"text":"Variation in genotypes may be responsible for differences in dispersal rates, directional biases, and growth rates of individuals. These traits may favor certain genotypes and enhance their spatiotemporal spreading into areas occupied by the less advantageous genotypes. We study how these factors influence the speed of spreading in the case of two competing genotypes under the assumption that spatial variation of the total population is small compared to the spatial variation of the frequencies of the genotypes in the population. In that case, the dynamics of the frequency of one of the genotypes is approximately described by a generalized Fisher–Kolmogorov–Petrovskii–Piskunov (F–KPP) equation. This generalized F–KPP equation with (nonlinear) frequency-dependent diffusion and advection terms admits traveling wave solutions that characterize the invasion of the dominant genotype. Our existence results generalize the classical theory for traveling waves for the F–KPP with constant coefficients. Moreover, in the particular case of the quadratic (monostable) nonlinear growth–decay rate in the generalized F–KPP we study in detail the influence of the variance in diffusion and mean displacement rates of the two genotypes on the minimal wave propagation speed.","lang":"eng"}],"oa_version":"Preprint","department":[{"_id":"NiBa"}],"date_updated":"2021-01-12T06:48:58Z","type":"journal_article","status":"public","_id":"1191"},{"date_updated":"2021-01-12T06:49:07Z","ddc":["530"],"file_date_updated":"2020-07-14T12:44:39Z","department":[{"_id":"BjHo"}],"_id":"1211","type":"journal_article","status":"public","pubrep_id":"782","publication_status":"published","file":[{"creator":"system","file_size":2820207,"date_updated":"2020-07-14T12:44:39Z","file_name":"IST-2017-782-v1+1_BudCvi15.pdf","date_created":"2018-12-12T10:18:01Z","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_id":"5319","checksum":"3e971d09eb167761aa0888ed415b0056"}],"language":[{"iso":"eng"}],"volume":167,"issue":"3-4","abstract":[{"text":"Systems such as fluid flows in channels and pipes or the complex Ginzburg–Landau system, defined over periodic domains, exhibit both continuous symmetries, translational and rotational, as well as discrete symmetries under spatial reflections or complex conjugation. The simplest, and very common symmetry of this type is the equivariance of the defining equations under the orthogonal group O(2). We formulate a novel symmetry reduction scheme for such systems by combining the method of slices with invariant polynomial methods, and show how it works by applying it to the Kuramoto–Sivashinsky system in one spatial dimension. As an example, we track a relative periodic orbit through a sequence of bifurcations to the onset of chaos. Within the symmetry-reduced state space we are able to compute and visualize the unstable manifolds of relative periodic orbits, their torus bifurcations, a transition to chaos via torus breakdown, and heteroclinic connections between various relative periodic orbits. It would be very hard to carry through such analysis in the full state space, without a symmetry reduction such as the one we present here.","lang":"eng"}],"oa_version":"Submitted Version","scopus_import":1,"month":"05","intvolume":" 167","citation":{"apa":"Budanur, N. B., & Cvitanović, P. (2017). Unstable manifolds of relative periodic orbits in the symmetry reduced state space of the Kuramoto–Sivashinsky system. Journal of Statistical Physics. Springer. https://doi.org/10.1007/s10955-016-1672-z","ama":"Budanur NB, Cvitanović P. Unstable manifolds of relative periodic orbits in the symmetry reduced state space of the Kuramoto–Sivashinsky system. Journal of Statistical Physics. 2017;167(3-4):636-655. doi:10.1007/s10955-016-1672-z","short":"N.B. Budanur, P. Cvitanović, Journal of Statistical Physics 167 (2017) 636–655.","ieee":"N. B. Budanur and P. Cvitanović, “Unstable manifolds of relative periodic orbits in the symmetry reduced state space of the Kuramoto–Sivashinsky system,” Journal of Statistical Physics, vol. 167, no. 3–4. Springer, pp. 636–655, 2017.","mla":"Budanur, Nazmi B., and Predrag Cvitanović. “Unstable Manifolds of Relative Periodic Orbits in the Symmetry Reduced State Space of the Kuramoto–Sivashinsky System.” Journal of Statistical Physics, vol. 167, no. 3–4, Springer, 2017, pp. 636–55, doi:10.1007/s10955-016-1672-z.","ista":"Budanur NB, Cvitanović P. 2017. Unstable manifolds of relative periodic orbits in the symmetry reduced state space of the Kuramoto–Sivashinsky system. Journal of Statistical Physics. 167(3–4), 636–655.","chicago":"Budanur, Nazmi B, and Predrag Cvitanović. “Unstable Manifolds of Relative Periodic Orbits in the Symmetry Reduced State Space of the Kuramoto–Sivashinsky System.” Journal of Statistical Physics. Springer, 2017. https://doi.org/10.1007/s10955-016-1672-z."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Budanur, Nazmi B","orcid":"0000-0003-0423-5010","last_name":"Budanur","first_name":"Nazmi B","id":"3EA1010E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Predrag","last_name":"Cvitanović","full_name":"Cvitanović, Predrag"}],"publist_id":"6136","title":"Unstable manifolds of relative periodic orbits in the symmetry reduced state space of the Kuramoto–Sivashinsky system","has_accepted_license":"1","year":"2017","day":"01","publication":"Journal of Statistical Physics","page":"636-655","doi":"10.1007/s10955-016-1672-z","date_published":"2017-05-01T00:00:00Z","date_created":"2018-12-11T11:50:44Z","acknowledgement":"This work was supported by the family of late G. Robinson, Jr. and NSF Grant DMS-1211827. ","quality_controlled":"1","publisher":"Springer","oa":1}]