---
_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.'
corr_author: '1'
date_created: 2018-12-11T12:08:37Z
date_published: 2010-07-29T00:00:00Z
date_updated: 2024-10-09T20:53:58Z
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
fulldoi: https://doi.org/10.1007/978-3-642-13754-9_3
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
corr_author: '1'
date_created: 2018-12-11T12:08:37Z
date_published: 2010-11-01T00:00:00Z
date_updated: 2026-06-18T18:41:23Z
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
fulldoi: https://doi.org/10.1007/978-3-642-15375-4_18
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: '5389'
relation: earlier_version
status: public
- id: '3249'
relation: later_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'
fulldoi: https://doi.org/10.1007/978-3-642-11970-5_7
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
fulldoi: https://doi.org/10.1007/978-3-642-12029-9_19
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.
article_processing_charge: No
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.
corr_author: '1'
date_created: 2018-12-11T11:46:40Z
date_published: 2010-09-01T00:00:00Z
date_updated: 2025-09-30T09:50:22Z
day: '01'
department:
- _id: NiBa
doi: 10.1111/j.1558-5646.2010.01019.x
external_id:
isi:
- '000281636400017'
fulldoi: https://doi.org/10.1111/j.1558-5646.2010.01019.x
intvolume: ' 64'
isi: 1
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
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
article_processing_charge: No
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
corr_author: '1'
date_created: 2018-12-11T11:46:45Z
date_published: 2010-01-01T00:00:00Z
date_updated: 2025-09-30T09:49:32Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.4230/LIPIcs.FSTTCS.2010.1
external_id:
isi:
- '000310361000001'
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
fulldoi: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.1
has_accepted_license: '1'
intvolume: ' 8'
isi: 1
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
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
article_processing_charge: No
arxiv: 1
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
corr_author: '1'
date_created: 2018-12-11T11:46:45Z
date_published: 2010-06-09T00:00:00Z
date_updated: 2026-06-18T18:51:53Z
day: '09'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4204/EPTCS.25.7
external_id:
arxiv:
- '1006.1404'
fulldoi: https://doi.org/10.4204/EPTCS.25.7
intvolume: ' 25'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1006.1404
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: 2DF688A6-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.
article_processing_charge: No
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.
corr_author: '1'
date_created: 2018-12-11T11:47:01Z
date_published: 2010-12-01T00:00:00Z
date_updated: 2025-09-30T09:48:58Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/s10703-010-0102-0
external_id:
isi:
- '000286631700004'
fulldoi: https://doi.org/10.1007/s10703-010-0102-0
intvolume: ' 37'
isi: 1
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 37
year: '2010'
...
---
_id: '5388'
abstract:
- lang: eng
text: "We present an algorithmic method for the synthesis of concurrent programs
that are optimal with respect to quantitative performance measures. The input
consists of a sequential sketch, that is, a program that does not contain synchronization
constructs, and of a parametric performance model that assigns costs to actions
such as locking, context switching, and idling. The quantitative synthesis problem
is to automatically introduce synchronization constructs into the sequential sketch
so that both correctness is guaranteed and worst-case (or average-case) performance
is optimized. Correctness is formalized as race freedom or linearizability.\r\n\r\nWe
show that for worst-case performance, the problem can be modeled\r\nas a 2-player
graph game with quantitative (limit-average) objectives, and\r\nfor average-case
performance, as a 2 1/2 -player graph game (with probabilistic transitions). In
both cases, the optimal correct program is derived from an optimal strategy in
the corresponding quantitative game. We prove that the respective game problems
are computationally expensive (NP-complete), and present several techniques that
overcome the theoretical difficulty in cases of concurrent programs of practical
interest.\r\n\r\nWe have implemented a prototype tool and used it for the automatic
syn- thesis of programs that access a concurrent list. For certain parameter val-
ues, our method automatically synthesizes various classical synchronization schemes
for implementing a concurrent list, such as fine-grained locking or a lazy algorithm.
For other parameter values, a new, hybrid synchronization style is synthesized,
which uses both the lazy approach and coarse-grained locks (instead of standard
fine-grained locks). The trade-off occurs because while fine-grained locking tends
to decrease the cost that is due to waiting for locks, it increases cache size
requirements."
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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
- first_name: Rohit
full_name: Singh, Rohit
last_name: Singh
citation:
ama: Chatterjee K, Cerny P, Henzinger TA, Radhakrishna A, Singh R. Quantitative
Synthesis for Concurrent Programs. IST Austria; 2010. doi:10.15479/AT:IST-2010-0004
apa: Chatterjee, K., Cerny, P., Henzinger, T. A., Radhakrishna, A., & Singh,
R. (2010). Quantitative synthesis for concurrent programs. IST Austria.
https://doi.org/10.15479/AT:IST-2010-0004
chicago: Chatterjee, Krishnendu, Pavol Cerny, Thomas A Henzinger, Arjun Radhakrishna,
and Rohit Singh. Quantitative Synthesis for Concurrent Programs. IST Austria,
2010. https://doi.org/10.15479/AT:IST-2010-0004.
ieee: K. Chatterjee, P. Cerny, T. A. Henzinger, A. Radhakrishna, and R. Singh, Quantitative
synthesis for concurrent programs. IST Austria, 2010.
ista: Chatterjee K, Cerny P, Henzinger TA, Radhakrishna A, Singh R. 2010. Quantitative
synthesis for concurrent programs, IST Austria, 17p.
mla: Chatterjee, Krishnendu, et al. Quantitative Synthesis for Concurrent Programs.
IST Austria, 2010, doi:10.15479/AT:IST-2010-0004.
short: K. Chatterjee, P. Cerny, T.A. Henzinger, A. Radhakrishna, R. Singh, Quantitative
Synthesis for Concurrent Programs, IST Austria, 2010.
date_created: 2018-12-12T11:39:03Z
date_published: 2010-10-07T00:00:00Z
date_updated: 2025-04-15T08:12:00Z
day: '07'
ddc:
- '000'
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:IST-2010-0004
file:
- access_level: open_access
checksum: da38782d2388a6fa32109d10bb9bad67
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:53Z
date_updated: 2020-07-14T12:46:42Z
file_id: '5515'
file_name: IST-2010-0004_IST-2010-0004.pdf
file_size: 429101
relation: main_file
file_date_updated: 2020-07-14T12:46:42Z
fulldoi: https://doi.org/10.15479/AT:IST-2010-0004
has_accepted_license: '1'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: '17'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '24'
related_material:
record:
- id: '3366'
relation: later_version
status: public
status: public
title: Quantitative synthesis for concurrent programs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '5389'
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 im- plementation 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.
alternative_title:
- IST Austria Technical Report
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. IST Austria;
2010. doi:10.15479/AT:IST-2010-0003
apa: Cerny, P., Henzinger, T. A., & Radhakrishna, A. (2010). Simulation distances.
IST Austria. https://doi.org/10.15479/AT:IST-2010-0003
chicago: Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. Simulation
Distances. IST Austria, 2010. https://doi.org/10.15479/AT:IST-2010-0003.
ieee: P. Cerny, T. A. Henzinger, and A. Radhakrishna, Simulation distances.
IST Austria, 2010.
ista: Cerny P, Henzinger TA, Radhakrishna A. 2010. Simulation distances, IST Austria,
24p.
mla: Cerny, Pavol, et al. Simulation Distances. IST Austria, 2010, doi:10.15479/AT:IST-2010-0003.
short: P. Cerny, T.A. Henzinger, A. Radhakrishna, Simulation Distances, IST Austria,
2010.
date_created: 2018-12-12T11:39:03Z
date_published: 2010-06-04T00:00:00Z
date_updated: 2026-06-18T18:41:23Z
day: '04'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2010-0003
file:
- access_level: open_access
checksum: 284ded99764e32a583a8ea83fcea254b
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:25Z
date_updated: 2020-07-14T12:46:42Z
file_id: '5547'
file_name: IST-2010-0003_IST-2010-0003.pdf
file_size: 367246
relation: main_file
file_date_updated: 2020-07-14T12:46:42Z
fulldoi: https://doi.org/10.15479/AT:IST-2010-0003
has_accepted_license: '1'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: '24'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '25'
related_material:
record:
- id: '4393'
relation: later_version
status: public
- id: '3249'
relation: later_version
status: public
status: public
title: Simulation distances
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '5390'
abstract:
- lang: eng
text: The class of ω regular languages provide a robust specification language in
verification. Every ω-regular condition can be decomposed into a safety part and
a liveness part. The liveness part ensures that something good happens “eventually.”
Two main strengths of the classical, infinite-limit formulation of liveness are
robustness (independence from the granularity of transitions) and simplicity (abstraction
of complicated time bounds). However, the classical liveness formulation suffers
from the drawback that the time until something good happens may be unbounded.
A stronger formulation of liveness, so-called finitary liveness, overcomes this
drawback, while still retaining robustness and simplicity. Finitary liveness requires
that there exists an unknown, fixed bound b such that something good happens within
b transitions. In this work we consider the finitary parity and Streett (fairness)
conditions. We present the topological, automata-theoretic and logical characterization
of finitary languages defined by finitary parity and Streett conditions. We (a)
show that the finitary parity and Streett languages are Σ2-complete; (b) present
a complete characterization of the expressive power of various classes of automata
with finitary and infinitary conditions (in particular we show that non-deterministic
finitary parity and Streett automata cannot be determinized to deterministic finitary
parity or Streett automata); and (c) show that the languages defined by non-deterministic
finitary parity automata exactly characterize the star-free fragment of ωB-regular
languages.
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Nathanaël
full_name: Fijalkow, Nathanaël
last_name: Fijalkow
citation:
ama: Chatterjee K, Fijalkow N. Topological, Automata-Theoretic and Logical Characterization
of Finitary Languages. IST Austria; 2010. doi:10.15479/AT:IST-2010-0002
apa: Chatterjee, K., & Fijalkow, N. (2010). Topological, automata-theoretic
and logical characterization of finitary languages. IST Austria. https://doi.org/10.15479/AT:IST-2010-0002
chicago: Chatterjee, Krishnendu, and Nathanaël Fijalkow. Topological, Automata-Theoretic
and Logical Characterization of Finitary Languages. IST Austria, 2010. https://doi.org/10.15479/AT:IST-2010-0002.
ieee: K. Chatterjee and N. Fijalkow, Topological, automata-theoretic and logical
characterization of finitary languages. IST Austria, 2010.
ista: Chatterjee K, Fijalkow N. 2010. Topological, automata-theoretic and logical
characterization of finitary languages, IST Austria, 21p.
mla: Chatterjee, Krishnendu, and Nathanaël Fijalkow. Topological, Automata-Theoretic
and Logical Characterization of Finitary Languages. IST Austria, 2010, doi:10.15479/AT:IST-2010-0002.
short: K. Chatterjee, N. Fijalkow, Topological, Automata-Theoretic and Logical Characterization
of Finitary Languages, IST Austria, 2010.
date_created: 2018-12-12T11:39:03Z
date_published: 2010-06-04T00:00:00Z
date_updated: 2020-07-14T23:04:41Z
day: '04'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2010-0002
file:
- access_level: open_access
checksum: 283d3604d76dd4d5161585d4c8625fbe
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:10Z
date_updated: 2020-07-14T12:46:43Z
file_id: '5532'
file_name: IST-2010-0002_IST-2010-0002.pdf
file_size: 395662
relation: main_file
file_date_updated: 2020-07-14T12:46:43Z
fulldoi: https://doi.org/10.15479/AT:IST-2010-0002
has_accepted_license: '1'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: '21'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '26'
status: public
title: Topological, automata-theoretic and logical characterization of finitary languages
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '5391'
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 node consists 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
imple- mentation and proved that the corrected version is linearizable.
alternative_title:
- IST Austria Technical Report
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. IST Austria; 2010.
doi:10.15479/AT:IST-2010-0001
apa: Cerny, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., & Alur, R. (2010).
Model checking of linearizability of concurrent list implementations. IST
Austria. https://doi.org/10.15479/AT:IST-2010-0001
chicago: Cerny, Pavol, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, and
Rajeev Alur. Model Checking of Linearizability of Concurrent List Implementations.
IST Austria, 2010. https://doi.org/10.15479/AT:IST-2010-0001.
ieee: P. Cerny, A. Radhakrishna, D. Zufferey, S. Chaudhuri, and R. Alur, Model
checking of linearizability of concurrent list implementations. IST Austria,
2010.
ista: Cerny P, Radhakrishna A, Zufferey D, Chaudhuri S, Alur R. 2010. Model checking
of linearizability of concurrent list implementations, IST Austria, 27p.
mla: Cerny, Pavol, et al. Model Checking of Linearizability of Concurrent List
Implementations. IST Austria, 2010, doi:10.15479/AT:IST-2010-0001.
short: P. Cerny, A. Radhakrishna, D. Zufferey, S. Chaudhuri, R. Alur, Model Checking
of Linearizability of Concurrent List Implementations, IST Austria, 2010.
date_created: 2018-12-12T11:39:04Z
date_published: 2010-04-19T00:00:00Z
date_updated: 2024-10-21T06:03:05Z
day: '19'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2010-0001
file:
- access_level: open_access
checksum: 986645caad7dd85a6a091488f6c646dc
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:44Z
date_updated: 2020-07-14T12:46:43Z
file_id: '5505'
file_name: IST-2010-0001_IST-2010-0001.pdf
file_size: 372286
relation: main_file
file_date_updated: 2020-07-14T12:46:43Z
fulldoi: https://doi.org/10.15479/AT:IST-2010-0001
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: '27'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '27'
related_material:
record:
- id: '4390'
relation: later_version
status: public
status: public
title: Model checking of linearizability of concurrent list implementations
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '5940'
article_processing_charge: No
author:
- first_name: Gabriel
full_name: Juhás, Gabriel
last_name: Juhás
- first_name: Igor
full_name: Kazlov, Igor
id: 4A997E50-F248-11E8-B48F-1D18A9856A87
last_name: Kazlov
- first_name: Ana
full_name: Juhásová, Ana
last_name: Juhásová
citation:
ama: 'Juhás G, Kazlov I, Juhásová A. Instance Deadlock: A Mystery behind Frozen
Programs. In: Applications and Theory of Petri Nets. Berlin, Heidelberg:
Springer Berlin Heidelberg; 2010:1-17. doi:10.1007/978-3-642-13675-7_1'
apa: 'Juhás, G., Kazlov, I., & Juhásová, A. (2010). Instance Deadlock: A Mystery
behind Frozen Programs. In Applications and Theory of Petri Nets (pp. 1–17).
Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-13675-7_1'
chicago: 'Juhás, Gabriel, Igor Kazlov, and Ana Juhásová. “Instance Deadlock: A Mystery
behind Frozen Programs.” In Applications and Theory of Petri Nets, 1–17.
Berlin, Heidelberg: Springer Berlin Heidelberg, 2010. https://doi.org/10.1007/978-3-642-13675-7_1.'
ieee: 'G. Juhás, I. Kazlov, and A. Juhásová, “Instance Deadlock: A Mystery behind
Frozen Programs,” in Applications and Theory of Petri Nets, Berlin, Heidelberg:
Springer Berlin Heidelberg, 2010, pp. 1–17.'
ista: 'Juhás G, Kazlov I, Juhásová A. 2010.Instance Deadlock: A Mystery behind Frozen
Programs. In: Applications and Theory of Petri Nets. , 1–17.'
mla: 'Juhás, Gabriel, et al. “Instance Deadlock: A Mystery behind Frozen Programs.”
Applications and Theory of Petri Nets, Springer Berlin Heidelberg, 2010,
pp. 1–17, doi:10.1007/978-3-642-13675-7_1.'
short: G. Juhás, I. Kazlov, A. Juhásová, in:, Applications and Theory of Petri Nets,
Springer Berlin Heidelberg, Berlin, Heidelberg, 2010, pp. 1–17.
date_created: 2019-02-08T09:33:41Z
date_published: 2010-01-01T00:00:00Z
date_updated: 2022-04-01T13:45:24Z
doi: 10.1007/978-3-642-13675-7_1
extern: '1'
fulldoi: https://doi.org/10.1007/978-3-642-13675-7_1
language:
- iso: eng
oa_version: None
page: 1-17
place: Berlin, Heidelberg
publication: Applications and Theory of Petri Nets
publication_identifier:
isbn:
- '9783642136740'
- '9783642136757'
issn:
- 0302-9743
- 1611-3349
publication_status: published
publisher: Springer Berlin Heidelberg
status: public
title: 'Instance Deadlock: A Mystery behind Frozen Programs'
type: book_chapter
user_id: 4A997E50-F248-11E8-B48F-1D18A9856A87
year: '2010'
...
---
_id: '598'
abstract:
- lang: eng
text: It is not well understood how the human Mediator complex, transcription factor
IIH and RNA polymerase II (Pol II) work together with activators to initiate transcription.
Activator binding alters Mediator structure, yet the functional consequences of
such structural shifts remain unknown. The p53 C terminus and its activation domain
interact with different Mediator subunits, and we find that each interaction differentially
affects Mediator structure; strikingly, distinct p53-Mediator structures differentially
affect Pol II activity. Only the p53 activation domain induces the formation of
a large pocket domain at the Mediator-Pol II interaction site, and this correlates
with activation of stalled Pol II to a productively elongating state. Moreover,
we define a Mediator requirement for TFIIH-dependent Pol II C-terminal domain
phosphorylation and identify substantial differences in Pol II C-terminal domain
processing that correspond to distinct p53-Mediator structural states. Our results
define a fundamental mechanism by which p53 activates transcription and suggest
that Mediator structural shifts trigger activation of stalled Pol II complexes.
article_processing_charge: No
author:
- first_name: Krista
full_name: Meyer, Krista
last_name: Meyer
- first_name: Shih
full_name: Lin, Shih
last_name: Lin
- first_name: Carrie A
full_name: Bernecky, Carrie A
id: 2CB9DFE2-F248-11E8-B48F-1D18A9856A87
last_name: Bernecky
orcid: 0000-0003-0893-7036
- first_name: Yuefeng
full_name: Gao, Yuefeng
last_name: Gao
- first_name: Dylan
full_name: Taatjes, Dylan
last_name: Taatjes
citation:
ama: Meyer K, Lin S, Bernecky C, Gao Y, Taatjes D. P53 activates transcription by
directing structural shifts in Mediator. Nature Structural and Molecular Biology.
2010;17(6):753-760. doi:10.1038/nsmb.1816
apa: Meyer, K., Lin, S., Bernecky, C., Gao, Y., & Taatjes, D. (2010). P53 activates
transcription by directing structural shifts in Mediator. Nature Structural
and Molecular Biology. Nature Publishing Group. https://doi.org/10.1038/nsmb.1816
chicago: Meyer, Krista, Shih Lin, Carrie Bernecky, Yuefeng Gao, and Dylan Taatjes.
“P53 Activates Transcription by Directing Structural Shifts in Mediator.” Nature
Structural and Molecular Biology. Nature Publishing Group, 2010. https://doi.org/10.1038/nsmb.1816.
ieee: K. Meyer, S. Lin, C. Bernecky, Y. Gao, and D. Taatjes, “P53 activates transcription
by directing structural shifts in Mediator,” Nature Structural and Molecular
Biology, vol. 17, no. 6. Nature Publishing Group, pp. 753–760, 2010.
ista: Meyer K, Lin S, Bernecky C, Gao Y, Taatjes D. 2010. P53 activates transcription
by directing structural shifts in Mediator. Nature Structural and Molecular Biology.
17(6), 753–760.
mla: Meyer, Krista, et al. “P53 Activates Transcription by Directing Structural
Shifts in Mediator.” Nature Structural and Molecular Biology, vol. 17,
no. 6, Nature Publishing Group, 2010, pp. 753–60, doi:10.1038/nsmb.1816.
short: K. Meyer, S. Lin, C. Bernecky, Y. Gao, D. Taatjes, Nature Structural and
Molecular Biology 17 (2010) 753–760.
date_created: 2018-12-11T11:47:24Z
date_published: 2010-06-01T00:00:00Z
date_updated: 2021-01-12T08:05:28Z
day: '01'
doi: 10.1038/nsmb.1816
extern: '1'
fulldoi: https://doi.org/10.1038/nsmb.1816
intvolume: ' 17'
issue: '6'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC2932482/
month: '06'
oa: 1
oa_version: None
page: 753 - 760
publication: Nature Structural and Molecular Biology
publication_status: published
publisher: Nature Publishing Group
publist_id: '7210'
status: public
title: P53 activates transcription by directing structural shifts in Mediator
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 17
year: '2010'
...
---
_id: '6142'
abstract:
- lang: eng
text: Defining the mutational landscape when individuals of a species grow separately
and diverge over many generations can provide insights into trait evolution. A
specific example of this involves studying changes associated with domestication
where different lines of the same wild stock have been cultivated independently
in different standard environments. Whole genome sequence comparison of such lines
permits estimation of mutation rates, inference of genes' ancestral states and
ancestry of existing strains, and correction of sequencing errors in genome databases.
Here we study domestication of the C. elegans Bristol strain as a model, and report
the genome sequence of LSJ1 (Bristol), a sibling of the standard C. elegans reference
wild type N2 (Bristol). The LSJ1 and N2 lines were cultivated separately from
shortly after the Bristol strain was isolated until methods to freeze C. elegans
were developed. We find that during this time the two strains have accumulated
1208 genetic differences. We describe phenotypic variation between N2 and LSJ1
in the rate at which embryos develop, the rate of production of eggs, the maturity
of eggs at laying, and feeding behavior, all the result of post-isolation changes.
We infer the ancestral alleles in the original Bristol isolate and highlight 2038
likely sequencing errors in the original N2 reference genome sequence. Many of
these changes modify genome annotation. Our study provides a starting point to
further investigate genotype-phenotype association and offers insights into the
process of selection as a result of laboratory domestication.
article_number: e13922
author:
- first_name: Katherine P.
full_name: Weber, Katherine P.
last_name: Weber
- first_name: Subhajyoti
full_name: De, Subhajyoti
last_name: De
- first_name: Iwanka
full_name: Kozarewa, Iwanka
last_name: Kozarewa
- first_name: Daniel J.
full_name: Turner, Daniel J.
last_name: Turner
- first_name: M. Madan
full_name: Babu, M. Madan
last_name: Babu
- first_name: Mario
full_name: de Bono, Mario
id: 4E3FF80E-F248-11E8-B48F-1D18A9856A87
last_name: de Bono
orcid: 0000-0001-8347-0443
citation:
ama: Weber KP, De S, Kozarewa I, Turner DJ, Babu MM, de Bono M. Whole genome sequencing
highlights genetic changes associated with laboratory domestication of C. elegans.
PLoS ONE. 2010;5(11). doi:10.1371/journal.pone.0013922
apa: Weber, K. P., De, S., Kozarewa, I., Turner, D. J., Babu, M. M., & de Bono,
M. (2010). Whole genome sequencing highlights genetic changes associated with
laboratory domestication of C. elegans. PLoS ONE. Public Library of Science.
https://doi.org/10.1371/journal.pone.0013922
chicago: Weber, Katherine P., Subhajyoti De, Iwanka Kozarewa, Daniel J. Turner,
M. Madan Babu, and Mario de Bono. “Whole Genome Sequencing Highlights Genetic
Changes Associated with Laboratory Domestication of C. Elegans.” PLoS ONE.
Public Library of Science, 2010. https://doi.org/10.1371/journal.pone.0013922.
ieee: K. P. Weber, S. De, I. Kozarewa, D. J. Turner, M. M. Babu, and M. de Bono,
“Whole genome sequencing highlights genetic changes associated with laboratory
domestication of C. elegans,” PLoS ONE, vol. 5, no. 11. Public Library
of Science, 2010.
ista: Weber KP, De S, Kozarewa I, Turner DJ, Babu MM, de Bono M. 2010. Whole genome
sequencing highlights genetic changes associated with laboratory domestication
of C. elegans. PLoS ONE. 5(11), e13922.
mla: Weber, Katherine P., et al. “Whole Genome Sequencing Highlights Genetic Changes
Associated with Laboratory Domestication of C. Elegans.” PLoS ONE, vol.
5, no. 11, e13922, Public Library of Science, 2010, doi:10.1371/journal.pone.0013922.
short: K.P. Weber, S. De, I. Kozarewa, D.J. Turner, M.M. Babu, M. de Bono, PLoS
ONE 5 (2010).
date_created: 2019-03-20T15:20:30Z
date_published: 2010-11-11T00:00:00Z
date_updated: 2021-01-12T08:06:20Z
day: '11'
ddc:
- '570'
doi: 10.1371/journal.pone.0013922
extern: '1'
external_id:
pmid:
- '21085631'
file:
- access_level: open_access
checksum: a01e6bbe15f044c0c79a26d7d881953e
content_type: application/pdf
creator: kschuh
date_created: 2019-03-20T15:22:48Z
date_updated: 2020-07-14T12:47:20Z
file_id: '6143'
file_name: 2010_PLOS_Weber.PDF
file_size: 578059
relation: main_file
file_date_updated: 2020-07-14T12:47:20Z
fulldoi: https://doi.org/10.1371/journal.pone.0013922
has_accepted_license: '1'
intvolume: ' 5'
issue: '11'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
pmid: 1
publication: PLoS ONE
publication_identifier:
issn:
- 1932-6203
publication_status: published
publisher: Public Library of Science
quality_controlled: '1'
status: public
title: Whole genome sequencing highlights genetic changes associated with laboratory
domestication of C. elegans
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 5
year: '2010'
...
---
_id: '619'
abstract:
- lang: eng
text: Sinclair Ross’s novel As for Me and My House has long since been canonized
as Canadian prairie fiction. Accordingly, it has been the subject of many critical
studies and academic papers. Most commentators have concentrated on such literary
issues as the representation of the western landscape or the reliability of the
female narrator. But so far little consideration has been given to the social
and cultural implications of the novel. Few attempts have been made to analyze
the text from a cultural perspective including such social markers as class, gender
and ethnicity. That is all the more surprising because Sinclair Ross has often
been credited for being a realistic author and As for Me and My House has often
been interpreted as a regional novel characteristic of a particular time and place.
author:
- first_name: Waldemar
full_name: Zacharasiewicz, Waldemar
last_name: Zacharasiewicz
- first_name: Fritz
full_name: Kirsch, Fritz Peter
last_name: Kirsch
citation:
ama: 'Zacharasiewicz W, Kirsch F. “This is a fundamentalist town”: The Prairie Town
as a Site of Social and Cultural Conflict in Sinclair Ross’s As for Me and My
House. In: Social and Cultural Interaction and Literary Landscapes in the Canadian
West : Impressions of an Exploratory Field Trip and Academic Interaction in the
Canadian West : Rapports Interculturels et Paysages Littéraires Dans l’Ouest Canadien.
Facultas.WUV; 2010:173-179.'
apa: 'Zacharasiewicz, W., & Kirsch, F. (2010). “This is a fundamentalist town”:
The Prairie Town as a Site of Social and Cultural Conflict in Sinclair Ross’s
As for Me and My House. In Social and cultural interaction and literary landscapes
in the Canadian West : impressions of an exploratory field trip and academic interaction
in the Canadian West : Rapports interculturels et paysages littéraires dans l’Ouest
canadien (pp. 173–179). Facultas.WUV.'
chicago: 'Zacharasiewicz, Waldemar, and Fritz Kirsch. “‘This Is a Fundamentalist
Town’: The Prairie Town as a Site of Social and Cultural Conflict in Sinclair
Ross’s As for Me and My House.” In Social and Cultural Interaction and Literary
Landscapes in the Canadian West : Impressions of an Exploratory Field Trip and
Academic Interaction in the Canadian West : Rapports Interculturels et Paysages
Littéraires Dans l’Ouest Canadien, 173–79. Facultas.WUV, 2010.'
ieee: 'W. Zacharasiewicz and F. Kirsch, “‘This is a fundamentalist town’: The Prairie
Town as a Site of Social and Cultural Conflict in Sinclair Ross’s As for Me and
My House,” in Social and cultural interaction and literary landscapes in the
Canadian West : impressions of an exploratory field trip and academic interaction
in the Canadian West : Rapports interculturels et paysages littéraires dans l’Ouest
canadien, Facultas.WUV, 2010, pp. 173–179.'
ista: 'Zacharasiewicz W, Kirsch F. 2010.“This is a fundamentalist town”: The Prairie
Town as a Site of Social and Cultural Conflict in Sinclair Ross’s As for Me and
My House. In: Social and cultural interaction and literary landscapes in the Canadian
West : impressions of an exploratory field trip and academic interaction in the
Canadian West : Rapports interculturels et paysages littéraires dans l’Ouest canadien.
, 173–179.'
mla: 'Zacharasiewicz, Waldemar, and Fritz Kirsch. “‘This Is a Fundamentalist Town’:
The Prairie Town as a Site of Social and Cultural Conflict in Sinclair Ross’s
As for Me and My House.” Social and Cultural Interaction and Literary Landscapes
in the Canadian West : Impressions of an Exploratory Field Trip and Academic Interaction
in the Canadian West : Rapports Interculturels et Paysages Littéraires Dans l’Ouest
Canadien, Facultas.WUV, 2010, pp. 173–79.'
short: 'W. Zacharasiewicz, F. Kirsch, in:, Social and Cultural Interaction and Literary
Landscapes in the Canadian West : Impressions of an Exploratory Field Trip and
Academic Interaction in the Canadian West : Rapports Interculturels et Paysages
Littéraires Dans l’Ouest Canadien, Facultas.WUV, 2010, pp. 173–179.'
date_created: 2018-12-11T11:47:32Z
date_published: 2010-01-01T00:00:00Z
date_updated: 2021-01-12T08:06:40Z
day: '01'
extern: 1
month: '01'
page: 173 - 179
publication: 'Social and cultural interaction and literary landscapes in the Canadian
West : impressions of an exploratory field trip and academic interaction in the
Canadian West : Rapports interculturels et paysages littéraires dans l''Ouest canadien'
publication_status: published
publisher: Facultas.WUV
publist_id: '7185'
quality_controlled: 0
status: public
title: '“This is a fundamentalist town”: The Prairie Town as a Site of Social and
Cultural Conflict in Sinclair Ross’s As for Me and My House'
type: book_chapter
year: '2010'
...
---
_id: '6198'
abstract:
- lang: eng
text: 'Stroke is a major public health problem leading to high rates of death and
disability in adults. Excessive stimulation of N-methyl-D-aspartate receptors
(NMDARs) and the resulting neuronal nitric oxide synthase (nNOS) activation are
crucial for neuronal injury after stroke insult. However, directly inhibiting
NMDARs or nNOS can cause severe side effects because they have key physiological
functions in the CNS. Here we show that cerebral ischemia induces the interaction
of nNOS with postsynaptic density protein-95 (PSD-95). Disrupting nNOS-PSD-95
interaction via overexpressing the N-terminal amino acid residues 1-133 of nNOS
(nNOS-N(1-133)) prevented glutamate-induced excitotoxicity and cerebral ischemic
damage. Given the mechanism of nNOS-PSD-95 interaction, we developed a series
of compounds and discovered a small-molecular inhibitor of the nNOS-PSD-95 interaction,
ZL006. This drug blocked the ischemia-induced nNOS-PSD-95 association selectively,
had potent neuroprotective activity in vitro and ameliorated focal cerebral ischemic
damage in mice and rats subjected to middle cerebral artery occlusion (MCAO) and
reperfusion. Moreover, it readily crossed the blood-brain barrier, did not inhibit
NMDAR function, catalytic activity of nNOS or spatial memory, and had no effect
on aggressive behaviors. Thus, this new drug may serve as a treatment for stroke,
perhaps without major side effects. '
author:
- first_name: L
full_name: Zhou, L
last_name: Zhou
- first_name: F
full_name: Li, F
last_name: Li
- first_name: Haibing
full_name: Xu, Haibing
id: 310349D0-F248-11E8-B48F-1D18A9856A87
last_name: Xu
- first_name: CX
full_name: Luo, CX
last_name: Luo
- first_name: HY
full_name: Wu, HY
last_name: Wu
- first_name: MM
full_name: Zhu, MM
last_name: Zhu
- first_name: W
full_name: Lu, W
last_name: Lu
- first_name: X
full_name: Ji, X
last_name: Ji
- first_name: QG
full_name: Zhou, QG
last_name: Zhou
- first_name: DY
full_name: Zhu, DY
last_name: Zhu
citation:
ama: Zhou L, Li F, Xu H, et al. Treatment of cerebral ischemia by disrupting ischemia-induced
interaction of nNOS with PSD-95. Nature Medicine. 2010;16(12):1439-1443.
doi:10.1038/nm.2245
apa: Zhou, L., Li, F., Xu, H., Luo, C., Wu, H., Zhu, M., … Zhu, D. (2010). Treatment
of cerebral ischemia by disrupting ischemia-induced interaction of nNOS with PSD-95.
Nature Medicine. Nature Publishing Group. https://doi.org/10.1038/nm.2245
chicago: Zhou, L, F Li, Haibing Xu, CX Luo, HY Wu, MM Zhu, W Lu, X Ji, QG Zhou,
and DY Zhu. “Treatment of Cerebral Ischemia by Disrupting Ischemia-Induced Interaction
of NNOS with PSD-95.” Nature Medicine. Nature Publishing Group, 2010. https://doi.org/10.1038/nm.2245.
ieee: L. Zhou et al., “Treatment of cerebral ischemia by disrupting ischemia-induced
interaction of nNOS with PSD-95,” Nature Medicine, vol. 16, no. 12. Nature
Publishing Group, pp. 1439–1443, 2010.
ista: Zhou L, Li F, Xu H, Luo C, Wu H, Zhu M, Lu W, Ji X, Zhou Q, Zhu D. 2010. Treatment
of cerebral ischemia by disrupting ischemia-induced interaction of nNOS with PSD-95.
Nature Medicine. 16(12), 1439–1443.
mla: Zhou, L., et al. “Treatment of Cerebral Ischemia by Disrupting Ischemia-Induced
Interaction of NNOS with PSD-95.” Nature Medicine, vol. 16, no. 12, Nature
Publishing Group, 2010, pp. 1439–43, doi:10.1038/nm.2245.
short: L. Zhou, F. Li, H. Xu, C. Luo, H. Wu, M. Zhu, W. Lu, X. Ji, Q. Zhou, D. Zhu,
Nature Medicine 16 (2010) 1439–1443.
date_created: 2019-04-04T14:55:32Z
date_published: 2010-11-21T00:00:00Z
date_updated: 2021-01-12T08:06:43Z
day: '21'
doi: 10.1038/nm.2245
extern: '1'
external_id:
pmid:
- '21102461'
fulldoi: https://doi.org/10.1038/nm.2245
intvolume: ' 16'
issue: '12'
language:
- iso: eng
month: '11'
oa_version: None
page: 1439-1443
pmid: 1
publication: Nature Medicine
publication_identifier:
issn:
- 1078-8956
- 1546-170x
publication_status: published
publisher: Nature Publishing Group
quality_controlled: '1'
status: public
title: Treatment of cerebral ischemia by disrupting ischemia-induced interaction of
nNOS with PSD-95
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 16
year: '2010'
...
---
_id: '2071'
abstract:
- lang: eng
text: The X or Z chromosome has several characteristics that distinguish it from
the autosomes, namely hemizygosity in the heterogametic sex, and a potentially
different effective population size, both of which may influence the rate and
nature of evolution. In particular, there may be an accelerated rate of adaptive
change for X-linked compared to autosomal coding sequences, often referred to
as the Faster-X effect. Empirical studies have indicated that the strength of
Faster-X evolution varies among different species, and theoretical treatments
have shown that demography and mating system can substantially affect the degree
of Faster-X evolution. Here we integrate genomic data on Faster-X evolution from
a variety of animals with the demographic factors, mating system, and sex chromosome
regulatory characteristics that may influence it. Our results suggest that differences
in effective population size and mechanisms of dosage compensation may influence
the perceived extent of Faster-X evolution, and help to explain several clade-specific
patterns that we observe.
acknowledgement: We gratefully acknowledge funding from the Royal Society (to JEM)
author:
- first_name: Judith
full_name: Mank, Judith E
last_name: Mank
- first_name: Beatriz
full_name: Beatriz Vicoso
id: 49E1C5C6-F248-11E8-B48F-1D18A9856A87
last_name: Vicoso
orcid: 0000-0002-4579-8306
- first_name: Sofia
full_name: Berlin, Sofia
last_name: Berlin
- first_name: Brian
full_name: Charlesworth, Brian
last_name: Charlesworth
citation:
ama: 'Mank J, Vicoso B, Berlin S, Charlesworth B. Effective population size and
the Faster-X effect: Empirical results and their interpretation. Evolution.
2010;64(3):663-674. doi:10.1111/j.1558-5646.2009.00853.x'
apa: 'Mank, J., Vicoso, B., Berlin, S., & Charlesworth, B. (2010). Effective
population size and the Faster-X effect: Empirical results and their interpretation.
Evolution. Wiley-Blackwell. https://doi.org/10.1111/j.1558-5646.2009.00853.x'
chicago: 'Mank, Judith, Beatriz Vicoso, Sofia Berlin, and Brian Charlesworth. “Effective
Population Size and the Faster-X Effect: Empirical Results and Their Interpretation.”
Evolution. Wiley-Blackwell, 2010. https://doi.org/10.1111/j.1558-5646.2009.00853.x.'
ieee: 'J. Mank, B. Vicoso, S. Berlin, and B. Charlesworth, “Effective population
size and the Faster-X effect: Empirical results and their interpretation,” Evolution,
vol. 64, no. 3. Wiley-Blackwell, pp. 663–674, 2010.'
ista: 'Mank J, Vicoso B, Berlin S, Charlesworth B. 2010. Effective population size
and the Faster-X effect: Empirical results and their interpretation. Evolution.
64(3), 663–674.'
mla: 'Mank, Judith, et al. “Effective Population Size and the Faster-X Effect: Empirical
Results and Their Interpretation.” Evolution, vol. 64, no. 3, Wiley-Blackwell,
2010, pp. 663–74, doi:10.1111/j.1558-5646.2009.00853.x.'
short: J. Mank, B. Vicoso, S. Berlin, B. Charlesworth, Evolution 64 (2010) 663–674.
date_created: 2018-12-11T11:55:32Z
date_published: 2010-03-01T00:00:00Z
date_updated: 2021-01-12T06:55:07Z
day: '01'
doi: 10.1111/j.1558-5646.2009.00853.x
extern: 1
fulldoi: https://doi.org/10.1111/j.1558-5646.2009.00853.x
intvolume: ' 64'
issue: '3'
month: '03'
page: 663 - 674
publication: Evolution
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4967'
quality_controlled: 0
status: public
title: 'Effective population size and the Faster-X effect: Empirical results and their
interpretation'
type: journal_article
volume: 64
year: '2010'
...
---
_id: '2075'
abstract:
- lang: eng
text: "This thesis investigates the combination of data-driven and physically based
techniques for acquiring, modeling, and animating deformable materials, with a
special focus on human faces. Furthermore, based on these techniques, we introduce
a data-driven process for designing and fabricating materials with desired deformation
behavior. \nRealistic simulation behavior, surface details, and appearance are
still demanding tasks. Neither pure data-driven, pure procedural, nor pure physical
methods are best suited for accurate synthesis of facial motion and details (both
for appearance and geometry), due to the difficulties in model design, parameter
estimation, and desired controllability for animators. Capturing of a small but
representative amount of real data, and then synthesizing diverse on-demand examples
with physically-based models and real data as input benefits from both sides:
Highly realistic model behavior due to real-world data and controllability due
to physically-based models.\nTo model the face and its behavior, hybrid physically-based
and data-driven approaches are elaborated. We investigate surface-based representations
as well as a solid representation based on FEM. To achieve realistic behavior,
we propose to build light-weighted data capture devices to acquire real-world
data to estimate model parameters and to employ concepts from data-driven modeling
techniques and machine learning. The resulting models support simple acquisition
systems, offer techniques to process and extract model parameters from real-world
data, provide a compact representation of the facial geometry and its motion,
and allow intuitive editing. We demonstrate applications such as capture of facial
geometry and motion and real-time animation and transfer of facial details, and
show that our soft tissue model can react to external forces and produce realistic
deformations beyond facial expressions.\nBased on this model, we furthermore introduce
a data-driven process for designing and fabricating materials with desired deformation
behavior. The process starts with measuring deformation properties of base materials.
Each material is represented as a non-linear stress-strain relationship in a finite-element
model. For material design and fabrication, we introduce an optimization process
that finds the best combination of base materials that meets a user’s criteria
specified by example deformations. Our algorithm employs a number of strategies
to prune poor solutions from the combinatorial search space. We finally demonstrate
the complete process by designing and fabricating objects with complex heterogeneous
materials using modern multi-material 3D printers.\n"
author:
- first_name: Bernd
full_name: Bernd Bickel
id: 49876194-F248-11E8-B48F-1D18A9856A87
last_name: Bickel
orcid: 0000-0001-6511-9385
citation:
ama: Bickel B. Measurement-based modeling and fabrication of deformable materials
for human faces. Unknown. 2010;499(7458). doi:dx.doi.org/10.3929/ethz-a-006354908
apa: Bickel, B. (2010). Measurement-based modeling and fabrication of deformable
materials for human faces. Unknown. Unknown. https://doi.org/dx.doi.org/10.3929/ethz-a-006354908
chicago: Bickel, Bernd. “Measurement-Based Modeling and Fabrication of Deformable
Materials for Human Faces.” Unknown. Unknown, 2010. https://doi.org/dx.doi.org/10.3929/ethz-a-006354908.
ieee: B. Bickel, “Measurement-based modeling and fabrication of deformable materials
for human faces,” Unknown, 2010.
ista: Bickel B. 2010. Measurement-based modeling and fabrication of deformable materials
for human faces. Unknown.
mla: Bickel, Bernd. “Measurement-Based Modeling and Fabrication of Deformable Materials
for Human Faces.” Unknown, vol. 499, no. 7458, Unknown, 2010, doi:dx.doi.org/10.3929/ethz-a-006354908.
short: B. Bickel, Measurement-Based Modeling and Fabrication of Deformable Materials
for Human Faces, Unknown, 2010.
date_created: 2018-12-11T11:55:34Z
date_published: 2010-01-01T00:00:00Z
date_updated: 2021-01-12T06:55:09Z
day: '01'
doi: dx.doi.org/10.3929/ethz-a-006354908
extern: 1
fulldoi: https://doi.org/dx.doi.org/10.3929/ethz-a-006354908
intvolume: ' 499'
issue: '7458'
month: '01'
publication: Unknown
publication_status: published
publisher: Unknown
publist_id: '4963'
quality_controlled: 0
status: public
title: Measurement-based modeling and fabrication of deformable materials for human
faces
type: dissertation
volume: 499
year: '2010'
...
---
_id: '10127'
abstract:
- lang: eng
text: We use numerical simulations to show how noninteracting hard particles binding
to a deformable elastic shell may self-assemble into a variety of linear patterns.
This is a result of the nontrivial elastic response to deformations of shells.
The morphology of the patterns can be controlled by the mechanical properties
of the surface, and can be fine-tuned by varying the binding energy of the particles.
We also repeat our calculations for a fully flexible chain and find that the chain
conformations follow patterns similar to those formed by the nanoparticles under
analogous conditions. We propose a simple way of understanding and sorting the
different structures and relate it to the underlying shape transition of the shell.
Finally, we discuss the implications of our results.
acknowledgement: This work was supported by the National Science Foundation under
Career Grant No. DMR-0846426. We thank Josep C. Pàmies for helpful discussions.
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Anđela
full_name: Šarić, Anđela
id: bf63d406-f056-11eb-b41d-f263a6566d8b
last_name: Šarić
orcid: 0000-0002-7854-2139
- first_name: Angelo
full_name: Cacciuto, Angelo
last_name: Cacciuto
citation:
ama: Šarić A, Cacciuto A. Particle self-assembly on soft elastic shells. Soft
Matter. 2010;7(5):1874-1878. doi:10.1039/c0sm01143f
apa: Šarić, A., & Cacciuto, A. (2010). Particle self-assembly on soft elastic
shells. Soft Matter. Royal Society of Chemistry (RSC). https://doi.org/10.1039/c0sm01143f
chicago: Šarić, Anđela, and Angelo Cacciuto. “Particle Self-Assembly on Soft Elastic
Shells.” Soft Matter. Royal Society of Chemistry (RSC), 2010. https://doi.org/10.1039/c0sm01143f.
ieee: A. Šarić and A. Cacciuto, “Particle self-assembly on soft elastic shells,”
Soft Matter, vol. 7, no. 5. Royal Society of Chemistry (RSC), pp. 1874–1878,
2010.
ista: Šarić A, Cacciuto A. 2010. Particle self-assembly on soft elastic shells.
Soft Matter. 7(5), 1874–1878.
mla: Šarić, Anđela, and Angelo Cacciuto. “Particle Self-Assembly on Soft Elastic
Shells.” Soft Matter, vol. 7, no. 5, Royal Society of Chemistry (RSC),
2010, pp. 1874–78, doi:10.1039/c0sm01143f.
short: A. Šarić, A. Cacciuto, Soft Matter 7 (2010) 1874–1878.
date_created: 2021-10-12T08:34:23Z
date_published: 2010-12-23T00:00:00Z
date_updated: 2021-10-12T09:49:27Z
day: '23'
doi: 10.1039/c0sm01143f
extern: '1'
external_id:
arxiv:
- '1010.2453'
fulldoi: https://doi.org/10.1039/c0sm01143f
intvolume: ' 7'
issue: '5'
keyword:
- condensed matter physics
- general chemistry
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1010.2453
month: '12'
oa: 1
oa_version: Preprint
page: 1874-1878
publication: Soft Matter
publication_identifier:
issn:
- 1744-683X
- 1744-6848
publication_status: published
publisher: Royal Society of Chemistry (RSC)
quality_controlled: '1'
status: public
title: Particle self-assembly on soft elastic shells
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 7
year: '2010'
...