---
_id: '3990'
abstract:
- lang: eng
text: The writhing number measures the global geometry of a closed space curve or
knot. We show that this measure is related to the average winding number of its
Gauss map. Using this relationship, we give an algorithm for computing the writhing
number for a polygonal knot with n edges in time roughly proportional to n(1.6).
We also implement a different, simple algorithm and provide experimental evidence
for its practical efficiency.
acknowledgement: Partially supported by NSF under grants CCR-00-86013, EIA-9972879
and NSF under grant CCR-97-12088.
author:
- first_name: Pankaj
full_name: Agarwal, Pankaj K
last_name: Agarwal
- first_name: Herbert
full_name: Herbert Edelsbrunner
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Yusu
full_name: Wang, Yusu
last_name: Wang
citation:
ama: Agarwal P, Edelsbrunner H, Wang Y. Computing the writhing number of a polygonal
knot. Discrete & Computational Geometry. 2004;32(1):37-53. doi:10.1007/s00454-004-2864-x
apa: Agarwal, P., Edelsbrunner, H., & Wang, Y. (2004). Computing the writhing
number of a polygonal knot. Discrete & Computational Geometry. Springer.
https://doi.org/10.1007/s00454-004-2864-x
chicago: Agarwal, Pankaj, Herbert Edelsbrunner, and Yusu Wang. “Computing the Writhing
Number of a Polygonal Knot.” Discrete & Computational Geometry. Springer,
2004. https://doi.org/10.1007/s00454-004-2864-x.
ieee: P. Agarwal, H. Edelsbrunner, and Y. Wang, “Computing the writhing number of
a polygonal knot,” Discrete & Computational Geometry, vol. 32, no.
1. Springer, pp. 37–53, 2004.
ista: Agarwal P, Edelsbrunner H, Wang Y. 2004. Computing the writhing number of
a polygonal knot. Discrete & Computational Geometry. 32(1), 37–53.
mla: Agarwal, Pankaj, et al. “Computing the Writhing Number of a Polygonal Knot.”
Discrete & Computational Geometry, vol. 32, no. 1, Springer, 2004,
pp. 37–53, doi:10.1007/s00454-004-2864-x.
short: P. Agarwal, H. Edelsbrunner, Y. Wang, Discrete & Computational Geometry
32 (2004) 37–53.
date_created: 2018-12-11T12:06:18Z
date_published: 2004-05-01T00:00:00Z
date_updated: 2021-01-12T07:53:42Z
day: '01'
doi: 10.1007/s00454-004-2864-x
extern: 1
intvolume: ' 32'
issue: '1'
month: '05'
page: 37 - 53
publication: Discrete & Computational Geometry
publication_status: published
publisher: Springer
publist_id: '2138'
quality_controlled: 0
status: public
title: Computing the writhing number of a polygonal knot
type: journal_article
volume: 32
year: '2004'
...
---
_id: '4172'
abstract:
- lang: eng
text: 'During vertebrate gastrulation, a relatively limited number of blastodermal
cells undergoes a stereotypical set of cellular movements that leads to formation
of the three germ layers: ectoderm, mesoderm and endoderm. Gastrulation, therefore,
provides a unique developmental system in which to study cell movements in vivo
in a fairly simple cellular context. Recent advances have been made in elucidating
the cellular and molecular mechanisms that underlie cell movements during zebrafish
gastrulation. These findings can be compared with observations made in other model
systems to identify potential general mechanisms of cell migration during development.'
article_processing_charge: No
author:
- first_name: Juan
full_name: Montero, Juan
last_name: Montero
- first_name: Carl-Philipp J
full_name: Heisenberg, Carl-Philipp J
id: 39427864-F248-11E8-B48F-1D18A9856A87
last_name: Heisenberg
orcid: 0000-0002-0912-4566
citation:
ama: 'Montero J, Heisenberg C-PJ. Gastrulation dynamics: cells move into focus.
Trends in Cell Biology. 2004;14(11):620-627. doi:10.1016/j.tcb.2004.09.008'
apa: 'Montero, J., & Heisenberg, C.-P. J. (2004). Gastrulation dynamics: cells
move into focus. Trends in Cell Biology. Cell Press. https://doi.org/10.1016/j.tcb.2004.09.008'
chicago: 'Montero, Juan, and Carl-Philipp J Heisenberg. “Gastrulation Dynamics:
Cells Move into Focus.” Trends in Cell Biology. Cell Press, 2004. https://doi.org/10.1016/j.tcb.2004.09.008.'
ieee: 'J. Montero and C.-P. J. Heisenberg, “Gastrulation dynamics: cells move into
focus,” Trends in Cell Biology, vol. 14, no. 11. Cell Press, pp. 620–627,
2004.'
ista: 'Montero J, Heisenberg C-PJ. 2004. Gastrulation dynamics: cells move into
focus. Trends in Cell Biology. 14(11), 620–627.'
mla: 'Montero, Juan, and Carl-Philipp J. Heisenberg. “Gastrulation Dynamics: Cells
Move into Focus.” Trends in Cell Biology, vol. 14, no. 11, Cell Press,
2004, pp. 620–27, doi:10.1016/j.tcb.2004.09.008.'
short: J. Montero, C.-P.J. Heisenberg, Trends in Cell Biology 14 (2004) 620–627.
date_created: 2018-12-11T12:07:23Z
date_published: 2004-11-01T00:00:00Z
date_updated: 2021-01-12T07:55:02Z
day: '01'
doi: 10.1016/j.tcb.2004.09.008
extern: '1'
intvolume: ' 14'
issue: '11'
language:
- iso: eng
month: '11'
oa_version: None
page: 620 - 627
publication: Trends in Cell Biology
publication_status: published
publisher: Cell Press
publist_id: '1948'
status: public
title: 'Gastrulation dynamics: cells move into focus'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 14
year: '2004'
...
---
_id: '4224'
abstract:
- lang: eng
text: Developing cells acquire positional information by reading the graded distribution
of morphogens. In Drosophila, the Dpp morphogen forms a long-range concentration
gradient by spreading from a restricted source in the developing wing. It has
been assumed that Dpp spreads by extracellular diffusion. Under this assumption,
the main role of endocytosis in gradient formation is to downregulate receptors
at the cell surface. These surface receptors bind to the ligand and thereby interfere
with its long-range movement. Recent experiments indicate that Dpp spreading is
mediated by Dynamin-dependent endocytosis in the target tissue, suggesting that
extracellular diffusion alone cannot account for Dpp dispersal. Here, we perform
a theoretical study of a model for morphogen spreading based on extracellular
diffusion, which takes into account receptor binding and trafficking. We compare
profiles of ligand and surface receptors obtained in this model with experimental
data. To this end, we monitored directly the pool of surface receptors and extracellular
Dpp with specific antibodies. We conclude that current models considering pure
extracellular diffusion cannot explain the observed role of endocytosis during
Dpp long-range movement.
article_processing_charge: No
author:
- first_name: Karsten
full_name: Kruse, Karsten
last_name: Kruse
- first_name: Periklis
full_name: Pantazis, Periklis
last_name: Pantazis
- first_name: Mark Tobias
full_name: Bollenbach, Mark Tobias
id: 3E6DB97A-F248-11E8-B48F-1D18A9856A87
last_name: Bollenbach
orcid: 0000-0003-4398-476X
- first_name: Frank
full_name: Julicher, Frank
last_name: Julicher
- first_name: Marcos
full_name: Gonzalez Gaitan, Marcos
last_name: Gonzalez Gaitan
citation:
ama: 'Kruse K, Pantazis P, Bollenbach MT, Julicher F, Gonzalez Gaitan M. Dpp gradient
formation by dynamin-dependent endocytosis: receptor trafficking and the diffusion
model. Development. 2004;131(19):4843-4856. doi:10.1242/dev.01335'
apa: 'Kruse, K., Pantazis, P., Bollenbach, M. T., Julicher, F., & Gonzalez Gaitan,
M. (2004). Dpp gradient formation by dynamin-dependent endocytosis: receptor trafficking
and the diffusion model. Development. Company of Biologists. https://doi.org/10.1242/dev.01335'
chicago: 'Kruse, Karsten, Periklis Pantazis, Mark Tobias Bollenbach, Frank Julicher,
and Marcos Gonzalez Gaitan. “Dpp Gradient Formation by Dynamin-Dependent Endocytosis:
Receptor Trafficking and the Diffusion Model.” Development. Company of
Biologists, 2004. https://doi.org/10.1242/dev.01335.'
ieee: 'K. Kruse, P. Pantazis, M. T. Bollenbach, F. Julicher, and M. Gonzalez Gaitan,
“Dpp gradient formation by dynamin-dependent endocytosis: receptor trafficking
and the diffusion model,” Development, vol. 131, no. 19. Company of Biologists,
pp. 4843–4856, 2004.'
ista: 'Kruse K, Pantazis P, Bollenbach MT, Julicher F, Gonzalez Gaitan M. 2004.
Dpp gradient formation by dynamin-dependent endocytosis: receptor trafficking
and the diffusion model. Development. 131(19), 4843–4856.'
mla: 'Kruse, Karsten, et al. “Dpp Gradient Formation by Dynamin-Dependent Endocytosis:
Receptor Trafficking and the Diffusion Model.” Development, vol. 131, no.
19, Company of Biologists, 2004, pp. 4843–56, doi:10.1242/dev.01335.'
short: K. Kruse, P. Pantazis, M.T. Bollenbach, F. Julicher, M. Gonzalez Gaitan,
Development 131 (2004) 4843–4856.
date_created: 2018-12-11T12:07:41Z
date_published: 2004-01-01T00:00:00Z
date_updated: 2021-01-12T07:55:26Z
day: '01'
doi: 10.1242/dev.01335
extern: '1'
intvolume: ' 131'
issue: '19'
language:
- iso: eng
month: '01'
oa_version: None
page: 4843 - 4856
publication: Development
publication_status: published
publisher: Company of Biologists
publist_id: '1893'
status: public
title: 'Dpp gradient formation by dynamin-dependent endocytosis: receptor trafficking
and the diffusion model'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 131
year: '2004'
...
---
_id: '4230'
alternative_title:
- Cellular Origin and Life in Extreme Habitats and Astrobiology
author:
- first_name: Harold
full_name: Harold Vladar
id: 2A181218-F248-11E8-B48F-1D18A9856A87
last_name: Vladar
orcid: 0000-0002-5985-7653
- first_name: Roberto
full_name: Cipriani, Roberto
last_name: Cipriani
- first_name: Benjamin
full_name: Scharifker, Benjamin
last_name: Scharifker
- first_name: Jose
full_name: Bubis, Jose
last_name: Bubis
citation:
ama: 'de Vladar H, Cipriani R, Scharifker B, Bubis J. A mechanism for the prebiotic
emergence of proteins. In: Hanslmeier A, Kempe S, Seckbach J, eds. Life in
the Universe From the Miller Experiment to the Search for Life on Other Worlds.
Springer; 2004:83-87.'
apa: de Vladar, H., Cipriani, R., Scharifker, B., & Bubis, J. (2004). A mechanism
for the prebiotic emergence of proteins. In A. Hanslmeier, S. Kempe, & J.
Seckbach (Eds.), Life in the Universe From the Miller Experiment to the Search
for Life on Other Worlds (pp. 83–87). Springer.
chicago: Vladar, Harold de, Roberto Cipriani, Benjamin Scharifker, and Jose Bubis.
“A Mechanism for the Prebiotic Emergence of Proteins.” In Life in the Universe
From the Miller Experiment to the Search for Life on Other Worlds, edited
by A. Hanslmeier, S. Kempe, and J. Seckbach, 83–87. Springer, 2004.
ieee: H. de Vladar, R. Cipriani, B. Scharifker, and J. Bubis, “A mechanism for the
prebiotic emergence of proteins,” in Life in the Universe From the Miller Experiment
to the Search for Life on Other Worlds, A. Hanslmeier, S. Kempe, and J. Seckbach,
Eds. Springer, 2004, pp. 83–87.
ista: 'de Vladar H, Cipriani R, Scharifker B, Bubis J. 2004.A mechanism for the
prebiotic emergence of proteins. In: Life in the Universe From the Miller Experiment
to the Search for Life on Other Worlds. Cellular Origin and Life in Extreme Habitats
and Astrobiology, , 83–87.'
mla: de Vladar, Harold, et al. “A Mechanism for the Prebiotic Emergence of Proteins.”
Life in the Universe From the Miller Experiment to the Search for Life on Other
Worlds, edited by A. Hanslmeier et al., Springer, 2004, pp. 83–87.
short: H. de Vladar, R. Cipriani, B. Scharifker, J. Bubis, in:, A. Hanslmeier, S.
Kempe, J. Seckbach (Eds.), Life in the Universe From the Miller Experiment to
the Search for Life on Other Worlds, Springer, 2004, pp. 83–87.
date_created: 2018-12-11T12:07:44Z
date_published: 2004-12-31T00:00:00Z
date_updated: 2021-01-12T07:55:28Z
day: '31'
editor:
- first_name: A.
full_name: Hanslmeier,A.
last_name: Hanslmeier
- first_name: S.
full_name: Kempe,S.
last_name: Kempe
- first_name: J.
full_name: Seckbach,J.
last_name: Seckbach
extern: 1
month: '12'
page: 83 - 87
publication: Life in the Universe From the Miller Experiment to the Search for Life
on Other Worlds
publication_status: published
publisher: Springer
publist_id: '1884'
quality_controlled: 0
status: public
title: A mechanism for the prebiotic emergence of proteins
type: book_chapter
year: '2004'
...
---
_id: '4236'
article_processing_charge: No
author:
- first_name: Harold
full_name: de Vladar, Harold
id: 2A181218-F248-11E8-B48F-1D18A9856A87
last_name: de Vladar
orcid: 0000-0002-5985-7653
citation:
ama: de Vladar H. Métodos no lineales y sus aplicaciones en dinámicas aleatorias
de poblaciones celulares. 2004. doi:3810
apa: de Vladar, H. (2004). Métodos no lineales y sus aplicaciones en dinámicas
aleatorias de poblaciones celulares. Centro de estudios avazados, IVIC. https://doi.org/3810
chicago: Vladar, Harold de. “Métodos No Lineales y Sus Aplicaciones En Dinámicas
Aleatorias de Poblaciones Celulares.” Centro de estudios avazados, IVIC, 2004.
https://doi.org/3810.
ieee: H. de Vladar, “Métodos no lineales y sus aplicaciones en dinámicas aleatorias
de poblaciones celulares,” Centro de estudios avazados, IVIC, 2004.
ista: de Vladar H. 2004. Métodos no lineales y sus aplicaciones en dinámicas aleatorias
de poblaciones celulares. Centro de estudios avazados, IVIC.
mla: de Vladar, Harold. Métodos No Lineales y Sus Aplicaciones En Dinámicas Aleatorias
de Poblaciones Celulares. Centro de estudios avazados, IVIC, 2004, doi:3810.
short: H. de Vladar, Métodos No Lineales y Sus Aplicaciones En Dinámicas Aleatorias
de Poblaciones Celulares, Centro de estudios avazados, IVIC, 2004.
date_created: 2018-12-11T12:07:46Z
date_published: 2004-01-01T00:00:00Z
date_updated: 2021-01-12T07:55:30Z
day: '01'
doi: '3810'
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
publication_status: published
publisher: Centro de estudios avazados, IVIC
publist_id: '1877'
status: public
title: Métodos no lineales y sus aplicaciones en dinámicas aleatorias de poblaciones
celulares
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2004'
...
---
_id: '4238'
abstract:
- lang: eng
text: The dynamical basis of tumoral growth has been controversial. Many models
have been proposed to explain cancer development. The descriptions employ exponential,
potential, logistic or Gompertzian growth laws. Some of these models are concerned
with the interaction between cancer and the immunological, system. Among other
properties, these models are concerned with the microscopic behavior of tumors
and the emergence of cancer. We propose a modification of a previous model by
Stepanova, which describes the specific immunological response against cancer.
The modification consists of the substitution of a Gompertian law for the exponential
rate used for tumoral growth. This modification is motivated by the numerous works
confirming that Gompertz's equation correctly describes solid tumor growth. The
modified model predicts that near zero, tumors always tend to grow. Immunological
contraposition never suffices to induce a complete regression of the tumor. Instead,
a stable microscopic equilibrium between cancer and immunological activity can
be attained. In other words, our model predicts that the theory of immune surveillance
is plausible. A macroscopic equilibrium in which the system develops cancer is
also possible. In this case, immunological activity is depleted. This is consistent
with the phenomena of cancer tolerance. Both equilibrium points can coexist or
can exist without the other. In all cases the fixed point at zero tumor size is
unstable. Since immunity cannot induce a complete tumor regression, a therapy
is required. We include constant-dose therapies and show that they are insufficient.
Final levels of immunocompetent cells and tumoral cells are finite, thus post-treatment
regrowth of the tumor is certain. We also evaluate late-intensification therapies
which are successful. They induce an asymptotic regression to zero tumor size.
Immune response is also suppressed by the therapy, and thus plays a negligible
role in the remission. We conclude that treatment evaluation should be successful
without taking into account immunological effects. (C) 2003 Elsevier Ltd. All
rights reserved.
article_processing_charge: No
author:
- first_name: Harold
full_name: de Vladar, Harold
id: 2A181218-F248-11E8-B48F-1D18A9856A87
last_name: de Vladar
orcid: 0000-0002-5985-7653
- first_name: J.
full_name: González, J.
last_name: González
citation:
ama: de Vladar H, González J. Dynamic response of cancer under the influence of
immunological activity and therapy. Journal of Theoretical Biology. 2004;227(3):335-348.
doi:3801
apa: de Vladar, H., & González, J. (2004). Dynamic response of cancer under
the influence of immunological activity and therapy. Journal of Theoretical
Biology. Elsevier. https://doi.org/3801
chicago: Vladar, Harold de, and J. González. “Dynamic Response of Cancer under the
Influence of Immunological Activity and Therapy.” Journal of Theoretical Biology.
Elsevier, 2004. https://doi.org/3801.
ieee: H. de Vladar and J. González, “Dynamic response of cancer under the influence
of immunological activity and therapy,” Journal of Theoretical Biology,
vol. 227, no. 3. Elsevier, pp. 335–348, 2004.
ista: de Vladar H, González J. 2004. Dynamic response of cancer under the influence
of immunological activity and therapy. Journal of Theoretical Biology. 227(3),
335–348.
mla: de Vladar, Harold, and J. González. “Dynamic Response of Cancer under the Influence
of Immunological Activity and Therapy.” Journal of Theoretical Biology,
vol. 227, no. 3, Elsevier, 2004, pp. 335–48, doi:3801.
short: H. de Vladar, J. González, Journal of Theoretical Biology 227 (2004) 335–348.
date_created: 2018-12-11T12:07:46Z
date_published: 2004-01-01T00:00:00Z
date_updated: 2021-01-12T07:55:31Z
day: '01'
doi: '3801'
extern: '1'
intvolume: ' 227'
issue: '3'
language:
- iso: eng
month: '01'
oa_version: None
page: 335 - 348
publication: Journal of Theoretical Biology
publication_status: published
publisher: Elsevier
publist_id: '1876'
status: public
title: Dynamic response of cancer under the influence of immunological activity and
therapy
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 227
year: '2004'
...
---
_id: '4239'
alternative_title:
- Cellular Origin, Life in Extreme Habitats and Astrobiology
author:
- first_name: Harold
full_name: Harold Vladar
id: 2A181218-F248-11E8-B48F-1D18A9856A87
last_name: Vladar
orcid: 0000-0002-5985-7653
- first_name: Roberto
full_name: 'Cipriani, Roberto '
last_name: Cipriani
- first_name: Benjamin
full_name: Scharifker, Benjamin
last_name: Scharifker
- first_name: Jose
full_name: Bubis, Jose
last_name: Bubis
citation:
ama: 'de Vladar H, Cipriani R, Scharifker B, Bubis J. A Mechanism for the Prebiotic
Emergence of Proteins. In: Seckbach J, Chela Flores J, Owen T, Raulin F, eds.
Life in the Universe From the Miller Experiment to the Search for Life on Other
Worlds. Vol 7. Springer; 2004:83-87. doi:3807'
apa: de Vladar, H., Cipriani, R., Scharifker, B., & Bubis, J. (2004). A Mechanism
for the Prebiotic Emergence of Proteins. In J. Seckbach, J. Chela Flores, T. Owen,
& F. Raulin (Eds.), Life in the Universe From the Miller Experiment to
the Search for Life on Other Worlds (Vol. 7, pp. 83–87). Springer. https://doi.org/3807
chicago: Vladar, Harold de, Roberto Cipriani, Benjamin Scharifker, and Jose Bubis.
“A Mechanism for the Prebiotic Emergence of Proteins.” In Life in the Universe
From the Miller Experiment to the Search for Life on Other Worlds, edited
by J. Seckbach, J. Chela Flores, T. Owen, and F. Raulin, 7:83–87. Springer, 2004.
https://doi.org/3807.
ieee: H. de Vladar, R. Cipriani, B. Scharifker, and J. Bubis, “A Mechanism for the
Prebiotic Emergence of Proteins,” in Life in the Universe From the Miller Experiment
to the Search for Life on Other Worlds, vol. 7, J. Seckbach, J. Chela Flores,
T. Owen, and F. Raulin, Eds. Springer, 2004, pp. 83–87.
ista: 'de Vladar H, Cipriani R, Scharifker B, Bubis J. 2004.A Mechanism for the
Prebiotic Emergence of Proteins. In: Life in the Universe From the Miller Experiment
to the Search for Life on Other Worlds. Cellular Origin, Life in Extreme Habitats
and Astrobiology, vol. 7, 83–87.'
mla: de Vladar, Harold, et al. “A Mechanism for the Prebiotic Emergence of Proteins.”
Life in the Universe From the Miller Experiment to the Search for Life on Other
Worlds, edited by J. Seckbach et al., vol. 7, Springer, 2004, pp. 83–87, doi:3807.
short: H. de Vladar, R. Cipriani, B. Scharifker, J. Bubis, in:, J. Seckbach, J.
Chela Flores, T. Owen, F. Raulin (Eds.), Life in the Universe From the Miller
Experiment to the Search for Life on Other Worlds, Springer, 2004, pp. 83–87.
date_created: 2018-12-11T12:07:47Z
date_published: 2004-01-01T00:00:00Z
date_updated: 2021-01-12T07:55:32Z
day: '01'
doi: '3807'
editor:
- first_name: J.
full_name: Seckbach,J.
last_name: Seckbach
- first_name: J.
full_name: Chela-Flores,J.
last_name: Chela Flores
- first_name: T.
full_name: Owen,T.
last_name: Owen
- first_name: F.
full_name: Raulin,F.
last_name: Raulin
extern: 1
intvolume: ' 7'
month: '01'
page: 83 - 87
publication: Life in the Universe From the Miller Experiment to the Search for Life
on Other Worlds
publication_status: published
publisher: Springer
publist_id: '1875'
quality_controlled: 0
status: public
title: A Mechanism for the Prebiotic Emergence of Proteins
type: book_chapter
volume: 7
year: '2004'
...
---
_id: '4253'
abstract:
- lang: eng
text: We consider a single genetic locus which carries two alleles, labelled P and
Q. This locus experiences selection and mutation. It is linked to a second neutral
locus with recombination rate r. If r = 0, this reduces to the study of a single
selected locus. Assuming a Moran model for the population dynamics, we pass to
a diffusion approximation and, assuming that the allele frequencies at the selected
locus have reached stationarity, establish the joint generating function for the
genealogy of a sample from the population and the frequency of the P allele. In
essence this is the joint generating function for a coalescent and the random
background in which it evolves. We use this to characterize, for the diffusion
approximation, the probability of identity in state at the neutral locus of a
sample of two individuals (whose type at the selected locus is known) as solutions
to a system of ordinary differential equations. The only subtlety is to find the
boundary conditions for this system. Finally, numerical examples are presented
that illustrate the accuracy and predictions of the diffusion approximation. In
particular, a comparison is made between this approach and one in which the frequencies
at the selected locus are estimated by their value in the absence of fluctuations
and a classical structured coalescent model is used.
author:
- first_name: Nicholas H
full_name: Nicholas Barton
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
- first_name: Alison
full_name: Etheridge, Alison M
last_name: Etheridge
- first_name: Anja
full_name: Sturm, Anja K
last_name: Sturm
citation:
ama: Barton NH, Etheridge A, Sturm A. Coalescence in a Random Background. Annals
of Applied Probability. 2004;14(2):754-785.
apa: Barton, N. H., Etheridge, A., & Sturm, A. (2004). Coalescence in a Random
Background. Annals of Applied Probability. Institute of Mathematical Statistics.
chicago: Barton, Nicholas H, Alison Etheridge, and Anja Sturm. “Coalescence in a
Random Background.” Annals of Applied Probability. Institute of Mathematical
Statistics, 2004.
ieee: N. H. Barton, A. Etheridge, and A. Sturm, “Coalescence in a Random Background,”
Annals of Applied Probability, vol. 14, no. 2. Institute of Mathematical
Statistics, pp. 754–785, 2004.
ista: Barton NH, Etheridge A, Sturm A. 2004. Coalescence in a Random Background.
Annals of Applied Probability. 14(2), 754–785.
mla: Barton, Nicholas H., et al. “Coalescence in a Random Background.” Annals
of Applied Probability, vol. 14, no. 2, Institute of Mathematical Statistics,
2004, pp. 754–85.
short: N.H. Barton, A. Etheridge, A. Sturm, Annals of Applied Probability 14 (2004)
754–785.
date_created: 2018-12-11T12:07:52Z
date_published: 2004-05-01T00:00:00Z
date_updated: 2021-01-12T07:55:38Z
day: '01'
extern: 1
intvolume: ' 14'
issue: '2'
main_file_link:
- open_access: '0'
url: http://www.jstor.org/stable/4140427
month: '05'
page: 754 - 785
publication: Annals of Applied Probability
publication_status: published
publisher: Institute of Mathematical Statistics
publist_id: '1842'
quality_controlled: 0
status: public
title: Coalescence in a Random Background
type: journal_article
volume: 14
year: '2004'
...
---
_id: '4372'
alternative_title:
- LNCS
author:
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Dejan Nickovic
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: 'Maler O, Nickovic D. Monitoring Temporal Properties of Continuous Signals.
In: Springer; 2004:152-166. doi:1572'
apa: 'Maler, O., & Nickovic, D. (2004). Monitoring Temporal Properties of Continuous
Signals (pp. 152–166). Presented at the FORMATS: Formal Modeling and Analysis
of Timed Systems, Springer. https://doi.org/1572'
chicago: Maler, Oded, and Dejan Nickovic. “Monitoring Temporal Properties of Continuous
Signals,” 152–66. Springer, 2004. https://doi.org/1572.
ieee: 'O. Maler and D. Nickovic, “Monitoring Temporal Properties of Continuous Signals,”
presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, 2004,
pp. 152–166.'
ista: 'Maler O, Nickovic D. 2004. Monitoring Temporal Properties of Continuous Signals.
FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, , 152–166.'
mla: Maler, Oded, and Dejan Nickovic. Monitoring Temporal Properties of Continuous
Signals. Springer, 2004, pp. 152–66, doi:1572.
short: O. Maler, D. Nickovic, in:, Springer, 2004, pp. 152–166.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:08:31Z
date_published: 2004-12-14T00:00:00Z
date_updated: 2021-01-12T07:56:29Z
day: '14'
doi: '1572'
extern: 1
month: '12'
page: 152 - 166
publication_status: published
publisher: Springer
publist_id: '1088'
quality_controlled: 0
status: public
title: Monitoring Temporal Properties of Continuous Signals
type: conference
year: '2004'
...
---
_id: '4424'
abstract:
- lang: eng
text: "The enormous cost and ubiquity of software errors necessitates the need for
techniques and tools that can precisely analyze large systems and prove that they
meet given specifications, or if they don't, return counterexample behaviors showing
how the system fails. Recent advances in model checking, decision procedures,
program analysis and type systems, and a shift of focus to partial specifications
common to several systems (e.g., memory safety and race freedom) have resulted
in several practical verification methods. However, these methods are either precise
or they are scalable, depending on whether they track the values of variables
or only a fixed small set of dataflow facts (e.g., types), and are usually insufficient
for precisely verifying large programs.\r\n\r\nWe describe a new technique called
Lazy Abstraction (LA) which achieves both precision and scalability by localizing
the use of precise information. LA automatically builds, explores and refines
a single abstract model of the program in a way that different parts of the model
exhibit different degrees of precision, namely just enough to verify the desired
property. The algorithm automatically mines the information required by partitioning
mechanical proofs of unsatisfiability of spurious counterexamples into Craig Interpolants.
For multithreaded systems, we give a new technique based on analyzing the behavior
of a single thread executing in a context which is an abstraction of the other
(arbitrarily many) threads. We define novel context models and show how to automatically
infer them and analyze the full system (thread + context) using LA.\r\n\r\nLA
is implemented in BLAST. We have run BLAST on Windows and Linux Device Drivers
to verify API conformance properties, and have used it to find (or guarantee the
absence of) data races in multithreaded Networked Embedded Systems (NESC) applications.
BLAST is able to prove the absence of races in several cases where earlier methods,
which depend on lock-based synchronization, fail."
article_processing_charge: No
author:
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
citation:
ama: Jhala R. Program verification by lazy abstraction. 2004:1-165.
apa: Jhala, R. (2004). Program verification by lazy abstraction. University
of California, Berkeley.
chicago: Jhala, Ranjit. “Program Verification by Lazy Abstraction.” University of
California, Berkeley, 2004.
ieee: R. Jhala, “Program verification by lazy abstraction,” University of California,
Berkeley, 2004.
ista: Jhala R. 2004. Program verification by lazy abstraction. University of California,
Berkeley.
mla: Jhala, Ranjit. Program Verification by Lazy Abstraction. University
of California, Berkeley, 2004, pp. 1–165.
short: R. Jhala, Program Verification by Lazy Abstraction, University of California,
Berkeley, 2004.
date_created: 2018-12-11T12:08:47Z
date_published: 2004-12-01T00:00:00Z
date_updated: 2021-01-12T07:56:52Z
day: '01'
extern: '1'
language:
- iso: eng
month: '12'
oa_version: None
page: 1 - 165
publication_status: published
publisher: University of California, Berkeley
publist_id: '307'
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: Program verification by lazy abstraction
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2004'
...
---
_id: '4445'
abstract:
- lang: eng
text: We present a type system for E code, which is an assembly language that manages
the release, interaction, and termination of real-time tasks. E code specifies
a deadline for each task, and the type system ensures that the deadlines are path-insensitive.
We show that typed E programs allow, for given worst-case execution times of tasks,
a simple schedulability analysis. Moreover, the real-time programming language
Giotto can be compiled into typed E~code. This shows that typed E~code identifies
an easily schedulable yet expressive class of real-time programs. We have extended
the Giotto compiler to generate typed E code, and enabled the run-time system
for E code to perform a type and schedulability check before executing the code.
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327
and by the NSF grants CCR- 0208875 and CCR-0225610.
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Christoph
full_name: Kirsch, Christoph M
last_name: Kirsch
citation:
ama: 'Henzinger TA, Kirsch C. A typed assembly language for real-time programs.
In: ACM; 2004:104-113. doi:10.1145/1017753.1017774'
apa: 'Henzinger, T. A., & Kirsch, C. (2004). A typed assembly language for real-time
programs (pp. 104–113). Presented at the EMSOFT: Embedded Software , ACM. https://doi.org/10.1145/1017753.1017774'
chicago: Henzinger, Thomas A, and Christoph Kirsch. “A Typed Assembly Language for
Real-Time Programs,” 104–13. ACM, 2004. https://doi.org/10.1145/1017753.1017774.
ieee: 'T. A. Henzinger and C. Kirsch, “A typed assembly language for real-time programs,”
presented at the EMSOFT: Embedded Software , 2004, pp. 104–113.'
ista: 'Henzinger TA, Kirsch C. 2004. A typed assembly language for real-time programs.
EMSOFT: Embedded Software , 104–113.'
mla: Henzinger, Thomas A., and Christoph Kirsch. A Typed Assembly Language for
Real-Time Programs. ACM, 2004, pp. 104–13, doi:10.1145/1017753.1017774.
short: T.A. Henzinger, C. Kirsch, in:, ACM, 2004, pp. 104–113.
conference:
name: 'EMSOFT: Embedded Software '
date_created: 2018-12-11T12:08:53Z
date_published: 2004-09-01T00:00:00Z
date_updated: 2021-01-12T07:57:01Z
day: '01'
doi: 10.1145/1017753.1017774
extern: 1
month: '09'
page: 104 - 113
publication_status: published
publisher: ACM
publist_id: '285'
quality_controlled: 0
status: public
title: A typed assembly language for real-time programs
type: conference
year: '2004'
...
---
_id: '4458'
abstract:
- lang: eng
text: 'The success of model checking for large programs depends crucially on the
ability to efficiently construct parsimonious abstractions. A predicate abstraction
is parsimonious if at each control location, it specifies only relationships between
current values of variables, and only those which are required for proving correctness.
Previous methods for automatically refining predicate abstractions until sufficient
precision is obtained do not systematically construct parsimonious abstractions:
predicates usually contain symbolic variables, and are added heuristically and
often uniformly to many or all control locations at once. We use Craig interpolation
to efficiently construct, from a given abstract error trace which cannot be concretized,
a parsominous abstraction that removes the trace. At each location of the trace,
we infer the relevant predicates as an interpolant between the two formulas that
define the past and the future segment of the trace. Each interpolant is a relationship
between current values of program variables, and is relevant only at that particular
program location. It can be found by a linear scan of the proof of infeasibility
of the trace.We develop our method for programs with arithmetic and pointer expressions,
and call-by-value function calls. For function calls, Craig interpolation offers
a systematic way of generating relevant predicates that contain only the local
variables of the function and the values of the formal parameters when the function
was called. We have extended our model checker Blast with predicate discovery
by Craig interpolation, and applied it successfully to C programs with more than
130,000 lines of code, which was not possible with approaches that build less
parsimonious abstractions.'
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Kenneth
full_name: McMillan, Kenneth L
last_name: Mcmillan
citation:
ama: 'Henzinger TA, Jhala R, Majumdar R, Mcmillan K. Abstractions from proofs. In:
ACM; 2004:232-244. doi:10.1145/964001.964021'
apa: 'Henzinger, T. A., Jhala, R., Majumdar, R., & Mcmillan, K. (2004). Abstractions
from proofs (pp. 232–244). Presented at the POPL: Principles of Programming Languages,
ACM. https://doi.org/10.1145/964001.964021'
chicago: Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Kenneth Mcmillan.
“Abstractions from Proofs,” 232–44. ACM, 2004. https://doi.org/10.1145/964001.964021.
ieee: 'T. A. Henzinger, R. Jhala, R. Majumdar, and K. Mcmillan, “Abstractions from
proofs,” presented at the POPL: Principles of Programming Languages, 2004, pp.
232–244.'
ista: 'Henzinger TA, Jhala R, Majumdar R, Mcmillan K. 2004. Abstractions from proofs.
POPL: Principles of Programming Languages, 232–244.'
mla: Henzinger, Thomas A., et al. Abstractions from Proofs. ACM, 2004, pp.
232–44, doi:10.1145/964001.964021.
short: T.A. Henzinger, R. Jhala, R. Majumdar, K. Mcmillan, in:, ACM, 2004, pp. 232–244.
conference:
name: 'POPL: Principles of Programming Languages'
date_created: 2018-12-11T12:08:57Z
date_published: 2004-04-01T00:00:00Z
date_updated: 2021-01-12T07:57:06Z
day: '01'
doi: 10.1145/964001.964021
extern: 1
month: '04'
page: 232 - 244
publication_status: published
publisher: ACM
publist_id: '270'
quality_controlled: 0
status: public
title: Abstractions from proofs
type: conference
year: '2004'
...
---
_id: '4459'
abstract:
- lang: eng
text: Software model checking has been successful for sequential programs, where
predicate abstraction offers suitable models, and counterexample-guided abstraction
refinement permits the automatic inference of models. When checking concurrent
programs, we need to abstract threads as well as the contexts in which they execute.
Stateless context models, such as predicates on global variables, prove insufficient
for showing the absence of race conditions in many examples. We therefore use
richer context models, which combine (1) predicates for abstracting data state,
(2) control flow quotients for abstracting control state, and (3) counters for
abstracting an unbounded number of threads. We infer suitable context models automatically
by a combination of counterexample-guided abstraction refinement, bisimulation
minimization, circular assume-guarantee reasoning, and parametric reasoning about
an unbounded number of threads. This algorithm, called CIRC, has been implemented
in BLAST and succeeds in checking many examples of NESC code for data races. In
particular, BLAST proves the absence of races in several cases where previous
race checkers give false positives.
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: 'Henzinger TA, Jhala R, Majumdar R. Race checking by context inference. In:
ACM; 2004:1-13. doi:10.1145/996841.996844'
apa: 'Henzinger, T. A., Jhala, R., & Majumdar, R. (2004). Race checking by context
inference (pp. 1–13). Presented at the PLDI: Programming Languages Design and
Implementation, ACM. https://doi.org/10.1145/996841.996844'
chicago: Henzinger, Thomas A, Ranjit Jhala, and Ritankar Majumdar. “Race Checking
by Context Inference,” 1–13. ACM, 2004. https://doi.org/10.1145/996841.996844.
ieee: 'T. A. Henzinger, R. Jhala, and R. Majumdar, “Race checking by context inference,”
presented at the PLDI: Programming Languages Design and Implementation, 2004,
pp. 1–13.'
ista: 'Henzinger TA, Jhala R, Majumdar R. 2004. Race checking by context inference.
PLDI: Programming Languages Design and Implementation, 1–13.'
mla: Henzinger, Thomas A., et al. Race Checking by Context Inference. ACM,
2004, pp. 1–13, doi:10.1145/996841.996844.
short: T.A. Henzinger, R. Jhala, R. Majumdar, in:, ACM, 2004, pp. 1–13.
conference:
name: 'PLDI: Programming Languages Design and Implementation'
date_created: 2018-12-11T12:08:57Z
date_published: 2004-06-01T00:00:00Z
date_updated: 2021-01-12T07:57:07Z
day: '01'
doi: 10.1145/996841.996844
extern: 1
month: '06'
page: 1 - 13
publication_status: published
publisher: ACM
publist_id: '271'
quality_controlled: 0
status: public
title: Race checking by context inference
type: conference
year: '2004'
...
---
_id: '4461'
abstract:
- lang: eng
text: One of the central axioms of extreme programming is the disciplined use of
regression testing during stepwise software development. Due to recent progress
in software model checking, it has become possible to supplement this process
with automatic checks for behavioral safety properties of programs, such as conformance
with locking idioms and other programming protocols and patterns. For efficiency
reasons, all checks must be incremental, i.e., they must reuse partial results
from previous checks in order to avoid all unnecessary repetition of expensive
verification tasks. We show that the lazy-abstraction algorithm, and its implementation
in Blast, can be extended to support the fully automatic and incremental checking
of temporal safety properties during software development.
acknowledgement: 'This work was supported in part by the NSF grants CCR-9988172, CCR-0085949,
and CCR-0234690, the ONR grant N00014-02-1-0671, the DARPA grant F33615-00-C-1693,
and the MARCO grant 98-DT-660. '
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Marco
full_name: Sanvido, Marco A
last_name: Sanvido
citation:
ama: 'Henzinger TA, Jhala R, Majumdar R, Sanvido M. Extreme model checking. In:
Verification: Theory and Practice. Vol 2772. Springer; 2004:332-358. doi:10.1007/978-3-540-39910-0_16'
apa: 'Henzinger, T. A., Jhala, R., Majumdar, R., & Sanvido, M. (2004). Extreme
model checking. In Verification: Theory and Practice (Vol. 2772, pp. 332–358).
Springer. https://doi.org/10.1007/978-3-540-39910-0_16'
chicago: 'Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Marco Sanvido.
“Extreme Model Checking.” In Verification: Theory and Practice, 2772:332–58.
Springer, 2004. https://doi.org/10.1007/978-3-540-39910-0_16.'
ieee: 'T. A. Henzinger, R. Jhala, R. Majumdar, and M. Sanvido, “Extreme model checking,”
in Verification: Theory and Practice, vol. 2772, Springer, 2004, pp. 332–358.'
ista: 'Henzinger TA, Jhala R, Majumdar R, Sanvido M. 2004.Extreme model checking.
In: Verification: Theory and Practice. LNCS, vol. 2772, 332–358.'
mla: 'Henzinger, Thomas A., et al. “Extreme Model Checking.” Verification: Theory
and Practice, vol. 2772, Springer, 2004, pp. 332–58, doi:10.1007/978-3-540-39910-0_16.'
short: 'T.A. Henzinger, R. Jhala, R. Majumdar, M. Sanvido, in:, Verification: Theory
and Practice, Springer, 2004, pp. 332–358.'
date_created: 2018-12-11T12:08:58Z
date_published: 2004-02-24T00:00:00Z
date_updated: 2021-01-12T07:57:08Z
day: '24'
doi: 10.1007/978-3-540-39910-0_16
extern: 1
intvolume: ' 2772'
month: '02'
page: 332 - 358
publication: 'Verification: Theory and Practice'
publication_status: published
publisher: Springer
publist_id: '269'
quality_controlled: 0
status: public
title: Extreme model checking
type: book_chapter
volume: 2772
year: '2004'
...
---
_id: '4525'
abstract:
- lang: eng
text: 'We present a new high-level programming language, called xGiotto, for programming
applications with hard real-time constraints. Like its predecessor, xGiotto is
based on the LET (logical execution time) assumption: the programmer specifies
when the outputs of a task become available, and the compiler checks if the specification
can be implemented on a given platform. However, while the predecessor language
xGiotto was purely time-triggered, xGiotto accommodates also asynchronous events.
Indeed, through a mechanism called event scoping, events are the main structuring
principle of the new language. The xGiotto compiler and run-time system implement
event scoping through a tree-based event filter. The compiler also checks programs
for determinism (absence of race conditions).'
acknowledgement: This research is supported by the AFOSR MURI grant F49620-00-1-0327,
the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, and the NSF
grants CCR-0208875 and CCR-0225610.
alternative_title:
- LNCS
author:
- first_name: Arkadeb
full_name: Ghosal, Arkadeb
last_name: Ghosal
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Christoph
full_name: Kirsch, Christoph M
last_name: Kirsch
- first_name: Marco
full_name: Sanvido, Marco A
last_name: Sanvido
citation:
ama: 'Ghosal A, Henzinger TA, Kirsch C, Sanvido M. Event-driven programming with
logical execution times. In: Vol 2993. Springer; 2004:167-170. doi:10.1007/978-3-540-24743-2_24'
apa: 'Ghosal, A., Henzinger, T. A., Kirsch, C., & Sanvido, M. (2004). Event-driven
programming with logical execution times (Vol. 2993, pp. 167–170). Presented at
the HSCC: Hybrid Systems - Computation and Control, Springer. https://doi.org/10.1007/978-3-540-24743-2_24'
chicago: Ghosal, Arkadeb, Thomas A Henzinger, Christoph Kirsch, and Marco Sanvido.
“Event-Driven Programming with Logical Execution Times,” 2993:167–70. Springer,
2004. https://doi.org/10.1007/978-3-540-24743-2_24.
ieee: 'A. Ghosal, T. A. Henzinger, C. Kirsch, and M. Sanvido, “Event-driven programming
with logical execution times,” presented at the HSCC: Hybrid Systems - Computation
and Control, 2004, vol. 2993, pp. 167–170.'
ista: 'Ghosal A, Henzinger TA, Kirsch C, Sanvido M. 2004. Event-driven programming
with logical execution times. HSCC: Hybrid Systems - Computation and Control,
LNCS, vol. 2993, 167–170.'
mla: Ghosal, Arkadeb, et al. Event-Driven Programming with Logical Execution
Times. Vol. 2993, Springer, 2004, pp. 167–70, doi:10.1007/978-3-540-24743-2_24.
short: A. Ghosal, T.A. Henzinger, C. Kirsch, M. Sanvido, in:, Springer, 2004, pp.
167–170.
conference:
name: 'HSCC: Hybrid Systems - Computation and Control'
date_created: 2018-12-11T12:09:18Z
date_published: 2004-03-12T00:00:00Z
date_updated: 2021-01-12T07:59:26Z
day: '12'
doi: 10.1007/978-3-540-24743-2_24
extern: 1
intvolume: ' 2993'
month: '03'
page: 167 - 170
publication_status: published
publisher: Springer
publist_id: '200'
quality_controlled: 0
status: public
title: Event-driven programming with logical execution times
type: conference
volume: 2993
year: '2004'
...
---
_id: '4555'
abstract:
- lang: eng
text: Strategies in repeated games can be classified as to whether or not they use
memory and/or randomization. We consider Markov decision processes and 2-player
graph games, both of the deterministic and probabilistic varieties. We characterize
when memory and/or randomization are required for winning with respect to various
classes of w-regular objectives, noting particularly when the use of memory can
be traded for the use of randomization. In particular, we show that Markov decision
processes allow randomized memoryless optimal strategies for all M?ller objectives.
Furthermore, we show that 2-player probabilistic graph games allow randomized
memoryless strategies for winning with probability 1 those M?ller objectives which
are upward-closed. Upward-closure means that if a set α of infinitely repeating
vertices is winning, then all supersets of α are also winning.
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Luca
full_name: de Alfaro, Luca
last_name: De Alfaro
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, De Alfaro L, Henzinger TA. Trading memory for randomness. In:
IEEE; 2004:206-217. doi:10.1109/QEST.2004.10051'
apa: 'Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2004). Trading memory
for randomness (pp. 206–217). Presented at the QEST: Quantitative Evaluation of
Systems, IEEE. https://doi.org/10.1109/QEST.2004.10051'
chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Trading
Memory for Randomness,” 206–17. IEEE, 2004. https://doi.org/10.1109/QEST.2004.10051.
ieee: 'K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Trading memory for randomness,”
presented at the QEST: Quantitative Evaluation of Systems, 2004, pp. 206–217.'
ista: 'Chatterjee K, De Alfaro L, Henzinger TA. 2004. Trading memory for randomness.
QEST: Quantitative Evaluation of Systems, 206–217.'
mla: Chatterjee, Krishnendu, et al. Trading Memory for Randomness. IEEE,
2004, pp. 206–17, doi:10.1109/QEST.2004.10051.
short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, IEEE, 2004, pp. 206–217.
conference:
name: 'QEST: Quantitative Evaluation of Systems'
date_created: 2018-12-11T12:09:27Z
date_published: 2004-09-30T00:00:00Z
date_updated: 2021-01-12T07:59:40Z
day: '30'
doi: 10.1109/QEST.2004.10051
extern: 1
month: '09'
page: 206 - 217
publication_status: published
publisher: IEEE
publist_id: '155'
quality_controlled: 0
status: public
title: Trading memory for randomness
type: conference
year: '2004'
...
---
_id: '4556'
abstract:
- lang: eng
text: We study the problem of determining stack boundedness and the exact maximum
stack size for three classes of interrupt-driven programs. Interrupt-driven programs
are used in many real-time applications that require responsive interrupt handling.
In order to ensure responsiveness, programmers often enable interrupt processing
in the body of lower-priority interrupt handlers. In such programs a programming
error can allow interrupt handlers to be interrupted in a cyclic fashion to lead
to an unbounded stack, causing the system to crash. For a restricted class of
interrupt-driven programs, we show that there is a polynomial-time procedure to
check stack boundedness, while determining the exact maximum stack size is PSPACE-complete.
For a larger class of programs, the two problems are both PSPACE-complete, and
for the largest class of programs we consider, the two problems are PSPACE-hard
and can be solved in exponential time. While the complexities are high, our algorithms
are exponential only in the number of handlers, and polynomial in the size of
the program.
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Di
full_name: Ma, Di
last_name: Ma
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Tian
full_name: Zhao, Tian
last_name: Zhao
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jens
full_name: Palsberg, Jens
last_name: Palsberg
citation:
ama: Chatterjee K, Ma D, Majumdar R, Zhao T, Henzinger TA, Palsberg J. Stack size
analysis for interrupt-driven programs. Information and Computation. 2004;194(2):144-174.
doi:10.1016/j.ic.2004.06.001
apa: Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T. A., & Palsberg,
J. (2004). Stack size analysis for interrupt-driven programs. Information and
Computation. Elsevier. https://doi.org/10.1016/j.ic.2004.06.001
chicago: Chatterjee, Krishnendu, Di Ma, Ritankar Majumdar, Tian Zhao, Thomas A Henzinger,
and Jens Palsberg. “Stack Size Analysis for Interrupt-Driven Programs.” Information
and Computation. Elsevier, 2004. https://doi.org/10.1016/j.ic.2004.06.001.
ieee: K. Chatterjee, D. Ma, R. Majumdar, T. Zhao, T. A. Henzinger, and J. Palsberg,
“Stack size analysis for interrupt-driven programs,” Information and Computation,
vol. 194, no. 2. Elsevier, pp. 144–174, 2004.
ista: Chatterjee K, Ma D, Majumdar R, Zhao T, Henzinger TA, Palsberg J. 2004. Stack
size analysis for interrupt-driven programs. Information and Computation. 194(2),
144–174.
mla: Chatterjee, Krishnendu, et al. “Stack Size Analysis for Interrupt-Driven Programs.”
Information and Computation, vol. 194, no. 2, Elsevier, 2004, pp. 144–74,
doi:10.1016/j.ic.2004.06.001.
short: K. Chatterjee, D. Ma, R. Majumdar, T. Zhao, T.A. Henzinger, J. Palsberg,
Information and Computation 194 (2004) 144–174.
date_created: 2018-12-11T12:09:28Z
date_published: 2004-08-11T00:00:00Z
date_updated: 2021-01-12T07:59:40Z
day: '11'
doi: 10.1016/j.ic.2004.06.001
extern: 1
intvolume: ' 194'
issue: '2'
month: '08'
page: 144 - 174
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '156'
quality_controlled: 0
status: public
title: Stack size analysis for interrupt-driven programs
type: journal_article
volume: 194
year: '2004'
...
---
_id: '4558'
abstract:
- lang: eng
text: We study perfect-information stochastic parity games. These are two-player
nonterminating games which are played on a graph with turn-based probabilistic
transitions. A play results in an infinite path and the conflicting goals of the
two players are ω-regular path properties, formalized as parity winning conditions.
The qualitative solution of such a game amounts to computing the set of vertices
from which a player has a strategy to win with probability 1 (or with positive
probability). The quantitative solution amounts to computing the value of the
game in every vertex, i.e., the highest probability with which a player can guarantee
satisfaction of his own objective in a play that starts from the vertex.For the
important special case of one-player stochastic parity games (parity Markov decision
processes) we give polynomial-time algorithms both for the qualitative and the
quantitative solution. The running time of the qualitative solution is O(d · m3/2)
for graphs with m edges and d priorities. The quantitative solution is based on
a linear-programming formulation.For the two-player case, we establish the existence
of optimal pure memoryless strategies. This has several important ramifications.
First, it implies that the values of the games are rational. This is in contrast
to the concurrent stochastic parity games of de Alfaro et al.; there, values are
in general algebraic numbers, optimal strategies do not exist, and ε-optimal strategies
have to be mixed and with infinite memory. Second, the existence of optimal pure
memoryless strategies together with the polynomial-time solution forone-player
case implies that the quantitative two-player stochastic parity game problem is
in NP ∩ co-NP. This generalizes a result of Condon for stochastic games with reachability
objectives. It also constitutes an exponential improvement over the best previous
algorithm, which is based on a doubly exponential procedure of de Alfaro and Majumdar
for concurrent stochastic parity games and provides only ε-approximations of the
values.
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Marcin
full_name: Jurdziński, Marcin
last_name: Jurdziński
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Jurdziński M, Henzinger TA. Quantitative stochastic parity games.
In: SIAM; 2004:121-130.'
apa: 'Chatterjee, K., Jurdziński, M., & Henzinger, T. A. (2004). Quantitative
stochastic parity games (pp. 121–130). Presented at the SODA: Symposium on Discrete
Algorithms, SIAM.'
chicago: Chatterjee, Krishnendu, Marcin Jurdziński, and Thomas A Henzinger. “Quantitative
Stochastic Parity Games,” 121–30. SIAM, 2004.
ieee: 'K. Chatterjee, M. Jurdziński, and T. A. Henzinger, “Quantitative stochastic
parity games,” presented at the SODA: Symposium on Discrete Algorithms, 2004,
pp. 121–130.'
ista: 'Chatterjee K, Jurdziński M, Henzinger TA. 2004. Quantitative stochastic parity
games. SODA: Symposium on Discrete Algorithms, 121–130.'
mla: Chatterjee, Krishnendu, et al. Quantitative Stochastic Parity Games.
SIAM, 2004, pp. 121–30.
short: K. Chatterjee, M. Jurdziński, T.A. Henzinger, in:, SIAM, 2004, pp. 121–130.
conference:
name: 'SODA: Symposium on Discrete Algorithms'
date_created: 2018-12-11T12:09:28Z
date_published: 2004-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:41Z
day: '01'
extern: 1
month: '01'
page: 121 - 130
publication_status: published
publisher: SIAM
publist_id: '153'
quality_controlled: 0
status: public
title: Quantitative stochastic parity games
type: conference
year: '2004'
...
---
_id: '2623'
abstract:
- lang: eng
text: Patients with Hodgkin's disease can develop paraneoplastic cerebellar ataxia
because of the generation of autoantibodies against mGluR1 (mGluR1-Abs). Yet,
the pathophysiological mechanisms underlying their motor coordination deficits
remain to be elucidated. Here, we show that application of IgG purified from the
patients' serum to cerebellar slices of mice acutely reduces the basal activity
of Purkinje cells, whereas application to the flocculus of mice in vivo evokes
acute disturbances in the performance of their compensatory eye movements. In
addition, the mGluR1-Abs block induction of long-term depression in cultured mouse
Purkinje cells, whereas the cerebellar motor learning behavior of the patients
is affected in that they show impaired adaptation of their saccadic eye movements.
Finally, postmortem analysis of the cerebellum of a paraneoplastic cerebellar
ataxia patient showed that the number of Purkinje cells was significantly reduced
by approximately two thirds compared with three controls. We conclude that autoantibodies
against mGluR1 can cause cerebellar motor coordination deficits caused by a combination
of rapid effects on both acute and plastic responses of Purkinje cells and chronic
degenerative effects.
author:
- first_name: Michiel
full_name: Coesmans, Michiel P
last_name: Coesmans
- first_name: Peter
full_name: Sillevis-Smitt, Peter A
last_name: Sillevis Smitt
- first_name: David
full_name: Linden, David J
last_name: Linden
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Tomoo
full_name: Hirano, Tomoo
last_name: Hirano
- first_name: Yoshinori
full_name: Yamakawa, Yoshinori
last_name: Yamakawa
- first_name: Adriaan
full_name: Van Alphen, Adriaan M
last_name: Van Alphen
- first_name: Chongde
full_name: Luo, Chongde
last_name: Luo
- first_name: Jos
full_name: Van Der Geest, Jos N
last_name: Van Der Geest
- first_name: Johan
full_name: Kros, Johan M
last_name: Kros
- first_name: Carlo
full_name: Gaillard, Carlo A
last_name: Gaillard
- first_name: Maarten
full_name: Frens, Maarten A
last_name: Frens
- first_name: Chris
full_name: De Zeeuw, Chris I
last_name: De Zeeuw
citation:
ama: Coesmans M, Sillevis Smitt P, Linden D, et al. Mechanisms underlying cerebellar
motor deficits due to mGluR1-autoantibodies. Annals of Neurology. 2003;53(3):325-336.
doi:10.1002/ana.10451
apa: Coesmans, M., Sillevis Smitt, P., Linden, D., Shigemoto, R., Hirano, T., Yamakawa,
Y., … De Zeeuw, C. (2003). Mechanisms underlying cerebellar motor deficits due
to mGluR1-autoantibodies. Annals of Neurology. Wiley-Blackwell. https://doi.org/10.1002/ana.10451
chicago: Coesmans, Michiel, Peter Sillevis Smitt, David Linden, Ryuichi Shigemoto,
Tomoo Hirano, Yoshinori Yamakawa, Adriaan Van Alphen, et al. “Mechanisms Underlying
Cerebellar Motor Deficits Due to MGluR1-Autoantibodies.” Annals of Neurology.
Wiley-Blackwell, 2003. https://doi.org/10.1002/ana.10451.
ieee: M. Coesmans et al., “Mechanisms underlying cerebellar motor deficits
due to mGluR1-autoantibodies,” Annals of Neurology, vol. 53, no. 3. Wiley-Blackwell,
pp. 325–336, 2003.
ista: Coesmans M, Sillevis Smitt P, Linden D, Shigemoto R, Hirano T, Yamakawa Y,
Van Alphen A, Luo C, Van Der Geest J, Kros J, Gaillard C, Frens M, De Zeeuw C.
2003. Mechanisms underlying cerebellar motor deficits due to mGluR1-autoantibodies.
Annals of Neurology. 53(3), 325–336.
mla: Coesmans, Michiel, et al. “Mechanisms Underlying Cerebellar Motor Deficits
Due to MGluR1-Autoantibodies.” Annals of Neurology, vol. 53, no. 3, Wiley-Blackwell,
2003, pp. 325–36, doi:10.1002/ana.10451.
short: M. Coesmans, P. Sillevis Smitt, D. Linden, R. Shigemoto, T. Hirano, Y. Yamakawa,
A. Van Alphen, C. Luo, J. Van Der Geest, J. Kros, C. Gaillard, M. Frens, C. De
Zeeuw, Annals of Neurology 53 (2003) 325–336.
date_created: 2018-12-11T11:58:44Z
date_published: 2003-03-01T00:00:00Z
date_updated: 2021-01-12T06:58:39Z
day: '01'
doi: 10.1002/ana.10451
extern: 1
intvolume: ' 53'
issue: '3'
month: '03'
page: 325 - 336
publication: Annals of Neurology
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4274'
quality_controlled: 0
status: public
title: Mechanisms underlying cerebellar motor deficits due to mGluR1-autoantibodies
type: journal_article
volume: 53
year: '2003'
...
---
_id: '2625'
abstract:
- lang: eng
text: Metabotropic glutamate receptor 1 (mGluR1) plays a crucial role in synaptic
plasticity and motor learning in the cerebellum. We have studied activity-dependent
changes in mGluR1 function in mouse cultured Purkinje neurons. Depolarizing stimulation
potentiated Ca2+ and current responses to an mGluR1 agonist for several hours
in the cultured Purkinje neurons. It also blocked internalization of mGluR1 and
increased the number of mGluR1s on the cell membrane. We found that depolarization
simultaneously increased transcription of Homer1a in Purkinje neurons. Homer1a
inhibited internalization and increased cell-surface expression of mGluR1 when
coexpressed in human embryonic kidney (HEK)-293 cells. Depolarization-induced
Homer1a expression in Purkinje neurons was blocked by a mitogen-activated protein
kinase (MAPK) inhibitor. Changes in internalization and mGluR1-mediated Ca2+ response
were also blocked by inhibition of MAPK activity, suggesting that localization
and activity of mGluR1 were regulated in the same signalling pathway as Homer1a
expression. It is thus suggested that depolarization of the Purkinje neuron leads
to the increment in mGluR1 responsiveness through MAPK activity and induction
of Homer1a expression, which increases active mGluR1 on the cell surface by blocking
internalization of mGluR1.
author:
- first_name: Itsunari
full_name: Minami, Itsunari
last_name: Minami
- first_name: Mineko
full_name: Kengaku, Mineko
last_name: Kengaku
- first_name: Sillevis
full_name: Smitt, Sillevis P
last_name: Smitt
- first_name: Ryuichi
full_name: Ryuichi Shigemoto
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Tomoo
full_name: Hirano, Tomoo
last_name: Hirano
citation:
ama: Minami I, Kengaku M, Smitt S, Shigemoto R, Hirano T. Long-term potentiation
of mGluR1 activity by depolarization-induced Homer1a in mouse cerebellar Purkinje
neurons. European Journal of Neuroscience. 2003;17(5):1023-1032. doi:10.1046/j.1460-9568.2003.02499.x
apa: Minami, I., Kengaku, M., Smitt, S., Shigemoto, R., & Hirano, T. (2003).
Long-term potentiation of mGluR1 activity by depolarization-induced Homer1a in
mouse cerebellar Purkinje neurons. European Journal of Neuroscience. Wiley-Blackwell.
https://doi.org/10.1046/j.1460-9568.2003.02499.x
chicago: Minami, Itsunari, Mineko Kengaku, Sillevis Smitt, Ryuichi Shigemoto, and
Tomoo Hirano. “Long-Term Potentiation of MGluR1 Activity by Depolarization-Induced
Homer1a in Mouse Cerebellar Purkinje Neurons.” European Journal of Neuroscience.
Wiley-Blackwell, 2003. https://doi.org/10.1046/j.1460-9568.2003.02499.x.
ieee: I. Minami, M. Kengaku, S. Smitt, R. Shigemoto, and T. Hirano, “Long-term potentiation
of mGluR1 activity by depolarization-induced Homer1a in mouse cerebellar Purkinje
neurons,” European Journal of Neuroscience, vol. 17, no. 5. Wiley-Blackwell,
pp. 1023–1032, 2003.
ista: Minami I, Kengaku M, Smitt S, Shigemoto R, Hirano T. 2003. Long-term potentiation
of mGluR1 activity by depolarization-induced Homer1a in mouse cerebellar Purkinje
neurons. European Journal of Neuroscience. 17(5), 1023–1032.
mla: Minami, Itsunari, et al. “Long-Term Potentiation of MGluR1 Activity by Depolarization-Induced
Homer1a in Mouse Cerebellar Purkinje Neurons.” European Journal of Neuroscience,
vol. 17, no. 5, Wiley-Blackwell, 2003, pp. 1023–32, doi:10.1046/j.1460-9568.2003.02499.x.
short: I. Minami, M. Kengaku, S. Smitt, R. Shigemoto, T. Hirano, European Journal
of Neuroscience 17 (2003) 1023–1032.
date_created: 2018-12-11T11:58:44Z
date_published: 2003-03-01T00:00:00Z
date_updated: 2021-01-12T06:58:39Z
day: '01'
doi: 10.1046/j.1460-9568.2003.02499.x
extern: 1
intvolume: ' 17'
issue: '5'
month: '03'
page: 1023 - 1032
publication: European Journal of Neuroscience
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4273'
quality_controlled: 0
status: public
title: Long-term potentiation of mGluR1 activity by depolarization-induced Homer1a
in mouse cerebellar Purkinje neurons
type: journal_article
volume: 17
year: '2003'
...