[{"author":[{"full_name":"Campbell, C. J.","first_name":"C. J.","last_name":"Campbell"},{"first_name":"M.","last_name":"Fialkowski","full_name":"Fialkowski, M."},{"full_name":"Klajn, Rafal","first_name":"Rafal","last_name":"Klajn","id":"8e84690e-1e48-11ed-a02b-a1e6fb8bb53b"},{"full_name":"Bensemann, I. T.","first_name":"I. T.","last_name":"Bensemann"},{"first_name":"B. A.","last_name":"Grzybowski","full_name":"Grzybowski, B. A."}],"_id":"13434","publication":"Advanced Materials","publication_identifier":{"issn":["0935-9648"],"eissn":["1521-4095"]},"date_published":"2004-11-14T00:00:00Z","doi":"10.1002/adma.200400383","language":[{"iso":"eng"}],"article_processing_charge":"No","extern":"1","date_updated":"2023-08-08T12:41:23Z","abstract":[{"text":"Thin films of ionically doped gelatin have been color-patterned with submicrometer precision using the wet-stamping technique. Inorganic salts are delivered onto the gelatin surface from an agarose stamp, and diffuse into the gelatine layer, producting deeply colored precipitates. Reaction fronts originating from different features of the stamp cease within < 1 μm of each other, leaving sharp, transparent regions in between.","lang":"eng"}],"month":"11","status":"public","article_type":"original","intvolume":"        16","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"None","quality_controlled":"1","citation":{"ama":"Campbell CJ, Fialkowski M, Klajn R, Bensemann IT, Grzybowski BA. Color micro- and nanopatterning with counter-propagating reaction-diffusion fronts. <i>Advanced Materials</i>. 2004;16(21):1912-1917. doi:<a href=\"https://doi.org/10.1002/adma.200400383\">10.1002/adma.200400383</a>","short":"C.J. Campbell, M. Fialkowski, R. Klajn, I.T. Bensemann, B.A. Grzybowski, Advanced Materials 16 (2004) 1912–1917.","apa":"Campbell, C. J., Fialkowski, M., Klajn, R., Bensemann, I. T., &#38; Grzybowski, B. A. (2004). Color micro- and nanopatterning with counter-propagating reaction-diffusion fronts. <i>Advanced Materials</i>. Wiley. <a href=\"https://doi.org/10.1002/adma.200400383\">https://doi.org/10.1002/adma.200400383</a>","ista":"Campbell CJ, Fialkowski M, Klajn R, Bensemann IT, Grzybowski BA. 2004. Color micro- and nanopatterning with counter-propagating reaction-diffusion fronts. Advanced Materials. 16(21), 1912–1917.","chicago":"Campbell, C. J., M. Fialkowski, Rafal Klajn, I. T. Bensemann, and B. A. Grzybowski. “Color Micro- and Nanopatterning with Counter-Propagating Reaction-Diffusion Fronts.” <i>Advanced Materials</i>. Wiley, 2004. <a href=\"https://doi.org/10.1002/adma.200400383\">https://doi.org/10.1002/adma.200400383</a>.","mla":"Campbell, C. J., et al. “Color Micro- and Nanopatterning with Counter-Propagating Reaction-Diffusion Fronts.” <i>Advanced Materials</i>, vol. 16, no. 21, Wiley, 2004, pp. 1912–17, doi:<a href=\"https://doi.org/10.1002/adma.200400383\">10.1002/adma.200400383</a>.","ieee":"C. J. Campbell, M. Fialkowski, R. Klajn, I. T. Bensemann, and B. A. Grzybowski, “Color micro- and nanopatterning with counter-propagating reaction-diffusion fronts,” <i>Advanced Materials</i>, vol. 16, no. 21. Wiley, pp. 1912–1917, 2004."},"volume":16,"date_created":"2023-08-01T10:39:09Z","scopus_import":"1","day":"14","publication_status":"published","publisher":"Wiley","page":"1912-1917","year":"2004","title":"Color micro- and nanopatterning with counter-propagating reaction-diffusion fronts","keyword":["Mechanical Engineering","Mechanics of Materials","General Materials Science"],"type":"journal_article","issue":"21"},{"day":"19","scopus_import":"1","volume":3,"date_created":"2023-08-01T10:39:23Z","citation":{"chicago":"Klajn, Rafal, Marcin Fialkowski, Igor T. Bensemann, Agnieszka Bitner, C. J. Campbell, Kyle Bishop, Stoyan Smoukov, and Bartosz A. Grzybowski. “Multicolour Micropatterning of Thin Films of Dry Gels.” <i>Nature Materials</i>. Springer Nature, 2004. <a href=\"https://doi.org/10.1038/nmat1231\">https://doi.org/10.1038/nmat1231</a>.","mla":"Klajn, Rafal, et al. “Multicolour Micropatterning of Thin Films of Dry Gels.” <i>Nature Materials</i>, vol. 3, Springer Nature, 2004, pp. 729–35, doi:<a href=\"https://doi.org/10.1038/nmat1231\">10.1038/nmat1231</a>.","short":"R. Klajn, M. Fialkowski, I.T. Bensemann, A. Bitner, C.J. Campbell, K. Bishop, S. Smoukov, B.A. Grzybowski, Nature Materials 3 (2004) 729–735.","ama":"Klajn R, Fialkowski M, Bensemann IT, et al. Multicolour micropatterning of thin films of dry gels. <i>Nature Materials</i>. 2004;3:729-735. doi:<a href=\"https://doi.org/10.1038/nmat1231\">10.1038/nmat1231</a>","ista":"Klajn R, Fialkowski M, Bensemann IT, Bitner A, Campbell CJ, Bishop K, Smoukov S, Grzybowski BA. 2004. Multicolour micropatterning of thin films of dry gels. Nature Materials. 3, 729–735.","apa":"Klajn, R., Fialkowski, M., Bensemann, I. T., Bitner, A., Campbell, C. J., Bishop, K., … Grzybowski, B. A. (2004). Multicolour micropatterning of thin films of dry gels. <i>Nature Materials</i>. Springer Nature. <a href=\"https://doi.org/10.1038/nmat1231\">https://doi.org/10.1038/nmat1231</a>","ieee":"R. Klajn <i>et al.</i>, “Multicolour micropatterning of thin films of dry gels,” <i>Nature Materials</i>, vol. 3. Springer Nature, pp. 729–735, 2004."},"title":"Multicolour micropatterning of thin films of dry gels","type":"journal_article","keyword":["Mechanical Engineering","Mechanics of Materials","Condensed Matter Physics","General Materials Science","General Chemistry"],"page":"729-735","year":"2004","publication_status":"published","publisher":"Springer Nature","article_processing_charge":"No","extern":"1","date_published":"2004-09-19T00:00:00Z","doi":"10.1038/nmat1231","language":[{"iso":"eng"}],"publication_identifier":{"eissn":["1476-4660"],"issn":["1476-1122"]},"publication":"Nature Materials","author":[{"id":"8e84690e-1e48-11ed-a02b-a1e6fb8bb53b","full_name":"Klajn, Rafal","first_name":"Rafal","last_name":"Klajn"},{"last_name":"Fialkowski","first_name":"Marcin","full_name":"Fialkowski, Marcin"},{"first_name":"Igor T.","last_name":"Bensemann","full_name":"Bensemann, Igor T."},{"full_name":"Bitner, Agnieszka","first_name":"Agnieszka","last_name":"Bitner"},{"full_name":"Campbell, C. J.","first_name":"C. J.","last_name":"Campbell"},{"full_name":"Bishop, Kyle","last_name":"Bishop","first_name":"Kyle"},{"last_name":"Smoukov","first_name":"Stoyan","full_name":"Smoukov, Stoyan"},{"last_name":"Grzybowski","first_name":"Bartosz A.","full_name":"Grzybowski, Bartosz A."}],"_id":"13435","oa_version":"None","quality_controlled":"1","status":"public","article_type":"original","intvolume":"         3","pmid":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","external_id":{"pmid":["15378052"]},"date_updated":"2023-08-08T12:42:51Z","abstract":[{"text":"Micropatterning of surfaces with several chemicals at different spatial locations usually requires multiple stamping and registration steps. Here, we describe an experimental method based on reaction–diffusion phenomena that allows for simultaneous micropatterning of a substrate with several coloured chemicals. In this method, called wet stamping (WETS), aqueous solutions of two or more inorganic salts are delivered onto a film of dry, ionically doped gelatin from an agarose stamp patterned in bas relief. Once in conformal contact, these salts diffuse into the gelatin, where they react to give deeply coloured precipitates. Separation of colours in the plane of the surface is the consequence of the differences in the diffusion coefficients, the solubility products, and the amounts of different salts delivered from the stamp, and is faithfully reproduced by a theoretical model based on a system of reaction–diffusion partial differential equations. The multicolour micropatterns are useful as non-binary optical elements, and could potentially form the basis of new applications in microseparations and in controlled delivery.","lang":"eng"}],"month":"09"},{"intvolume":"       122","oa":1,"title":"Hodge cohomology of gravitational instantons","status":"public","type":"journal_article","issue":"3","quality_controlled":0,"publisher":"Duke University Press","month":"04","publication_status":"published","date_updated":"2021-01-12T06:50:52Z","abstract":[{"lang":"eng","text":"We study the space of L2 harmonic forms on complete manifolds with metrics of fibred boundary or fibred cusp type. These metrics generalize the geometric structures at infinity of several different well-known classes of metrics, including asymptotically locally Euclidean manifolds, the (known types of) gravitational instantons, and also Poincaré metrics on ℚ-rank 1 ends of locally symmetric spaces and on the complements of smooth divisors in Kähler manifolds. The answer in all cases is given in terms of intersection cohomology of a stratified compactification of the manifold. The L2 signature formula implied by our result is closely related to the one proved by Dai and more generally by Vaillant and identifies Dai's τ-invariant directly in terms of intersection cohomology of differing perversities. This work is also closely related to a recent paper of Carron and the forthcoming paper of Cheeger and Dai. We apply our results to a number of examples, gravitational instantons among them, arising in predictions about L2 harmonic forms in duality theories in string theory."}],"page":"485 - 548","year":"2004","publist_id":"5737","acknowledgement":"Hausel’s work supported by a Miller Research Fellowship at the University of California, Berkeley.\nHunsicker’s work partially supported by Stanford University.\nMazzeo’s work supported by National Science Foundation grant numbers DMS-991975 and DMS-0204730 and\nby the Mathematical Sciences Research Institute.","date_published":"2004-04-15T00:00:00Z","doi":"10.1215/S0012-7094-04-12233-X","extern":1,"day":"15","citation":{"ieee":"T. Hausel, E. Hunsicker, and R. Mazzeo, “Hodge cohomology of gravitational instantons,” <i>Duke Mathematical Journal</i>, vol. 122, no. 3. Duke University Press, pp. 485–548, 2004.","ama":"Hausel T, Hunsicker E, Mazzeo R. Hodge cohomology of gravitational instantons. <i>Duke Mathematical Journal</i>. 2004;122(3):485-548. doi:<a href=\"https://doi.org/10.1215/S0012-7094-04-12233-X\">10.1215/S0012-7094-04-12233-X</a>","short":"T. Hausel, E. Hunsicker, R. Mazzeo, Duke Mathematical Journal 122 (2004) 485–548.","ista":"Hausel T, Hunsicker E, Mazzeo R. 2004. Hodge cohomology of gravitational instantons. Duke Mathematical Journal. 122(3), 485–548.","apa":"Hausel, T., Hunsicker, E., &#38; Mazzeo, R. (2004). Hodge cohomology of gravitational instantons. <i>Duke Mathematical Journal</i>. Duke University Press. <a href=\"https://doi.org/10.1215/S0012-7094-04-12233-X\">https://doi.org/10.1215/S0012-7094-04-12233-X</a>","chicago":"Hausel, Tamás, Eugénie Hunsicker, and Rafe Mazzeo. “Hodge Cohomology of Gravitational Instantons.” <i>Duke Mathematical Journal</i>. Duke University Press, 2004. <a href=\"https://doi.org/10.1215/S0012-7094-04-12233-X\">https://doi.org/10.1215/S0012-7094-04-12233-X</a>.","mla":"Hausel, Tamás, et al. “Hodge Cohomology of Gravitational Instantons.” <i>Duke Mathematical Journal</i>, vol. 122, no. 3, Duke University Press, 2004, pp. 485–548, doi:<a href=\"https://doi.org/10.1215/S0012-7094-04-12233-X\">10.1215/S0012-7094-04-12233-X</a>."},"_id":"1456","author":[{"id":"4A0666D8-F248-11E8-B48F-1D18A9856A87","full_name":"Tamas Hausel","first_name":"Tamas","last_name":"Hausel"},{"full_name":"Hunsicker, Eugénie","first_name":"Eugénie","last_name":"Hunsicker"},{"last_name":"Mazzeo","first_name":"Rafe","full_name":"Mazzeo, Rafe R"}],"publication":"Duke Mathematical Journal","volume":122,"date_created":"2018-12-11T11:52:08Z","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/math/0207169"}]},{"quality_controlled":0,"issue":"3","intvolume":"        88","oa":1,"title":"Generators for the cohomology ring of the moduli space of rank 2 higgs bundles","status":"public","type":"journal_article","page":"632 - 658","year":"2004","publist_id":"5736","publisher":"Oxford University Press","month":"05","publication_status":"published","date_updated":"2021-01-12T06:50:55Z","abstract":[{"lang":"eng","text":"The moduli space of stable vector bundles on a Riemann surface is smooth when the rank and degree are coprime, and is diffeomorphic to the space of unitary connections of central constant curvature. A classic result of Newstead and Atiyah and Bott asserts that its rational cohomology ring is generated by the universal classes, that is, by the Kunneth components of the Chern classes of the universal bundle.\n\nThis paper studies the larger, non-compact moduli space of Higgs bundles, as introduced by Hitchin and Simpson, with values in the canonical bundle K. This is diffeomorphic to the space of all connections of central constant curvature, whether unitary or not. The main result of the paper is that, in the rank 2 case, the rational cohomology ring of this space is again generated by universal classes.\n\nThe spaces of Higgs bundles with values in K(n) for n &gt; 0 turn out to be essential to the story. Indeed, we show that their direct limit has the homotopy type of the classifying space of the gauge group, and hence has cohomology generated by universal classes. 2000 Mathematics Subject Classification 14H60 (primary), 14D20, 14H81, 32Q55, 58D27 (secondary). "}],"extern":1,"day":"01","date_published":"2004-05-01T00:00:00Z","doi":"10.1112/S0024611503014618","publication":"Proceedings of the London Mathematical Society","volume":88,"date_created":"2018-12-11T11:52:10Z","main_file_link":[{"url":"http://arxiv.org/abs/math/0003093","open_access":"1"}],"citation":{"apa":"Hausel, T., &#38; Thaddeus, M. (2004). Generators for the cohomology ring of the moduli space of rank 2 higgs bundles. <i>Proceedings of the London Mathematical Society</i>. Oxford University Press. <a href=\"https://doi.org/10.1112/S0024611503014618\">https://doi.org/10.1112/S0024611503014618</a>","ista":"Hausel T, Thaddeus M. 2004. Generators for the cohomology ring of the moduli space of rank 2 higgs bundles. Proceedings of the London Mathematical Society. 88(3), 632–658.","short":"T. Hausel, M. Thaddeus, Proceedings of the London Mathematical Society 88 (2004) 632–658.","ama":"Hausel T, Thaddeus M. Generators for the cohomology ring of the moduli space of rank 2 higgs bundles. <i>Proceedings of the London Mathematical Society</i>. 2004;88(3):632-658. doi:<a href=\"https://doi.org/10.1112/S0024611503014618\">10.1112/S0024611503014618</a>","mla":"Hausel, Tamás, and Michael Thaddeus. “Generators for the Cohomology Ring of the Moduli Space of Rank 2 Higgs Bundles.” <i>Proceedings of the London Mathematical Society</i>, vol. 88, no. 3, Oxford University Press, 2004, pp. 632–58, doi:<a href=\"https://doi.org/10.1112/S0024611503014618\">10.1112/S0024611503014618</a>.","chicago":"Hausel, Tamás, and Michael Thaddeus. “Generators for the Cohomology Ring of the Moduli Space of Rank 2 Higgs Bundles.” <i>Proceedings of the London Mathematical Society</i>. Oxford University Press, 2004. <a href=\"https://doi.org/10.1112/S0024611503014618\">https://doi.org/10.1112/S0024611503014618</a>.","ieee":"T. Hausel and M. Thaddeus, “Generators for the cohomology ring of the moduli space of rank 2 higgs bundles,” <i>Proceedings of the London Mathematical Society</i>, vol. 88, no. 3. Oxford University Press, pp. 632–658, 2004."},"_id":"1464","author":[{"full_name":"Tamas Hausel","last_name":"Hausel","first_name":"Tamas","id":"4A0666D8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Thaddeus, Michael","first_name":"Michael","last_name":"Thaddeus"}]},{"date_created":"2025-01-03T12:33:47Z","volume":308,"main_file_link":[{"url":"https://arxiv.org/abs/astro-ph/0403225","open_access":"1"}],"series_title":"ASSL","OA_type":"green","citation":{"ieee":"Z. Haiman and E. Quataert, “The Formation and Evolution of the First Massive Black Holes,” in <i>Supermassive Black Holes in the Distant Universe</i>, vol. 308, Springer Nature, 2004, pp. 147–185.","ama":"Haiman Z, Quataert E. The Formation and Evolution of the First Massive Black Holes. In: <i>Supermassive Black Holes in the Distant Universe</i>. Vol 308. ASSL. Springer Nature; 2004:147-185. doi:<a href=\"https://doi.org/10.1007/978-1-4020-2471-9_5\">10.1007/978-1-4020-2471-9_5</a>","short":"Z. Haiman, E. Quataert, in:, Supermassive Black Holes in the Distant Universe, Springer Nature, 2004, pp. 147–185.","apa":"Haiman, Z., &#38; Quataert, E. (2004). The Formation and Evolution of the First Massive Black Holes. In <i>Supermassive Black Holes in the Distant Universe</i> (Vol. 308, pp. 147–185). Springer Nature. <a href=\"https://doi.org/10.1007/978-1-4020-2471-9_5\">https://doi.org/10.1007/978-1-4020-2471-9_5</a>","ista":"Haiman Z, Quataert E. 2004.The Formation and Evolution of the First Massive Black Holes. In: Supermassive Black Holes in the Distant Universe. Astrophysics and Space Science Library, vol. 308, 147–185.","chicago":"Haiman, Zoltán, and Eliot Quataert. “The Formation and Evolution of the First Massive Black Holes.” In <i>Supermassive Black Holes in the Distant Universe</i>, 308:147–85. ASSL. Springer Nature, 2004. <a href=\"https://doi.org/10.1007/978-1-4020-2471-9_5\">https://doi.org/10.1007/978-1-4020-2471-9_5</a>.","mla":"Haiman, Zoltán, and Eliot Quataert. “The Formation and Evolution of the First Massive Black Holes.” <i>Supermassive Black Holes in the Distant Universe</i>, vol. 308, Springer Nature, 2004, pp. 147–85, doi:<a href=\"https://doi.org/10.1007/978-1-4020-2471-9_5\">10.1007/978-1-4020-2471-9_5</a>."},"day":"03","scopus_import":"1","year":"2004","page":"147-185","publisher":"Springer Nature","publication_status":"published","type":"book_chapter","title":"The Formation and Evolution of the First Massive Black Holes","publication_identifier":{"isbn":["9789048166626"],"issn":["0067-0057"],"eisbn":["9781402024719"]},"publication":"Supermassive Black Holes in the Distant Universe","_id":"18739","alternative_title":["Astrophysics and Space Science Library"],"author":[{"first_name":"Zoltán","last_name":"Haiman","orcid":"0000-0003-3633-5403","full_name":"Haiman, Zoltán","id":"7c006e8c-cc0d-11ee-8322-cb904ef76f36"},{"first_name":"Eliot","last_name":"Quataert","full_name":"Quataert, Eliot"}],"article_processing_charge":"No","extern":"1","OA_place":"repository","language":[{"iso":"eng"}],"doi":"10.1007/978-1-4020-2471-9_5","date_published":"2004-08-03T00:00:00Z","external_id":{"arxiv":["astro-ph/0403225"]},"month":"08","abstract":[{"lang":"eng","text":"The first massive astrophysical black holes likely formed at high redshifts (z≳ 10) at the centers of low mass (~ 106 M⊙) dark matter concentrations. These black holes grow by mergers and gas accretion, evolve into the population of bright quasars observed at lower redshifts, and eventually leave the supermassive black hole remnants that are ubiquitous at the centers of galaxies in the nearby universe. The astrophysical processes responsible for the formation of the earliest seed black holes are poorly understood. The purpose of this review is threefold: (1) to describe theoretical expectations for the formation and growth of the earliest black holes within the general paradigm of hierarchical cold dark matter cosmologies, (2) to summarize several relevant recent observations that have implications for the formation of the earliest black holes, and (3) to look into the future and assess the power of forthcoming observations to probe the physics of the first active galactic nuclei."}],"date_updated":"2025-01-07T13:46:38Z","arxiv":1,"quality_controlled":"1","oa_version":"Preprint","oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":"       308","status":"public"},{"extern":"1","OA_place":"repository","article_processing_charge":"No","language":[{"iso":"eng"}],"date_published":"2004-11-01T00:00:00Z","doi":"10.1086/423951","publication":"The Astrophysical Journal","publication_identifier":{"eissn":["1538-4357"],"issn":["0004-637X"]},"_id":"18742","author":[{"first_name":"Kristen","last_name":"Menou","full_name":"Menou, Kristen"},{"id":"7c006e8c-cc0d-11ee-8322-cb904ef76f36","full_name":"Haiman, Zoltán","orcid":"0000-0003-3633-5403","last_name":"Haiman","first_name":"Zoltán"}],"arxiv":1,"oa_version":"Preprint","quality_controlled":"1","intvolume":"       615","oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","article_type":"original","external_id":{"arxiv":["astro-ph/0405335"]},"month":"11","abstract":[{"text":"Recent improved determinations of the mass density ρBH of supermassive black holes (SMBHs) in the local universe have allowed accurate comparisons of ρBH with the amount of light received from past quasar activity. These comparisons support the notion that local SMBHs are \"dead quasars\" and yield a value epsilon ≳ 0.1 for the average radiative efficiency of cosmic SMBH accretion. BH coalescences may represent an important component of the quasar mass assembly and yet not produce any observable electromagnetic signature. Therefore, ignoring gravitational wave (GW) emission during such coalescences, which reduces the amount of mass locked into remnant BHs, results in an overestimate of epsilon. Here we put constraints on the magnitude of this bias. We calculate the cumulative mass loss to GWs experienced by a representative population of BHs during repeated cosmological mergers, using loss prescriptions based on detailed general relativistic calculations. Despite the possibly large number of mergers in the assembly history of each individual SMBH, we find that near-equal mass mergers are rare; therefore, the cumulative loss is likely to be modest, amounting at most to a 20% increase in the inferred epsilon value. Thus, recent estimates of epsilon ≳ 0.1 appear robust. The space interferometer LISA should provide empirical constraints on the dark side of quasar evolution by measuring the masses and rates of coalescence of massive BHs to cosmological distances.","lang":"eng"}],"date_updated":"2025-01-07T14:02:29Z","day":"01","scopus_import":"1","volume":615,"date_created":"2025-01-03T12:34:57Z","main_file_link":[{"url":"https://arxiv.org/abs/astro-ph/0405335","open_access":"1"}],"citation":{"ista":"Menou K, Haiman Z. 2004. On the dark side of quasar evolution. The Astrophysical Journal. 615(1), 130–134.","apa":"Menou, K., &#38; Haiman, Z. (2004). On the dark side of quasar evolution. <i>The Astrophysical Journal</i>. American Astronomical Society. <a href=\"https://doi.org/10.1086/423951\">https://doi.org/10.1086/423951</a>","ama":"Menou K, Haiman Z. On the dark side of quasar evolution. <i>The Astrophysical Journal</i>. 2004;615(1):130-134. doi:<a href=\"https://doi.org/10.1086/423951\">10.1086/423951</a>","short":"K. Menou, Z. Haiman, The Astrophysical Journal 615 (2004) 130–134.","mla":"Menou, Kristen, and Zoltán Haiman. “On the Dark Side of Quasar Evolution.” <i>The Astrophysical Journal</i>, vol. 615, no. 1, American Astronomical Society, 2004, pp. 130–34, doi:<a href=\"https://doi.org/10.1086/423951\">10.1086/423951</a>.","chicago":"Menou, Kristen, and Zoltán Haiman. “On the Dark Side of Quasar Evolution.” <i>The Astrophysical Journal</i>. American Astronomical Society, 2004. <a href=\"https://doi.org/10.1086/423951\">https://doi.org/10.1086/423951</a>.","ieee":"K. Menou and Z. Haiman, “On the dark side of quasar evolution,” <i>The Astrophysical Journal</i>, vol. 615, no. 1. American Astronomical Society, pp. 130–134, 2004."},"OA_type":"green","issue":"1","title":"On the dark side of quasar evolution","type":"journal_article","year":"2004","page":"130-134","publisher":"American Astronomical Society","publication_status":"published"},{"quality_controlled":0,"issue":"22","type":"journal_article","status":"public","title":"Substrate-induced conformational change in bacterial complex I","intvolume":"       279","publist_id":"5123","page":"23830 - 23836","year":"2004","abstract":[{"lang":"eng","text":"The mechanism coupling electron transfer and proton pumping in respiratory complex I (NADH-ubiquinone oxidoreductase) has not been established, but it has been suggested that it involves conformational changes. Here, the influence of substrates on the conformation of purified complex I from Escherichia coli was studied by cross-linking and electron microscopy. When a zero-length cross-linking reagent was used, the presence of NAD(P)H, in contrast to that of NAD+, prevented the formation of cross-links between the hydrophilic subunits of the complex, including NuoB, NuoI, and NuoCD. Comparisons using different cross-linkers suggested that NuoB, which is likely to coordinate the key iron-sulfur cluster N2, is the most mobile subunit. The presence of NAD(P)H led also to enhanced proteolysis of subunit NuoG. These data indicate that upon NAD(P)H binding, the peripheral arm of the complex adopts a more open conformation, with increased distances between subunits. Single particle analysis showed the nature of this conformational change. The enzyme retains its L-shape in the presence of NADH, but exhibits a significantly more open or expanded structure both in the peripheral arm and, unexpectedly, in the membrane domain also."}],"date_updated":"2021-01-12T06:54:22Z","publication_status":"published","month":"05","publisher":"American Society for Biochemistry and Molecular Biology","day":"28","extern":1,"doi":"10.1074/jbc.M401539200","date_published":"2004-05-28T00:00:00Z","acknowledgement":"This work was supported by the Medical Research Council and by a Royal Society/North Atlantic Treaty Organization postdoctoral fellowship (to A. A. M.)","date_created":"2018-12-11T11:54:56Z","publication":"Journal of Biological Chemistry","volume":279,"author":[{"full_name":"Mamedova, Aygun A","first_name":"Aygun","last_name":"Mamedova"},{"full_name":"Holt, Peter J","first_name":"Peter","last_name":"Holt"},{"full_name":"Carroll, Joe D","first_name":"Joe","last_name":"Carroll"},{"id":"338D39FE-F248-11E8-B48F-1D18A9856A87","first_name":"Leonid A","last_name":"Sazanov","orcid":"0000-0002-0977-7989","full_name":"Leonid Sazanov"}],"_id":"1963","citation":{"mla":"Mamedova, Aygun, et al. “Substrate-Induced Conformational Change in Bacterial Complex I.” <i>Journal of Biological Chemistry</i>, vol. 279, no. 22, American Society for Biochemistry and Molecular Biology, 2004, pp. 23830–36, doi:<a href=\"https://doi.org/10.1074/jbc.M401539200\">10.1074/jbc.M401539200</a>.","chicago":"Mamedova, Aygun, Peter Holt, Joe Carroll, and Leonid A Sazanov. “Substrate-Induced Conformational Change in Bacterial Complex I.” <i>Journal of Biological Chemistry</i>. American Society for Biochemistry and Molecular Biology, 2004. <a href=\"https://doi.org/10.1074/jbc.M401539200\">https://doi.org/10.1074/jbc.M401539200</a>.","apa":"Mamedova, A., Holt, P., Carroll, J., &#38; Sazanov, L. A. (2004). Substrate-induced conformational change in bacterial complex I. <i>Journal of Biological Chemistry</i>. American Society for Biochemistry and Molecular Biology. <a href=\"https://doi.org/10.1074/jbc.M401539200\">https://doi.org/10.1074/jbc.M401539200</a>","ista":"Mamedova A, Holt P, Carroll J, Sazanov LA. 2004. Substrate-induced conformational change in bacterial complex I. Journal of Biological Chemistry. 279(22), 23830–23836.","ama":"Mamedova A, Holt P, Carroll J, Sazanov LA. Substrate-induced conformational change in bacterial complex I. <i>Journal of Biological Chemistry</i>. 2004;279(22):23830-23836. doi:<a href=\"https://doi.org/10.1074/jbc.M401539200\">10.1074/jbc.M401539200</a>","short":"A. Mamedova, P. Holt, J. Carroll, L.A. Sazanov, Journal of Biological Chemistry 279 (2004) 23830–23836.","ieee":"A. Mamedova, P. Holt, J. Carroll, and L. A. Sazanov, “Substrate-induced conformational change in bacterial complex I,” <i>Journal of Biological Chemistry</i>, vol. 279, no. 22. American Society for Biochemistry and Molecular Biology, pp. 23830–23836, 2004."}},{"quality_controlled":"1","oa_version":"None","type":"conference","title":"Monitoring Temporal Properties of Continuous Signals","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"1088","page":"152 - 166","year":"2004","date_updated":"2025-06-26T09:05:17Z","publication_status":"published","month":"12","publisher":"Springer","conference":{"name":"FORMATS: Formal Modeling and Analysis of Timed Systems"},"day":"14","extern":"1","article_processing_charge":"No","doi":"10.1007/978-3-540-30206-3_12","date_published":"2004-12-14T00:00:00Z","scopus_import":"1","acknowledgement":"This work was partially supported by the EC projects IST-2001-33520 CC (Control and Computation), IST-2001-35302 AMETIST (Advanced Methods for Timed Systems) and IST-2003-507219 PROSYD (Property-Based System Design).","language":[{"iso":"eng"}],"date_created":"2018-12-11T12:08:31Z","author":[{"full_name":"Maler, Oded","last_name":"Maler","first_name":"Oded"},{"id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan","first_name":"Dejan","last_name":"Nickovic"}],"_id":"4372","citation":{"ista":"Maler O, Nickovic D. 2004. Monitoring Temporal Properties of Continuous Signals. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, , 152–166.","apa":"Maler, O., &#38; Nickovic, D. (2004). Monitoring Temporal Properties of Continuous Signals (pp. 152–166). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Springer. <a href=\"https://doi.org/10.1007/978-3-540-30206-3_12\">https://doi.org/10.1007/978-3-540-30206-3_12</a>","short":"O. Maler, D. Nickovic, in:, Springer, 2004, pp. 152–166.","ama":"Maler O, Nickovic D. Monitoring Temporal Properties of Continuous Signals. In: Springer; 2004:152-166. doi:<a href=\"https://doi.org/10.1007/978-3-540-30206-3_12\">10.1007/978-3-540-30206-3_12</a>","mla":"Maler, Oded, and Dejan Nickovic. <i>Monitoring Temporal Properties of Continuous Signals</i>. Springer, 2004, pp. 152–66, doi:<a href=\"https://doi.org/10.1007/978-3-540-30206-3_12\">10.1007/978-3-540-30206-3_12</a>.","chicago":"Maler, Oded, and Dejan Nickovic. “Monitoring Temporal Properties of Continuous Signals,” 152–66. Springer, 2004. <a href=\"https://doi.org/10.1007/978-3-540-30206-3_12\">https://doi.org/10.1007/978-3-540-30206-3_12</a>.","ieee":"O. Maler and D. Nickovic, “Monitoring Temporal Properties of Continuous Signals,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, 2004, pp. 152–166."},"alternative_title":["LNCS"]},{"supervisor":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"None","type":"dissertation","title":"Program verification by lazy abstraction","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"307","page":"1 - 165","year":"2004","date_updated":"2021-01-12T07:56:52Z","abstract":[{"lang":"eng","text":"The enormous cost and ubiquity of software errors necessitates the need for techniques and tools that can precisely analyze large systems and prove that they meet given specifications, or if they don't, return counterexample behaviors showing how the system fails. Recent advances in model checking, decision procedures, program analysis and type systems, and a shift of focus to partial specifications common to several systems (e.g., memory safety and race freedom) have resulted in several practical verification methods. However, these methods are either precise or they are scalable, depending on whether they track the values of variables or only a fixed small set of dataflow facts (e.g., types), and are usually insufficient for precisely verifying large programs.\r\n\r\nWe describe a new technique called Lazy Abstraction (LA) which achieves both precision and scalability by localizing the use of precise information. LA automatically builds, explores and refines a single abstract model of the program in a way that different parts of the model exhibit different degrees of precision, namely just enough to verify the desired property. The algorithm automatically mines the information required by partitioning mechanical proofs of unsatisfiability of spurious counterexamples into Craig Interpolants. For multithreaded systems, we give a new technique based on analyzing the behavior of a single thread executing in a context which is an abstraction of the other (arbitrarily many) threads. We define novel context models and show how to automatically infer them and analyze the full system (thread + context) using LA.\r\n\r\nLA is implemented in BLAST. We have run BLAST on Windows and Linux Device Drivers to verify API conformance properties, and have used it to find (or guarantee the absence of) data races in multithreaded Networked Embedded Systems (NESC) applications. BLAST is able to prove the absence of races in several cases where earlier methods, which depend on lock-based synchronization, fail."}],"publication_status":"published","month":"12","publisher":"University of California, Berkeley","day":"01","article_processing_charge":"No","extern":"1","date_published":"2004-12-01T00:00:00Z","language":[{"iso":"eng"}],"date_created":"2018-12-11T12:08:47Z","author":[{"last_name":"Jhala","first_name":"Ranjit","full_name":"Jhala, Ranjit"}],"_id":"4424","citation":{"ieee":"R. Jhala, “Program verification by lazy abstraction,” University of California, Berkeley, 2004.","chicago":"Jhala, Ranjit. “Program Verification by Lazy Abstraction.” University of California, Berkeley, 2004.","mla":"Jhala, Ranjit. <i>Program Verification by Lazy Abstraction</i>. University of California, Berkeley, 2004, pp. 1–165.","short":"R. Jhala, Program Verification by Lazy Abstraction, University of California, Berkeley, 2004.","ama":"Jhala R. Program verification by lazy abstraction. 2004:1-165.","ista":"Jhala R. 2004. Program verification by lazy abstraction. University of California, Berkeley.","apa":"Jhala, R. (2004). <i>Program verification by lazy abstraction</i>. University of California, Berkeley."}},{"publication_status":"published","date_updated":"2026-05-29T09:45:12Z","abstract":[{"text":"We present a type system for E code, which is an assembly language that manages the release, interaction, and termination of real-time tasks. E code specifies a deadline for each task, and the type system ensures that the deadlines are path-insensitive. We show that typed E programs allow, for given worst-case execution times of tasks, a simple schedulability analysis. Moreover, the real-time programming language Giotto can be compiled into typed E~code. This shows that typed E~code identifies an easily schedulable yet expressive class of real-time programs. We have extended the Giotto compiler to generate typed E code, and enabled the run-time system for E code to perform a type and schedulability check before executing the code.","lang":"eng"}],"publisher":"Association for Computing Machinery","month":"09","year":"2004","page":"104 - 113","publist_id":"285","status":"public","title":"A typed assembly language for real-time programs","type":"conference","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","oa_version":"None","quality_controlled":"1","author":[{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kirsch, Christoph","first_name":"Christoph","last_name":"Kirsch"}],"OA_type":"closed access","citation":{"mla":"Henzinger, Thomas A., and Christoph Kirsch. “A Typed Assembly Language for Real-Time Programs.” <i>Proceedings of the 4th ACM International Conference on Embedded Software</i>, Association for Computing Machinery, 2004, pp. 104–13, doi:<a href=\"https://doi.org/10.1145/1017753.1017774\">10.1145/1017753.1017774</a>.","chicago":"Henzinger, Thomas A, and Christoph Kirsch. “A Typed Assembly Language for Real-Time Programs.” In <i>Proceedings of the 4th ACM International Conference on Embedded Software</i>, 104–13. Association for Computing Machinery, 2004. <a href=\"https://doi.org/10.1145/1017753.1017774\">https://doi.org/10.1145/1017753.1017774</a>.","ista":"Henzinger TA, Kirsch C. 2004. A typed assembly language for real-time programs. Proceedings of the 4th ACM international conference on Embedded software. EMSOFT: Embedded Software , 104–113.","apa":"Henzinger, T. A., &#38; Kirsch, C. (2004). A typed assembly language for real-time programs. In <i>Proceedings of the 4th ACM international conference on Embedded software</i> (pp. 104–113). Pisa, Italy: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/1017753.1017774\">https://doi.org/10.1145/1017753.1017774</a>","ama":"Henzinger TA, Kirsch C. A typed assembly language for real-time programs. In: <i>Proceedings of the 4th ACM International Conference on Embedded Software</i>. Association for Computing Machinery; 2004:104-113. doi:<a href=\"https://doi.org/10.1145/1017753.1017774\">10.1145/1017753.1017774</a>","short":"T.A. Henzinger, C. Kirsch, in:, Proceedings of the 4th ACM International Conference on Embedded Software, Association for Computing Machinery, 2004, pp. 104–113.","ieee":"T. A. Henzinger and C. Kirsch, “A typed assembly language for real-time programs,” in <i>Proceedings of the 4th ACM international conference on Embedded software</i>, Pisa, Italy, 2004, pp. 104–113."},"_id":"4445","publication":"Proceedings of the 4th ACM international conference on Embedded software","publication_identifier":{"isbn":["9781581138603"]},"date_created":"2018-12-11T12:08:53Z","date_published":"2004-09-27T00:00:00Z","doi":"10.1145/1017753.1017774","acknowledgement":"This research was supported in part by the AFOSR MURI grant F49620-00-1-0327 and by the NSF grants CCR- 0208875 and CCR-0225610.","language":[{"iso":"eng"}],"scopus_import":"1","conference":{"end_date":"2004-09-29","location":"Pisa, Italy","name":"EMSOFT: Embedded Software ","start_date":"2004-09-27"},"article_processing_charge":"No","extern":"1","day":"27"},{"publist_id":"270","page":"232 - 244","year":"2004","abstract":[{"lang":"eng","text":"The success of model checking for large programs depends crucially on the ability to efficiently construct parsimonious abstractions. A predicate abstraction is parsimonious if at each control location, it specifies only relationships between current values of variables, and only those which are required for proving correctness. Previous methods for automatically refining predicate abstractions until sufficient precision is obtained do not systematically construct parsimonious abstractions: predicates usually contain symbolic variables, and are added heuristically and often uniformly to many or all control locations at once. We use Craig interpolation to efficiently construct, from a given abstract error trace which cannot be concretized, a parsominous abstraction that removes the trace. At each location of the trace, we infer the relevant predicates as an interpolant between the two formulas that define the past and the future segment of the trace. Each interpolant is a relationship between current values of program variables, and is relevant only at that particular program location. It can be found by a linear scan of the proof of infeasibility of the trace.We develop our method for programs with arithmetic and pointer expressions, and call-by-value function calls. For function calls, Craig interpolation offers a systematic way of generating relevant predicates that contain only the local variables of the function and the values of the formal parameters when the function was called. We have extended our model checker Blast with predicate discovery by Craig interpolation, and applied it successfully to C programs with more than 130,000 lines of code, which was not possible with approaches that build less parsimonious abstractions."}],"date_updated":"2026-05-29T09:32:36Z","publication_status":"published","month":"04","publisher":"Association for Computing Machinery","quality_controlled":"1","oa_version":"None","type":"conference","title":"Abstractions from proofs","status":"public","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","date_created":"2018-12-11T12:08:57Z","publication_identifier":{"isbn":["9781581137293"]},"publication":"Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Jhala, Ranjit","first_name":"Ranjit","last_name":"Jhala"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar"},{"first_name":"Kenneth","last_name":"Mcmillan","full_name":"Mcmillan, Kenneth"}],"_id":"4458","citation":{"chicago":"Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Kenneth Mcmillan. “Abstractions from Proofs.” In <i>Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>, 232–44. Association for Computing Machinery, 2004. <a href=\"https://doi.org/10.1145/964001.964021\">https://doi.org/10.1145/964001.964021</a>.","mla":"Henzinger, Thomas A., et al. “Abstractions from Proofs.” <i>Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>, Association for Computing Machinery, 2004, pp. 232–44, doi:<a href=\"https://doi.org/10.1145/964001.964021\">10.1145/964001.964021</a>.","short":"T.A. Henzinger, R. Jhala, R. Majumdar, K. Mcmillan, in:, Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, 2004, pp. 232–244.","ama":"Henzinger TA, Jhala R, Majumdar R, Mcmillan K. Abstractions from proofs. In: <i>Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>. Association for Computing Machinery; 2004:232-244. doi:<a href=\"https://doi.org/10.1145/964001.964021\">10.1145/964001.964021</a>","apa":"Henzinger, T. A., Jhala, R., Majumdar, R., &#38; Mcmillan, K. (2004). Abstractions from proofs. In <i>Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages</i> (pp. 232–244). Venice, Italy: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/964001.964021\">https://doi.org/10.1145/964001.964021</a>","ista":"Henzinger TA, Jhala R, Majumdar R, Mcmillan K. 2004. Abstractions from proofs. Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. POPL: Principles of Programming Languages, 232–244.","ieee":"T. A. Henzinger, R. Jhala, R. Majumdar, and K. Mcmillan, “Abstractions from proofs,” in <i>Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages</i>, Venice, Italy, 2004, pp. 232–244."},"OA_type":"closed access","conference":{"end_date":"2004-01-16","location":"Venice, Italy","start_date":"2004-01-14","name":"POPL: Principles of Programming Languages"},"day":"01","extern":"1","article_processing_charge":"No","doi":"10.1145/964001.964021","date_published":"2004-04-01T00:00:00Z","scopus_import":"1","language":[{"iso":"eng"}]},{"abstract":[{"text":"Software model checking has been successful for sequential programs, where predicate abstraction offers suitable models, and counterexample-guided abstraction refinement permits the automatic inference of models. When checking concurrent programs, we need to abstract threads as well as the contexts in which they execute. Stateless context models, such as predicates on global variables, prove insufficient for showing the absence of race conditions in many examples. We therefore use richer context models, which combine (1) predicates for abstracting data state, (2) control flow quotients for abstracting control state, and (3) counters for abstracting an unbounded number of threads. We infer suitable context models automatically by a combination of counterexample-guided abstraction refinement, bisimulation minimization, circular assume-guarantee reasoning, and parametric reasoning about an unbounded number of threads. This algorithm, called CIRC, has been implemented in BLAST and succeeds in checking many examples of NESC code for data races. In particular, BLAST proves the absence of races in several cases where previous race checkers give false positives.","lang":"eng"}],"date_updated":"2026-05-29T09:37:45Z","publication_status":"published","month":"06","publisher":"Association for Computing Machinery","publist_id":"271","year":"2004","page":"1 - 13","type":"conference","status":"public","title":"Race checking by context inference","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","quality_controlled":"1","oa_version":"None","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Jhala, Ranjit","last_name":"Jhala","first_name":"Ranjit"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar"}],"_id":"4459","citation":{"ista":"Henzinger TA, Jhala R, Majumdar R. 2004. Race checking by context inference. Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation. PLDI: Programming Languages Design and Implementation, 1–13.","apa":"Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2004). Race checking by context inference. In <i>Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation</i> (pp. 1–13). Washington, DC, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/996841.996844\">https://doi.org/10.1145/996841.996844</a>","short":"T.A. Henzinger, R. Jhala, R. Majumdar, in:, Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2004, pp. 1–13.","ama":"Henzinger TA, Jhala R, Majumdar R. Race checking by context inference. In: <i>Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2004:1-13. doi:<a href=\"https://doi.org/10.1145/996841.996844\">10.1145/996841.996844</a>","mla":"Henzinger, Thomas A., et al. “Race Checking by Context Inference.” <i>Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2004, pp. 1–13, doi:<a href=\"https://doi.org/10.1145/996841.996844\">10.1145/996841.996844</a>.","chicago":"Henzinger, Thomas A, Ranjit Jhala, and Ritankar Majumdar. “Race Checking by Context Inference.” In <i>Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation</i>, 1–13. Association for Computing Machinery, 2004. <a href=\"https://doi.org/10.1145/996841.996844\">https://doi.org/10.1145/996841.996844</a>.","ieee":"T. A. Henzinger, R. Jhala, and R. Majumdar, “Race checking by context inference,” in <i>Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation</i>, Washington, DC, United States, 2004, pp. 1–13."},"OA_type":"closed access","date_created":"2018-12-11T12:08:57Z","publication_identifier":{"isbn":["1581138075"]},"publication":"Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation","doi":"10.1145/996841.996844","date_published":"2004-06-09T00:00:00Z","scopus_import":"1","language":[{"iso":"eng"}],"conference":{"name":"PLDI: Programming Languages Design and Implementation","start_date":"2004-06-09","location":"Washington, DC, United States","end_date":"2004-06-11"},"day":"09","article_processing_charge":"No","extern":"1"},{"month":"02","date_updated":"2026-05-29T09:24:17Z","abstract":[{"text":"One of the central axioms of extreme programming is the disciplined use of regression testing during stepwise software development. Due to recent progress in software model checking, it has become possible to supplement this process with automatic checks for behavioral safety properties of programs, such as conformance with locking idioms and other programming protocols and patterns. For efficiency reasons, all checks must be incremental, i.e., they must reuse partial results from previous checks in order to avoid all unnecessary repetition of expensive verification tasks. We show that the lazy-abstraction algorithm, and its implementation in Blast, can be extended to support the fully automatic and incremental checking of temporal safety properties during software development.","lang":"eng"}],"place":"Berlin","publist_id":"269","oa":1,"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","intvolume":"      2772","status":"public","quality_controlled":"1","oa_version":"Preprint","_id":"4461","alternative_title":["Lecture Notes in Computer Science"],"author":[{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jhala, Ranjit","first_name":"Ranjit","last_name":"Jhala"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar"},{"full_name":"Sanvido, Marco","first_name":"Marco","last_name":"Sanvido"}],"publication_identifier":{"eisbn":["9783540399100"],"isbn":["9783540210023"]},"publication":"Verification: Theory and Practice","language":[{"iso":"eng"}],"acknowledgement":"This work was supported in part by the NSF grants CCR-9988172, CCR-0085949, and CCR-0234690, the ONR grant N00014-02-1-0671, the DARPA grant F33615-00-C-1693, and the MARCO grant 98-DT-660. ","doi":"10.1007/978-3-540-39910-0_16","date_published":"2004-02-24T00:00:00Z","OA_place":"repository","extern":"1","article_processing_charge":"No","publisher":"Springer Nature","publication_status":"published","year":"2004","page":"332 - 358","type":"book_chapter","title":"Extreme Model Checking","OA_type":"green","citation":{"ieee":"T. A. Henzinger, R. Jhala, R. Majumdar, and M. Sanvido, “Extreme Model Checking,” in <i>Verification: Theory and Practice</i>, vol. 2772, Berlin: Springer Nature, 2004, pp. 332–358.","chicago":"Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Marco Sanvido. “Extreme Model Checking.” In <i>Verification: Theory and Practice</i>, 2772:332–58. Lecture Notes in Computer Science. Berlin: Springer Nature, 2004. <a href=\"https://doi.org/10.1007/978-3-540-39910-0_16\">https://doi.org/10.1007/978-3-540-39910-0_16</a>.","mla":"Henzinger, Thomas A., et al. “Extreme Model Checking.” <i>Verification: Theory and Practice</i>, vol. 2772, Springer Nature, 2004, pp. 332–58, doi:<a href=\"https://doi.org/10.1007/978-3-540-39910-0_16\">10.1007/978-3-540-39910-0_16</a>.","ama":"Henzinger TA, Jhala R, Majumdar R, Sanvido M. Extreme Model Checking. In: <i>Verification: Theory and Practice</i>. Vol 2772. Lecture Notes in Computer Science. Berlin: Springer Nature; 2004:332-358. doi:<a href=\"https://doi.org/10.1007/978-3-540-39910-0_16\">10.1007/978-3-540-39910-0_16</a>","short":"T.A. Henzinger, R. Jhala, R. Majumdar, M. Sanvido, in:, Verification: Theory and Practice, Springer Nature, Berlin, 2004, pp. 332–358.","ista":"Henzinger TA, Jhala R, Majumdar R, Sanvido M. 2004.Extreme Model Checking. In: Verification: Theory and Practice. Lecture Notes in Computer Science, vol. 2772, 332–358.","apa":"Henzinger, T. A., Jhala, R., Majumdar, R., &#38; Sanvido, M. (2004). Extreme Model Checking. In <i>Verification: Theory and Practice</i> (Vol. 2772, pp. 332–358). Berlin: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-540-39910-0_16\">https://doi.org/10.1007/978-3-540-39910-0_16</a>"},"date_created":"2018-12-11T12:08:58Z","volume":2772,"main_file_link":[{"open_access":"1","url":"http://progsys.ucsd.edu/~rjhala/papers/extreme_model_checking.pdf"}],"series_title":"Lecture Notes in Computer Science","day":"24"},{"day":"12","conference":{"end_date":"2004-03-27","name":"HSCC: Hybrid Systems - Computation and Control","location":"Philadelphia, PA, United States","start_date":"2004-03-25"},"date_created":"2018-12-11T12:09:18Z","main_file_link":[{"url":"https://www.cs.uni-salzburg.at/~ck/content/publications/conferences/HSCC04-EventDrivenProgramming.pdf","open_access":"1"}],"OA_type":"green","citation":{"ieee":"A. Ghosal, T. A. Henzinger, C. Kirsch, and M. Sanvido, “Event-driven programming with logical execution times,” presented at the HSCC: Hybrid Systems - Computation and Control, Philadelphia, PA, United States, 2004, pp. 357–371.","chicago":"Ghosal, Arkadeb, Thomas A Henzinger, Christoph Kirsch, and Marco Sanvido. “Event-Driven Programming with Logical Execution Times,” 357–71. Springer Nature, 2004. <a href=\"https://doi.org/10.1007/978-3-540-24743-2_24\">https://doi.org/10.1007/978-3-540-24743-2_24</a>.","mla":"Ghosal, Arkadeb, et al. <i>Event-Driven Programming with Logical Execution Times</i>. Springer Nature, 2004, pp. 357–71, doi:<a href=\"https://doi.org/10.1007/978-3-540-24743-2_24\">10.1007/978-3-540-24743-2_24</a>.","short":"A. Ghosal, T.A. Henzinger, C. Kirsch, M. Sanvido, in:, Springer Nature, 2004, pp. 357–371.","ama":"Ghosal A, Henzinger TA, Kirsch C, Sanvido M. Event-driven programming with logical execution times. In: Springer Nature; 2004:357-371. doi:<a href=\"https://doi.org/10.1007/978-3-540-24743-2_24\">10.1007/978-3-540-24743-2_24</a>","apa":"Ghosal, A., Henzinger, T. A., Kirsch, C., &#38; Sanvido, M. (2004). Event-driven programming with logical execution times (pp. 357–371). Presented at the HSCC: Hybrid Systems - Computation and Control, Philadelphia, PA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-540-24743-2_24\">https://doi.org/10.1007/978-3-540-24743-2_24</a>","ista":"Ghosal A, Henzinger TA, Kirsch C, Sanvido M. 2004. Event-driven programming with logical execution times. HSCC: Hybrid Systems - Computation and Control, Lecture Notes in Computer Science, , 357–371."},"type":"conference","title":"Event-driven programming with logical execution times","page":"357-371","year":"2004","publisher":"Springer Nature","publication_status":"published","extern":"1","article_processing_charge":"No","OA_place":"repository","language":[{"iso":"eng"}],"acknowledgement":"This research is supported by the AFOSR MURI grant F49620-00-1-0327, the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, and the NSF grants CCR-0208875 and CCR-0225610.","doi":"10.1007/978-3-540-24743-2_24","date_published":"2004-03-12T00:00:00Z","publication_identifier":{"isbn":["9783540212591"],"eisbn":["9783540247432"]},"_id":"4525","alternative_title":["Lecture Notes in Computer Science"],"author":[{"first_name":"Arkadeb","last_name":"Ghosal","full_name":"Ghosal, Arkadeb"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"first_name":"Christoph","last_name":"Kirsch","full_name":"Kirsch, Christoph"},{"last_name":"Sanvido","first_name":"Marco","full_name":"Sanvido, Marco"}],"quality_controlled":"1","oa_version":"Preprint","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","oa":1,"status":"public","publist_id":"200","month":"03","date_updated":"2026-05-29T09:15:20Z","abstract":[{"text":"We present a new high-level programming language, called xGiotto, for programming applications with hard real-time constraints. Like its predecessor, xGiotto is based on the LET (logical execution time) assumption: the programmer specifies when the outputs of a task become available, and the compiler checks if the specification can be implemented on a given platform. However, while the predecessor language xGiotto was purely time-triggered, xGiotto accommodates also asynchronous events. Indeed, through a mechanism called event scoping, events are the main structuring principle of the new language. The xGiotto compiler and run-time system implement event scoping through a tree-based event filter. The compiler also checks programs for determinism (absence of race conditions).","lang":"eng"}]},{"day":"30","article_processing_charge":"No","extern":"1","conference":{"end_date":"2004-09-30","location":"Enschede, Netherlands","start_date":"2004-09-27","name":"QEST: Quantitative Evaluation of Systems"},"language":[{"iso":"eng"}],"doi":"10.1109/QEST.2004.10051","date_published":"2004-09-30T00:00:00Z","date_created":"2018-12-11T12:09:27Z","publication_identifier":{"isbn":["0769521851"]},"_id":"4555","OA_type":"closed access","citation":{"ieee":"K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Trading memory for randomness,” presented at the QEST: Quantitative Evaluation of Systems, Enschede, Netherlands, 2004, pp. 206–217.","mla":"Chatterjee, Krishnendu, et al. <i>Trading Memory for Randomness</i>. IEEE, 2004, pp. 206–17, doi:<a href=\"https://doi.org/10.1109/QEST.2004.10051\">10.1109/QEST.2004.10051</a>.","chicago":"Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Trading Memory for Randomness,” 206–17. IEEE, 2004. <a href=\"https://doi.org/10.1109/QEST.2004.10051\">https://doi.org/10.1109/QEST.2004.10051</a>.","ista":"Chatterjee K, De Alfaro L, Henzinger TA. 2004. Trading memory for randomness. QEST: Quantitative Evaluation of Systems, 206–217.","apa":"Chatterjee, K., De Alfaro, L., &#38; Henzinger, T. A. (2004). Trading memory for randomness (pp. 206–217). Presented at the QEST: Quantitative Evaluation of Systems, Enschede, Netherlands: IEEE. <a href=\"https://doi.org/10.1109/QEST.2004.10051\">https://doi.org/10.1109/QEST.2004.10051</a>","ama":"Chatterjee K, De Alfaro L, Henzinger TA. Trading memory for randomness. In: IEEE; 2004:206-217. doi:<a href=\"https://doi.org/10.1109/QEST.2004.10051\">10.1109/QEST.2004.10051</a>","short":"K. Chatterjee, L. De Alfaro, T.A. Henzinger, in:, IEEE, 2004, pp. 206–217."},"author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"De Alfaro, Luca","first_name":"Luca","last_name":"De Alfaro"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"}],"quality_controlled":"1","oa_version":"None","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","type":"conference","status":"public","title":"Trading memory for randomness","publist_id":"155","year":"2004","page":"206 - 217","month":"09","publisher":"IEEE","date_updated":"2026-05-29T09:05:35Z","abstract":[{"text":"Strategies in repeated games can be classified as to whether or not they use memory and/or randomization. We consider Markov decision processes and 2-player graph games, both of the deterministic and probabilistic varieties. We characterize when memory and/or randomization are required for winning with respect to various classes of w-regular objectives, noting particularly when the use of memory can be traded for the use of randomization. In particular, we show that Markov decision processes allow randomized memoryless optimal strategies for all M?ller objectives. Furthermore, we show that 2-player probabilistic graph games allow randomized memoryless strategies for winning with probability 1 those M?ller objectives which are upward-closed. Upward-closure means that if a set α of infinitely repeating vertices is winning, then all supersets of α are also winning.","lang":"eng"}],"publication_status":"published"},{"date_published":"2004-11-01T00:00:00Z","doi":"10.1016/j.ic.2004.06.001","language":[{"iso":"eng"}],"extern":"1","article_processing_charge":"No","OA_place":"publisher","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Di","last_name":"Ma","full_name":"Ma, Di"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar"},{"full_name":"Zhao, Tian","first_name":"Tian","last_name":"Zhao"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Palsberg, Jens","last_name":"Palsberg","first_name":"Jens"}],"_id":"4556","publication_identifier":{"issn":["0890-5401"],"eissn":["1090-2651"]},"publication":"Information and Computation","status":"public","article_type":"original","intvolume":"       194","oa":1,"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","oa_version":"Accepted Version","quality_controlled":"1","abstract":[{"text":"We study the problem of determining stack boundedness and the exact maximum stack size for three classes of interrupt-driven programs. Interrupt-driven programs are used in many real-time applications that require responsive interrupt handling. In order to ensure responsiveness, programmers often enable interrupt processing in the body of lower-priority interrupt handlers. In such programs a programming error can allow interrupt handlers to be interrupted in a cyclic fashion to lead to an unbounded stack, causing the system to crash. For a restricted class of interrupt-driven programs, we show that there is a polynomial-time procedure to check stack boundedness, while determining the exact maximum stack size is PSPACE-complete. For a larger class of programs, the two problems are both PSPACE-complete, and for the largest class of programs we consider, the two problems are PSPACE-hard and can be solved in exponential time. While the complexities are high, our algorithms are exponential only in the number of handlers, and polynomial in the size of the program.","lang":"eng"}],"date_updated":"2026-05-29T09:10:28Z","month":"11","publist_id":"156","scopus_import":"1","day":"01","OA_type":"free access","citation":{"ieee":"K. Chatterjee, D. Ma, R. Majumdar, T. Zhao, T. A. Henzinger, and J. Palsberg, “Stack size analysis for interrupt-driven programs,” <i>Information and Computation</i>, vol. 194, no. 2. Elsevier, pp. 144–174, 2004.","ama":"Chatterjee K, Ma D, Majumdar R, Zhao T, Henzinger TA, Palsberg J. Stack size analysis for interrupt-driven programs. <i>Information and Computation</i>. 2004;194(2):144-174. doi:<a href=\"https://doi.org/10.1016/j.ic.2004.06.001\">10.1016/j.ic.2004.06.001</a>","short":"K. Chatterjee, D. Ma, R. Majumdar, T. Zhao, T.A. Henzinger, J. Palsberg, Information and Computation 194 (2004) 144–174.","apa":"Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T. A., &#38; Palsberg, J. (2004). Stack size analysis for interrupt-driven programs. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2004.06.001\">https://doi.org/10.1016/j.ic.2004.06.001</a>","ista":"Chatterjee K, Ma D, Majumdar R, Zhao T, Henzinger TA, Palsberg J. 2004. Stack size analysis for interrupt-driven programs. Information and Computation. 194(2), 144–174.","chicago":"Chatterjee, Krishnendu, Di Ma, Ritankar Majumdar, Tian Zhao, Thomas A Henzinger, and Jens Palsberg. “Stack Size Analysis for Interrupt-Driven Programs.” <i>Information and Computation</i>. Elsevier, 2004. <a href=\"https://doi.org/10.1016/j.ic.2004.06.001\">https://doi.org/10.1016/j.ic.2004.06.001</a>.","mla":"Chatterjee, Krishnendu, et al. “Stack Size Analysis for Interrupt-Driven Programs.” <i>Information and Computation</i>, vol. 194, no. 2, Elsevier, 2004, pp. 144–74, doi:<a href=\"https://doi.org/10.1016/j.ic.2004.06.001\">10.1016/j.ic.2004.06.001</a>."},"main_file_link":[{"open_access":"1","url":"https://doi.org/10.1016/j.ic.2004.06.001"}],"volume":194,"date_created":"2018-12-11T12:09:28Z","title":"Stack size analysis for interrupt-driven programs","type":"journal_article","issue":"2","publication_status":"published","publisher":"Elsevier","page":"144 - 174","year":"2004"},{"quality_controlled":"1","oa_version":"Preprint","status":"public","oa":1,"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","publist_id":"153","abstract":[{"lang":"eng","text":"We study perfect-information stochastic parity games. These are two-player nonterminating games which are played on a graph with turn-based probabilistic transitions. A play results in an infinite path and the conflicting goals of the two players are ω-regular path properties, formalized as parity winning conditions. The qualitative solution of such a game amounts to computing the set of vertices from which a player has a strategy to win with probability 1 (or with positive probability). The quantitative solution amounts to computing the value of the game in every vertex, i.e., the highest probability with which a player can guarantee satisfaction of his own objective in a play that starts from the vertex.For the important special case of one-player stochastic parity games (parity Markov decision processes) we give polynomial-time algorithms both for the qualitative and the quantitative solution. The running time of the qualitative solution is O(d · m3/2) for graphs with m edges and d priorities. The quantitative solution is based on a linear-programming formulation.For the two-player case, we establish the existence of optimal pure memoryless strategies. This has several important ramifications. First, it implies that the values of the games are rational. This is in contrast to the concurrent stochastic parity games of de Alfaro et al.; there, values are in general algebraic numbers, optimal strategies do not exist, and ε-optimal strategies have to be mixed and with infinite memory. Second, the existence of optimal pure memoryless strategies together with the polynomial-time solution forone-player case implies that the quantitative two-player stochastic parity game problem is in NP ∩ co-NP. This generalizes a result of Condon for stochastic games with reachability objectives. It also constitutes an exponential improvement over the best previous algorithm, which is based on a doubly exponential procedure of de Alfaro and Majumdar for concurrent stochastic parity games and provides only ε-approximations of the values."}],"date_updated":"2026-05-29T08:40:03Z","month":"02","article_processing_charge":"No","OA_place":"repository","extern":"1","doi":"10.5555/982792.982808","date_published":"2004-02-01T00:00:00Z","language":[{"iso":"eng"}],"publication":"Proceedings of the 15th annual ACM-SIAM symposium on Discrete algorithms","publication_identifier":{"isbn":["089871558X"]},"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Marcin","last_name":"Jurdziński","full_name":"Jurdziński, Marcin"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"}],"_id":"4558","type":"conference","title":"Quantitative stochastic parity games","year":"2004","page":"121 - 130","publication_status":"published","publisher":"Association for Computing Machinery","conference":{"location":"New Orleans, LA, United States","name":"SODA: Symposium on Discrete Algorithms","start_date":"2004-01-11","end_date":"2004-01-14"},"day":"01","scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://www.dcs.warwick.ac.uk/people/academic/Marcin.Jurdzinski/Papers/CJH04-SODA.pdf"}],"date_created":"2018-12-11T12:09:28Z","OA_type":"green","citation":{"apa":"Chatterjee, K., Jurdziński, M., &#38; Henzinger, T. A. (2004). Quantitative stochastic parity games. In <i>Proceedings of the 15th annual ACM-SIAM symposium on Discrete algorithms</i> (pp. 121–130). New Orleans, LA, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.5555/982792.982808\">https://doi.org/10.5555/982792.982808</a>","ista":"Chatterjee K, Jurdziński M, Henzinger TA. 2004. Quantitative stochastic parity games. Proceedings of the 15th annual ACM-SIAM symposium on Discrete algorithms. SODA: Symposium on Discrete Algorithms, 121–130.","short":"K. Chatterjee, M. Jurdziński, T.A. Henzinger, in:, Proceedings of the 15th Annual ACM-SIAM Symposium on Discrete Algorithms, Association for Computing Machinery, 2004, pp. 121–130.","ama":"Chatterjee K, Jurdziński M, Henzinger TA. Quantitative stochastic parity games. In: <i>Proceedings of the 15th Annual ACM-SIAM Symposium on Discrete Algorithms</i>. Association for Computing Machinery; 2004:121-130. doi:<a href=\"https://doi.org/10.5555/982792.982808\">10.5555/982792.982808</a>","mla":"Chatterjee, Krishnendu, et al. “Quantitative Stochastic Parity Games.” <i>Proceedings of the 15th Annual ACM-SIAM Symposium on Discrete Algorithms</i>, Association for Computing Machinery, 2004, pp. 121–30, doi:<a href=\"https://doi.org/10.5555/982792.982808\">10.5555/982792.982808</a>.","chicago":"Chatterjee, Krishnendu, Marcin Jurdziński, and Thomas A Henzinger. “Quantitative Stochastic Parity Games.” In <i>Proceedings of the 15th Annual ACM-SIAM Symposium on Discrete Algorithms</i>, 121–30. Association for Computing Machinery, 2004. <a href=\"https://doi.org/10.5555/982792.982808\">https://doi.org/10.5555/982792.982808</a>.","ieee":"K. Chatterjee, M. Jurdziński, and T. A. Henzinger, “Quantitative stochastic parity games,” in <i>Proceedings of the 15th annual ACM-SIAM symposium on Discrete algorithms</i>, New Orleans, LA, United States, 2004, pp. 121–130."}},{"publication_status":"published","date_updated":"2026-05-29T08:23:32Z","abstract":[{"lang":"eng","text":"While model checking has been successful in uncovering subtle bugs in code, its adoption in software engineering practice has been hampered by the absence of a simple interface to the programmer in an integrated development environment. We describe an integration of the software model checker BLAST into the Eclipse development environment. We provide a verification interface for practical solutions for some typical program analysis problems - assertion checking, reachability analysis, dead code analysis, and test generation - directly on the source code. The analysis is completely automatic, and assumes no knowledge of model checking or formal notation. Moreover, the interface supports incremental program verification to support incremental design and evolution of code."}],"publisher":"IEEE","month":"07","page":"251 - 255","year":"2004","publist_id":"129","status":"public","title":"An eclipse plug-in for model checking","type":"conference","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","oa_version":"None","quality_controlled":"1","author":[{"first_name":"Dirk","last_name":"Beyer","full_name":"Beyer, Dirk"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jhala, Ranjit","first_name":"Ranjit","last_name":"Jhala"},{"full_name":"Majumdar, Ritankar","last_name":"Majumdar","first_name":"Ritankar"}],"citation":{"short":"D. Beyer, T.A. Henzinger, R. Jhala, R. Majumdar, in:, Proceedings of the 12th IEEE International Workshop on Program Comprehension, IEEE, 2004, pp. 251–255.","ama":"Beyer D, Henzinger TA, Jhala R, Majumdar R. An eclipse plug-in for model checking. In: <i>Proceedings of the 12th IEEE International Workshop on Program Comprehension</i>. IEEE; 2004:251-255. doi:<a href=\"https://doi.org/10.1109/WPC.2004.1311069  \">10.1109/WPC.2004.1311069  </a>","apa":"Beyer, D., Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2004). An eclipse plug-in for model checking. In <i>Proceedings of the 12th IEEE International Workshop on Program Comprehension</i> (pp. 251–255). Bari, Italy: IEEE. <a href=\"https://doi.org/10.1109/WPC.2004.1311069  \">https://doi.org/10.1109/WPC.2004.1311069  </a>","ista":"Beyer D, Henzinger TA, Jhala R, Majumdar R. 2004. An eclipse plug-in for model checking. Proceedings of the 12th IEEE International Workshop on Program Comprehension. IWPC: Program Comprehension, 251–255.","chicago":"Beyer, Dirk, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “An Eclipse Plug-in for Model Checking.” In <i>Proceedings of the 12th IEEE International Workshop on Program Comprehension</i>, 251–55. IEEE, 2004. <a href=\"https://doi.org/10.1109/WPC.2004.1311069  \">https://doi.org/10.1109/WPC.2004.1311069  </a>.","mla":"Beyer, Dirk, et al. “An Eclipse Plug-in for Model Checking.” <i>Proceedings of the 12th IEEE International Workshop on Program Comprehension</i>, IEEE, 2004, pp. 251–55, doi:<a href=\"https://doi.org/10.1109/WPC.2004.1311069  \">10.1109/WPC.2004.1311069  </a>.","ieee":"D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, “An eclipse plug-in for model checking,” in <i>Proceedings of the 12th IEEE International Workshop on Program Comprehension</i>, Bari, Italy, 2004, pp. 251–255."},"OA_type":"closed access","_id":"4577","publication":"Proceedings of the 12th IEEE International Workshop on Program Comprehension","publication_identifier":{"isbn":["0769521495"],"issn":["1092-8138"]},"date_created":"2018-12-11T12:09:34Z","date_published":"2004-07-12T00:00:00Z","doi":"10.1109/WPC.2004.1311069  ","language":[{"iso":"eng"}],"acknowledgement":"This research was supported in part by the NSF grants CCR-0085949, CCR-0234690, and ITR-0326577.","scopus_import":"1","conference":{"name":"IWPC: Program Comprehension","location":"Bari, Italy","start_date":"2004-06-26","end_date":"2004-06-26"},"extern":"1","article_processing_charge":"No","day":"12"},{"extern":"1","article_processing_charge":"No","language":[{"iso":"eng"}],"acknowledgement":"This research was supported in part by the NSF grants CCR-0085949, CCR-0234690, and ITR-0326577.","doi":"10.1007/978-3-540-27864-1_2","date_published":"2004-08-17T00:00:00Z","publication_identifier":{"eisbn":["9783540278641"],"issn":["0302-9743"],"isbn":["9783540227915"]},"_id":"4578","alternative_title":["Lecture Notes in Computer Science"],"author":[{"full_name":"Beyer, Dirk","first_name":"Dirk","last_name":"Beyer"},{"full_name":"Chlipala, Adam","first_name":"Adam","last_name":"Chlipala"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ranjit","last_name":"Jhala","full_name":"Jhala, Ranjit"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar"}],"quality_controlled":"1","oa_version":"None","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","intvolume":"      3148","status":"public","publist_id":"130","month":"08","date_updated":"2026-05-29T08:31:41Z","abstract":[{"lang":"eng","text":"BLAST is an automatic verification tool for checking temporal safety properties of C programs. Blast is based on lazy predicate abstraction driven by interpolation-based predicate discovery. In this paper, we present the Blast specification language. The language specifies program properties at two levels of precision. At the lower level, monitor automata are used to specify temporal safety properties of program executions (traces). At the higher level, relational reachability queries over program locations are used to combine lower-level trace properties. The two-level specification language can be used to break down a verification task into several independent calls of the model-checking engine. In this way, each call to the model checker may have to analyze only part of the program, or part of the specification, and may thus succeed in a reduction of the number of predicates needed for the analysis. In addition, the two-level specification language provides a means for structuring and maintaining specifications. "}],"day":"17","conference":{"end_date":"2004-08-28","name":"SAS: Static Analysis Symposium","location":"Verona, Italy","start_date":"2004-08-26"},"scopus_import":"1","date_created":"2018-12-11T12:09:34Z","volume":3148,"OA_type":"closed access","citation":{"chicago":"Beyer, Dirk, Adam Chlipala, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “The BLAST Query Language for Software Verification,” 3148:2–18. Springer, 2004. <a href=\"https://doi.org/10.1007/978-3-540-27864-1_2\">https://doi.org/10.1007/978-3-540-27864-1_2</a>.","mla":"Beyer, Dirk, et al. <i>The BLAST Query Language for Software Verification</i>. Vol. 3148, Springer, 2004, pp. 2–18, doi:<a href=\"https://doi.org/10.1007/978-3-540-27864-1_2\">10.1007/978-3-540-27864-1_2</a>.","short":"D. Beyer, A. Chlipala, T.A. Henzinger, R. Jhala, R. Majumdar, in:, Springer, 2004, pp. 2–18.","ama":"Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. The BLAST query language for software verification. In: Vol 3148. Springer; 2004:2-18. doi:<a href=\"https://doi.org/10.1007/978-3-540-27864-1_2\">10.1007/978-3-540-27864-1_2</a>","ista":"Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. 2004. The BLAST query language for software verification. SAS: Static Analysis Symposium, Lecture Notes in Computer Science, vol. 3148, 2–18.","apa":"Beyer, D., Chlipala, A., Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2004). The BLAST query language for software verification (Vol. 3148, pp. 2–18). Presented at the SAS: Static Analysis Symposium, Verona, Italy: Springer. <a href=\"https://doi.org/10.1007/978-3-540-27864-1_2\">https://doi.org/10.1007/978-3-540-27864-1_2</a>","ieee":"D. Beyer, A. Chlipala, T. A. Henzinger, R. Jhala, and R. Majumdar, “The BLAST query language for software verification,” presented at the SAS: Static Analysis Symposium, Verona, Italy, 2004, vol. 3148, pp. 2–18."},"type":"conference","title":"The BLAST query language for software verification","page":"2 - 18","year":"2004","publisher":"Springer","publication_status":"published"},{"extern":"1","article_processing_charge":"No","day":"26","conference":{"name":"ICSE: Software Engineering","start_date":"2004-05-23","location":"Edinburgh, United Kingdom","end_date":"2004-05-28"},"language":[{"iso":"eng"}],"scopus_import":"1","date_published":"2004-07-26T00:00:00Z","doi":"10.1109/ICSE.2004.1317455","publication_identifier":{"isbn":["0769521630"],"issn":["0270-5257"]},"publication":"Proceedings of the 26th International Conference on Software Engineering","date_created":"2018-12-11T12:09:35Z","OA_type":"closed access","citation":{"ieee":"D. Beyer, A. Chlipala, T. A. Henzinger, R. Jhala, and R. Majumdar, “Generating tests from counterexamples,” in <i>Proceedings of the 26th International Conference on Software Engineering</i>, Edinburgh, United Kingdom, 2004, pp. 326–335.","apa":"Beyer, D., Chlipala, A., Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2004). Generating tests from counterexamples. In <i>Proceedings of the 26th International Conference on Software Engineering</i> (pp. 326–335). Edinburgh, United Kingdom: IEEE. <a href=\"https://doi.org/10.1109/ICSE.2004.1317455\">https://doi.org/10.1109/ICSE.2004.1317455</a>","ista":"Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. 2004. Generating tests from counterexamples. Proceedings of the 26th International Conference on Software Engineering. ICSE: Software Engineering, 326–335.","short":"D. Beyer, A. Chlipala, T.A. Henzinger, R. Jhala, R. Majumdar, in:, Proceedings of the 26th International Conference on Software Engineering, IEEE, 2004, pp. 326–335.","ama":"Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. Generating tests from counterexamples. In: <i>Proceedings of the 26th International Conference on Software Engineering</i>. IEEE; 2004:326-335. doi:<a href=\"https://doi.org/10.1109/ICSE.2004.1317455\">10.1109/ICSE.2004.1317455</a>","mla":"Beyer, Dirk, et al. “Generating Tests from Counterexamples.” <i>Proceedings of the 26th International Conference on Software Engineering</i>, IEEE, 2004, pp. 326–35, doi:<a href=\"https://doi.org/10.1109/ICSE.2004.1317455\">10.1109/ICSE.2004.1317455</a>.","chicago":"Beyer, Dirk, Adam Chlipala, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “Generating Tests from Counterexamples.” In <i>Proceedings of the 26th International Conference on Software Engineering</i>, 326–35. IEEE, 2004. <a href=\"https://doi.org/10.1109/ICSE.2004.1317455\">https://doi.org/10.1109/ICSE.2004.1317455</a>."},"_id":"4581","author":[{"first_name":"Dirk","last_name":"Beyer","full_name":"Beyer, Dirk"},{"first_name":"Adam","last_name":"Chlipala","full_name":"Chlipala, Adam"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"last_name":"Jhala","first_name":"Ranjit","full_name":"Jhala, Ranjit"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar"}],"oa_version":"None","quality_controlled":"1","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","title":"Generating tests from counterexamples","status":"public","type":"conference","page":"326 - 335","year":"2004","publist_id":"128","publisher":"IEEE","month":"07","publication_status":"published","abstract":[{"lang":"eng","text":"We have extended the software model checker BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. More precisely, given a C program and a target predicate p, BLAST determines the set L of program locations which program execution can reach with p true, and automatically generates a set of test vectors that exhibit the truth of p at all locations in L. We have used BLAST to generate test suites and to detect dead code in C programs with up to 30 K lines of code. The analysis and test vector generation is fully automatic (no user intervention) and exact (no false positives)."}],"date_updated":"2026-05-29T07:46:59Z"}]