[{"month":"01","publication_identifier":{"isbn":["978-331963386-2"]},"conference":{"start_date":"2017-07-24","location":"Heidelberg, Germany","end_date":"2017-07-28","name":"CAV: Computer Aided Verification"},"doi":"10.1007/978-3-319-63387-9_6","language":[{"iso":"eng"}],"main_file_link":[{"url":"https://arxiv.org/abs/1705.00314","open_access":"1"}],"oa":1,"quality_controlled":"1","project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"publist_id":"7166","ec_funded":1,"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Fu, Hongfei","last_name":"Fu","first_name":"Hongfei"},{"first_name":"Aniket","last_name":"Murhekar","full_name":"Murhekar, Aniket"}],"date_updated":"2021-01-12T08:06:55Z","date_created":"2018-12-11T11:47:35Z","volume":10426,"year":"2017","publication_status":"published","department":[{"_id":"KrCh"}],"publisher":"Springer","editor":[{"first_name":"Rupak","last_name":"Majumdar","full_name":"Majumdar, Rupak"},{"last_name":"Kunčak","first_name":"Viktor","full_name":"Kunčak, Viktor"}],"day":"01","scopus_import":1,"date_published":"2017-01-01T00:00:00Z","citation":{"mla":"Chatterjee, Krishnendu, et al. Automated Recurrence Analysis for Almost Linear Expected Runtime Bounds. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426, Springer, 2017, pp. 118–39, doi:10.1007/978-3-319-63387-9_6.","short":"K. Chatterjee, H. Fu, A. Murhekar, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 118–139.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Aniket Murhekar. “Automated Recurrence Analysis for Almost Linear Expected Runtime Bounds.” edited by Rupak Majumdar and Viktor Kunčak, 10426:118–39. Springer, 2017. https://doi.org/10.1007/978-3-319-63387-9_6.","ama":"Chatterjee K, Fu H, Murhekar A. Automated recurrence analysis for almost linear expected runtime bounds. In: Majumdar R, Kunčak V, eds. Vol 10426. Springer; 2017:118-139. doi:10.1007/978-3-319-63387-9_6","ista":"Chatterjee K, Fu H, Murhekar A. 2017. Automated recurrence analysis for almost linear expected runtime bounds. CAV: Computer Aided Verification, LNCS, vol. 10426, 118–139.","ieee":"K. Chatterjee, H. Fu, and A. Murhekar, “Automated recurrence analysis for almost linear expected runtime bounds,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10426, pp. 118–139.","apa":"Chatterjee, K., Fu, H., & Murhekar, A. (2017). Automated recurrence analysis for almost linear expected runtime bounds. In R. Majumdar & V. Kunčak (Eds.) (Vol. 10426, pp. 118–139). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63387-9_6"},"page":"118 - 139","abstract":[{"lang":"eng","text":"We consider the problem of developing automated techniques for solving recurrence relations to aid the expected-runtime analysis of programs. The motivation is that several classical textbook algorithms have quite efficient expected-runtime complexity, whereas the corresponding worst-case bounds are either inefficient (e.g., Quick-Sort), or completely ineffective (e.g., Coupon-Collector). Since the main focus of expected-runtime analysis is to obtain efficient bounds, we consider bounds that are either logarithmic, linear or almost-linear (O(log n), O(n), O(n · log n), respectively, where n represents the input size). Our main contribution is an efficient (simple linear-time algorithm) sound approach for deriving such expected-runtime bounds for the analysis of recurrence relations induced by randomized algorithms. The experimental results show that our approach can efficiently derive asymptotically optimal expected-runtime bounds for recurrences of classical randomized algorithms, including Randomized-Search, Quick-Sort, Quick-Select, Coupon-Collector, where the worst-case bounds are either inefficient (such as linear as compared to logarithmic expected-runtime complexity, or quadratic as compared to linear or almost-linear expected-runtime complexity), or ineffective."}],"type":"conference","alternative_title":["LNCS"],"oa_version":"Submitted Version","_id":"628","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","status":"public","title":"Automated recurrence analysis for almost linear expected runtime bounds","intvolume":" 10426"},{"scopus_import":1,"series_title":"Sub-Cellular Biochemistry","day":"13","publication":"Prokaryotic Cytoskeletons","citation":{"ista":"Loose M, Zieske K, Schwille P. 2017.Reconstitution of protein dynamics involved in bacterial cell division. In: Prokaryotic Cytoskeletons. vol. 84, 419–444.","ieee":"M. Loose, K. Zieske, and P. Schwille, “Reconstitution of protein dynamics involved in bacterial cell division,” in Prokaryotic Cytoskeletons, vol. 84, Springer, 2017, pp. 419–444.","apa":"Loose, M., Zieske, K., & Schwille, P. (2017). Reconstitution of protein dynamics involved in bacterial cell division. In Prokaryotic Cytoskeletons (Vol. 84, pp. 419–444). Springer. https://doi.org/10.1007/978-3-319-53047-5_15","ama":"Loose M, Zieske K, Schwille P. Reconstitution of protein dynamics involved in bacterial cell division. In: Prokaryotic Cytoskeletons. Vol 84. Sub-Cellular Biochemistry. Springer; 2017:419-444. doi:10.1007/978-3-319-53047-5_15","chicago":"Loose, Martin, Katja Zieske, and Petra Schwille. “Reconstitution of Protein Dynamics Involved in Bacterial Cell Division.” In Prokaryotic Cytoskeletons, 84:419–44. Sub-Cellular Biochemistry. Springer, 2017. https://doi.org/10.1007/978-3-319-53047-5_15.","mla":"Loose, Martin, et al. “Reconstitution of Protein Dynamics Involved in Bacterial Cell Division.” Prokaryotic Cytoskeletons, vol. 84, Springer, 2017, pp. 419–44, doi:10.1007/978-3-319-53047-5_15.","short":"M. Loose, K. Zieske, P. Schwille, in:, Prokaryotic Cytoskeletons, Springer, 2017, pp. 419–444."},"page":"419 - 444","date_published":"2017-05-13T00:00:00Z","type":"book_chapter","abstract":[{"text":"Even simple cells like bacteria have precisely regulated cellular anatomies, which allow them to grow, divide and to respond to internal or external cues with high fidelity. How spatial and temporal intracellular organization in prokaryotic cells is achieved and maintained on the basis of locally interacting proteins still remains largely a mystery. Bulk biochemical assays with purified components and in vivo experiments help us to approach key cellular processes from two opposite ends, in terms of minimal and maximal complexity. However, to understand how cellular phenomena emerge, that are more than the sum of their parts, we have to assemble cellular subsystems step by step from the bottom up. Here, we review recent in vitro reconstitution experiments with proteins of the bacterial cell division machinery and illustrate how they help to shed light on fundamental cellular mechanisms that constitute spatiotemporal order and regulate cell division.","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"629","title":"Reconstitution of protein dynamics involved in bacterial cell division","status":"public","intvolume":" 84","oa_version":"None","month":"05","publication_identifier":{"eisbn":["978-3-319-53047-5"]},"external_id":{"pmid":["28500535"]},"quality_controlled":"1","doi":"10.1007/978-3-319-53047-5_15","language":[{"iso":"eng"}],"publist_id":"7165","year":"2017","pmid":1,"publication_status":"published","publisher":"Springer","department":[{"_id":"MaLo"}],"author":[{"full_name":"Loose, Martin","last_name":"Loose","first_name":"Martin","orcid":"0000-0001-7309-9724","id":"462D4284-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Zieske, Katja","first_name":"Katja","last_name":"Zieske"},{"first_name":"Petra","last_name":"Schwille","full_name":"Schwille, Petra"}],"date_updated":"2021-01-12T08:06:57Z","date_created":"2018-12-11T11:47:35Z","volume":84},{"has_accepted_license":"1","day":"01","scopus_import":1,"date_published":"2017-01-01T00:00:00Z","citation":{"chicago":"Sauermann, Stefan, Veronika David, Alois Schlögl, Reinhard Egelkraut, Matthias Frohner, Birgit Pohn, Philipp Urbauer, and Alexander Mense. “Biosignals Standards and FHIR: The Way to Go,” 236:356–62. IOS Press, 2017. https://doi.org/10.3233/978-1-61499-759-7-356.","short":"S. Sauermann, V. David, A. Schlögl, R. Egelkraut, M. Frohner, B. Pohn, P. Urbauer, A. Mense, in:, IOS Press, 2017, pp. 356–362.","mla":"Sauermann, Stefan, et al. Biosignals Standards and FHIR: The Way to Go. Vol. 236, IOS Press, 2017, pp. 356–62, doi:10.3233/978-1-61499-759-7-356.","apa":"Sauermann, S., David, V., Schlögl, A., Egelkraut, R., Frohner, M., Pohn, B., … Mense, A. (2017). Biosignals standards and FHIR: The way to go (Vol. 236, pp. 356–362). Presented at the eHealth: Health Informatics Meets eHealth, Vienna, Austria: IOS Press. https://doi.org/10.3233/978-1-61499-759-7-356","ieee":"S. Sauermann et al., “Biosignals standards and FHIR: The way to go,” presented at the eHealth: Health Informatics Meets eHealth, Vienna, Austria, 2017, vol. 236, pp. 356–362.","ista":"Sauermann S, David V, Schlögl A, Egelkraut R, Frohner M, Pohn B, Urbauer P, Mense A. 2017. Biosignals standards and FHIR: The way to go. eHealth: Health Informatics Meets eHealth, Studies in Health Technology and Informatics, vol. 236, 356–362.","ama":"Sauermann S, David V, Schlögl A, et al. Biosignals standards and FHIR: The way to go. In: Vol 236. IOS Press; 2017:356-362. doi:10.3233/978-1-61499-759-7-356"},"page":"356 - 362","abstract":[{"text":"Background: Standards have become available to share semantically encoded vital parameters from medical devices, as required for example by personal healthcare records. Standardised sharing of biosignal data largely remains open. Objectives: The goal of this work is to explore available biosignal file format and data exchange standards and profiles, and to conceptualise end-To-end solutions. Methods: The authors reviewed and discussed available biosignal file format standards with other members of international standards development organisations (SDOs). Results: A raw concept for standards based acquisition, storage, archiving and sharing of biosignals was developed. The GDF format may serve for storing biosignals. Signals can then be shared using FHIR resources and may be stored on FHIR servers or in DICOM archives, with DICOM waveforms as one possible format. Conclusion: Currently a group of international SDOs (e.g. HL7, IHE, DICOM, IEEE) is engaged in intensive discussions. This discussion extends existing work that already was adopted by large implementer communities. The concept presented here only reports the current status of the discussion in Austria. The discussion will continue internationally, with results to be expected over the coming years.","lang":"eng"}],"type":"conference","alternative_title":["Studies in Health Technology and Informatics"],"pubrep_id":"906","oa_version":"Published Version","file":[{"access_level":"open_access","file_name":"IST-2017-906-v1+1_SHTI236-0356.pdf","creator":"system","content_type":"application/pdf","file_size":443635,"file_id":"4913","relation":"main_file","checksum":"1254dcc5b04a996d97fad9a726b42727","date_updated":"2020-07-14T12:47:27Z","date_created":"2018-12-12T10:11:56Z"}],"_id":"630","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 236","title":"Biosignals standards and FHIR: The way to go","status":"public","ddc":["005"],"publication_identifier":{"isbn":["978-161499758-0"]},"month":"01","doi":"10.3233/978-1-61499-759-7-356","conference":{"name":"eHealth: Health Informatics Meets eHealth","start_date":"2017-05-23","location":"Vienna, Austria","end_date":"2017-05-24"},"language":[{"iso":"eng"}],"oa":1,"tmp":{"name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode","image":"/images/cc_by_nc.png","short":"CC BY-NC (4.0)"},"quality_controlled":"1","publist_id":"7164","file_date_updated":"2020-07-14T12:47:27Z","license":"https://creativecommons.org/licenses/by-nc/4.0/","author":[{"full_name":"Sauermann, Stefan","last_name":"Sauermann","first_name":"Stefan"},{"full_name":"David, Veronika","first_name":"Veronika","last_name":"David"},{"orcid":"0000-0002-5621-8100","id":"45BF87EE-F248-11E8-B48F-1D18A9856A87","last_name":"Schlögl","first_name":"Alois","full_name":"Schlögl, Alois"},{"full_name":"Egelkraut, Reinhard","last_name":"Egelkraut","first_name":"Reinhard"},{"last_name":"Frohner","first_name":"Matthias","full_name":"Frohner, Matthias"},{"full_name":"Pohn, Birgit","first_name":"Birgit","last_name":"Pohn"},{"full_name":"Urbauer, Philipp","first_name":"Philipp","last_name":"Urbauer"},{"first_name":"Alexander","last_name":"Mense","full_name":"Mense, Alexander"}],"volume":236,"date_updated":"2021-01-12T08:06:59Z","date_created":"2018-12-11T11:47:36Z","year":"2017","department":[{"_id":"ScienComp"},{"_id":"PeJo"}],"publisher":"IOS Press","publication_status":"published"},{"doi":"10.1090/proc/13468","language":[{"iso":"eng"}],"main_file_link":[{"url":"https://arxiv.org/abs/1509.09045","open_access":"1"}],"oa":1,"quality_controlled":"1","project":[{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"}],"month":"01","author":[{"full_name":"Lewin, Mathieu","last_name":"Lewin","first_name":"Mathieu"},{"id":"404092F4-F248-11E8-B48F-1D18A9856A87","last_name":"Nam","first_name":"Phan","full_name":"Nam, Phan"},{"full_name":"Rougerie, Nicolas","last_name":"Rougerie","first_name":"Nicolas"}],"date_created":"2018-12-11T11:47:36Z","date_updated":"2021-01-12T08:07:03Z","volume":145,"year":"2017","publication_status":"published","department":[{"_id":"RoSe"}],"publisher":"American Mathematical Society","publist_id":"7160","ec_funded":1,"date_published":"2017-01-01T00:00:00Z","publication":"Proceedings of the American Mathematical Society","citation":{"chicago":"Lewin, Mathieu, Phan Nam, and Nicolas Rougerie. “A Note on 2D Focusing Many Boson Systems.” Proceedings of the American Mathematical Society. American Mathematical Society, 2017. https://doi.org/10.1090/proc/13468.","mla":"Lewin, Mathieu, et al. “A Note on 2D Focusing Many Boson Systems.” Proceedings of the American Mathematical Society, vol. 145, no. 6, American Mathematical Society, 2017, pp. 2441–54, doi:10.1090/proc/13468.","short":"M. Lewin, P. Nam, N. Rougerie, Proceedings of the American Mathematical Society 145 (2017) 2441–2454.","ista":"Lewin M, Nam P, Rougerie N. 2017. A note on 2D focusing many boson systems. Proceedings of the American Mathematical Society. 145(6), 2441–2454.","ieee":"M. Lewin, P. Nam, and N. Rougerie, “A note on 2D focusing many boson systems,” Proceedings of the American Mathematical Society, vol. 145, no. 6. American Mathematical Society, pp. 2441–2454, 2017.","apa":"Lewin, M., Nam, P., & Rougerie, N. (2017). A note on 2D focusing many boson systems. Proceedings of the American Mathematical Society. American Mathematical Society. https://doi.org/10.1090/proc/13468","ama":"Lewin M, Nam P, Rougerie N. A note on 2D focusing many boson systems. Proceedings of the American Mathematical Society. 2017;145(6):2441-2454. doi:10.1090/proc/13468"},"page":"2441 - 2454","day":"01","scopus_import":1,"oa_version":"Submitted Version","_id":"632","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","status":"public","title":"A note on 2D focusing many boson systems","intvolume":" 145","abstract":[{"lang":"eng","text":"We consider a 2D quantum system of N bosons in a trapping potential |x|s, interacting via a pair potential of the form N2β−1 w(Nβ x). We show that for all 0 < β < (s + 1)/(s + 2), the leading order behavior of ground states of the many-body system is described in the large N limit by the corresponding cubic nonlinear Schrödinger energy functional. Our result covers the focusing case (w < 0) where even the stability of the many-body system is not obvious. This answers an open question mentioned by X. Chen and J. Holmer for harmonic traps (s = 2). Together with the BBGKY hierarchy approach used by these authors, our result implies the convergence of the many-body quantum dynamics to the focusing NLS equation with harmonic trap for all 0 < β < 3/4. "}],"issue":"6","type":"journal_article"},{"volume":224,"date_created":"2018-12-11T11:47:37Z","date_updated":"2021-01-12T08:07:08Z","author":[{"full_name":"Schroeder, Jan","first_name":"Jan","last_name":"Schroeder"},{"full_name":"Deliu, Elena","first_name":"Elena","last_name":"Deliu","id":"37A40D7E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-7370-5293"},{"orcid":"0000-0002-7673-7178","id":"3E57A680-F248-11E8-B48F-1D18A9856A87","last_name":"Novarino","first_name":"Gaia","full_name":"Novarino, Gaia"},{"first_name":"Michael","last_name":"Schmeisser","full_name":"Schmeisser, Michael"}],"publisher":"Springer","department":[{"_id":"GaNo"}],"editor":[{"full_name":"Schmeisser, Michael","last_name":"Schmeisser","first_name":"Michael"},{"full_name":"Boekers, Tobias","last_name":"Boekers","first_name":"Tobias"}],"publication_status":"published","year":"2017","publist_id":"7156","language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-52498-6_10","project":[{"grant_number":"F03523","_id":"25473368-B435-11E9-9278-68D0E5697425","name":"Transmembrane Transporters in Health and Disease","call_identifier":"FWF"}],"quality_controlled":"1","publication_identifier":{"eisbn":["978-3-319-52498-6"]},"month":"05","oa_version":"None","intvolume":" 224","title":"Genetic and pharmacological reversibility of phenotypes in mouse models of autism spectrum disorder","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"634","abstract":[{"text":"As autism spectrum disorder (ASD) is largely regarded as a neurodevelopmental condition, long-time consensus was that its hallmark features are irreversible. However, several studies from recent years using defined mouse models of ASD have provided clear evidence that in mice neurobiological and behavioural alterations can be ameliorated or even reversed by genetic restoration or pharmacological treatment either before or after symptom onset. Here, we review findings on genetic and pharmacological reversibility of phenotypes in mouse models of ASD. Our review should give a comprehensive overview on both aspects and encourage future studies to better understand the underlying molecular mechanisms that might be translatable from animals to humans.","lang":"eng"}],"alternative_title":["ADVSANAT"],"type":"book_chapter","date_published":"2017-05-28T00:00:00Z","page":"189 - 211","citation":{"apa":"Schroeder, J., Deliu, E., Novarino, G., & Schmeisser, M. (2017). Genetic and pharmacological reversibility of phenotypes in mouse models of autism spectrum disorder. In M. Schmeisser & T. Boekers (Eds.), Translational Anatomy and Cell Biology of Autism Spectrum Disorder (Vol. 224, pp. 189–211). Springer. https://doi.org/10.1007/978-3-319-52498-6_10","ieee":"J. Schroeder, E. Deliu, G. Novarino, and M. Schmeisser, “Genetic and pharmacological reversibility of phenotypes in mouse models of autism spectrum disorder,” in Translational Anatomy and Cell Biology of Autism Spectrum Disorder, vol. 224, M. Schmeisser and T. Boekers, Eds. Springer, 2017, pp. 189–211.","ista":"Schroeder J, Deliu E, Novarino G, Schmeisser M. 2017.Genetic and pharmacological reversibility of phenotypes in mouse models of autism spectrum disorder. In: Translational Anatomy and Cell Biology of Autism Spectrum Disorder. ADVSANAT, vol. 224, 189–211.","ama":"Schroeder J, Deliu E, Novarino G, Schmeisser M. Genetic and pharmacological reversibility of phenotypes in mouse models of autism spectrum disorder. In: Schmeisser M, Boekers T, eds. Translational Anatomy and Cell Biology of Autism Spectrum Disorder. Vol 224. Advances in Anatomy Embryology and Cell Biology. Springer; 2017:189-211. doi:10.1007/978-3-319-52498-6_10","chicago":"Schroeder, Jan, Elena Deliu, Gaia Novarino, and Michael Schmeisser. “Genetic and Pharmacological Reversibility of Phenotypes in Mouse Models of Autism Spectrum Disorder.” In Translational Anatomy and Cell Biology of Autism Spectrum Disorder, edited by Michael Schmeisser and Tobias Boekers, 224:189–211. Advances in Anatomy Embryology and Cell Biology. Springer, 2017. https://doi.org/10.1007/978-3-319-52498-6_10.","short":"J. Schroeder, E. Deliu, G. Novarino, M. Schmeisser, in:, M. Schmeisser, T. Boekers (Eds.), Translational Anatomy and Cell Biology of Autism Spectrum Disorder, Springer, 2017, pp. 189–211.","mla":"Schroeder, Jan, et al. “Genetic and Pharmacological Reversibility of Phenotypes in Mouse Models of Autism Spectrum Disorder.” Translational Anatomy and Cell Biology of Autism Spectrum Disorder, edited by Michael Schmeisser and Tobias Boekers, vol. 224, Springer, 2017, pp. 189–211, doi:10.1007/978-3-319-52498-6_10."},"publication":"Translational Anatomy and Cell Biology of Autism Spectrum Disorder","day":"28","series_title":"Advances in Anatomy Embryology and Cell Biology","scopus_import":1},{"citation":{"mla":"Bak, Stanley, et al. Challenges and Tool Implementation of Hybrid Rapidly Exploring Random Trees. Edited by Alessandro Abate and Sylvie Bodo, vol. 10381, Springer, 2017, pp. 83–89, doi:10.1007/978-3-319-63501-9_6.","short":"S. Bak, S. Bogomolov, T.A. Henzinger, A. Kumar, in:, A. Abate, S. Bodo (Eds.), Springer, 2017, pp. 83–89.","chicago":"Bak, Stanley, Sergiy Bogomolov, Thomas A Henzinger, and Aviral Kumar. “Challenges and Tool Implementation of Hybrid Rapidly Exploring Random Trees.” edited by Alessandro Abate and Sylvie Bodo, 10381:83–89. Springer, 2017. https://doi.org/10.1007/978-3-319-63501-9_6.","ama":"Bak S, Bogomolov S, Henzinger TA, Kumar A. Challenges and tool implementation of hybrid rapidly exploring random trees. In: Abate A, Bodo S, eds. Vol 10381. Springer; 2017:83-89. doi:10.1007/978-3-319-63501-9_6","ista":"Bak S, Bogomolov S, Henzinger TA, Kumar A. 2017. Challenges and tool implementation of hybrid rapidly exploring random trees. NSV: Numerical Software Verification, LNCS, vol. 10381, 83–89.","ieee":"S. Bak, S. Bogomolov, T. A. Henzinger, and A. Kumar, “Challenges and tool implementation of hybrid rapidly exploring random trees,” presented at the NSV: Numerical Software Verification, Heidelberg, Germany, 2017, vol. 10381, pp. 83–89.","apa":"Bak, S., Bogomolov, S., Henzinger, T. A., & Kumar, A. (2017). Challenges and tool implementation of hybrid rapidly exploring random trees. In A. Abate & S. Bodo (Eds.) (Vol. 10381, pp. 83–89). Presented at the NSV: Numerical Software Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63501-9_6"},"page":"83 - 89","date_published":"2017-01-01T00:00:00Z","scopus_import":1,"day":"01","_id":"633","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":" 10381","title":"Challenges and tool implementation of hybrid rapidly exploring random trees","status":"public","oa_version":"None","type":"conference","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"A Rapidly-exploring Random Tree (RRT) is an algorithm which can search a non-convex region of space by incrementally building a space-filling tree. The tree is constructed from random points drawn from system’s state space and is biased to grow towards large unexplored areas in the system. RRT can provide better coverage of a system’s possible behaviors compared with random simulations, but is more lightweight than full reachability analysis. In this paper, we explore some of the design decisions encountered while implementing a hybrid extension of the RRT algorithm, which have not been elaborated on before. In particular, we focus on handling non-determinism, which arises due to discrete transitions. We introduce the notion of important points to account for this phenomena. We showcase our ideas using heater and navigation benchmarks."}],"project":[{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","doi":"10.1007/978-3-319-63501-9_6","conference":{"start_date":"2017-07-22","location":"Heidelberg, Germany","end_date":"2017-07-23","name":"NSV: Numerical Software Verification"},"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-331963500-2"]},"month":"01","year":"2017","publisher":"Springer","editor":[{"last_name":"Abate","first_name":"Alessandro","full_name":"Abate, Alessandro"},{"first_name":"Sylvie","last_name":"Bodo","full_name":"Bodo, Sylvie"}],"department":[{"_id":"ToHe"}],"publication_status":"published","author":[{"full_name":"Bak, Stanley","first_name":"Stanley","last_name":"Bak"},{"full_name":"Bogomolov, Sergiy","last_name":"Bogomolov","first_name":"Sergiy","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Kumar, Aviral","last_name":"Kumar","first_name":"Aviral"}],"volume":10381,"date_created":"2018-12-11T11:47:37Z","date_updated":"2021-01-12T08:07:06Z","publist_id":"7159"},{"publication_identifier":{"isbn":["978-331956616-0"]},"month":"01","oa":1,"main_file_link":[{"open_access":"1","url":"https://eprint.iacr.org/2016/989"}],"project":[{"name":"Teaching Old Crypto New Tricks","call_identifier":"H2020","grant_number":"682815","_id":"258AA5B2-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","doi":"10.1007/978-3-319-56617-7_2","conference":{"name":"EUROCRYPT: Theory and Applications of Cryptographic Techniques","end_date":"2017-05-04","location":"Paris, France","start_date":"2017-04-30"},"language":[{"iso":"eng"}],"ec_funded":1,"publist_id":"7154","year":"2017","publisher":"Springer","editor":[{"full_name":"Coron, Jean-Sébastien","first_name":"Jean-Sébastien","last_name":"Coron"},{"last_name":"Buus Nielsen","first_name":"Jesper","full_name":"Buus Nielsen, Jesper"}],"department":[{"_id":"KrPi"}],"publication_status":"published","author":[{"full_name":"Alwen, Joel F","last_name":"Alwen","first_name":"Joel F","id":"2A8DFA8C-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Chen, Binchi","first_name":"Binchi","last_name":"Chen"},{"full_name":"Pietrzak, Krzysztof Z","last_name":"Pietrzak","first_name":"Krzysztof Z","orcid":"0000-0002-9139-1654","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Reyzin, Leonid","first_name":"Leonid","last_name":"Reyzin"},{"full_name":"Tessaro, Stefano","last_name":"Tessaro","first_name":"Stefano"}],"volume":10212,"date_created":"2018-12-11T11:47:37Z","date_updated":"2021-01-12T08:07:10Z","scopus_import":1,"day":"01","citation":{"mla":"Alwen, Joel F., et al. Scrypt Is Maximally Memory Hard. Edited by Jean-Sébastien Coron and Jesper Buus Nielsen, vol. 10212, Springer, 2017, pp. 33–62, doi:10.1007/978-3-319-56617-7_2.","short":"J.F. Alwen, B. Chen, K.Z. Pietrzak, L. Reyzin, S. Tessaro, in:, J.-S. Coron, J. Buus Nielsen (Eds.), Springer, 2017, pp. 33–62.","chicago":"Alwen, Joel F, Binchi Chen, Krzysztof Z Pietrzak, Leonid Reyzin, and Stefano Tessaro. “Scrypt Is Maximally Memory Hard.” edited by Jean-Sébastien Coron and Jesper Buus Nielsen, 10212:33–62. Springer, 2017. https://doi.org/10.1007/978-3-319-56617-7_2.","ama":"Alwen JF, Chen B, Pietrzak KZ, Reyzin L, Tessaro S. Scrypt is maximally memory hard. In: Coron J-S, Buus Nielsen J, eds. Vol 10212. Springer; 2017:33-62. doi:10.1007/978-3-319-56617-7_2","ista":"Alwen JF, Chen B, Pietrzak KZ, Reyzin L, Tessaro S. 2017. Scrypt is maximally memory hard. EUROCRYPT: Theory and Applications of Cryptographic Techniques, LNCS, vol. 10212, 33–62.","ieee":"J. F. Alwen, B. Chen, K. Z. Pietrzak, L. Reyzin, and S. Tessaro, “Scrypt is maximally memory hard,” presented at the EUROCRYPT: Theory and Applications of Cryptographic Techniques, Paris, France, 2017, vol. 10212, pp. 33–62.","apa":"Alwen, J. F., Chen, B., Pietrzak, K. Z., Reyzin, L., & Tessaro, S. (2017). Scrypt is maximally memory hard. In J.-S. Coron & J. Buus Nielsen (Eds.) (Vol. 10212, pp. 33–62). Presented at the EUROCRYPT: Theory and Applications of Cryptographic Techniques, Paris, France: Springer. https://doi.org/10.1007/978-3-319-56617-7_2"},"page":"33 - 62","date_published":"2017-01-01T00:00:00Z","type":"conference","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"Memory-hard functions (MHFs) are hash algorithms whose evaluation cost is dominated by memory cost. As memory, unlike computation, costs about the same across different platforms, MHFs cannot be evaluated at significantly lower cost on dedicated hardware like ASICs. MHFs have found widespread applications including password hashing, key derivation, and proofs-of-work. This paper focuses on scrypt, a simple candidate MHF designed by Percival, and described in RFC 7914. It has been used within a number of cryptocurrencies (e.g., Litecoin and Dogecoin) and has been an inspiration for Argon2d, one of the winners of the recent password-hashing competition. Despite its popularity, no rigorous lower bounds on its memory complexity are known. We prove that scrypt is optimally memory-hard, i.e., its cumulative memory complexity (cmc) in the parallel random oracle model is Ω(n2w), where w and n are the output length and number of invocations of the underlying hash function, respectively. High cmc is a strong security target for MHFs introduced by Alwen and Serbinenko (STOC’15) which implies high memory cost even for adversaries who can amortize the cost over many evaluations and evaluate the underlying hash functions many times in parallel. Our proof is the first showing optimal memory-hardness for any MHF. Our result improves both quantitatively and qualitatively upon the recent work by Alwen et al. (EUROCRYPT’16) who proved a weaker lower bound of Ω(n2w/ log2 n) for a restricted class of adversaries."}],"_id":"635","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","intvolume":" 10212","title":"Scrypt is maximally memory hard","status":"public","oa_version":"Submitted Version"},{"citation":{"chicago":"Bakhirkin, Alexey, Thomas Ferrere, Oded Maler, and Dogan Ulus. “On the Quantitative Semantics of Regular Expressions over Real-Valued Signals.” edited by Alessandro Abate and Gilles Geeraerts, 10419:189–206. Springer, 2017. https://doi.org/10.1007/978-3-319-65765-3_11.","mla":"Bakhirkin, Alexey, et al. On the Quantitative Semantics of Regular Expressions over Real-Valued Signals. Edited by Alessandro Abate and Gilles Geeraerts, vol. 10419, Springer, 2017, pp. 189–206, doi:10.1007/978-3-319-65765-3_11.","short":"A. Bakhirkin, T. Ferrere, O. Maler, D. Ulus, in:, A. Abate, G. Geeraerts (Eds.), Springer, 2017, pp. 189–206.","ista":"Bakhirkin A, Ferrere T, Maler O, Ulus D. 2017. On the quantitative semantics of regular expressions over real-valued signals. FORMATS: Formal Modelling and Analysis of Timed Systems, LNCS, vol. 10419, 189–206.","apa":"Bakhirkin, A., Ferrere, T., Maler, O., & Ulus, D. (2017). On the quantitative semantics of regular expressions over real-valued signals. In A. Abate & G. Geeraerts (Eds.) (Vol. 10419, pp. 189–206). Presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany: Springer. https://doi.org/10.1007/978-3-319-65765-3_11","ieee":"A. Bakhirkin, T. Ferrere, O. Maler, and D. Ulus, “On the quantitative semantics of regular expressions over real-valued signals,” presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany, 2017, vol. 10419, pp. 189–206.","ama":"Bakhirkin A, Ferrere T, Maler O, Ulus D. On the quantitative semantics of regular expressions over real-valued signals. In: Abate A, Geeraerts G, eds. Vol 10419. Springer; 2017:189-206. doi:10.1007/978-3-319-65765-3_11"},"page":"189 - 206","date_published":"2017-08-03T00:00:00Z","scopus_import":1,"day":"03","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"636","intvolume":" 10419","status":"public","title":"On the quantitative semantics of regular expressions over real-valued signals","oa_version":"Submitted Version","type":"conference","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"Signal regular expressions can specify sequential properties of real-valued signals based on threshold conditions, regular operations, and duration constraints. In this paper we endow them with a quantitative semantics which indicates how robustly a signal matches or does not match a given expression. First, we show that this semantics is a safe approximation of a distance between the signal and the language defined by the expression. Then, we consider the robust matching problem, that is, computing the quantitative semantics of every segment of a given signal relative to an expression. We present an algorithm that solves this problem for piecewise-constant and piecewise-linear signals and show that for such signals the robustness map is a piecewise-linear function. The availability of an indicator describing how robustly a signal segment matches some regular pattern provides a general framework for quantitative monitoring of cyber-physical systems."}],"oa":1,"main_file_link":[{"open_access":"1","url":"https://hal.archives-ouvertes.fr/hal-01552132"}],"project":[{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"quality_controlled":"1","doi":"10.1007/978-3-319-65765-3_11","conference":{"name":"FORMATS: Formal Modelling and Analysis of Timed Systems","end_date":"2017-09-07","start_date":"2017-09-05","location":"Berlin, Germany"},"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-331965764-6"]},"month":"08","year":"2017","publisher":"Springer","department":[{"_id":"ToHe"}],"editor":[{"last_name":"Abate","first_name":"Alessandro","full_name":"Abate, Alessandro"},{"first_name":"Gilles","last_name":"Geeraerts","full_name":"Geeraerts, Gilles"}],"publication_status":"published","author":[{"full_name":"Bakhirkin, Alexey","last_name":"Bakhirkin","first_name":"Alexey"},{"full_name":"Ferrere, Thomas","last_name":"Ferrere","first_name":"Thomas","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Maler","first_name":"Oded","full_name":"Maler, Oded"},{"first_name":"Dogan","last_name":"Ulus","full_name":"Ulus, Dogan"}],"volume":10419,"date_updated":"2021-01-12T08:07:14Z","date_created":"2018-12-11T11:47:38Z","publist_id":"7152"},{"abstract":[{"lang":"eng","text":"This book constitutes the refereed proceedings of the 9th InternationalWorkshop on Numerical Software Verification, NSV 2016, held in Toronto, ON, Canada in July 2011 - colocated with CAV 2016, the 28th International Conference on Computer Aided Verification.\r\nThe NSV workshop is dedicated to the development of logical and mathematical techniques for the reasoning about programmability and reliability."}],"publist_id":"7150","type":"conference_editor","date_updated":"2022-05-24T07:09:52Z","date_created":"2018-12-11T11:47:38Z","oa_version":"None","volume":10152,"_id":"638","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2017","publication_status":"published","status":"public","title":"Numerical Software Verification","editor":[{"full_name":"Bogomolov, Sergiy","first_name":"Sergiy","last_name":"Bogomolov","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365"},{"full_name":"Martel, Matthieu","first_name":"Matthieu","last_name":"Martel"},{"full_name":"Prabhakar, Pavithra","last_name":"Prabhakar","first_name":"Pavithra"}],"intvolume":" 10152","publisher":"Springer","department":[{"_id":"ToHe"}],"month":"01","day":"01","publication_identifier":{"eisbn":["978-3-319-54292-8"],"issn":["0302-9743"]},"article_processing_charge":"No","series_title":"LNCS","conference":{"start_date":"2016-07-17","location":"Toronto, ON, Canada","end_date":"2016-07-18","name":"NSV: Numerical Software Verification"},"doi":"10.1007/978-3-319-54292-8","date_published":"2017-01-01T00:00:00Z","language":[{"iso":"eng"}],"citation":{"mla":"Bogomolov, Sergiy, et al., editors. Numerical Software Verification. Vol. 10152, Springer, 2017, doi:10.1007/978-3-319-54292-8.","short":"S. Bogomolov, M. Martel, P. Prabhakar, eds., Numerical Software Verification, Springer, 2017.","chicago":"Bogomolov, Sergiy, Matthieu Martel, and Pavithra Prabhakar, eds. Numerical Software Verification. Vol. 10152. LNCS. Springer, 2017. https://doi.org/10.1007/978-3-319-54292-8.","ama":"Bogomolov S, Martel M, Prabhakar P, eds. Numerical Software Verification. Vol 10152. Springer; 2017. doi:10.1007/978-3-319-54292-8","ista":"Bogomolov S, Martel M, Prabhakar P eds. 2017. Numerical Software Verification, Springer,p.","apa":"Bogomolov, S., Martel, M., & Prabhakar, P. (Eds.). (2017). Numerical Software Verification (Vol. 10152). Presented at the NSV: Numerical Software Verification, Toronto, ON, Canada: Springer. https://doi.org/10.1007/978-3-319-54292-8","ieee":"S. Bogomolov, M. Martel, and P. Prabhakar, Eds., Numerical Software Verification, vol. 10152. Springer, 2017."},"quality_controlled":"1"},{"year":"2017","publication_status":"published","department":[{"_id":"KrPi"}],"publisher":"Springer","editor":[{"full_name":"Coron, Jean-Sébastien","last_name":"Coron","first_name":"Jean-Sébastien"},{"full_name":"Buus Nielsen, Jesper","first_name":"Jesper","last_name":"Buus Nielsen"}],"author":[{"last_name":"Alwen","first_name":"Joel F","id":"2A8DFA8C-F248-11E8-B48F-1D18A9856A87","full_name":"Alwen, Joel F"},{"first_name":"Jeremiah","last_name":"Blocki","full_name":"Blocki, Jeremiah"},{"full_name":"Pietrzak, Krzysztof Z","last_name":"Pietrzak","first_name":"Krzysztof Z","orcid":"0000-0002-9139-1654","id":"3E04A7AA-F248-11E8-B48F-1D18A9856A87"}],"date_created":"2018-12-11T11:47:39Z","date_updated":"2021-01-12T08:07:22Z","volume":10212,"publist_id":"7148","ec_funded":1,"main_file_link":[{"open_access":"1","url":"https://eprint.iacr.org/2016/875"}],"oa":1,"quality_controlled":"1","project":[{"call_identifier":"H2020","name":"Teaching Old Crypto New Tricks","_id":"258AA5B2-B435-11E9-9278-68D0E5697425","grant_number":"682815"}],"conference":{"end_date":"2017-05-04","location":"Paris, France","start_date":"2017-04-30","name":"EUROCRYPT: Theory and Applications of Cryptographic Techniques"},"doi":"10.1007/978-3-319-56617-7_1","language":[{"iso":"eng"}],"month":"04","publication_identifier":{"isbn":["978-331956616-0"]},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"640","title":"Depth-robust graphs and their cumulative memory complexity","status":"public","intvolume":" 10212","oa_version":"Submitted Version","type":"conference","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"Data-independent Memory Hard Functions (iMHFS) are finding a growing number of applications in security; especially in the domain of password hashing. An important property of a concrete iMHF is specified by fixing a directed acyclic graph (DAG) Gn on n nodes. The quality of that iMHF is then captured by the following two pebbling complexities of Gn: – The parallel cumulative pebbling complexity Π∥cc(Gn) must be as high as possible (to ensure that the amortized cost of computing the function on dedicated hardware is dominated by the cost of memory). – The sequential space-time pebbling complexity Πst(Gn) should be as close as possible to Π∥cc(Gn) (to ensure that using many cores in parallel and amortizing over many instances does not give much of an advantage). In this paper we construct a family of DAGs with best possible parameters in an asymptotic sense, i.e., where Π∥cc(Gn) = Ω(n2/ log(n)) (which matches a known upper bound) and Πst(Gn) is within a constant factor of Π∥cc(Gn). Our analysis relies on a new connection between the pebbling complexity of a DAG and its depth-robustness (DR) – a well studied combinatorial property. We show that high DR is sufficient for high Π∥cc. Alwen and Blocki (CRYPTO’16) showed that high DR is necessary and so, together, these results fully characterize DAGs with high Π∥cc in terms of DR. Complementing these results, we provide new upper and lower bounds on the Π∥cc of several important candidate iMHFs from the literature. We give the first lower bounds on the memory hardness of the Catena and Balloon Hashing functions in a parallel model of computation and we give the first lower bounds of any kind for (a version) of Argon2i. Finally we describe a new class of pebbling attacks improving on those of Alwen and Blocki (CRYPTO’16). By instantiating these attacks we upperbound the Π∥cc of the Password Hashing Competition winner Argon2i and one of the Balloon Hashing functions by O (n1.71). We also show an upper bound of O(n1.625) for the Catena functions and the two remaining Balloon Hashing functions."}],"citation":{"ama":"Alwen JF, Blocki J, Pietrzak KZ. Depth-robust graphs and their cumulative memory complexity. In: Coron J-S, Buus Nielsen J, eds. Vol 10212. Springer; 2017:3-32. doi:10.1007/978-3-319-56617-7_1","ista":"Alwen JF, Blocki J, Pietrzak KZ. 2017. Depth-robust graphs and their cumulative memory complexity. EUROCRYPT: Theory and Applications of Cryptographic Techniques, LNCS, vol. 10212, 3–32.","ieee":"J. F. Alwen, J. Blocki, and K. Z. Pietrzak, “Depth-robust graphs and their cumulative memory complexity,” presented at the EUROCRYPT: Theory and Applications of Cryptographic Techniques, Paris, France, 2017, vol. 10212, pp. 3–32.","apa":"Alwen, J. F., Blocki, J., & Pietrzak, K. Z. (2017). Depth-robust graphs and their cumulative memory complexity. In J.-S. Coron & J. Buus Nielsen (Eds.) (Vol. 10212, pp. 3–32). Presented at the EUROCRYPT: Theory and Applications of Cryptographic Techniques, Paris, France: Springer. https://doi.org/10.1007/978-3-319-56617-7_1","mla":"Alwen, Joel F., et al. Depth-Robust Graphs and Their Cumulative Memory Complexity. Edited by Jean-Sébastien Coron and Jesper Buus Nielsen, vol. 10212, Springer, 2017, pp. 3–32, doi:10.1007/978-3-319-56617-7_1.","short":"J.F. Alwen, J. Blocki, K.Z. Pietrzak, in:, J.-S. Coron, J. Buus Nielsen (Eds.), Springer, 2017, pp. 3–32.","chicago":"Alwen, Joel F, Jeremiah Blocki, and Krzysztof Z Pietrzak. “Depth-Robust Graphs and Their Cumulative Memory Complexity.” edited by Jean-Sébastien Coron and Jesper Buus Nielsen, 10212:3–32. Springer, 2017. https://doi.org/10.1007/978-3-319-56617-7_1."},"page":"3 - 32","date_published":"2017-04-01T00:00:00Z","scopus_import":1,"day":"01"}]