---
_id: '1971'
abstract:
- lang: eng
text: Complex I plays a central role in cellular energy production, coupling electron
transfer between NADH and quinone to proton translocation. The mechanism of this
highly efficient enzyme is currently unknown. Mitochondrial complex I is a major
source of reactive oxygen species, which may be one of the causes of aging. Dysfunction
of complex I is implicated in many human neurodegenerative diseases. We have determined
several x-ray structures of the oxidized and reduced hydrophilic domain of complex
I from Thermus thermophilus at up to 3.1 Å resolution. The structures reveal the
mode of interaction of complex I with NADH, explaining known kinetic data and
providing implications for the mechanism of reactive oxygen species production
at the flavin site of complex I. Bound metals were identified in the channel at
the interface with the frataxin-like subunit Nqo15, indicating possible iron-binding
sites. Conformational changes upon reduction of the complex involve adjustments
in the nucleotide-binding pocket, as well as small but significant shifts of several
α-helices at the interface with the membrane domain. These shifts are likely to
be driven by the reduction of nearby iron-sulfur clusters N2 and N6a/b. Cluster
N2 is the electron donor to quinone and is coordinated by unique motif involving
two consecutive (tandem) cysteines. An unprecedented "on/off switch"
(disconnection) of coordinating bonds between the tandem cysteines and this cluster
was observed upon reduction. Comparison of the structures suggests a novel mechanism
of coupling between electron transfer and proton translocation, combining conformational
changes and protonation/deprotonation of tandem cysteines.
acknowledgement: 'This work was supported by the Medical Research Council. '
author:
- first_name: John
full_name: Berrisford, John M
last_name: Berrisford
- first_name: Leonid A
full_name: Leonid Sazanov
id: 338D39FE-F248-11E8-B48F-1D18A9856A87
last_name: Sazanov
orcid: 0000-0002-0977-7989
citation:
ama: Berrisford J, Sazanov LA. Structural basis for the mechanism of respiratory
complex I. Journal of Biological Chemistry. 2009;284(43):29773-29783. doi:10.1074/jbc.M109.032144
apa: Berrisford, J., & Sazanov, L. A. (2009). Structural basis for the mechanism
of respiratory complex I. Journal of Biological Chemistry. American Society
for Biochemistry and Molecular Biology. https://doi.org/10.1074/jbc.M109.032144
chicago: Berrisford, John, and Leonid A Sazanov. “Structural Basis for the Mechanism
of Respiratory Complex I.” Journal of Biological Chemistry. American Society
for Biochemistry and Molecular Biology, 2009. https://doi.org/10.1074/jbc.M109.032144.
ieee: J. Berrisford and L. A. Sazanov, “Structural basis for the mechanism of respiratory
complex I,” Journal of Biological Chemistry, vol. 284, no. 43. American
Society for Biochemistry and Molecular Biology, pp. 29773–29783, 2009.
ista: Berrisford J, Sazanov LA. 2009. Structural basis for the mechanism of respiratory
complex I. Journal of Biological Chemistry. 284(43), 29773–29783.
mla: Berrisford, John, and Leonid A. Sazanov. “Structural Basis for the Mechanism
of Respiratory Complex I.” Journal of Biological Chemistry, vol. 284, no.
43, American Society for Biochemistry and Molecular Biology, 2009, pp. 29773–83,
doi:10.1074/jbc.M109.032144.
short: J. Berrisford, L.A. Sazanov, Journal of Biological Chemistry 284 (2009) 29773–29783.
date_created: 2018-12-11T11:54:59Z
date_published: 2009-10-23T00:00:00Z
date_updated: 2021-01-12T06:54:26Z
day: '23'
doi: 10.1074/jbc.M109.032144
extern: 1
intvolume: ' 284'
issue: '43'
month: '10'
page: 29773 - 29783
publication: Journal of Biological Chemistry
publication_status: published
publisher: American Society for Biochemistry and Molecular Biology
publist_id: '5114'
quality_controlled: 0
status: public
title: Structural basis for the mechanism of respiratory complex I
type: journal_article
volume: 284
year: '2009'
...
---
_id: '4357'
abstract:
- lang: eng
text: Parallel evolution is the acquisition of identical adaptive traits in independently
evolving populations. Understanding whether the genetic changes underlying adaptation
to a common selective environment are parallel within and between species is interesting
because it sheds light on the degree of evolutionary constraints. If parallel
evolution is perfect, then the implication is that forces such as functional constraints,
epistasis, and pleiotropy play an important role in shaping the outcomes of adaptive
evolution. In addition, population genetic theory predicts that the probability
of parallel evolution will decline with an increase in the number of adaptive
solutions-if a single adaptive solution exists, then parallel evolution will be
observed among highly divergent species. For this reason, it is predicted that
close relatives-which likely overlap more in the details of their adaptive solutions-will
show more parallel evolution. By adapting three related bacteriophage species
to a novel environment we find (1) a high rate of parallel genetic evolution at
orthologous nucleotide and amino acid residues within species, (2) parallel beneficial
mutations do not occur in a common order in which they fix or appear in an evolving
population, (3) low rates of parallel evolution and convergent evolution between
species, and (4) the probability of parallel and convergent evolution between
species is strongly effected by divergence.
author:
- first_name: Jonathan P
full_name: Jonathan Bollback
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
- first_name: John
full_name: Huelsenbeck, John P
last_name: Huelsenbeck
citation:
ama: Bollback JP, Huelsenbeck J. Parallel genetic evolution within and between bacteriophage
species of varying degrees of divergence. Genetics. 2009;181(1):225-234.
doi:10.1534/genetics.107.085225
apa: Bollback, J. P., & Huelsenbeck, J. (2009). Parallel genetic evolution within
and between bacteriophage species of varying degrees of divergence. Genetics.
Genetics Society of America. https://doi.org/10.1534/genetics.107.085225
chicago: Bollback, Jonathan P, and John Huelsenbeck. “Parallel Genetic Evolution
within and between Bacteriophage Species of Varying Degrees of Divergence.” Genetics.
Genetics Society of America, 2009. https://doi.org/10.1534/genetics.107.085225.
ieee: J. P. Bollback and J. Huelsenbeck, “Parallel genetic evolution within and
between bacteriophage species of varying degrees of divergence,” Genetics,
vol. 181, no. 1. Genetics Society of America, pp. 225–234, 2009.
ista: Bollback JP, Huelsenbeck J. 2009. Parallel genetic evolution within and between
bacteriophage species of varying degrees of divergence. Genetics. 181(1), 225–234.
mla: Bollback, Jonathan P., and John Huelsenbeck. “Parallel Genetic Evolution within
and between Bacteriophage Species of Varying Degrees of Divergence.” Genetics,
vol. 181, no. 1, Genetics Society of America, 2009, pp. 225–34, doi:10.1534/genetics.107.085225.
short: J.P. Bollback, J. Huelsenbeck, Genetics 181 (2009) 225–234.
date_created: 2018-12-11T12:08:26Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:22Z
day: '01'
doi: 10.1534/genetics.107.085225
extern: 1
intvolume: ' 181'
issue: '1'
month: '01'
page: 225 - 234
publication: Genetics
publication_status: published
publisher: Genetics Society of America
publist_id: '1101'
quality_controlled: 0
status: public
title: Parallel genetic evolution within and between bacteriophage species of varying
degrees of divergence
type: journal_article
volume: 181
year: '2009'
...
---
_id: '4360'
abstract:
- lang: eng
text: 'Motivated by applications in software verification, we explore automated
reasoning about the non-disjoint combination of theories of infinitely many finite
structures, where the theories share set variables and set operations. We prove
a combination theorem and apply it to show the decidability of the satisfiability
problem for a class of formulas obtained by applying propositional connectives
to formulas belonging to: 1) Boolean Algebra with Presburger Arithmetic (with
quantifiers over sets and integers), 2) weak monadic second-order logic over trees
(with monadic second-order quantifiers), 3) two-variable logic with counting quantifiers
(ranging over elements), 4) the Bernays-Schönfinkel-Ramsey class of first-order
logic with equality (with ∃ * ∀ * quantifier prefix), and 5) the quantifier-free
logic of multisets with cardinality constraints.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Ruzica
full_name: Piskac, Ruzica
last_name: Piskac
- first_name: Viktor
full_name: Kuncak, Viktor
last_name: Kuncak
citation:
ama: 'Wies T, Piskac R, Kuncak V. Combining theories with shared set operations.
In: 7th International Symposium on Frontiers of Combining Systems. Vol
5749. Springer; 2009:366-382. doi:10.1007/978-3-642-04222-5_23'
apa: 'Wies, T., Piskac, R., & Kuncak, V. (2009). Combining theories with shared
set operations. In 7th International Symposium on Frontiers of Combining Systems
(Vol. 5749, pp. 366–382). Trento, Italy: Springer. https://doi.org/10.1007/978-3-642-04222-5_23'
chicago: Wies, Thomas, Ruzica Piskac, and Viktor Kuncak. “Combining Theories with
Shared Set Operations.” In 7th International Symposium on Frontiers of Combining
Systems, 5749:366–82. Springer, 2009. https://doi.org/10.1007/978-3-642-04222-5_23.
ieee: T. Wies, R. Piskac, and V. Kuncak, “Combining theories with shared set operations,”
in 7th International Symposium on Frontiers of Combining Systems, Trento,
Italy, 2009, vol. 5749, pp. 366–382.
ista: 'Wies T, Piskac R, Kuncak V. 2009. Combining theories with shared set operations.
7th International Symposium on Frontiers of Combining Systems. FroCoS: Frontiers
of Combining Systems, LNCS, vol. 5749, 366–382.'
mla: Wies, Thomas, et al. “Combining Theories with Shared Set Operations.” 7th
International Symposium on Frontiers of Combining Systems, vol. 5749, Springer,
2009, pp. 366–82, doi:10.1007/978-3-642-04222-5_23.
short: T. Wies, R. Piskac, V. Kuncak, in:, 7th International Symposium on Frontiers
of Combining Systems, Springer, 2009, pp. 366–382.
conference:
end_date: 2009-09-18
location: Trento, Italy
name: 'FroCoS: Frontiers of Combining Systems'
start_date: 2009-09-16
date_created: 2018-12-11T12:08:27Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2025-07-02T06:21:09Z
day: '01'
doi: 10.1007/978-3-642-04222-5_23
extern: '1'
intvolume: ' 5749'
language:
- iso: eng
month: '01'
oa_version: None
page: 366 - 382
publication: 7th International Symposium on Frontiers of Combining Systems
publication_status: published
publisher: Springer
publist_id: '1098'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Combining theories with shared set operations
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5749
year: '2009'
...
---
_id: '4363'
author:
- first_name: Vasu
full_name: Vasu Singh
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: Singh V. Formalizing and Verifying Transactional Memories. Formalizing and
Verifying Transactional Memories. 2009.
apa: Singh, V. (2009). Formalizing and Verifying Transactional Memories.
Formalizing and Verifying Transactional Memories. EPFL Lausanne.
chicago: Singh, Vasu. “Formalizing and Verifying Transactional Memories.” Formalizing
and Verifying Transactional Memories. EPFL Lausanne, 2009.
ieee: V. Singh, “Formalizing and Verifying Transactional Memories,” EPFL Lausanne,
2009.
ista: Singh V. 2009. Formalizing and Verifying Transactional Memories. EPFL Lausanne.
mla: Singh, Vasu. “Formalizing and Verifying Transactional Memories.” Formalizing
and Verifying Transactional Memories, EPFL Lausanne, 2009.
short: V. Singh, Formalizing and Verifying Transactional Memories, EPFL Lausanne,
2009.
date_created: 2018-12-11T12:08:28Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:25Z
day: '01'
extern: 1
month: '01'
publication: Formalizing and Verifying Transactional Memories
publication_status: published
publisher: EPFL Lausanne
publist_id: '1095'
quality_controlled: 0
status: public
title: Formalizing and Verifying Transactional Memories
type: dissertation
year: '2009'
...
---
_id: '4365'
abstract:
- lang: eng
text: We present an abstraction refinement technique for the verification of universally
quantified array assertions such as “all elements in the array are sorted”. Our
technique can be seamlessly combined with existing software model checking algorithms.
We implemented our technique in the ACSAR software model checker and successfully
verified quantified array assertions for both text book examples and real-life
examples taken from the Linux operating system kernel.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Mohamed
full_name: Seghir, Mohamed
last_name: Seghir
- first_name: Andreas
full_name: Podelski, Andreas
last_name: Podelski
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
citation:
ama: 'Seghir M, Podelski A, Wies T. Abstraction refinement for quantified array
assertions. In: 16th International Symposium on Static Analysis. Vol 5673.
Springer; 2009:3-18. doi:10.1007/978-3-642-03237-0_3'
apa: 'Seghir, M., Podelski, A., & Wies, T. (2009). Abstraction refinement for
quantified array assertions. In 16th International Symposium on Static Analysis
(Vol. 5673, pp. 3–18). Los Angeles, CA, United States: Springer. https://doi.org/10.1007/978-3-642-03237-0_3'
chicago: Seghir, Mohamed, Andreas Podelski, and Thomas Wies. “Abstraction Refinement
for Quantified Array Assertions.” In 16th International Symposium on Static
Analysis, 5673:3–18. Springer, 2009. https://doi.org/10.1007/978-3-642-03237-0_3.
ieee: M. Seghir, A. Podelski, and T. Wies, “Abstraction refinement for quantified
array assertions,” in 16th International Symposium on Static Analysis,
Los Angeles, CA, United States, 2009, vol. 5673, pp. 3–18.
ista: 'Seghir M, Podelski A, Wies T. 2009. Abstraction refinement for quantified
array assertions. 16th International Symposium on Static Analysis. SAS: Static
Analysis Symposium, LNCS, vol. 5673, 3–18.'
mla: Seghir, Mohamed, et al. “Abstraction Refinement for Quantified Array Assertions.”
16th International Symposium on Static Analysis, vol. 5673, Springer, 2009,
pp. 3–18, doi:10.1007/978-3-642-03237-0_3.
short: M. Seghir, A. Podelski, T. Wies, in:, 16th International Symposium on Static
Analysis, Springer, 2009, pp. 3–18.
conference:
end_date: 2009-08-11
location: Los Angeles, CA, United States
name: 'SAS: Static Analysis Symposium'
start_date: 2009-08-09
date_created: 2018-12-11T12:08:29Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2025-07-02T06:45:01Z
day: '01'
doi: 10.1007/978-3-642-03237-0_3
extern: '1'
intvolume: ' 5673'
language:
- iso: eng
month: '01'
oa_version: None
page: 3 - 18
publication: 16th International Symposium on Static Analysis
publication_status: published
publisher: Springer
publist_id: '1094'
status: public
title: Abstraction refinement for quantified array assertions
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5673
year: '2009'
...
---
_id: '4375'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Shuvendu
full_name: Lahiri, Shuvendu
last_name: Lahiri
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
- first_name: Juan
full_name: Galeotti, Juan
last_name: Galeotti
- first_name: Jan
full_name: Voung, Jan
last_name: Voung
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
citation:
ama: 'Lahiri S, Qadeer S, Galeotti J, Voung J, Wies T. Intra-module inference. In:
21st International Conference on Computer Aided Verification. Vol 5643.
Springer; 2009:493-508. doi:10.1007/978-3-642-02658-4_37'
apa: 'Lahiri, S., Qadeer, S., Galeotti, J., Voung, J., & Wies, T. (2009). Intra-module
inference. In 21st International Conference on Computer Aided Verification
(Vol. 5643, pp. 493–508). Grenoble, France: Springer. https://doi.org/10.1007/978-3-642-02658-4_37'
chicago: Lahiri, Shuvendu, Shaz Qadeer, Juan Galeotti, Jan Voung, and Thomas Wies.
“Intra-Module Inference.” In 21st International Conference on Computer Aided
Verification, 5643:493–508. Springer, 2009. https://doi.org/10.1007/978-3-642-02658-4_37.
ieee: S. Lahiri, S. Qadeer, J. Galeotti, J. Voung, and T. Wies, “Intra-module inference,”
in 21st International Conference on Computer Aided Verification, Grenoble,
France, 2009, vol. 5643, pp. 493–508.
ista: 'Lahiri S, Qadeer S, Galeotti J, Voung J, Wies T. 2009. Intra-module inference.
21st International Conference on Computer Aided Verification. CAV: Computer Aided
Verification, LNCS, vol. 5643, 493–508.'
mla: Lahiri, Shuvendu, et al. “Intra-Module Inference.” 21st International Conference
on Computer Aided Verification, vol. 5643, Springer, 2009, pp. 493–508, doi:10.1007/978-3-642-02658-4_37.
short: S. Lahiri, S. Qadeer, J. Galeotti, J. Voung, T. Wies, in:, 21st International
Conference on Computer Aided Verification, Springer, 2009, pp. 493–508.
conference:
end_date: 2009-07-02
location: Grenoble, France
name: 'CAV: Computer Aided Verification'
start_date: 2009-06-26
date_created: 2018-12-11T12:08:32Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2025-07-02T06:41:41Z
day: '01'
doi: 10.1007/978-3-642-02658-4_37
extern: '1'
intvolume: ' 5643'
language:
- iso: eng
month: '01'
oa_version: None
page: 493 - 508
publication: 21st International Conference on Computer Aided Verification
publication_identifier:
eisbn:
- 978-3-642-02658-4
publication_status: published
publisher: Springer
publist_id: '1082'
status: public
title: Intra-module inference
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5643
year: '2009'
...
---
_id: '4376'
abstract:
- lang: eng
text: "We present Chorus, a high-level parallel programming model suitable for irregular,
heap-manipulating applications like mesh refinement and epidemic simulations,
and JChorus, an implementation of the model on top of Java. One goal of Chorus
is to express the dynamic and instance-dependent patterns of memory access that
are common in typical irregular applications. Its other focus is locality of effects:
the property that in many of the same applications, typical imperative commands
only affect small, local regions in the shared heap.\r\nChorus addresses dynamism
and locality through the unifying abstraction of an object assembly: a local region
in a shared data structure equipped with a short-lived, speculative thread of
control. The thread of control in an assembly can only access objects within the
assembly. While objects can migrate from assembly to assembly, such migration
is local--i.e., objects only move from one assembly to a neighboring one--and
does not lead to aliasing. Programming primitives include a merge operation, by
which an assembly merges with an adjacent assembly, and a split operation, which
splits an assembly into smaller ones. Our abstractions are race and deadlock-free,
and inherently data-centric.\r\nWe demonstrate that Chorus and JChorus allow natural
programming of several important applications exhibiting irregular data-parallelism.
We also present an implementation of JChorus based on a many-to-one mapping of
assemblies to lower-level threads, and report on preliminary performance numbers."
article_processing_charge: No
author:
- first_name: Roberto
full_name: Lublinerman, Roberto
last_name: Lublinerman
- first_name: Swarat
full_name: Chaudhuri, Swarat
last_name: Chaudhuri
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
citation:
ama: Lublinerman R, Chaudhuri S, Cerny P. Parallel programming with object assemblies.
ACM SIGPLAN Notices. 2009;44(10):61-80. doi:10.1145/1639949.164009
apa: Lublinerman, R., Chaudhuri, S., & Cerny, P. (2009). Parallel programming
with object assemblies. ACM SIGPLAN Notices. ACM. https://doi.org/10.1145/1639949.164009
chicago: Lublinerman, Roberto, Swarat Chaudhuri, and Pavol Cerny. “Parallel Programming
with Object Assemblies.” ACM SIGPLAN Notices. ACM, 2009. https://doi.org/10.1145/1639949.164009.
ieee: R. Lublinerman, S. Chaudhuri, and P. Cerny, “Parallel programming with object
assemblies,” ACM SIGPLAN Notices, vol. 44, no. 10. ACM, pp. 61–80, 2009.
ista: Lublinerman R, Chaudhuri S, Cerny P. 2009. Parallel programming with object
assemblies. ACM SIGPLAN Notices. 44(10), 61–80.
mla: Lublinerman, Roberto, et al. “Parallel Programming with Object Assemblies.”
ACM SIGPLAN Notices, vol. 44, no. 10, ACM, 2009, pp. 61–80, doi:10.1145/1639949.164009.
short: R. Lublinerman, S. Chaudhuri, P. Cerny, ACM SIGPLAN Notices 44 (2009) 61–80.
date_created: 2018-12-11T12:08:32Z
date_published: 2009-10-25T00:00:00Z
date_updated: 2025-07-02T06:17:51Z
day: '25'
doi: 10.1145/1639949.164009
extern: '1'
intvolume: ' 44'
issue: '10'
language:
- iso: eng
month: '10'
oa_version: None
page: 61 - 80
publication: ACM SIGPLAN Notices
publication_status: published
publisher: ACM
publist_id: '1083'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Parallel programming with object assemblies
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 44
year: '2009'
...
---
_id: '4377'
abstract:
- lang: eng
text: Programming errors found early are the cheapest. Tools applying to the early
stage of code development exist but either they suffer from false positives (“noise”)
or they require strong user interaction. We propose to avoid this deficiency by
defining a new class of errors. A program fragment is doomed if its execution
will inevitably fail, in whatever state it is started. We use a formal verification
method to identify such errors fully automatically and, most significantly, without
producing noise. We report on preliminary experiments with a prototype tool.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Jochen
full_name: Hoenicke, Jochen
last_name: Hoenicke
- first_name: K Rustan
full_name: Leino, K Rustan
last_name: Leino
- first_name: Andreas
full_name: Podelski, Andreas
last_name: Podelski
- first_name: Martin
full_name: Schäf, Martin
last_name: Schäf
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
citation:
ama: 'Hoenicke J, Leino KR, Podelski A, Schäf M, Wies T. It’s doomed; we can prove
it. In: Second World Congress on Formal Methods. Vol 5850. Springer; 2009:338-353.
doi:10.1007/978-3-642-05089-3_22'
apa: 'Hoenicke, J., Leino, K. R., Podelski, A., Schäf, M., & Wies, T. (2009).
It’s doomed; we can prove it. In Second World Congress on Formal Methods
(Vol. 5850, pp. 338–353). Eindhoven, The Netherlands: Springer. https://doi.org/10.1007/978-3-642-05089-3_22'
chicago: Hoenicke, Jochen, K Rustan Leino, Andreas Podelski, Martin Schäf, and Thomas
Wies. “It’s Doomed; We Can Prove It.” In Second World Congress on Formal Methods,
5850:338–53. Springer, 2009. https://doi.org/10.1007/978-3-642-05089-3_22.
ieee: J. Hoenicke, K. R. Leino, A. Podelski, M. Schäf, and T. Wies, “It’s doomed;
we can prove it,” in Second World Congress on Formal Methods, Eindhoven,
The Netherlands, 2009, vol. 5850, pp. 338–353.
ista: 'Hoenicke J, Leino KR, Podelski A, Schäf M, Wies T. 2009. It’s doomed; we
can prove it. Second World Congress on Formal Methods. FM: Formal Methods, LNCS,
vol. 5850, 338–353.'
mla: Hoenicke, Jochen, et al. “It’s Doomed; We Can Prove It.” Second World Congress
on Formal Methods, vol. 5850, Springer, 2009, pp. 338–53, doi:10.1007/978-3-642-05089-3_22.
short: J. Hoenicke, K.R. Leino, A. Podelski, M. Schäf, T. Wies, in:, Second World
Congress on Formal Methods, Springer, 2009, pp. 338–353.
conference:
end_date: 2009-11-06
location: Eindhoven, The Netherlands
name: 'FM: Formal Methods'
start_date: 2009-11-02
date_created: 2018-12-11T12:08:32Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2025-07-02T06:38:22Z
day: '01'
doi: 10.1007/978-3-642-05089-3_22
extern: '1'
intvolume: ' 5850'
language:
- iso: eng
month: '01'
oa_version: None
page: 338 - 353
publication: Second World Congress on Formal Methods
publication_status: published
publisher: Springer
publist_id: '1079'
quality_controlled: '1'
scopus_import: '1'
status: public
title: It's doomed; we can prove it
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5850
year: '2009'
...
---
_id: '4383'
abstract:
- lang: eng
text: Pseudo-code descriptions of STMs assume sequentially consistent program execution
and atomicity of high-level STM operations like read, write, and commit. These
assumptions are often violated in realistic settings, as STM implementations run
on relaxed memory models, with the atomicity of operations as provided by the
hardware. This paper presents the first approach to verify STMs under relaxed
memory models with atomicity of 32 bit loads and stores, and read-modify-write
operations. We present RML, a new high-level language for expressing concurrent
algorithms with a hardware-level atomicity of instructions, and whose semantics
is parametrized by various relaxed memory models. We then present our tool, FOIL,
which takes as input the RML description of an STM algorithm and the description
of a memory model, and automatically determines the locations of fences, which
if inserted, ensure the correctness of the STM algorithm under the given memory
model. We use FOIL to verify DSTM, TL2, and McRT STM under the memory models of
sequential consistency, total store order, partial store order, and relaxed memory
order.
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. Software transactional memory on relaxed
memory models. In: Vol 5643. Springer; 2009:321-336. doi:10.1007/978-3-642-02658-4_26'
apa: 'Guerraoui, R., Henzinger, T. A., & Singh, V. (2009). Software transactional
memory on relaxed memory models (Vol. 5643, pp. 321–336). Presented at the CAV:
Computer Aided Verification, Springer. https://doi.org/10.1007/978-3-642-02658-4_26'
chicago: Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Software Transactional
Memory on Relaxed Memory Models,” 5643:321–36. Springer, 2009. https://doi.org/10.1007/978-3-642-02658-4_26.
ieee: 'R. Guerraoui, T. A. Henzinger, and V. Singh, “Software transactional memory
on relaxed memory models,” presented at the CAV: Computer Aided Verification,
2009, vol. 5643, pp. 321–336.'
ista: 'Guerraoui R, Henzinger TA, Singh V. 2009. Software transactional memory on
relaxed memory models. CAV: Computer Aided Verification, LNCS, vol. 5643, 321–336.'
mla: Guerraoui, Rachid, et al. Software Transactional Memory on Relaxed Memory
Models. Vol. 5643, Springer, 2009, pp. 321–36, doi:10.1007/978-3-642-02658-4_26.
short: R. Guerraoui, T.A. Henzinger, V. Singh, in:, Springer, 2009, pp. 321–336.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:34Z
date_published: 2009-06-19T00:00:00Z
date_updated: 2021-01-12T07:56:34Z
day: '19'
doi: 10.1007/978-3-642-02658-4_26
extern: 1
file:
- access_level: open_access
checksum: df3c3e6306afd3f630a9146f91642f0a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:50Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5105'
file_name: IST-2012-45-v1+1_Software_transactional_memory_on_relaxed_memory_models.pdf
file_size: 265763
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
intvolume: ' 5643'
month: '06'
oa: 1
page: 321 - 336
publication_status: published
publisher: Springer
publist_id: '1074'
pubrep_id: '45'
quality_controlled: 0
status: public
title: Software transactional memory on relaxed memory models
type: conference
volume: 5643
year: '2009'
...
---
_id: '4385'
abstract:
- lang: eng
text: "Transactional memories are typically speculative and rely on contention managers
to cure conflicts. This paper explores a complementary approach that prevents
conflicts by scheduling transactions according to predictions on their access
sets.\r\nWe first explore the theoretical boundaries of this approach and prove
that (1) a TM scheduler with an accurate prediction can be 2-competitive with
an optimal offline TM scheduler, but (2) even a slight inaccuracy in prediction
makes the competitive ratio of the TM scheduler in the order of the number of
transactions.\r\nWe then show that, in practice, there is room for a pragmatic
approach with good average case performance. We present Shrink, a scheduler that
(1) bases its prediction of transactional accesses on the access patterns of the
past transactions from the same thread, and (2) uses a novel heuristic, which
we call serialization affinity, to schedule transactions with a probability proportional
to the current amount of contention. Shrink obtains roughly 70% accurate read
and write access predictions on STMBench7 and STAMP. In our experimental evaluation,
Shrink significantly improves STM performance in cases the number of executing
threads is higher than the number of available CPU cores. For SwissTM, Shrink
improves the performance by up to 55% on STMBench7, and up to 120% on STAMP. For
TinySTM, Shrink drastically improves the performance on STMBench7 and STAMP benchmarks."
article_processing_charge: No
author:
- first_name: Aleksandar
full_name: Dragojevic, Aleksandar
last_name: Dragojevic
- first_name: Rachid
full_name: Guerraoui, Rachid
last_name: Guerraoui
- first_name: Anmol
full_name: Singh, Anmol
last_name: Singh
- first_name: Vasu
full_name: Singh, Vasu
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: 'Dragojevic A, Guerraoui R, Singh A, Singh V. Preventing versus curing: Avoiding
conflicts in transactional memories. In: Proceedings of the 28th ACM Symposium
on Principles of Distributed Computing. ACM; 2009:7-16. doi:10.1145/1582716.1582725'
apa: 'Dragojevic, A., Guerraoui, R., Singh, A., & Singh, V. (2009). Preventing
versus curing: Avoiding conflicts in transactional memories. In Proceedings
of the 28th ACM symposium on Principles of distributed computing (pp. 7–16).
Calgary, Canada: ACM. https://doi.org/10.1145/1582716.1582725'
chicago: 'Dragojevic, Aleksandar, Rachid Guerraoui, Anmol Singh, and Vasu Singh.
“Preventing versus Curing: Avoiding Conflicts in Transactional Memories.” In Proceedings
of the 28th ACM Symposium on Principles of Distributed Computing, 7–16. ACM,
2009. https://doi.org/10.1145/1582716.1582725.'
ieee: 'A. Dragojevic, R. Guerraoui, A. Singh, and V. Singh, “Preventing versus curing:
Avoiding conflicts in transactional memories,” in Proceedings of the 28th ACM
symposium on Principles of distributed computing, Calgary, Canada, 2009, pp.
7–16.'
ista: 'Dragojevic A, Guerraoui R, Singh A, Singh V. 2009. Preventing versus curing:
Avoiding conflicts in transactional memories. Proceedings of the 28th ACM symposium
on Principles of distributed computing. POPL: Principles of Programming Languages,
7–16.'
mla: 'Dragojevic, Aleksandar, et al. “Preventing versus Curing: Avoiding Conflicts
in Transactional Memories.” Proceedings of the 28th ACM Symposium on Principles
of Distributed Computing, ACM, 2009, pp. 7–16, doi:10.1145/1582716.1582725.'
short: A. Dragojevic, R. Guerraoui, A. Singh, V. Singh, in:, Proceedings of the
28th ACM Symposium on Principles of Distributed Computing, ACM, 2009, pp. 7–16.
conference:
end_date: 2009-08-12
location: Calgary, Canada
name: 'POPL: Principles of Programming Languages'
start_date: 2009-08-10
date_created: 2018-12-11T12:08:35Z
date_published: 2009-08-10T00:00:00Z
date_updated: 2025-07-02T06:35:49Z
day: '10'
doi: 10.1145/1582716.1582725
extern: '1'
language:
- iso: eng
month: '08'
oa_version: None
page: 7 - 16
publication: Proceedings of the 28th ACM symposium on Principles of distributed computing
publication_status: published
publisher: ACM
publist_id: '1070'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Preventing versus curing: Avoiding conflicts in transactional memories'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2009'
...
---
_id: '4391'
abstract:
- lang: eng
text: We address the problem of analyzing programs such as J2ME midlets for mobile
devices, where a central correctness requirement concerns confidentiality of data
that the user wants to keep secret. Existing software model checking tools analyze
individual program executions, and are not applicable to checking confidentiality
properties that require reasoning about equivalence among executions. We develop
an automated analysis technique for such properties. We show that both over- and
under- approximation is needed for sound analysis. Given a program and a confidentiality
requirement, our technique produces a formula that is satisfiable if the requirement
holds. We evaluate the approach by analyzing bytecode of a set of Java (J2ME)
methods.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
citation:
ama: 'Cerny P, Alur R. Automated analysis of Java methods for confidentiality. In:
21st International Conference on Computer Aided Verification. Vol 5643.
Springer; 2009:173-187. doi:10.1007/978-3-642-02658-4_16'
apa: Cerny, P., & Alur, R. (2009). Automated analysis of Java methods for confidentiality.
In 21st International Conference on Computer Aided Verification (Vol. 5643,
pp. 173–187). Springer. https://doi.org/10.1007/978-3-642-02658-4_16
chicago: Cerny, Pavol, and Rajeev Alur. “Automated Analysis of Java Methods for
Confidentiality.” In 21st International Conference on Computer Aided Verification,
5643:173–87. Springer, 2009. https://doi.org/10.1007/978-3-642-02658-4_16.
ieee: P. Cerny and R. Alur, “Automated analysis of Java methods for confidentiality,”
in 21st International Conference on Computer Aided Verification, 2009,
vol. 5643, pp. 173–187.
ista: 'Cerny P, Alur R. 2009. Automated analysis of Java methods for confidentiality.
21st International Conference on Computer Aided Verification. CAV: Computer Aided
Verification, LNCS, vol. 5643, 173–187.'
mla: Cerny, Pavol, and Rajeev Alur. “Automated Analysis of Java Methods for Confidentiality.”
21st International Conference on Computer Aided Verification, vol. 5643,
Springer, 2009, pp. 173–87, doi:10.1007/978-3-642-02658-4_16.
short: P. Cerny, R. Alur, in:, 21st International Conference on Computer Aided Verification,
Springer, 2009, pp. 173–187.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:36Z
date_published: 2009-07-01T00:00:00Z
date_updated: 2025-07-02T06:32:32Z
day: '01'
doi: 10.1007/978-3-642-02658-4_16
extern: '1'
intvolume: ' 5643'
language:
- iso: eng
month: '07'
oa_version: None
page: 173 - 187
publication: 21st International Conference on Computer Aided Verification
publication_status: published
publisher: Springer
publist_id: '1067'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Automated analysis of Java methods for confidentiality
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5643
year: '2009'
...
---
_id: '4403'
abstract:
- lang: eng
text: For programs whose data variables range over boolean or finite domains, program
verification is decidable, and this forms the basis of recent tools for software
model checking. In this paper, we consider algorithmic verification of programs
that use boolean variables, and in addition, access a single read-only array whose
length is potentially unbounded, and whose elements range over a potentially unbounded
data domain. We show that the reachability problem, while undecidable in general,
is (1) Pspace-complete for programs in which the array-accessing for-loops are
not nested, (2) decidable for a restricted class of programs with doubly-nested
loops. The second result establishes connections to automata and logics defining
languages over data words.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Scott
full_name: Weinstein, Scott
last_name: Weinstein
citation:
ama: 'Alur R, Cerny P, Weinstein S. Algorithmic analysis of array-accessing programs.
In: Vol 5771. Springer; 2009:86-101. doi:10.1007/978-3-642-04027-6_9'
apa: 'Alur, R., Cerny, P., & Weinstein, S. (2009). Algorithmic analysis of array-accessing
programs (Vol. 5771, pp. 86–101). Presented at the CSL: Computer Science Logic,
Coimbra, Portugal: Springer. https://doi.org/10.1007/978-3-642-04027-6_9'
chicago: Alur, Rajeev, Pavol Cerny, and Scott Weinstein. “Algorithmic Analysis of
Array-Accessing Programs,” 5771:86–101. Springer, 2009. https://doi.org/10.1007/978-3-642-04027-6_9.
ieee: 'R. Alur, P. Cerny, and S. Weinstein, “Algorithmic analysis of array-accessing
programs,” presented at the CSL: Computer Science Logic, Coimbra, Portugal, 2009,
vol. 5771, pp. 86–101.'
ista: 'Alur R, Cerny P, Weinstein S. 2009. Algorithmic analysis of array-accessing
programs. CSL: Computer Science Logic, LNCS, vol. 5771, 86–101.'
mla: Alur, Rajeev, et al. Algorithmic Analysis of Array-Accessing Programs.
Vol. 5771, Springer, 2009, pp. 86–101, doi:10.1007/978-3-642-04027-6_9.
short: R. Alur, P. Cerny, S. Weinstein, in:, Springer, 2009, pp. 86–101.
conference:
end_date: 2009-09-11
location: Coimbra, Portugal
name: 'CSL: Computer Science Logic'
start_date: 2009-09-07
date_created: 2018-12-11T12:08:40Z
date_published: 2009-09-01T00:00:00Z
date_updated: 2025-09-30T08:04:32Z
day: '01'
doi: 10.1007/978-3-642-04027-6_9
extern: '1'
intvolume: ' 5771'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://repository.upenn.edu/cis_reports/894/
month: '09'
oa: 1
oa_version: Submitted Version
page: 86 - 101
publication_status: published
publisher: Springer
publist_id: '1056'
quality_controlled: '1'
related_material:
record:
- id: '2967'
relation: later_version
status: public
status: public
title: Algorithmic analysis of array-accessing programs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5771
year: '2009'
...
---
_id: '4453'
abstract:
- lang: eng
text: We present an on-the-fly abstraction technique for infinite-state continuous
-time Markov chains. We consider Markov chains that are specified by a finite
set of transition classes. Such models naturally represent biochemical reactions
and therefore play an important role in the stochastic modeling of biological
systems. We approximate the transient probability distributions at various time
instances by solving a sequence of dynamically constructed abstract models, each
depending on the previous one. Each abstract model is a finite Markov chain that
represents the behavior of the original, infinite chain during a specific time
interval. Our approach provides complete information about probability distributions,
not just about individual parameters like the mean. The error of each abstraction
can be computed, and the precision of the abstraction refined when desired. We
implemented the algorithm and demonstrate its usefulness and efficiency on several
case studies from systems biology.
acknowledgement: The research has been partially funded by the Swiss National Science
Foundation under grant 205321-111840.
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: Maria
full_name: Maria Mateescu
id: 3B43276C-F248-11E8-B48F-1D18A9856A87
last_name: Mateescu
- first_name: Verena
full_name: Wolf, Verena
last_name: Wolf
citation:
ama: 'Henzinger TA, Mateescu M, Wolf V. Sliding-window abstraction for infinite
Markov chains. In: Vol 5643. Springer; 2009:337-352. doi:10.1007/978-3-642-02658-4_27'
apa: 'Henzinger, T. A., Mateescu, M., & Wolf, V. (2009). Sliding-window abstraction
for infinite Markov chains (Vol. 5643, pp. 337–352). Presented at the CAV: Computer
Aided Verification, Springer. https://doi.org/10.1007/978-3-642-02658-4_27'
chicago: Henzinger, Thomas A, Maria Mateescu, and Verena Wolf. “Sliding-Window Abstraction
for Infinite Markov Chains,” 5643:337–52. Springer, 2009. https://doi.org/10.1007/978-3-642-02658-4_27.
ieee: 'T. A. Henzinger, M. Mateescu, and V. Wolf, “Sliding-window abstraction for
infinite Markov chains,” presented at the CAV: Computer Aided Verification, 2009,
vol. 5643, pp. 337–352.'
ista: 'Henzinger TA, Mateescu M, Wolf V. 2009. Sliding-window abstraction for infinite
Markov chains. CAV: Computer Aided Verification, LNCS, vol. 5643, 337–352.'
mla: Henzinger, Thomas A., et al. Sliding-Window Abstraction for Infinite Markov
Chains. Vol. 5643, Springer, 2009, pp. 337–52, doi:10.1007/978-3-642-02658-4_27.
short: T.A. Henzinger, M. Mateescu, V. Wolf, in:, Springer, 2009, pp. 337–352.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:55Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2021-01-12T07:57:04Z
day: '01'
doi: 10.1007/978-3-642-02658-4_27
extern: 1
file:
- access_level: open_access
checksum: 36b974111521ea534aae294166e93a63
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:20Z
date_updated: 2020-07-14T12:46:30Z
file_id: '4938'
file_name: IST-2012-40-v1+1_Sliding-window_abstraction_for_infinite_markov_chains.pdf
file_size: 804295
relation: main_file
file_date_updated: 2020-07-14T12:46:30Z
intvolume: ' 5643'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/sliding-window_abstraction_for_infinite_markov_chains.pdf
month: '01'
oa: 1
page: 337 - 352
publication_status: published
publisher: Springer
publist_id: '278'
pubrep_id: '40'
quality_controlled: 0
status: public
title: Sliding-window abstraction for infinite Markov chains
type: conference
volume: 5643
year: '2009'
...
---
_id: '4535'
abstract:
- lang: eng
text: |-
Molecular noise, which arises from the randomness of the discrete events in the cell, significantly influences fundamental biological processes. Discrete -state continuous-time stochastic models (CTMC) can be used to describe such effects, but the calculation of the probabilities of certain events is computationally expensive.
We present a comparison of two analysis approaches for CTMC. On one hand, we estimate the probabilities of interest using repeated Gillespie simulation and determine the statistical accuracy that we obtain. On the other hand, we apply a numerical reachability analysis that approximates the probability distributions of the system at several time instances. We use examples of cellular processes to demonstrate the superiority of the reachability analysis if accurate results are required.
acknowledgement: This research was supported in part by the Swiss National Science
Foundation under grant 205321-111840 and by the Excellence Cluster on Multimodal
Computing and Interaction.
alternative_title:
- LNCS
author:
- first_name: Frédéric
full_name: Didier, Frédéric
last_name: Didier
- 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: Verena
full_name: Wolf, Verena
last_name: Wolf
citation:
ama: 'Didier F, Henzinger TA, Mateescu M, Wolf V. Approximation of event probabilities
in noisy cellular processes. In: Vol 5688. Springer; 2009:173-188. doi:10.1007/978-3-642-03845-7_12'
apa: 'Didier, F., Henzinger, T. A., Mateescu, M., & Wolf, V. (2009). Approximation
of event probabilities in noisy cellular processes (Vol. 5688, pp. 173–188). Presented
at the CMSB: Computational Methods in Systems Biology, Springer. https://doi.org/10.1007/978-3-642-03845-7_12'
chicago: Didier, Frédéric, Thomas A Henzinger, Maria Mateescu, and Verena Wolf.
“Approximation of Event Probabilities in Noisy Cellular Processes,” 5688:173–88.
Springer, 2009. https://doi.org/10.1007/978-3-642-03845-7_12.
ieee: 'F. Didier, T. A. Henzinger, M. Mateescu, and V. Wolf, “Approximation of event
probabilities in noisy cellular processes,” presented at the CMSB: Computational
Methods in Systems Biology, 2009, vol. 5688, pp. 173–188.'
ista: 'Didier F, Henzinger TA, Mateescu M, Wolf V. 2009. Approximation of event
probabilities in noisy cellular processes. CMSB: Computational Methods in Systems
Biology, LNCS, vol. 5688, 173–188.'
mla: Didier, Frédéric, et al. Approximation of Event Probabilities in Noisy Cellular
Processes. Vol. 5688, Springer, 2009, pp. 173–88, doi:10.1007/978-3-642-03845-7_12.
short: F. Didier, T.A. Henzinger, M. Mateescu, V. Wolf, in:, Springer, 2009, pp.
173–188.
conference:
name: 'CMSB: Computational Methods in Systems Biology'
date_created: 2018-12-11T12:09:21Z
date_published: 2009-08-17T00:00:00Z
date_updated: 2025-09-30T09:03:30Z
day: '17'
doi: 10.1007/978-3-642-03845-7_12
extern: 1
intvolume: ' 5688'
month: '08'
page: 173 - 188
publication_status: published
publisher: Springer
publist_id: '189'
quality_controlled: 0
related_material:
record:
- id: '3364'
relation: later_version
status: public
status: public
title: Approximation of event probabilities in noisy cellular processes
type: conference
volume: 5688
year: '2009'
...
---
_id: '4540'
abstract:
- lang: eng
text: Weighted automata are nondeterministic automata with numerical weights on
transitions. They can define quantitative languages L that assign to each word
w a real number L(w). In the case of infinite words, the value of a run is naturally
computed as the maximum, limsup, liminf, limit average, or discounted sum of the
transition weights. We study expressiveness and closure questions about these
quantitative languages. We first show that the set of words with value greater
than a threshold can be non-w-regular for deterministic limit-average and discounted-sum
automata, while this set is always w-regular when the threshold is isolated (i.e.,
some neighborhood around the threshold contains no word). In the latter case,
we prove that the w-regular language is robust against small perturbations of
the transition weights. We next consider automata with transition weights 0 or
1 and show that they are as expressive as general weighted automata in the limit-average
case, but not in the discounted-sum case. Third, for quantitative languages L-1
and L-2, we consider the operations max(L-1, L-2), min(L-1, L-2), and 1-L-1, which
generalize the boolean operations on languages, as well as the sum L-1 + L-2.
We establish the closure properties of all classes of quantitative languages with
respect to these four operations.
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Doyen L, Henzinger TA. Expressiveness and closure properties
for quantitative languages. In: IEEE; 2009:199-208. doi:10.1109/LICS.2009.16'
apa: 'Chatterjee, K., Doyen, L., & Henzinger, T. A. (2009). Expressiveness and
closure properties for quantitative languages (pp. 199–208). Presented at the
LICS: Logic in Computer Science, IEEE. https://doi.org/10.1109/LICS.2009.16'
chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Expressiveness
and Closure Properties for Quantitative Languages,” 199–208. IEEE, 2009. https://doi.org/10.1109/LICS.2009.16.
ieee: 'K. Chatterjee, L. Doyen, and T. A. Henzinger, “Expressiveness and closure
properties for quantitative languages,” presented at the LICS: Logic in Computer
Science, 2009, pp. 199–208.'
ista: 'Chatterjee K, Doyen L, Henzinger TA. 2009. Expressiveness and closure properties
for quantitative languages. LICS: Logic in Computer Science, 199–208.'
mla: Chatterjee, Krishnendu, et al. Expressiveness and Closure Properties for
Quantitative Languages. IEEE, 2009, pp. 199–208, doi:10.1109/LICS.2009.16.
short: K. Chatterjee, L. Doyen, T.A. Henzinger, in:, IEEE, 2009, pp. 199–208.
conference:
name: 'LICS: Logic in Computer Science'
date_created: 2018-12-11T12:09:23Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2025-09-30T09:30:59Z
day: '01'
doi: 10.1109/LICS.2009.16
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 199 - 208
publication_status: published
publisher: IEEE
publist_id: '181'
pubrep_id: '55'
quality_controlled: '1'
related_material:
record:
- id: '3867'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Expressiveness and closure properties for quantitative languages
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2009'
...
---
_id: '4542'
abstract:
- lang: eng
text: "Weighted automata are finite automata with numerical weights on transitions.
Nondeterministic weighted automata define quantitative languages L that assign
to each word w a real number L(w) computed as the maximal value of all runs over
w, and the value of a run r is a function of the sequence of weights that appear
along r. There are several natural functions to consider such as Sup, LimSup,
LimInf, limit average, and discounted sum of transition weights.\r\nWe introduce
alternating weighted automata in which the transitions of the runs are chosen
by two players in a turn-based fashion. Each word is assigned the maximal value
of a run that the first player can enforce regardless of the choices made by the
second player. We survey the results about closure properties, expressiveness,
and decision problems for nondeterministic weighted automata, and we extend these
results to alternating weighted automata.\r\nFor quantitative languages L 1 and
L 2, we consider the pointwise operations max(L 1,L 2), min(L 1,L 2), 1 − L 1,
and the sum L 1 + L 2. We establish the closure properties of all classes of alternating
weighted automata with respect to these four operations.\r\nWe next compare the
expressive power of the various classes of alternating and nondeterministic weighted
automata over infinite words. In particular, for limit average and discounted
sum, we show that alternation brings more expressive power than nondeterminism.\r\nFinally,
we present decidability results and open questions for the quantitative extension
of the classical decision problems in automata theory: emptiness, universality,
language inclusion, and language equivalence."
acknowledgement: This research was supported in part by the Swiss National Science
Foundation under the Indo-Swiss Joint Research Programme, by the European Network
of Excellence on Embedded Systems Design (ArtistDesign), by the European Combest,
Quasimodo, and Gasics projects, by the PAI program Moves funded by the Belgian Federal
Government, and by the CFV (Federated Center in Verification) funded by the F.R.S.-FNRS.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Doyen L, Henzinger TA. Alternating weighted automata. In: Vol
5699. Springer; 2009:3-13. doi:10.1007/978-3-642-03409-1_2'
apa: 'Chatterjee, K., Doyen, L., & Henzinger, T. A. (2009). Alternating weighted
automata (Vol. 5699, pp. 3–13). Presented at the FCT: Fundamentals of Computation
Theory, Wroclaw, Poland: Springer. https://doi.org/10.1007/978-3-642-03409-1_2'
chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Alternating
Weighted Automata,” 5699:3–13. Springer, 2009. https://doi.org/10.1007/978-3-642-03409-1_2.
ieee: 'K. Chatterjee, L. Doyen, and T. A. Henzinger, “Alternating weighted automata,”
presented at the FCT: Fundamentals of Computation Theory, Wroclaw, Poland, 2009,
vol. 5699, pp. 3–13.'
ista: 'Chatterjee K, Doyen L, Henzinger TA. 2009. Alternating weighted automata.
FCT: Fundamentals of Computation Theory, LNCS, vol. 5699, 3–13.'
mla: Chatterjee, Krishnendu, et al. Alternating Weighted Automata. Vol. 5699,
Springer, 2009, pp. 3–13, doi:10.1007/978-3-642-03409-1_2.
short: K. Chatterjee, L. Doyen, T.A. Henzinger, in:, Springer, 2009, pp. 3–13.
conference:
end_date: 2009-09-04
location: Wroclaw, Poland
name: 'FCT: Fundamentals of Computation Theory'
start_date: 2009-09-02
corr_author: '1'
date_created: 2018-12-11T12:09:23Z
date_published: 2009-09-10T00:00:00Z
date_updated: 2024-10-09T20:53:55Z
day: '10'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.1007/978-3-642-03409-1_2
ec_funded: 1
file:
- access_level: open_access
checksum: e8f53abb63579de3f2bff58b2a1188e2
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:09Z
date_updated: 2020-07-14T12:46:31Z
file_id: '5126'
file_name: IST-2012-39-v1+1_Alternating_Weighted_Automata.pdf
file_size: 164428
relation: main_file
file_date_updated: 2020-07-14T12:46:31Z
has_accepted_license: '1'
intvolume: ' 5699'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 3 - 13
project:
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
publication_status: published
publisher: Springer
publist_id: '180'
pubrep_id: '39'
quality_controlled: '1'
scopus_import: 1
status: public
title: Alternating weighted automata
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5699
year: '2009'
...
---
_id: '4543'
abstract:
- lang: eng
text: The synthesis of a reactive system with respect to all omega-regular specification
requires the solution of a graph game. Such games have been extended in two natural
ways. First, a game graph can be equipped with probabilistic choices between alternative
transitions, thus allowing the, modeling of uncertain behaviour. These are called
stochastic games. Second, a liveness specification can he strengthened to require
satisfaction within all unknown but bounded amount of time. These are called finitary
objectives. We study. for the first time, the, combination of Stochastic games
and finitary objectives. We characterize the requirements on optimal strategies
and provide algorithms for Computing the maximal achievable probability of winning
stochastic games with finitary parity or Street, objectives. Most notably the
set of state's from which a player can win with probability . for a finitary parity
objective can he computed in polynomial time even though no polynomial-time algorithm
is known in the nonfinitary case.
acknowledgement: This research was supported in part by the Swiss National Science
Foundation under the Indo-Swiss Joint Research Programme, by the European Network
of Excellence on Embedded Systems Design (ArtistDesign), and by the European project
Combest.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Florian
full_name: Horn, Florian
id: 37327ACE-F248-11E8-B48F-1D18A9856A87
last_name: Horn
citation:
ama: 'Chatterjee K, Henzinger TA, Horn F. Stochastic games with finitary objectives.
In: Vol 5734. Springer; 2009:34-54. doi:10.1007/978-3-642-03816-7_4'
apa: 'Chatterjee, K., Henzinger, T. A., & Horn, F. (2009). Stochastic games
with finitary objectives (Vol. 5734, pp. 34–54). Presented at the MFCS: Mathematical
Foundations of Computer Science, High Tatras, Slovakia: Springer. https://doi.org/10.1007/978-3-642-03816-7_4'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Florian Horn. “Stochastic
Games with Finitary Objectives,” 5734:34–54. Springer, 2009. https://doi.org/10.1007/978-3-642-03816-7_4.
ieee: 'K. Chatterjee, T. A. Henzinger, and F. Horn, “Stochastic games with finitary
objectives,” presented at the MFCS: Mathematical Foundations of Computer Science,
High Tatras, Slovakia, 2009, vol. 5734, pp. 34–54.'
ista: 'Chatterjee K, Henzinger TA, Horn F. 2009. Stochastic games with finitary
objectives. MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 5734,
34–54.'
mla: Chatterjee, Krishnendu, et al. Stochastic Games with Finitary Objectives.
Vol. 5734, Springer, 2009, pp. 34–54, doi:10.1007/978-3-642-03816-7_4.
short: K. Chatterjee, T.A. Henzinger, F. Horn, in:, Springer, 2009, pp. 34–54.
conference:
end_date: 2009-08-28
location: High Tatras, Slovakia
name: 'MFCS: Mathematical Foundations of Computer Science'
start_date: 2009-08-24
corr_author: '1'
date_created: 2018-12-11T12:09:24Z
date_published: 2009-08-01T00:00:00Z
date_updated: 2024-10-09T20:53:54Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-03816-7_4
ec_funded: 1
intvolume: ' 5734'
language:
- iso: eng
month: '08'
oa_version: None
page: 34 - 54
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication_status: published
publisher: Springer
publist_id: '178'
quality_controlled: '1'
scopus_import: 1
status: public
title: Stochastic games with finitary objectives
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5734
year: '2009'
...
---
_id: '4544'
abstract:
- lang: eng
text: We consider concurrent games played on graphs. At every round of a game, each
player simultaneously and independently selects a move; the moves jointly determine
the transition to a successor state. Two basic objectives are the safety objective
to stay forever in a given set of states, and its dual, the reachability objective
to reach a given set of states. We present in this paper a strategy improvement
algorithm for computing the value of a concurrent safety game, that is, the maximal
probability with which player 1 can enforce the safety objective. The algorithm
yields a sequence of player-1 strategies which ensure probabilities of winning
that converge monotonically to the value of the safety game. Our result is significant
because the strategy improvement algorithm provides, for the first time, a way
to approximate the value of a concurrent safety game from below. Since a value
iteration algorithm, or a strategy improvement algorithm for reachability games,
can be used to approximate the same value from above, the combination of both
algorithms yields a method for computing a converging sequence of upper and lower
bounds for the values of concurrent reachability and safety games. Previous methods
could approximate the values of these games only from one direction, and as no
rates of convergence are known, they did not provide a practical way to solve
these games.
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. Termination criteria for solving
concurrent safety and reachability games. In: SIAM; 2009:197-206. doi:10.1137/1.9781611973068.23'
apa: 'Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2009). Termination
criteria for solving concurrent safety and reachability games (pp. 197–206). Presented
at the SODA: Symposium on Discrete Algorithms, SIAM. https://doi.org/10.1137/1.9781611973068.23'
chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Termination
Criteria for Solving Concurrent Safety and Reachability Games,” 197–206. SIAM,
2009. https://doi.org/10.1137/1.9781611973068.23.
ieee: 'K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Termination criteria for
solving concurrent safety and reachability games,” presented at the SODA: Symposium
on Discrete Algorithms, 2009, pp. 197–206.'
ista: 'Chatterjee K, De Alfaro L, Henzinger TA. 2009. Termination criteria for solving
concurrent safety and reachability games. SODA: Symposium on Discrete Algorithms,
197–206.'
mla: Chatterjee, Krishnendu, et al. Termination Criteria for Solving Concurrent
Safety and Reachability Games. SIAM, 2009, pp. 197–206, doi:10.1137/1.9781611973068.23.
short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, SIAM, 2009, pp. 197–206.
conference:
name: 'SODA: Symposium on Discrete Algorithms'
date_created: 2018-12-11T12:09:24Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:35Z
day: '01'
doi: 10.1137/1.9781611973068.23
extern: 1
file:
- access_level: open_access
checksum: ce7dc1667502e26b23c07a767ac41ae6
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:03Z
date_updated: 2020-07-14T12:46:31Z
file_id: '4662'
file_name: IST-2012-37-v1+1_Termination_criteria_for_solving_concurrent_safety_and_reachability_games.pdf
file_size: 212369
relation: main_file
file_date_updated: 2020-07-14T12:46:31Z
main_file_link:
- open_access: '1'
url: https://repository.ist.ac.at/id/eprint/37
month: '01'
oa: 1
page: 197 - 206
publication_status: published
publisher: SIAM
publist_id: '176'
pubrep_id: '37'
quality_controlled: 0
status: public
title: Termination criteria for solving concurrent safety and reachability games
type: conference
year: '2009'
...
---
_id: '4545'
abstract:
- lang: eng
text: 'A stochastic game is a two-player game played oil a graph, where in each
state the successor is chosen either by One of the players, or according to a
probability distribution. We Survey Stochastic games with limsup and liminf objectives.
A real-valued re-ward is assigned to each state, and the value of all infinite
path is the limsup (resp. liminf) of all rewards along the path. The value of
a stochastic game is the maximal expected value of an infinite path that call
he achieved by resolving the decisions of the first player. We present the complexity
of computing values of Stochastic games and their subclasses, and the complexity,
of optimal strategies in such games. '
acknowledgement: This research was supported in part by the Swiss National Science
Foundation under the Indo-Swiss Joint Research Programme, by the European Network
of Excellence on Embedded Systems Design (ArtistDesign), by the European projects
COMBEST, Quasimodo, Gasics, by the PAI program Moves funded by the Belgian Federal
Government, and by the CFV (Federated Center in Verification) funded by the F.R.S.-FNRS.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Doyen L, Henzinger TA. A survey of stochastic games with limsup
and liminf objectives. In: Vol 5556. Springer; 2009:1-15. doi:10.1007/978-3-642-02930-1_1'
apa: 'Chatterjee, K., Doyen, L., & Henzinger, T. A. (2009). A survey of stochastic
games with limsup and liminf objectives (Vol. 5556, pp. 1–15). Presented at the
ICALP: Automata, Languages and Programming, Rhodos, Greece: Springer. https://doi.org/10.1007/978-3-642-02930-1_1'
chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “A Survey
of Stochastic Games with Limsup and Liminf Objectives,” 5556:1–15. Springer, 2009.
https://doi.org/10.1007/978-3-642-02930-1_1.
ieee: 'K. Chatterjee, L. Doyen, and T. A. Henzinger, “A survey of stochastic games
with limsup and liminf objectives,” presented at the ICALP: Automata, Languages
and Programming, Rhodos, Greece, 2009, vol. 5556, pp. 1–15.'
ista: 'Chatterjee K, Doyen L, Henzinger TA. 2009. A survey of stochastic games with
limsup and liminf objectives. ICALP: Automata, Languages and Programming, LNCS,
vol. 5556, 1–15.'
mla: Chatterjee, Krishnendu, et al. A Survey of Stochastic Games with Limsup
and Liminf Objectives. Vol. 5556, Springer, 2009, pp. 1–15, doi:10.1007/978-3-642-02930-1_1.
short: K. Chatterjee, L. Doyen, T.A. Henzinger, in:, Springer, 2009, pp. 1–15.
conference:
end_date: 2009-07-12
location: Rhodos, Greece
name: 'ICALP: Automata, Languages and Programming'
start_date: 2009-07-05
corr_author: '1'
date_created: 2018-12-11T12:09:24Z
date_published: 2009-06-24T00:00:00Z
date_updated: 2024-10-09T20:53:54Z
day: '24'
ddc:
- '000'
- '005'
department:
- _id: KrCh
doi: 10.1007/978-3-642-02930-1_1
ec_funded: 1
file:
- access_level: open_access
checksum: dabb6d24428a000254c95493d9c492e6
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:13:11Z
date_updated: 2020-07-14T12:46:31Z
file_id: '4992'
file_name: IST-2012-38-v1+1_A_survey_of_stochastic_games_with_limsup_and_liminf_objectives.pdf
file_size: 187419
relation: main_file
file_date_updated: 2020-07-14T12:46:31Z
has_accepted_license: '1'
intvolume: ' 5556'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 1 - 15
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
publication_status: published
publisher: Springer
publist_id: '177'
pubrep_id: '38'
quality_controlled: '1'
scopus_import: 1
status: public
title: A survey of stochastic games with limsup and liminf objectives
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5556
year: '2009'
...
---
_id: '4569'
abstract:
- lang: eng
text: "Most specification languages express only qualitative constraints. However,
among two implementations that satisfy a given specification, one may be preferred
to another. For example, if a specification asks that every request is followed
by a response, one may prefer an implementation that generates responses quickly
but does not generate unnecessary responses. We use quantitative properties to
measure the “goodness” of an implementation. Using games with corresponding quantitative
objectives, we can synthesize “optimal” implementations, which are preferred among
the set of possible implementations that satisfy a given specification.\r\nIn
particular, we show how automata with lexicographic mean-payoff conditions can
be used to express many interesting quantitative properties for reactive systems.
In this framework, the synthesis of optimal implementations requires the solution
of lexicographic mean-payoff games (for safety requirements), and the solution
of games with both lexicographic mean-payoff and parity objectives (for liveness
requirements). We present algorithms for solving both kinds of novel graph games."
acknowledgement: This research was supported by the Swiss National Science Foundation
(Indo-Swiss Research Program and NCCR MICS) and the European Union projects COMBEST
and COCONUT.
alternative_title:
- LNCS
arxiv: 1
author:
- first_name: Roderick
full_name: Bloem, Roderick
last_name: Bloem
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Barbara
full_name: Jobstmann, Barbara
last_name: Jobstmann
citation:
ama: 'Bloem R, Chatterjee K, Henzinger TA, Jobstmann B. Better quality in synthesis
through quantitative objectives. In: Vol 5643. Springer; 2009:140-156. doi:10.1007/978-3-642-02658-4_14'
apa: 'Bloem, R., Chatterjee, K., Henzinger, T. A., & Jobstmann, B. (2009). Better
quality in synthesis through quantitative objectives (Vol. 5643, pp. 140–156).
Presented at the CAV: Computer Aided Verification, Grenoble, France: Springer.
https://doi.org/10.1007/978-3-642-02658-4_14'
chicago: Bloem, Roderick, Krishnendu Chatterjee, Thomas A Henzinger, and Barbara
Jobstmann. “Better Quality in Synthesis through Quantitative Objectives,” 5643:140–56.
Springer, 2009. https://doi.org/10.1007/978-3-642-02658-4_14.
ieee: 'R. Bloem, K. Chatterjee, T. A. Henzinger, and B. Jobstmann, “Better quality
in synthesis through quantitative objectives,” presented at the CAV: Computer
Aided Verification, Grenoble, France, 2009, vol. 5643, pp. 140–156.'
ista: 'Bloem R, Chatterjee K, Henzinger TA, Jobstmann B. 2009. Better quality in
synthesis through quantitative objectives. CAV: Computer Aided Verification, LNCS,
vol. 5643, 140–156.'
mla: Bloem, Roderick, et al. Better Quality in Synthesis through Quantitative
Objectives. Vol. 5643, Springer, 2009, pp. 140–56, doi:10.1007/978-3-642-02658-4_14.
short: R. Bloem, K. Chatterjee, T.A. Henzinger, B. Jobstmann, in:, Springer, 2009,
pp. 140–156.
conference:
end_date: 2009-07-02
location: Grenoble, France
name: 'CAV: Computer Aided Verification'
start_date: 2009-06-26
date_created: 2018-12-11T12:09:31Z
date_published: 2009-06-19T00:00:00Z
date_updated: 2024-10-21T06:03:07Z
day: '19'
department:
- _id: KrCh
doi: 10.1007/978-3-642-02658-4_14
ec_funded: 1
external_id:
arxiv:
- '0904.2638'
intvolume: ' 5643'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/0904.2638
month: '06'
oa: 1
oa_version: Preprint
page: 140 - 156
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
publication_status: published
publisher: Springer
publist_id: '141'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Better quality in synthesis through quantitative objectives
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5643
year: '2009'
...