---
OA_place: publisher
_id: '1396'
abstract:
- lang: eng
text: CA3 pyramidal neurons are thought to pay a key role in memory storage and
pattern completion by activity-dependent synaptic plasticity between CA3-CA3 recurrent
excitatory synapses. To examine the induction rules of synaptic plasticity at
CA3-CA3 synapses, we performed whole-cell patch-clamp recordings in acute hippocampal
slices from rats (postnatal 21-24 days) at room temperature. Compound excitatory
postsynaptic potentials (ESPSs) were recorded by tract stimulation in stratum
oriens in the presence of 10 µM gabazine. High-frequency stimulation (HFS) induced
N-methyl-D-aspartate (NMDA) receptor-dependent long-term potentiation (LTP). Although
LTP by HFS did not requier postsynaptic spikes, it was blocked by Na+-channel
blockers suggesting that local active processes (e.g.) dendritic spikes) may contribute
to LTP induction without requirement of a somatic action potential (AP). We next
examined the properties of spike timing-dependent plasticity (STDP) at CA3-CA3
synapses. Unexpectedly, low-frequency pairing of EPSPs and backpropagated action
potentialy (bAPs) induced LTP, independent of temporal order. The STDP curve was
symmetric and broad, with a half-width of ~150 ms. Consistent with these specific
STDP induction properties, post-presynaptic sequences led to a supralinear summation
of spine [Ca2+] transients. Furthermore, in autoassociative network models, storage
and recall was substantially more robust with symmetric than with asymmetric STDP
rules. In conclusion, we found associative forms of LTP at CA3-CA3 recurrent collateral
synapses with distinct induction rules. LTP induced by HFS may be associated with
dendritic spikes. In contrast, low frequency pairing of pre- and postsynaptic
activity induced LTP only if EPSP-AP were temporally very close. Together, these
induction mechanisms of synaptiic plasticity may contribute to memory storage
in the CA3-CA3 microcircuit at different ranges of activity.
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Rajiv Kumar
full_name: Mishra, Rajiv Kumar
id: 46CB58F2-F248-11E8-B48F-1D18A9856A87
last_name: Mishra
citation:
ama: Mishra RK. Synaptic plasticity rules at CA3-CA3 recurrent synapses in hippocampus.
2016.
apa: Mishra, R. K. (2016). Synaptic plasticity rules at CA3-CA3 recurrent synapses
in hippocampus. Institute of Science and Technology Austria.
chicago: Mishra, Rajiv Kumar. “Synaptic Plasticity Rules at CA3-CA3 Recurrent Synapses
in Hippocampus.” Institute of Science and Technology Austria, 2016.
ieee: R. K. Mishra, “Synaptic plasticity rules at CA3-CA3 recurrent synapses in
hippocampus,” Institute of Science and Technology Austria, 2016.
ista: Mishra RK. 2016. Synaptic plasticity rules at CA3-CA3 recurrent synapses in
hippocampus. Institute of Science and Technology Austria.
mla: Mishra, Rajiv Kumar. Synaptic Plasticity Rules at CA3-CA3 Recurrent Synapses
in Hippocampus. Institute of Science and Technology Austria, 2016.
short: R.K. Mishra, Synaptic Plasticity Rules at CA3-CA3 Recurrent Synapses in Hippocampus,
Institute of Science and Technology Austria, 2016.
corr_author: '1'
date_created: 2018-12-11T11:51:46Z
date_published: 2016-03-01T00:00:00Z
date_updated: 2026-04-09T10:52:26Z
day: '01'
ddc:
- '570'
degree_awarded: PhD
department:
- _id: PeJo
file:
- access_level: closed
checksum: 5a010a838faf040f7064f3cfb802f743
content_type: application/pdf
creator: dernst
date_created: 2019-08-09T12:14:46Z
date_updated: 2020-07-14T12:44:48Z
file_id: '6782'
file_name: Thesis_Mishra_Rajiv (Final).pdf
file_size: 2407572
relation: main_file
- access_level: open_access
checksum: 81b26d9ede92c99f1d8cc6fa1d04cbbb
content_type: application/pdf
creator: dernst
date_created: 2021-02-22T11:48:44Z
date_updated: 2021-02-22T11:48:44Z
file_id: '9183'
file_name: 2016_RajivMishra_Thesis.pdf
file_size: 2407572
relation: main_file
success: 1
file_date_updated: 2021-02-22T11:48:44Z
has_accepted_license: '1'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: '83'
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '5811'
related_material:
record:
- id: '1432'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Peter M
full_name: Jonas, Peter M
id: 353C1B58-F248-11E8-B48F-1D18A9856A87
last_name: Jonas
orcid: 0000-0001-5001-4804
title: Synaptic plasticity rules at CA3-CA3 recurrent synapses in hippocampus
type: dissertation
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2016'
...
---
_id: '5553'
abstract:
- lang: eng
text: "Genotypic, phenotypic and demographic data for 2128 wild snapdragons and
1127 open-pollinated progeny from a natural hybrid zone, collected as part of
Tom Ellis' PhD thesis (submitted) February 2016).\r\n\r\nTissue samples were sent
to LGC Genomics in Berlin for DNA extraction, and genotyping at 70 SNP markers
by KASPR genotyping. 29 of these SNPs failed to amplify reliably, and have been
removed from this dataset.\r\n\r\nOther data were retreived from an online database
of this population at www.antspec.org."
article_processing_charge: No
author:
- first_name: David
full_name: Field, David
id: 419049E2-F248-11E8-B48F-1D18A9856A87
last_name: Field
orcid: 0000-0002-4014-8478
- first_name: Thomas
full_name: Ellis, Thomas
id: 3153D6D4-F248-11E8-B48F-1D18A9856A87
last_name: Ellis
orcid: 0000-0002-8511-0254
citation:
ama: Field D, Ellis T. Inference of mating patterns among wild snapdragons in a
natural hybrid zone in 2012. 2016. doi:10.15479/AT:ISTA:37
apa: Field, D., & Ellis, T. (2016). Inference of mating patterns among wild
snapdragons in a natural hybrid zone in 2012. Institute of Science and Technology
Austria. https://doi.org/10.15479/AT:ISTA:37
chicago: Field, David, and Thomas Ellis. “Inference of Mating Patterns among Wild
Snapdragons in a Natural Hybrid Zone in 2012.” Institute of Science and Technology
Austria, 2016. https://doi.org/10.15479/AT:ISTA:37.
ieee: D. Field and T. Ellis, “Inference of mating patterns among wild snapdragons
in a natural hybrid zone in 2012.” Institute of Science and Technology Austria,
2016.
ista: Field D, Ellis T. 2016. Inference of mating patterns among wild snapdragons
in a natural hybrid zone in 2012, Institute of Science and Technology Austria,
10.15479/AT:ISTA:37.
mla: Field, David, and Thomas Ellis. Inference of Mating Patterns among Wild
Snapdragons in a Natural Hybrid Zone in 2012. Institute of Science and Technology
Austria, 2016, doi:10.15479/AT:ISTA:37.
short: D. Field, T. Ellis, (2016).
contributor:
- contributor_type: project_manager
first_name: Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
datarep_id: '37'
date_created: 2018-12-12T12:31:30Z
date_published: 2016-02-19T00:00:00Z
date_updated: 2026-04-09T10:52:06Z
day: '19'
ddc:
- '576'
department:
- _id: NiBa
doi: 10.15479/AT:ISTA:37
file:
- access_level: open_access
checksum: 4ae751b1fa4897fa216241f975a57313
content_type: application/zip
creator: system
date_created: 2018-12-12T13:03:02Z
date_updated: 2020-07-14T12:47:01Z
file_id: '5620'
file_name: IST-2016-37-v1+1_paternity_archive.zip
file_size: 132808
relation: main_file
file_date_updated: 2020-07-14T12:47:01Z
has_accepted_license: '1'
keyword:
- paternity assignment
- pedigree
- matting patterns
- assortative mating
- Antirrhinum majus
- frequency-dependent selection
- plant-pollinator interaction
license: https://creativecommons.org/publicdomain/zero/1.0/
month: '02'
oa: 1
oa_version: Published Version
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '1398'
relation: part_of_dissertation
status: public
status: public
title: Inference of mating patterns among wild snapdragons in a natural hybrid zone
in 2012
tmp:
image: /images/cc_0.png
legal_code_url: https://creativecommons.org/publicdomain/zero/1.0/legalcode
name: Creative Commons Public Domain Dedication (CC0 1.0)
short: CC0 (1.0)
type: research_data
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5551'
abstract:
- lang: eng
text: "Data from array experiments investigating pollinator behaviour on snapdragons
in controlled conditions, and their effect on plant mating. Data were collected
as part of Tom Ellis' PhD thesis , submitted February 2016.\r\n\r\nWe placed a
total of 36 plants in a grid inside a closed organza tent, with a single hive
of commercially bred bumblebees (Bombus hortorum). We used only the yellow-flowered
Antirrhinum majus striatum and the magenta-flowered Antirrhinum majus pseudomajus,
at ratios of 6:36, 12:24, 18:18, 24:12 and 30:6.\r\n\r\nAfter 24 hours to learn
how to deal with snapdragons, I observed pollinators foraging on plants, and recorded
the transitions between plants. Thereafter seeds on plants were allowed to develops.
A sample of these were grown to maturity when their flower colour could be determined,
and they were scored as yellow, magenta, or hybrid."
article_processing_charge: No
author:
- first_name: Thomas
full_name: Ellis, Thomas
id: 3153D6D4-F248-11E8-B48F-1D18A9856A87
last_name: Ellis
orcid: 0000-0002-8511-0254
citation:
ama: Ellis T. Data on pollinator observations and offpsring phenotypes. 2016. doi:10.15479/AT:ISTA:35
apa: Ellis, T. (2016). Data on pollinator observations and offpsring phenotypes.
Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:35
chicago: Ellis, Thomas. “Data on Pollinator Observations and Offpsring Phenotypes.”
Institute of Science and Technology Austria, 2016. https://doi.org/10.15479/AT:ISTA:35.
ieee: T. Ellis, “Data on pollinator observations and offpsring phenotypes.” Institute
of Science and Technology Austria, 2016.
ista: Ellis T. 2016. Data on pollinator observations and offpsring phenotypes, Institute
of Science and Technology Austria, 10.15479/AT:ISTA:35.
mla: Ellis, Thomas. Data on Pollinator Observations and Offpsring Phenotypes.
Institute of Science and Technology Austria, 2016, doi:10.15479/AT:ISTA:35.
short: T. Ellis, (2016).
contributor:
- first_name: David
id: 419049E2-F248-11E8-B48F-1D18A9856A87
last_name: Field
- first_name: Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
datarep_id: '35'
date_created: 2018-12-12T12:31:29Z
date_published: 2016-02-19T00:00:00Z
date_updated: 2026-04-09T10:52:07Z
day: '19'
department:
- _id: NiBa
doi: 10.15479/AT:ISTA:35
file:
- access_level: open_access
checksum: aa3eb85d52b110cd192aa23147c4d4f3
content_type: application/zip
creator: system
date_created: 2018-12-12T13:05:12Z
date_updated: 2020-07-14T12:47:01Z
file_id: '5640'
file_name: IST-2016-35-v1+1_array_data.zip
file_size: 32775
relation: main_file
file_date_updated: 2020-07-14T12:47:01Z
has_accepted_license: '1'
month: '02'
oa: 1
oa_version: Published Version
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '1398'
relation: part_of_dissertation
status: public
status: public
title: Data on pollinator observations and offpsring phenotypes
tmp:
image: /images/cc_0.png
legal_code_url: https://creativecommons.org/publicdomain/zero/1.0/legalcode
name: Creative Commons Public Domain Dedication (CC0 1.0)
short: CC0 (1.0)
type: research_data
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5552'
abstract:
- lang: eng
text: "Data on pollinator visitation to wild snapdragons in a natural hybrid zone,
collected as part of Tom Ellis' PhD thesis (submitted February 2016).\r\n\r\nSnapdragon
flowers have a mouth-like structure which pollinators must open to access nectar.
We placed 5mm cellophane tags in these mouths, which are held in place by the
pressure of the flower until a pollinator visits. When she opens the flower, the
tag drops out, and one can infer a visit. We surveyed plants over multiple days
in 2010, 2011 and 2012.\r\n\r\nAlso included are data on phenotypic and demographic
variables which may be explanatory variables for pollinator visitation."
article_processing_charge: No
author:
- first_name: Thomas
full_name: Ellis, Thomas
id: 3153D6D4-F248-11E8-B48F-1D18A9856A87
last_name: Ellis
orcid: 0000-0002-8511-0254
citation:
ama: Ellis T. Pollinator visitation data for wild Antirrhinum majus plants, with
phenotypic and frequency data. 2016. doi:10.15479/AT:ISTA:36
apa: Ellis, T. (2016). Pollinator visitation data for wild Antirrhinum majus plants,
with phenotypic and frequency data. Institute of Science and Technology Austria.
https://doi.org/10.15479/AT:ISTA:36
chicago: Ellis, Thomas. “Pollinator Visitation Data for Wild Antirrhinum Majus Plants,
with Phenotypic and Frequency Data.” Institute of Science and Technology Austria,
2016. https://doi.org/10.15479/AT:ISTA:36.
ieee: T. Ellis, “Pollinator visitation data for wild Antirrhinum majus plants, with
phenotypic and frequency data.” Institute of Science and Technology Austria, 2016.
ista: Ellis T. 2016. Pollinator visitation data for wild Antirrhinum majus plants,
with phenotypic and frequency data., Institute of Science and Technology Austria,
10.15479/AT:ISTA:36.
mla: Ellis, Thomas. Pollinator Visitation Data for Wild Antirrhinum Majus Plants,
with Phenotypic and Frequency Data. Institute of Science and Technology Austria,
2016, doi:10.15479/AT:ISTA:36.
short: T. Ellis, (2016).
contributor:
- first_name: David
id: 419049E2-F248-11E8-B48F-1D18A9856A87
last_name: Field
- first_name: Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
datarep_id: '36'
date_created: 2018-12-12T12:31:30Z
date_published: 2016-02-19T00:00:00Z
date_updated: 2026-04-09T10:52:07Z
day: '19'
department:
- _id: NiBa
doi: 10.15479/AT:ISTA:36
file:
- access_level: open_access
checksum: cbc61b523d4d475a04a737d50dc470ef
content_type: application/zip
creator: system
date_created: 2018-12-12T13:03:07Z
date_updated: 2020-07-14T12:47:01Z
file_id: '5625'
file_name: IST-2016-36-v1+1_tag_assay_archive.zip
file_size: 44905
relation: main_file
file_date_updated: 2020-07-14T12:47:01Z
has_accepted_license: '1'
month: '02'
oa: 1
oa_version: Published Version
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '1398'
relation: part_of_dissertation
status: public
status: public
title: Pollinator visitation data for wild Antirrhinum majus plants, with phenotypic
and frequency data.
type: research_data
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
OA_place: publisher
_id: '1130'
abstract:
- lang: eng
text: "In this thesis we present a computer-aided programming approach to concurrency.
Our approach helps the programmer by automatically fixing concurrency-related
bugs, i.e. bugs that occur when the program is executed using an aggressive preemptive
scheduler, but not when using a non-preemptive (cooperative) scheduler. Bugs are
program behaviours that are incorrect w.r.t. a specification. We consider both
user-provided explicit specifications in the form of assertion\r\nstatements in
the code as well as an implicit specification. The implicit specification is inferred
from the non-preemptive behaviour. Let us consider sequences of calls that the
program makes to an external interface. The implicit specification requires that
any such sequence produced under a preemptive scheduler should be included in
the set of sequences produced under a non-preemptive scheduler. We consider several
semantics-preserving fixes that go beyond atomic sections typically explored in
the synchronisation synthesis literature. Our synthesis is able to place locks,
barriers and wait-signal statements and last, but not least reorder independent
statements. The latter may be useful if a thread is released to early, e.g., before
some initialisation is completed. We guarantee that our synthesis does not introduce
deadlocks and that the synchronisation inserted is optimal w.r.t. a given objective
function. We dub our solution trace-based synchronisation synthesis and it is
loosely based on counterexample-guided inductive synthesis (CEGIS). The synthesis
works by discovering a trace that is incorrect w.r.t. the specification and identifying
ordering constraints crucial to trigger the specification violation. Synchronisation
may be placed immediately (greedy approach) or delayed until all incorrect traces
are found (non-greedy approach). For the non-greedy approach we construct a set
of global constraints over synchronisation placements. Each model of the global
constraints set corresponds to a correctness-ensuring synchronisation placement.
The placement that is optimal w.r.t. the given objective function is chosen as
the synchronisation solution. We evaluate our approach on a number of realistic
(albeit simplified) Linux device-driver\r\nbenchmarks. The benchmarks are versions
of the drivers with known concurrency-related bugs. For the experiments with an
explicit specification we added assertions that would detect the bugs in the experiments.
Device drivers lend themselves to implicit specification, where the device and
the operating system are the external interfaces. Our experiments demonstrate
that our synthesis method is precise and efficient. We implemented objective functions
for coarse-grained and fine-grained locking and observed that different synchronisation
placements are produced for our experiments, favouring e.g. a minimal number of
synchronisation operations or maximum concurrency."
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Thorsten
full_name: Tarrach, Thorsten
id: 3D6E8F2C-F248-11E8-B48F-1D18A9856A87
last_name: Tarrach
orcid: 0000-0003-4409-8487
citation:
ama: Tarrach T. Automatic synthesis of synchronisation primitives for concurrent
programs. 2016. doi:10.15479/at:ista:1130
apa: Tarrach, T. (2016). Automatic synthesis of synchronisation primitives for
concurrent programs. Institute of Science and Technology Austria. https://doi.org/10.15479/at:ista:1130
chicago: Tarrach, Thorsten. “Automatic Synthesis of Synchronisation Primitives for
Concurrent Programs.” Institute of Science and Technology Austria, 2016. https://doi.org/10.15479/at:ista:1130.
ieee: T. Tarrach, “Automatic synthesis of synchronisation primitives for concurrent
programs,” Institute of Science and Technology Austria, 2016.
ista: Tarrach T. 2016. Automatic synthesis of synchronisation primitives for concurrent
programs. Institute of Science and Technology Austria.
mla: Tarrach, Thorsten. Automatic Synthesis of Synchronisation Primitives for
Concurrent Programs. Institute of Science and Technology Austria, 2016, doi:10.15479/at:ista:1130.
short: T. Tarrach, Automatic Synthesis of Synchronisation Primitives for Concurrent
Programs, Institute of Science and Technology Austria, 2016.
corr_author: '1'
date_created: 2018-12-11T11:50:19Z
date_published: 2016-07-07T00:00:00Z
date_updated: 2026-04-09T10:54:01Z
day: '07'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: ToHe
- _id: GradSch
doi: 10.15479/at:ista:1130
ec_funded: 1
file:
- access_level: open_access
checksum: 319a506831650327e85376db41fc1094
content_type: application/pdf
creator: dernst
date_created: 2021-02-22T11:39:32Z
date_updated: 2021-02-22T11:39:32Z
file_id: '9179'
file_name: 2016_Tarrach_Thesis.pdf
file_size: 1523935
relation: main_file
success: 1
- access_level: closed
checksum: 39efcd789f0ad859ff15652cb7afc412
content_type: application/pdf
creator: cchlebak
date_created: 2021-11-16T14:14:38Z
date_updated: 2021-11-17T13:46:55Z
file_id: '10296'
file_name: 2016_Tarrach_Thesispdfa.pdf
file_size: 1306068
relation: main_file
file_date_updated: 2021-11-17T13:46:55Z
has_accepted_license: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://thorstent.github.io/theses/phd_thorsten_tarrach.pdf
month: '07'
oa: 1
oa_version: Published Version
page: '151'
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '6230'
related_material:
record:
- id: '2218'
relation: part_of_dissertation
status: public
- id: '2445'
relation: part_of_dissertation
status: public
- id: '1729'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
title: Automatic synthesis of synchronisation primitives for concurrent programs
type: dissertation
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2016'
...
---
OA_place: publisher
_id: '1131'
abstract:
- lang: eng
text: "Evolution of gene regulation is important for phenotypic evolution and diversity.
Sequence-specific binding of regulatory proteins is one of the key regulatory
mechanisms determining gene expression. Although there has been intense interest
in evolution of regulatory binding sites in the last decades, a theoretical understanding
is far from being complete. In this thesis, I aim at a better understanding of
the evolution of transcriptional regulatory binding sequences by using biophysical
and population genetic models.\r\nIn the first part of the thesis, I discuss how
to formulate the evolutionary dynamics of binding se- quences in a single isolated
binding site and in promoter/enhancer regions. I develop a theoretical framework
bridging between a thermodynamical model for transcription and a mutation-selection-drift
model for monomorphic populations. I mainly address the typical evolutionary rates,
and how they de- pend on biophysical parameters (e.g. binding length and specificity)
and population genetic parameters (e.g. population size and selection strength).\r\nIn
the second part of the thesis, I analyse empirical data for a better evolutionary
and biophysical understanding of sequence-specific binding of bacterial RNA polymerase.
First, I infer selection on regulatory and non-regulatory binding sites of RNA
polymerase in the E. coli K12 genome. Second, I infer the chemical potential of
RNA polymerase, an important but unknown physical parameter defining the threshold
energy for strong binding. Furthermore, I try to understand the relation between
the lac promoter sequence diversity and the LacZ activity variation among 20 bacterial
isolates by constructing a simple but biophysically motivated gene expression
model. Lastly, I lay out a statistical framework to predict adaptive point mutations
in de novo promoter evolution in a selection experiment."
acknowledgement: This PhD thesis may not have been completed without the help and
care I received from some peo- ple during my PhD life. I am especially grateful
to Tiago Paixao, Gasper Tkacik, Nick Barton, not only for their scientific advices
but also for their patience and support. I thank Calin Guet and Jonathan Bollback
for allowing me to “play around” in their labs and get some experience on experimental
evolution. I thank Magdalena Steinrueck and Fabienne Jesse for collaborating and
sharing their experimental data with me. I thank Johannes Jaeger for reviewing my
thesis. I thank all members of Barton group (aka bartonians) for their feedback,
and all workers of IST Austria for making the best working conditions. Lastly, I
thank two special women, Nejla Sag ̆lam and Setenay Dog ̆an, for their continuous
support and encouragement. I truly had a great chance of having right people around
me.
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Murat
full_name: Tugrul, Murat
id: 37C323C6-F248-11E8-B48F-1D18A9856A87
last_name: Tugrul
orcid: 0000-0002-8523-0758
citation:
ama: Tugrul M. Evolution of transcriptional regulatory sequences. 2016.
apa: Tugrul, M. (2016). Evolution of transcriptional regulatory sequences.
Institute of Science and Technology Austria.
chicago: Tugrul, Murat. “Evolution of Transcriptional Regulatory Sequences.” Institute
of Science and Technology Austria, 2016.
ieee: M. Tugrul, “Evolution of transcriptional regulatory sequences,” Institute
of Science and Technology Austria, 2016.
ista: Tugrul M. 2016. Evolution of transcriptional regulatory sequences. Institute
of Science and Technology Austria.
mla: Tugrul, Murat. Evolution of Transcriptional Regulatory Sequences. Institute
of Science and Technology Austria, 2016.
short: M. Tugrul, Evolution of Transcriptional Regulatory Sequences, Institute of
Science and Technology Austria, 2016.
corr_author: '1'
date_created: 2018-12-11T11:50:19Z
date_published: 2016-07-01T00:00:00Z
date_updated: 2026-04-09T10:52:40Z
day: '01'
ddc:
- '576'
degree_awarded: PhD
department:
- _id: NiBa
file:
- access_level: closed
checksum: 66cb61a59943e4fb7447c6a86be5ef51
content_type: application/pdf
creator: dernst
date_created: 2019-08-13T08:53:52Z
date_updated: 2019-08-13T08:53:52Z
file_id: '6810'
file_name: Tugrul_thesis_w_signature_page.pdf
file_size: 3695257
relation: main_file
- access_level: open_access
checksum: 293e388d70563760f6b24c3e66283dda
content_type: application/pdf
creator: dernst
date_created: 2021-02-22T11:45:20Z
date_updated: 2021-02-22T11:45:20Z
file_id: '9182'
file_name: 2016_Tugrul_Thesis.pdf
file_size: 3880811
relation: main_file
success: 1
file_date_updated: 2021-02-22T11:45:20Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '89'
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '6229'
related_material:
record:
- id: '5554'
relation: research_data
status: public
- id: '1666'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
title: Evolution of transcriptional regulatory sequences
type: dissertation
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2016'
...
---
_id: '5554'
abstract:
- lang: eng
text: "The data stored here is used in Murat Tugrul's PhD thesis (Chapter 3), which
is related to the evolution of bacterial RNA polymerase binding.\r\nMagdalena
Steinrueck (PhD Student in Calin Guet's group at IST Austria) performed the experiments
and created the data on de novo promoter evolution. Fabienne Jesse (PhD Student
in Jon Bollback's group at IST Austria) performed the experiments and created
the data on lac promoter evolution."
article_processing_charge: No
author:
- first_name: Murat
full_name: Tugrul, Murat
id: 37C323C6-F248-11E8-B48F-1D18A9856A87
last_name: Tugrul
orcid: 0000-0002-8523-0758
citation:
ama: Tugrul M. Experimental Data for Binding Site Evolution of Bacterial RNA Polymerase.
2016. doi:10.15479/AT:ISTA:43
apa: Tugrul, M. (2016). Experimental Data for Binding Site Evolution of Bacterial
RNA Polymerase. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:43
chicago: Tugrul, Murat. “Experimental Data for Binding Site Evolution of Bacterial
RNA Polymerase.” Institute of Science and Technology Austria, 2016. https://doi.org/10.15479/AT:ISTA:43.
ieee: M. Tugrul, “Experimental Data for Binding Site Evolution of Bacterial RNA
Polymerase.” Institute of Science and Technology Austria, 2016.
ista: Tugrul M. 2016. Experimental Data for Binding Site Evolution of Bacterial
RNA Polymerase, Institute of Science and Technology Austria, 10.15479/AT:ISTA:43.
mla: Tugrul, Murat. Experimental Data for Binding Site Evolution of Bacterial
RNA Polymerase. Institute of Science and Technology Austria, 2016, doi:10.15479/AT:ISTA:43.
short: M. Tugrul, (2016).
contributor:
- contributor_type: researcher
first_name: Magdalena
id: 2C023F40-F248-11E8-B48F-1D18A9856A87
last_name: Steinrück
- contributor_type: researcher
first_name: Fabienne
id: 4C8C26A4-F248-11E8-B48F-1D18A9856A87
last_name: Jesse
datarep_id: '43'
date_created: 2018-12-12T12:31:30Z
date_published: 2016-05-12T00:00:00Z
date_updated: 2026-04-09T10:52:40Z
day: '12'
department:
- _id: NiBa
- _id: JoBo
doi: 10.15479/AT:ISTA:43
file:
- access_level: open_access
checksum: 1fc0a10bb7ce110fcb5e1fbe3cf0c4e2
content_type: application/zip
creator: system
date_created: 2018-12-12T13:03:08Z
date_updated: 2020-07-14T12:47:01Z
file_id: '5626'
file_name: IST-2016-43-v1+1_DATA_MTugrul_PhDThesis_Chapter3.zip
file_size: 1123495
relation: main_file
file_date_updated: 2020-07-14T12:47:01Z
has_accepted_license: '1'
keyword:
- RNAP binding
- de novo promoter evolution
- lac promoter
month: '05'
oa: 1
oa_version: Published Version
publisher: Institute of Science and Technology Austria
related_material:
record:
- id: '1131'
relation: used_in_publication
status: public
status: public
title: Experimental Data for Binding Site Evolution of Bacterial RNA Polymerase
tmp:
image: /images/cc_0.png
legal_code_url: https://creativecommons.org/publicdomain/zero/1.0/legalcode
name: Creative Commons Public Domain Dedication (CC0 1.0)
short: CC0 (1.0)
type: research_data
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
OA_place: publisher
_id: '1125'
abstract:
- lang: eng
text: "Natural environments are never constant but subject to spatial and temporal
change on\r\nall scales, increasingly so due to human activity. Hence, it is crucial
to understand the\r\nimpact of environmental variation on evolutionary processes.
In this thesis, I present\r\nthree topics that share the common theme of environmental
variation, yet illustrate its\r\neffect from different perspectives.\r\nFirst,
I show how a temporally fluctuating environment gives rise to second-order\r\nselection
on a modifier for stress-induced mutagenesis. Without fluctuations, when\r\npopulations
are adapted to their environment, mutation rates are minimized. I argue\r\nthat
a stress-induced mutator mechanism may only be maintained if the population is\r\nrepeatedly
subjected to diverse environmental challenges, and I outline implications of\r\nthe
presented results to antibiotic treatment strategies.\r\nSecond, I discuss my
work on the evolution of dispersal. Besides reproducing\r\nknown results about
the effect of heterogeneous habitats on dispersal, it identifies\r\nspatial changes
in dispersal type frequencies as a source for selection for increased\r\npropensities
to disperse. This concept contains effects of relatedness that are known\r\nto
promote dispersal, and I explain how it identifies other forces selecting for
dispersal\r\nand puts them on a common scale.\r\nThird, I analyse genetic variances
of phenotypic traits under multivariate stabilizing\r\nselection. For the case
of constant environments, I generalize known formulae of\r\nequilibrium variances
to multiple traits and discuss how the genetic variance of a focal\r\ntrait is
influenced by selection on background traits. I conclude by presenting ideas and\r\npreliminary
work aiming at including environmental fluctuations in the form of moving\r\ntrait
optima into the model."
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Sebastian
full_name: Novak, Sebastian
id: 461468AE-F248-11E8-B48F-1D18A9856A87
last_name: Novak
orcid: 0000-0002-2519-824X
citation:
ama: Novak S. Evolutionary proccesses in variable emvironments. 2016.
apa: Novak, S. (2016). Evolutionary proccesses in variable emvironments.
Institute of Science and Technology Austria.
chicago: Novak, Sebastian. “Evolutionary Proccesses in Variable Emvironments.” Institute
of Science and Technology Austria, 2016.
ieee: S. Novak, “Evolutionary proccesses in variable emvironments,” Institute of
Science and Technology Austria, 2016.
ista: Novak S. 2016. Evolutionary proccesses in variable emvironments. Institute
of Science and Technology Austria.
mla: Novak, Sebastian. Evolutionary Proccesses in Variable Emvironments.
Institute of Science and Technology Austria, 2016.
short: S. Novak, Evolutionary Proccesses in Variable Emvironments, Institute of
Science and Technology Austria, 2016.
corr_author: '1'
date_created: 2018-12-11T11:50:17Z
date_published: 2016-07-01T00:00:00Z
date_updated: 2026-04-09T14:25:34Z
day: '01'
ddc:
- '576'
degree_awarded: PhD
department:
- _id: NiBa
file:
- access_level: closed
checksum: 81dcc838dfcf7aa0b1a27ecf4fe2da4e
content_type: application/pdf
creator: dernst
date_created: 2019-08-13T09:01:00Z
date_updated: 2019-08-13T09:01:00Z
file_id: '6811'
file_name: Novak_thesis.pdf
file_size: 3564901
relation: main_file
- access_level: open_access
checksum: 30808d2f7ca920e09f63a95cdc49bffd
content_type: application/pdf
creator: dernst
date_created: 2021-02-22T13:42:47Z
date_updated: 2021-02-22T13:42:47Z
file_id: '9186'
file_name: 2016_Novak_Thesis.pdf
file_size: 2814384
relation: main_file
success: 1
file_date_updated: 2021-02-22T13:42:47Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '124'
publication_identifier:
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '6235'
related_material:
record:
- id: '2023'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
title: Evolutionary proccesses in variable emvironments
type: dissertation
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2016'
...
---
_id: '1662'
abstract:
- lang: eng
text: We introduce a modification of the classic notion of intrinsic volume using
persistence moments of height functions. Evaluating the modified first intrinsic
volume on digital approximations of a compact body with smoothly embedded boundary
in Rn, we prove convergence to the first intrinsic volume of the body as the resolution
of the approximation improves. We have weaker results for the other modified intrinsic
volumes, proving they converge to the corresponding intrinsic volumes of the n-dimensional
unit ball.
acknowledgement: "This research is partially supported by the Toposys project FP7-ICT-318493-STREP,
and by ESF under the ACAT Research Network Programme.\r\nBoth authors thank Anne
Marie Svane for her comments on an early version of this paper. The second author
wishes to thank Eva B. Vedel Jensen and Markus Kiderlen from Aarhus University for
enlightening discussions and their kind hospitality during a visit of their department
in 2014."
article_processing_charge: No
author:
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Florian
full_name: Pausinger, Florian
id: 2A77D7A2-F248-11E8-B48F-1D18A9856A87
last_name: Pausinger
orcid: 0000-0002-8379-3768
citation:
ama: Edelsbrunner H, Pausinger F. Approximation and convergence of the intrinsic
volume. Advances in Mathematics. 2016;287:674-703. doi:10.1016/j.aim.2015.10.004
apa: Edelsbrunner, H., & Pausinger, F. (2016). Approximation and convergence
of the intrinsic volume. Advances in Mathematics. Academic Press. https://doi.org/10.1016/j.aim.2015.10.004
chicago: Edelsbrunner, Herbert, and Florian Pausinger. “Approximation and Convergence
of the Intrinsic Volume.” Advances in Mathematics. Academic Press, 2016.
https://doi.org/10.1016/j.aim.2015.10.004.
ieee: H. Edelsbrunner and F. Pausinger, “Approximation and convergence of the intrinsic
volume,” Advances in Mathematics, vol. 287. Academic Press, pp. 674–703,
2016.
ista: Edelsbrunner H, Pausinger F. 2016. Approximation and convergence of the intrinsic
volume. Advances in Mathematics. 287, 674–703.
mla: Edelsbrunner, Herbert, and Florian Pausinger. “Approximation and Convergence
of the Intrinsic Volume.” Advances in Mathematics, vol. 287, Academic Press,
2016, pp. 674–703, doi:10.1016/j.aim.2015.10.004.
short: H. Edelsbrunner, F. Pausinger, Advances in Mathematics 287 (2016) 674–703.
corr_author: '1'
date_created: 2018-12-11T11:53:20Z
date_published: 2016-01-10T00:00:00Z
date_updated: 2026-04-09T14:26:05Z
day: '10'
ddc:
- '004'
department:
- _id: HeEd
doi: 10.1016/j.aim.2015.10.004
ec_funded: 1
external_id:
isi:
- '000375634100016'
file:
- access_level: open_access
checksum: f8869ec110c35c852ef6a37425374af7
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:10Z
date_updated: 2020-07-14T12:45:10Z
file_id: '4928'
file_name: IST-2017-774-v1+1_2016-J-03-FirstIntVolume.pdf
file_size: 248985
relation: main_file
file_date_updated: 2020-07-14T12:45:10Z
has_accepted_license: '1'
intvolume: ' 287'
isi: 1
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 674 - 703
project:
- _id: 255D761E-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '318493'
name: Topological Complex Systems
publication: Advances in Mathematics
publication_status: published
publisher: Academic Press
publist_id: '5488'
pubrep_id: '774'
quality_controlled: '1'
related_material:
record:
- id: '1399'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Approximation and convergence of the intrinsic volume
tmp:
image: /images/cc_by_nc_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
(CC BY-NC-ND 4.0)
short: CC BY-NC-ND (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 287
year: '2016'
...
---
_id: '1093'
abstract:
- lang: eng
text: 'We introduce a general class of distances (metrics) between Markov chains,
which are based on linear behaviour. This class encompasses distances given topologically
(such as the total variation distance or trace distance) as well as by temporal
logics or automata. We investigate which of the distances can be approximated
by observing the systems, i.e. by black-box testing or simulation, and we provide
both negative and positive results. '
acknowledgement: "This research was funded in part by the European Research Council
(ERC) under grant agreement 267989\r\n(QUAREM), the Austrian Science Fund (FWF)
under grants project S11402-N23 (RiSE and SHiNE)\r\nand Z211-N23 (Wittgenstein Award),
by the Czech Science Foundation Grant No. P202/12/G061, and\r\nby the SNSF Advanced
Postdoc. Mobility Fellowship – grant number P300P2_161067."
alternative_title:
- LIPIcs
article_number: '20'
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
citation:
ama: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. Linear distances between Markov
chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.20'
apa: 'Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2016). Linear
distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency
Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPIcs.CONCUR.2016.20'
chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
“Linear Distances between Markov Chains,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.20.
ieee: 'P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Linear distances
between Markov chains,” presented at the CONCUR: Concurrency Theory, Quebec City;
Canada, 2016, vol. 59.'
ista: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between
Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.'
mla: Daca, Przemyslaw, et al. Linear Distances between Markov Chains. Vol.
59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.20.
short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl -
Leibniz-Zentrum für Informatik, 2016.
conference:
end_date: 2016-08-26
location: Quebec City; Canada
name: 'CONCUR: Concurrency Theory'
start_date: 2016-08-23
date_created: 2018-12-11T11:50:06Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2026-04-15T10:02:12Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
- _id: KrCh
- _id: CaGu
doi: 10.4230/LIPIcs.CONCUR.2016.20
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:39Z
date_updated: 2018-12-12T10:11:39Z
file_id: '4895'
file_name: IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf
file_size: 501827
relation: main_file
file_date_updated: 2018-12-12T10:11:39Z
has_accepted_license: '1'
intvolume: ' 59'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6283'
pubrep_id: '794'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Linear distances between Markov chains
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 59
year: '2016'
...
---
_id: '1234'
abstract:
- lang: eng
text: We present a new algorithm for the statistical model checking of Markov chains
with respect to unbounded temporal properties, including full linear temporal
logic. The main idea is that we monitor each simulation run on the fly, in order
to detect quickly if a bottom strongly connected component is entered with high
probability, in which case the simulation run can be terminated early. As a result,
our simulation runs are often much shorter than required by termination bounds
that are computed a priori for a desired level of confidence on a large state
space. In comparison to previous algorithms for statistical model checking our
method is not only faster in many cases but also requires less information about
the system, namely, only the minimum transition probability that occurs in the
Markov chain. In addition, our method can be generalised to unbounded quantitative
properties such as mean-payoff bounds.
acknowledgement: "This research was funded in part by the European Research Council
(ERC) under\r\ngrant agreement 267989 (QUAREM), the Austrian Science Fund
\ (FWF) under\r\ngrants project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award),
the Peo-\r\nple Programme (Marie Curie Actions) of the European Union’s Seventh
Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734, the SNSF Advanced Postdoc.\r\nMobility
Fellowship – grant number P300P2\r\n161067, and the Czech Science Foun-\r\ndation
under grant agreement P202/12/G061."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jan
full_name: Kretinsky, Jan
id: 44CEF464-F248-11E8-B48F-1D18A9856A87
last_name: Kretinsky
orcid: 0000-0002-8122-2881
- first_name: Tatjana
full_name: Petrov, Tatjana
id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
last_name: Petrov
orcid: 0000-0002-9041-0905
citation:
ama: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking
for unbounded temporal properties. In: Vol 9636. Springer; 2016:112-129. doi:10.1007/978-3-662-49674-9_7'
apa: 'Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2016). Faster
statistical model checking for unbounded temporal properties (Vol. 9636, pp. 112–129).
Presented at the TACAS: Tools and Algorithms for the Construction and Analysis
of Systems, Eindhoven, The Netherlands: Springer. https://doi.org/10.1007/978-3-662-49674-9_7'
chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
“Faster Statistical Model Checking for Unbounded Temporal Properties,” 9636:112–29.
Springer, 2016. https://doi.org/10.1007/978-3-662-49674-9_7.
ieee: 'P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical
model checking for unbounded temporal properties,” presented at the TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands,
2016, vol. 9636, pp. 112–129.'
ista: 'Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Faster statistical model
checking for unbounded temporal properties. TACAS: Tools and Algorithms for the
Construction and Analysis of Systems, LNCS, vol. 9636, 112–129.'
mla: Daca, Przemyslaw, et al. Faster Statistical Model Checking for Unbounded
Temporal Properties. Vol. 9636, Springer, 2016, pp. 112–29, doi:10.1007/978-3-662-49674-9_7.
short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Springer, 2016, pp.
112–129.
conference:
end_date: 2016-04-08
location: Eindhoven, The Netherlands
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2016-04-02
date_created: 2018-12-11T11:50:51Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2026-04-15T10:02:12Z
day: '01'
department:
- _id: ToHe
- _id: CaGu
doi: 10.1007/978-3-662-49674-9_7
ec_funded: 1
external_id:
arxiv:
- '1504.05739'
isi:
- '000406428000007'
intvolume: ' 9636'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1504.05739
month: '01'
oa: 1
oa_version: Preprint
page: 112 - 129
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 25681D80-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '291734'
name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '6099'
quality_controlled: '1'
related_material:
record:
- id: '471'
relation: later_version
status: public
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Faster statistical model checking for unbounded temporal properties
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9636
year: '2016'
...
---
_id: '1391'
abstract:
- lang: eng
text: "We present an extension to the quantifier-free theory of integer arrays which
allows us to express counting. The properties expressible in Array Folds Logic
(AFL) include statements such as "the first array cell contains the array
length," and "the array contains equally many minimal and maximal elements."
These properties cannot be expressed in quantified fragments of the theory of
arrays, nor in the theory of concatenation. Using reduction to counter machines,
we show that the satisfiability problem of AFL is PSPACE-complete, and with a
natural restriction the complexity decreases to NP. We also show that adding either
universal quantifiers or concatenation leads to undecidability.\r\nAFL contains
terms that fold a function over an array. We demonstrate that folding, a well-known
concept from functional languages, allows us to concisely summarize loops that
count over arrays, which occurs frequently in real-life programs. We provide a
tool that can discharge proof obligations in AFL, and we demonstrate on practical
examples that our decision procedure can solve a broad range of problems in symbolic
testing and program verification."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Andrey
full_name: Kupriyanov, Andrey
id: 2C311BF8-F248-11E8-B48F-1D18A9856A87
last_name: Kupriyanov
citation:
ama: 'Daca P, Henzinger TA, Kupriyanov A. Array folds logic. In: Vol 9780. Springer;
2016:230-248. doi:10.1007/978-3-319-41540-6_13'
apa: 'Daca, P., Henzinger, T. A., & Kupriyanov, A. (2016). Array folds logic
(Vol. 9780, pp. 230–248). Presented at the CAV: Computer Aided Verification, Toronto,
Canada: Springer. https://doi.org/10.1007/978-3-319-41540-6_13'
chicago: Daca, Przemyslaw, Thomas A Henzinger, and Andrey Kupriyanov. “Array Folds
Logic,” 9780:230–48. Springer, 2016. https://doi.org/10.1007/978-3-319-41540-6_13.
ieee: 'P. Daca, T. A. Henzinger, and A. Kupriyanov, “Array folds logic,” presented
at the CAV: Computer Aided Verification, Toronto, Canada, 2016, vol. 9780, pp.
230–248.'
ista: 'Daca P, Henzinger TA, Kupriyanov A. 2016. Array folds logic. CAV: Computer
Aided Verification, LNCS, vol. 9780, 230–248.'
mla: Daca, Przemyslaw, et al. Array Folds Logic. Vol. 9780, Springer, 2016,
pp. 230–48, doi:10.1007/978-3-319-41540-6_13.
short: P. Daca, T.A. Henzinger, A. Kupriyanov, in:, Springer, 2016, pp. 230–248.
conference:
end_date: 2016-07-23
location: Toronto, Canada
name: 'CAV: Computer Aided Verification'
start_date: 2016-07-17
corr_author: '1'
date_created: 2018-12-11T11:51:45Z
date_published: 2016-07-13T00:00:00Z
date_updated: 2026-04-15T10:02:12Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-319-41540-6_13
ec_funded: 1
external_id:
arxiv:
- '1603.06850'
isi:
- '000387731400013'
intvolume: ' 9780'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1603.06850
month: '07'
oa: 1
oa_version: Preprint
page: 230 - 248
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication_status: published
publisher: Springer
publist_id: '5818'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Array folds logic
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9780
year: '2016'
...
---
_id: '1230'
abstract:
- lang: eng
text: Concolic testing is a promising method for generating test suites for large
programs. However, it suffers from the path-explosion problem and often fails
to find tests that cover difficult-to-reach parts of programs. In contrast, model
checkers based on counterexample-guided abstraction refinement explore programs
exhaustively, while failing to scale on large programs with precision. In this
paper, we present a novel method that iteratively combines concolic testing and
model checking to find a test suite for a given coverage criterion. If concolic
testing fails to cover some test goals, then the model checker refines its program
abstraction to prove more paths infeasible, which reduces the search space for
concolic testing. We have implemented our method on top of the concolictesting
tool Crest and the model checker CpaChecker. We evaluated our tool on a collection
of programs and a category of SvComp benchmarks. In our experiments, we observed
an improvement in branch coverage compared to Crest from 48% to 63% in the best
case, and from 66% to 71% on average.
acknowledgement: "We thank Andrey Kupriyanov for feedback on the manuscript,\r\nand
Michael Tautschnig for help with preparing the experiments. This research was supported
in part by the European Research Council (ERC) under grant 267989 (QUAREM) and by
the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein
Award)."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Ashutosh
full_name: Gupta, Ashutosh
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Daca P, Gupta A, Henzinger TA. Abstraction-driven concolic testing. In: Vol
9583. Springer; 2016:328-347. doi:10.1007/978-3-662-49122-5_16'
apa: 'Daca, P., Gupta, A., & Henzinger, T. A. (2016). Abstraction-driven concolic
testing (Vol. 9583, pp. 328–347). Presented at the VMCAI: Verification, Model
Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer. https://doi.org/10.1007/978-3-662-49122-5_16'
chicago: Daca, Przemyslaw, Ashutosh Gupta, and Thomas A Henzinger. “Abstraction-Driven
Concolic Testing,” 9583:328–47. Springer, 2016. https://doi.org/10.1007/978-3-662-49122-5_16.
ieee: 'P. Daca, A. Gupta, and T. A. Henzinger, “Abstraction-driven concolic testing,”
presented at the VMCAI: Verification, Model Checking and Abstract Interpretation,
St. Petersburg, FL, USA, 2016, vol. 9583, pp. 328–347.'
ista: 'Daca P, Gupta A, Henzinger TA. 2016. Abstraction-driven concolic testing.
VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 9583,
328–347.'
mla: Daca, Przemyslaw, et al. Abstraction-Driven Concolic Testing. Vol. 9583,
Springer, 2016, pp. 328–47, doi:10.1007/978-3-662-49122-5_16.
short: P. Daca, A. Gupta, T.A. Henzinger, in:, Springer, 2016, pp. 328–347.
conference:
end_date: 2016-01-19
location: St. Petersburg, FL, USA
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
start_date: 2016-01-17
date_created: 2018-12-11T11:50:50Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2026-04-15T10:02:12Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-662-49122-5_16
ec_funded: 1
external_id:
arxiv:
- '1511.02615'
isi:
- '000375148800016'
intvolume: ' 9583'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1511.02615
month: '01'
oa: 1
oa_version: Preprint
page: 328 - 347
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _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: '6104'
quality_controlled: '1'
related_material:
record:
- id: '1155'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Abstraction-driven concolic testing
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9583
year: '2016'
...
---
OA_type: closed access
_id: '21522'
abstract:
- lang: eng
text: In this Letter, we demonstrate highly efficient, polarization-insensitive
planar lenses (metalenses) at red, green, and blue wavelengths (λ = 660, 532,
and 405 nm). Metalenses with numerical apertures (NA) of 0.85 and 0.6 and corresponding
efficiencies as high as 60% and 90% are achieved. These metalenses are less than
600 nm-thick and can focus incident light down to diffraction-limited spots as
small as ∼0.64λ and provide high-resolution imaging. In addition, the focal spots
are very symmetric with high Strehl ratios. The single step lithography and compatibility
with large-scale fabrication processes make metalenses highly promising for widespread
applications in imaging and spectroscopy.
article_processing_charge: No
article_type: original
author:
- first_name: M.
full_name: Khorasaninejad, M.
last_name: Khorasaninejad
- first_name: A. Y.
full_name: Zhu, A. Y.
last_name: Zhu
- first_name: Charles
full_name: Roques-Carmes, Charles
id: e2e68fc9-6505-11ef-a541-eb4e72cc3e82
last_name: Roques-Carmes
- first_name: W. T.
full_name: Chen, W. T.
last_name: Chen
- first_name: J.
full_name: Oh, J.
last_name: Oh
- first_name: I.
full_name: Mishra, I.
last_name: Mishra
- first_name: R. C.
full_name: Devlin, R. C.
last_name: Devlin
- first_name: F.
full_name: Capasso, F.
last_name: Capasso
citation:
ama: Khorasaninejad M, Zhu AY, Roques-Carmes C, et al. Polarization-insensitive
metalenses at visible wavelengths. Nano Letters. 2016;16(11):7229-7234.
doi:10.1021/acs.nanolett.6b03626
apa: Khorasaninejad, M., Zhu, A. Y., Roques-Carmes, C., Chen, W. T., Oh, J., Mishra,
I., … Capasso, F. (2016). Polarization-insensitive metalenses at visible wavelengths.
Nano Letters. American Chemical Society. https://doi.org/10.1021/acs.nanolett.6b03626
chicago: Khorasaninejad, M., A. Y. Zhu, Charles Roques-Carmes, W. T. Chen, J. Oh,
I. Mishra, R. C. Devlin, and F. Capasso. “Polarization-Insensitive Metalenses
at Visible Wavelengths.” Nano Letters. American Chemical Society, 2016.
https://doi.org/10.1021/acs.nanolett.6b03626.
ieee: M. Khorasaninejad et al., “Polarization-insensitive metalenses at visible
wavelengths,” Nano Letters, vol. 16, no. 11. American Chemical Society,
pp. 7229–7234, 2016.
ista: Khorasaninejad M, Zhu AY, Roques-Carmes C, Chen WT, Oh J, Mishra I, Devlin
RC, Capasso F. 2016. Polarization-insensitive metalenses at visible wavelengths.
Nano Letters. 16(11), 7229–7234.
mla: Khorasaninejad, M., et al. “Polarization-Insensitive Metalenses at Visible
Wavelengths.” Nano Letters, vol. 16, no. 11, American Chemical Society,
2016, pp. 7229–34, doi:10.1021/acs.nanolett.6b03626.
short: M. Khorasaninejad, A.Y. Zhu, C. Roques-Carmes, W.T. Chen, J. Oh, I. Mishra,
R.C. Devlin, F. Capasso, Nano Letters 16 (2016) 7229–7234.
date_created: 2026-03-30T12:22:47Z
date_published: 2016-10-24T00:00:00Z
date_updated: 2026-04-15T11:53:17Z
day: '24'
ddc:
- '530'
doi: 10.1021/acs.nanolett.6b03626
extern: '1'
external_id:
pmid:
- '27791380'
intvolume: ' 16'
issue: '11'
keyword:
- Metasurface
- polarization-insensitive metalenses
- visible wavelength
- titanium dioxide
language:
- iso: eng
month: '10'
oa_version: None
page: 7229-7234
pmid: 1
publication: Nano Letters
publication_identifier:
eissn:
- 1530-6992
issn:
- 1530-6984
publication_status: published
publisher: American Chemical Society
quality_controlled: '1'
scopus_import: '1'
status: public
title: Polarization-insensitive metalenses at visible wavelengths
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16
year: '2016'
...
---
_id: '1341'
abstract:
- lang: eng
text: In resource allocation games, selfish players share resources that are needed
in order to fulfill their objectives. The cost of using a resource depends on
the load on it. In the traditional setting, the players make their choices concurrently
and in one-shot. That is, a strategy for a player is a subset of the resources.
We introduce and study dynamic resource allocation games. In this setting, the
game proceeds in phases. In each phase each player chooses one resource. A scheduler
dictates the order in which the players proceed in a phase, possibly scheduling
several players to proceed concurrently. The game ends when each player has collected
a set of resources that fulfills his objective. The cost for each player then
depends on this set as well as on the load on the resources in it – we consider
both congestion and cost-sharing games. We argue that the dynamic setting is the
suitable setting for many applications in practice. We study the stability of
dynamic resource allocation games, where the appropriate notion of stability is
that of subgame perfect equilibrium, study the inefficiency incurred due to selfish
behavior, and also study problems that are particular to the dynamic setting,
like constraints on the order in which resources can be chosen or the problem
of finding a scheduler that achieves stability.
acknowledgement: This research was supported in part by the European Research Council
(ERC) under grants 267989 (QUAREM) and 278410 (QUALITY), and by the Austrian Science
Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: 'Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. In:
Vol 9928. Springer; 2016:153-166. doi:10.1007/978-3-662-53354-3_13'
apa: 'Avni, G., Henzinger, T. A., & Kupferman, O. (2016). Dynamic resource allocation
games (Vol. 9928, pp. 153–166). Presented at the SAGT: Symposium on Algorithmic
Game Theory, Liverpool, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53354-3_13'
chicago: Avni, Guy, Thomas A Henzinger, and Orna Kupferman. “Dynamic Resource Allocation
Games,” 9928:153–66. Springer, 2016. https://doi.org/10.1007/978-3-662-53354-3_13.
ieee: 'G. Avni, T. A. Henzinger, and O. Kupferman, “Dynamic resource allocation
games,” presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool,
United Kingdom, 2016, vol. 9928, pp. 153–166.'
ista: 'Avni G, Henzinger TA, Kupferman O. 2016. Dynamic resource allocation games.
SAGT: Symposium on Algorithmic Game Theory, LNCS, vol. 9928, 153–166.'
mla: Avni, Guy, et al. Dynamic Resource Allocation Games. Vol. 9928, Springer,
2016, pp. 153–66, doi:10.1007/978-3-662-53354-3_13.
short: G. Avni, T.A. Henzinger, O. Kupferman, in:, Springer, 2016, pp. 153–166.
conference:
end_date: 2016-09-21
location: Liverpool, United Kingdom
name: 'SAGT: Symposium on Algorithmic Game Theory'
start_date: 2016-09-19
corr_author: '1'
date_created: 2018-12-11T11:51:28Z
date_published: 2016-09-01T00:00:00Z
date_updated: 2026-04-16T09:35:14Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-662-53354-3_13
ec_funded: 1
external_id:
isi:
- '000389020400013'
file:
- access_level: open_access
checksum: 0825eefd4e22774f6f62cb7d7389b05a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:22Z
date_updated: 2020-07-14T12:44:45Z
file_id: '5073'
file_name: IST-2016-645-v1+1_sagt-cr.pdf
file_size: 243458
relation: main_file
file_date_updated: 2020-07-14T12:44:45Z
has_accepted_license: '1'
intvolume: ' 9928'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Preprint
page: 153 - 166
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication_status: published
publisher: Springer
publist_id: '5926'
pubrep_id: '645'
quality_controlled: '1'
related_material:
record:
- id: '6761'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Dynamic resource allocation games
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9928
year: '2016'
...
---
_id: '1321'
abstract:
- lang: eng
text: Most migrating cells extrude their front by the force of actin polymerization.
Polymerization requires an initial nucleation step, which is mediated by factors
establishing either parallel filaments in the case of filopodia or branched filaments
that form the branched lamellipodial network. Branches are considered essential
for regular cell motility and are initiated by the Arp2/3 complex, which in turn
is activated by nucleation-promoting factors of the WASP and WAVE families. Here
we employed rapid amoeboid crawling leukocytes and found that deletion of the
WAVE complex eliminated actin branching and thus lamellipodia formation. The cells
were left with parallel filaments at the leading edge, which translated, depending
on the differentiation status of the cell, into a unipolar pointed cell shape
or cells with multiple filopodia. Remarkably, unipolar cells migrated with increased
speed and enormous directional persistence, while they were unable to turn towards
chemotactic gradients. Cells with multiple filopodia retained chemotactic activity
but their migration was progressively impaired with increasing geometrical complexity
of the extracellular environment. These findings establish that diversified leading
edge protrusions serve as explorative structures while they slow down actual locomotion.
acknowledged_ssus:
- _id: SSU
acknowledgement: "This work was supported by the German Research Foundation (DFG)
Priority Program SP 1464 to T.E.B.S. and M.S., and European Research Council (ERC
GA 281556) and Human Frontiers Program grants to M.S.\r\nService Units of IST Austria
for excellent technical support."
article_processing_charge: No
article_type: original
author:
- first_name: Alexander F
full_name: Leithner, Alexander F
id: 3B1B77E4-F248-11E8-B48F-1D18A9856A87
last_name: Leithner
orcid: 0000-0002-1073-744X
- first_name: Alexander
full_name: Eichner, Alexander
id: 4DFA52AE-F248-11E8-B48F-1D18A9856A87
last_name: Eichner
- first_name: Jan
full_name: Müller, Jan
id: AD07FDB4-0F61-11EA-8158-C4CC64CEAA8D
last_name: Müller
- first_name: Anne
full_name: Reversat, Anne
id: 35B76592-F248-11E8-B48F-1D18A9856A87
last_name: Reversat
orcid: 0000-0003-0666-8928
- first_name: Markus
full_name: Brown, Markus
id: 3DAB9AFC-F248-11E8-B48F-1D18A9856A87
last_name: Brown
- first_name: Jan
full_name: Schwarz, Jan
id: 346C1EC6-F248-11E8-B48F-1D18A9856A87
last_name: Schwarz
- first_name: Jack
full_name: Merrin, Jack
id: 4515C308-F248-11E8-B48F-1D18A9856A87
last_name: Merrin
orcid: 0000-0001-5145-4609
- first_name: David
full_name: De Gorter, David
last_name: De Gorter
- first_name: Florian
full_name: Schur, Florian
id: 48AD8942-F248-11E8-B48F-1D18A9856A87
last_name: Schur
orcid: 0000-0003-4790-8078
- first_name: Jonathan
full_name: Bayerl, Jonathan
last_name: Bayerl
- first_name: Ingrid
full_name: De Vries, Ingrid
id: 4C7D837E-F248-11E8-B48F-1D18A9856A87
last_name: De Vries
- first_name: Stefan
full_name: Wieser, Stefan
id: 355AA5A0-F248-11E8-B48F-1D18A9856A87
last_name: Wieser
orcid: 0000-0002-2670-2217
- first_name: Robert
full_name: Hauschild, Robert
id: 4E01D6B4-F248-11E8-B48F-1D18A9856A87
last_name: Hauschild
orcid: 0000-0001-9843-3522
- first_name: Frank
full_name: Lai, Frank
last_name: Lai
- first_name: Markus
full_name: Moser, Markus
last_name: Moser
- first_name: Dontscho
full_name: Kerjaschki, Dontscho
last_name: Kerjaschki
- first_name: Klemens
full_name: Rottner, Klemens
last_name: Rottner
- first_name: Victor
full_name: Small, Victor
last_name: Small
- first_name: Theresia
full_name: Stradal, Theresia
last_name: Stradal
- first_name: Michael K
full_name: Sixt, Michael K
id: 41E9FBEA-F248-11E8-B48F-1D18A9856A87
last_name: Sixt
orcid: 0000-0002-6620-9179
citation:
ama: Leithner AF, Eichner A, Müller J, et al. Diversified actin protrusions promote
environmental exploration but are dispensable for locomotion of leukocytes. Nature
Cell Biology. 2016;18:1253-1259. doi:10.1038/ncb3426
apa: Leithner, A. F., Eichner, A., Müller, J., Reversat, A., Brown, M., Schwarz,
J., … Sixt, M. K. (2016). Diversified actin protrusions promote environmental
exploration but are dispensable for locomotion of leukocytes. Nature Cell Biology.
Nature Publishing Group. https://doi.org/10.1038/ncb3426
chicago: Leithner, Alexander F, Alexander Eichner, Jan Müller, Anne Reversat, Markus
Brown, Jan Schwarz, Jack Merrin, et al. “Diversified Actin Protrusions Promote
Environmental Exploration but Are Dispensable for Locomotion of Leukocytes.” Nature
Cell Biology. Nature Publishing Group, 2016. https://doi.org/10.1038/ncb3426.
ieee: A. F. Leithner et al., “Diversified actin protrusions promote environmental
exploration but are dispensable for locomotion of leukocytes,” Nature Cell
Biology, vol. 18. Nature Publishing Group, pp. 1253–1259, 2016.
ista: Leithner AF, Eichner A, Müller J, Reversat A, Brown M, Schwarz J, Merrin J,
De Gorter D, Schur FK, Bayerl J, de Vries I, Wieser S, Hauschild R, Lai F, Moser
M, Kerjaschki D, Rottner K, Small V, Stradal T, Sixt MK. 2016. Diversified actin
protrusions promote environmental exploration but are dispensable for locomotion
of leukocytes. Nature Cell Biology. 18, 1253–1259.
mla: Leithner, Alexander F., et al. “Diversified Actin Protrusions Promote Environmental
Exploration but Are Dispensable for Locomotion of Leukocytes.” Nature Cell
Biology, vol. 18, Nature Publishing Group, 2016, pp. 1253–59, doi:10.1038/ncb3426.
short: A.F. Leithner, A. Eichner, J. Müller, A. Reversat, M. Brown, J. Schwarz,
J. Merrin, D. De Gorter, F.K. Schur, J. Bayerl, I. de Vries, S. Wieser, R. Hauschild,
F. Lai, M. Moser, D. Kerjaschki, K. Rottner, V. Small, T. Stradal, M.K. Sixt,
Nature Cell Biology 18 (2016) 1253–1259.
corr_author: '1'
date_created: 2018-12-11T11:51:21Z
date_published: 2016-10-24T00:00:00Z
date_updated: 2026-04-25T22:30:20Z
day: '24'
ddc:
- '570'
department:
- _id: MiSi
- _id: NanoFab
- _id: Bio
doi: 10.1038/ncb3426
ec_funded: 1
external_id:
isi:
- '000387165600018'
file:
- access_level: open_access
checksum: e1411cb7c99a2d9089c178a6abef25e7
content_type: application/pdf
creator: dernst
date_created: 2020-05-14T16:33:46Z
date_updated: 2020-07-14T12:44:43Z
file_id: '7844'
file_name: 2018_NatureCell_Leithner.pdf
file_size: 4433280
relation: main_file
file_date_updated: 2020-07-14T12:44:43Z
has_accepted_license: '1'
intvolume: ' 18'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-sa/4.0/
month: '10'
oa: 1
oa_version: Submitted Version
page: 1253 - 1259
project:
- _id: 25A603A2-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '281556'
name: Cytoskeletal force generation and force transduction of migrating leukocytes
publication: Nature Cell Biology
publication_status: published
publisher: Nature Publishing Group
publist_id: '5949'
quality_controlled: '1'
related_material:
record:
- id: '323'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Diversified actin protrusions promote environmental exploration but are dispensable
for locomotion of leukocytes
tmp:
image: /images/cc_by_nc_sa.png
legal_code_url: https://creativecommons.org/licenses/by-nc-sa/4.0/legalcode
name: Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International (CC
BY-NC-SA 4.0)
short: CC BY-NC-SA (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 18
year: '2016'
...
---
_id: '1183'
abstract:
- lang: eng
text: Autism spectrum disorders (ASD) are a group of genetic disorders often overlapping
with other neurological conditions. We previously described abnormalities in the
branched-chain amino acid (BCAA) catabolic pathway as a cause of ASD. Here, we
show that the solute carrier transporter 7a5 (SLC7A5), a large neutral amino acid
transporter localized at the blood brain barrier (BBB), has an essential role
in maintaining normal levels of brain BCAAs. In mice, deletion of Slc7a5 from
the endothelial cells of the BBB leads to atypical brain amino acid profile, abnormal
mRNA translation, and severe neurological abnormalities. Furthermore, we identified
several patients with autistic traits and motor delay carrying deleterious homozygous
mutations in the SLC7A5 gene. Finally, we demonstrate that BCAA intracerebroventricular
administration ameliorates abnormal behaviors in adult mutant mice. Our data elucidate
a neurological syndrome defined by SLC7A5 mutations and support an essential role
for the BCAA in human brain function.
acknowledgement: "This work was supported by NICHD (P01HD070494) and SFARI (grant
275275) to J.G.G., and FWF (SFB35_3523) to G.N.\r\nWe thank A.C. Manzano, Mike Liu,
and F. Marr for technical assistance, and R. Shigemoto and the IST Austria Electron
Microscopy (EM) Facility for assistance. We acknowledge support from CIDR for genome-wide
SNP analysis (X01HG008823) and Broad Institute Center for Mendelian Disorders (UM1HG008900
to D. MacArthur), the Yale Center for Mendelian Disorders (U54HG006504 to M.G.),
the Gregory M. Kiez and Mehmet Kutman Foundation (M.G.), Italian Ministry of Instruction
University and Research (PON01_00937 to C.I.), and NIH (R01-GM108911 to A.S.). This
work was supported by NICHD (P01HD070494) and SFARI (grant 275275) to J.G.G., and
FWF (SFB35_3523) to G.N.\r\n\r\n#EMFacility"
article_processing_charge: No
article_type: original
author:
- first_name: Dora-Clara
full_name: Tarlungeanu, Dora-Clara
id: 2ABCE612-F248-11E8-B48F-1D18A9856A87
last_name: Tarlungeanu
- first_name: Elena
full_name: Deliu, Elena
id: 37A40D7E-F248-11E8-B48F-1D18A9856A87
last_name: Deliu
orcid: 0000-0002-7370-5293
- first_name: Christoph
full_name: Dotter, Christoph
id: 4C66542E-F248-11E8-B48F-1D18A9856A87
last_name: Dotter
orcid: 0000-0002-9033-9096
- first_name: Majdi
full_name: Kara, Majdi
last_name: Kara
- first_name: Philipp
full_name: Janiesch, Philipp
last_name: Janiesch
- first_name: Mariafrancesca
full_name: Scalise, Mariafrancesca
last_name: Scalise
- first_name: Michele
full_name: Galluccio, Michele
last_name: Galluccio
- first_name: Mateja
full_name: Tesulov, Mateja
last_name: Tesulov
- first_name: Emanuela
full_name: Morelli, Emanuela
id: 3F4D1282-F248-11E8-B48F-1D18A9856A87
last_name: Morelli
- first_name: Fatma
full_name: Sönmez, Fatma
last_name: Sönmez
- first_name: Kaya
full_name: Bilgüvar, Kaya
last_name: Bilgüvar
- first_name: Ryuichi
full_name: Ohgaki, Ryuichi
last_name: Ohgaki
- first_name: Yoshikatsu
full_name: Kanai, Yoshikatsu
last_name: Kanai
- first_name: Anide
full_name: Johansen, Anide
last_name: Johansen
- first_name: Seham
full_name: Esharif, Seham
last_name: Esharif
- first_name: Tawfeg
full_name: Ben Omran, Tawfeg
last_name: Ben Omran
- first_name: Meral
full_name: Topcu, Meral
last_name: Topcu
- first_name: Avner
full_name: Schlessinger, Avner
last_name: Schlessinger
- first_name: Cesare
full_name: Indiveri, Cesare
last_name: Indiveri
- first_name: Kent
full_name: Duncan, Kent
last_name: Duncan
- first_name: Ahmet
full_name: Caglayan, Ahmet
last_name: Caglayan
- first_name: Murat
full_name: Günel, Murat
last_name: Günel
- first_name: Joseph
full_name: Gleeson, Joseph
last_name: Gleeson
- first_name: Gaia
full_name: Novarino, Gaia
id: 3E57A680-F248-11E8-B48F-1D18A9856A87
last_name: Novarino
orcid: 0000-0002-7673-7178
citation:
ama: Tarlungeanu D-C, Deliu E, Dotter C, et al. Impaired amino acid transport at
the blood brain barrier is a cause of autism spectrum disorder. Cell. 2016;167(6):1481-1494.
doi:10.1016/j.cell.2016.11.013
apa: Tarlungeanu, D.-C., Deliu, E., Dotter, C., Kara, M., Janiesch, P., Scalise,
M., … Novarino, G. (2016). Impaired amino acid transport at the blood brain barrier
is a cause of autism spectrum disorder. Cell. Cell Press. https://doi.org/10.1016/j.cell.2016.11.013
chicago: Tarlungeanu, Dora-Clara, Elena Deliu, Christoph Dotter, Majdi Kara, Philipp
Janiesch, Mariafrancesca Scalise, Michele Galluccio, et al. “Impaired Amino Acid
Transport at the Blood Brain Barrier Is a Cause of Autism Spectrum Disorder.”
Cell. Cell Press, 2016. https://doi.org/10.1016/j.cell.2016.11.013.
ieee: D.-C. Tarlungeanu et al., “Impaired amino acid transport at the blood
brain barrier is a cause of autism spectrum disorder,” Cell, vol. 167,
no. 6. Cell Press, pp. 1481–1494, 2016.
ista: Tarlungeanu D-C, Deliu E, Dotter C, Kara M, Janiesch P, Scalise M, Galluccio
M, Tesulov M, Morelli E, Sönmez F, Bilgüvar K, Ohgaki R, Kanai Y, Johansen A,
Esharif S, Ben Omran T, Topcu M, Schlessinger A, Indiveri C, Duncan K, Caglayan
A, Günel M, Gleeson J, Novarino G. 2016. Impaired amino acid transport at the
blood brain barrier is a cause of autism spectrum disorder. Cell. 167(6), 1481–1494.
mla: Tarlungeanu, Dora-Clara, et al. “Impaired Amino Acid Transport at the Blood
Brain Barrier Is a Cause of Autism Spectrum Disorder.” Cell, vol. 167,
no. 6, Cell Press, 2016, pp. 1481–94, doi:10.1016/j.cell.2016.11.013.
short: D.-C. Tarlungeanu, E. Deliu, C. Dotter, M. Kara, P. Janiesch, M. Scalise,
M. Galluccio, M. Tesulov, E. Morelli, F. Sönmez, K. Bilgüvar, R. Ohgaki, Y. Kanai,
A. Johansen, S. Esharif, T. Ben Omran, M. Topcu, A. Schlessinger, C. Indiveri,
K. Duncan, A. Caglayan, M. Günel, J. Gleeson, G. Novarino, Cell 167 (2016) 1481–1494.
date_created: 2018-12-11T11:50:35Z
date_published: 2016-12-01T00:00:00Z
date_updated: 2026-04-25T22:31:27Z
day: '01'
ddc:
- '576'
- '616'
department:
- _id: GaNo
doi: 10.1016/j.cell.2016.11.013
external_id:
isi:
- '000389470500012'
file:
- access_level: open_access
checksum: 7fe01ab12a6610d3db421e0136db2f77
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:44Z
date_updated: 2020-07-14T12:44:37Z
file_id: '5030'
file_name: IST-2017-771-v1+1_Tarlungeanu_et_al._Final_edited.pdf
file_size: 73907957
relation: main_file
file_date_updated: 2020-07-14T12:44:37Z
has_accepted_license: '1'
intvolume: ' 167'
isi: 1
issue: '6'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Submitted Version
page: 1481 - 1494
project:
- _id: 25473368-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: F03523
name: Transmembrane Transporters in Health and Disease
publication: Cell
publication_status: published
publisher: Cell Press
publist_id: '6170'
pubrep_id: '771'
quality_controlled: '1'
related_material:
record:
- id: '395'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Impaired amino acid transport at the blood brain barrier is a cause of autism
spectrum disorder
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 167
year: '2016'
...
---
_id: '1100'
abstract:
- lang: eng
text: During metazoan development, the temporal pattern of morphogen signaling is
critical for organizing cell fates in space and time. Yet, tools for temporally
controlling morphogen signaling within the embryo are still scarce. Here, we developed
a photoactivatable Nodal receptor to determine how the temporal pattern of Nodal
signaling affects cell fate specification during zebrafish gastrulation. By using
this receptor to manipulate the duration of Nodal signaling in vivo by light,
we show that extended Nodal signaling within the organizer promotes prechordal
plate specification and suppresses endoderm differentiation. Endoderm differentiation
is suppressed by extended Nodal signaling inducing expression of the transcriptional
repressor goosecoid (gsc) in prechordal plate progenitors, which in turn restrains
Nodal signaling from upregulating the endoderm differentiation gene sox17 within
these cells. Thus, optogenetic manipulation of Nodal signaling identifies a critical
role of Nodal signaling duration for organizer cell fate specification during
gastrulation.
acknowledged_ssus:
- _id: SSU
acknowledgement: 'We are grateful to members of the C.-P.H. and H.J. labs for discussions,
R. Hauschild and the different Scientific Service Units at IST Austria for technical
help, M. Dravecka for performing initial experiments, A. Schier for reading an earlier
version of the manuscript, K.W. Rogers for technical help, and C. Hill, A. Bruce,
and L. Solnica-Krezel for sending plasmids. This work was supported by grants from
the Austrian Science Foundation (FWF): (T560-B17) and (I 812-B12) to V.R. and C.-P.H.,
and from the European Union (EU FP7): (6275) to H.J. A.I.-P. is supported by a Ramon
Areces fellowship.'
article_processing_charge: No
author:
- first_name: Keisuke
full_name: Sako, Keisuke
id: 3BED66BE-F248-11E8-B48F-1D18A9856A87
last_name: Sako
orcid: 0000-0002-6453-8075
- first_name: Saurabh
full_name: Pradhan, Saurabh
last_name: Pradhan
- first_name: Vanessa
full_name: Barone, Vanessa
id: 419EECCC-F248-11E8-B48F-1D18A9856A87
last_name: Barone
orcid: 0000-0003-2676-3367
- first_name: Álvaro
full_name: Inglés Prieto, Álvaro
id: 2A9DB292-F248-11E8-B48F-1D18A9856A87
last_name: Inglés Prieto
orcid: 0000-0002-5409-8571
- first_name: Patrick
full_name: Mueller, Patrick
last_name: Mueller
- first_name: Verena
full_name: Ruprecht, Verena
id: 4D71A03A-F248-11E8-B48F-1D18A9856A87
last_name: Ruprecht
orcid: 0000-0003-4088-8633
- first_name: Daniel
full_name: Capek, Daniel
id: 31C42484-F248-11E8-B48F-1D18A9856A87
last_name: Capek
orcid: 0000-0001-5199-9940
- first_name: Sanjeev
full_name: Galande, Sanjeev
last_name: Galande
- first_name: Harald L
full_name: Janovjak, Harald L
id: 33BA6C30-F248-11E8-B48F-1D18A9856A87
last_name: Janovjak
orcid: 0000-0002-8023-9315
- first_name: Carl-Philipp J
full_name: Heisenberg, Carl-Philipp J
id: 39427864-F248-11E8-B48F-1D18A9856A87
last_name: Heisenberg
orcid: 0000-0002-0912-4566
citation:
ama: Sako K, Pradhan S, Barone V, et al. Optogenetic control of nodal signaling
reveals a temporal pattern of nodal signaling regulating cell fate specification
during gastrulation. Cell Reports. 2016;16(3):866-877. doi:10.1016/j.celrep.2016.06.036
apa: Sako, K., Pradhan, S., Barone, V., Inglés Prieto, Á., Mueller, P., Ruprecht,
V., … Heisenberg, C.-P. J. (2016). Optogenetic control of nodal signaling reveals
a temporal pattern of nodal signaling regulating cell fate specification during
gastrulation. Cell Reports. Cell Press. https://doi.org/10.1016/j.celrep.2016.06.036
chicago: Sako, Keisuke, Saurabh Pradhan, Vanessa Barone, Álvaro Inglés Prieto, Patrick
Mueller, Verena Ruprecht, Daniel Capek, Sanjeev Galande, Harald L Janovjak, and
Carl-Philipp J Heisenberg. “Optogenetic Control of Nodal Signaling Reveals a Temporal
Pattern of Nodal Signaling Regulating Cell Fate Specification during Gastrulation.”
Cell Reports. Cell Press, 2016. https://doi.org/10.1016/j.celrep.2016.06.036.
ieee: K. Sako et al., “Optogenetic control of nodal signaling reveals a temporal
pattern of nodal signaling regulating cell fate specification during gastrulation,”
Cell Reports, vol. 16, no. 3. Cell Press, pp. 866–877, 2016.
ista: Sako K, Pradhan S, Barone V, Inglés Prieto Á, Mueller P, Ruprecht V, Capek
D, Galande S, Janovjak HL, Heisenberg C-PJ. 2016. Optogenetic control of nodal
signaling reveals a temporal pattern of nodal signaling regulating cell fate specification
during gastrulation. Cell Reports. 16(3), 866–877.
mla: Sako, Keisuke, et al. “Optogenetic Control of Nodal Signaling Reveals a Temporal
Pattern of Nodal Signaling Regulating Cell Fate Specification during Gastrulation.”
Cell Reports, vol. 16, no. 3, Cell Press, 2016, pp. 866–77, doi:10.1016/j.celrep.2016.06.036.
short: K. Sako, S. Pradhan, V. Barone, Á. Inglés Prieto, P. Mueller, V. Ruprecht,
D. Capek, S. Galande, H.L. Janovjak, C.-P.J. Heisenberg, Cell Reports 16 (2016)
866–877.
date_created: 2018-12-11T11:50:08Z
date_published: 2016-07-19T00:00:00Z
date_updated: 2026-04-25T22:31:36Z
day: '19'
ddc:
- '570'
- '576'
department:
- _id: CaHe
- _id: HaJa
doi: 10.1016/j.celrep.2016.06.036
ec_funded: 1
external_id:
isi:
- '000380264200024'
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:04Z
date_updated: 2018-12-12T10:11:04Z
file_id: '4857'
file_name: IST-2017-754-v1+1_1-s2.0-S2211124716307768-main.pdf
file_size: 3921947
relation: main_file
file_date_updated: 2018-12-12T10:11:04Z
has_accepted_license: '1'
intvolume: ' 16'
isi: 1
issue: '3'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 866 - 877
project:
- _id: 2529486C-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: T 560-B17
name: Cell- and Tissue Mechanics in Zebrafish Germ Layer Formation
- _id: 2527D5CC-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: I812-B12
name: Cell Cortex and Germ Layer Formation in Zebrafish Gastrulation
- _id: 25548C20-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '303564'
name: Microbial Ion Channels for Synthetic Neurobiology
publication: Cell Reports
publication_status: published
publisher: Cell Press
publist_id: '6275'
pubrep_id: '754'
quality_controlled: '1'
related_material:
record:
- id: '961'
relation: dissertation_contains
status: public
- id: '50'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Optogenetic control of nodal signaling reveals a temporal pattern of nodal
signaling regulating cell fate specification during gastrulation
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 16
year: '2016'
...
---
_id: '1437'
abstract:
- lang: eng
text: We study algorithmic questions for concurrent systems where the transitions
are labeled from a complete, closed semiring, and path properties are algebraic
with semiring operations. The algebraic path properties can model dataflow analysis
problems, the shortest path problem, and many other natural problems that arise
in program analysis. We consider that each component of the concurrent system
is a graph with constant treewidth, a property satisfied by the controlflow graphs
of most programs. We allow for multiple possible queries, which arise naturally
in demand driven dataflow analysis. The study of multiple queries allows us to
consider the tradeoff between the resource usage of the one-time preprocessing
and for each individual query. The traditional approach constructs the product
graph of all components and applies the best-known graph algorithm on the product.
In this approach, even the answer to a single query requires the transitive closure
(i.e., the results of all possible queries), which provides no room for tradeoff
between preprocessing and query time. Our main contributions are algorithms that
significantly improve the worst-case running time of the traditional approach,
and provide various tradeoffs depending on the number of queries. For example,
in a concurrent system of two components, the traditional approach requires hexic
time in the worst case for answering one query as well as computing the transitive
closure, whereas we show that with one-time preprocessing in almost cubic time,
each subsequent query can be answered in at most linear time, and even the transitive
closure can be computed in almost quartic time. Furthermore, we establish conditional
optimality results showing that the worst-case running time of our algorithms
cannot be improved without achieving major breakthroughs in graph algorithms (i.e.,
improving the worst-case bound for the shortest path problem in general graphs).
Preliminary experimental results show that our algorithms perform favorably on
several benchmarks.
alternative_title:
- POPL
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Amir
full_name: Goharshady, Amir
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: 'Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. Algorithms for
algebraic path properties in concurrent systems of constant treewidth components.
In: Vol 20-22. ACM; 2016:733-747. doi:10.1145/2837614.2837624'
apa: 'Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., & Pavlogiannis, A.
(2016). Algorithms for algebraic path properties in concurrent systems of constant
treewidth components (Vol. 20–22, pp. 733–747). Presented at the POPL: Principles
of Programming Languages, St. Petersburg, FL, USA: ACM. https://doi.org/10.1145/2837614.2837624'
chicago: Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen,
and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent
Systems of Constant Treewidth Components,” 20–22:733–47. ACM, 2016. https://doi.org/10.1145/2837614.2837624.
ieee: 'K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and A. Pavlogiannis, “Algorithms
for algebraic path properties in concurrent systems of constant treewidth components,”
presented at the POPL: Principles of Programming Languages, St. Petersburg, FL,
USA, 2016, vol. 20–22, pp. 733–747.'
ista: 'Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. 2016. Algorithms
for algebraic path properties in concurrent systems of constant treewidth components.
POPL: Principles of Programming Languages, POPL, vol. 20–22, 733–747.'
mla: Chatterjee, Krishnendu, et al. Algorithms for Algebraic Path Properties
in Concurrent Systems of Constant Treewidth Components. Vol. 20–22, ACM, 2016,
pp. 733–47, doi:10.1145/2837614.2837624.
short: K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, ACM,
2016, pp. 733–747.
conference:
end_date: 2016-01-22
location: St. Petersburg, FL, USA
name: 'POPL: Principles of Programming Languages'
start_date: 2016-01-20
corr_author: '1'
date_created: 2018-12-11T11:52:01Z
date_published: 2016-01-11T00:00:00Z
date_updated: 2026-04-25T22:31:40Z
day: '11'
department:
- _id: KrCh
doi: 10.1145/2837614.2837624
ec_funded: 1
external_id:
arxiv:
- '1510.07565'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1510.07565
month: '01'
oa: 1
oa_version: Preprint
page: 733 - 747
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
publication_status: published
publisher: ACM
publist_id: '5761'
quality_controlled: '1'
related_material:
record:
- id: '5441'
relation: earlier_version
status: public
- id: '5442'
relation: earlier_version
status: public
- id: '6009'
relation: later_version
status: public
- id: '821'
relation: dissertation_contains
status: public
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Algorithms for algebraic path properties in concurrent systems of constant
treewidth components
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 20-22
year: '2016'
...
---
_id: '1386'
abstract:
- lang: eng
text: We consider nondeterministic probabilistic programs with the most basic liveness
property of termination. We present efficient methods for termination analysis
of nondeterministic probabilistic programs with polynomial guards and assignments.
Our approach is through synthesis of polynomial ranking supermartingales, that
on one hand significantly generalizes linear ranking supermartingales and on the
other hand is a counterpart of polynomial ranking-functions for proving termination
of nonprobabilistic programs. The approach synthesizes polynomial ranking-supermartingales
through Positivstellensatz's, yielding an efficient method which is not only sound,
but also semi-complete over a large subclass of programs. We show experimental
results to demonstrate that our approach can handle several classical programs
with complex polynomial guards and assignments, and can synthesize efficient quadratic
ranking-supermartingales when a linear one does not exist even for simple affine
programs.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Hongfei
full_name: Fu, Hongfei
id: 3AAD03D6-F248-11E8-B48F-1D18A9856A87
last_name: Fu
- first_name: Amir
full_name: Goharshady, Amir
id: 391365CE-F248-11E8-B48F-1D18A9856A87
last_name: Goharshady
orcid: 0000-0003-1702-6584
citation:
ama: 'Chatterjee K, Fu H, Goharshady AK. Termination analysis of probabilistic programs
through Positivstellensatz’s. In: Vol 9779. Springer; 2016:3-22. doi:10.1007/978-3-319-41528-4_1'
apa: 'Chatterjee, K., Fu, H., & Goharshady, A. K. (2016). Termination analysis
of probabilistic programs through Positivstellensatz’s (Vol. 9779, pp. 3–22).
Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer.
https://doi.org/10.1007/978-3-319-41528-4_1'
chicago: Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Termination
Analysis of Probabilistic Programs through Positivstellensatz’s,” 9779:3–22. Springer,
2016. https://doi.org/10.1007/978-3-319-41528-4_1.
ieee: 'K. Chatterjee, H. Fu, and A. K. Goharshady, “Termination analysis of probabilistic
programs through Positivstellensatz’s,” presented at the CAV: Computer Aided Verification,
Toronto, Canada, 2016, vol. 9779, pp. 3–22.'
ista: 'Chatterjee K, Fu H, Goharshady AK. 2016. Termination analysis of probabilistic
programs through Positivstellensatz’s. CAV: Computer Aided Verification, LNCS,
vol. 9779, 3–22.'
mla: Chatterjee, Krishnendu, et al. Termination Analysis of Probabilistic Programs
through Positivstellensatz’s. Vol. 9779, Springer, 2016, pp. 3–22, doi:10.1007/978-3-319-41528-4_1.
short: K. Chatterjee, H. Fu, A.K. Goharshady, in:, Springer, 2016, pp. 3–22.
conference:
end_date: 2016-07-23
location: Toronto, Canada
name: 'CAV: Computer Aided Verification'
start_date: 2016-07-17
corr_author: '1'
date_created: 2018-12-11T11:51:43Z
date_published: 2016-07-01T00:00:00Z
date_updated: 2026-04-25T22:31:40Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-319-41528-4_1
ec_funded: 1
external_id:
arxiv:
- '1604.07169'
isi:
- '000387731200001'
intvolume: ' 9779'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1604.07169
month: '07'
oa: 1
oa_version: Preprint
page: 3 - 22
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '5824'
quality_controlled: '1'
related_material:
record:
- id: '8934'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Termination analysis of probabilistic programs through Positivstellensatz's
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9779
year: '2016'
...