---
_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: '2498'
abstract:
- lang: eng
text: Activation of G protein-gated inwardly-rectifying K+ (GIRK or Kir3) channels
by metabotropic gamma-aminobutyric acid (B) (GABAB) receptors is an essential
signalling pathway controlling neuronal excitability and synaptic transmission
in the brain. To investigate the relationship between GIRK channel subunits and
GABAB receptors in cerebellar Purkinje cells at post- and pre-synaptic sites,
we used biochemical, functional and immunohistochemical techniques. Co-immunoprecipitation
analysis demonstrated that GIRK subunits are co-assembled with GABAB receptors
in the cerebellum. Immunoelectron microscopy showed that the subunit composition
of GIRK channels in Purkinje cell spines is compartment-dependent. Thus, at extrasynaptic
sites GIRK channels are formed by GIRK1/GIRK2/GIRK3, post-synaptic densities contain
GIRK2/GIRK3 and dendritic shafts contain GIRK1/GIRK3. The post-synaptic association
of GIRK subunits with GABAB receptors in Purkinje cells is supported by the subcellular
regulation of the ion channel and the receptor in mutant mice. At pre-synaptic
sites, GIRK channels localized to parallel fibre terminals are formed by GIRK1/GIRK2/GIRK3
and co-localize with GABAB receptors. Consistent with this morphological evidence
we demonstrate their functional interaction at axon terminals in the cerebellum
by showing that GIRK channels play a role in the inhibition of glutamate release
by GABAB receptors. The association of GIRK channels and GABA B receptors with
excitatory synapses at both post- and pre-synaptic sites indicates their intimate
involvement in the modulation of glutamatergic neurotransmission in the cerebellum.
author:
- first_name: Laura
full_name: Fernández-Alacid, Laura
last_name: Fernández Alacid
- first_name: Carolina
full_name: Aguado, Carolina
last_name: Aguado
- first_name: Francisco
full_name: Ciruela, Francisco
last_name: Ciruela
- first_name: Ricardo
full_name: Martín, Ricardo J
last_name: Martín
- first_name: José
full_name: Colón, José
last_name: Colón
- first_name: María
full_name: Cabañero, María José
last_name: Cabañero
- first_name: Martin
full_name: Gassmann, Martin
last_name: Gassmann
- first_name: Masahiko
full_name: Watanabe, Masahiko
last_name: Watanabe
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Kevin
full_name: Wickman, Kevin D
last_name: Wickman
- first_name: Bernhard
full_name: Bettler, Bernhard
last_name: Bettler
- first_name: José
full_name: Sánchez-Prieto, José
last_name: Sánchez Prieto
- first_name: Rafael
full_name: Luján, Rafael
last_name: Luján
citation:
ama: Fernández Alacid L, Aguado C, Ciruela F, et al. Subcellular compartment-specific
molecular diversity of pre- and post-synaptic GABAB-activated GIRK channels in
Purkinje cells. Journal of Neurochemistry. 2009;110(4):1363-1376. doi:10.1111/j.1471-4159.2009.06229.x
apa: Fernández Alacid, L., Aguado, C., Ciruela, F., Martín, R., Colón, J., Cabañero,
M., … Luján, R. (2009). Subcellular compartment-specific molecular diversity
of pre- and post-synaptic GABAB-activated GIRK channels in Purkinje cells. Journal
of Neurochemistry. Wiley-Blackwell. https://doi.org/10.1111/j.1471-4159.2009.06229.x
chicago: Fernández Alacid, Laura, Carolina Aguado, Francisco Ciruela, Ricardo Martín,
José Colón, María Cabañero, Martin Gassmann, et al. “ Subcellular Compartment-Specific
Molecular Diversity of Pre- and Post-Synaptic GABAB-Activated GIRK Channels in
Purkinje Cells.” Journal of Neurochemistry. Wiley-Blackwell, 2009. https://doi.org/10.1111/j.1471-4159.2009.06229.x.
ieee: L. Fernández Alacid et al., “ Subcellular compartment-specific molecular
diversity of pre- and post-synaptic GABAB-activated GIRK channels in Purkinje
cells,” Journal of Neurochemistry, vol. 110, no. 4. Wiley-Blackwell, pp.
1363–1376, 2009.
ista: Fernández Alacid L, Aguado C, Ciruela F, Martín R, Colón J, Cabañero M, Gassmann
M, Watanabe M, Shigemoto R, Wickman K, Bettler B, Sánchez Prieto J, Luján R. 2009. Subcellular
compartment-specific molecular diversity of pre- and post-synaptic GABAB-activated
GIRK channels in Purkinje cells. Journal of Neurochemistry. 110(4), 1363–1376.
mla: Fernández Alacid, Laura, et al. “ Subcellular Compartment-Specific Molecular
Diversity of Pre- and Post-Synaptic GABAB-Activated GIRK Channels in Purkinje
Cells.” Journal of Neurochemistry, vol. 110, no. 4, Wiley-Blackwell, 2009,
pp. 1363–76, doi:10.1111/j.1471-4159.2009.06229.x.
short: L. Fernández Alacid, C. Aguado, F. Ciruela, R. Martín, J. Colón, M. Cabañero,
M. Gassmann, M. Watanabe, R. Shigemoto, K. Wickman, B. Bettler, J. Sánchez Prieto,
R. Luján, Journal of Neurochemistry 110 (2009) 1363–1376.
date_created: 2018-12-11T11:58:01Z
date_published: 2009-08-01T00:00:00Z
date_updated: 2021-01-12T06:57:50Z
day: '01'
doi: 10.1111/j.1471-4159.2009.06229.x
extern: 1
intvolume: ' 110'
issue: '4'
month: '08'
page: 1363 - 1376
publication: Journal of Neurochemistry
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4403'
quality_controlled: 0
status: public
title: ' Subcellular compartment-specific molecular diversity of pre- and post-synaptic
GABAB-activated GIRK channels in Purkinje cells'
type: journal_article
volume: 110
year: '2009'
...
---
_id: '2499'
abstract:
- lang: eng
text: G protein-coupled receptors (GPCRs) have critical functions in intercellular
communication. Although a wide range of different receptors have been identified
in the same cells, the mechanism by which signals are integrated remains elusive.
The ability of GPCRs to form dimers or larger hetero-oligomers is thought to generate
such signal integration. We examined the molecular mechanisms responsible for
the GABAB receptor-mediated potentiation of the mGlu receptor signalling reported
in Purkinje neurons. We showed that this effect does not require a physical interaction
between both receptors. Instead, it is the result of a more general mechanism
in which the βγ subunits produced by the Gi-coupled GABAB receptor enhance the
mGlu-mediated Gq response. Most importantly, this mechanism could be generally
applied to other pairs of Gi- and Gq-coupled receptors and the signal integration
varied depending on the time delay between activation of each receptor. Such a
mechanism helps explain specific properties of cells expressing two different
Gi- and Gq-coupled receptors activated by a single transmitter, or properties
of GPCRs naturally coupled to both types of the G protein.
author:
- first_name: Marie
full_name: Rives, Marie L
last_name: Rives
- first_name: Claire
full_name: Vol, Claire
last_name: Vol
- first_name: Yugo
full_name: Fukazawa, Yugo
last_name: Fukazawa
- first_name: Norbert
full_name: Tinel, Norbert
last_name: Tinel
- first_name: Eric
full_name: Trinquet, Eric
last_name: Trinquet
- first_name: Mohammed
full_name: Ayoub, Mohammed A
last_name: Ayoub
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Jean
full_name: Pin, Jean-Philippe
last_name: Pin
- first_name: Laurent
full_name: Prezèau, Laurent
last_name: Prezèau
citation:
ama: Rives M, Vol C, Fukazawa Y, et al. Crosstalk between GABAB and mGlu1a receptors
reveals new insight into GPCR signal integration. EMBO Journal. 2009;28(15):2195-2208.
doi:10.1038/emboj.2009.177
apa: Rives, M., Vol, C., Fukazawa, Y., Tinel, N., Trinquet, E., Ayoub, M., … Prezèau,
L. (2009). Crosstalk between GABAB and mGlu1a receptors reveals new insight into
GPCR signal integration. EMBO Journal. Wiley-Blackwell. https://doi.org/10.1038/emboj.2009.177
chicago: Rives, Marie, Claire Vol, Yugo Fukazawa, Norbert Tinel, Eric Trinquet,
Mohammed Ayoub, Ryuichi Shigemoto, Jean Pin, and Laurent Prezèau. “Crosstalk between
GABAB and MGlu1a Receptors Reveals New Insight into GPCR Signal Integration.”
EMBO Journal. Wiley-Blackwell, 2009. https://doi.org/10.1038/emboj.2009.177.
ieee: M. Rives et al., “Crosstalk between GABAB and mGlu1a receptors reveals
new insight into GPCR signal integration,” EMBO Journal, vol. 28, no. 15.
Wiley-Blackwell, pp. 2195–2208, 2009.
ista: Rives M, Vol C, Fukazawa Y, Tinel N, Trinquet E, Ayoub M, Shigemoto R, Pin
J, Prezèau L. 2009. Crosstalk between GABAB and mGlu1a receptors reveals new insight
into GPCR signal integration. EMBO Journal. 28(15), 2195–2208.
mla: Rives, Marie, et al. “Crosstalk between GABAB and MGlu1a Receptors Reveals
New Insight into GPCR Signal Integration.” EMBO Journal, vol. 28, no. 15,
Wiley-Blackwell, 2009, pp. 2195–208, doi:10.1038/emboj.2009.177.
short: M. Rives, C. Vol, Y. Fukazawa, N. Tinel, E. Trinquet, M. Ayoub, R. Shigemoto,
J. Pin, L. Prezèau, EMBO Journal 28 (2009) 2195–2208.
date_created: 2018-12-11T11:58:01Z
date_published: 2009-08-15T00:00:00Z
date_updated: 2021-01-12T06:57:51Z
day: '15'
doi: 10.1038/emboj.2009.177
extern: 1
intvolume: ' 28'
issue: '15'
main_file_link:
- open_access: '1'
url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC2726695/
month: '08'
oa: 1
page: 2195 - 2208
publication: EMBO Journal
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4402'
quality_controlled: 0
status: public
title: Crosstalk between GABAB and mGlu1a receptors reveals new insight into GPCR
signal integration
type: journal_article
volume: 28
year: '2009'
...
---
_id: '2500'
abstract:
- lang: eng
text: 'To examine the intrasynaptic arrangement of postsynaptic receptors in relation
to the functional role of the synapse,we quantitatively analyzed the two-dimensional
distribution of AMPA and NMDA receptors (AMPARs and NMDARs, respectively) using
SDS-digested freeze-fracture replica labeling (SDS-FRL) and assessed the implication
of distribution differences on the postsynaptic responses by simulation. In the
dorsal lateral geniculate nucleus, corticogeniculate (CG) synapses were twice
as large as retinogeniculate (RG) synapses but expressed similar numbers of AMPARs.
Two-dimensional views of replicas revealed that AMPARs form microclusters in both
synapses to a similar extent, resulting in larger AMPAR-lacking areas in the CG
synapses. Despite the broad difference in the AMPAR distribution within a synapse,
our simulations based on the actual receptor distributions suggested that the
AMPAR quantal response at individual RG synapses is only slightly larger in amplitude,
less variable, and faster in kinetics than that at CG synapses having a similar
number of the receptors. NMDARs at the CG synapses were expressed twice as many
as those in the RG synapses. Electrophysiological recordings confirmed a larger
contribution of NMDAR relative to AMPAR-mediated responses in CG synapses. We
conclude that synapse size and the density and distribution of receptors have
minor influences on quantal responses and that the number of receptors acts as
a predominant postsynaptic determinant of the synaptic strength mediated by both
the AMPARs and NMDARs. '
author:
- first_name: Etsuko
full_name: Tarusawa, Etsuko
last_name: Tarusawa
- first_name: Ko
full_name: Matsui, Ko
last_name: Matsui
- first_name: Timotheus
full_name: Budisantoso, Timotheus
last_name: Budisantoso
- first_name: Elek
full_name: Molnár, Elek
last_name: Molnár
- first_name: Masahiko
full_name: Watanabe, Masahiko
last_name: Watanabe
- first_name: Minoru
full_name: Matsui, Minoru
last_name: Matsui
- first_name: Yugo
full_name: Fukazawa, Yugo
last_name: Fukazawa
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
citation:
ama: Tarusawa E, Matsui K, Budisantoso T, et al. Input-specific intrasynaptic arrangements
of ionotropic glutamate receptors and their impact on postsynaptic responses.
Journal of Neuroscience. 2009;29(41):12896-12908. doi:10.1523/JNEUROSCI.6160-08.2009
apa: Tarusawa, E., Matsui, K., Budisantoso, T., Molnár, E., Watanabe, M., Matsui,
M., … Shigemoto, R. (2009). Input-specific intrasynaptic arrangements of ionotropic
glutamate receptors and their impact on postsynaptic responses. Journal of
Neuroscience. Society for Neuroscience. https://doi.org/10.1523/JNEUROSCI.6160-08.2009
chicago: Tarusawa, Etsuko, Ko Matsui, Timotheus Budisantoso, Elek Molnár, Masahiko
Watanabe, Minoru Matsui, Yugo Fukazawa, and Ryuichi Shigemoto. “Input-Specific
Intrasynaptic Arrangements of Ionotropic Glutamate Receptors and Their Impact
on Postsynaptic Responses.” Journal of Neuroscience. Society for Neuroscience,
2009. https://doi.org/10.1523/JNEUROSCI.6160-08.2009.
ieee: E. Tarusawa et al., “Input-specific intrasynaptic arrangements of ionotropic
glutamate receptors and their impact on postsynaptic responses,” Journal of
Neuroscience, vol. 29, no. 41. Society for Neuroscience, pp. 12896–12908,
2009.
ista: Tarusawa E, Matsui K, Budisantoso T, Molnár E, Watanabe M, Matsui M, Fukazawa
Y, Shigemoto R. 2009. Input-specific intrasynaptic arrangements of ionotropic
glutamate receptors and their impact on postsynaptic responses. Journal of Neuroscience.
29(41), 12896–12908.
mla: Tarusawa, Etsuko, et al. “Input-Specific Intrasynaptic Arrangements of Ionotropic
Glutamate Receptors and Their Impact on Postsynaptic Responses.” Journal of
Neuroscience, vol. 29, no. 41, Society for Neuroscience, 2009, pp. 12896–908,
doi:10.1523/JNEUROSCI.6160-08.2009.
short: E. Tarusawa, K. Matsui, T. Budisantoso, E. Molnár, M. Watanabe, M. Matsui,
Y. Fukazawa, R. Shigemoto, Journal of Neuroscience 29 (2009) 12896–12908.
date_created: 2018-12-11T11:58:02Z
date_published: 2009-10-14T00:00:00Z
date_updated: 2021-01-12T06:57:52Z
day: '14'
doi: 10.1523/JNEUROSCI.6160-08.2009
extern: 1
intvolume: ' 29'
issue: '41'
month: '10'
page: 12896 - 12908
publication: Journal of Neuroscience
publication_status: published
publisher: Society for Neuroscience
publist_id: '4401'
quality_controlled: 0
status: public
title: Input-specific intrasynaptic arrangements of ionotropic glutamate receptors
and their impact on postsynaptic responses
type: journal_article
volume: 29
year: '2009'
...
---
_id: '2501'
abstract:
- lang: eng
text: The brain-specific immediate early gene Arc/Arg3.1 is induced in response
to a variety of stimuli, including sensory and behavior-linked neural activity.
Here we report the generation of transgenic mice, termed TgArc/Arg3.1-d4EGFP,
expressing a 4-h half-life form of enhanced green fluorescent protein (d4EGFP)
under the control of the Arc/Arg3.1 promoter. We show that d4EGFP-mediated fluorescence
faithfully reports Arc/Arg3.1 induction in response to physiological, pathological
and pharmacological stimuli, and that this fluorescence permits electrical recording
from activated neurons in the live mouse. Moreover, the fluorescent Arc/Arg3.1
indicator revealed activity changes in circumscribed brain areas in distinct modes
of stress and in a mouse model of Alzheimer's disease. These findings identify
the TgArc/Arg3.1-d4EGFP mouse as a versatile tool to monitor Arc/Arg3.1 induction
in neural circuits, both in vitro and in vivo.
author:
- first_name: Valery
full_name: Grinevich, Valery V
last_name: Grinevich
- first_name: Alexander
full_name: Kolleker, Alexander
last_name: Kolleker
- first_name: Marina
full_name: Eliava, Marina I
last_name: Eliava
- first_name: Naoki
full_name: Takada, Naoki
last_name: Takada
- first_name: Hiroshi
full_name: Takuma, Hiroshi
last_name: Takuma
- first_name: Yugo
full_name: Fukazawa, Yugo
last_name: Fukazawa
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Dietmar
full_name: Kuhl, Dietmar
last_name: Kuhl
- first_name: Jack
full_name: Waters, Jack
last_name: Waters
- first_name: Peter
full_name: Seeburg, Peter H
last_name: Seeburg
- first_name: Pavel
full_name: Osten, Pavel
last_name: Osten
citation:
ama: 'Grinevich V, Kolleker A, Eliava M, et al. Fluorescent Arc/Arg3.1 indicator
mice: A versatile tool to study brain activity changes in vitro and in vivo. Journal
of Neuroscience Methods. 2009;184(1):25-36. doi:10.1016/j.jneumeth.2009.07.015'
apa: 'Grinevich, V., Kolleker, A., Eliava, M., Takada, N., Takuma, H., Fukazawa,
Y., … Osten, P. (2009). Fluorescent Arc/Arg3.1 indicator mice: A versatile tool
to study brain activity changes in vitro and in vivo. Journal of Neuroscience
Methods. Elsevier. https://doi.org/10.1016/j.jneumeth.2009.07.015'
chicago: 'Grinevich, Valery, Alexander Kolleker, Marina Eliava, Naoki Takada, Hiroshi
Takuma, Yugo Fukazawa, Ryuichi Shigemoto, et al. “Fluorescent Arc/Arg3.1 Indicator
Mice: A Versatile Tool to Study Brain Activity Changes in Vitro and in Vivo.”
Journal of Neuroscience Methods. Elsevier, 2009. https://doi.org/10.1016/j.jneumeth.2009.07.015.'
ieee: 'V. Grinevich et al., “Fluorescent Arc/Arg3.1 indicator mice: A versatile
tool to study brain activity changes in vitro and in vivo,” Journal of Neuroscience
Methods, vol. 184, no. 1. Elsevier, pp. 25–36, 2009.'
ista: 'Grinevich V, Kolleker A, Eliava M, Takada N, Takuma H, Fukazawa Y, Shigemoto
R, Kuhl D, Waters J, Seeburg P, Osten P. 2009. Fluorescent Arc/Arg3.1 indicator
mice: A versatile tool to study brain activity changes in vitro and in vivo. Journal
of Neuroscience Methods. 184(1), 25–36.'
mla: 'Grinevich, Valery, et al. “Fluorescent Arc/Arg3.1 Indicator Mice: A Versatile
Tool to Study Brain Activity Changes in Vitro and in Vivo.” Journal of Neuroscience
Methods, vol. 184, no. 1, Elsevier, 2009, pp. 25–36, doi:10.1016/j.jneumeth.2009.07.015.'
short: V. Grinevich, A. Kolleker, M. Eliava, N. Takada, H. Takuma, Y. Fukazawa,
R. Shigemoto, D. Kuhl, J. Waters, P. Seeburg, P. Osten, Journal of Neuroscience
Methods 184 (2009) 25–36.
date_created: 2018-12-11T11:58:02Z
date_published: 2009-10-30T00:00:00Z
date_updated: 2021-01-12T06:57:52Z
day: '30'
doi: 10.1016/j.jneumeth.2009.07.015
extern: 1
intvolume: ' 184'
issue: '1'
month: '10'
page: 25 - 36
publication: Journal of Neuroscience Methods
publication_status: published
publisher: Elsevier
publist_id: '4400'
quality_controlled: 0
status: public
title: 'Fluorescent Arc/Arg3.1 indicator mice: A versatile tool to study brain activity
changes in vitro and in vivo'
type: journal_article
volume: 184
year: '2009'
...
---
_id: '2502'
abstract:
- lang: eng
text: In order to acquire phase-contrast images with adequate contrast, conventional
TEM requires large amount of defocus. Increasing the defocus improves the low-frequency
components but attenuates the high-frequency ones. On the other hand, Zernike
phase-contrast TEM (ZPC-TEM) can recover low-frequency components without losing
the high-frequency ones under in-focus conditions. ZPC-TEM however, has another
problem, especially in imaging of complex biological specimens such as cells and
tissues; strong halos appear around specimen structures, and these halos hinder
the interpretation of images. Due to this problem, the application of ZPC-TEM
has been restricted to imaging of smaller particles. In order to improve the halo
appearance, we fabricated a new quarter-wave thin film phase-plate with a smaller
central hole and tested it on vitreous biological specimens. ZPC-TEM with the
new plate could successfully visualize, in in-focus images, the intracellular
fine features of cultured cells and brain tissues. This result indicates that
reduction of the central hole diameter makes ZPC-TEM applicable on size scales
ranging from protein particles to tissue sections. The application of ZPC-TEM
to vitreous biological specimens will be a powerful method to advance the new
field of imaging science for ultrastructures in close-to-physiological state.
author:
- first_name: Yoshiyuki
full_name: Fukuda, Yoshiyuki
last_name: Fukuda
- first_name: Yugo
full_name: Fukazawa, Yugo
last_name: Fukazawa
- first_name: Radostin
full_name: Danev, Radostin S
last_name: Danev
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Kuniaki
full_name: Nagayama, Kuniaki
last_name: Nagayama
citation:
ama: Fukuda Y, Fukazawa Y, Danev R, Shigemoto R, Nagayama K. Tuning of the Zernike
phase-plate for visualization of detailed ultrastructure in complex biological
specimens. Journal of Structural Biology. 2009;168(3):476-484. doi:10.1016/j.jsb.2009.08.011
apa: Fukuda, Y., Fukazawa, Y., Danev, R., Shigemoto, R., & Nagayama, K. (2009).
Tuning of the Zernike phase-plate for visualization of detailed ultrastructure
in complex biological specimens. Journal of Structural Biology. Academic
Press. https://doi.org/10.1016/j.jsb.2009.08.011
chicago: Fukuda, Yoshiyuki, Yugo Fukazawa, Radostin Danev, Ryuichi Shigemoto, and
Kuniaki Nagayama. “Tuning of the Zernike Phase-Plate for Visualization of Detailed
Ultrastructure in Complex Biological Specimens.” Journal of Structural Biology.
Academic Press, 2009. https://doi.org/10.1016/j.jsb.2009.08.011.
ieee: Y. Fukuda, Y. Fukazawa, R. Danev, R. Shigemoto, and K. Nagayama, “Tuning of
the Zernike phase-plate for visualization of detailed ultrastructure in complex
biological specimens,” Journal of Structural Biology, vol. 168, no. 3.
Academic Press, pp. 476–484, 2009.
ista: Fukuda Y, Fukazawa Y, Danev R, Shigemoto R, Nagayama K. 2009. Tuning of the
Zernike phase-plate for visualization of detailed ultrastructure in complex biological
specimens. Journal of Structural Biology. 168(3), 476–484.
mla: Fukuda, Yoshiyuki, et al. “Tuning of the Zernike Phase-Plate for Visualization
of Detailed Ultrastructure in Complex Biological Specimens.” Journal of Structural
Biology, vol. 168, no. 3, Academic Press, 2009, pp. 476–84, doi:10.1016/j.jsb.2009.08.011.
short: Y. Fukuda, Y. Fukazawa, R. Danev, R. Shigemoto, K. Nagayama, Journal of Structural
Biology 168 (2009) 476–484.
date_created: 2018-12-11T11:58:03Z
date_published: 2009-12-01T00:00:00Z
date_updated: 2021-01-12T06:57:52Z
day: '01'
doi: 10.1016/j.jsb.2009.08.011
extern: 1
intvolume: ' 168'
issue: '3'
month: '12'
page: 476 - 484
publication: Journal of Structural Biology
publication_status: published
publisher: Academic Press
publist_id: '4399'
quality_controlled: 0
status: public
title: Tuning of the Zernike phase-plate for visualization of detailed ultrastructure
in complex biological specimens
type: journal_article
volume: 168
year: '2009'
...
---
_id: '2680'
abstract:
- lang: eng
text: 'GABA B receptor subtypes are based on the subunit isoforms GABA B1a and GABA
B1b, which associate with GABA B2 subunits to form pharmacologically indistinguishable
GABA B(1a,2) and GABA B(1b,2) receptors. Studies with mice selectively expressing
GABA B1a or GABA B1b subunits revealed that GABA B(1a,2) receptors are more abundant
than GABA B(1b,2) receptors at glutamatergic terminals. Accordingly, it was found
that GABA B(1a,2) receptors are more efficient than GABA B(1b,2) receptors in
inhibiting glutamate release when maximally activated by exogenous application
of the agonist baclofen. Here, we used a combination of genetic, ultrastructural
and electrophysiological approaches to analyze to what extent GABA B(1a,2) and
GABA B(1b,2) receptors inhibit glutamate release in response to physiological
activation. We first show that at hippocampal mossy fiber (MF)-CA3 pyramidal neuron
synapses more GABA B1a than GABA B1b protein is present at presynaptic sites,
consistent with the findings at other glutamatergic synapses. In the presence
of baclofen at concentrations ≥1 μM, both GABA B(1a,2) and GABA B(1b,2) receptors
contribute to presynaptic inhibition of glutamate release. However, at lower concentrations
of baclofen, selectively GABA B(1a,2) receptors contribute to presynaptic inhibition.
Remarkably, exclusively GABA B(1a,2) receptors inhibit glutamate release in response
to synaptically released GABA. Specifically, we demonstrate that selectively GABA
B(1a,2) receptors mediate heterosynaptic depression of MF transmission, a physiological
phenomenon involving transsynaptic inhibition of glutamate release via presynaptic
GABA B receptors. Our data demonstrate that the difference in GABA B1a and GABA
B1b protein levels at MF terminals is sufficient to produce a strictly GABA B1a-specific
effect under physiological conditions. This consolidates that the differential
subcellular localization of the GABA B1a and GABA B1b proteins is of regulatory
relevance. '
author:
- first_name: Nicole
full_name: Guetg, Nicole
last_name: Guetg
- first_name: Riad
full_name: Seddik, Riad
last_name: Seddik
- first_name: Réjan
full_name: Vigot, Réjan
last_name: Vigot
- first_name: Rostislav
full_name: Tureček, Rostislav
last_name: Tureček
- first_name: Martin
full_name: Gassmann, Martin
last_name: Gassmann
- first_name: Kaspar
full_name: Vogt, Kaspar E
last_name: Vogt
- first_name: Hans
full_name: Bräuner-Osborne, Hans
last_name: Bräuner Osborne
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Oliver
full_name: Kretz, Oliver
last_name: Kretz
- first_name: Michael
full_name: Frotscher, Michael
last_name: Frotscher
- first_name: Ákos
full_name: Kulik, Ákos
last_name: Kulik
- first_name: Bernhard
full_name: Bettler, Bernhard
last_name: Bettler
citation:
ama: Guetg N, Seddik R, Vigot R, et al. The GABA B1a isoform mediates heterosynaptic
depression at hippocampal mossy fiber synapses. Journal of Neuroscience.
2009;29(5):1414-1423. doi:10.1523/JNEUROSCI.3697-08.2009
apa: Guetg, N., Seddik, R., Vigot, R., Tureček, R., Gassmann, M., Vogt, K., … Bettler,
B. (2009). The GABA B1a isoform mediates heterosynaptic depression at hippocampal
mossy fiber synapses. Journal of Neuroscience. Society for Neuroscience.
https://doi.org/10.1523/JNEUROSCI.3697-08.2009
chicago: Guetg, Nicole, Riad Seddik, Réjan Vigot, Rostislav Tureček, Martin Gassmann,
Kaspar Vogt, Hans Bräuner Osborne, et al. “The GABA B1a Isoform Mediates Heterosynaptic
Depression at Hippocampal Mossy Fiber Synapses.” Journal of Neuroscience.
Society for Neuroscience, 2009. https://doi.org/10.1523/JNEUROSCI.3697-08.2009.
ieee: N. Guetg et al., “The GABA B1a isoform mediates heterosynaptic depression
at hippocampal mossy fiber synapses,” Journal of Neuroscience, vol. 29,
no. 5. Society for Neuroscience, pp. 1414–1423, 2009.
ista: Guetg N, Seddik R, Vigot R, Tureček R, Gassmann M, Vogt K, Bräuner Osborne
H, Shigemoto R, Kretz O, Frotscher M, Kulik Á, Bettler B. 2009. The GABA B1a isoform
mediates heterosynaptic depression at hippocampal mossy fiber synapses. Journal
of Neuroscience. 29(5), 1414–1423.
mla: Guetg, Nicole, et al. “The GABA B1a Isoform Mediates Heterosynaptic Depression
at Hippocampal Mossy Fiber Synapses.” Journal of Neuroscience, vol. 29,
no. 5, Society for Neuroscience, 2009, pp. 1414–23, doi:10.1523/JNEUROSCI.3697-08.2009.
short: N. Guetg, R. Seddik, R. Vigot, R. Tureček, M. Gassmann, K. Vogt, H. Bräuner
Osborne, R. Shigemoto, O. Kretz, M. Frotscher, Á. Kulik, B. Bettler, Journal of
Neuroscience 29 (2009) 1414–1423.
date_created: 2018-12-11T11:59:02Z
date_published: 2009-02-04T00:00:00Z
date_updated: 2021-01-12T06:59:01Z
day: '04'
doi: 10.1523/JNEUROSCI.3697-08.2009
extern: 1
intvolume: ' 29'
issue: '5'
month: '02'
page: 1414 - 1423
publication: Journal of Neuroscience
publication_status: published
publisher: Society for Neuroscience
publist_id: '4216'
quality_controlled: 0
status: public
title: The GABA B1a isoform mediates heterosynaptic depression at hippocampal mossy
fiber synapses
type: journal_article
volume: 29
year: '2009'
...
---
_id: '2682'
abstract:
- lang: eng
text: The living cell imaging using a two-photon microscope using gold nanoplates
and nanoparticle aggregates was demonstrated. The dimensions of the nanoplates
were determined through scanning electron microscopy (SEM) and atomic force microscopy.
The height of a 100 nm base-length nanotriangle was around 10 nm, while the height
of 300 nm base-length nanotriangle was around 12 nm. A spectrophotometer was also
used to determine the extinction spectra of gold nanoparticle colloids. Two-photon-induced
photoluminescence (TPIPL) under far-field excitation was tested for gold nanoplates
on a glass substrate using two-photon laser scanning microscopy (TPLSM). It was
observed that living-cell microscopic imaging can be carried out with TPIPL from
gold nanoplates and aggregated nanosphere. This method provided a platform for
developing tools for biological and biomedical studies.
author:
- first_name: Yuqiang
full_name: Jiang, Yuqiang
last_name: Jiang
- first_name: Noriko
full_name: Horimoto, Noriko N
last_name: Horimoto
- first_name: Kohei
full_name: Imura, Kohei
last_name: Imura
- first_name: Ko
full_name: Matsui, Ko
last_name: Matsui
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
citation:
ama: Jiang Y, Horimoto N, Imura K, Matsui K, Shigemoto R. Bioimaging with two-photon-induced
luminescence from triangular nanoplates and nanoparticle aggregates of gold. Advanced
Materials. 2009;21(22):2309-2313. doi:10.1002/adma.200802312
apa: Jiang, Y., Horimoto, N., Imura, K., Matsui, K., & Shigemoto, R. (2009).
Bioimaging with two-photon-induced luminescence from triangular nanoplates and
nanoparticle aggregates of gold. Advanced Materials. Wiley-Blackwell. https://doi.org/10.1002/adma.200802312
chicago: Jiang, Yuqiang, Noriko Horimoto, Kohei Imura, Ko Matsui, and Ryuichi Shigemoto.
“Bioimaging with Two-Photon-Induced Luminescence from Triangular Nanoplates and
Nanoparticle Aggregates of Gold.” Advanced Materials. Wiley-Blackwell,
2009. https://doi.org/10.1002/adma.200802312.
ieee: Y. Jiang, N. Horimoto, K. Imura, K. Matsui, and R. Shigemoto, “Bioimaging
with two-photon-induced luminescence from triangular nanoplates and nanoparticle
aggregates of gold,” Advanced Materials, vol. 21, no. 22. Wiley-Blackwell,
pp. 2309–2313, 2009.
ista: Jiang Y, Horimoto N, Imura K, Matsui K, Shigemoto R. 2009. Bioimaging with
two-photon-induced luminescence from triangular nanoplates and nanoparticle aggregates
of gold. Advanced Materials. 21(22), 2309–2313.
mla: Jiang, Yuqiang, et al. “Bioimaging with Two-Photon-Induced Luminescence from
Triangular Nanoplates and Nanoparticle Aggregates of Gold.” Advanced Materials,
vol. 21, no. 22, Wiley-Blackwell, 2009, pp. 2309–13, doi:10.1002/adma.200802312.
short: Y. Jiang, N. Horimoto, K. Imura, K. Matsui, R. Shigemoto, Advanced Materials
21 (2009) 2309–2313.
date_created: 2018-12-11T11:59:02Z
date_published: 2009-06-12T00:00:00Z
date_updated: 2021-01-12T06:59:01Z
day: '12'
doi: 10.1002/adma.200802312
extern: 1
intvolume: ' 21'
issue: '22'
month: '06'
page: 2309 - 2313
publication: Advanced Materials
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4214'
quality_controlled: 0
status: public
title: Bioimaging with two-photon-induced luminescence from triangular nanoplates
and nanoparticle aggregates of gold
type: journal_article
volume: 21
year: '2009'
...
---
_id: '2683'
abstract:
- lang: eng
text: GABAb receptor (GABAbR)-mediated suppression of glutamate release is critical
for limiting glutamatergic transmission across the central nervous system (CNS).
Here we show that, upon tetanic stimulation of afferents to lateral amygdala,
presynaptic GABAbR-mediated inhibition only occurs in glutamatergic inputs to
principle neurons (PNs), not to interneurons (INs), despite the presence of GABAbR
in terminals to both types of neurons. The selectivity is caused by differential
local GABA accumulation; it requires GABA reuptake and parallels distinct spatial
distributions of presynaptic GABAbR in terminals to PNs and INs. Moreover, GABAbR-mediated
suppression of theta-burst-induced long-term potentiation (LTP) occurs only in
the inputs to PNs, not to INs. Thus, target-cell-specific control of glutamate
release by presynaptic GABAbR orchestrates the inhibitory dominance inside amygdala
and might contribute to prevention of nonadaptive defensive behaviors.
author:
- first_name: Bingxing
full_name: Pan, Bingxing
last_name: Pan
- first_name: Yu
full_name: Dong, Yu-Lin
last_name: Dong
- first_name: Wataru
full_name: Ito, Wataru
last_name: Ito
- first_name: Yuchio
full_name: Yanagawa, Yuchio
last_name: Yanagawa
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Alexei
full_name: Morozov, Alexei A
last_name: Morozov
citation:
ama: Pan B, Dong Y, Ito W, Yanagawa Y, Shigemoto R, Morozov A. Selective gating
of glutamatergic inputs to excitatory neurons of amygdala by presynaptic GABAb
receptor. Neuron. 2009;61(6):917-929. doi:10.1016/j.neuron.2009.01.029
apa: Pan, B., Dong, Y., Ito, W., Yanagawa, Y., Shigemoto, R., & Morozov, A.
(2009). Selective gating of glutamatergic inputs to excitatory neurons of amygdala
by presynaptic GABAb receptor. Neuron. Elsevier. https://doi.org/10.1016/j.neuron.2009.01.029
chicago: Pan, Bingxing, Yu Dong, Wataru Ito, Yuchio Yanagawa, Ryuichi Shigemoto,
and Alexei Morozov. “Selective Gating of Glutamatergic Inputs to Excitatory Neurons
of Amygdala by Presynaptic GABAb Receptor.” Neuron. Elsevier, 2009. https://doi.org/10.1016/j.neuron.2009.01.029.
ieee: B. Pan, Y. Dong, W. Ito, Y. Yanagawa, R. Shigemoto, and A. Morozov, “Selective
gating of glutamatergic inputs to excitatory neurons of amygdala by presynaptic
GABAb receptor,” Neuron, vol. 61, no. 6. Elsevier, pp. 917–929, 2009.
ista: Pan B, Dong Y, Ito W, Yanagawa Y, Shigemoto R, Morozov A. 2009. Selective
gating of glutamatergic inputs to excitatory neurons of amygdala by presynaptic
GABAb receptor. Neuron. 61(6), 917–929.
mla: Pan, Bingxing, et al. “Selective Gating of Glutamatergic Inputs to Excitatory
Neurons of Amygdala by Presynaptic GABAb Receptor.” Neuron, vol. 61, no.
6, Elsevier, 2009, pp. 917–29, doi:10.1016/j.neuron.2009.01.029.
short: B. Pan, Y. Dong, W. Ito, Y. Yanagawa, R. Shigemoto, A. Morozov, Neuron 61
(2009) 917–929.
date_created: 2018-12-11T11:59:03Z
date_published: 2009-03-26T00:00:00Z
date_updated: 2021-01-12T06:59:02Z
day: '26'
doi: 10.1016/j.neuron.2009.01.029
extern: 1
intvolume: ' 61'
issue: '6'
month: '03'
page: 917 - 929
publication: Neuron
publication_status: published
publisher: Elsevier
publist_id: '4215'
quality_controlled: 0
status: public
title: Selective gating of glutamatergic inputs to excitatory neurons of amygdala
by presynaptic GABAb receptor
type: journal_article
volume: 61
year: '2009'
...
---
_id: '2684'
abstract:
- lang: eng
text: Calcium-activated potassium channels have been shown to be critically involved
in neuronal function, but an elucidation of their detailed roles awaits identification
of the microdomains where they are located. This study was undertaken to unravel
the precise subcellular distribution of the large-conductance calcium-activated
potassium channels (called BK, KCa1.1, or Slo1) in the somatodendritic compartment
of cerebellar Purkinje cells by means of postembedding immunogold cytochemistry
and SDS-digested freeze-fracture replica labeling (SDS-FRL). We found BK channels
to be unevenly distributed over the Purkinje cell plasma membrane. At distal dendritic
compartments, BK channels were scattered over the plasma membrane of dendritic
shafts and spines but absent from postsynaptic densities. At the soma and proximal
dendrites, BK channels formed two distinct pools. One pool was scattered over
the plasma membrane, whereas the other pool was clustered in plasma membrane domains
overlying subsurface cisterns. The labeling density ratio of clustered to scattered
channels was about 60:1, established in SDS-FRL. Subsurface cisterns, also called
hypolemmal cisterns, are subcompartments of the endoplasmic reticulum likely representing
calciosomes that unload and refill Ca2+ independently. Purkinje cell subsurface
cisterns are enriched in inositol 1,4,5-triphosphate receptors that mediate the
effects of several neurotransmitters, hormones, and growth factors by releasing
Ca2+ into the cytosol, generating local Ca2+ sparks. Such increases in cytosolic
[Ca2+] may be sufficient for BK channel activation. Clustered BK channels in the
plasma membrane may thus participate in building a functional unit (plasmerosome)
with the underlying calciosome that contributes significantly to local signaling
in Purkinje cells.
author:
- first_name: Walter
full_name: Walter Kaufmann
id: 3F99E422-F248-11E8-B48F-1D18A9856A87
last_name: Kaufmann
orcid: 0000-0001-9735-5315
- first_name: Francesco
full_name: Ferraguti, Francesco
last_name: Ferraguti
- first_name: Yugo
full_name: Fukazawa, Yugo
last_name: Fukazawa
- first_name: Yu
full_name: Kasugai, Yu
last_name: Kasugai
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Petter
full_name: Laake, Petter
last_name: Laake
- first_name: Joseph
full_name: Sexton, Joseph A
last_name: Sexton
- first_name: Peter
full_name: Ruth, Peter
last_name: Ruth
- first_name: Georg
full_name: Wietzorrek, Georg
last_name: Wietzorrek
- first_name: Hans
full_name: Knaus, Hans G
last_name: Knaus
- first_name: Johan
full_name: Storm, Johan F
last_name: Storm
- first_name: Ole
full_name: Ottersen, Ole P
last_name: Ottersen
citation:
ama: Kaufmann W, Ferraguti F, Fukazawa Y, et al. Large-conductance calcium-activated
potassium channels in Purkinje cell plasma membranes are clustered at sites of
hypolemmal microdomains. Journal of Comparative Neurology. 2009;515(2):215-230.
doi:10.1002/cne.22066
apa: Kaufmann, W., Ferraguti, F., Fukazawa, Y., Kasugai, Y., Shigemoto, R., Laake,
P., … Ottersen, O. (2009). Large-conductance calcium-activated potassium channels
in Purkinje cell plasma membranes are clustered at sites of hypolemmal microdomains.
Journal of Comparative Neurology. Wiley-Blackwell. https://doi.org/10.1002/cne.22066
chicago: Kaufmann, Walter, Francesco Ferraguti, Yugo Fukazawa, Yu Kasugai, Ryuichi
Shigemoto, Petter Laake, Joseph Sexton, et al. “Large-Conductance Calcium-Activated
Potassium Channels in Purkinje Cell Plasma Membranes Are Clustered at Sites of
Hypolemmal Microdomains.” Journal of Comparative Neurology. Wiley-Blackwell,
2009. https://doi.org/10.1002/cne.22066.
ieee: W. Kaufmann et al., “Large-conductance calcium-activated potassium
channels in Purkinje cell plasma membranes are clustered at sites of hypolemmal
microdomains,” Journal of Comparative Neurology, vol. 515, no. 2. Wiley-Blackwell,
pp. 215–230, 2009.
ista: Kaufmann W, Ferraguti F, Fukazawa Y, Kasugai Y, Shigemoto R, Laake P, Sexton
J, Ruth P, Wietzorrek G, Knaus H, Storm J, Ottersen O. 2009. Large-conductance
calcium-activated potassium channels in Purkinje cell plasma membranes are clustered
at sites of hypolemmal microdomains. Journal of Comparative Neurology. 515(2),
215–230.
mla: Kaufmann, Walter, et al. “Large-Conductance Calcium-Activated Potassium Channels
in Purkinje Cell Plasma Membranes Are Clustered at Sites of Hypolemmal Microdomains.”
Journal of Comparative Neurology, vol. 515, no. 2, Wiley-Blackwell, 2009,
pp. 215–30, doi:10.1002/cne.22066.
short: W. Kaufmann, F. Ferraguti, Y. Fukazawa, Y. Kasugai, R. Shigemoto, P. Laake,
J. Sexton, P. Ruth, G. Wietzorrek, H. Knaus, J. Storm, O. Ottersen, Journal of
Comparative Neurology 515 (2009) 215–230.
date_created: 2018-12-11T11:59:03Z
date_published: 2009-07-10T00:00:00Z
date_updated: 2023-02-23T10:53:41Z
day: '10'
doi: 10.1002/cne.22066
extern: 1
intvolume: ' 515'
issue: '2'
month: '07'
page: 215 - 230
publication: Journal of Comparative Neurology
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4212'
quality_controlled: 0
status: public
title: Large-conductance calcium-activated potassium channels in Purkinje cell plasma
membranes are clustered at sites of hypolemmal microdomains
type: journal_article
volume: 515
year: '2009'
...
---
_id: '2685'
abstract:
- lang: eng
text: Conduction velocity (CV) of myelinated axons has been shown to be regulated
by oligodendrocytes even after myelination has been completed. However, how myelinating
oligodendrocytes regulate CV, and what the significance of this regulation is
for normal brain function remain unknown. To address these questions, we analyzed
a transgenic mouse line harboring extra copies of the myelin proteolipid protein
1 (plp1) gene (plp1tg/- mice) at 2 months of age. At this stage, the plp1tg/-
mice have an unaffected myelin structure with a normally appearing ion channel
distribution, but the CV in all axonal tracts tested in the CNS is greatly reduced.
We also found decreased axonal diameters and slightly abnormal paranodal structures,
both of which can be a cause for the reduced CV. Interestingly the plp1tg/- mice
showed altered anxiety-like behaviors, reduced prepulse inhibitions, spatial learning
deficits and working memory deficit, all of which are schizophrenia-related behaviors.
Our results implicate that abnormalities in the neuron-glia interactions at the
paranodal junctions can result in reduced CV in the CNS, which then induces behavioral
abnormalities related to schizophrenia.
author:
- first_name: Hisataka
full_name: Tanaka, Hisataka
last_name: Tanaka
- first_name: Jianmei
full_name: Ma, Jianmei
last_name: Ma
- first_name: Kenji
full_name: Tanaka, Kenji F
last_name: Tanaka
- first_name: Keizo
full_name: Takao, Keizo
last_name: Takao
- first_name: Munekazu
full_name: Komada, Munekazu
last_name: Komada
- first_name: Koichi
full_name: Tanda, Koichi
last_name: Tanda
- first_name: Ayaka
full_name: Suzuki, Ayaka
last_name: Suzuki
- first_name: Tomoko
full_name: Ishibashi, Tomoko
last_name: Ishibashi
- first_name: Hiroko
full_name: Baba, Hiroko
last_name: Baba
- first_name: Tadashi
full_name: Isa, Tadashi
last_name: Isa
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Katsuhiko
full_name: Ono, Katsuhiko
last_name: Ono
- first_name: Tsuyoshi
full_name: Miyakawa, Tsuyoshi
last_name: Miyakawa
- first_name: Kazuhiro
full_name: Ikenaka, Kazuhiro
last_name: Ikenaka
citation:
ama: Tanaka H, Ma J, Tanaka K, et al. Mice with altered myelin proteolipid protein
gene expression display cognitive deficits accompanied by abnormal neuron-glia
interactions and decreased conduction velocities. Journal of Neuroscience.
2009;29(26):8363-8371. doi:10.1523/JNEUROSCI.3216-08.2009
apa: Tanaka, H., Ma, J., Tanaka, K., Takao, K., Komada, M., Tanda, K., … Ikenaka,
K. (2009). Mice with altered myelin proteolipid protein gene expression display
cognitive deficits accompanied by abnormal neuron-glia interactions and decreased
conduction velocities. Journal of Neuroscience. Society for Neuroscience.
https://doi.org/10.1523/JNEUROSCI.3216-08.2009
chicago: Tanaka, Hisataka, Jianmei Ma, Kenji Tanaka, Keizo Takao, Munekazu Komada,
Koichi Tanda, Ayaka Suzuki, et al. “Mice with Altered Myelin Proteolipid Protein
Gene Expression Display Cognitive Deficits Accompanied by Abnormal Neuron-Glia
Interactions and Decreased Conduction Velocities.” Journal of Neuroscience.
Society for Neuroscience, 2009. https://doi.org/10.1523/JNEUROSCI.3216-08.2009.
ieee: H. Tanaka et al., “Mice with altered myelin proteolipid protein gene
expression display cognitive deficits accompanied by abnormal neuron-glia interactions
and decreased conduction velocities,” Journal of Neuroscience, vol. 29,
no. 26. Society for Neuroscience, pp. 8363–8371, 2009.
ista: Tanaka H, Ma J, Tanaka K, Takao K, Komada M, Tanda K, Suzuki A, Ishibashi
T, Baba H, Isa T, Shigemoto R, Ono K, Miyakawa T, Ikenaka K. 2009. Mice with altered
myelin proteolipid protein gene expression display cognitive deficits accompanied
by abnormal neuron-glia interactions and decreased conduction velocities. Journal
of Neuroscience. 29(26), 8363–8371.
mla: Tanaka, Hisataka, et al. “Mice with Altered Myelin Proteolipid Protein Gene
Expression Display Cognitive Deficits Accompanied by Abnormal Neuron-Glia Interactions
and Decreased Conduction Velocities.” Journal of Neuroscience, vol. 29,
no. 26, Society for Neuroscience, 2009, pp. 8363–71, doi:10.1523/JNEUROSCI.3216-08.2009.
short: H. Tanaka, J. Ma, K. Tanaka, K. Takao, M. Komada, K. Tanda, A. Suzuki, T.
Ishibashi, H. Baba, T. Isa, R. Shigemoto, K. Ono, T. Miyakawa, K. Ikenaka, Journal
of Neuroscience 29 (2009) 8363–8371.
date_created: 2018-12-11T11:59:03Z
date_published: 2009-07-01T00:00:00Z
date_updated: 2021-01-12T06:59:02Z
day: '01'
doi: 10.1523/JNEUROSCI.3216-08.2009
extern: 1
intvolume: ' 29'
issue: '26'
month: '07'
page: 8363 - 8371
publication: Journal of Neuroscience
publication_status: published
publisher: Society for Neuroscience
publist_id: '4213'
quality_controlled: 0
status: public
title: Mice with altered myelin proteolipid protein gene expression display cognitive
deficits accompanied by abnormal neuron-glia interactions and decreased conduction
velocities
type: journal_article
volume: 29
year: '2009'
...