[{"place":"Dordrecht","publication":"Astrophysics and Space Science Proceedings","type":"conference","external_id":{"arxiv":["0809.3926"]},"citation":{"ieee":"Z. Haiman, “Observing the first stars and black holes,” in <i>Astrophysics and Space Science Proceedings</i>, 2009, pp. 385–418.","mla":"Haiman, Zoltán. “Observing the First Stars and Black Holes.” <i>Astrophysics and Space Science Proceedings</i>, Springer Nature, 2009, pp. 385–418, doi:<a href=\"https://doi.org/10.1007/978-1-4020-9457-6_15\">10.1007/978-1-4020-9457-6_15</a>.","apa":"Haiman, Z. (2009). Observing the first stars and black holes. In <i>Astrophysics and Space Science Proceedings</i> (pp. 385–418). Dordrecht: Springer Nature. <a href=\"https://doi.org/10.1007/978-1-4020-9457-6_15\">https://doi.org/10.1007/978-1-4020-9457-6_15</a>","ama":"Haiman Z. Observing the first stars and black holes. In: <i>Astrophysics and Space Science Proceedings</i>. Dordrecht: Springer Nature; 2009:385-418. doi:<a href=\"https://doi.org/10.1007/978-1-4020-9457-6_15\">10.1007/978-1-4020-9457-6_15</a>","ista":"Haiman Z. 2009. Observing the first stars and black holes. Astrophysics and Space Science Proceedings. , Astrophysics and Space Science Proceedings, , 385–418.","chicago":"Haiman, Zoltán. “Observing the First Stars and Black Holes.” In <i>Astrophysics and Space Science Proceedings</i>, 385–418. Dordrecht: Springer Nature, 2009. <a href=\"https://doi.org/10.1007/978-1-4020-9457-6_15\">https://doi.org/10.1007/978-1-4020-9457-6_15</a>.","short":"Z. Haiman, in:, Astrophysics and Space Science Proceedings, Springer Nature, Dordrecht, 2009, pp. 385–418."},"arxiv":1,"quality_controlled":"1","author":[{"last_name":"Haiman","orcid":"0000-0003-3633-5403","id":"7c006e8c-cc0d-11ee-8322-cb904ef76f36","first_name":"Zoltán","full_name":"Haiman, Zoltán"}],"page":"385-418","_id":"18726","doi":"10.1007/978-1-4020-9457-6_15","extern":"1","scopus_import":"1","language":[{"iso":"eng"}],"main_file_link":[{"url":"https://arxiv.org/abs/0809.3926","open_access":"1"}],"title":"Observing the first stars and black holes","date_created":"2025-01-03T12:09:18Z","day":"01","abstract":[{"lang":"eng","text":"The high sensitivity of JWST will open a new window on the end of the cosmological dark ages. Small stellar clusters, with a stellar mass of several × 106 M⊙, and low-mass black holes (BHs), with a mass of several $× 105 M⊙ should be directly detectable out to redshift z = 10, and individual supernovae (SNe) and gamma ray burst GRB afterglows are bright enough to be visible beyond this redshift. Dense primordial gas, in the process of collapsing from large scales to form protogalaxies, may also be possible to image through diffuse recombination line emission, possibly even before stars or BHs are formed. In this article, I discuss the key physical processes that are expected to have determined the sizes of the first star–clusters and black holes, and the prospect of studying these objects by direct detections with JWST and with other instruments. The direct light emitted by the very first stellar clusters and intermediate-mass black holes at z > 10 will likely fall below JWST’s detection threshold. However, JWST could reveal a decline at the faint-end of the high-redshift luminosity function, and thereby shed light on radiative and other feedback effects that operate at these early epochs. JWST will also have the sensitivity to detect individual SNe from beyond z = 10. In a dedicated survey lasting for several weeks, thousands of SNe could be detected at z > 6, with a redshift distribution extending to the formation of the very first stars at z ≳ 15. Using these SNe as tracers may be the only method to map out the earliest stages of the cosmic star–formation history. Finally, we point out that studying the earliest objects at high redshift will also offer a new window on the primordial power spectrum, on ∼100 times smaller scales than probed by current large-scale structure data."}],"publication_identifier":{"eissn":["1570-6605"],"eisbn":["9781402094576"],"issn":["1570-6591"],"isbn":["9781402094569"]},"OA_place":"repository","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","alternative_title":["Astrophysics and Space Science Proceedings"],"OA_type":"green","status":"public","year":"2009","date_updated":"2025-01-03T12:14:49Z","publication_status":"published","date_published":"2009-01-01T00:00:00Z","month":"01","publisher":"Springer Nature","oa":1,"article_processing_charge":"No"},{"article_processing_charge":"No","oa":1,"publisher":"Springer Nature","date_published":"2009-02-11T00:00:00Z","month":"02","date_updated":"2025-01-07T12:52:13Z","publication_status":"published","editor":[{"first_name":"Harley A.","full_name":"Thronson, Harley A.","last_name":"Thronson"},{"last_name":"Stiavelli","full_name":"Stiavelli, Massimo","first_name":"Massimo"},{"last_name":"Tielens","full_name":"Tielens, Alexander","first_name":"Alexander"}],"year":"2009","status":"public","OA_type":"green","alternative_title":["Astrophysics and Space Science Proceedings"],"oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_place":"repository","publication_identifier":{"issn":["1570-6591"],"isbn":["9781402094569"],"eissn":["1570-6605"],"eisbn":["9781402094576"]},"day":"11","abstract":[{"text":"The high sensitivity of JWST will open a new window on the end of the cosmological dark ages. Small stellar clusters, with a stellar mass of several × 106 M⊙, and low-mass black holes (BHs), with a mass of several $× 105 M⊙ should be directly detectable out to redshift z = 10, and individual supernovae (SNe) and gamma ray burst GRB afterglows are bright enough to be visible beyond this redshift. Dense primordial gas, in the process of collapsing from large scales to form protogalaxies, may also be possible to image through diffuse recombination line emission, possibly even before stars or BHs are formed. In this article, I discuss the key physical processes that are expected to have determined the sizes of the first star–clusters and black holes, and the prospect of studying these objects by direct detections with JWST and with other instruments. The direct light emitted by the very first stellar clusters and intermediate-mass black holes at z > 10 will likely fall below JWST’s detection threshold. However, JWST could reveal a decline at the faint-end of the high-redshift luminosity function, and thereby shed light on radiative and other feedback effects that operate at these early epochs. JWST will also have the sensitivity to detect individual SNe from beyond z = 10. In a dedicated survey lasting for several weeks, thousands of SNe could be detected at z > 6, with a redshift distribution extending to the formation of the very first stars at z ≳ 15. Using these SNe as tracers may be the only method to map out the earliest stages of the cosmic star–formation history. Finally, we point out that studying the earliest objects at high redshift will also offer a new window on the primordial power spectrum, on ∼100 times smaller scales than probed by current large-scale structure data.","lang":"eng"}],"date_created":"2025-01-03T12:29:16Z","title":"Observing the First Stars and Black Holes","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/0809.3926"}],"language":[{"iso":"eng"}],"extern":"1","scopus_import":"1","doi":"10.1007/978-1-4020-9457-6_15","_id":"18735","author":[{"last_name":"Haiman","orcid":"0000-0003-3633-5403","id":"7c006e8c-cc0d-11ee-8322-cb904ef76f36","first_name":"Zoltán","full_name":"Haiman, Zoltán"}],"page":"385-418","quality_controlled":"1","arxiv":1,"citation":{"chicago":"Haiman, Zoltán. “Observing the First Stars and Black Holes.” In <i>Astrophysics in the Next Decade</i>, edited by Harley A. Thronson, Massimo Stiavelli, and Alexander Tielens, 385–418. Springer Nature, 2009. <a href=\"https://doi.org/10.1007/978-1-4020-9457-6_15\">https://doi.org/10.1007/978-1-4020-9457-6_15</a>.","short":"Z. Haiman, in:, H.A. Thronson, M. Stiavelli, A. Tielens (Eds.), Astrophysics in the Next Decade, Springer Nature, 2009, pp. 385–418.","ista":"Haiman Z. 2009.Observing the First Stars and Black Holes. In: Astrophysics in the Next Decade. Astrophysics and Space Science Proceedings, , 385–418.","apa":"Haiman, Z. (2009). Observing the First Stars and Black Holes. In H. A. Thronson, M. Stiavelli, &#38; A. Tielens (Eds.), <i>Astrophysics in the Next Decade</i> (pp. 385–418). Springer Nature. <a href=\"https://doi.org/10.1007/978-1-4020-9457-6_15\">https://doi.org/10.1007/978-1-4020-9457-6_15</a>","ama":"Haiman Z. Observing the First Stars and Black Holes. In: Thronson HA, Stiavelli M, Tielens A, eds. <i>Astrophysics in the Next Decade</i>. Springer Nature; 2009:385-418. doi:<a href=\"https://doi.org/10.1007/978-1-4020-9457-6_15\">10.1007/978-1-4020-9457-6_15</a>","ieee":"Z. Haiman, “Observing the First Stars and Black Holes,” in <i>Astrophysics in the Next Decade</i>, H. A. Thronson, M. Stiavelli, and A. Tielens, Eds. Springer Nature, 2009, pp. 385–418.","mla":"Haiman, Zoltán. “Observing the First Stars and Black Holes.” <i>Astrophysics in the Next Decade</i>, edited by Harley A. Thronson et al., Springer Nature, 2009, pp. 385–418, doi:<a href=\"https://doi.org/10.1007/978-1-4020-9457-6_15\">10.1007/978-1-4020-9457-6_15</a>."},"external_id":{"arxiv":["0809.3926"]},"publication":"Astrophysics in the Next Decade","type":"book_chapter"},{"day":"23","abstract":[{"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 &quot;on/off switch&quot; (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.","lang":"eng"}],"date_created":"2018-12-11T11:54:59Z","title":"Structural basis for the mechanism of respiratory complex I","volume":284,"publisher":"American Society for Biochemistry and Molecular Biology","month":"10","date_published":"2009-10-23T00:00:00Z","extern":1,"date_updated":"2021-01-12T06:54:26Z","publication_status":"published","doi":"10.1074/jbc.M109.032144","_id":"1971","quality_controlled":0,"author":[{"full_name":"Berrisford, John M","first_name":"John","last_name":"Berrisford"},{"orcid":"0000-0002-0977-7989","last_name":"Sazanov","full_name":"Leonid Sazanov","first_name":"Leonid A","id":"338D39FE-F248-11E8-B48F-1D18A9856A87"}],"issue":"43","page":"29773 - 29783","year":"2009","status":"public","citation":{"short":"J. Berrisford, L.A. Sazanov, Journal of Biological Chemistry 284 (2009) 29773–29783.","chicago":"Berrisford, John, and Leonid A Sazanov. “Structural Basis for the Mechanism of Respiratory Complex I.” <i>Journal of Biological Chemistry</i>. American Society for Biochemistry and Molecular Biology, 2009. <a href=\"https://doi.org/10.1074/jbc.M109.032144\">https://doi.org/10.1074/jbc.M109.032144</a>.","ista":"Berrisford J, Sazanov LA. 2009. Structural basis for the mechanism of respiratory complex I. Journal of Biological Chemistry. 284(43), 29773–29783.","ama":"Berrisford J, Sazanov LA. Structural basis for the mechanism of respiratory complex I. <i>Journal of Biological Chemistry</i>. 2009;284(43):29773-29783. doi:<a href=\"https://doi.org/10.1074/jbc.M109.032144\">10.1074/jbc.M109.032144</a>","apa":"Berrisford, J., &#38; Sazanov, L. A. (2009). Structural basis for the mechanism of respiratory complex I. <i>Journal of Biological Chemistry</i>. American Society for Biochemistry and Molecular Biology. <a href=\"https://doi.org/10.1074/jbc.M109.032144\">https://doi.org/10.1074/jbc.M109.032144</a>","mla":"Berrisford, John, and Leonid A. Sazanov. “Structural Basis for the Mechanism of Respiratory Complex I.” <i>Journal of Biological Chemistry</i>, vol. 284, no. 43, American Society for Biochemistry and Molecular Biology, 2009, pp. 29773–83, doi:<a href=\"https://doi.org/10.1074/jbc.M109.032144\">10.1074/jbc.M109.032144</a>.","ieee":"J. Berrisford and L. A. Sazanov, “Structural basis for the mechanism of respiratory complex I,” <i>Journal of Biological Chemistry</i>, vol. 284, no. 43. American Society for Biochemistry and Molecular Biology, pp. 29773–29783, 2009."},"acknowledgement":"This work was supported by the Medical Research Council. ","intvolume":"       284","publist_id":"5114","type":"journal_article","publication":"Journal of Biological Chemistry"},{"publisher":"Genetics Society of America","month":"01","date_published":"2009-01-01T00:00:00Z","date_updated":"2021-01-12T07:56:22Z","publication_status":"published","extern":1,"day":"01","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."}],"date_created":"2018-12-11T12:08:26Z","volume":181,"title":"Parallel genetic evolution within and between bacteriophage species of varying degrees of divergence","intvolume":"       181","citation":{"mla":"Bollback, Jonathan P., and John Huelsenbeck. “Parallel Genetic Evolution within and between Bacteriophage Species of Varying Degrees of Divergence.” <i>Genetics</i>, vol. 181, no. 1, Genetics Society of America, 2009, pp. 225–34, doi:<a href=\"https://doi.org/10.1534/genetics.107.085225\">10.1534/genetics.107.085225</a>.","ieee":"J. P. Bollback and J. Huelsenbeck, “Parallel genetic evolution within and between bacteriophage species of varying degrees of divergence,” <i>Genetics</i>, vol. 181, no. 1. Genetics Society of America, pp. 225–234, 2009.","apa":"Bollback, J. P., &#38; Huelsenbeck, J. (2009). Parallel genetic evolution within and between bacteriophage species of varying degrees of divergence. <i>Genetics</i>. Genetics Society of America. <a href=\"https://doi.org/10.1534/genetics.107.085225\">https://doi.org/10.1534/genetics.107.085225</a>","ama":"Bollback JP, Huelsenbeck J. Parallel genetic evolution within and between bacteriophage species of varying degrees of divergence. <i>Genetics</i>. 2009;181(1):225-234. doi:<a href=\"https://doi.org/10.1534/genetics.107.085225\">10.1534/genetics.107.085225</a>","ista":"Bollback JP, Huelsenbeck J. 2009. Parallel genetic evolution within and between bacteriophage species of varying degrees of divergence. Genetics. 181(1), 225–234.","chicago":"Bollback, Jonathan P, and John Huelsenbeck. “Parallel Genetic Evolution within and between Bacteriophage Species of Varying Degrees of Divergence.” <i>Genetics</i>. Genetics Society of America, 2009. <a href=\"https://doi.org/10.1534/genetics.107.085225\">https://doi.org/10.1534/genetics.107.085225</a>.","short":"J.P. Bollback, J. Huelsenbeck, Genetics 181 (2009) 225–234."},"publication":"Genetics","type":"journal_article","publist_id":"1101","doi":"10.1534/genetics.107.085225","_id":"4357","status":"public","issue":"1","author":[{"full_name":"Jonathan Bollback","first_name":"Jonathan P","id":"2C6FA9CC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4624-4612","last_name":"Bollback"},{"last_name":"Huelsenbeck","first_name":"John","full_name":"Huelsenbeck, John P"}],"page":"225 - 234","year":"2009","quality_controlled":0},{"publist_id":"1098","publication":"7th International Symposium on Frontiers of Combining Systems","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"None","alternative_title":["LNCS"],"citation":{"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.","chicago":"Wies, Thomas, Ruzica Piskac, and Viktor Kuncak. “Combining Theories with Shared Set Operations.” In <i>7th International Symposium on Frontiers of Combining Systems</i>, 5749:366–82. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-04222-5_23\">https://doi.org/10.1007/978-3-642-04222-5_23</a>.","short":"T. Wies, R. Piskac, V. Kuncak, in:, 7th International Symposium on Frontiers of Combining Systems, Springer, 2009, pp. 366–382.","ieee":"T. Wies, R. Piskac, and V. Kuncak, “Combining theories with shared set operations,” in <i>7th International Symposium on Frontiers of Combining Systems</i>, Trento, Italy, 2009, vol. 5749, pp. 366–382.","mla":"Wies, Thomas, et al. “Combining Theories with Shared Set Operations.” <i>7th International Symposium on Frontiers of Combining Systems</i>, vol. 5749, Springer, 2009, pp. 366–82, doi:<a href=\"https://doi.org/10.1007/978-3-642-04222-5_23\">10.1007/978-3-642-04222-5_23</a>.","apa":"Wies, T., Piskac, R., &#38; Kuncak, V. (2009). Combining theories with shared set operations. In <i>7th International Symposium on Frontiers of Combining Systems</i> (Vol. 5749, pp. 366–382). Trento, Italy: Springer. <a href=\"https://doi.org/10.1007/978-3-642-04222-5_23\">https://doi.org/10.1007/978-3-642-04222-5_23</a>","ama":"Wies T, Piskac R, Kuncak V. Combining theories with shared set operations. In: <i>7th International Symposium on Frontiers of Combining Systems</i>. Vol 5749. Springer; 2009:366-382. doi:<a href=\"https://doi.org/10.1007/978-3-642-04222-5_23\">10.1007/978-3-642-04222-5_23</a>"},"intvolume":"      5749","quality_controlled":"1","author":[{"last_name":"Wies","full_name":"Wies, Thomas","first_name":"Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Piskac, Ruzica","first_name":"Ruzica","last_name":"Piskac"},{"last_name":"Kuncak","full_name":"Kuncak, Viktor","first_name":"Viktor"}],"status":"public","page":"366 - 382","year":"2009","_id":"4360","doi":"10.1007/978-3-642-04222-5_23","publication_status":"published","scopus_import":"1","date_updated":"2025-07-02T06:21:09Z","extern":"1","month":"01","date_published":"2009-01-01T00:00:00Z","publisher":"Springer","language":[{"iso":"eng"}],"title":"Combining theories with shared set operations","volume":5749,"date_created":"2018-12-11T12:08:27Z","abstract":[{"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.","lang":"eng"}],"day":"01","article_processing_charge":"No","conference":{"start_date":"2009-09-16","name":"FroCoS: Frontiers of Combining Systems","end_date":"2009-09-18","location":"Trento, Italy"}},{"year":"2009","status":"public","author":[{"full_name":"Vasu Singh","first_name":"Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","last_name":"Singh"}],"quality_controlled":0,"_id":"4363","publication":"Formalizing and Verifying Transactional Memories","publist_id":"1095","type":"dissertation","citation":{"ieee":"V. Singh, “Formalizing and Verifying Transactional Memories,” EPFL Lausanne, 2009.","mla":"Singh, Vasu. “Formalizing and Verifying Transactional Memories.” <i>Formalizing and Verifying Transactional Memories</i>, EPFL Lausanne, 2009.","apa":"Singh, V. (2009). <i>Formalizing and Verifying Transactional Memories</i>. <i>Formalizing and Verifying Transactional Memories</i>. EPFL Lausanne.","ama":"Singh V. Formalizing and Verifying Transactional Memories. <i>Formalizing and Verifying Transactional Memories</i>. 2009.","ista":"Singh V. 2009. Formalizing and Verifying Transactional Memories. EPFL Lausanne.","chicago":"Singh, Vasu. “Formalizing and Verifying Transactional Memories.” <i>Formalizing and Verifying Transactional Memories</i>. EPFL Lausanne, 2009.","short":"V. Singh, Formalizing and Verifying Transactional Memories, EPFL Lausanne, 2009."},"title":"Formalizing and Verifying Transactional Memories","day":"01","date_created":"2018-12-11T12:08:28Z","month":"01","date_published":"2009-01-01T00:00:00Z","publication_status":"published","extern":1,"date_updated":"2021-01-12T07:56:25Z","publisher":"EPFL Lausanne"},{"language":[{"iso":"eng"}],"title":"Abstraction refinement for quantified array assertions","volume":5673,"date_created":"2018-12-11T12:08:29Z","day":"01","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."}],"article_processing_charge":"No","conference":{"start_date":"2009-08-09","name":"SAS: Static Analysis Symposium","end_date":"2009-08-11","location":"Los Angeles, CA, United States"},"publication_status":"published","extern":"1","date_updated":"2025-07-02T06:45:01Z","date_published":"2009-01-01T00:00:00Z","month":"01","publisher":"Springer","author":[{"last_name":"Seghir","first_name":"Mohamed","full_name":"Seghir, Mohamed"},{"last_name":"Podelski","full_name":"Podelski, Andreas","first_name":"Andreas"},{"last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","full_name":"Wies, Thomas"}],"year":"2009","page":"3 - 18","status":"public","_id":"4365","doi":"10.1007/978-3-642-03237-0_3","publist_id":"1094","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication":"16th International Symposium on Static Analysis","oa_version":"None","alternative_title":["LNCS"],"citation":{"mla":"Seghir, Mohamed, et al. “Abstraction Refinement for Quantified Array Assertions.” <i>16th International Symposium on Static Analysis</i>, vol. 5673, Springer, 2009, pp. 3–18, doi:<a href=\"https://doi.org/10.1007/978-3-642-03237-0_3\">10.1007/978-3-642-03237-0_3</a>.","ieee":"M. Seghir, A. Podelski, and T. Wies, “Abstraction refinement for quantified array assertions,” in <i>16th International Symposium on Static Analysis</i>, Los Angeles, CA, United States, 2009, vol. 5673, pp. 3–18.","ama":"Seghir M, Podelski A, Wies T. Abstraction refinement for quantified array assertions. In: <i>16th International Symposium on Static Analysis</i>. Vol 5673. Springer; 2009:3-18. doi:<a href=\"https://doi.org/10.1007/978-3-642-03237-0_3\">10.1007/978-3-642-03237-0_3</a>","apa":"Seghir, M., Podelski, A., &#38; Wies, T. (2009). Abstraction refinement for quantified array assertions. In <i>16th International Symposium on Static Analysis</i> (Vol. 5673, pp. 3–18). Los Angeles, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-642-03237-0_3\">https://doi.org/10.1007/978-3-642-03237-0_3</a>","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.","short":"M. Seghir, A. Podelski, T. Wies, in:, 16th International Symposium on Static Analysis, Springer, 2009, pp. 3–18.","chicago":"Seghir, Mohamed, Andreas Podelski, and Thomas Wies. “Abstraction Refinement for Quantified Array Assertions.” In <i>16th International Symposium on Static Analysis</i>, 5673:3–18. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-03237-0_3\">https://doi.org/10.1007/978-3-642-03237-0_3</a>."},"intvolume":"      5673"},{"_id":"4375","doi":"10.1007/978-3-642-02658-4_37","year":"2009","status":"public","author":[{"last_name":"Lahiri","full_name":"Lahiri, Shuvendu","first_name":"Shuvendu"},{"first_name":"Shaz","full_name":"Qadeer, Shaz","last_name":"Qadeer"},{"first_name":"Juan","full_name":"Galeotti, Juan","last_name":"Galeotti"},{"last_name":"Voung","first_name":"Jan","full_name":"Voung, Jan"},{"first_name":"Thomas","full_name":"Wies, Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","last_name":"Wies"}],"page":"493 - 508","intvolume":"      5643","oa_version":"None","citation":{"apa":"Lahiri, S., Qadeer, S., Galeotti, J., Voung, J., &#38; Wies, T. (2009). Intra-module inference. In <i>21st International Conference on Computer Aided Verification</i> (Vol. 5643, pp. 493–508). Grenoble, France: Springer. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_37\">https://doi.org/10.1007/978-3-642-02658-4_37</a>","ama":"Lahiri S, Qadeer S, Galeotti J, Voung J, Wies T. Intra-module inference. In: <i>21st International Conference on Computer Aided Verification</i>. Vol 5643. Springer; 2009:493-508. doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_37\">10.1007/978-3-642-02658-4_37</a>","mla":"Lahiri, Shuvendu, et al. “Intra-Module Inference.” <i>21st International Conference on Computer Aided Verification</i>, vol. 5643, Springer, 2009, pp. 493–508, doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_37\">10.1007/978-3-642-02658-4_37</a>.","ieee":"S. Lahiri, S. Qadeer, J. Galeotti, J. Voung, and T. Wies, “Intra-module inference,” in <i>21st International Conference on Computer Aided Verification</i>, Grenoble, France, 2009, vol. 5643, pp. 493–508.","chicago":"Lahiri, Shuvendu, Shaz Qadeer, Juan Galeotti, Jan Voung, and Thomas Wies. “Intra-Module Inference.” In <i>21st International Conference on Computer Aided Verification</i>, 5643:493–508. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_37\">https://doi.org/10.1007/978-3-642-02658-4_37</a>.","short":"S. Lahiri, S. Qadeer, J. Galeotti, J. Voung, T. Wies, in:, 21st International Conference on Computer Aided Verification, Springer, 2009, 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."},"alternative_title":["LNCS"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","publist_id":"1082","publication":"21st International Conference on Computer Aided Verification","publication_identifier":{"eisbn":["978-3-642-02658-4"]},"conference":{"location":"Grenoble, France","end_date":"2009-07-02","name":"CAV: Computer Aided Verification","start_date":"2009-06-26"},"date_created":"2018-12-11T12:08:32Z","day":"01","article_processing_charge":"No","volume":5643,"language":[{"iso":"eng"}],"title":"Intra-module inference","publisher":"Springer","extern":"1","publication_status":"published","date_updated":"2025-07-02T06:41:41Z","month":"01","date_published":"2009-01-01T00:00:00Z"},{"publisher":"ACM","scopus_import":"1","publication_status":"published","extern":"1","date_updated":"2025-07-02T06:17:51Z","date_published":"2009-10-25T00:00:00Z","month":"10","date_created":"2018-12-11T12:08:32Z","article_processing_charge":"No","day":"25","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."}],"volume":44,"language":[{"iso":"eng"}],"title":"Parallel programming with object assemblies","intvolume":"        44","oa_version":"None","citation":{"short":"R. Lublinerman, S. Chaudhuri, P. Cerny, ACM SIGPLAN Notices 44 (2009) 61–80.","chicago":"Lublinerman, Roberto, Swarat Chaudhuri, and Pavol Cerny. “Parallel Programming with Object Assemblies.” <i>ACM SIGPLAN Notices</i>. ACM, 2009. <a href=\"https://doi.org/10.1145/1639949.164009\">https://doi.org/10.1145/1639949.164009</a>.","ista":"Lublinerman R, Chaudhuri S, Cerny P. 2009. Parallel programming with object assemblies. ACM SIGPLAN Notices. 44(10), 61–80.","ama":"Lublinerman R, Chaudhuri S, Cerny P. Parallel programming with object assemblies. <i>ACM SIGPLAN Notices</i>. 2009;44(10):61-80. doi:<a href=\"https://doi.org/10.1145/1639949.164009\">10.1145/1639949.164009</a>","apa":"Lublinerman, R., Chaudhuri, S., &#38; Cerny, P. (2009). Parallel programming with object assemblies. <i>ACM SIGPLAN Notices</i>. ACM. <a href=\"https://doi.org/10.1145/1639949.164009\">https://doi.org/10.1145/1639949.164009</a>","mla":"Lublinerman, Roberto, et al. “Parallel Programming with Object Assemblies.” <i>ACM SIGPLAN Notices</i>, vol. 44, no. 10, ACM, 2009, pp. 61–80, doi:<a href=\"https://doi.org/10.1145/1639949.164009\">10.1145/1639949.164009</a>.","ieee":"R. Lublinerman, S. Chaudhuri, and P. Cerny, “Parallel programming with object assemblies,” <i>ACM SIGPLAN Notices</i>, vol. 44, no. 10. ACM, pp. 61–80, 2009."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","publication":"ACM SIGPLAN Notices","publist_id":"1083","_id":"4376","doi":"10.1145/1639949.164009","year":"2009","author":[{"full_name":"Lublinerman, Roberto","first_name":"Roberto","last_name":"Lublinerman"},{"first_name":"Swarat","full_name":"Chaudhuri, Swarat","last_name":"Chaudhuri"},{"full_name":"Cerny, Pavol","first_name":"Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","last_name":"Cerny"}],"status":"public","issue":"10","page":"61 - 80","quality_controlled":"1"},{"alternative_title":["LNCS"],"citation":{"apa":"Hoenicke, J., Leino, K. R., Podelski, A., Schäf, M., &#38; Wies, T. (2009). It’s doomed; we can prove it. In <i>Second World Congress on Formal Methods</i> (Vol. 5850, pp. 338–353). Eindhoven, The Netherlands: Springer. <a href=\"https://doi.org/10.1007/978-3-642-05089-3_22\">https://doi.org/10.1007/978-3-642-05089-3_22</a>","ama":"Hoenicke J, Leino KR, Podelski A, Schäf M, Wies T. It’s doomed; we can prove it. In: <i>Second World Congress on Formal Methods</i>. Vol 5850. Springer; 2009:338-353. doi:<a href=\"https://doi.org/10.1007/978-3-642-05089-3_22\">10.1007/978-3-642-05089-3_22</a>","ieee":"J. Hoenicke, K. R. Leino, A. Podelski, M. Schäf, and T. Wies, “It’s doomed; we can prove it,” in <i>Second World Congress on Formal Methods</i>, Eindhoven, The Netherlands, 2009, vol. 5850, pp. 338–353.","mla":"Hoenicke, Jochen, et al. “It’s Doomed; We Can Prove It.” <i>Second World Congress on Formal Methods</i>, vol. 5850, Springer, 2009, pp. 338–53, doi:<a href=\"https://doi.org/10.1007/978-3-642-05089-3_22\">10.1007/978-3-642-05089-3_22</a>.","chicago":"Hoenicke, Jochen, K Rustan Leino, Andreas Podelski, Martin Schäf, and Thomas Wies. “It’s Doomed; We Can Prove It.” In <i>Second World Congress on Formal Methods</i>, 5850:338–53. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-05089-3_22\">https://doi.org/10.1007/978-3-642-05089-3_22</a>.","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.","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."},"oa_version":"None","intvolume":"      5850","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"1079","publication":"Second World Congress on Formal Methods","doi":"10.1007/978-3-642-05089-3_22","_id":"4377","quality_controlled":"1","page":"338 - 353","year":"2009","status":"public","author":[{"last_name":"Hoenicke","first_name":"Jochen","full_name":"Hoenicke, Jochen"},{"full_name":"Leino, K Rustan","first_name":"K Rustan","last_name":"Leino"},{"last_name":"Podelski","first_name":"Andreas","full_name":"Podelski, Andreas"},{"last_name":"Schäf","full_name":"Schäf, Martin","first_name":"Martin"},{"last_name":"Wies","full_name":"Wies, Thomas","first_name":"Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87"}],"publisher":"Springer","month":"01","date_published":"2009-01-01T00:00:00Z","publication_status":"published","date_updated":"2025-07-02T06:38:22Z","extern":"1","scopus_import":"1","article_processing_charge":"No","day":"01","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."}],"date_created":"2018-12-11T12:08:32Z","conference":{"start_date":"2009-11-02","name":"FM: Formal Methods","end_date":"2009-11-06","location":"Eindhoven, The Netherlands"},"title":"It's doomed; we can prove it","language":[{"iso":"eng"}],"volume":5850},{"conference":{"name":"CAV: Computer Aided Verification"},"date_created":"2018-12-11T12:08:34Z","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."}],"day":"19","volume":5643,"file_date_updated":"2020-07-14T12:46:28Z","oa":1,"title":"Software transactional memory on relaxed memory models","publisher":"Springer","pubrep_id":"45","date_updated":"2021-01-12T07:56:34Z","publication_status":"published","extern":1,"date_published":"2009-06-19T00:00:00Z","month":"06","_id":"4383","doi":"10.1007/978-3-642-02658-4_26","year":"2009","page":"321 - 336","author":[{"last_name":"Guerraoui","first_name":"Rachid","full_name":"Guerraoui, Rachid"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","first_name":"Vasu","full_name":"Vasu Singh","last_name":"Singh"}],"status":"public","quality_controlled":0,"intvolume":"      5643","acknowledgement":"This research was supported by the Swiss National Science Foundation.","file":[{"date_updated":"2020-07-14T12:46:28Z","creator":"system","access_level":"open_access","content_type":"application/pdf","checksum":"df3c3e6306afd3f630a9146f91642f0a","file_size":265763,"file_id":"5105","relation":"main_file","file_name":"IST-2012-45-v1+1_Software_transactional_memory_on_relaxed_memory_models.pdf","date_created":"2018-12-12T10:14:50Z"}],"citation":{"ama":"Guerraoui R, Henzinger TA, Singh V. Software transactional memory on relaxed memory models. In: Vol 5643. Springer; 2009:321-336. doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_26\">10.1007/978-3-642-02658-4_26</a>","apa":"Guerraoui, R., Henzinger, T. A., &#38; Singh, V. (2009). Software transactional memory on relaxed memory models (Vol. 5643, pp. 321–336). Presented at the CAV: Computer Aided Verification, Springer. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_26\">https://doi.org/10.1007/978-3-642-02658-4_26</a>","mla":"Guerraoui, Rachid, et al. <i>Software Transactional Memory on Relaxed Memory Models</i>. Vol. 5643, Springer, 2009, pp. 321–36, doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_26\">10.1007/978-3-642-02658-4_26</a>.","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.","short":"R. Guerraoui, T.A. Henzinger, V. Singh, in:, Springer, 2009, pp. 321–336.","chicago":"Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Software Transactional Memory on Relaxed Memory Models,” 5643:321–36. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_26\">https://doi.org/10.1007/978-3-642-02658-4_26</a>.","ista":"Guerraoui R, Henzinger TA, Singh V. 2009. Software transactional memory on relaxed memory models. CAV: Computer Aided Verification, LNCS, vol. 5643, 321–336."},"alternative_title":["LNCS"],"publist_id":"1074","type":"conference"},{"_id":"4385","doi":"10.1145/1582716.1582725","page":"7 - 16","status":"public","author":[{"first_name":"Aleksandar","full_name":"Dragojevic, Aleksandar","last_name":"Dragojevic"},{"last_name":"Guerraoui","full_name":"Guerraoui, Rachid","first_name":"Rachid"},{"first_name":"Anmol","full_name":"Singh, Anmol","last_name":"Singh"},{"last_name":"Singh","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","first_name":"Vasu","full_name":"Singh, Vasu"}],"year":"2009","quality_controlled":"1","oa_version":"None","citation":{"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.","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.","chicago":"Dragojevic, Aleksandar, Rachid Guerraoui, Anmol Singh, and Vasu Singh. “Preventing versus Curing: Avoiding Conflicts in Transactional Memories.” In <i>Proceedings of the 28th ACM Symposium on Principles of Distributed Computing</i>, 7–16. ACM, 2009. <a href=\"https://doi.org/10.1145/1582716.1582725\">https://doi.org/10.1145/1582716.1582725</a>.","mla":"Dragojevic, Aleksandar, et al. “Preventing versus Curing: Avoiding Conflicts in Transactional Memories.” <i>Proceedings of the 28th ACM Symposium on Principles of Distributed Computing</i>, ACM, 2009, pp. 7–16, doi:<a href=\"https://doi.org/10.1145/1582716.1582725\">10.1145/1582716.1582725</a>.","ieee":"A. Dragojevic, R. Guerraoui, A. Singh, and V. Singh, “Preventing versus curing: Avoiding conflicts in transactional memories,” in <i>Proceedings of the 28th ACM symposium on Principles of distributed computing</i>, Calgary, Canada, 2009, pp. 7–16.","ama":"Dragojevic A, Guerraoui R, Singh A, Singh V. Preventing versus curing: Avoiding conflicts in transactional memories. In: <i>Proceedings of the 28th ACM Symposium on Principles of Distributed Computing</i>. ACM; 2009:7-16. doi:<a href=\"https://doi.org/10.1145/1582716.1582725\">10.1145/1582716.1582725</a>","apa":"Dragojevic, A., Guerraoui, R., Singh, A., &#38; Singh, V. (2009). Preventing versus curing: Avoiding conflicts in transactional memories. In <i>Proceedings of the 28th ACM symposium on Principles of distributed computing</i> (pp. 7–16). Calgary, Canada: ACM. <a href=\"https://doi.org/10.1145/1582716.1582725\">https://doi.org/10.1145/1582716.1582725</a>"},"type":"conference","publication":"Proceedings of the 28th ACM symposium on Principles of distributed computing","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"1070","conference":{"start_date":"2009-08-10","name":"POPL: Principles of Programming Languages","end_date":"2009-08-12","location":"Calgary, Canada"},"date_created":"2018-12-11T12:08:35Z","day":"10","article_processing_charge":"No","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."}],"language":[{"iso":"eng"}],"title":"Preventing versus curing: Avoiding conflicts in transactional memories","publisher":"ACM","extern":"1","publication_status":"published","date_updated":"2025-07-02T06:35:49Z","scopus_import":"1","month":"08","date_published":"2009-08-10T00:00:00Z"},{"month":"07","date_published":"2009-07-01T00:00:00Z","scopus_import":"1","date_updated":"2025-07-02T06:32:32Z","publication_status":"published","extern":"1","publisher":"Springer","volume":5643,"title":"Automated analysis of Java methods for confidentiality","language":[{"iso":"eng"}],"conference":{"name":"CAV: Computer Aided Verification"},"day":"01","abstract":[{"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.","lang":"eng"}],"article_processing_charge":"No","date_created":"2018-12-11T12:08:36Z","publication":"21st International Conference on Computer Aided Verification","publist_id":"1067","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":"      5643","alternative_title":["LNCS"],"citation":{"ama":"Cerny P, Alur R. Automated analysis of Java methods for confidentiality. In: <i>21st International Conference on Computer Aided Verification</i>. Vol 5643. Springer; 2009:173-187. doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_16\">10.1007/978-3-642-02658-4_16</a>","apa":"Cerny, P., &#38; Alur, R. (2009). Automated analysis of Java methods for confidentiality. In <i>21st International Conference on Computer Aided Verification</i> (Vol. 5643, pp. 173–187). Springer. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_16\">https://doi.org/10.1007/978-3-642-02658-4_16</a>","ieee":"P. Cerny and R. Alur, “Automated analysis of Java methods for confidentiality,” in <i>21st International Conference on Computer Aided Verification</i>, 2009, vol. 5643, pp. 173–187.","mla":"Cerny, Pavol, and Rajeev Alur. “Automated Analysis of Java Methods for Confidentiality.” <i>21st International Conference on Computer Aided Verification</i>, vol. 5643, Springer, 2009, pp. 173–87, doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_16\">10.1007/978-3-642-02658-4_16</a>.","short":"P. Cerny, R. Alur, in:, 21st International Conference on Computer Aided Verification, Springer, 2009, pp. 173–187.","chicago":"Cerny, Pavol, and Rajeev Alur. “Automated Analysis of Java Methods for Confidentiality.” In <i>21st International Conference on Computer Aided Verification</i>, 5643:173–87. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_16\">https://doi.org/10.1007/978-3-642-02658-4_16</a>.","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."},"oa_version":"None","author":[{"last_name":"Cerny","first_name":"Pavol","full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"}],"page":"173 - 187","year":"2009","status":"public","quality_controlled":"1","doi":"10.1007/978-3-642-02658-4_16","_id":"4391"},{"month":"09","date_published":"2009-09-01T00:00:00Z","publication_status":"published","date_updated":"2025-09-30T08:04:32Z","publisher":"Springer","oa":1,"conference":{"start_date":"2009-09-07","name":"CSL: Computer Science Logic","end_date":"2009-09-11","location":"Coimbra, Portugal"},"article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["LNCS"],"oa_version":"Submitted Version","year":"2009","status":"public","extern":"1","volume":5771,"title":"Algorithmic analysis of array-accessing programs","main_file_link":[{"url":"http://repository.upenn.edu/cis_reports/894/","open_access":"1"}],"language":[{"iso":"eng"}],"related_material":{"record":[{"status":"public","id":"2967","relation":"later_version"}]},"abstract":[{"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.","lang":"eng"}],"day":"01","date_created":"2018-12-11T12:08:40Z","type":"conference","publist_id":"1056","intvolume":"      5771","citation":{"short":"R. Alur, P. Cerny, S. Weinstein, in:, Springer, 2009, pp. 86–101.","chicago":"Alur, Rajeev, Pavol Cerny, and Scott Weinstein. “Algorithmic Analysis of Array-Accessing Programs,” 5771:86–101. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-04027-6_9\">https://doi.org/10.1007/978-3-642-04027-6_9</a>.","ista":"Alur R, Cerny P, Weinstein S. 2009. Algorithmic analysis of array-accessing programs. CSL: Computer Science Logic, LNCS, vol. 5771, 86–101.","ama":"Alur R, Cerny P, Weinstein S. Algorithmic analysis of array-accessing programs. In: Vol 5771. Springer; 2009:86-101. doi:<a href=\"https://doi.org/10.1007/978-3-642-04027-6_9\">10.1007/978-3-642-04027-6_9</a>","apa":"Alur, R., Cerny, P., &#38; Weinstein, S. (2009). Algorithmic analysis of array-accessing programs (Vol. 5771, pp. 86–101). Presented at the CSL: Computer Science Logic, Coimbra, Portugal: Springer. <a href=\"https://doi.org/10.1007/978-3-642-04027-6_9\">https://doi.org/10.1007/978-3-642-04027-6_9</a>","mla":"Alur, Rajeev, et al. <i>Algorithmic Analysis of Array-Accessing Programs</i>. Vol. 5771, Springer, 2009, pp. 86–101, doi:<a href=\"https://doi.org/10.1007/978-3-642-04027-6_9\">10.1007/978-3-642-04027-6_9</a>.","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."},"author":[{"first_name":"Rajeev","full_name":"Alur, Rajeev","last_name":"Alur"},{"last_name":"Cerny","full_name":"Cerny, Pavol","first_name":"Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Weinstein","full_name":"Weinstein, Scott","first_name":"Scott"}],"page":"86 - 101","quality_controlled":"1","doi":"10.1007/978-3-642-04027-6_9","_id":"4403"},{"main_file_link":[{"open_access":"0","url":"http://pub.ist.ac.at/%7Etah/Publications/sliding-window_abstraction_for_infinite_markov_chains.pdf"}],"oa":1,"title":"Sliding-window abstraction for infinite Markov chains","volume":5643,"file_date_updated":"2020-07-14T12:46:30Z","date_created":"2018-12-11T12:08:55Z","abstract":[{"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.","lang":"eng"}],"day":"01","conference":{"name":"CAV: Computer Aided Verification"},"date_updated":"2021-01-12T07:57:04Z","extern":1,"publication_status":"published","date_published":"2009-01-01T00:00:00Z","month":"01","publisher":"Springer","pubrep_id":"40","quality_controlled":0,"author":[{"full_name":"Thomas Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"last_name":"Mateescu","full_name":"Maria Mateescu","first_name":"Maria","id":"3B43276C-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Wolf","first_name":"Verena","full_name":"Wolf, Verena"}],"year":"2009","status":"public","page":"337 - 352","_id":"4453","doi":"10.1007/978-3-642-02658-4_27","publist_id":"278","type":"conference","alternative_title":["LNCS"],"file":[{"date_updated":"2020-07-14T12:46:30Z","content_type":"application/pdf","file_size":804295,"access_level":"open_access","checksum":"36b974111521ea534aae294166e93a63","creator":"system","file_id":"4938","relation":"main_file","date_created":"2018-12-12T10:12:20Z","file_name":"IST-2012-40-v1+1_Sliding-window_abstraction_for_infinite_markov_chains.pdf"}],"citation":{"ama":"Henzinger TA, Mateescu M, Wolf V. Sliding-window abstraction for infinite Markov chains. In: Vol 5643. Springer; 2009:337-352. doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_27\">10.1007/978-3-642-02658-4_27</a>","apa":"Henzinger, T. A., Mateescu, M., &#38; Wolf, V. (2009). Sliding-window abstraction for infinite Markov chains (Vol. 5643, pp. 337–352). Presented at the CAV: Computer Aided Verification, Springer. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_27\">https://doi.org/10.1007/978-3-642-02658-4_27</a>","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.","mla":"Henzinger, Thomas A., et al. <i>Sliding-Window Abstraction for Infinite Markov Chains</i>. Vol. 5643, Springer, 2009, pp. 337–52, doi:<a href=\"https://doi.org/10.1007/978-3-642-02658-4_27\">10.1007/978-3-642-02658-4_27</a>.","short":"T.A. Henzinger, M. Mateescu, V. Wolf, in:, Springer, 2009, pp. 337–352.","chicago":"Henzinger, Thomas A, Maria Mateescu, and Verena Wolf. “Sliding-Window Abstraction for Infinite Markov Chains,” 5643:337–52. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-02658-4_27\">https://doi.org/10.1007/978-3-642-02658-4_27</a>.","ista":"Henzinger TA, Mateescu M, Wolf V. 2009. Sliding-window abstraction for infinite Markov chains. CAV: Computer Aided Verification, LNCS, vol. 5643, 337–352."},"acknowledgement":"The research has been partially funded by the Swiss National Science Foundation under grant 205321-111840.","intvolume":"      5643"},{"publisher":"Springer","extern":1,"publication_status":"published","date_updated":"2025-09-30T09:03:30Z","month":"08","date_published":"2009-08-17T00:00:00Z","date_created":"2018-12-11T12:09:21Z","day":"17","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.\nWe 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."}],"conference":{"name":"CMSB: Computational Methods in Systems Biology"},"related_material":{"record":[{"status":"public","id":"3364","relation":"later_version"}]},"title":"Approximation of event probabilities in noisy cellular processes","volume":5688,"citation":{"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. <a href=\"https://doi.org/10.1007/978-3-642-03845-7_12\">https://doi.org/10.1007/978-3-642-03845-7_12</a>.","short":"F. Didier, T.A. Henzinger, M. Mateescu, V. Wolf, in:, Springer, 2009, 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.","apa":"Didier, F., Henzinger, T. A., Mateescu, M., &#38; 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. <a href=\"https://doi.org/10.1007/978-3-642-03845-7_12\">https://doi.org/10.1007/978-3-642-03845-7_12</a>","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:<a href=\"https://doi.org/10.1007/978-3-642-03845-7_12\">10.1007/978-3-642-03845-7_12</a>","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.","mla":"Didier, Frédéric, et al. <i>Approximation of Event Probabilities in Noisy Cellular Processes</i>. Vol. 5688, Springer, 2009, pp. 173–88, doi:<a href=\"https://doi.org/10.1007/978-3-642-03845-7_12\">10.1007/978-3-642-03845-7_12</a>."},"alternative_title":["LNCS"],"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.","intvolume":"      5688","type":"conference","publist_id":"189","_id":"4535","doi":"10.1007/978-3-642-03845-7_12","quality_controlled":0,"year":"2009","page":"173 - 188","status":"public","author":[{"last_name":"Didier","full_name":"Didier, Frédéric","first_name":"Frédéric"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Thomas Henzinger"},{"last_name":"Mateescu","first_name":"Maria","full_name":"Maria Mateescu","id":"3B43276C-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Verena","full_name":"Wolf, Verena","last_name":"Wolf"}]},{"date_published":"2009-01-01T00:00:00Z","month":"01","extern":"1","publication_status":"published","scopus_import":"1","date_updated":"2025-09-30T09:30:59Z","pubrep_id":"55","publisher":"IEEE","title":"Expressiveness and closure properties for quantitative languages","related_material":{"record":[{"status":"public","id":"3867","relation":"later_version"}]},"language":[{"iso":"eng"}],"conference":{"name":"LICS: Logic in Computer Science"},"article_processing_charge":"No","abstract":[{"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.","lang":"eng"}],"day":"01","date_created":"2018-12-11T12:09:23Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","publist_id":"181","citation":{"ista":"Chatterjee K, Doyen L, Henzinger TA. 2009. Expressiveness and closure properties for quantitative languages. LICS: Logic in Computer Science, 199–208.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, IEEE, 2009, pp. 199–208.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Expressiveness and Closure Properties for Quantitative Languages,” 199–208. IEEE, 2009. <a href=\"https://doi.org/10.1109/LICS.2009.16\">https://doi.org/10.1109/LICS.2009.16</a>.","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.","mla":"Chatterjee, Krishnendu, et al. <i>Expressiveness and Closure Properties for Quantitative Languages</i>. IEEE, 2009, pp. 199–208, doi:<a href=\"https://doi.org/10.1109/LICS.2009.16\">10.1109/LICS.2009.16</a>.","ama":"Chatterjee K, Doyen L, Henzinger TA. Expressiveness and closure properties for quantitative languages. In: IEEE; 2009:199-208. doi:<a href=\"https://doi.org/10.1109/LICS.2009.16\">10.1109/LICS.2009.16</a>","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2009). Expressiveness and closure properties for quantitative languages (pp. 199–208). Presented at the LICS: Logic in Computer Science, IEEE. <a href=\"https://doi.org/10.1109/LICS.2009.16\">https://doi.org/10.1109/LICS.2009.16</a>"},"oa_version":"None","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724"}],"year":"2009","status":"public","page":"199 - 208","quality_controlled":"1","doi":"10.1109/LICS.2009.16","_id":"4540"},{"project":[{"grant_number":"214373","call_identifier":"FP7","name":"Design for Embedded Systems","_id":"25F1337C-B435-11E9-9278-68D0E5697425"},{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543","call_identifier":"FP7","name":"COMponent-Based Embedded Systems design Techniques"}],"_id":"4542","doi":"10.1007/978-3-642-03409-1_2","page":"3 - 13","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"quality_controlled":"1","intvolume":"      5699","ddc":["004"],"citation":{"chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Alternating Weighted Automata,” 5699:3–13. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-03409-1_2\">https://doi.org/10.1007/978-3-642-03409-1_2</a>.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, Springer, 2009, pp. 3–13.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2009. Alternating weighted automata. FCT: Fundamentals of Computation Theory, LNCS, vol. 5699, 3–13.","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2009). Alternating weighted automata (Vol. 5699, pp. 3–13). Presented at the FCT: Fundamentals of Computation Theory, Wroclaw, Poland: Springer. <a href=\"https://doi.org/10.1007/978-3-642-03409-1_2\">https://doi.org/10.1007/978-3-642-03409-1_2</a>","ama":"Chatterjee K, Doyen L, Henzinger TA. Alternating weighted automata. In: Vol 5699. Springer; 2009:3-13. doi:<a href=\"https://doi.org/10.1007/978-3-642-03409-1_2\">10.1007/978-3-642-03409-1_2</a>","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.","mla":"Chatterjee, Krishnendu, et al. <i>Alternating Weighted Automata</i>. Vol. 5699, Springer, 2009, pp. 3–13, doi:<a href=\"https://doi.org/10.1007/978-3-642-03409-1_2\">10.1007/978-3-642-03409-1_2</a>."},"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.","publist_id":"180","type":"conference","date_created":"2018-12-11T12:09:23Z","day":"10","abstract":[{"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.","lang":"eng"}],"volume":5699,"file_date_updated":"2020-07-14T12:46:31Z","language":[{"iso":"eng"}],"title":"Alternating weighted automata","pubrep_id":"39","scopus_import":1,"has_accepted_license":"1","corr_author":"1","year":"2009","status":"public","oa_version":"Submitted Version","file":[{"file_size":164428,"access_level":"open_access","checksum":"e8f53abb63579de3f2bff58b2a1188e2","content_type":"application/pdf","creator":"system","date_updated":"2020-07-14T12:46:31Z","date_created":"2018-12-12T10:15:09Z","file_name":"IST-2012-39-v1+1_Alternating_Weighted_Automata.pdf","relation":"main_file","file_id":"5126"}],"alternative_title":["LNCS"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"conference":{"start_date":"2009-09-02","name":"FCT: Fundamentals of Computation Theory","end_date":"2009-09-04","location":"Wroclaw, Poland"},"oa":1,"ec_funded":1,"publisher":"Springer","publication_status":"published","date_updated":"2024-10-09T20:53:55Z","date_published":"2009-09-10T00:00:00Z","month":"09"},{"corr_author":"1","status":"public","year":"2009","oa_version":"None","alternative_title":["LNCS"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"location":"High Tatras, Slovakia","end_date":"2009-08-28","name":"MFCS: Mathematical Foundations of Computer Science","start_date":"2009-08-24"},"department":[{"_id":"KrCh"}],"publisher":"Springer","ec_funded":1,"publication_status":"published","date_updated":"2024-10-09T20:53:54Z","month":"08","date_published":"2009-08-01T00:00:00Z","_id":"4543","doi":"10.1007/978-3-642-03816-7_4","project":[{"_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques"},{"grant_number":"214373","call_identifier":"FP7","name":"Design for Embedded Systems","_id":"25F1337C-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","page":"34 - 54","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"37327ACE-F248-11E8-B48F-1D18A9856A87","full_name":"Horn, Florian","first_name":"Florian","last_name":"Horn"}],"citation":{"ista":"Chatterjee K, Henzinger TA, Horn F. 2009. Stochastic games with finitary objectives. MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 5734, 34–54.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Florian Horn. “Stochastic Games with Finitary Objectives,” 5734:34–54. Springer, 2009. <a href=\"https://doi.org/10.1007/978-3-642-03816-7_4\">https://doi.org/10.1007/978-3-642-03816-7_4</a>.","short":"K. Chatterjee, T.A. Henzinger, F. Horn, in:, Springer, 2009, pp. 34–54.","mla":"Chatterjee, Krishnendu, et al. <i>Stochastic Games with Finitary Objectives</i>. Vol. 5734, Springer, 2009, pp. 34–54, doi:<a href=\"https://doi.org/10.1007/978-3-642-03816-7_4\">10.1007/978-3-642-03816-7_4</a>.","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.","apa":"Chatterjee, K., Henzinger, T. A., &#38; 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. <a href=\"https://doi.org/10.1007/978-3-642-03816-7_4\">https://doi.org/10.1007/978-3-642-03816-7_4</a>","ama":"Chatterjee K, Henzinger TA, Horn F. Stochastic games with finitary objectives. In: Vol 5734. Springer; 2009:34-54. doi:<a href=\"https://doi.org/10.1007/978-3-642-03816-7_4\">10.1007/978-3-642-03816-7_4</a>"},"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.","intvolume":"      5734","type":"conference","publist_id":"178","date_created":"2018-12-11T12:09:24Z","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."}],"day":"01","language":[{"iso":"eng"}],"title":"Stochastic games with finitary objectives","volume":5734,"scopus_import":1},{"page":"197 - 206","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Krishnendu Chatterjee","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"last_name":"De Alfaro","full_name":"de Alfaro, Luca","first_name":"Luca"},{"first_name":"Thomas A","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger"}],"status":"public","year":"2009","quality_controlled":0,"_id":"4544","doi":"10.1137/1.9781611973068.23","publist_id":"176","type":"conference","file":[{"file_id":"4662","relation":"main_file","date_created":"2018-12-12T10:08:03Z","file_name":"IST-2012-37-v1+1_Termination_criteria_for_solving_concurrent_safety_and_reachability_games.pdf","date_updated":"2020-07-14T12:46:31Z","file_size":212369,"content_type":"application/pdf","access_level":"open_access","checksum":"ce7dc1667502e26b23c07a767ac41ae6","creator":"system"}],"citation":{"apa":"Chatterjee, K., De Alfaro, L., &#38; 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. <a href=\"https://doi.org/10.1137/1.9781611973068.23\">https://doi.org/10.1137/1.9781611973068.23</a>","ama":"Chatterjee K, De Alfaro L, Henzinger TA. Termination criteria for solving concurrent safety and reachability games. In: SIAM; 2009:197-206. doi:<a href=\"https://doi.org/10.1137/1.9781611973068.23\">10.1137/1.9781611973068.23</a>","mla":"Chatterjee, Krishnendu, et al. <i>Termination Criteria for Solving Concurrent Safety and Reachability Games</i>. SIAM, 2009, pp. 197–206, doi:<a href=\"https://doi.org/10.1137/1.9781611973068.23\">10.1137/1.9781611973068.23</a>.","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.","chicago":"Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Termination Criteria for Solving Concurrent Safety and Reachability Games,” 197–206. SIAM, 2009. <a href=\"https://doi.org/10.1137/1.9781611973068.23\">https://doi.org/10.1137/1.9781611973068.23</a>.","short":"K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, SIAM, 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."},"file_date_updated":"2020-07-14T12:46:31Z","main_file_link":[{"url":"https://repository.ist.ac.at/id/eprint/37","open_access":"1"}],"oa":1,"title":"Termination criteria for solving concurrent safety and reachability games","conference":{"name":"SODA: Symposium on Discrete Algorithms"},"date_created":"2018-12-11T12:09:24Z","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."}],"day":"01","date_updated":"2021-01-12T07:59:35Z","extern":1,"publication_status":"published","date_published":"2009-01-01T00:00:00Z","month":"01","publisher":"SIAM","pubrep_id":"37"}]