--- _id: '160' abstract: - lang: eng text: We present layered concurrent programs, a compact and expressive notation for specifying refinement proofs of concurrent programs. A layered concurrent program specifies a sequence of connected concurrent programs, from most concrete to most abstract, such that common parts of different programs are written exactly once. These programs are expressed in the ordinary syntax of imperative concurrent programs using gated atomic actions, sequencing, choice, and (recursive) procedure calls. Each concurrent program is automatically extracted from the layered program. We reduce refinement to the safety of a sequence of concurrent checker programs, one each to justify the connection between every two consecutive concurrent programs. These checker programs are also automatically extracted from the layered program. Layered concurrent programs have been implemented in the CIVL verifier which has been successfully used for the verification of several complex concurrent programs. alternative_title: - LNCS article_processing_charge: No author: - first_name: Bernhard full_name: Kragl, Bernhard id: 320FC952-F248-11E8-B48F-1D18A9856A87 last_name: Kragl orcid: 0000-0001-7745-9117 - first_name: Shaz full_name: Qadeer, Shaz last_name: Qadeer citation: ama: 'Kragl B, Qadeer S. Layered Concurrent Programs. In: Vol 10981. Springer; 2018:79-102. doi:10.1007/978-3-319-96145-3_5' apa: 'Kragl, B., & Qadeer, S. (2018). Layered Concurrent Programs (Vol. 10981, pp. 79–102). Presented at the CAV: Computer Aided Verification, Oxford, UK: Springer. https://doi.org/10.1007/978-3-319-96145-3_5' chicago: Kragl, Bernhard, and Shaz Qadeer. “Layered Concurrent Programs,” 10981:79–102. Springer, 2018. https://doi.org/10.1007/978-3-319-96145-3_5. ieee: 'B. Kragl and S. Qadeer, “Layered Concurrent Programs,” presented at the CAV: Computer Aided Verification, Oxford, UK, 2018, vol. 10981, pp. 79–102.' ista: 'Kragl B, Qadeer S. 2018. Layered Concurrent Programs. CAV: Computer Aided Verification, LNCS, vol. 10981, 79–102.' mla: Kragl, Bernhard, and Shaz Qadeer. Layered Concurrent Programs. Vol. 10981, Springer, 2018, pp. 79–102, doi:10.1007/978-3-319-96145-3_5. short: B. Kragl, S. Qadeer, in:, Springer, 2018, pp. 79–102. conference: end_date: 2018-07-17 location: Oxford, UK name: 'CAV: Computer Aided Verification' start_date: 2018-07-14 date_created: 2018-12-11T11:44:57Z date_published: 2018-07-18T00:00:00Z date_updated: 2023-09-13T08:45:09Z day: '18' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-319-96145-3_5 external_id: isi: - '000491481600005' file: - access_level: open_access checksum: c64fff560fe5a7532ec10626ad1c215e content_type: application/pdf creator: dernst date_created: 2018-12-17T12:52:12Z date_updated: 2020-07-14T12:45:04Z file_id: '5705' file_name: 2018_LNCS_Kragl.pdf file_size: 1603844 relation: main_file file_date_updated: 2020-07-14T12:45:04Z has_accepted_license: '1' intvolume: ' 10981' isi: 1 language: - iso: eng license: https://creativecommons.org/licenses/by/4.0/ month: '07' oa: 1 oa_version: Published Version page: 79 - 102 project: - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication_status: published publisher: Springer publist_id: '7761' quality_controlled: '1' related_material: record: - id: '8332' relation: dissertation_contains status: public scopus_import: '1' status: public title: Layered Concurrent Programs tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 10981 year: '2018' ... --- _id: '82' abstract: - lang: eng text: In experimental cultures, when bacteria are mixed with lytic (virulent) bacteriophage, bacterial cells resistant to the phage commonly emerge and become the dominant population of bacteria. Following the ascent of resistant mutants, the densities of bacteria in these simple communities become limited by resources rather than the phage. Despite the evolution of resistant hosts, upon which the phage cannot replicate, the lytic phage population is most commonly maintained in an apparently stable state with the resistant bacteria. Several mechanisms have been put forward to account for this result. Here we report the results of population dynamic/evolution experiments with a virulent mutant of phage Lambda, λVIR, and Escherichia coli in serial transfer cultures. We show that, following the ascent of λVIR-resistant bacteria, λVIRis maintained in the majority of cases in maltose-limited minimal media and in all cases in nutrient-rich broth. Using mathematical models and experiments, we show that the dominant mechanism responsible for maintenance of λVIRin these resource-limited populations dominated by resistant E. coli is a high rate of either phenotypic or genetic transition from resistance to susceptibility—a hitherto undemonstrated mechanism we term "leaky resistance." We discuss the implications of leaky resistance to our understanding of the conditions for the maintenance of phage in populations of bacteria—their “existence conditions.”. article_number: '2005971' article_processing_charge: Yes author: - first_name: Waqas full_name: Chaudhry, Waqas last_name: Chaudhry - first_name: Maros full_name: Pleska, Maros id: 4569785E-F248-11E8-B48F-1D18A9856A87 last_name: Pleska orcid: 0000-0001-7460-7479 - first_name: Nilang full_name: Shah, Nilang last_name: Shah - first_name: Howard full_name: Weiss, Howard last_name: Weiss - first_name: Ingrid full_name: Mccall, Ingrid last_name: Mccall - first_name: Justin full_name: Meyer, Justin last_name: Meyer - first_name: Animesh full_name: Gupta, Animesh last_name: Gupta - first_name: Calin C full_name: Guet, Calin C id: 47F8433E-F248-11E8-B48F-1D18A9856A87 last_name: Guet orcid: 0000-0001-6220-2052 - first_name: Bruce full_name: Levin, Bruce last_name: Levin citation: ama: Chaudhry W, Pleska M, Shah N, et al. Leaky resistance and the conditions for the existence of lytic bacteriophage. PLoS Biology. 2018;16(8). doi:10.1371/journal.pbio.2005971 apa: Chaudhry, W., Pleska, M., Shah, N., Weiss, H., Mccall, I., Meyer, J., … Levin, B. (2018). Leaky resistance and the conditions for the existence of lytic bacteriophage. PLoS Biology. Public Library of Science. https://doi.org/10.1371/journal.pbio.2005971 chicago: Chaudhry, Waqas, Maros Pleska, Nilang Shah, Howard Weiss, Ingrid Mccall, Justin Meyer, Animesh Gupta, Calin C Guet, and Bruce Levin. “Leaky Resistance and the Conditions for the Existence of Lytic Bacteriophage.” PLoS Biology. Public Library of Science, 2018. https://doi.org/10.1371/journal.pbio.2005971. ieee: W. Chaudhry et al., “Leaky resistance and the conditions for the existence of lytic bacteriophage,” PLoS Biology, vol. 16, no. 8. Public Library of Science, 2018. ista: Chaudhry W, Pleska M, Shah N, Weiss H, Mccall I, Meyer J, Gupta A, Guet CC, Levin B. 2018. Leaky resistance and the conditions for the existence of lytic bacteriophage. PLoS Biology. 16(8), 2005971. mla: Chaudhry, Waqas, et al. “Leaky Resistance and the Conditions for the Existence of Lytic Bacteriophage.” PLoS Biology, vol. 16, no. 8, 2005971, Public Library of Science, 2018, doi:10.1371/journal.pbio.2005971. short: W. Chaudhry, M. Pleska, N. Shah, H. Weiss, I. Mccall, J. Meyer, A. Gupta, C.C. Guet, B. Levin, PLoS Biology 16 (2018). date_created: 2018-12-11T11:44:32Z date_published: 2018-08-16T00:00:00Z date_updated: 2023-09-13T08:45:41Z day: '16' ddc: - '570' department: - _id: CaGu doi: 10.1371/journal.pbio.2005971 external_id: isi: - '000443383300024' file: - access_level: open_access checksum: 527076f78265cd4ea192cd1569851587 content_type: application/pdf creator: dernst date_created: 2018-12-17T12:55:31Z date_updated: 2020-07-14T12:48:10Z file_id: '5706' file_name: 2018_Plos_Chaudhry.pdf file_size: 4007095 relation: main_file file_date_updated: 2020-07-14T12:48:10Z has_accepted_license: '1' intvolume: ' 16' isi: 1 issue: '8' language: - iso: eng month: '08' oa: 1 oa_version: Published Version publication: PLoS Biology publication_status: published publisher: Public Library of Science publist_id: '7972' quality_controlled: '1' related_material: record: - id: '9810' relation: research_data status: public scopus_import: '1' status: public title: Leaky resistance and the conditions for the existence of lytic bacteriophage tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 16 year: '2018' ... --- _id: '4' abstract: - lang: eng text: We present a data-driven technique to instantly predict how fluid flows around various three-dimensional objects. Such simulation is useful for computational fabrication and engineering, but is usually computationally expensive since it requires solving the Navier-Stokes equation for many time steps. To accelerate the process, we propose a machine learning framework which predicts aerodynamic forces and velocity and pressure fields given a threedimensional shape input. Handling detailed free-form three-dimensional shapes in a data-driven framework is challenging because machine learning approaches usually require a consistent parametrization of input and output. We present a novel PolyCube maps-based parametrization that can be computed for three-dimensional shapes at interactive rates. This allows us to efficiently learn the nonlinear response of the flow using a Gaussian process regression. We demonstrate the effectiveness of our approach for the interactive design and optimization of a car body. article_number: '89' article_processing_charge: No author: - first_name: Nobuyuki full_name: Umetani, Nobuyuki last_name: Umetani - first_name: Bernd full_name: Bickel, Bernd id: 49876194-F248-11E8-B48F-1D18A9856A87 last_name: Bickel orcid: 0000-0001-6511-9385 citation: ama: Umetani N, Bickel B. Learning three-dimensional flow for interactive aerodynamic design. ACM Trans Graph. 2018;37(4). doi:10.1145/3197517.3201325 apa: Umetani, N., & Bickel, B. (2018). Learning three-dimensional flow for interactive aerodynamic design. ACM Trans. Graph. ACM. https://doi.org/10.1145/3197517.3201325 chicago: Umetani, Nobuyuki, and Bernd Bickel. “Learning Three-Dimensional Flow for Interactive Aerodynamic Design.” ACM Trans. Graph. ACM, 2018. https://doi.org/10.1145/3197517.3201325. ieee: N. Umetani and B. Bickel, “Learning three-dimensional flow for interactive aerodynamic design,” ACM Trans. Graph., vol. 37, no. 4. ACM, 2018. ista: Umetani N, Bickel B. 2018. Learning three-dimensional flow for interactive aerodynamic design. ACM Trans. Graph. 37(4), 89. mla: Umetani, Nobuyuki, and Bernd Bickel. “Learning Three-Dimensional Flow for Interactive Aerodynamic Design.” ACM Trans. Graph., vol. 37, no. 4, 89, ACM, 2018, doi:10.1145/3197517.3201325. short: N. Umetani, B. Bickel, ACM Trans. Graph. 37 (2018). date_created: 2018-12-11T11:44:06Z date_published: 2018-08-04T00:00:00Z date_updated: 2023-09-13T08:46:15Z day: '04' ddc: - '003' - '004' department: - _id: BeBi doi: 10.1145/3197517.3201325 ec_funded: 1 external_id: isi: - '000448185000050' file: - access_level: open_access checksum: 7a2243668f215821bc6aecad0320079a content_type: application/pdf creator: system date_created: 2018-12-12T10:16:28Z date_updated: 2020-07-14T12:46:22Z file_id: '5216' file_name: IST-2018-1049-v1+1_2018_sigg_Learning3DAerodynamics.pdf file_size: 22803163 relation: main_file file_date_updated: 2020-07-14T12:46:22Z has_accepted_license: '1' intvolume: ' 37' isi: 1 issue: '4' language: - iso: eng month: '08' oa: 1 oa_version: Submitted Version project: - _id: 24F9549A-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '715767' name: 'MATERIALIZABLE: Intelligent fabrication-oriented Computational Design and Modeling' publication: ACM Trans. Graph. publication_status: published publisher: ACM publist_id: '8053' pubrep_id: '1049' quality_controlled: '1' related_material: link: - description: News on IST Homepage relation: press_release url: https://ist.ac.at/en/news/new-interactive-machine-learning-tool-makes-car-designs-more-aerodynamic/ scopus_import: '1' status: public title: Learning three-dimensional flow for interactive aerodynamic design type: journal_article user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 37 year: '2018' ... --- _id: '566' abstract: - lang: eng text: "We consider large random matrices X with centered, independent entries which have comparable but not necessarily identical variances. Girko's circular law asserts that the spectrum is supported in a disk and in case of identical variances, the limiting density is uniform. In this special case, the local circular law by Bourgade et. al. [11,12] shows that the empirical density converges even locally on scales slightly above the typical eigenvalue spacing. In the general case, the limiting density is typically inhomogeneous and it is obtained via solving a system of deterministic equations. Our main result is the local inhomogeneous circular law in the bulk spectrum on the optimal scale for a general variance profile of the entries of X. \r\n\r\n" article_processing_charge: No article_type: original author: - first_name: Johannes full_name: Alt, Johannes id: 36D3D8B6-F248-11E8-B48F-1D18A9856A87 last_name: Alt - first_name: László full_name: Erdös, László id: 4DBD5372-F248-11E8-B48F-1D18A9856A87 last_name: Erdös orcid: 0000-0001-5366-9603 - first_name: Torben H full_name: Krüger, Torben H id: 3020C786-F248-11E8-B48F-1D18A9856A87 last_name: Krüger orcid: 0000-0002-4821-3297 citation: ama: Alt J, Erdös L, Krüger TH. Local inhomogeneous circular law. Annals Applied Probability . 2018;28(1):148-203. doi:10.1214/17-AAP1302 apa: Alt, J., Erdös, L., & Krüger, T. H. (2018). Local inhomogeneous circular law. Annals Applied Probability . Institute of Mathematical Statistics. https://doi.org/10.1214/17-AAP1302 chicago: Alt, Johannes, László Erdös, and Torben H Krüger. “Local Inhomogeneous Circular Law.” Annals Applied Probability . Institute of Mathematical Statistics, 2018. https://doi.org/10.1214/17-AAP1302. ieee: J. Alt, L. Erdös, and T. H. Krüger, “Local inhomogeneous circular law,” Annals Applied Probability , vol. 28, no. 1. Institute of Mathematical Statistics, pp. 148–203, 2018. ista: Alt J, Erdös L, Krüger TH. 2018. Local inhomogeneous circular law. Annals Applied Probability . 28(1), 148–203. mla: Alt, Johannes, et al. “Local Inhomogeneous Circular Law.” Annals Applied Probability , vol. 28, no. 1, Institute of Mathematical Statistics, 2018, pp. 148–203, doi:10.1214/17-AAP1302. short: J. Alt, L. Erdös, T.H. Krüger, Annals Applied Probability 28 (2018) 148–203. date_created: 2018-12-11T11:47:13Z date_published: 2018-03-03T00:00:00Z date_updated: 2023-09-13T08:47:52Z day: '03' department: - _id: LaEr doi: 10.1214/17-AAP1302 ec_funded: 1 external_id: arxiv: - '1612.07776 ' isi: - '000431721800005' intvolume: ' 28' isi: 1 issue: '1' language: - iso: eng main_file_link: - open_access: '1' url: 'https://arxiv.org/abs/1612.07776 ' month: '03' oa: 1 oa_version: Preprint page: 148-203 project: - _id: 258DCDE6-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '338804' name: Random matrices, universality and disordered quantum systems publication: 'Annals Applied Probability ' publication_status: published publisher: Institute of Mathematical Statistics quality_controlled: '1' related_material: record: - id: '149' relation: dissertation_contains status: public scopus_import: '1' status: public title: Local inhomogeneous circular law type: journal_article user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 28 year: '2018' ... --- _id: '106' abstract: - lang: eng text: The goal of this article is to introduce the reader to the theory of intrinsic geometry of convex surfaces. We illustrate the power of the tools by proving a theorem on convex surfaces containing an arbitrarily long closed simple geodesic. Let us remind ourselves that a curve in a surface is called geodesic if every sufficiently short arc of the curve is length minimizing; if, in addition, it has no self-intersections, we call it simple geodesic. A tetrahedron with equal opposite edges is called isosceles. The axiomatic method of Alexandrov geometry allows us to work with the metrics of convex surfaces directly, without approximating it first by a smooth or polyhedral metric. Such approximations destroy the closed geodesics on the surface; therefore it is difficult (if at all possible) to apply approximations in the proof of our theorem. On the other hand, a proof in the smooth or polyhedral case usually admits a translation into Alexandrov’s language; such translation makes the result more general. In fact, our proof resembles a translation of the proof given by Protasov. Note that the main theorem implies in particular that a smooth convex surface does not have arbitrarily long simple closed geodesics. However we do not know a proof of this corollary that is essentially simpler than the one presented below. article_processing_charge: No author: - first_name: Arseniy full_name: Akopyan, Arseniy id: 430D2C90-F248-11E8-B48F-1D18A9856A87 last_name: Akopyan orcid: 0000-0002-2548-617X - first_name: Anton full_name: Petrunin, Anton last_name: Petrunin citation: ama: Akopyan A, Petrunin A. Long geodesics on convex surfaces. Mathematical Intelligencer. 2018;40(3):26-31. doi:10.1007/s00283-018-9795-5 apa: Akopyan, A., & Petrunin, A. (2018). Long geodesics on convex surfaces. Mathematical Intelligencer. Springer. https://doi.org/10.1007/s00283-018-9795-5 chicago: Akopyan, Arseniy, and Anton Petrunin. “Long Geodesics on Convex Surfaces.” Mathematical Intelligencer. Springer, 2018. https://doi.org/10.1007/s00283-018-9795-5. ieee: A. Akopyan and A. Petrunin, “Long geodesics on convex surfaces,” Mathematical Intelligencer, vol. 40, no. 3. Springer, pp. 26–31, 2018. ista: Akopyan A, Petrunin A. 2018. Long geodesics on convex surfaces. Mathematical Intelligencer. 40(3), 26–31. mla: Akopyan, Arseniy, and Anton Petrunin. “Long Geodesics on Convex Surfaces.” Mathematical Intelligencer, vol. 40, no. 3, Springer, 2018, pp. 26–31, doi:10.1007/s00283-018-9795-5. short: A. Akopyan, A. Petrunin, Mathematical Intelligencer 40 (2018) 26–31. date_created: 2018-12-11T11:44:40Z date_published: 2018-09-01T00:00:00Z date_updated: 2023-09-13T08:49:16Z day: '01' department: - _id: HeEd doi: 10.1007/s00283-018-9795-5 external_id: arxiv: - '1702.05172' isi: - '000444141200005' intvolume: ' 40' isi: 1 issue: '3' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1702.05172 month: '09' oa: 1 oa_version: Preprint page: 26 - 31 publication: Mathematical Intelligencer publication_status: published publisher: Springer publist_id: '7948' quality_controlled: '1' scopus_import: '1' status: public title: Long geodesics on convex surfaces type: journal_article user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 40 year: '2018' ...