---
_id: '4193'
abstract:
- lang: eng
text: The controlled adhesion of cells to each other and to the extracellular matrix
is crucial for tissue development and maintenance. Numerous assays have been developed
to quantify cell adhesion. Among these, the use of atomic force microscopy (AFM)
for single-cell force spectroscopy (SCFS) has recently been established. This
assay permits the adhesion of living cells to be studied in near-physiological
conditions. This implementation of AFM allows unrivaled spatial and temporal control
of cells, as well as highly quantitative force actuation and force measurement
that is sufficiently sensitive to characterize the interaction of single molecules.
Therefore, not only overall cell adhesion but also the properties of single adhesion-receptor-ligand
interactions can be studied. Here we describe current implementations and applications
of SCFS, as well as potential pitfalls, and outline how developments will provide
insight into the forces, energetics and kinetics of cell-adhesion processes.
article_processing_charge: No
author:
- first_name: Jonne
full_name: Helenius, Jonne
last_name: Helenius
- 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
- first_name: Hermann
full_name: Gaub, Hermann
last_name: Gaub
- first_name: Daniel
full_name: Mueller, Daniel
last_name: Mueller
citation:
ama: Helenius J, Heisenberg C-PJ, Gaub H, Mueller D. Single-cell force spectroscopy.
Journal of Cell Science. 2008;121(11):1785-1791. doi:10.1242/jcs.030999
apa: Helenius, J., Heisenberg, C.-P. J., Gaub, H., & Mueller, D. (2008). Single-cell
force spectroscopy. Journal of Cell Science. Company of Biologists. https://doi.org/10.1242/jcs.030999
chicago: Helenius, Jonne, Carl-Philipp J Heisenberg, Hermann Gaub, and Daniel Mueller.
“Single-Cell Force Spectroscopy.” Journal of Cell Science. Company of Biologists,
2008. https://doi.org/10.1242/jcs.030999.
ieee: J. Helenius, C.-P. J. Heisenberg, H. Gaub, and D. Mueller, “Single-cell force
spectroscopy,” Journal of Cell Science, vol. 121, no. 11. Company of Biologists,
pp. 1785–1791, 2008.
ista: Helenius J, Heisenberg C-PJ, Gaub H, Mueller D. 2008. Single-cell force spectroscopy.
Journal of Cell Science. 121(11), 1785–1791.
mla: Helenius, Jonne, et al. “Single-Cell Force Spectroscopy.” Journal of Cell
Science, vol. 121, no. 11, Company of Biologists, 2008, pp. 1785–91, doi:10.1242/jcs.030999.
short: J. Helenius, C.-P.J. Heisenberg, H. Gaub, D. Mueller, Journal of Cell Science
121 (2008) 1785–1791.
date_created: 2018-12-11T12:07:30Z
date_published: 2008-06-01T00:00:00Z
date_updated: 2021-01-12T07:55:12Z
day: '01'
doi: 10.1242/jcs.030999
extern: '1'
intvolume: ' 121'
issue: '11'
language:
- iso: eng
month: '06'
oa_version: None
page: 1785 - 1791
publication: Journal of Cell Science
publication_status: published
publisher: Company of Biologists
publist_id: '1924'
status: public
title: Single-cell force spectroscopy
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 121
year: '2008'
...
---
_id: '4198'
abstract:
- lang: eng
text: Animal body plan arises during gastrulation and organogenesis by the coordination
of inductive events and cell movements. Several signaling pathways, such as BMP,
FGF, Hedgehog, Nodal, and Wnt have well-recognized instructive roles in cell fate
specification during vertebrate embryogenesis. Growing evidence indicates that
BMP, Nodal, and FGF signaling also regulate cell movements, and that they do so
through mechanisms distinct from those that specify cell fates. Moreover, pathways
controlling cell movements can also indirectly influence cell fate specification
by regulating dimensions and relative positions of interacting tissues. The current
challenge is to delineate the molecular mechanisms via which the major signaling
pathways regulate cell fate specification and movements, and how these two processes
are coordinated to ensure normal development.
article_processing_charge: No
author:
- 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
- first_name: Lilianna
full_name: Solnica Krezel, Lilianna
last_name: Solnica Krezel
citation:
ama: Heisenberg C-PJ, Solnica Krezel L. Back and forth between cell fate specification
and movement during vertebrate gastrulation. Current Opinion in Genetics &
Development. 2008;18(4):311-316. doi:10.1016/j.gde.2008.07.011
apa: Heisenberg, C.-P. J., & Solnica Krezel, L. (2008). Back and forth between
cell fate specification and movement during vertebrate gastrulation. Current
Opinion in Genetics & Development. Elsevier. https://doi.org/10.1016/j.gde.2008.07.011
chicago: Heisenberg, Carl-Philipp J, and Lilianna Solnica Krezel. “Back and Forth
between Cell Fate Specification and Movement during Vertebrate Gastrulation.”
Current Opinion in Genetics & Development. Elsevier, 2008. https://doi.org/10.1016/j.gde.2008.07.011.
ieee: C.-P. J. Heisenberg and L. Solnica Krezel, “Back and forth between cell fate
specification and movement during vertebrate gastrulation,” Current Opinion
in Genetics & Development, vol. 18, no. 4. Elsevier, pp. 311–316, 2008.
ista: Heisenberg C-PJ, Solnica Krezel L. 2008. Back and forth between cell fate
specification and movement during vertebrate gastrulation. Current Opinion in
Genetics & Development. 18(4), 311–316.
mla: Heisenberg, Carl-Philipp J., and Lilianna Solnica Krezel. “Back and Forth between
Cell Fate Specification and Movement during Vertebrate Gastrulation.” Current
Opinion in Genetics & Development, vol. 18, no. 4, Elsevier, 2008, pp.
311–16, doi:10.1016/j.gde.2008.07.011.
short: C.-P.J. Heisenberg, L. Solnica Krezel, Current Opinion in Genetics &
Development 18 (2008) 311–316.
date_created: 2018-12-11T12:07:32Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2021-01-12T07:55:14Z
day: '01'
doi: 10.1016/j.gde.2008.07.011
extern: '1'
intvolume: ' 18'
issue: '4'
language:
- iso: eng
month: '01'
oa_version: None
page: 311 - 316
publication: Current Opinion in Genetics & Development
publication_status: published
publisher: Elsevier
publist_id: '1918'
status: public
title: Back and forth between cell fate specification and movement during vertebrate
gastrulation
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2008'
...
---
_id: '4227'
abstract:
- lang: eng
text: 'Morphogen concentration gradients provide positional information by activating
target genes in a concentration-dependent manner. Recent reports show that the
gradient of the syncytial morphogen Bicoid seems to provide precise positional
information to determine target gene domains. For secreted morphogenetic ligands,
the precision of the gradients, the signal transduction and the reliability of
target gene expression domains have not been studied. Here we investigate these
issues for the TGF-beta-type morphogen Dpp. We first studied theoretically how
cell-to-cell variability in the source, the target tissue, or both, contribute
to the variations of the gradient. Fluctuations in the source and target generate
a local maximum of precision at a finite distance to the source. We then determined
experimentally in the wing epithelium: (1) the precision of the Dpp concentration
gradient; (2) the precision of the Dpp signaling activity profile; and (3) the
precision of activation of the Dpp target gene spalt. As captured by our theoretical
description, the Dpp gradient provides positional information with a maximal precision
a few cells away from the source. This maximal precision corresponds to a positional
uncertainly of about a single cell diameter. The precision of the Dpp gradient
accounts for the precision of the spalt expression range, implying that Dpp can
act as a morphogen to coarsely determine the expression pattern of target genes.'
author:
- first_name: Tobias
full_name: Bollenbach, Tobias
last_name: Bollenbach
- first_name: Periklis
full_name: Pantazis, Periklis
last_name: Pantazis
- first_name: Anna
full_name: Anna Kicheva
id: 3959A2A0-F248-11E8-B48F-1D18A9856A87
last_name: Kicheva
orcid: 0000-0003-4509-4998
- first_name: Christian
full_name: Bokel, Christian
last_name: Bokel
- first_name: Marcos
full_name: González-Gaitán, Marcos
last_name: González Gaitán
- first_name: Frank
full_name: Julicher, Frank
last_name: Julicher
citation:
ama: Bollenbach T, Pantazis P, Kicheva A, Bokel C, González Gaitán M, Julicher F.
Precision of the Dpp gradient. Development. 2008;135(6):1137-1146. doi:10.1242/dev.012062
apa: Bollenbach, T., Pantazis, P., Kicheva, A., Bokel, C., González Gaitán, M.,
& Julicher, F. (2008). Precision of the Dpp gradient. Development.
Company of Biologists. https://doi.org/10.1242/dev.012062
chicago: Bollenbach, Tobias, Periklis Pantazis, Anna Kicheva, Christian Bokel, Marcos
González Gaitán, and Frank Julicher. “Precision of the Dpp Gradient.” Development.
Company of Biologists, 2008. https://doi.org/10.1242/dev.012062.
ieee: T. Bollenbach, P. Pantazis, A. Kicheva, C. Bokel, M. González Gaitán, and
F. Julicher, “Precision of the Dpp gradient,” Development, vol. 135, no.
6. Company of Biologists, pp. 1137–1146, 2008.
ista: Bollenbach T, Pantazis P, Kicheva A, Bokel C, González Gaitán M, Julicher
F. 2008. Precision of the Dpp gradient. Development. 135(6), 1137–1146.
mla: Bollenbach, Tobias, et al. “Precision of the Dpp Gradient.” Development,
vol. 135, no. 6, Company of Biologists, 2008, pp. 1137–46, doi:10.1242/dev.012062.
short: T. Bollenbach, P. Pantazis, A. Kicheva, C. Bokel, M. González Gaitán, F.
Julicher, Development 135 (2008) 1137–1146.
date_created: 2018-12-11T12:07:42Z
date_published: 2008-03-15T00:00:00Z
date_updated: 2021-01-12T07:55:27Z
day: '15'
doi: 10.1242/dev.012062
extern: 1
intvolume: ' 135'
issue: '6'
month: '03'
page: 1137 - 1146
publication: Development
publication_status: published
publisher: Company of Biologists
publist_id: '1889'
quality_controlled: 0
status: public
title: Precision of the Dpp gradient
type: journal_article
volume: 135
year: '2008'
...
---
_id: '4244'
abstract:
- lang: eng
text: This paper presents a new approach to optimization of an energy-constrained
modulation scheme for wireless sensor networks by taking advantage of a novel
bio-inspired optimization algorithm. The algorithm is inspired by Wrightpsilas
shifting balance theory (SBT) of evolution in population genetics. The total energy
consumption of an energy-constrained modulation scheme is minimized by using the
new SBT-based optimization algorithm. The results obtained by this new algorithm
are compared with other popular optimization algorithms. Numerical experiments
are performed to demonstrate that the SBT-based algorithm could be used as an
efficient optimizer for solving the optimization problems arising from currently
emerging energy-efficient wireless sensor networks.
author:
- first_name: Erfu
full_name: Yang, Erfu
last_name: Yang
- first_name: Nicholas H
full_name: Nicholas Barton
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
- first_name: Tughrul
full_name: Arslan, Tughrul
last_name: Arslan
- first_name: Ahmet
full_name: Erdogan, Ahmet T
last_name: Erdogan
citation:
ama: 'Yang E, Barton NH, Arslan T, Erdogan A. A novel shifting balance theory-based
approach to optimization of an energy-constrained modulation scheme for wireless
sensor networks. In: IEEE; 2008:2749-2756. doi:10.1109/CEC.2008.4631167'
apa: 'Yang, E., Barton, N. H., Arslan, T., & Erdogan, A. (2008). A novel shifting
balance theory-based approach to optimization of an energy-constrained modulation
scheme for wireless sensor networks (pp. 2749–2756). Presented at the WCCI: IEEE
World Congress on Computational Intelligence, IEEE. https://doi.org/10.1109/CEC.2008.4631167'
chicago: Yang, Erfu, Nicholas H Barton, Tughrul Arslan, and Ahmet Erdogan. “A Novel
Shifting Balance Theory-Based Approach to Optimization of an Energy-Constrained
Modulation Scheme for Wireless Sensor Networks,” 2749–56. IEEE, 2008. https://doi.org/10.1109/CEC.2008.4631167.
ieee: 'E. Yang, N. H. Barton, T. Arslan, and A. Erdogan, “A novel shifting balance
theory-based approach to optimization of an energy-constrained modulation scheme
for wireless sensor networks,” presented at the WCCI: IEEE World Congress on Computational
Intelligence, 2008, pp. 2749–2756.'
ista: 'Yang E, Barton NH, Arslan T, Erdogan A. 2008. A novel shifting balance theory-based
approach to optimization of an energy-constrained modulation scheme for wireless
sensor networks. WCCI: IEEE World Congress on Computational Intelligence, 2749–2756.'
mla: Yang, Erfu, et al. A Novel Shifting Balance Theory-Based Approach to Optimization
of an Energy-Constrained Modulation Scheme for Wireless Sensor Networks. IEEE,
2008, pp. 2749–56, doi:10.1109/CEC.2008.4631167.
short: E. Yang, N.H. Barton, T. Arslan, A. Erdogan, in:, IEEE, 2008, pp. 2749–2756.
conference:
name: 'WCCI: IEEE World Congress on Computational Intelligence'
date_created: 2018-12-11T12:07:49Z
date_published: 2008-09-23T00:00:00Z
date_updated: 2021-01-12T07:55:34Z
day: '23'
doi: 10.1109/CEC.2008.4631167
extern: 1
month: '09'
page: 2749 - 2756
publication_status: published
publisher: IEEE
publist_id: '1861'
quality_controlled: 0
status: public
title: A novel shifting balance theory-based approach to optimization of an energy-constrained
modulation scheme for wireless sensor networks
type: conference
year: '2008'
...
---
_id: '4245'
abstract:
- lang: eng
text: Sex allocation theory has proved extremely successful at predicting when individuals
should adjust the sex of their offspring in response to environmental conditions.
However, we know rather little about the underlying genetics of sex ratio or how
genetic architecture might constrain adaptive sex-ratio behavior. We examined
how mutation influenced genetic variation in the sex ratios produced by the parasitoid
wasp Nasonia vitripennis. In a mutation accumulation experiment, we determined
the mutability of sex ratio, and compared this with the amount of genetic variation
observed in natural populations. We found that the mutability (h2m) ranges from
0.001 to 0.002, similar to estimates for life-history traits in other organisms.
These estimates suggest one mutation every 5–60 generations, which shift the sex
ratio by approximately 0.01 (proportion males). In this and other studies, the
genetic variation in N. vitripennis sex ratio ranged from 0.02 to 0.17 (broad-sense
heritability, H2). If sex ratio is maintained by mutation–selection balance, a
higher genetic variance would be expected given our mutational parameters. Instead,
the observed genetic variance perhaps suggests additional selection against sex-ratio
mutations with deleterious effects on other fitness traits as well as sex ratio
(i.e., pleiotropy), as has been argued to be the case more generally.
author:
- first_name: Bart
full_name: Pannebakker, Bart A
last_name: Pannebakker
- first_name: Daniel
full_name: Halligan, Daniel
last_name: Halligan
- first_name: K Tracy
full_name: Reynolds, K Tracy
last_name: Reynolds
- first_name: Gavin
full_name: Ballantyne, Gavin A
last_name: Ballantyne
- first_name: David
full_name: Shuker, David M
last_name: Shuker
- first_name: Nicholas H
full_name: Nicholas Barton
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
- first_name: Stuart
full_name: West, Stuart A
last_name: West
citation:
ama: Pannebakker B, Halligan D, Reynolds KT, et al. Effects of spontaneous mutation
accumulation on sex ratio traits. Evolution; International Journal of Organic
Evolution. 2008;62(8):1921-1935. doi:10.1111/j.1558-5646.2008.00434.x
apa: Pannebakker, B., Halligan, D., Reynolds, K. T., Ballantyne, G., Shuker, D.,
Barton, N. H., & West, S. (2008). Effects of spontaneous mutation accumulation
on sex ratio traits. Evolution; International Journal of Organic Evolution.
Wiley-Blackwell. https://doi.org/10.1111/j.1558-5646.2008.00434.x
chicago: Pannebakker, Bart, Daniel Halligan, K Tracy Reynolds, Gavin Ballantyne,
David Shuker, Nicholas H Barton, and Stuart West. “Effects of Spontaneous Mutation
Accumulation on Sex Ratio Traits.” Evolution; International Journal of Organic
Evolution. Wiley-Blackwell, 2008. https://doi.org/10.1111/j.1558-5646.2008.00434.x.
ieee: B. Pannebakker et al., “Effects of spontaneous mutation accumulation
on sex ratio traits,” Evolution; International Journal of Organic Evolution,
vol. 62, no. 8. Wiley-Blackwell, pp. 1921–1935, 2008.
ista: Pannebakker B, Halligan D, Reynolds KT, Ballantyne G, Shuker D, Barton NH,
West S. 2008. Effects of spontaneous mutation accumulation on sex ratio traits.
Evolution; International Journal of Organic Evolution. 62(8), 1921–1935.
mla: Pannebakker, Bart, et al. “Effects of Spontaneous Mutation Accumulation on
Sex Ratio Traits.” Evolution; International Journal of Organic Evolution,
vol. 62, no. 8, Wiley-Blackwell, 2008, pp. 1921–35, doi:10.1111/j.1558-5646.2008.00434.x.
short: B. Pannebakker, D. Halligan, K.T. Reynolds, G. Ballantyne, D. Shuker, N.H.
Barton, S. West, Evolution; International Journal of Organic Evolution 62 (2008)
1921–1935.
date_created: 2018-12-11T12:07:49Z
date_published: 2008-08-01T00:00:00Z
date_updated: 2021-01-12T07:55:34Z
day: '01'
doi: 10.1111/j.1558-5646.2008.00434.x
extern: 1
intvolume: ' 62'
issue: '8'
month: '08'
page: 1921 - 1935
publication: Evolution; International Journal of Organic Evolution
publication_status: published
publisher: Wiley-Blackwell
publist_id: '1860'
quality_controlled: 0
status: public
title: Effects of spontaneous mutation accumulation on sex ratio traits
type: journal_article
volume: 62
year: '2008'
...
---
_id: '4366'
abstract:
- lang: eng
text: Termination of a heap-manipulating program generally depends on preconditions
that express heap assumptions (i.e., assertions describing reachability, aliasing,
separation and sharing in the heap). We present an algorithm for the inference
of such preconditions. The algorithm exploits a unique interplay between counterexample-producing
abstract termination checker and shape analysis. The shape analysis produces heap
assumptions on demand to eliminate counterexamples, i.e., non-terminating abstract
computations. The experiments with our prototype implementation indicate its practical
potential.
alternative_title:
- LNCS
author:
- first_name: Andreas
full_name: Podelski,Andreas
last_name: Podelski
- first_name: Andrey
full_name: Rybalchenko, Andrey
last_name: Rybalchenko
- first_name: Thomas
full_name: Thomas Wies
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
citation:
ama: 'Podelski A, Rybalchenko A, Wies T. Heap Assumptions on Demand. In: Vol 5123.
Springer; 2008:314-327. doi:10.1007/978-3-540-70545-1_31'
apa: 'Podelski, A., Rybalchenko, A., & Wies, T. (2008). Heap Assumptions on
Demand (Vol. 5123, pp. 314–327). Presented at the CAV: Computer Aided Verification,
Springer. https://doi.org/10.1007/978-3-540-70545-1_31'
chicago: Podelski, Andreas, Andrey Rybalchenko, and Thomas Wies. “Heap Assumptions
on Demand,” 5123:314–27. Springer, 2008. https://doi.org/10.1007/978-3-540-70545-1_31.
ieee: 'A. Podelski, A. Rybalchenko, and T. Wies, “Heap Assumptions on Demand,” presented
at the CAV: Computer Aided Verification, 2008, vol. 5123, pp. 314–327.'
ista: 'Podelski A, Rybalchenko A, Wies T. 2008. Heap Assumptions on Demand. CAV:
Computer Aided Verification, LNCS, vol. 5123, 314–327.'
mla: Podelski, Andreas, et al. Heap Assumptions on Demand. Vol. 5123, Springer,
2008, pp. 314–27, doi:10.1007/978-3-540-70545-1_31.
short: A. Podelski, A. Rybalchenko, T. Wies, in:, Springer, 2008, pp. 314–327.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:29Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:26Z
day: '01'
doi: 10.1007/978-3-540-70545-1_31
extern: 1
intvolume: ' 5123'
month: '01'
page: 314 - 327
publication_status: published
publisher: Springer
publist_id: '1091'
quality_controlled: 0
status: public
title: Heap Assumptions on Demand
type: conference
volume: 5123
year: '2008'
...
---
_id: '4371'
abstract:
- lang: eng
text: We survey some of the problems associated with checking whether a given behavior
(a sequence, a Boolean signal or a continuous signal) satisfies a property specified
in an appropriate temporal logic and describe two such monitoring algorithms for
the real-time logic MITL.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Amir
full_name: Pnueli, Amir
last_name: Pnueli
citation:
ama: 'Maler O, Nickovic D, Pnueli A. Checking Temporal Properties of Discrete, Timed
and Continuous Behaviors. In: Pillars of Computer Science: Essays Dedicated
To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday. Springer;
2008:475-505. doi:10.1007/978-3-540-78127-1_26'
apa: 'Maler, O., Nickovic, D., & Pnueli, A. (2008). Checking Temporal Properties
of Discrete, Timed and Continuous Behaviors. In Pillars of Computer science:
Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday
(pp. 475–505). Springer. https://doi.org/10.1007/978-3-540-78127-1_26'
chicago: 'Maler, Oded, Dejan Nickovic, and Amir Pnueli. “Checking Temporal Properties
of Discrete, Timed and Continuous Behaviors.” In Pillars of Computer Science:
Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday,
475–505. Springer, 2008. https://doi.org/10.1007/978-3-540-78127-1_26.'
ieee: 'O. Maler, D. Nickovic, and A. Pnueli, “Checking Temporal Properties of Discrete,
Timed and Continuous Behaviors,” in Pillars of Computer science: Essays Dedicated
To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, Springer,
2008, pp. 475–505.'
ista: 'Maler O, Nickovic D, Pnueli A. 2008.Checking Temporal Properties of Discrete,
Timed and Continuous Behaviors. In: Pillars of Computer science: Essays Dedicated
To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday. LNCS, , 475–505.'
mla: 'Maler, Oded, et al. “Checking Temporal Properties of Discrete, Timed and Continuous
Behaviors.” Pillars of Computer Science: Essays Dedicated To Boris (Boaz) Trakhtenbrot
on the Occasion of His 85th Birthday, Springer, 2008, pp. 475–505, doi:10.1007/978-3-540-78127-1_26.'
short: 'O. Maler, D. Nickovic, A. Pnueli, in:, Pillars of Computer Science: Essays
Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, Springer,
2008, pp. 475–505.'
date_created: 2018-12-11T12:08:30Z
date_published: 2008-03-11T00:00:00Z
date_updated: 2023-02-14T10:42:38Z
day: '11'
doi: 10.1007/978-3-540-78127-1_26
extern: '1'
language:
- iso: eng
month: '03'
oa_version: None
page: 475 - 505
publication: 'Pillars of Computer science: Essays Dedicated To Boris (Boaz) Trakhtenbrot
on the Occasion of His 85th Birthday'
publication_identifier:
isbn:
- '9783540781264'
publication_status: published
publisher: Springer
publist_id: '1087'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Checking Temporal Properties of Discrete, Timed and Continuous Behaviors
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2008'
...
---
_id: '4384'
abstract:
- lang: eng
text: |-
Model checking software transactional memories (STMs) is difficult because of the unbounded number, length, and delay of concurrent transactions and the unbounded size of the memory. We show that, under certain conditions, the verification problem can be reduced to a finite-state problem, and we illustrate the use of the method by proving the correctness of several STMs, including two-phase locking, DSTM, TL2, and optimistic concurrency control. The safety properties we consider include strict serializability and opacity; the liveness properties include obstruction freedom, livelock freedom, and wait freedom.
Our main contribution lies in the structure of the proofs, which are largely automated and not restricted to the STMs mentioned above. In a first step we show that every STM that enjoys certain structural properties either violates a safety or liveness requirement on some program with two threads and two shared variables, or satisfies the requirement on all programs. In the second step we use a model checker to prove the requirement for the STM applied to a most general program with two threads and two variables. In the safety case, the model checker constructs a simulation relation between two carefully constructed finite-state transition systems, one representing the given STM applied to a most general program, and the other representing a most liberal safe STM applied to the same program. In the liveness case, the model checker analyzes fairness conditions on the given STM transition system.
author:
- first_name: Rachid
full_name: Guerraoui, Rachid
last_name: Guerraoui
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Barbara
full_name: Jobstmann, Barbara
last_name: Jobstmann
- first_name: Vasu
full_name: Vasu Singh
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: 'Guerraoui R, Henzinger TA, Jobstmann B, Singh V. Model checking transactional
memories. In: ACM; 2008:372-382. doi:10.1145/1375581.1375626'
apa: 'Guerraoui, R., Henzinger, T. A., Jobstmann, B., & Singh, V. (2008). Model
checking transactional memories (pp. 372–382). Presented at the PLDI: Programming
Languages Design and Implementation, ACM. https://doi.org/10.1145/1375581.1375626'
chicago: Guerraoui, Rachid, Thomas A Henzinger, Barbara Jobstmann, and Vasu Singh.
“Model Checking Transactional Memories,” 372–82. ACM, 2008. https://doi.org/10.1145/1375581.1375626.
ieee: 'R. Guerraoui, T. A. Henzinger, B. Jobstmann, and V. Singh, “Model checking
transactional memories,” presented at the PLDI: Programming Languages Design and
Implementation, 2008, pp. 372–382.'
ista: 'Guerraoui R, Henzinger TA, Jobstmann B, Singh V. 2008. Model checking transactional
memories. PLDI: Programming Languages Design and Implementation, 372–382.'
mla: Guerraoui, Rachid, et al. Model Checking Transactional Memories. ACM,
2008, pp. 372–82, doi:10.1145/1375581.1375626.
short: R. Guerraoui, T.A. Henzinger, B. Jobstmann, V. Singh, in:, ACM, 2008, pp.
372–382.
conference:
name: 'PLDI: Programming Languages Design and Implementation'
date_created: 2018-12-11T12:08:34Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:34Z
day: '01'
doi: 10.1145/1375581.1375626
extern: 1
file:
- access_level: open_access
checksum: 1238258a27f212fc1a2050a9a246da20
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:05Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5054'
file_name: IST-2012-74-v1+1_Model_checking_transactional_memories.pdf
file_size: 201583
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/model_checking_transactional_memories.pdf
month: '01'
oa: 1
page: 372 - 382
publication_status: published
publisher: ACM
publist_id: '1073'
quality_controlled: 0
status: public
title: Model checking transactional memories
type: conference
year: '2008'
...
---
_id: '4386'
abstract:
- lang: eng
text: We introduce the notion of permissiveness in transactional memories (TM).
Intuitively, a TM is permissive if it never aborts a transaction when it need
not. More specifically, a TM is permissive with respect to a safety property p
if the TM accepts every history that satisfies p. Permissiveness, like safety
and liveness, can be used as a metric to compare TMs. We illustrate that it is
impractical to achieve permissiveness deterministically, and then show how randomization
can be used to achieve permissiveness efficiently. We introduce Adaptive Validation
STM (AVSTM), which is probabilistically permissive with respect to opacity; that
is, every opaque history is accepted by AVSTM with positive probability. Moreover,
AVSTM guarantees lock freedom. Owing to its permissiveness, AVSTM outperforms
other STMs by up to 40% in read dominated workloads in high contention scenarios.
But, in low contention scenarios, the book-keeping done by AVSTM to achieve permissiveness
makes AVSTM, on average, 20-30% worse than existing STMs.
acknowledgement: This research was supported by the Swiss National Science Foundation.
alternative_title:
- LNCS
author:
- first_name: Rachid
full_name: Guerraoui, Rachid
last_name: Guerraoui
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Vasu
full_name: Vasu Singh
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: 'Guerraoui R, Henzinger TA, Singh V. Permissiveness in transactional memories.
In: Vol 5218. Springer; 2008:305-319. doi:10.1007/978-3-540-87779-0_21'
apa: 'Guerraoui, R., Henzinger, T. A., & Singh, V. (2008). Permissiveness in
transactional memories (Vol. 5218, pp. 305–319). Presented at the DISC: Distributed
Computing, Springer. https://doi.org/10.1007/978-3-540-87779-0_21'
chicago: Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Permissiveness
in Transactional Memories,” 5218:305–19. Springer, 2008. https://doi.org/10.1007/978-3-540-87779-0_21.
ieee: 'R. Guerraoui, T. A. Henzinger, and V. Singh, “Permissiveness in transactional
memories,” presented at the DISC: Distributed Computing, 2008, vol. 5218, pp.
305–319.'
ista: 'Guerraoui R, Henzinger TA, Singh V. 2008. Permissiveness in transactional
memories. DISC: Distributed Computing, LNCS, vol. 5218, 305–319.'
mla: Guerraoui, Rachid, et al. Permissiveness in Transactional Memories.
Vol. 5218, Springer, 2008, pp. 305–19, doi:10.1007/978-3-540-87779-0_21.
short: R. Guerraoui, T.A. Henzinger, V. Singh, in:, Springer, 2008, pp. 305–319.
conference:
name: 'DISC: Distributed Computing'
date_created: 2018-12-11T12:08:35Z
date_published: 2008-09-10T00:00:00Z
date_updated: 2021-01-12T07:56:35Z
day: '10'
doi: 10.1007/978-3-540-87779-0_21
extern: 1
intvolume: ' 5218'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/permissiveness_in_transactional_memories.pdf
month: '09'
page: 305 - 319
publication_status: published
publisher: Springer
publist_id: '1072'
quality_controlled: 0
status: public
title: Permissiveness in transactional memories
type: conference
volume: 5218
year: '2008'
...
---
_id: '4387'
abstract:
- lang: eng
text: Software transactional memory (STM) offers a disciplined concurrent programming
model for exploiting the parallelism of modern processor architectures. This paper
presents the first deterministic specification automata for strict serializability
and opacity in STMs. Using an antichain-based tool, we show our deterministic
specifications to be equivalent to more intuitive, nondeterministic specification
automata (which are too large to be determinized automatically). Using deterministic
specification automata, we obtain a complete verification tool for STMs. We also
show how to model and verify contention management within STMs. We automatically
check the opacity of popular STM algorithms, such as TL2 and DSTM, with a universal
contention manager. The universal contention manager is nondeterministic and establishes
correctness for all possible contention management schemes.
acknowledgement: This research was supported by the Swiss National Science Foundation.
alternative_title:
- LNCS
author:
- first_name: Rachid
full_name: Guerraoui, Rachid
last_name: Guerraoui
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Vasu
full_name: Vasu Singh
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: 'Guerraoui R, Henzinger TA, Singh V. Completeness and nondeterminism in model
checking transactional memories. In: Vol 5201. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik; 2008:21-35. doi:10.1007/978-3-540-85361-9_6'
apa: 'Guerraoui, R., Henzinger, T. A., & Singh, V. (2008). Completeness and
nondeterminism in model checking transactional memories (Vol. 5201, pp. 21–35).
Presented at the CONCUR: Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.1007/978-3-540-85361-9_6'
chicago: Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Completeness and
Nondeterminism in Model Checking Transactional Memories,” 5201:21–35. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2008. https://doi.org/10.1007/978-3-540-85361-9_6.
ieee: 'R. Guerraoui, T. A. Henzinger, and V. Singh, “Completeness and nondeterminism
in model checking transactional memories,” presented at the CONCUR: Concurrency
Theory, 2008, vol. 5201, pp. 21–35.'
ista: 'Guerraoui R, Henzinger TA, Singh V. 2008. Completeness and nondeterminism
in model checking transactional memories. CONCUR: Concurrency Theory, LNCS, vol.
5201, 21–35.'
mla: Guerraoui, Rachid, et al. Completeness and Nondeterminism in Model Checking
Transactional Memories. Vol. 5201, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2008, pp. 21–35, doi:10.1007/978-3-540-85361-9_6.
short: R. Guerraoui, T.A. Henzinger, V. Singh, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2008, pp. 21–35.
conference:
name: 'CONCUR: Concurrency Theory'
date_created: 2018-12-11T12:08:35Z
date_published: 2008-07-30T00:00:00Z
date_updated: 2021-01-12T07:56:35Z
day: '30'
doi: 10.1007/978-3-540-85361-9_6
extern: 1
intvolume: ' 5201'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/completeness_and_nondeterminism_in_model_checking_transactional_memories.pdf
month: '07'
page: 21 - 35
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '1071'
quality_controlled: 0
status: public
title: Completeness and nondeterminism in model checking transactional memories
type: conference
volume: 5201
year: '2008'
...
---
_id: '4397'
alternative_title:
- LNCS 5123
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Damien
full_name: Damien Zufferey
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: 'Beyer D, Zufferey D, Majumdar R. CSIsat: Interpolation for LA+EUF. In: Springer;
2008:304-308.'
apa: 'Beyer, D., Zufferey, D., & Majumdar, R. (2008). CSIsat: Interpolation
for LA+EUF (pp. 304–308). Presented at the CAV: Computer Aided Verification, Springer.'
chicago: 'Beyer, Dirk, Damien Zufferey, and Ritankar Majumdar. “CSIsat: Interpolation
for LA+EUF,” 304–8. Springer, 2008.'
ieee: 'D. Beyer, D. Zufferey, and R. Majumdar, “CSIsat: Interpolation for LA+EUF,”
presented at the CAV: Computer Aided Verification, 2008, pp. 304–308.'
ista: 'Beyer D, Zufferey D, Majumdar R. 2008. CSIsat: Interpolation for LA+EUF.
CAV: Computer Aided Verification, LNCS 5123, , 304–308.'
mla: 'Beyer, Dirk, et al. CSIsat: Interpolation for LA+EUF. Springer, 2008,
pp. 304–08.'
short: D. Beyer, D. Zufferey, R. Majumdar, in:, Springer, 2008, pp. 304–308.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:38Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:40Z
day: '01'
extern: 1
month: '01'
page: 304 - 308
publication_status: published
publisher: Springer
publist_id: '1060'
quality_controlled: 0
status: public
title: 'CSIsat: Interpolation for LA+EUF'
type: conference
year: '2008'
...
---
_id: '4400'
author:
- first_name: Adam
full_name: Aviv,Adam J.
last_name: Aviv
- first_name: Pavol
full_name: Pavol Cerny
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Sandy
full_name: Clark,Sandy
last_name: Clark
- first_name: Eric
full_name: Cronin,Eric
last_name: Cronin
- first_name: Gaurav
full_name: Shah,Gaurav
last_name: Shah
- first_name: Micah
full_name: Sherr,Micah
last_name: Sherr
- first_name: Matt
full_name: Blaze,Matt
last_name: Blaze
citation:
ama: 'Aviv A, Cerny P, Clark S, et al. Security Evaluation of ES&S Voting
Machines and Election Management System. In: USENIX; 2008. doi:1545'
apa: Aviv, A., Cerny, P., Clark, S., Cronin, E., Shah, G., Sherr, M., & Blaze,
M. (2008). Security Evaluation of ES&S Voting Machines and Election Management
System. Presented at the Usenix/ Accurate Electronic Voting Technology Workshop
(EVT) 08, USENIX. https://doi.org/1545
chicago: Aviv, Adam, Pavol Cerny, Sandy Clark, Eric Cronin, Gaurav Shah, Micah Sherr,
and Matt Blaze. “Security Evaluation of ES&S Voting Machines and Election
Management System.” USENIX, 2008. https://doi.org/1545.
ieee: A. Aviv et al., “Security Evaluation of ES&S Voting Machines
and Election Management System,” presented at the Usenix/ Accurate Electronic
Voting Technology Workshop (EVT) 08, 2008.
ista: Aviv A, Cerny P, Clark S, Cronin E, Shah G, Sherr M, Blaze M. 2008. Security
Evaluation of ES&S Voting Machines and Election Management System. Usenix/
Accurate Electronic Voting Technology Workshop (EVT) 08.
mla: Aviv, Adam, et al. Security Evaluation of ES&S Voting Machines and
Election Management System. USENIX, 2008, doi:1545.
short: A. Aviv, P. Cerny, S. Clark, E. Cronin, G. Shah, M. Sherr, M. Blaze, in:,
USENIX, 2008.
conference:
name: Usenix/ Accurate Electronic Voting Technology Workshop (EVT) 08
date_created: 2018-12-11T12:08:39Z
date_published: 2008-07-29T00:00:00Z
date_updated: 2021-01-12T07:56:42Z
day: '29'
doi: '1545'
extern: 1
main_file_link:
- open_access: '0'
url: http://www.usenix.org/event/evt08/tech/full_papers/aviv/aviv.pdf
month: '07'
publication_status: published
publisher: USENIX
publist_id: '1057'
quality_controlled: 0
status: public
title: Security Evaluation of ES&S Voting Machines and Election Management System
type: conference
year: '2008'
...
---
_id: '4409'
abstract:
- lang: eng
text: "Models of timed systems must incorporate not only the sequence of system
events, but the timings of these events as well to capture the real-time aspects
of physical systems. Timed automata are models of real-time systems in which states
consist of discrete locations and values for real-time clocks. The presence of
real-time clocks leads to an uncountable state space. This thesis studies verification
problems on timed automata in a game theoretic framework.\r\n\r\nFor untimed systems,
two systems are close if every sequence of events of one system is also observable
in the second system. For timed systems, the difference in timings of the two
corresponding sequences is also of importance. We propose the notion of bisimulation
distance which quantifies timing differences; if the bisimulation distance between
two systems is epsilon, then (a) every sequence of events of one system has a
corresponding matching sequence in the other, and (b) the timings of matching
events in between the two corresponding traces do not differ by more than epsilon.
We show that we can compute the bisimulation distance between two timed automata
to within any desired degree of accuracy. We also show that the timed verification
logic TCTL is robust with respect to our notion of quantitative bisimilarity,
in particular, if a system satisfies a formula, then every close system satisfies
a close formula.\r\n\r\nTimed games are used for distinguishing between the actions
of several agents, typically a controller and an environment. The controller must
achieve its objective against all possible choices of the environment. The modeling
of the passage of time leads to the presence of zeno executions, and corresponding
unrealizable strategies of the controller which may achieve objectives by blocking
time. We disallow such unreasonable strategies by restricting all agents to use
only receptive strategies --strategies which while not being required to ensure
time divergence by any agent, are such that no agent is responsible for blocking
time. Time divergence is guaranteed when all players use receptive strategies.
We show that timed automaton games with receptive strategies can be solved by
a reduction to finite state turn based game graphs. We define the logic timed
alternating-time temporal logic for verification of timed automaton games and
show that the logic can be model checked in EXPTIME. We also show that the minimum
time required by an agent to reach a desired location, and the maximum time an
agent can stay safe within a set of locations, against all possible actions of
its adversaries are both computable.\r\n\r\nWe next study the memory requirements
of winning strategies for timed automaton games. We prove that finite memory strategies
suffice for safety objectives, and that winning strategies for reachability objectives
may require infinite memory in general. We introduce randomized strategies in
which an agent can propose a probabilistic distribution of moves and show that
finite memory randomized strategies suffice for all omega-regular objectives.
We also show that while randomization helps in simplifying winning strategies,
and thus allows the construction of simpler controllers, it does not help a player
in winning at more states, and thus does not allow the construction of more powerful
controllers.\r\n\r\nFinally we study robust winning strategies in timed games.
In a physical system, a controller may propose an action together with a time
delay, but the action cannot be assumed to be executed at the exact proposed time
delay. We present robust strategies which incorporate such jitters and show that
the set of states from which an agent can win robustly is computable."
article_processing_charge: No
author:
- first_name: Vinayak
full_name: Prabhu, Vinayak
last_name: Prabhu
citation:
ama: Prabhu V. Games for the verification of timed systems. 2008:1-137.
apa: Prabhu, V. (2008). Games for the verification of timed systems. University
of California, Berkeley.
chicago: Prabhu, Vinayak. “Games for the Verification of Timed Systems.” University
of California, Berkeley, 2008.
ieee: V. Prabhu, “Games for the verification of timed systems,” University of California,
Berkeley, 2008.
ista: Prabhu V. 2008. Games for the verification of timed systems. University of
California, Berkeley.
mla: Prabhu, Vinayak. Games for the Verification of Timed Systems. University
of California, Berkeley, 2008, pp. 1–137.
short: V. Prabhu, Games for the Verification of Timed Systems, University of California,
Berkeley, 2008.
date_created: 2018-12-11T12:08:42Z
date_published: 2008-09-01T00:00:00Z
date_updated: 2022-02-14T14:35:11Z
day: '01'
degree_awarded: PhD
extern: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-97.html
month: '09'
oa: 1
oa_version: None
page: 1 - 137
publication_status: published
publisher: University of California, Berkeley
publist_id: '319'
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
- first_name: John
full_name: Steel, John
last_name: Steel
- first_name: Pravin
full_name: Varaiya, Pravin
last_name: Varaiya
title: Games for the verification of timed systems
type: dissertation
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2008'
...
---
_id: '4415'
abstract:
- lang: eng
text: 'Many computing applications, especially those in safety critical embedded
systems, require highly predictable timing properties. However, time is often
not present in the prevailing computing and networking abstractions. In fact,
most advances in computer architecture, software, and networking favor average-case
performance over timing predictability. This thesis studies several methods for
the design of concurrent and/or distributed embedded systems with precise timing
guarantees. The focus is on flexible and compositional methods for programming
and verification of the timing properties. The presented methods together with
related formalisms cover two levels of design: (1) Programming language/model
level. We propose the distributed variant of Giotto, a coordination programming
language with an explicit temporal semantics—the logical execution time (LET)
semantics. The LET of a task is an interval of time that specifies the time instants
at which task inputs and outputs become available (task release and termination
instants). The LET of a task is always non-zero. This allows us to communicate
values across the network without changing the timing information of the task,
and without introducing nondeterminism. We show how this methodology supports
distributed code generation for distributed real-time systems. The method gives
up some performance in favor of composability and predictability. We characterize
the tradeoff by comparing the LET semantics with the semantics used in Simulink.
(2) Abstract task graph level. We study interface-based design and verification
of applications represented with task graphs. We consider task sequence graphs
with general event models, and cyclic graphs with periodic event models with jitter
and phase. Here an interface of a component exposes time and resource constraints
of the component. Together with interfaces we formally define interface composition
operations and the refinement relation. For efficient and flexible composability
checking two properties are important: incremental design and independent refinement.
According to the incremental design property the composition of interfaces can
be performed in any order, even if interfaces for some components are not known.
The refinement relation is defined such that in a design we can always substitute
a refined interface for an abstract one. We show that the framework supports independent
refinement, i.e., the refinement relation is preserved under composition operations.'
acknowledgement: 978-0-549-83480-9
article_processing_charge: No
author:
- first_name: Slobodan
full_name: Matic, Slobodan
last_name: Matic
citation:
ama: Matic S. Compositionality in deterministic real-time embedded systems. 2008:1-148.
apa: Matic, S. (2008). Compositionality in deterministic real-time embedded systems.
University of California, Berkeley.
chicago: Matic, Slobodan. “Compositionality in Deterministic Real-Time Embedded
Systems.” University of California, Berkeley, 2008.
ieee: S. Matic, “Compositionality in deterministic real-time embedded systems,”
University of California, Berkeley, 2008.
ista: Matic S. 2008. Compositionality in deterministic real-time embedded systems.
University of California, Berkeley.
mla: Matic, Slobodan. Compositionality in Deterministic Real-Time Embedded Systems.
University of California, Berkeley, 2008, pp. 1–148.
short: S. Matic, Compositionality in Deterministic Real-Time Embedded Systems, University
of California, Berkeley, 2008.
date_created: 2018-12-11T12:08:44Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2022-02-14T14:08:50Z
day: '01'
degree_awarded: PhD
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 1 - 148
publication_status: published
publisher: University of California, Berkeley
publist_id: '316'
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
- first_name: Edward
full_name: Lee, Edward
last_name: Lee
- first_name: Raja
full_name: Sengupta, Raja
last_name: Sengupta
title: Compositionality in deterministic real-time embedded systems
type: dissertation
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2008'
...
---
_id: '4452'
abstract:
- lang: eng
text: We describe Valigator, a software tool for imperative program verification
that efficiently combines symbolic computation and automated reasoning in a uniform
framework. The system offers support for automatically generating and proving
verification conditions and, most importantly, for automatically inferring loop
invariants and bound assertions by means of symbolic summation, Gröbner basis
computation, and quantifier elimination. We present general principles of the
implementation and illustrate them on examples.
acknowledgement: This research was supported by the Swiss NSF.
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: Thibaud
full_name: Hottelier, Thibaud
last_name: Hottelier
- first_name: Laura
full_name: Kovács, Laura
last_name: Kovács
citation:
ama: 'Henzinger TA, Hottelier T, Kovács L. Valigator: A verification tool with bound
and invariant generation. In: Vol 5330. Springer; 2008:333-342. doi:10.1007/978-3-540-89439-1_24'
apa: 'Henzinger, T. A., Hottelier, T., & Kovács, L. (2008). Valigator: A verification
tool with bound and invariant generation (Vol. 5330, pp. 333–342). Presented at
the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Springer.
https://doi.org/10.1007/978-3-540-89439-1_24'
chicago: 'Henzinger, Thomas A, Thibaud Hottelier, and Laura Kovács. “Valigator:
A Verification Tool with Bound and Invariant Generation,” 5330:333–42. Springer,
2008. https://doi.org/10.1007/978-3-540-89439-1_24.'
ieee: 'T. A. Henzinger, T. Hottelier, and L. Kovács, “Valigator: A verification
tool with bound and invariant generation,” presented at the LPAR: Logic for Programming,
Artificial Intelligence, and Reasoning, 2008, vol. 5330, pp. 333–342.'
ista: 'Henzinger TA, Hottelier T, Kovács L. 2008. Valigator: A verification tool
with bound and invariant generation. LPAR: Logic for Programming, Artificial Intelligence,
and Reasoning, LNCS, vol. 5330, 333–342.'
mla: 'Henzinger, Thomas A., et al. Valigator: A Verification Tool with Bound
and Invariant Generation. Vol. 5330, Springer, 2008, pp. 333–42, doi:10.1007/978-3-540-89439-1_24.'
short: T.A. Henzinger, T. Hottelier, L. Kovács, in:, Springer, 2008, pp. 333–342.
conference:
name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning'
date_created: 2018-12-11T12:08:55Z
date_published: 2008-11-13T00:00:00Z
date_updated: 2021-01-12T07:57:04Z
day: '13'
doi: 10.1007/978-3-540-89439-1_24
extern: 1
intvolume: ' 5330'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/valigator.pdf
month: '11'
page: 333 - 342
publication_status: published
publisher: Springer
publist_id: '277'
quality_controlled: 0
status: public
title: 'Valigator: A verification tool with bound and invariant generation'
type: conference
volume: 5330
year: '2008'
...
---
_id: '4509'
abstract:
- lang: eng
text: 'I discuss two main challenges in embedded systems design: the challenge to
build predictable systems, and that to build robust systems. I suggest how predictability
can be formalized as a form of determinism, and robustness as a form of continuity.'
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Henzinger TA. Two challenges in embedded systems design: Predictability and
robustness. Philosophical Transactions of the Royal Society A Mathematical
Physical and Engineering Sciences. 2008;366(1881):3727-3736. doi:10.1098/rsta.2008.0141'
apa: 'Henzinger, T. A. (2008). Two challenges in embedded systems design: Predictability
and robustness. Philosophical Transactions of the Royal Society A Mathematical
Physical and Engineering Sciences. Royal Society of London. https://doi.org/10.1098/rsta.2008.0141'
chicago: 'Henzinger, Thomas A. “Two Challenges in Embedded Systems Design: Predictability
and Robustness.” Philosophical Transactions of the Royal Society A Mathematical
Physical and Engineering Sciences. Royal Society of London, 2008. https://doi.org/10.1098/rsta.2008.0141.'
ieee: 'T. A. Henzinger, “Two challenges in embedded systems design: Predictability
and robustness,” Philosophical Transactions of the Royal Society A Mathematical
Physical and Engineering Sciences, vol. 366, no. 1881. Royal Society of London,
pp. 3727–3736, 2008.'
ista: 'Henzinger TA. 2008. Two challenges in embedded systems design: Predictability
and robustness. Philosophical Transactions of the Royal Society A Mathematical
Physical and Engineering Sciences. 366(1881), 3727–3736.'
mla: 'Henzinger, Thomas A. “Two Challenges in Embedded Systems Design: Predictability
and Robustness.” Philosophical Transactions of the Royal Society A Mathematical
Physical and Engineering Sciences, vol. 366, no. 1881, Royal Society of London,
2008, pp. 3727–36, doi:10.1098/rsta.2008.0141.'
short: T.A. Henzinger, Philosophical Transactions of the Royal Society A Mathematical
Physical and Engineering Sciences 366 (2008) 3727–3736.
date_created: 2018-12-11T12:09:13Z
date_published: 2008-07-31T00:00:00Z
date_updated: 2021-01-12T07:59:19Z
day: '31'
doi: 10.1098/rsta.2008.0141
extern: 1
intvolume: ' 366'
issue: '1881'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/two_challenges_in_embedded_systems_design.pdf
month: '07'
page: 3727 - 3736
publication: Philosophical Transactions of the Royal Society A Mathematical Physical
and Engineering Sciences
publication_status: published
publisher: Royal Society of London
publist_id: '219'
quality_controlled: 0
status: public
title: 'Two challenges in embedded systems design: Predictability and robustness'
type: journal_article
volume: 366
year: '2008'
...
---
_id: '4521'
abstract:
- lang: eng
text: The search for proof and the search for counterexamples (bugs) are complementary
activities that need to be pursued concurrently in order to maximize the practical
success rate of verification tools.While this is well-understood in safety verification,
the current focus of liveness verification has been almost exclusively on the
search for termination proofs. A counterexample to termination is an infinite
programexecution. In this paper, we propose a method to search for such counterexamples.
The search proceeds in two phases. We first dynamically enumerate lasso-shaped
candidate paths for counterexamples, and then statically prove their feasibility.
We illustrate the utility of our nontermination prover, called TNT, on several
nontrivial examples, some of which require bit-level reasoning about integer representations.
author:
- first_name: Ashutosh
full_name: Ashutosh Gupta
id: 335E5684-F248-11E8-B48F-1D18A9856A87
last_name: Gupta
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
- first_name: Andrey
full_name: Rybalchenko, Andrey
last_name: Rybalchenko
- first_name: Ru
full_name: Xu, Ru-Gang
last_name: Xu
citation:
ama: 'Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R. Proving non-termination.
In: ACM; 2008:147-158. doi:10.1145/1328438.1328459'
apa: 'Gupta, A., Henzinger, T. A., Majumdar, R., Rybalchenko, A., & Xu, R. (2008).
Proving non-termination (pp. 147–158). Presented at the POPL: Principles of Programming
Languages, ACM. https://doi.org/10.1145/1328438.1328459'
chicago: Gupta, Ashutosh, Thomas A Henzinger, Ritankar Majumdar, Andrey Rybalchenko,
and Ru Xu. “Proving Non-Termination,” 147–58. ACM, 2008. https://doi.org/10.1145/1328438.1328459.
ieee: 'A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, and R. Xu, “Proving
non-termination,” presented at the POPL: Principles of Programming Languages,
2008, pp. 147–158.'
ista: 'Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R. 2008. Proving non-termination.
POPL: Principles of Programming Languages, 147–158.'
mla: Gupta, Ashutosh, et al. Proving Non-Termination. ACM, 2008, pp. 147–58,
doi:10.1145/1328438.1328459.
short: A. Gupta, T.A. Henzinger, R. Majumdar, A. Rybalchenko, R. Xu, in:, ACM, 2008,
pp. 147–158.
conference:
name: 'POPL: Principles of Programming Languages'
date_created: 2018-12-11T12:09:17Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:25Z
day: '01'
doi: 10.1145/1328438.1328459
extern: 1
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/proving_non-termination.pdf
month: '01'
page: 147 - 158
publication_status: published
publisher: ACM
publist_id: '208'
quality_controlled: 0
status: public
title: Proving non-termination
type: conference
year: '2008'
...
---
_id: '4524'
abstract:
- lang: eng
text: "Complex requirements, time-to-market pressure and regulatory constraints
have made the designing of embedded systems extremely challenging. This is evident
by the increase in effort and expenditure for design of safety-driven real-time
control-dominated applications like automotive and avionic controllers. Design
processes are often challenged by lack of proper programming tools for specifying
and verifying critical requirements (e.g. timing and reliability) of such applications.
Platform based design, an approach for designing embedded systems, addresses the
above concerns by separating requirement from architecture. The requirement specifies
the intended behavior of an application while the architecture specifies the guarantees
(e.g. execution speed, failure rate etc). An implementation, a mapping of the
requirement on the architecture, is then analyzed for correctness. The orthogonalization
of concerns makes the specification and analyses simpler. An effective use of
such design methodology has been proposed in Logical Execution Time (LET) model
of real-time tasks. The model separates the timing requirements (specified by
release and termination instances of a task) from the architecture guarantees
(specified by worst-case execution time of the task).\r\n\r\nThis dissertation
proposes a coordination language, Hierarchical Timing Language (HTL), that captures
the timing and reliability requirements of real-time applications. An implementation
of the program on an architecture is then analyzed to check whether desired timing
and reliability requirements are met or not. The core framework extends the LET
model by accounting for reliability and refinement. The reliability model separates
the reliability requirements of tasks from the reliability guarantees of the architecture.
The requirement expresses the desired long-term reliability while the architecture
provides a short-term reliability guarantee (e.g. failure rate for each iteration).
The analysis checks if the short-term guarantee ensures the desired long-term
reliability. The refinement model allows replacing a task by another task during
program execution. Refinement preserves schedulability and reliability, i.e.,
if a refined task is schedulable and reliable for an implementation, then the
refining task is also schedulable and reliable for the implementation. Refinement
helps in concise specification without overloading analysis.\r\n\r\nThe work presents
the formal model, the analyses (both with and without refinement), and a compiler
for HTL programs. The compiler checks composition and refinement constraints,
performs schedulability and reliability analyses, and generates code for implementation
of an HTL program on a virtual machine. Three real-time controllers, one each
from automatic control, automotive control and avionic control, are used to illustrate
the steps in modeling and analyzing HTL programs."
acknowledgement: 978-0-549-83679-7
article_processing_charge: No
author:
- first_name: Arkadeb
full_name: Ghosal, Arkadeb
last_name: Ghosal
citation:
ama: Ghosal A. A hierarchical coordination language for reliable real-time tasks.
2008:1-210.
apa: Ghosal, A. (2008). A hierarchical coordination language for reliable real-time
tasks. University of California, Berkeley.
chicago: Ghosal, Arkadeb. “A Hierarchical Coordination Language for Reliable Real-Time
Tasks.” University of California, Berkeley, 2008.
ieee: A. Ghosal, “A hierarchical coordination language for reliable real-time tasks,”
University of California, Berkeley, 2008.
ista: Ghosal A. 2008. A hierarchical coordination language for reliable real-time
tasks. University of California, Berkeley.
mla: Ghosal, Arkadeb. A Hierarchical Coordination Language for Reliable Real-Time
Tasks. University of California, Berkeley, 2008, pp. 1–210.
short: A. Ghosal, A Hierarchical Coordination Language for Reliable Real-Time Tasks,
University of California, Berkeley, 2008.
date_created: 2018-12-11T12:09:18Z
date_published: 2008-01-31T00:00:00Z
date_updated: 2021-01-12T07:59:26Z
day: '31'
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 1 - 210
publication_status: published
publisher: University of California, Berkeley
publist_id: '199'
status: public
supervisor:
- first_name: Alberto
full_name: Sangiovanni-Vincentelli, Alberto
last_name: Sangiovanni-Vincentelli
- 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: Edward
full_name: Lee, Edward
last_name: Lee
- first_name: Karl
full_name: Hedrick, Karl
last_name: Hedrick
title: A hierarchical coordination language for reliable real-time tasks
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2008'
...
---
_id: '4527'
abstract:
- lang: eng
text: |-
We introduce bounded asynchrony, a notion of concurrency tailored to the modeling of biological cell-cell interactions. Bounded asynchrony is the result of a scheduler that bounds the number of steps that one process gets ahead of other processes; this allows the components of a system to move independently while keeping them coupled. Bounded asynchrony accurately reproduces the experimental observations made about certain cell-cell interactions: its constrained nondeterminism captures the variability observed in cells that, although equally potent, assume distinct fates. Real-life cells are not “scheduled”, but we show that distributed real-time behavior can lead to component interactions that are observationally equivalent to bounded asynchrony; this provides a possible mechanistic explanation for the phenomena observed during cell fate specification.
We use model checking to determine cell fates. The nondeterminism of bounded asynchrony causes state explosion during model checking, but partial-order methods are not directly applicable. We present a new algorithm that reduces the number of states that need to be explored: our optimization takes advantage of the bounded-asynchronous progress and the spatially local interactions of components that model cells. We compare our own communication-based reduction with partial-order reduction (on a restricted form of bounded asynchrony) and experiments illustrate that our algorithm leads to significant savings.
acknowledgement: Supported in part by the Swiss National Science Foundation (grant
205321-111840).
alternative_title:
- LNCS
author:
- first_name: Jasmin
full_name: Fisher, Jasmin
last_name: Fisher
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Maria
full_name: Maria Mateescu
id: 3B43276C-F248-11E8-B48F-1D18A9856A87
last_name: Mateescu
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
citation:
ama: 'Fisher J, Henzinger TA, Mateescu M, Piterman N. Bounded asynchrony: Concurrency
for modeling cell-cell interactions. In: Vol 5054. Springer; 2008:17-32. doi:10.1007/978-3-540-68413-8_2'
apa: 'Fisher, J., Henzinger, T. A., Mateescu, M., & Piterman, N. (2008). Bounded
asynchrony: Concurrency for modeling cell-cell interactions (Vol. 5054, pp. 17–32).
Presented at the FMSB: Formal Methods in Systems Biology, Springer. https://doi.org/10.1007/978-3-540-68413-8_2'
chicago: 'Fisher, Jasmin, Thomas A Henzinger, Maria Mateescu, and Nir Piterman.
“Bounded Asynchrony: Concurrency for Modeling Cell-Cell Interactions,” 5054:17–32.
Springer, 2008. https://doi.org/10.1007/978-3-540-68413-8_2.'
ieee: 'J. Fisher, T. A. Henzinger, M. Mateescu, and N. Piterman, “Bounded asynchrony:
Concurrency for modeling cell-cell interactions,” presented at the FMSB: Formal
Methods in Systems Biology, 2008, vol. 5054, pp. 17–32.'
ista: 'Fisher J, Henzinger TA, Mateescu M, Piterman N. 2008. Bounded asynchrony:
Concurrency for modeling cell-cell interactions. FMSB: Formal Methods in Systems
Biology, LNCS, vol. 5054, 17–32.'
mla: 'Fisher, Jasmin, et al. Bounded Asynchrony: Concurrency for Modeling Cell-Cell
Interactions. Vol. 5054, Springer, 2008, pp. 17–32, doi:10.1007/978-3-540-68413-8_2.'
short: J. Fisher, T.A. Henzinger, M. Mateescu, N. Piterman, in:, Springer, 2008,
pp. 17–32.
conference:
name: 'FMSB: Formal Methods in Systems Biology'
date_created: 2018-12-11T12:09:19Z
date_published: 2008-05-26T00:00:00Z
date_updated: 2021-01-12T07:59:27Z
day: '26'
doi: 10.1007/978-3-540-68413-8_2
extern: 1
intvolume: ' 5054'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/bounded_asynchrony.pdf
month: '05'
page: 17 - 32
publication_status: published
publisher: Springer
publist_id: '196'
quality_controlled: 0
status: public
title: 'Bounded asynchrony: Concurrency for modeling cell-cell interactions'
type: conference
volume: 5054
year: '2008'
...
---
_id: '4532'
abstract:
- lang: eng
text: We consider the equivalence problem for labeled Markov chains (LMCs), where
each state is labeled with an observation. Two LMCs are equivalent if every finite
sequence of observations has the same probability of occurrence in the two LMCs.
We show that equivalence can be decided in polynomial time, using a reduction
to the equivalence problem for probabilistic automata, which is known to be solvable
in polynomial time. We provide an alternative algorithm to solve the equivalence
problem, which is based on a new definition of bisimulation for probabilistic
automata. We also extend the technique to decide the equivalence of weighted probabilistic
automata.
author:
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jean
full_name: Raskin, Jean-François
last_name: Raskin
citation:
ama: Doyen L, Henzinger TA, Raskin J. Equivalence of labeled Markov chains. International
Journal of Foundations of Computer Science. 2008;19(3):549-563. doi:10.1142/S0129054108005814
apa: Doyen, L., Henzinger, T. A., & Raskin, J. (2008). Equivalence of labeled
Markov chains. International Journal of Foundations of Computer Science.
World Scientific Publishing. https://doi.org/10.1142/S0129054108005814
chicago: Doyen, Laurent, Thomas A Henzinger, and Jean Raskin. “Equivalence of Labeled
Markov Chains.” International Journal of Foundations of Computer Science.
World Scientific Publishing, 2008. https://doi.org/10.1142/S0129054108005814 .
ieee: L. Doyen, T. A. Henzinger, and J. Raskin, “Equivalence of labeled Markov chains,”
International Journal of Foundations of Computer Science, vol. 19, no.
3. World Scientific Publishing, pp. 549–563, 2008.
ista: Doyen L, Henzinger TA, Raskin J. 2008. Equivalence of labeled Markov chains.
International Journal of Foundations of Computer Science. 19(3), 549–563.
mla: Doyen, Laurent, et al. “Equivalence of Labeled Markov Chains.” International
Journal of Foundations of Computer Science, vol. 19, no. 3, World Scientific
Publishing, 2008, pp. 549–63, doi:10.1142/S0129054108005814 .
short: L. Doyen, T.A. Henzinger, J. Raskin, International Journal of Foundations
of Computer Science 19 (2008) 549–563.
date_created: 2018-12-11T12:09:20Z
date_published: 2008-06-01T00:00:00Z
date_updated: 2021-01-12T07:59:30Z
day: '01'
doi: '10.1142/S0129054108005814 '
extern: 1
intvolume: ' 19'
issue: '3'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/equivalence_of_labeled_markov_chains.pdf
month: '06'
page: 549 - 563
publication: International Journal of Foundations of Computer Science
publication_status: published
publisher: World Scientific Publishing
publist_id: '192'
quality_controlled: 0
status: public
title: Equivalence of labeled Markov chains
type: journal_article
volume: 19
year: '2008'
...