---
_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'
...