---
_id: '4380'
abstract:
- lang: eng
text: Cloud computing is an emerging paradigm aimed to offer users pay-per-use computing
resources, while leaving the burden of managing the computing infrastructure to
the cloud provider. We present a new programming and pricing model that gives
the cloud user the flexibility of trading execution speed and price on a per-job
basis. We discuss the scheduling and resource management challenges for the cloud
provider that arise in the implementation of this model. We argue that techniques
from real-time and embedded software can be useful in this context.
author:
- 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: Anmol
full_name: Tomar, Anmol
id: 3D8D36B6-F248-11E8-B48F-1D18A9856A87
last_name: Tomar
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. A marketplace for cloud
resources. In: ACM; 2010:1-8. doi:10.1145/1879021.1879022'
apa: 'Henzinger, T. A., Tomar, A., Singh, V., Wies, T., & Zufferey, D. (2010).
A marketplace for cloud resources (pp. 1–8). Presented at the EMSOFT: Embedded
Software , Arizona, USA: ACM. https://doi.org/10.1145/1879021.1879022'
chicago: Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien Zufferey.
“A Marketplace for Cloud Resources,” 1–8. ACM, 2010. https://doi.org/10.1145/1879021.1879022.
ieee: 'T. A. Henzinger, A. Tomar, V. Singh, T. Wies, and D. Zufferey, “A marketplace
for cloud resources,” presented at the EMSOFT: Embedded Software , Arizona, USA,
2010, pp. 1–8.'
ista: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. A marketplace for
cloud resources. EMSOFT: Embedded Software , 1–8.'
mla: Henzinger, Thomas A., et al. A Marketplace for Cloud Resources. ACM,
2010, pp. 1–8, doi:10.1145/1879021.1879022.
short: T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2010,
pp. 1–8.
conference:
end_date: 2010-10-29
location: Arizona, USA
name: 'EMSOFT: Embedded Software '
start_date: 2010-10-24
date_created: 2018-12-11T12:08:33Z
date_published: 2010-10-24T00:00:00Z
date_updated: 2021-01-12T07:56:32Z
day: '24'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1145/1879021.1879022
file:
- access_level: open_access
checksum: 7680dd24016810710f7c977bc94f85e9
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:42Z
date_updated: 2020-07-14T12:46:28Z
file_id: '4767'
file_name: IST-2012-48-v1+1_A_marketplace_for_cloud_resources.pdf
file_size: 222626
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 1 - 8
publication_status: published
publisher: ACM
publist_id: '1078'
pubrep_id: '48'
quality_controlled: '1'
scopus_import: 1
status: public
title: A marketplace for cloud resources
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '4381'
abstract:
- lang: eng
text: Cloud computing aims to give users virtually unlimited pay-per-use computing
resources without the burden of managing the underlying infrastructure. We claim
that, in order to realize the full potential of cloud computing, the user must
be presented with a pricing model that offers flexibility at the requirements
level, such as a choice between different degrees of execution speed and the cloud
provider must be presented with a programming model that offers flexibility at
the execution level, such as a choice between different scheduling policies. In
such a flexible framework, with each job, the user purchases a virtual computer
with the desired speed and cost characteristics, and the cloud provider can optimize
the utilization of resources across a stream of jobs from different users. We
designed a flexible framework to test our hypothesis, which is called FlexPRICE
(Flexible Provisioning of Resources in a Cloud Environment) and works as follows.
A user presents a job to the cloud. The cloud finds different schedules to execute
the job and presents a set of quotes to the user in terms of price and duration
for the execution. The user then chooses a particular quote and the cloud is obliged
to execute the job according to the chosen quote. FlexPRICE thus hides the complexity
of the actual scheduling decisions from the user, but still provides enough flexibility
to meet the users actual demands. We implemented FlexPRICE in a simulator called
PRICES that allows us to experiment with our framework. We observe that FlexPRICE
provides a wide range of execution options-from fast and expensive to slow and
cheap-- for the whole spectrum of data-intensive and computation-intensive jobs.
We also observe that the set of quotes computed by FlexPRICE do not vary as the
number of simultaneous jobs increases.
article_processing_charge: No
author:
- 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: Anmol
full_name: Tomar, Anmol
id: 3D8D36B6-F248-11E8-B48F-1D18A9856A87
last_name: Tomar
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. FlexPRICE: Flexible provisioning
of resources in a cloud environment. In: IEEE; 2010:83-90. doi:10.1109/CLOUD.2010.71'
apa: 'Henzinger, T. A., Tomar, A., Singh, V., Wies, T., & Zufferey, D. (2010).
FlexPRICE: Flexible provisioning of resources in a cloud environment (pp. 83–90).
Presented at the CLOUD: Cloud Computing, Miami, USA: IEEE. https://doi.org/10.1109/CLOUD.2010.71'
chicago: 'Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien
Zufferey. “FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment,”
83–90. IEEE, 2010. https://doi.org/10.1109/CLOUD.2010.71.'
ieee: 'T. A. Henzinger, A. Tomar, V. Singh, T. Wies, and D. Zufferey, “FlexPRICE:
Flexible provisioning of resources in a cloud environment,” presented at the CLOUD:
Cloud Computing, Miami, USA, 2010, pp. 83–90.'
ista: 'Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. FlexPRICE: Flexible
provisioning of resources in a cloud environment. CLOUD: Cloud Computing, 83–90.'
mla: 'Henzinger, Thomas A., et al. FlexPRICE: Flexible Provisioning of Resources
in a Cloud Environment. IEEE, 2010, pp. 83–90, doi:10.1109/CLOUD.2010.71.'
short: T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, IEEE, 2010,
pp. 83–90.
conference:
end_date: 2010-07-10
location: Miami, USA
name: 'CLOUD: Cloud Computing'
start_date: 2010-07-05
date_created: 2018-12-11T12:08:33Z
date_published: 2010-08-26T00:00:00Z
date_updated: 2021-01-12T07:56:33Z
day: '26'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1109/CLOUD.2010.71
file:
- access_level: open_access
checksum: 98e534675339a8e2beca08890d048145
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:03Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5188'
file_name: IST-2012-47-v1+1_FlexPRICE-_Flexible_provisioning_of_resources_in_a_cloud_environment.pdf
file_size: 467436
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 83 - 90
publication_status: published
publisher: IEEE
publist_id: '1077'
pubrep_id: '47'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'FlexPRICE: Flexible provisioning of resources in a cloud environment'
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '4382'
abstract:
- lang: eng
text: 'Transactional memory (TM) has shown potential to simplify the task of writing
concurrent programs. Inspired by classical work on databases, formal definitions
of the semantics of TM executions have been proposed. Many of these definitions
assumed that accesses to shared data are solely performed through transactions.
In practice, due to legacy code and concurrency libraries, transactions in a TM
have to share data with non-transactional operations. The semantics of such interaction,
while widely discussed by practitioners, lacks a clear formal specification. Those
interactions can vary, sometimes in subtle ways, between TM implementations and
underlying memory models. We propose a correctness condition for TMs, parametrized
opacity, to formally capture the now folklore notion of strong atomicity by stipulating
the two following intuitive requirements: first, every transaction appears as
if it is executed instantaneously with respect to other transactions and non-transactional
operations, and second, non-transactional operations conform to the given underlying
memory model. We investigate the inherent cost of implementing parametrized opacity.
We first prove that parametrized opacity requires either instrumenting non-transactional
operations (for most memory models) or writing to memory by transactions using
potentially expensive read-modify-write instructions (such as compare-and-swap).
Then, we show that for a class of practical relaxed memory models, parametrized
opacity can indeed be implemented with constant-time instrumentation of non-transactional
writes and no instrumentation of non-transactional reads. We show that, in practice,
parametrizing the notion of correctness allows developing more efficient TM implementations.'
author:
- first_name: Rachid
full_name: Guerraoui, Rachid
last_name: Guerraoui
- 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: Michal
full_name: Kapalka, Michal
last_name: Kapalka
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: 'Guerraoui R, Henzinger TA, Kapalka M, Singh V. Transactions in the jungle.
In: ACM; 2010:263-272. doi:10.1145/1810479.1810529'
apa: 'Guerraoui, R., Henzinger, T. A., Kapalka, M., & Singh, V. (2010). Transactions
in the jungle (pp. 263–272). Presented at the SPAA: ACM Symposium on Parallel
Algorithms and Architectures, Santorini, Greece: ACM. https://doi.org/10.1145/1810479.1810529'
chicago: Guerraoui, Rachid, Thomas A Henzinger, Michal Kapalka, and Vasu Singh.
“Transactions in the Jungle,” 263–72. ACM, 2010. https://doi.org/10.1145/1810479.1810529.
ieee: 'R. Guerraoui, T. A. Henzinger, M. Kapalka, and V. Singh, “Transactions in
the jungle,” presented at the SPAA: ACM Symposium on Parallel Algorithms and Architectures,
Santorini, Greece, 2010, pp. 263–272.'
ista: 'Guerraoui R, Henzinger TA, Kapalka M, Singh V. 2010. Transactions in the
jungle. SPAA: ACM Symposium on Parallel Algorithms and Architectures, 263–272.'
mla: Guerraoui, Rachid, et al. Transactions in the Jungle. ACM, 2010, pp.
263–72, doi:10.1145/1810479.1810529.
short: R. Guerraoui, T.A. Henzinger, M. Kapalka, V. Singh, in:, ACM, 2010, pp. 263–272.
conference:
end_date: 2010-06-15
location: Santorini, Greece
name: 'SPAA: ACM Symposium on Parallel Algorithms and Architectures'
start_date: 2010-06-13
date_created: 2018-12-11T12:08:34Z
date_published: 2010-06-13T00:00:00Z
date_updated: 2021-01-12T07:56:33Z
day: '13'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1145/1810479.1810529
file:
- access_level: open_access
checksum: f2ad6c00a6304da34bf21bcdcfd36c4b
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:28Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5080'
file_name: IST-2012-46-v1+1_Transactions_in_the_jungle.pdf
file_size: 246409
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 263 - 272
publication_status: published
publisher: ACM
publist_id: '1076'
pubrep_id: '46'
quality_controlled: '1'
status: public
title: Transactions in the jungle
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '4388'
abstract:
- lang: eng
text: GIST is a tool that (a) solves the qualitative analysis problem of turn-based
probabilistic games with ω-regular objectives; and (b) synthesizes reasonable
environment assumptions for synthesis of unrealizable specifications. Our tool
provides the first and efficient implementations of several reduction-based techniques
to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic
games for synthesizing environment assumptions for unrealizable specifications.
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: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Barbara
full_name: Jobstmann, Barbara
last_name: Jobstmann
- first_name: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
citation:
ama: 'Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. GIST: A solver for
probabilistic games. In: Vol 6174. Springer; 2010:665-669. doi:10.1007/978-3-642-14295-6_57'
apa: 'Chatterjee, K., Henzinger, T. A., Jobstmann, B., & Radhakrishna, A. (2010).
GIST: A solver for probabilistic games (Vol. 6174, pp. 665–669). Presented at
the CAV: Computer Aided Verification, Edinburgh, UK: Springer. https://doi.org/10.1007/978-3-642-14295-6_57'
chicago: 'Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Arjun
Radhakrishna. “GIST: A Solver for Probabilistic Games,” 6174:665–69. Springer,
2010. https://doi.org/10.1007/978-3-642-14295-6_57.'
ieee: 'K. Chatterjee, T. A. Henzinger, B. Jobstmann, and A. Radhakrishna, “GIST:
A solver for probabilistic games,” presented at the CAV: Computer Aided Verification,
Edinburgh, UK, 2010, vol. 6174, pp. 665–669.'
ista: 'Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. 2010. GIST: A solver
for probabilistic games. CAV: Computer Aided Verification, LNCS, vol. 6174, 665–669.'
mla: 'Chatterjee, Krishnendu, et al. GIST: A Solver for Probabilistic Games.
Vol. 6174, Springer, 2010, pp. 665–69, doi:10.1007/978-3-642-14295-6_57.'
short: K. Chatterjee, T.A. Henzinger, B. Jobstmann, A. Radhakrishna, in:, Springer,
2010, pp. 665–669.
conference:
end_date: 2010-07-17
location: Edinburgh, UK
name: 'CAV: Computer Aided Verification'
start_date: 2010-07-15
date_created: 2018-12-11T12:08:36Z
date_published: 2010-07-01T00:00:00Z
date_updated: 2023-02-23T12:24:17Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-14295-6_57
ec_funded: 1
external_id:
arxiv:
- '1004.2367'
file:
- access_level: open_access
checksum: 0b2ef8c4037ffccc6902d93081af24f7
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:33Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5221'
file_name: IST-2012-43-v1+1_GIST-_A_solver_for_probabilistic_games.pdf
file_size: 293605
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
intvolume: ' 6174'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 665 - 669
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication_status: published
publisher: Springer
publist_id: '1068'
pubrep_id: '43'
quality_controlled: '1'
related_material:
record:
- id: '5393'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: 'GIST: A solver for probabilistic games'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6174
year: '2010'
...
---
_id: '4389'
abstract:
- lang: eng
text: 'Digital components play a central role in the design of complex embedded
systems. These components are interconnected with other, possibly analog, devices
and the physical environment. This environment cannot be entirely captured and
can provide inaccurate input data to the component. It is thus important for digital
components to have a robust behavior, i.e. the presence of a small change in the
input sequences should not result in a drastic change in the output sequences.
In this paper, we study a notion of robustness for sequential circuits. However,
since sequential circuits may have parts that are naturally discontinuous (e.g.,
digital controllers with switching behavior), we need a flexible framework that
accommodates this fact and leaves discontinuous parts of the circuit out from
the robustness analysis. As a consequence, we consider sequential circuits that
have their input variables partitioned into two disjoint sets: control and disturbance
variables. Our contributions are (1) a definition of robustness for sequential
circuits as a form of continuity with respect to disturbance variables, (2) the
characterization of the exact class of sequential circuits that are robust according
to our definition, (3) an algorithm to decide whether a sequential circuit is
robust or not.'
author:
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- 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: Axel
full_name: Legay, Axel
last_name: Legay
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: 'Doyen L, Henzinger TA, Legay A, Nickovic D. Robustness of sequential circuits.
In: IEEE; 2010:77-84. doi:10.1109/ACSD.2010.26'
apa: 'Doyen, L., Henzinger, T. A., Legay, A., & Nickovic, D. (2010). Robustness
of sequential circuits (pp. 77–84). Presented at the ACSD: Application of Concurrency
to System Design, IEEE. https://doi.org/10.1109/ACSD.2010.26'
chicago: Doyen, Laurent, Thomas A Henzinger, Axel Legay, and Dejan Nickovic. “Robustness
of Sequential Circuits,” 77–84. IEEE, 2010. https://doi.org/10.1109/ACSD.2010.26.
ieee: 'L. Doyen, T. A. Henzinger, A. Legay, and D. Nickovic, “Robustness of sequential
circuits,” presented at the ACSD: Application of Concurrency to System Design,
2010, pp. 77–84.'
ista: 'Doyen L, Henzinger TA, Legay A, Nickovic D. 2010. Robustness of sequential
circuits. ACSD: Application of Concurrency to System Design, 77–84.'
mla: Doyen, Laurent, et al. Robustness of Sequential Circuits. IEEE, 2010,
pp. 77–84, doi:10.1109/ACSD.2010.26.
short: L. Doyen, T.A. Henzinger, A. Legay, D. Nickovic, in:, IEEE, 2010, pp. 77–84.
conference:
name: 'ACSD: Application of Concurrency to System Design'
date_created: 2018-12-11T12:08:36Z
date_published: 2010-08-23T00:00:00Z
date_updated: 2021-01-12T07:56:36Z
day: '23'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1109/ACSD.2010.26
file:
- access_level: open_access
checksum: 42b2952bfc6b6974617bd554842b904a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:10Z
date_updated: 2020-07-14T12:46:28Z
file_id: '4733'
file_name: IST-2012-44-v1+1_Robustness_of_sequential_circuits.pdf
file_size: 159920
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 77 - 84
publication_status: published
publisher: IEEE
publist_id: '1069'
pubrep_id: '44'
quality_controlled: '1'
scopus_import: 1
status: public
title: Robustness of sequential circuits
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '4390'
abstract:
- lang: eng
text: Concurrent data structures with fine-grained synchronization are notoriously
difficult to implement correctly. The difficulty of reasoning about these implementations
does not stem from the number of variables or the program size, but rather from
the large number of possible interleavings. These implementations are therefore
prime candidates for model checking. We introduce an algorithm for verifying linearizability
of singly-linked heap-based concurrent data structures. We consider a model consisting
of an unbounded heap where each vertex stores an element from an unbounded data
domain, with a restricted set of operations for testing and updating pointers
and data elements. Our main result is that linearizability is decidable for programs
that invoke a fixed number of methods, possibly in parallel. This decidable fragment
covers many of the common implementation techniques — fine-grained locking, lazy
synchronization, and lock-free synchronization. We also show how the technique
can be used to verify optimistic implementations with the help of programmer annotations.
We developed a verification tool CoLT and evaluated it on a representative sample
of Java implementations of the concurrent set data structure. The tool verified
linearizability of a number of implementations, found a known error in a lock-free
implementation and proved that the corrected version is linearizable.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
- first_name: Swarat
full_name: Chaudhuri, Swarat
last_name: Chaudhuri
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
citation:
ama: 'Cerny P, Radhakrishna A, Zufferey D, Chaudhuri S, Alur R. Model checking of
linearizability of concurrent list implementations. In: Vol 6174. Springer; 2010:465-479.
doi:10.1007/978-3-642-14295-6_41'
apa: 'Cerny, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., & Alur, R. (2010).
Model checking of linearizability of concurrent list implementations (Vol. 6174,
pp. 465–479). Presented at the CAV: Computer Aided Verification, Edinburgh, UK:
Springer. https://doi.org/10.1007/978-3-642-14295-6_41'
chicago: Cerny, Pavol, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, and
Rajeev Alur. “Model Checking of Linearizability of Concurrent List Implementations,”
6174:465–79. Springer, 2010. https://doi.org/10.1007/978-3-642-14295-6_41.
ieee: 'P. Cerny, A. Radhakrishna, D. Zufferey, S. Chaudhuri, and R. Alur, “Model
checking of linearizability of concurrent list implementations,” presented at
the CAV: Computer Aided Verification, Edinburgh, UK, 2010, vol. 6174, pp. 465–479.'
ista: 'Cerny P, Radhakrishna A, Zufferey D, Chaudhuri S, Alur R. 2010. Model checking
of linearizability of concurrent list implementations. CAV: Computer Aided Verification,
LNCS, vol. 6174, 465–479.'
mla: Cerny, Pavol, et al. Model Checking of Linearizability of Concurrent List
Implementations. Vol. 6174, Springer, 2010, pp. 465–79, doi:10.1007/978-3-642-14295-6_41.
short: P. Cerny, A. Radhakrishna, D. Zufferey, S. Chaudhuri, R. Alur, in:, Springer,
2010, pp. 465–479.
conference:
end_date: 2010-07-17
location: Edinburgh, UK
name: 'CAV: Computer Aided Verification'
start_date: 2010-07-15
date_created: 2018-12-11T12:08:36Z
date_published: 2010-07-01T00:00:00Z
date_updated: 2023-02-23T12:24:12Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-14295-6_41
file:
- access_level: open_access
checksum: 2eb211ce40b3c4988bce3a3592980704
content_type: application/pdf
creator: dernst
date_created: 2020-05-19T16:31:56Z
date_updated: 2020-07-14T12:46:28Z
file_id: '7873'
file_name: 2010_CAV_Cerny.pdf
file_size: 3633276
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
intvolume: ' 6174'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 465 - 479
publication_status: published
publisher: Springer
publist_id: '1066'
pubrep_id: '27'
quality_controlled: '1'
related_material:
record:
- id: '5391'
relation: earlier_version
status: public
status: public
title: Model checking of linearizability of concurrent list implementations
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6174
year: '2010'
...
---
_id: '4392'
abstract:
- lang: eng
text: 'While a boolean notion of correctness is given by a preorder on systems and
properties, a quantitative notion of correctness is defined by a distance function
on systems and properties, where the distance between a system and a property
provides a measure of “fit” or “desirability.” In this article, we explore several
ways how the simulation preorder can be generalized to a distance function. This
is done by equipping the classical simulation game between a system and a property
with quantitative objectives. In particular, for systems that satisfy a property,
a quantitative simulation game can measure the “robustness” of the satisfaction,
that is, how much the system can deviate from its nominal behavior while still
satisfying the property. For systems that violate a property, a quantitative simulation
game can measure the “seriousness” of the violation, that is, how much the property
has to be modified so that it is satisfied by the system. These distances can
be computed in polynomial time, since the computation reduces to the value problem
in limit average games with constant weights. Finally, we demonstrate how the
robustness distance can be used to measure how many transmission errors are tolerated
by error correcting codes. '
alternative_title:
- LNCS
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- 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: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
citation:
ama: 'Cerny P, Henzinger TA, Radhakrishna A. Quantitative Simulation Games. In:
Manna Z, Peled D, eds. Time For Verification: Essays in Memory of Amir Pnueli.
Vol 6200. Essays in Memory of Amir Pnueli. Springer; 2010:42-60. doi:10.1007/978-3-642-13754-9_3'
apa: 'Cerny, P., Henzinger, T. A., & Radhakrishna, A. (2010). Quantitative Simulation
Games. In Z. Manna & D. Peled (Eds.), Time For Verification: Essays in
Memory of Amir Pnueli (Vol. 6200, pp. 42–60). Springer. https://doi.org/10.1007/978-3-642-13754-9_3'
chicago: 'Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Quantitative
Simulation Games.” In Time For Verification: Essays in Memory of Amir Pnueli,
edited by Zohar Manna and Doron Peled, 6200:42–60. Essays in Memory of Amir Pnueli.
Springer, 2010. https://doi.org/10.1007/978-3-642-13754-9_3.'
ieee: 'P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Quantitative Simulation
Games,” in Time For Verification: Essays in Memory of Amir Pnueli, vol.
6200, Z. Manna and D. Peled, Eds. Springer, 2010, pp. 42–60.'
ista: 'Cerny P, Henzinger TA, Radhakrishna A. 2010.Quantitative Simulation Games.
In: Time For Verification: Essays in Memory of Amir Pnueli. LNCS, vol. 6200, 42–60.'
mla: 'Cerny, Pavol, et al. “Quantitative Simulation Games.” Time For Verification:
Essays in Memory of Amir Pnueli, edited by Zohar Manna and Doron Peled, vol.
6200, Springer, 2010, pp. 42–60, doi:10.1007/978-3-642-13754-9_3.'
short: 'P. Cerny, T.A. Henzinger, A. Radhakrishna, in:, Z. Manna, D. Peled (Eds.),
Time For Verification: Essays in Memory of Amir Pnueli, Springer, 2010, pp. 42–60.'
date_created: 2018-12-11T12:08:37Z
date_published: 2010-07-29T00:00:00Z
date_updated: 2021-01-12T07:56:38Z
day: '29'
department:
- _id: ToHe
doi: 10.1007/978-3-642-13754-9_3
ec_funded: 1
editor:
- first_name: Zohar
full_name: Manna, Zohar
last_name: Manna
- first_name: Doron
full_name: Peled, Doron
last_name: Peled
intvolume: ' 6200'
language:
- iso: eng
month: '07'
oa_version: None
page: 42 - 60
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication: 'Time For Verification: Essays in Memory of Amir Pnueli'
publication_status: published
publisher: Springer
publist_id: '1064'
quality_controlled: '1'
scopus_import: 1
series_title: Essays in Memory of Amir Pnueli
status: public
title: Quantitative Simulation Games
type: book_chapter
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6200
year: '2010'
...
---
_id: '4393'
abstract:
- lang: eng
text: Boolean notions of correctness are formalized by preorders on systems. Quantitative
measures of correctness can be formalized by real-valued distance functions between
systems, where the distance between implementation and specification provides
a measure of “fit” or “desirability.” We extend the simulation preorder to the
quantitative setting, by making each player of a simulation game pay a certain
price for her choices. We use the resulting games with quantitative objectives
to define three different simulation distances. The correctness distance measures
how much the specification must be changed in order to be satisfied by the implementation.
The coverage distance measures how much the implementation restricts the degrees
of freedom offered by the specification. The robustness distance measures how
much a system can deviate from the implementation description without violating
the specification. We consider these distances for safety as well as liveness
specifications. The distances can be computed in polynomial time for safety specifications,
and for liveness specifications given by weak fairness constraints. We show that
the distance functions satisfy the triangle inequality, that the distance between
two systems does not increase under parallel composition with a third system,
and that the distance between two systems can be bounded from above and below
by distances between abstractions of the two systems. These properties suggest
that our simulation distances provide an appropriate basis for a quantitative
theory of discrete systems. We also demonstrate how the robustness distance can
be used to measure how many transmission errors are tolerated by error correcting
codes.
acknowledgement: This work was partially supported by the European Union project COMBEST
and the European Network of Excellence ArtistDesign.
alternative_title:
- LNCS
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- 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: Arjun
full_name: Radhakrishna, Arjun
id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
last_name: Radhakrishna
citation:
ama: 'Cerny P, Henzinger TA, Radhakrishna A. Simulation distances. In: Vol 6269.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2010:235-268. doi:10.1007/978-3-642-15375-4_18'
apa: 'Cerny, P., Henzinger, T. A., & Radhakrishna, A. (2010). Simulation distances
(Vol. 6269, pp. 235–268). Presented at the CONCUR: Concurrency Theory, Paris,
France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-642-15375-4_18'
chicago: Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Simulation Distances,”
6269:235–68. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. https://doi.org/10.1007/978-3-642-15375-4_18.
ieee: 'P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Simulation distances,” presented
at the CONCUR: Concurrency Theory, Paris, France, 2010, vol. 6269, pp. 235–268.'
ista: 'Cerny P, Henzinger TA, Radhakrishna A. 2010. Simulation distances. CONCUR:
Concurrency Theory, LNCS, vol. 6269, 235–268.'
mla: Cerny, Pavol, et al. Simulation Distances. Vol. 6269, Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 2010, pp. 235–68, doi:10.1007/978-3-642-15375-4_18.
short: P. Cerny, T.A. Henzinger, A. Radhakrishna, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2010, pp. 235–268.
conference:
end_date: 2010-09-03
location: Paris, France
name: 'CONCUR: Concurrency Theory'
start_date: 2010-08-31
date_created: 2018-12-11T12:08:37Z
date_published: 2010-11-01T00:00:00Z
date_updated: 2023-02-23T12:24:04Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-15375-4_18
ec_funded: 1
file:
- access_level: open_access
checksum: ea567903676ba8afe0507ee11313dce5
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:12Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5130'
file_name: IST-2012-42-v1+1_Simulation_distances.pdf
file_size: 198913
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
has_accepted_license: '1'
intvolume: ' 6269'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Submitted Version
page: 235 - 268
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '1065'
pubrep_id: '42'
quality_controlled: '1'
related_material:
record:
- id: '3249'
relation: later_version
status: public
- id: '5389'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Simulation distances
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 6269
year: '2010'
...
---
_id: '4395'
abstract:
- lang: eng
text: The problem of locally transforming or translating programs without altering
their semantics is central to the construction of correct compilers. For concurrent
shared-memory programs this task is challenging because (1) concurrent threads
can observe transformations that would be undetectable in a sequential program,
and (2) contemporary multiprocessors commonly use relaxed memory models that complicate
the reasoning. In this paper, we present a novel proof methodology for verifying
that a local program transformation is sound with respect to a specific hardware
memory model, in the sense that it is not observable in any context. The methodology
is based on a structural induction and relies on a novel compositional denotational
semantics for relaxed memory models that formalizes (1) the behaviors of program
fragments as a set of traces, and (2) the effect of memory model relaxations as
local trace rewrite operations. To apply this methodology in practice, we implemented
a semi- automated tool called Traver and used it to verify/falsify several compiler
transformations for a number of different hardware memory models.
alternative_title:
- LNCS
author:
- first_name: Sebastian
full_name: Burckhardt, Sebastian
last_name: Burckhardt
- first_name: Madanlal
full_name: Musuvathi, Madanlal
last_name: Musuvathi
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: 'Burckhardt S, Musuvathi M, Singh V. Verifying local transformations on relaxed
memory models. In: Gupta R, ed. Vol 6011. Springer; 2010:104-123. doi:10.1007/978-3-642-11970-5_7'
apa: 'Burckhardt, S., Musuvathi, M., & Singh, V. (2010). Verifying local transformations
on relaxed memory models. In R. Gupta (Ed.) (Vol. 6011, pp. 104–123). Presented
at the CC: Compiler Construction, Pahos, Cyprus: Springer. https://doi.org/10.1007/978-3-642-11970-5_7'
chicago: Burckhardt, Sebastian, Madanlal Musuvathi, and Vasu Singh. “Verifying Local
Transformations on Relaxed Memory Models.” edited by Rajiv Gupta, 6011:104–23.
Springer, 2010. https://doi.org/10.1007/978-3-642-11970-5_7.
ieee: 'S. Burckhardt, M. Musuvathi, and V. Singh, “Verifying local transformations
on relaxed memory models,” presented at the CC: Compiler Construction, Pahos,
Cyprus, 2010, vol. 6011, pp. 104–123.'
ista: 'Burckhardt S, Musuvathi M, Singh V. 2010. Verifying local transformations
on relaxed memory models. CC: Compiler Construction, LNCS, vol. 6011, 104–123.'
mla: Burckhardt, Sebastian, et al. Verifying Local Transformations on Relaxed
Memory Models. Edited by Rajiv Gupta, vol. 6011, Springer, 2010, pp. 104–23,
doi:10.1007/978-3-642-11970-5_7.
short: S. Burckhardt, M. Musuvathi, V. Singh, in:, R. Gupta (Ed.), Springer, 2010,
pp. 104–123.
conference:
end_date: 2010-03-28
location: Pahos, Cyprus
name: 'CC: Compiler Construction'
start_date: 2010-03-20
date_created: 2018-12-11T12:08:38Z
date_published: 2010-04-21T00:00:00Z
date_updated: 2021-01-12T07:56:39Z
day: '21'
doi: 10.1007/978-3-642-11970-5_7
editor:
- first_name: Rajiv
full_name: Gupta, Rajiv
last_name: Gupta
extern: '1'
intvolume: ' 6011'
language:
- iso: eng
month: '04'
oa_version: None
page: 104 - 123
publication_status: published
publisher: Springer
publist_id: '1063'
quality_controlled: '1'
status: public
title: Verifying local transformations on relaxed memory models
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6011
year: '2010'
...
---
_id: '4396'
abstract:
- lang: eng
text: 'Shape analysis is a promising technique to prove program properties about
recursive data structures. The challenge is to automatically determine the data-structure
type, and to supply the shape analysis with the necessary information about the
data structure. We present a stepwise approach to the selection of instrumentation
predicates for a TVLA-based shape analysis, which takes us a step closer towards
the fully automatic verification of data structures. The approach uses two techniques
to guide the refinement of shape abstractions: (1) during program exploration,
an explicit heap analysis collects sample instances of the heap structures, which
are used to identify the data structures that are manipulated by the program;
and (2) during abstraction refinement along an infeasible error path, we consider
different possible heap abstractions and choose the coarsest one that eliminates
the infeasible path. We have implemented this combined approach for automatic
shape refinement as an extension of the software model checker BLAST. Example
programs from a data-structure library that manipulate doubly-linked lists and
trees were successfully verified by our tool.'
alternative_title:
- LNCS
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- 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: Grégory
full_name: Théoduloz, Grégory
last_name: Théoduloz
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: 'Beyer D, Henzinger TA, Théoduloz G, Zufferey D. Shape refinement through explicit
heap analysis. In: Rosenblum D, Taenzer G, eds. Vol 6013. Springer; 2010:263-277.
doi:10.1007/978-3-642-12029-9_19'
apa: 'Beyer, D., Henzinger, T. A., Théoduloz, G., & Zufferey, D. (2010). Shape
refinement through explicit heap analysis. In D. Rosenblum & G. Taenzer (Eds.)
(Vol. 6013, pp. 263–277). Presented at the FASE: Fundamental Approaches To Software
Engineering, Paphos, Cyprus: Springer. https://doi.org/10.1007/978-3-642-12029-9_19'
chicago: Beyer, Dirk, Thomas A Henzinger, Grégory Théoduloz, and Damien Zufferey.
“Shape Refinement through Explicit Heap Analysis.” edited by David Rosenblum and
Gabriele Taenzer, 6013:263–77. Springer, 2010. https://doi.org/10.1007/978-3-642-12029-9_19.
ieee: 'D. Beyer, T. A. Henzinger, G. Théoduloz, and D. Zufferey, “Shape refinement
through explicit heap analysis,” presented at the FASE: Fundamental Approaches
To Software Engineering, Paphos, Cyprus, 2010, vol. 6013, pp. 263–277.'
ista: 'Beyer D, Henzinger TA, Théoduloz G, Zufferey D. 2010. Shape refinement through
explicit heap analysis. FASE: Fundamental Approaches To Software Engineering,
LNCS, vol. 6013, 263–277.'
mla: Beyer, Dirk, et al. Shape Refinement through Explicit Heap Analysis.
Edited by David Rosenblum and Gabriele Taenzer, vol. 6013, Springer, 2010, pp.
263–77, doi:10.1007/978-3-642-12029-9_19.
short: D. Beyer, T.A. Henzinger, G. Théoduloz, D. Zufferey, in:, D. Rosenblum, G.
Taenzer (Eds.), Springer, 2010, pp. 263–277.
conference:
end_date: 2010-03-28
location: Paphos, Cyprus
name: 'FASE: Fundamental Approaches To Software Engineering'
start_date: 2010-03-20
date_created: 2018-12-11T12:08:38Z
date_published: 2010-04-21T00:00:00Z
date_updated: 2021-01-12T07:56:40Z
day: '21'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-12029-9_19
editor:
- first_name: David
full_name: Rosenblum, David
last_name: Rosenblum
- first_name: Gabriele
full_name: Taenzer, Gabriele
last_name: Taenzer
file:
- access_level: open_access
checksum: 7d26e59a9681487d7283eba337292b2c
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:13Z
date_updated: 2020-07-14T12:46:29Z
file_id: '5332'
file_name: IST-2012-41-v1+1_Shape_refinement_through_explicit_heap_analysis.pdf
file_size: 312147
relation: main_file
file_date_updated: 2020-07-14T12:46:29Z
has_accepted_license: '1'
intvolume: ' 6013'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Submitted Version
page: 263 - 277
project:
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: Springer
publist_id: '1061'
pubrep_id: '41'
quality_controlled: '1'
scopus_import: 1
status: public
title: Shape refinement through explicit heap analysis
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6013
year: '2010'
...
---
_id: '474'
abstract:
- lang: eng
text: 'Classical models of gene flow fail in three ways: they cannot explain large-scale
patterns; they predict much more genetic diversity than is observed; and they
assume that loosely linked genetic loci evolve independently. We propose a new
model that deals with these problems. Extinction events kill some fraction of
individuals in a region. These are replaced by offspring from a small number of
parents, drawn from the preexisting population. This model of evolution forwards
in time corresponds to a backwards model, in which ancestral lineages jump to
a new location if they are hit by an event, and may coalesce with other lineages
that are hit by the same event. We derive an expression for the identity in allelic
state, and show that, over scales much larger than the largest event, this converges
to the classical value derived by Wright and Malécot. However, rare events that
cover large areas cause low genetic diversity, large-scale patterns, and correlations
in ancestry between unlinked loci.'
acknowledgement: This work has made use of the resources provided by the Edinburgh
Compute and Data Facility (ECDF). The ECDF is partially supported by the eDIKT initiative.
NHB is supported in part by EPSRC Grant EP/E066070/1; JK is supported by EPSRC Grant
EP/E066070/1; and AME is supported in part by EPSRC Grant EP/E065945/1.
author:
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
- first_name: Jerome
full_name: Kelleher, Jerome
last_name: Kelleher
- first_name: Alison
full_name: Etheridge, Alison
last_name: Etheridge
citation:
ama: 'Barton NH, Kelleher J, Etheridge A. A new model for extinction and recolonization
in two dimensions: Quantifying phylogeography. Evolution. 2010;64(9):2701-2715.
doi:10.1111/j.1558-5646.2010.01019.x'
apa: 'Barton, N. H., Kelleher, J., & Etheridge, A. (2010). A new model for extinction
and recolonization in two dimensions: Quantifying phylogeography. Evolution.
Wiley-Blackwell. https://doi.org/10.1111/j.1558-5646.2010.01019.x'
chicago: 'Barton, Nicholas H, Jerome Kelleher, and Alison Etheridge. “A New Model
for Extinction and Recolonization in Two Dimensions: Quantifying Phylogeography.”
Evolution. Wiley-Blackwell, 2010. https://doi.org/10.1111/j.1558-5646.2010.01019.x.'
ieee: 'N. H. Barton, J. Kelleher, and A. Etheridge, “A new model for extinction
and recolonization in two dimensions: Quantifying phylogeography,” Evolution,
vol. 64, no. 9. Wiley-Blackwell, pp. 2701–2715, 2010.'
ista: 'Barton NH, Kelleher J, Etheridge A. 2010. A new model for extinction and
recolonization in two dimensions: Quantifying phylogeography. Evolution. 64(9),
2701–2715.'
mla: 'Barton, Nicholas H., et al. “A New Model for Extinction and Recolonization
in Two Dimensions: Quantifying Phylogeography.” Evolution, vol. 64, no.
9, Wiley-Blackwell, 2010, pp. 2701–15, doi:10.1111/j.1558-5646.2010.01019.x.'
short: N.H. Barton, J. Kelleher, A. Etheridge, Evolution 64 (2010) 2701–2715.
date_created: 2018-12-11T11:46:40Z
date_published: 2010-09-01T00:00:00Z
date_updated: 2021-01-12T08:00:52Z
day: '01'
department:
- _id: NiBa
doi: 10.1111/j.1558-5646.2010.01019.x
intvolume: ' 64'
issue: '9'
language:
- iso: eng
month: '09'
oa_version: None
page: 2701 - 2715
publication: Evolution
publication_status: published
publisher: Wiley-Blackwell
publist_id: '2780'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'A new model for extinction and recolonization in two dimensions: Quantifying
phylogeography'
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 64
year: '2010'
...
---
_id: '488'
abstract:
- lang: eng
text: 'Streaming string transducers [1] define (partial) functions from input strings
to output strings. A streaming string transducer makes a single pass through the
input string and uses a finite set of variables that range over strings from the
output alphabet. At every step, the transducer processes an input symbol, and
updates all the variables in parallel using assignments whose right-hand-sides
are concatenations of output symbols and variables with the restriction that a
variable can be used at most once in a right-hand-side expression. It has been
shown that streaming string transducers operating on strings over infinite data
domains are of interest in algorithmic verification of list-processing programs,
as they lead to PSPACE decision procedures for checking pre/post conditions and
for checking semantic equivalence, for a well-defined class of heap-manipulating
programs. In order to understand the theoretical expressiveness of streaming transducers,
we focus on streaming transducers processing strings over finite alphabets, given
the existence of a robust and well-studied class of "regular" transductions
for this case. Such regular transductions can be defined either by two-way deterministic
finite-state transducers, or using a logical MSO-based characterization. Our main
result is that the expressiveness of streaming string transducers coincides exactly
with this class of regular transductions. '
alternative_title:
- LIPIcs
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
citation:
ama: 'Alur R, Cerny P. Expressiveness of streaming string transducers. In: Vol 8.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2010:1-12. doi:10.4230/LIPIcs.FSTTCS.2010.1'
apa: 'Alur, R., & Cerny, P. (2010). Expressiveness of streaming string transducers
(Vol. 8, pp. 1–12). Presented at the FSTTCS: Foundations of Software Technology
and Theoretical Computer Science, Chennai, India: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2010.1'
chicago: Alur, Rajeev, and Pavol Cerny. “Expressiveness of Streaming String Transducers,”
8:1–12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. https://doi.org/10.4230/LIPIcs.FSTTCS.2010.1.
ieee: 'R. Alur and P. Cerny, “Expressiveness of streaming string transducers,” presented
at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science,
Chennai, India, 2010, vol. 8, pp. 1–12.'
ista: 'Alur R, Cerny P. 2010. Expressiveness of streaming string transducers. FSTTCS:
Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol.
8, 1–12.'
mla: Alur, Rajeev, and Pavol Cerny. Expressiveness of Streaming String Transducers.
Vol. 8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 1–12, doi:10.4230/LIPIcs.FSTTCS.2010.1.
short: R. Alur, P. Cerny, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2010, pp. 1–12.
conference:
end_date: 2010-12-18
location: Chennai, India
name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science'
start_date: 2010-12-15
date_created: 2018-12-11T11:46:45Z
date_published: 2010-01-01T00:00:00Z
date_updated: 2021-01-12T08:01:00Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.FSTTCS.2010.1
file:
- access_level: open_access
checksum: 5845be5aa19791830f7407d8853f2df0
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:29Z
date_updated: 2020-07-14T12:46:35Z
file_id: '4690'
file_name: IST-2018-948-v1+1_2011_Cerny_Expressiveness_of.pdf
file_size: 492344
relation: main_file
file_date_updated: 2020-07-14T12:46:35Z
has_accepted_license: '1'
intvolume: ' 8'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 1 - 12
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '7331'
pubrep_id: '948'
quality_controlled: '1'
scopus_import: 1
status: public
title: Expressiveness of streaming string transducers
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: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 8
year: '2010'
...
---
_id: '489'
abstract:
- lang: eng
text: 'Graph games of infinite length are a natural model for open reactive processes:
one player represents the controller, trying to ensure a given specification,
and the other represents a hostile environment. The evolution of the system depends
on the decisions of both players, supplemented by chance. In this work, we focus
on the notion of randomised strategy. More specifically, we show that three natural
definitions may lead to very different results: in the most general cases, an
almost-surely winning situation may become almost-surely losing if the player
is only allowed to use a weaker notion of strategy. In more reasonable settings,
translations exist, but they require infinite memory, even in simple cases. Finally,
some traditional problems becomes undecidable for the strongest type of strategies.'
alternative_title:
- EPTCS
author:
- first_name: Julien
full_name: Cristau, Julien
last_name: Cristau
- first_name: Claire
full_name: David, Claire
last_name: David
- first_name: Florian
full_name: Horn, Florian
id: 37327ACE-F248-11E8-B48F-1D18A9856A87
last_name: Horn
citation:
ama: 'Cristau J, David C, Horn F. How do we remember the past in randomised strategies?
. In: Proceedings of GandALF 2010. Vol 25. Open Publishing Association;
2010:30-39. doi:10.4204/EPTCS.25.7'
apa: 'Cristau, J., David, C., & Horn, F. (2010). How do we remember the past
in randomised strategies? . In Proceedings of GandALF 2010 (Vol. 25, pp.
30–39). Minori, Amalfi Coast, Italy: Open Publishing Association. https://doi.org/10.4204/EPTCS.25.7'
chicago: Cristau, Julien, Claire David, and Florian Horn. “How Do We Remember the
Past in Randomised Strategies? .” In Proceedings of GandALF 2010, 25:30–39.
Open Publishing Association, 2010. https://doi.org/10.4204/EPTCS.25.7.
ieee: J. Cristau, C. David, and F. Horn, “How do we remember the past in randomised
strategies? ,” in Proceedings of GandALF 2010, Minori, Amalfi Coast, Italy,
2010, vol. 25, pp. 30–39.
ista: 'Cristau J, David C, Horn F. 2010. How do we remember the past in randomised
strategies? . Proceedings of GandALF 2010. GandALF: Games, Automata, Logic, and
Formal Verification, EPTCS, vol. 25, 30–39.'
mla: Cristau, Julien, et al. “How Do We Remember the Past in Randomised Strategies?
.” Proceedings of GandALF 2010, vol. 25, Open Publishing Association, 2010,
pp. 30–39, doi:10.4204/EPTCS.25.7.
short: J. Cristau, C. David, F. Horn, in:, Proceedings of GandALF 2010, Open Publishing
Association, 2010, pp. 30–39.
conference:
end_date: 2010-06-18
location: Minori, Amalfi Coast, Italy
name: 'GandALF: Games, Automata, Logic, and Formal Verification'
start_date: 2010-06-17
date_created: 2018-12-11T11:46:45Z
date_published: 2010-06-09T00:00:00Z
date_updated: 2021-01-12T08:01:01Z
day: '09'
department:
- _id: KrCh
doi: 10.4204/EPTCS.25.7
intvolume: ' 25'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1006.1404v1
month: '06'
oa: 1
oa_version: Published Version
page: 30 - 39
publication: Proceedings of GandALF 2010
publication_status: published
publisher: Open Publishing Association
publist_id: '7332'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'How do we remember the past in randomised strategies? '
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 25
year: '2010'
...
---
_id: '533'
abstract:
- lang: eng
text: Any programming error that can be revealed before compiling a program saves
precious time for the programmer. While integrated development environments already
do a good job by detecting, e.g., data-flow abnormalities, current static analysis
tools suffer from false positives ("noise") or require strong user interaction.
We propose to avoid this deficiency by defining a new class of errors. A program
fragment is doomed if its execution will inevitably fail, regardless of which
state it is started in. We use a formal verification method to identify such errors
fully automatically and, most significantly, without producing noise. We report
on experiments with a prototype tool.
author:
- first_name: Jochen
full_name: Hoenicke, Jochen
last_name: Hoenicke
- first_name: Kari
full_name: Leino, Kari
last_name: Leino
- first_name: Andreas
full_name: Podelski, Andreas
last_name: Podelski
- first_name: Martin
full_name: Schäf, Martin
last_name: Schäf
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
citation:
ama: Hoenicke J, Leino K, Podelski A, Schäf M, Wies T. Doomed program points. Formal
Methods in System Design. 2010;37(2-3):171-199. doi:10.1007/s10703-010-0102-0
apa: Hoenicke, J., Leino, K., Podelski, A., Schäf, M., & Wies, T. (2010). Doomed
program points. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-010-0102-0
chicago: Hoenicke, Jochen, Kari Leino, Andreas Podelski, Martin Schäf, and Thomas
Wies. “Doomed Program Points.” Formal Methods in System Design. Springer,
2010. https://doi.org/10.1007/s10703-010-0102-0.
ieee: J. Hoenicke, K. Leino, A. Podelski, M. Schäf, and T. Wies, “Doomed program
points,” Formal Methods in System Design, vol. 37, no. 2–3. Springer, pp.
171–199, 2010.
ista: Hoenicke J, Leino K, Podelski A, Schäf M, Wies T. 2010. Doomed program points.
Formal Methods in System Design. 37(2–3), 171–199.
mla: Hoenicke, Jochen, et al. “Doomed Program Points.” Formal Methods in System
Design, vol. 37, no. 2–3, Springer, 2010, pp. 171–99, doi:10.1007/s10703-010-0102-0.
short: J. Hoenicke, K. Leino, A. Podelski, M. Schäf, T. Wies, Formal Methods in
System Design 37 (2010) 171–199.
date_created: 2018-12-11T11:47:01Z
date_published: 2010-12-01T00:00:00Z
date_updated: 2021-01-12T08:01:28Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/s10703-010-0102-0
intvolume: ' 37'
issue: 2-3
language:
- iso: eng
month: '12'
oa_version: None
page: 171 - 199
publication: Formal Methods in System Design
publication_status: published
publisher: Springer
publist_id: '7284'
quality_controlled: '1'
scopus_import: 1
status: public
title: Doomed program points
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 37
year: '2010'
...
---
_id: '12654'
abstract:
- lang: eng
text: 'We investigate the transferability of an enhanced temperature-index melt
model that was developed and tested on Haut Glacier d’Arolla, Switzerland, in
the 2001 season. The model’s empirical parameters (temperature factor, TF, and
shortwave radiation factor, SRF) are recalibrated for: (1) other locations on
Haut Glacier d’Arolla; (2) subperiods of distinct meteorological conditions; (3)
different years on Haut Glacier d’Arolla; and (4) other glaciers in different
years. The model parameters are optimized against simulations of an energy-balance
model validated against ablation observations. Results are compared with those
obtained with the original parameters. The model works very well when applied
to other sites, seasons and glaciers, with the exception of overcast conditions.
Differences are due to underestimation of high melt rates. The parameter values
are associated with the prevailing energy-balance conditions, showing that high
SRF are obtained on clear-sky days, whereas higher TF are typical of locations
where glacier winds prevail and turbulent fluxes are high. We also provide a range
of parameters clearly associated with the site’s location and its meteorological
characteristics that could help to assign parameter values to sites where few
data are available.'
article_processing_charge: No
article_type: original
author:
- first_name: Marco
full_name: Carenzo, Marco
last_name: Carenzo
- first_name: Francesca
full_name: Pellicciotti, Francesca
id: b28f055a-81ea-11ed-b70c-a9fe7f7b0e70
last_name: Pellicciotti
- first_name: Stefan
full_name: Rimkus, Stefan
last_name: Rimkus
- first_name: Paolo
full_name: Burlando, Paolo
last_name: Burlando
citation:
ama: Carenzo M, Pellicciotti F, Rimkus S, Burlando P. Assessing the transferability
and robustness of an enhanced temperature-index glacier-melt model. Journal
of Glaciology. 2009;55(190):258-274. doi:10.3189/002214309788608804
apa: Carenzo, M., Pellicciotti, F., Rimkus, S., & Burlando, P. (2009). Assessing
the transferability and robustness of an enhanced temperature-index glacier-melt
model. Journal of Glaciology. Cambridge University Press. https://doi.org/10.3189/002214309788608804
chicago: Carenzo, Marco, Francesca Pellicciotti, Stefan Rimkus, and Paolo Burlando.
“Assessing the Transferability and Robustness of an Enhanced Temperature-Index
Glacier-Melt Model.” Journal of Glaciology. Cambridge University Press,
2009. https://doi.org/10.3189/002214309788608804.
ieee: M. Carenzo, F. Pellicciotti, S. Rimkus, and P. Burlando, “Assessing the transferability
and robustness of an enhanced temperature-index glacier-melt model,” Journal
of Glaciology, vol. 55, no. 190. Cambridge University Press, pp. 258–274,
2009.
ista: Carenzo M, Pellicciotti F, Rimkus S, Burlando P. 2009. Assessing the transferability
and robustness of an enhanced temperature-index glacier-melt model. Journal of
Glaciology. 55(190), 258–274.
mla: Carenzo, Marco, et al. “Assessing the Transferability and Robustness of an
Enhanced Temperature-Index Glacier-Melt Model.” Journal of Glaciology,
vol. 55, no. 190, Cambridge University Press, 2009, pp. 258–74, doi:10.3189/002214309788608804.
short: M. Carenzo, F. Pellicciotti, S. Rimkus, P. Burlando, Journal of Glaciology
55 (2009) 258–274.
date_created: 2023-02-20T08:18:34Z
date_published: 2009-03-01T00:00:00Z
date_updated: 2023-02-20T09:06:27Z
day: '01'
doi: 10.3189/002214309788608804
extern: '1'
intvolume: ' 55'
issue: '190'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.3189/002214309788608804
month: '03'
oa: 1
oa_version: Published Version
page: 258-274
publication: Journal of Glaciology
publication_identifier:
eissn:
- 1727-5652
issn:
- 0022-1430
publication_status: published
publisher: Cambridge University Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: Assessing the transferability and robustness of an enhanced temperature-index
glacier-melt model
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 55
year: '2009'
...
---
_id: '12655'
abstract:
- lang: eng
text: We discuss the inclusion of the subsurface heat-conduction flux into the calculation
of the energy balance and ablation at the glacier–atmosphere interface. Data from
automatic weather stations are used to force an energy-balance model at several
locations on alpine glaciers and at one site in the dry Andes of central Chile.
The heat-conduction flux is computed using a two-layer scheme, assuming that 36%
of the net shortwave radiation is absorbed by the surface layer and that the rest
penetrates into the snowpack. We compare simulations conducted with and without
subsurface heat flux. Results show that assuming a surface temperature of zero
degrees leads to a larger overestimation of melt at the sites in the accumulation
area (10.4–13.3%) than in the ablation area (0.5–2.8%), due to lower air temperatures
and the presence of snow. The difference between simulations with and without
heat conduction is also high at the beginning and end of the ablation season (up
to 29% for the first 15 days of the season), when air temperatures are lower and
snow covers the glacier surface, while they are of little importance during periods
of sustained melt at all the locations investigated.
article_processing_charge: No
article_type: original
author:
- first_name: Francesca
full_name: Pellicciotti, Francesca
id: b28f055a-81ea-11ed-b70c-a9fe7f7b0e70
last_name: Pellicciotti
- first_name: Marco
full_name: Carenzo, Marco
last_name: Carenzo
- first_name: Jakob
full_name: Helbing, Jakob
last_name: Helbing
- first_name: Stefan
full_name: Rimkus, Stefan
last_name: Rimkus
- first_name: Paolo
full_name: Burlando, Paolo
last_name: Burlando
citation:
ama: Pellicciotti F, Carenzo M, Helbing J, Rimkus S, Burlando P. On the role of
subsurface heat conduction in glacier energy-balance modelling. Annals of Glaciology.
2009;50(50):16-24. doi:10.3189/172756409787769555
apa: Pellicciotti, F., Carenzo, M., Helbing, J., Rimkus, S., & Burlando, P.
(2009). On the role of subsurface heat conduction in glacier energy-balance modelling.
Annals of Glaciology. International Glaciological Society. https://doi.org/10.3189/172756409787769555
chicago: Pellicciotti, Francesca, Marco Carenzo, Jakob Helbing, Stefan Rimkus, and
Paolo Burlando. “On the Role of Subsurface Heat Conduction in Glacier Energy-Balance
Modelling.” Annals of Glaciology. International Glaciological Society,
2009. https://doi.org/10.3189/172756409787769555.
ieee: F. Pellicciotti, M. Carenzo, J. Helbing, S. Rimkus, and P. Burlando, “On the
role of subsurface heat conduction in glacier energy-balance modelling,” Annals
of Glaciology, vol. 50, no. 50. International Glaciological Society, pp. 16–24,
2009.
ista: Pellicciotti F, Carenzo M, Helbing J, Rimkus S, Burlando P. 2009. On the role
of subsurface heat conduction in glacier energy-balance modelling. Annals of Glaciology.
50(50), 16–24.
mla: Pellicciotti, Francesca, et al. “On the Role of Subsurface Heat Conduction
in Glacier Energy-Balance Modelling.” Annals of Glaciology, vol. 50, no.
50, International Glaciological Society, 2009, pp. 16–24, doi:10.3189/172756409787769555.
short: F. Pellicciotti, M. Carenzo, J. Helbing, S. Rimkus, P. Burlando, Annals of
Glaciology 50 (2009) 16–24.
date_created: 2023-02-20T08:18:40Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2023-02-20T09:00:53Z
day: '01'
doi: 10.3189/172756409787769555
extern: '1'
intvolume: ' 50'
issue: '50'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.3189/172756409787769555
month: '01'
oa: 1
oa_version: Published Version
page: 16-24
publication: Annals of Glaciology
publication_identifier:
eissn:
- 1727-5644
issn:
- 0260-3055
publication_status: published
publisher: International Glaciological Society
quality_controlled: '1'
scopus_import: '1'
status: public
title: On the role of subsurface heat conduction in glacier energy-balance modelling
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 50
year: '2009'
...
---
_id: '1302'
abstract:
- lang: eng
text: 'The nervous system of seeing animals derives information about optic flow
in two subsequent steps. First, local motion vectors are calculated from moving
retinal images, and second, the spatial distribution of these vectors is analyzed
on the dendrites of large downstream neurons. In dipteran flies, this second step
relies on a set of motion-sensitive lobula plate tangential cells (LPTCs), which
have been studied in great detail in large fly species. Yet, studies on neurons
that convey information to LPTCs and neuroanatomical investigations that enable
a mechanistic understanding of the underlying dendritic computations in LPTCs
are rare. We investigated the subcellular distribution of nicotinic acetylcholine
receptors (nAChRs) on two sets of LPTCs: vertical system (VS) and horizontal system
(HS) cells in Drosophila melanogaster. In this paper, we describe that both cell
types express Dα7-type nAChR subunits specifically on higher order dendritic branches,
similar to the expression of gamma aminobutyric acid (GABA) receptors. These findings
support a model in which directional selectivity of LPTCs is achieved by the dendritic
integration of excitatory, cholinergic, and inhibitory GABA-ergic input from local
motion detectors with opposite preferred direction. Nonetheless, whole-cell recordings
in mutant flies without Dα7 nAChRs revealed that direction selectivity of VS and
HS cells is largely retained. In addition, mutant LPTCs were responsive to acetylcholine
and remaining nAChR receptors were labeled by α-bungarotoxin. These results in
LPTCs with genetically manipulated excitatory input synapses suggest a robust
cellular implementation of dendritic processing that warrants direction selectivity.
The underlying mechanism that ensures appropriate nAChR-mediated synaptic currents
and the functional implications of separate sets or heteromultimeric nAChRs can
now be addressed in this system.'
author:
- first_name: Shamprasad
full_name: Raghu, Shamprasad V
last_name: Raghu
- first_name: Maximilian A
full_name: Maximilian Jösch
id: 2BD278E6-F248-11E8-B48F-1D18A9856A87
last_name: Jösch
orcid: 0000-0002-3937-1330
- first_name: Stephan
full_name: Sigrist, Stephan J
last_name: Sigrist
- first_name: Alexander
full_name: Borst, Alexander
last_name: Borst
- first_name: Dierk
full_name: Reiff, Dierk F
last_name: Reiff
citation:
ama: 'Raghu S, Jösch MA, Sigrist S, Borst A, Reiff D. Synaptic organization of lobula
plate tangential cells in Drosophila: Dα7 cholinergic receptors. Journal of
Neurogenetics. 2009;23(1-2):200-209. doi:10.1080/01677060802471684'
apa: 'Raghu, S., Jösch, M. A., Sigrist, S., Borst, A., & Reiff, D. (2009). Synaptic
organization of lobula plate tangential cells in Drosophila: Dα7 cholinergic receptors.
Journal of Neurogenetics. Informa Healthcare. https://doi.org/10.1080/01677060802471684'
chicago: 'Raghu, Shamprasad, Maximilian A Jösch, Stephan Sigrist, Alexander Borst,
and Dierk Reiff. “Synaptic Organization of Lobula Plate Tangential Cells in Drosophila:
Dα7 Cholinergic Receptors.” Journal of Neurogenetics. Informa Healthcare,
2009. https://doi.org/10.1080/01677060802471684.'
ieee: 'S. Raghu, M. A. Jösch, S. Sigrist, A. Borst, and D. Reiff, “Synaptic organization
of lobula plate tangential cells in Drosophila: Dα7 cholinergic receptors,” Journal
of Neurogenetics, vol. 23, no. 1–2. Informa Healthcare, pp. 200–209, 2009.'
ista: 'Raghu S, Jösch MA, Sigrist S, Borst A, Reiff D. 2009. Synaptic organization
of lobula plate tangential cells in Drosophila: Dα7 cholinergic receptors. Journal
of Neurogenetics. 23(1–2), 200–209.'
mla: 'Raghu, Shamprasad, et al. “Synaptic Organization of Lobula Plate Tangential
Cells in Drosophila: Dα7 Cholinergic Receptors.” Journal of Neurogenetics,
vol. 23, no. 1–2, Informa Healthcare, 2009, pp. 200–09, doi:10.1080/01677060802471684.'
short: S. Raghu, M.A. Jösch, S. Sigrist, A. Borst, D. Reiff, Journal of Neurogenetics
23 (2009) 200–209.
date_created: 2018-12-11T11:51:15Z
date_published: 2009-03-01T00:00:00Z
date_updated: 2021-01-12T06:49:44Z
day: '01'
doi: 10.1080/01677060802471684
extern: 1
intvolume: ' 23'
issue: 1-2
month: '03'
page: 200 - 209
publication: Journal of Neurogenetics
publication_status: published
publisher: Informa Healthcare
publist_id: '5972'
quality_controlled: 0
status: public
title: 'Synaptic organization of lobula plate tangential cells in Drosophila: Dα7
cholinergic receptors'
type: journal_article
volume: 23
year: '2009'
...
---
_id: '8474'
abstract:
- lang: eng
text: Hydrogen bonds are ubiquitous interactions in proteins, and are important
for their folding and functionality. Scalar coupling constants across hydrogen
bonds in the protein backbone, some as small as 0.5 Hz, can be directly measured
in the solid state by NMR spectroscopy (see figure). The nuclei on both sides
of the hydrogen bond can be identified and the size of the coupling constant can
be measured accurately.
article_processing_charge: No
article_type: original
author:
- first_name: Paul
full_name: Schanda, Paul
id: 7B541462-FAF6-11E9-A490-E8DFE5697425
last_name: Schanda
orcid: 0000-0002-9350-7606
- first_name: Matthias
full_name: Huber, Matthias
last_name: Huber
- first_name: René
full_name: Verel, René
last_name: Verel
- first_name: Matthias
full_name: Ernst, Matthias
last_name: Ernst
- first_name: "Beatâ\x80\NH."
full_name: "Meier, Beatâ\x80\NH."
last_name: Meier
citation:
ama: Schanda P, Huber M, Verel R, Ernst M, Meier B. Direct detection of 3hJN’ hydrogen-bond
scalar couplings in proteins by solid-state NMR spectroscopy. Angewandte Chemie
International Edition. 2009;48(49):9322-9325. doi:10.1002/anie.200904411
apa: Schanda, P., Huber, M., Verel, R., Ernst, M., & Meier, B. (2009). Direct
detection of 3hJN’ hydrogen-bond scalar couplings in proteins by solid-state NMR
spectroscopy. Angewandte Chemie International Edition. Wiley. https://doi.org/10.1002/anie.200904411
chicago: "Schanda, Paul, Matthias Huber, René Verel, Matthias Ernst, and Beatâ\x80\NH.
Meier. “Direct Detection of 3hJN’ Hydrogen-Bond Scalar Couplings in Proteins by
Solid-State NMR Spectroscopy.” Angewandte Chemie International Edition.
Wiley, 2009. https://doi.org/10.1002/anie.200904411."
ieee: P. Schanda, M. Huber, R. Verel, M. Ernst, and B. Meier, “Direct detection
of 3hJN’ hydrogen-bond scalar couplings in proteins by solid-state NMR spectroscopy,”
Angewandte Chemie International Edition, vol. 48, no. 49. Wiley, pp. 9322–9325,
2009.
ista: Schanda P, Huber M, Verel R, Ernst M, Meier B. 2009. Direct detection of 3hJN’
hydrogen-bond scalar couplings in proteins by solid-state NMR spectroscopy. Angewandte
Chemie International Edition. 48(49), 9322–9325.
mla: Schanda, Paul, et al. “Direct Detection of 3hJN’ Hydrogen-Bond Scalar Couplings
in Proteins by Solid-State NMR Spectroscopy.” Angewandte Chemie International
Edition, vol. 48, no. 49, Wiley, 2009, pp. 9322–25, doi:10.1002/anie.200904411.
short: P. Schanda, M. Huber, R. Verel, M. Ernst, B. Meier, Angewandte Chemie International
Edition 48 (2009) 9322–9325.
date_created: 2020-09-18T10:11:33Z
date_published: 2009-11-17T00:00:00Z
date_updated: 2021-01-12T08:19:31Z
day: '17'
doi: 10.1002/anie.200904411
extern: '1'
intvolume: ' 48'
issue: '49'
keyword:
- General Chemistry
- Catalysis
language:
- iso: eng
month: '11'
oa_version: None
page: 9322-9325
publication: Angewandte Chemie International Edition
publication_identifier:
issn:
- 1433-7851
- 1521-3773
publication_status: published
publisher: Wiley
quality_controlled: '1'
status: public
title: Direct detection of 3hJN' hydrogen-bond scalar couplings in proteins by solid-state
NMR spectroscopy
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 48
year: '2009'
...
---
_id: '8475'
article_processing_charge: No
article_type: original
author:
- first_name: Paul
full_name: Schanda, Paul
id: 7B541462-FAF6-11E9-A490-E8DFE5697425
last_name: Schanda
orcid: 0000-0002-9350-7606
citation:
ama: 'Schanda P. Fast-pulsing longitudinal relaxation optimized techniques: Enriching
the toolbox of fast biomolecular NMR spectroscopy. Progress in Nuclear Magnetic
Resonance Spectroscopy. 2009;55(3):238-265. doi:10.1016/j.pnmrs.2009.05.002'
apa: 'Schanda, P. (2009). Fast-pulsing longitudinal relaxation optimized techniques:
Enriching the toolbox of fast biomolecular NMR spectroscopy. Progress in Nuclear
Magnetic Resonance Spectroscopy. Elsevier. https://doi.org/10.1016/j.pnmrs.2009.05.002'
chicago: 'Schanda, Paul. “Fast-Pulsing Longitudinal Relaxation Optimized Techniques:
Enriching the Toolbox of Fast Biomolecular NMR Spectroscopy.” Progress in Nuclear
Magnetic Resonance Spectroscopy. Elsevier, 2009. https://doi.org/10.1016/j.pnmrs.2009.05.002.'
ieee: 'P. Schanda, “Fast-pulsing longitudinal relaxation optimized techniques: Enriching
the toolbox of fast biomolecular NMR spectroscopy,” Progress in Nuclear Magnetic
Resonance Spectroscopy, vol. 55, no. 3. Elsevier, pp. 238–265, 2009.'
ista: 'Schanda P. 2009. Fast-pulsing longitudinal relaxation optimized techniques:
Enriching the toolbox of fast biomolecular NMR spectroscopy. Progress in Nuclear
Magnetic Resonance Spectroscopy. 55(3), 238–265.'
mla: 'Schanda, Paul. “Fast-Pulsing Longitudinal Relaxation Optimized Techniques:
Enriching the Toolbox of Fast Biomolecular NMR Spectroscopy.” Progress in Nuclear
Magnetic Resonance Spectroscopy, vol. 55, no. 3, Elsevier, 2009, pp. 238–65,
doi:10.1016/j.pnmrs.2009.05.002.'
short: P. Schanda, Progress in Nuclear Magnetic Resonance Spectroscopy 55 (2009)
238–265.
date_created: 2020-09-18T10:11:42Z
date_published: 2009-10-01T00:00:00Z
date_updated: 2021-01-12T08:19:32Z
day: '01'
doi: 10.1016/j.pnmrs.2009.05.002
extern: '1'
intvolume: ' 55'
issue: '3'
language:
- iso: eng
month: '10'
oa_version: None
page: 238-265
publication: Progress in Nuclear Magnetic Resonance Spectroscopy
publication_identifier:
issn:
- 0079-6565
publication_status: published
publisher: Elsevier
quality_controlled: '1'
status: public
title: 'Fast-pulsing longitudinal relaxation optimized techniques: Enriching the toolbox
of fast biomolecular NMR spectroscopy'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 55
year: '2009'
...
---
_id: '8476'
abstract:
- lang: eng
text: Atomic-resolution information on the structure and dynamics of nucleic acids
is essential for a better understanding of the mechanistic basis of many cellular
processes. NMR spectroscopy is a powerful method for studying the structure and
dynamics of nucleic acids; however, solution NMR studies are currently limited
to relatively small nucleic acids at high concentrations. Thus, technological
and methodological improvements that increase the experimental sensitivity and
spectral resolution of NMR spectroscopy are required for studies of larger nucleic
acids or protein−nucleic acid complexes. Here we introduce a series of imino-proton-detected
NMR experiments that yield an over 2-fold increase in sensitivity compared to
conventional pulse schemes. These methods can be applied to the detection of base
pair interactions, RNA−ligand titration experiments, measurement of residual dipolar
15N−1H couplings, and direct measurements of conformational transitions. These
NMR experiments employ longitudinal spin relaxation enhancement techniques that
have proven useful in protein NMR spectroscopy. The performance of these new experiments
is demonstrated for a 10 kDa TAR-TAR*GA RNA kissing complex and a 26 kDa tRNA.
article_processing_charge: No
article_type: original
author:
- first_name: Jonathan
full_name: Farjon, Jonathan
last_name: Farjon
- first_name: Jérôme
full_name: Boisbouvier, Jérôme
last_name: Boisbouvier
- first_name: Paul
full_name: Schanda, Paul
id: 7B541462-FAF6-11E9-A490-E8DFE5697425
last_name: Schanda
orcid: 0000-0002-9350-7606
- first_name: Arthur
full_name: Pardi, Arthur
last_name: Pardi
- first_name: Jean-Pierre
full_name: Simorre, Jean-Pierre
last_name: Simorre
- first_name: Bernhard
full_name: Brutscher, Bernhard
last_name: Brutscher
citation:
ama: Farjon J, Boisbouvier J, Schanda P, Pardi A, Simorre J-P, Brutscher B. Longitudinal-relaxation-enhanced
NMR experiments for the study of nucleic acids in solution. Journal of the
American Chemical Society. 2009;131(24):8571-8577. doi:10.1021/ja901633y
apa: Farjon, J., Boisbouvier, J., Schanda, P., Pardi, A., Simorre, J.-P., &
Brutscher, B. (2009). Longitudinal-relaxation-enhanced NMR experiments for the
study of nucleic acids in solution. Journal of the American Chemical Society.
American Chemical Society. https://doi.org/10.1021/ja901633y
chicago: Farjon, Jonathan, Jérôme Boisbouvier, Paul Schanda, Arthur Pardi, Jean-Pierre
Simorre, and Bernhard Brutscher. “Longitudinal-Relaxation-Enhanced NMR Experiments
for the Study of Nucleic Acids in Solution.” Journal of the American Chemical
Society. American Chemical Society, 2009. https://doi.org/10.1021/ja901633y.
ieee: J. Farjon, J. Boisbouvier, P. Schanda, A. Pardi, J.-P. Simorre, and B. Brutscher,
“Longitudinal-relaxation-enhanced NMR experiments for the study of nucleic acids
in solution,” Journal of the American Chemical Society, vol. 131, no. 24.
American Chemical Society, pp. 8571–8577, 2009.
ista: Farjon J, Boisbouvier J, Schanda P, Pardi A, Simorre J-P, Brutscher B. 2009.
Longitudinal-relaxation-enhanced NMR experiments for the study of nucleic acids
in solution. Journal of the American Chemical Society. 131(24), 8571–8577.
mla: Farjon, Jonathan, et al. “Longitudinal-Relaxation-Enhanced NMR Experiments
for the Study of Nucleic Acids in Solution.” Journal of the American Chemical
Society, vol. 131, no. 24, American Chemical Society, 2009, pp. 8571–77, doi:10.1021/ja901633y.
short: J. Farjon, J. Boisbouvier, P. Schanda, A. Pardi, J.-P. Simorre, B. Brutscher,
Journal of the American Chemical Society 131 (2009) 8571–8577.
date_created: 2020-09-18T10:11:49Z
date_published: 2009-06-01T00:00:00Z
date_updated: 2021-01-12T08:19:32Z
day: '01'
doi: 10.1021/ja901633y
extern: '1'
intvolume: ' 131'
issue: '24'
language:
- iso: eng
month: '06'
oa_version: None
page: 8571-8577
publication: Journal of the American Chemical Society
publication_identifier:
issn:
- 0002-7863
- 1520-5126
publication_status: published
publisher: American Chemical Society
quality_controlled: '1'
status: public
title: Longitudinal-relaxation-enhanced NMR experiments for the study of nucleic acids
in solution
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 131
year: '2009'
...