[{"page":"137 - 143","extern":1,"intvolume":"        20","author":[{"last_name":"Kicheva","first_name":"Anna","orcid":"0000-0003-4509-4998","id":"3959A2A0-F248-11E8-B48F-1D18A9856A87","full_name":"Anna Kicheva"},{"first_name":"Marcos","last_name":"González Gaitán","full_name":"González-Gaitán, Marcos A"}],"publist_id":"5412","title":"The Decapentaplegic morphogen gradient a precise definition","date_published":"2008-04-01T00:00:00Z","publication":"Current Opinion in Cell Biology","abstract":[{"text":"Two key processes are in the basis of morphogenesis: the spatial allocation of cell types in fields of naïve cells and the regulation of growth. Both are controlled by morphogens, which activate target genes in the growing tissue in a concentration-dependent manner. Thus the morphogen model is an intrinsically quantitative concept. However, quantitative studies were performed only in recent years on two morphogens: Bicoid and Decapentaplegic. This review covers quantitative aspects of the formation and precision of the Decapentaplegic morphogen gradient. The morphogen gradient concept is transitioning from a soft definition to a precise idea of what the gradient could really do.","lang":"eng"}],"volume":20,"issue":"2","day":"01","quality_controlled":0,"year":"2008","publisher":"Elsevier","citation":{"mla":"Kicheva, Anna, and Marcos González Gaitán. “The Decapentaplegic Morphogen Gradient a Precise Definition.” <i>Current Opinion in Cell Biology</i>, vol. 20, no. 2, Elsevier, 2008, pp. 137–43, doi:<a href=\"https://doi.org/10.1016/j.ceb.2008.01.008\">10.1016/j.ceb.2008.01.008</a>.","ieee":"A. Kicheva and M. González Gaitán, “The Decapentaplegic morphogen gradient a precise definition,” <i>Current Opinion in Cell Biology</i>, vol. 20, no. 2. Elsevier, pp. 137–143, 2008.","short":"A. Kicheva, M. González Gaitán, Current Opinion in Cell Biology 20 (2008) 137–143.","chicago":"Kicheva, Anna, and Marcos González Gaitán. “The Decapentaplegic Morphogen Gradient a Precise Definition.” <i>Current Opinion in Cell Biology</i>. Elsevier, 2008. <a href=\"https://doi.org/10.1016/j.ceb.2008.01.008\">https://doi.org/10.1016/j.ceb.2008.01.008</a>.","ama":"Kicheva A, González Gaitán M. The Decapentaplegic morphogen gradient a precise definition. <i>Current Opinion in Cell Biology</i>. 2008;20(2):137-143. doi:<a href=\"https://doi.org/10.1016/j.ceb.2008.01.008\">10.1016/j.ceb.2008.01.008</a>","ista":"Kicheva A, González Gaitán M. 2008. The Decapentaplegic morphogen gradient a precise definition. Current Opinion in Cell Biology. 20(2), 137–143.","apa":"Kicheva, A., &#38; González Gaitán, M. (2008). The Decapentaplegic morphogen gradient a precise definition. <i>Current Opinion in Cell Biology</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ceb.2008.01.008\">https://doi.org/10.1016/j.ceb.2008.01.008</a>"},"month":"04","date_updated":"2021-01-12T06:52:44Z","type":"journal_article","date_created":"2018-12-11T11:53:38Z","status":"public","doi":"10.1016/j.ceb.2008.01.008","_id":"1717","publication_status":"published","acknowledgement":"This work was supported by the University of Geneva, Max Planck Society, VW, EU, SNF, and HFSP"},{"abstract":[{"text":"We study the mechanics of tissue growth via cell division and cell death (apoptosis). The rearrangements of cells can on large scales and times be captured by a continuum theory which describes the tissue as an effective viscous material with active stresses generated by cell division. We study the effects of anisotropies of cell division on cell rearrangements and show that average cellular trajectories exhibit anisotropic scaling behaviors. If cell division and apoptosis balance, there is no net growth, but for anisotropic cell division the tissue undergoes spontaneous shear deformations. Our description is relevant for the study of developing tissues such as the imaginal disks of the fruit fly Drosophila melanogaster, which grow anisotropically.","lang":"eng"}],"publication":"New Journal of Physics","volume":10,"date_published":"2008-06-03T00:00:00Z","title":"Dynamics of anisotropic tissue growth","author":[{"last_name":"Bittig","first_name":"Thomas","full_name":"Bittig, Thomas"},{"full_name":"Wartlick, Ortrud","last_name":"Wartlick","first_name":"Ortrud"},{"orcid":"0000-0003-4509-4998","id":"3959A2A0-F248-11E8-B48F-1D18A9856A87","full_name":"Anna Kicheva","last_name":"Kicheva","first_name":"Anna"},{"full_name":"González-Gaitárr, Marcos","first_name":"Marcos","last_name":"González Gaitárr"},{"first_name":"Frank","last_name":"Julicher","full_name":"Julicher, Frank"}],"publist_id":"5411","intvolume":"        10","extern":1,"status":"public","doi":"10.1088/1367-2630/10/6/063001","date_created":"2018-12-11T11:53:39Z","_id":"1719","publication_status":"published","date_updated":"2021-01-12T06:52:44Z","month":"06","type":"journal_article","citation":{"ama":"Bittig T, Wartlick O, Kicheva A, González Gaitárr M, Julicher F. Dynamics of anisotropic tissue growth. <i>New Journal of Physics</i>. 2008;10. doi:<a href=\"https://doi.org/10.1088/1367-2630/10/6/063001\">10.1088/1367-2630/10/6/063001</a>","chicago":"Bittig, Thomas, Ortrud Wartlick, Anna Kicheva, Marcos González Gaitárr, and Frank Julicher. “Dynamics of Anisotropic Tissue Growth.” <i>New Journal of Physics</i>. IOP Publishing Ltd., 2008. <a href=\"https://doi.org/10.1088/1367-2630/10/6/063001\">https://doi.org/10.1088/1367-2630/10/6/063001</a>.","short":"T. Bittig, O. Wartlick, A. Kicheva, M. González Gaitárr, F. Julicher, New Journal of Physics 10 (2008).","mla":"Bittig, Thomas, et al. “Dynamics of Anisotropic Tissue Growth.” <i>New Journal of Physics</i>, vol. 10, IOP Publishing Ltd., 2008, doi:<a href=\"https://doi.org/10.1088/1367-2630/10/6/063001\">10.1088/1367-2630/10/6/063001</a>.","ieee":"T. Bittig, O. Wartlick, A. Kicheva, M. González Gaitárr, and F. Julicher, “Dynamics of anisotropic tissue growth,” <i>New Journal of Physics</i>, vol. 10. IOP Publishing Ltd., 2008.","apa":"Bittig, T., Wartlick, O., Kicheva, A., González Gaitárr, M., &#38; Julicher, F. (2008). Dynamics of anisotropic tissue growth. <i>New Journal of Physics</i>. IOP Publishing Ltd. <a href=\"https://doi.org/10.1088/1367-2630/10/6/063001\">https://doi.org/10.1088/1367-2630/10/6/063001</a>","ista":"Bittig T, Wartlick O, Kicheva A, González Gaitárr M, Julicher F. 2008. Dynamics of anisotropic tissue growth. New Journal of Physics. 10."},"publisher":"IOP Publishing Ltd.","year":"2008","day":"03","quality_controlled":0},{"extern":1,"intvolume":"        47","page":"10262 - 10270","date_published":"2008-09-30T00:00:00Z","abstract":[{"text":"Complex I of respiratory chains transfers electrons from NADH to ubiquinone, coupled to the translocation of protons across the membrane. Two alternative coupling mechanisms are being discussed, redox-driven or conformation-driven. Using &quot;zero-length&quot; cross-linking reagent and isolated hydrophilic domains of complex I from Escherichia coli and Thermus thermophilus, we show that the pattern of cross-links between subunits changes significantly in the presence of NADH. Similar observations were made previously with intact purified E. coli and bovine complex I. This indicates that, upon reduction with NADH, similar conformational changes are likely to occur in the intact enzyme and in the isolated hydrophilic domain (which can be used for crystallographic studies). Within intact E. coli complex I, the cross-link between the hydrophobic subunits NuoA and NuoJ was abolished in the presence of NADH, indicating that conformational changes extend into the membrane domain, possibly as part of a coupling mechanism. Unexpectedly, in the absence of any chemical cross-linker, incubation of complex I with NADH resulted in covalent cross-links between subunits Nqo4 (NuoCD) and Nqo6 (NuoB), as well as between Nqo6 and Nqo9. Their formation depends on the presence of oxygen and so is likely a result of oxidative damage via reactive oxygen species (ROS) induced cross-linking. In addition, ROS- and metal ion-dependent proteolysis of these subunits (as well as Nqo3) is observed. Fe-S cluster N2 is coordinated between subunits Nqo4 and Nqo6 and could be involved in these processes. Our observations suggest that oxidative damage to complex I in vivo may include not only side-chain modifications but also protein cross-linking and degradation.","lang":"eng"}],"publication":"Biochemistry","volume":47,"author":[{"full_name":"Berrisford, John M","first_name":"John","last_name":"Berrisford"},{"full_name":"Thompson, Christopher J","first_name":"Christopher","last_name":"Thompson"},{"first_name":"Leonid A","last_name":"Sazanov","full_name":"Leonid Sazanov","id":"338D39FE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0977-7989"}],"publist_id":"5115","title":"Chemical and NADH-induced, ROS-dependent, cross-linking between sublimits of complex I from Escherichia coli and Thermus thermophilus","day":"30","issue":"39","quality_controlled":0,"year":"2008","status":"public","doi":"10.1021/bi801160u","date_created":"2018-12-11T11:54:57Z","publication_status":"published","_id":"1967","acknowledgement":"This research was funded by the Medical Research Council.","publisher":"ACS","citation":{"apa":"Berrisford, J., Thompson, C., &#38; Sazanov, L. A. (2008). Chemical and NADH-induced, ROS-dependent, cross-linking between sublimits of complex I from Escherichia coli and Thermus thermophilus. <i>Biochemistry</i>. ACS. <a href=\"https://doi.org/10.1021/bi801160u\">https://doi.org/10.1021/bi801160u</a>","ista":"Berrisford J, Thompson C, Sazanov LA. 2008. Chemical and NADH-induced, ROS-dependent, cross-linking between sublimits of complex I from Escherichia coli and Thermus thermophilus. Biochemistry. 47(39), 10262–10270.","chicago":"Berrisford, John, Christopher Thompson, and Leonid A Sazanov. “Chemical and NADH-Induced, ROS-Dependent, Cross-Linking between Sublimits of Complex I from Escherichia Coli and Thermus Thermophilus.” <i>Biochemistry</i>. ACS, 2008. <a href=\"https://doi.org/10.1021/bi801160u\">https://doi.org/10.1021/bi801160u</a>.","ama":"Berrisford J, Thompson C, Sazanov LA. Chemical and NADH-induced, ROS-dependent, cross-linking between sublimits of complex I from Escherichia coli and Thermus thermophilus. <i>Biochemistry</i>. 2008;47(39):10262-10270. doi:<a href=\"https://doi.org/10.1021/bi801160u\">10.1021/bi801160u</a>","mla":"Berrisford, John, et al. “Chemical and NADH-Induced, ROS-Dependent, Cross-Linking between Sublimits of Complex I from Escherichia Coli and Thermus Thermophilus.” <i>Biochemistry</i>, vol. 47, no. 39, ACS, 2008, pp. 10262–70, doi:<a href=\"https://doi.org/10.1021/bi801160u\">10.1021/bi801160u</a>.","ieee":"J. Berrisford, C. Thompson, and L. A. Sazanov, “Chemical and NADH-induced, ROS-dependent, cross-linking between sublimits of complex I from Escherichia coli and Thermus thermophilus,” <i>Biochemistry</i>, vol. 47, no. 39. ACS, pp. 10262–10270, 2008.","short":"J. Berrisford, C. Thompson, L.A. Sazanov, Biochemistry 47 (2008) 10262–10270."},"date_updated":"2021-01-12T06:54:24Z","month":"09","type":"journal_article"},{"acknowledgement":"This work was supported by the Medical Research Council.","publication_status":"published","_id":"1968","status":"public","date_created":"2018-12-11T11:54:58Z","doi":"10.1016/j.bbabio.2008.03.023","type":"journal_article","month":"07","date_updated":"2021-01-12T06:54:24Z","publisher":"Elsevier","citation":{"ieee":"D. Morgan and L. A. Sazanov, “Three-dimensional structure of respiratory complex I from Escherichia coli in ice in the presence of nucleotides,” <i>Biochimica et Biophysica Acta - Bioenergetics</i>, vol. 1777, no. 7–8. Elsevier, pp. 711–718, 2008.","mla":"Morgan, David, and Leonid A. Sazanov. “Three-Dimensional Structure of Respiratory Complex I from Escherichia Coli in Ice in the Presence of Nucleotides.” <i>Biochimica et Biophysica Acta - Bioenergetics</i>, vol. 1777, no. 7–8, Elsevier, 2008, pp. 711–18, doi:<a href=\"https://doi.org/10.1016/j.bbabio.2008.03.023\">10.1016/j.bbabio.2008.03.023</a>.","short":"D. Morgan, L.A. Sazanov, Biochimica et Biophysica Acta - Bioenergetics 1777 (2008) 711–718.","chicago":"Morgan, David, and Leonid A Sazanov. “Three-Dimensional Structure of Respiratory Complex I from Escherichia Coli in Ice in the Presence of Nucleotides.” <i>Biochimica et Biophysica Acta - Bioenergetics</i>. Elsevier, 2008. <a href=\"https://doi.org/10.1016/j.bbabio.2008.03.023\">https://doi.org/10.1016/j.bbabio.2008.03.023</a>.","ama":"Morgan D, Sazanov LA. Three-dimensional structure of respiratory complex I from Escherichia coli in ice in the presence of nucleotides. <i>Biochimica et Biophysica Acta - Bioenergetics</i>. 2008;1777(7-8):711-718. doi:<a href=\"https://doi.org/10.1016/j.bbabio.2008.03.023\">10.1016/j.bbabio.2008.03.023</a>","ista":"Morgan D, Sazanov LA. 2008. Three-dimensional structure of respiratory complex I from Escherichia coli in ice in the presence of nucleotides. Biochimica et Biophysica Acta - Bioenergetics. 1777(7–8), 711–718.","apa":"Morgan, D., &#38; Sazanov, L. A. (2008). Three-dimensional structure of respiratory complex I from Escherichia coli in ice in the presence of nucleotides. <i>Biochimica et Biophysica Acta - Bioenergetics</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.bbabio.2008.03.023\">https://doi.org/10.1016/j.bbabio.2008.03.023</a>"},"year":"2008","quality_controlled":0,"issue":"7-8","day":"01","volume":1777,"publication":"Biochimica et Biophysica Acta - Bioenergetics","abstract":[{"text":"\n\nComplex I (NADH:ubiquinone oxidoreductase) is the largest protein complex of bacterial and mitochondrial respiratory chains. The first three-dimensional structure of bacterial complex I in vitrified ice was determined by electron cryo-microscopy and single particle analysis. The structure of the Escherichia coli enzyme incubated with either NAD+ (as a reference) or NADH was calculated to 35 and 39 Å resolution, respectively. The X-ray structure of the peripheral arm of Thermus thermophilus complex I was docked into the reference EM structure. The model obtained indicates that Fe-S cluster N2 is close to the membrane domain interface, allowing for effective electron transfer to membrane-embedded quinone. At the current resolution, the structures in the presence of NAD+ or NADH are similar. Additionally, side-view class averages were calculated for the negatively stained bovine enzyme. The structures of bovine complex I in the presence of either NAD+ or NADH also appeared to be similar. These observations indicate that conformational changes upon reduction with NADH, suggested to occur by a range of studies, are smaller than had been thought previously. The model of the entire bacterial complex I could be built from the crystal structures of subcomplexes using the EM envelope described here.","lang":"eng"}],"date_published":"2008-07-01T00:00:00Z","title":"Three-dimensional structure of respiratory complex I from Escherichia coli in ice in the presence of nucleotides","author":[{"full_name":"Morgan, David J","last_name":"Morgan","first_name":"David"},{"full_name":"Leonid Sazanov","id":"338D39FE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0977-7989","first_name":"Leonid A","last_name":"Sazanov"}],"publist_id":"5116","intvolume":"      1777","extern":1,"page":"711 - 718"},{"intvolume":"      5123","extern":"1","article_processing_charge":"No","conference":{"name":"CAV: Computer Aided Verification","location":"Princeton, NJ, United Stated","end_date":"2008-07-14","start_date":"2008-07-07"},"page":"314 - 327","volume":5123,"OA_type":"closed access","alternative_title":["Lecture Notes in Computer Science"],"publication":"Proceedings of the 30th international conference of computer aided verifacation","abstract":[{"text":"Termination of a heap-manipulating program generally depends on preconditions that express heap assumptions (i.e., assertions describing reachability, aliasing, separation and sharing in the heap). We present an algorithm for the inference of such preconditions. The algorithm exploits a unique interplay between counterexample-producing abstract termination checker and shape analysis. The shape analysis produces heap assumptions on demand to eliminate counterexamples, i.e., non-terminating abstract computations. The experiments with our prototype implementation indicate its practical potential.","lang":"eng"}],"date_published":"2008-07-07T00:00:00Z","title":"Heap Assumptions on Demand","author":[{"last_name":"Podelski","first_name":"Andreas","full_name":"Podelski, Andreas"},{"full_name":"Rybalchenko, Andrey","first_name":"Andrey","last_name":"Rybalchenko"},{"last_name":"Wies","first_name":"Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Wies, Thomas"}],"publist_id":"1091","year":"2008","language":[{"iso":"eng"}],"day":"07","oa_version":"None","_id":"4366","publication_status":"published","publication_identifier":{"eisbn":["9783540705451"],"isbn":["9783540705437"]},"date_created":"2018-12-11T12:08:29Z","status":"public","doi":"10.1007/978-3-540-70545-1_31","type":"conference","date_updated":"2026-05-28T13:24:39Z","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","month":"07","publisher":"Springer Nature","citation":{"ama":"Podelski A, Rybalchenko A, Wies T. Heap Assumptions on Demand. In: <i>Proceedings of the 30th International Conference of Computer Aided Verifacation</i>. Vol 5123. Springer Nature; 2008:314-327. doi:<a href=\"https://doi.org/10.1007/978-3-540-70545-1_31\">10.1007/978-3-540-70545-1_31</a>","chicago":"Podelski, Andreas, Andrey Rybalchenko, and Thomas Wies. “Heap Assumptions on Demand.” In <i>Proceedings of the 30th International Conference of Computer Aided Verifacation</i>, 5123:314–27. Springer Nature, 2008. <a href=\"https://doi.org/10.1007/978-3-540-70545-1_31\">https://doi.org/10.1007/978-3-540-70545-1_31</a>.","short":"A. Podelski, A. Rybalchenko, T. Wies, in:, Proceedings of the 30th International Conference of Computer Aided Verifacation, Springer Nature, 2008, pp. 314–327.","mla":"Podelski, Andreas, et al. “Heap Assumptions on Demand.” <i>Proceedings of the 30th International Conference of Computer Aided Verifacation</i>, vol. 5123, Springer Nature, 2008, pp. 314–27, doi:<a href=\"https://doi.org/10.1007/978-3-540-70545-1_31\">10.1007/978-3-540-70545-1_31</a>.","ieee":"A. Podelski, A. Rybalchenko, and T. Wies, “Heap Assumptions on Demand,” in <i>Proceedings of the 30th international conference of computer aided verifacation</i>, Princeton, NJ, United Stated, 2008, vol. 5123, pp. 314–327.","apa":"Podelski, A., Rybalchenko, A., &#38; Wies, T. (2008). Heap Assumptions on Demand. In <i>Proceedings of the 30th international conference of computer aided verifacation</i> (Vol. 5123, pp. 314–327). Princeton, NJ, United Stated: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-540-70545-1_31\">https://doi.org/10.1007/978-3-540-70545-1_31</a>","ista":"Podelski A, Rybalchenko A, Wies T. 2008. Heap Assumptions on Demand. Proceedings of the 30th international conference of computer aided verifacation. CAV: Computer Aided Verification, Lecture Notes in Computer Science, vol. 5123, 314–327."}},{"abstract":[{"lang":"eng","text":"We survey some of the problems associated with checking whether a given behavior (a sequence, a Boolean signal or a continuous signal) satisfies a property specified in an appropriate temporal logic and describe two such monitoring algorithms for the real-time logic MITL."}],"publication":"Pillars of Computer science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday","alternative_title":["LNCS"],"date_published":"2008-03-11T00:00:00Z","title":"Checking Temporal Properties of Discrete, Timed and Continuous Behaviors","publist_id":"1087","author":[{"last_name":"Maler","first_name":"Oded","full_name":"Maler, Oded"},{"full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan","last_name":"Nickovic"},{"first_name":"Amir","last_name":"Pnueli","full_name":"Pnueli, Amir"}],"extern":"1","page":"475 - 505","article_processing_charge":"No","doi":"10.1007/978-3-540-78127-1_26","date_created":"2018-12-11T12:08:30Z","status":"public","_id":"4371","publication_status":"published","publication_identifier":{"isbn":["9783540781264"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-14T10:42:38Z","month":"03","type":"book_chapter","scopus_import":"1","citation":{"ama":"Maler O, Nickovic D, Pnueli A. Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. In: <i>Pillars of Computer Science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday</i>. Springer; 2008:475-505. doi:<a href=\"https://doi.org/10.1007/978-3-540-78127-1_26\">10.1007/978-3-540-78127-1_26</a>","chicago":"Maler, Oded, Dejan Nickovic, and Amir Pnueli. “Checking Temporal Properties of Discrete, Timed and Continuous Behaviors.” In <i>Pillars of Computer Science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday</i>, 475–505. Springer, 2008. <a href=\"https://doi.org/10.1007/978-3-540-78127-1_26\">https://doi.org/10.1007/978-3-540-78127-1_26</a>.","short":"O. Maler, D. Nickovic, A. Pnueli, in:, Pillars of Computer Science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, Springer, 2008, pp. 475–505.","ieee":"O. Maler, D. Nickovic, and A. Pnueli, “Checking Temporal Properties of Discrete, Timed and Continuous Behaviors,” in <i>Pillars of Computer science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday</i>, Springer, 2008, pp. 475–505.","mla":"Maler, Oded, et al. “Checking Temporal Properties of Discrete, Timed and Continuous Behaviors.” <i>Pillars of Computer Science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday</i>, Springer, 2008, pp. 475–505, doi:<a href=\"https://doi.org/10.1007/978-3-540-78127-1_26\">10.1007/978-3-540-78127-1_26</a>.","apa":"Maler, O., Nickovic, D., &#38; Pnueli, A. (2008). Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. In <i>Pillars of Computer science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday</i> (pp. 475–505). Springer. <a href=\"https://doi.org/10.1007/978-3-540-78127-1_26\">https://doi.org/10.1007/978-3-540-78127-1_26</a>","ista":"Maler O, Nickovic D, Pnueli A. 2008.Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. In: Pillars of Computer science: Essays Dedicated To Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday. LNCS, , 475–505."},"publisher":"Springer","year":"2008","day":"11","language":[{"iso":"eng"}],"quality_controlled":"1","oa_version":"None"},{"file":[{"file_name":"IST-2012-74-v1+1_Model_checking_transactional_memories.pdf","file_id":"5054","date_created":"2018-12-12T10:14:05Z","checksum":"1238258a27f212fc1a2050a9a246da20","relation":"main_file","access_level":"open_access","creator":"system","file_size":201583,"content_type":"application/pdf","date_updated":"2020-07-14T12:46:28Z"}],"oa":1,"year":"2008","day":"01","quality_controlled":0,"date_updated":"2021-01-12T07:56:34Z","month":"01","type":"conference","citation":{"mla":"Guerraoui, Rachid, et al. <i>Model Checking Transactional Memories</i>. ACM, 2008, pp. 372–82, doi:<a href=\"https://doi.org/10.1145/1375581.1375626\">10.1145/1375581.1375626</a>.","ieee":"R. Guerraoui, T. A. Henzinger, B. Jobstmann, and V. Singh, “Model checking transactional memories,” presented at the PLDI: Programming Languages Design and Implementation, 2008, pp. 372–382.","short":"R. Guerraoui, T.A. Henzinger, B. Jobstmann, V. Singh, in:, ACM, 2008, pp. 372–382.","chicago":"Guerraoui, Rachid, Thomas A Henzinger, Barbara Jobstmann, and Vasu Singh. “Model Checking Transactional Memories,” 372–82. ACM, 2008. <a href=\"https://doi.org/10.1145/1375581.1375626\">https://doi.org/10.1145/1375581.1375626</a>.","ama":"Guerraoui R, Henzinger TA, Jobstmann B, Singh V. Model checking transactional memories. In: ACM; 2008:372-382. doi:<a href=\"https://doi.org/10.1145/1375581.1375626\">10.1145/1375581.1375626</a>","ista":"Guerraoui R, Henzinger TA, Jobstmann B, Singh V. 2008. Model checking transactional memories. PLDI: Programming Languages Design and Implementation, 372–382.","apa":"Guerraoui, R., Henzinger, T. A., Jobstmann, B., &#38; Singh, V. (2008). Model checking transactional memories (pp. 372–382). Presented at the PLDI: Programming Languages Design and Implementation, ACM. <a href=\"https://doi.org/10.1145/1375581.1375626\">https://doi.org/10.1145/1375581.1375626</a>"},"publisher":"ACM","main_file_link":[{"url":"http://pub.ist.ac.at/%7Etah/Publications/model_checking_transactional_memories.pdf","open_access":"0"}],"status":"public","date_created":"2018-12-11T12:08:34Z","doi":"10.1145/1375581.1375626","publication_status":"published","_id":"4384","conference":{"name":"PLDI: Programming Languages Design and Implementation"},"page":"372 - 382","extern":1,"title":"Model checking transactional memories","author":[{"full_name":"Guerraoui, Rachid","first_name":"Rachid","last_name":"Guerraoui"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger"},{"full_name":"Jobstmann, Barbara","last_name":"Jobstmann","first_name":"Barbara"},{"full_name":"Vasu Singh","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","first_name":"Vasu","last_name":"Singh"}],"publist_id":"1073","abstract":[{"text":"Model checking software transactional memories (STMs) is difficult because of the unbounded number, length, and delay of concurrent transactions and the unbounded size of the memory. We show that, under certain conditions, the verification problem can be reduced to a finite-state problem, and we illustrate the use of the method by proving the correctness of several STMs, including two-phase locking, DSTM, TL2, and optimistic concurrency control. The safety properties we consider include strict serializability and opacity; the liveness properties include obstruction freedom, livelock freedom, and wait freedom.\n\nOur main contribution lies in the structure of the proofs, which are largely automated and not restricted to the STMs mentioned above. In a first step we show that every STM that enjoys certain structural properties either violates a safety or liveness requirement on some program with two threads and two shared variables, or satisfies the requirement on all programs. In the second step we use a model checker to prove the requirement for the STM applied to a most general program with two threads and two variables. In the safety case, the model checker constructs a simulation relation between two carefully constructed finite-state transition systems, one representing the given STM applied to a most general program, and the other representing a most liberal safe STM applied to the same program. In the liveness case, the model checker analyzes fairness conditions on the given STM transition system.","lang":"eng"}],"file_date_updated":"2020-07-14T12:46:28Z","date_published":"2008-01-01T00:00:00Z"},{"year":"2008","day":"10","quality_controlled":0,"month":"09","date_updated":"2021-01-12T07:56:35Z","type":"conference","publisher":"Springer","citation":{"chicago":"Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Permissiveness in Transactional Memories,” 5218:305–19. Springer, 2008. <a href=\"https://doi.org/10.1007/978-3-540-87779-0_21\">https://doi.org/10.1007/978-3-540-87779-0_21</a>.","ama":"Guerraoui R, Henzinger TA, Singh V. Permissiveness in transactional memories. In: Vol 5218. Springer; 2008:305-319. doi:<a href=\"https://doi.org/10.1007/978-3-540-87779-0_21\">10.1007/978-3-540-87779-0_21</a>","mla":"Guerraoui, Rachid, et al. <i>Permissiveness in Transactional Memories</i>. Vol. 5218, Springer, 2008, pp. 305–19, doi:<a href=\"https://doi.org/10.1007/978-3-540-87779-0_21\">10.1007/978-3-540-87779-0_21</a>.","ieee":"R. Guerraoui, T. A. Henzinger, and V. Singh, “Permissiveness in transactional memories,” presented at the DISC: Distributed Computing, 2008, vol. 5218, pp. 305–319.","short":"R. Guerraoui, T.A. Henzinger, V. Singh, in:, Springer, 2008, pp. 305–319.","apa":"Guerraoui, R., Henzinger, T. A., &#38; Singh, V. (2008). Permissiveness in transactional memories (Vol. 5218, pp. 305–319). Presented at the DISC: Distributed Computing, Springer. <a href=\"https://doi.org/10.1007/978-3-540-87779-0_21\">https://doi.org/10.1007/978-3-540-87779-0_21</a>","ista":"Guerraoui R, Henzinger TA, Singh V. 2008. Permissiveness in transactional memories. DISC: Distributed Computing, LNCS, vol. 5218, 305–319."},"main_file_link":[{"url":"http://pub.ist.ac.at/%7Etah/Publications/permissiveness_in_transactional_memories.pdf","open_access":"0"}],"acknowledgement":"This research was supported by the Swiss National Science Foundation.","doi":"10.1007/978-3-540-87779-0_21","status":"public","date_created":"2018-12-11T12:08:35Z","_id":"4386","publication_status":"published","conference":{"name":"DISC: Distributed Computing"},"page":"305 - 319","intvolume":"      5218","extern":1,"title":"Permissiveness in transactional memories","author":[{"full_name":"Guerraoui, Rachid","first_name":"Rachid","last_name":"Guerraoui"},{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724"},{"first_name":"Vasu","last_name":"Singh","full_name":"Vasu Singh","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"1072","abstract":[{"text":"We introduce the notion of permissiveness in transactional memories (TM). Intuitively, a TM is permissive if it never aborts a transaction when it need not. More specifically, a TM is permissive with respect to a safety property p if the TM accepts every history that satisfies p. Permissiveness, like safety and liveness, can be used as a metric to compare TMs. We illustrate that it is impractical to achieve permissiveness deterministically, and then show how randomization can be used to achieve permissiveness efficiently. We introduce Adaptive Validation STM (AVSTM), which is probabilistically permissive with respect to opacity; that is, every opaque history is accepted by AVSTM with positive probability. Moreover, AVSTM guarantees lock freedom. Owing to its permissiveness, AVSTM outperforms other STMs by up to 40% in read dominated workloads in high contention scenarios. But, in low contention scenarios, the book-keeping done by AVSTM to achieve permissiveness makes AVSTM, on average, 20-30% worse than existing STMs.","lang":"eng"}],"volume":5218,"alternative_title":["LNCS"],"date_published":"2008-09-10T00:00:00Z"},{"quality_controlled":0,"day":"30","year":"2008","publication_status":"published","_id":"4387","doi":"10.1007/978-3-540-85361-9_6","status":"public","date_created":"2018-12-11T12:08:35Z","acknowledgement":"This research was supported by the Swiss National Science Foundation.","main_file_link":[{"url":"http://pub.ist.ac.at/%7Etah/Publications/completeness_and_nondeterminism_in_model_checking_transactional_memories.pdf","open_access":"0"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","citation":{"apa":"Guerraoui, R., Henzinger, T. A., &#38; Singh, V. (2008). Completeness and nondeterminism in model checking transactional memories (Vol. 5201, pp. 21–35). Presented at the CONCUR: Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/978-3-540-85361-9_6\">https://doi.org/10.1007/978-3-540-85361-9_6</a>","ista":"Guerraoui R, Henzinger TA, Singh V. 2008. Completeness and nondeterminism in model checking transactional memories. CONCUR: Concurrency Theory, LNCS, vol. 5201, 21–35.","ama":"Guerraoui R, Henzinger TA, Singh V. Completeness and nondeterminism in model checking transactional memories. In: Vol 5201. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2008:21-35. doi:<a href=\"https://doi.org/10.1007/978-3-540-85361-9_6\">10.1007/978-3-540-85361-9_6</a>","chicago":"Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Completeness and Nondeterminism in Model Checking Transactional Memories,” 5201:21–35. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2008. <a href=\"https://doi.org/10.1007/978-3-540-85361-9_6\">https://doi.org/10.1007/978-3-540-85361-9_6</a>.","short":"R. Guerraoui, T.A. Henzinger, V. Singh, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2008, pp. 21–35.","ieee":"R. Guerraoui, T. A. Henzinger, and V. Singh, “Completeness and nondeterminism in model checking transactional memories,” presented at the CONCUR: Concurrency Theory, 2008, vol. 5201, pp. 21–35.","mla":"Guerraoui, Rachid, et al. <i>Completeness and Nondeterminism in Model Checking Transactional Memories</i>. Vol. 5201, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2008, pp. 21–35, doi:<a href=\"https://doi.org/10.1007/978-3-540-85361-9_6\">10.1007/978-3-540-85361-9_6</a>."},"type":"conference","month":"07","date_updated":"2021-01-12T07:56:35Z","extern":1,"intvolume":"      5201","page":"21 - 35","conference":{"name":"CONCUR: Concurrency Theory"},"date_published":"2008-07-30T00:00:00Z","volume":5201,"alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"Software transactional memory (STM) offers a disciplined concurrent programming model for exploiting the parallelism of modern processor architectures. This paper presents the first deterministic specification automata for strict serializability and opacity in STMs. Using an antichain-based tool, we show our deterministic specifications to be equivalent to more intuitive, nondeterministic specification automata (which are too large to be determinized automatically). Using deterministic specification automata, we obtain a complete verification tool for STMs. We also show how to model and verify contention management within STMs. We automatically check the opacity of popular STM algorithms, such as TL2 and DSTM, with a universal contention manager. The universal contention manager is nondeterministic and establishes correctness for all possible contention management schemes."}],"author":[{"first_name":"Rachid","last_name":"Guerraoui","full_name":"Guerraoui, Rachid"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Vasu","last_name":"Singh","full_name":"Vasu Singh","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"1071","title":"Completeness and nondeterminism in model checking transactional memories"},{"page":"304 - 308","conference":{"name":"CAV: Computer Aided Verification"},"extern":1,"publist_id":"1060","author":[{"full_name":"Beyer, Dirk","last_name":"Beyer","first_name":"Dirk"},{"orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","full_name":"Damien Zufferey","last_name":"Zufferey","first_name":"Damien"},{"full_name":"Majumdar, Ritankar S","first_name":"Ritankar","last_name":"Majumdar"}],"title":"CSIsat: Interpolation for LA+EUF","date_published":"2008-01-01T00:00:00Z","alternative_title":["LNCS 5123"],"quality_controlled":0,"day":"01","year":"2008","citation":{"chicago":"Beyer, Dirk, Damien Zufferey, and Ritankar Majumdar. “CSIsat: Interpolation for LA+EUF,” 304–8. Springer, 2008.","ama":"Beyer D, Zufferey D, Majumdar R. CSIsat: Interpolation for LA+EUF. In: Springer; 2008:304-308.","ieee":"D. Beyer, D. Zufferey, and R. Majumdar, “CSIsat: Interpolation for LA+EUF,” presented at the CAV: Computer Aided Verification, 2008, pp. 304–308.","mla":"Beyer, Dirk, et al. <i>CSIsat: Interpolation for LA+EUF</i>. Springer, 2008, pp. 304–08.","short":"D. Beyer, D. Zufferey, R. Majumdar, in:, Springer, 2008, pp. 304–308.","apa":"Beyer, D., Zufferey, D., &#38; Majumdar, R. (2008). CSIsat: Interpolation for LA+EUF (pp. 304–308). Presented at the CAV: Computer Aided Verification, Springer.","ista":"Beyer D, Zufferey D, Majumdar R. 2008. CSIsat: Interpolation for LA+EUF. CAV: Computer Aided Verification, LNCS 5123, , 304–308."},"publisher":"Springer","type":"conference","month":"01","date_updated":"2021-01-12T07:56:40Z","publication_status":"published","_id":"4397","status":"public","date_created":"2018-12-11T12:08:38Z"},{"month":"07","date_updated":"2025-07-02T05:38:10Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","citation":{"chicago":"Aviv, Adam, Pavol Cerny, Sandy Clark, Eric Cronin, Gaurav Shah, Micah Sherr, and Matt Blaze. “Security Evaluation of ES&#38;S Voting Machines and Election Management System.” In <i>17th USENIX Security Symposium</i>, 2008.","ama":"Aviv A, Cerny P, Clark S, et al. Security evaluation of ES&#38;S voting machines and election management system. In: <i>17th USENIX Security Symposium</i>. ; 2008.","mla":"Aviv, Adam, et al. “Security Evaluation of ES&#38;S Voting Machines and Election Management System.” <i>17th USENIX Security Symposium</i>, 2008.","ieee":"A. Aviv <i>et al.</i>, “Security evaluation of ES&#38;S voting machines and election management system,” in <i>17th USENIX Security Symposium</i>, San Jose, CA, United States, 2008.","short":"A. Aviv, P. Cerny, S. Clark, E. Cronin, G. Shah, M. Sherr, M. Blaze, in:, 17th USENIX Security Symposium, 2008.","apa":"Aviv, A., Cerny, P., Clark, S., Cronin, E., Shah, G., Sherr, M., &#38; Blaze, M. (2008). Security evaluation of ES&#38;S voting machines and election management system. In <i>17th USENIX Security Symposium</i>. San Jose, CA, United States.","ista":"Aviv A, Cerny P, Clark S, Cronin E, Shah G, Sherr M, Blaze M. 2008. Security evaluation of ES&#38;S voting machines and election management system. 17th USENIX Security Symposium. USENIX: Security Symposium."},"main_file_link":[{"open_access":"1","url":"http://www.usenix.org/event/evt08/tech/full_papers/aviv/aviv.pdf"}],"date_created":"2018-12-11T12:08:39Z","status":"public","_id":"4400","publication_status":"published","oa_version":"None","oa":1,"year":"2008","day":"29","language":[{"iso":"eng"}],"title":"Security evaluation of ES&S voting machines and election management system","author":[{"first_name":"Adam","last_name":"Aviv","full_name":"Aviv, Adam"},{"last_name":"Cerny","first_name":"Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","full_name":"Cerny, Pavol"},{"last_name":"Clark","first_name":"Sandy","full_name":"Clark, Sandy"},{"full_name":"Cronin, Eric","last_name":"Cronin","first_name":"Eric"},{"first_name":"Gaurav","last_name":"Shah","full_name":"Shah, Gaurav"},{"full_name":"Sherr, Micah","first_name":"Micah","last_name":"Sherr"},{"last_name":"Blaze","first_name":"Matt","full_name":"Blaze, Matt"}],"publist_id":"1057","abstract":[{"text":"This paper summarizes a security analysis of the DRE and optical scan voting systems manufactured by Election Systems and Software (ES&S), as used in Ohio (and many\r\nother jurisdictions inside and outside the US). We found numerous exploitable vulnerabilities in nearly every component of the ES&S system. These vulnerabilities enable attacks that could alter or forge precinct results, install corrupt firmware, and erase audit records. Our analysis\r\nfocused on architectural issues in which the interactions between various software and hardware modules leads to systemic vulnerabilities that do not appear to be easily countered with election procedures or software updates. Despite a highly compressed schedule (ten weeks) during which we audited hundreds of thousands of lines of source code (much of which runs on custom hardware), we discovered numerous security flaws in the ES&S system that had escaped the notice of the certification authorities. We discuss our approach to the audit, which was part\r\nof Project EVEREST, commissioned by Ohio Secretary of State Jennifer Brunner.","lang":"eng"}],"publication":"17th USENIX Security Symposium","date_published":"2008-07-29T00:00:00Z","article_processing_charge":"No","conference":{"start_date":"2008-07-28","end_date":"2008-07-29","location":"San Jose, CA, United States","name":"USENIX: Security Symposium"},"extern":"1"},{"main_file_link":[{"url":"https://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-97.html","open_access":"1"}],"date_created":"2018-12-11T12:08:42Z","status":"public","publication_status":"published","_id":"4409","date_updated":"2022-02-14T14:35:11Z","month":"09","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","type":"dissertation","degree_awarded":"PhD","publisher":"University of California, Berkeley","citation":{"ista":"Prabhu V. 2008. Games for the verification of timed systems. University of California, Berkeley.","apa":"Prabhu, V. (2008). <i>Games for the verification of timed systems</i>. University of California, Berkeley.","mla":"Prabhu, Vinayak. <i>Games for the Verification of Timed Systems</i>. University of California, Berkeley, 2008, pp. 1–137.","ieee":"V. Prabhu, “Games for the verification of timed systems,” University of California, Berkeley, 2008.","short":"V. Prabhu, Games for the Verification of Timed Systems, University of California, Berkeley, 2008.","chicago":"Prabhu, Vinayak. “Games for the Verification of Timed Systems.” University of California, Berkeley, 2008.","ama":"Prabhu V. Games for the verification of timed systems. 2008:1-137."},"year":"2008","day":"01","language":[{"iso":"eng"}],"oa":1,"oa_version":"None","abstract":[{"text":"Models of timed systems must incorporate not only the sequence of system events, but the timings of these events as well to capture the real-time aspects of physical systems. Timed automata are models of real-time systems in which states consist of discrete locations and values for real-time clocks. The presence of real-time clocks leads to an uncountable state space. This thesis studies verification problems on timed automata in a game theoretic framework.\r\n\r\nFor untimed systems, two systems are close if every sequence of events of one system is also observable in the second system. For timed systems, the difference in timings of the two corresponding sequences is also of importance. We propose the notion of bisimulation distance which quantifies timing differences; if the bisimulation distance between two systems is epsilon, then (a) every sequence of events of one system has a corresponding matching sequence in the other, and (b) the timings of matching events in between the two corresponding traces do not differ by more than epsilon. We show that we can compute the bisimulation distance between two timed automata to within any desired degree of accuracy. We also show that the timed verification logic TCTL is robust with respect to our notion of quantitative bisimilarity, in particular, if a system satisfies a formula, then every close system satisfies a close formula.\r\n\r\nTimed games are used for distinguishing between the actions of several agents, typically a controller and an environment. The controller must achieve its objective against all possible choices of the environment. The modeling of the passage of time leads to the presence of zeno executions, and corresponding unrealizable strategies of the controller which may achieve objectives by blocking time. We disallow such unreasonable strategies by restricting all agents to use only receptive strategies --strategies which while not being required to ensure time divergence by any agent, are such that no agent is responsible for blocking time. Time divergence is guaranteed when all players use receptive strategies. We show that timed automaton games with receptive strategies can be solved by a reduction to finite state turn based game graphs. We define the logic timed alternating-time temporal logic for verification of timed automaton games and show that the logic can be model checked in EXPTIME. We also show that the minimum time required by an agent to reach a desired location, and the maximum time an agent can stay safe within a set of locations, against all possible actions of its adversaries are both computable.\r\n\r\nWe next study the memory requirements of winning strategies for timed automaton games. We prove that finite memory strategies suffice for safety objectives, and that winning strategies for reachability objectives may require infinite memory in general. We introduce randomized strategies in which an agent can propose a probabilistic distribution of moves and show that finite memory randomized strategies suffice for all omega-regular objectives. We also show that while randomization helps in simplifying winning strategies, and thus allows the construction of simpler controllers, it does not help a player in winning at more states, and thus does not allow the construction of more powerful controllers.\r\n\r\nFinally we study robust winning strategies in timed games. In a physical system, a controller may propose an action together with a time delay, but the action cannot be assumed to be executed at the exact proposed time delay. We present robust strategies which incorporate such jitters and show that the set of states from which an agent can win robustly is computable.","lang":"eng"}],"date_published":"2008-09-01T00:00:00Z","title":"Games for the verification of timed systems","author":[{"full_name":"Prabhu, Vinayak","last_name":"Prabhu","first_name":"Vinayak"}],"publist_id":"319","extern":"1","article_processing_charge":"No","page":"1 - 137","supervisor":[{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"John","last_name":"Steel","full_name":"Steel, John"},{"last_name":"Varaiya","first_name":"Pravin","full_name":"Varaiya, Pravin"}]},{"title":"Compositionality in deterministic real-time embedded systems","publist_id":"316","author":[{"first_name":"Slobodan","last_name":"Matic","full_name":"Matic, Slobodan"}],"abstract":[{"text":"Many computing applications, especially those in safety critical embedded systems, require highly predictable timing properties. However, time is often not present in the prevailing computing and networking abstractions. In fact, most advances in computer architecture, software, and networking favor average-case performance over timing predictability. This thesis studies several methods for the design of concurrent and/or distributed embedded systems with precise timing guarantees. The focus is on flexible and compositional methods for programming and verification of the timing properties. The presented methods together with related formalisms cover two levels of design: (1) Programming language/model level. We propose the distributed variant of Giotto, a coordination programming language with an explicit temporal semantics—the logical execution time (LET) semantics. The LET of a task is an interval of time that specifies the time instants at which task inputs and outputs become available (task release and termination instants). The LET of a task is always non-zero. This allows us to communicate values across the network without changing the timing information of the task, and without introducing nondeterminism. We show how this methodology supports distributed code generation for distributed real-time systems. The method gives up some performance in favor of composability and predictability. We characterize the tradeoff by comparing the LET semantics with the semantics used in Simulink. (2) Abstract task graph level. We study interface-based design and verification of applications represented with task graphs. We consider task sequence graphs with general event models, and cyclic graphs with periodic event models with jitter and phase. Here an interface of a component exposes time and resource constraints of the component. Together with interfaces we formally define interface composition operations and the refinement relation. For efficient and flexible composability checking two properties are important: incremental design and independent refinement. According to the incremental design property the composition of interfaces can be performed in any order, even if interfaces for some components are not known. The refinement relation is defined such that in a design we can always substitute a refined interface for an abstract one. We show that the framework supports independent refinement, i.e., the refinement relation is preserved under composition operations.","lang":"eng"}],"date_published":"2008-01-01T00:00:00Z","article_processing_charge":"No","page":"1 - 148","supervisor":[{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"},{"last_name":"Lee","first_name":"Edward","full_name":"Lee, Edward"},{"full_name":"Sengupta, Raja","first_name":"Raja","last_name":"Sengupta"}],"extern":"1","month":"01","date_updated":"2022-02-14T14:08:50Z","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","type":"dissertation","degree_awarded":"PhD","citation":{"apa":"Matic, S. (2008). <i>Compositionality in deterministic real-time embedded systems</i>. University of California, Berkeley.","ista":"Matic S. 2008. Compositionality in deterministic real-time embedded systems. University of California, Berkeley.","chicago":"Matic, Slobodan. “Compositionality in Deterministic Real-Time Embedded Systems.” University of California, Berkeley, 2008.","ama":"Matic S. Compositionality in deterministic real-time embedded systems. 2008:1-148.","mla":"Matic, Slobodan. <i>Compositionality in Deterministic Real-Time Embedded Systems</i>. University of California, Berkeley, 2008, pp. 1–148.","ieee":"S. Matic, “Compositionality in deterministic real-time embedded systems,” University of California, Berkeley, 2008.","short":"S. Matic, Compositionality in Deterministic Real-Time Embedded Systems, University of California, Berkeley, 2008."},"publisher":"University of California, Berkeley","acknowledgement":"978-0-549-83480-9","status":"public","date_created":"2018-12-11T12:08:44Z","publication_status":"published","_id":"4415","oa_version":"None","year":"2008","day":"01","language":[{"iso":"eng"}]},{"publist_id":"277","author":[{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Hottelier, Thibaud","first_name":"Thibaud","last_name":"Hottelier"},{"last_name":"Kovács","first_name":"Laura","full_name":"Kovács, Laura"}],"title":"Valigator: A verification tool with bound and invariant generation","date_published":"2008-11-13T00:00:00Z","volume":5330,"alternative_title":["LNCS"],"abstract":[{"text":"We describe Valigator, a software tool for imperative program verification that efficiently combines symbolic computation and automated reasoning in a uniform framework. The system offers support for automatically generating and proving verification conditions and, most importantly, for automatically inferring loop invariants and bound assertions by means of symbolic summation, Gröbner basis computation, and quantifier elimination. We present general principles of the implementation and illustrate them on examples.","lang":"eng"}],"page":"333 - 342","conference":{"name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning"},"extern":1,"intvolume":"      5330","citation":{"short":"T.A. Henzinger, T. Hottelier, L. Kovács, in:, Springer, 2008, pp. 333–342.","ieee":"T. A. Henzinger, T. Hottelier, and L. Kovács, “Valigator: A verification tool with bound and invariant generation,” presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, 2008, vol. 5330, pp. 333–342.","mla":"Henzinger, Thomas A., et al. <i>Valigator: A Verification Tool with Bound and Invariant Generation</i>. Vol. 5330, Springer, 2008, pp. 333–42, doi:<a href=\"https://doi.org/10.1007/978-3-540-89439-1_24\">10.1007/978-3-540-89439-1_24</a>.","ama":"Henzinger TA, Hottelier T, Kovács L. Valigator: A verification tool with bound and invariant generation. In: Vol 5330. Springer; 2008:333-342. doi:<a href=\"https://doi.org/10.1007/978-3-540-89439-1_24\">10.1007/978-3-540-89439-1_24</a>","chicago":"Henzinger, Thomas A, Thibaud Hottelier, and Laura Kovács. “Valigator: A Verification Tool with Bound and Invariant Generation,” 5330:333–42. Springer, 2008. <a href=\"https://doi.org/10.1007/978-3-540-89439-1_24\">https://doi.org/10.1007/978-3-540-89439-1_24</a>.","ista":"Henzinger TA, Hottelier T, Kovács L. 2008. Valigator: A verification tool with bound and invariant generation. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS, vol. 5330, 333–342.","apa":"Henzinger, T. A., Hottelier, T., &#38; Kovács, L. (2008). Valigator: A verification tool with bound and invariant generation (Vol. 5330, pp. 333–342). Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Springer. <a href=\"https://doi.org/10.1007/978-3-540-89439-1_24\">https://doi.org/10.1007/978-3-540-89439-1_24</a>"},"publisher":"Springer","type":"conference","month":"11","date_updated":"2021-01-12T07:57:04Z","publication_status":"published","_id":"4452","status":"public","date_created":"2018-12-11T12:08:55Z","doi":"10.1007/978-3-540-89439-1_24","main_file_link":[{"url":"http://pub.ist.ac.at/%7Etah/Publications/valigator.pdf","open_access":"0"}],"acknowledgement":"This research was supported by the Swiss NSF.","quality_controlled":0,"day":"13","year":"2008"},{"page":"3727 - 3736","intvolume":"       366","extern":1,"title":"Two challenges in embedded systems design: Predictability and robustness","author":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger","last_name":"Henzinger","first_name":"Thomas A"}],"publist_id":"219","publication":"Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences","abstract":[{"text":"I discuss two main challenges in embedded systems design: the challenge to build predictable systems, and that to build robust systems. I suggest how predictability can be formalized as a form of determinism, and robustness as a form of continuity.","lang":"eng"}],"volume":366,"date_published":"2008-07-31T00:00:00Z","year":"2008","day":"31","issue":"1881","quality_controlled":0,"month":"07","date_updated":"2021-01-12T07:59:19Z","type":"journal_article","publisher":"Royal Society of London","citation":{"short":"T.A. Henzinger, Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences 366 (2008) 3727–3736.","ieee":"T. A. Henzinger, “Two challenges in embedded systems design: Predictability and robustness,” <i>Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences</i>, vol. 366, no. 1881. Royal Society of London, pp. 3727–3736, 2008.","mla":"Henzinger, Thomas A. “Two Challenges in Embedded Systems Design: Predictability and Robustness.” <i>Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences</i>, vol. 366, no. 1881, Royal Society of London, 2008, pp. 3727–36, doi:<a href=\"https://doi.org/10.1098/rsta.2008.0141\">10.1098/rsta.2008.0141</a>.","ama":"Henzinger TA. Two challenges in embedded systems design: Predictability and robustness. <i>Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences</i>. 2008;366(1881):3727-3736. doi:<a href=\"https://doi.org/10.1098/rsta.2008.0141\">10.1098/rsta.2008.0141</a>","chicago":"Henzinger, Thomas A. “Two Challenges in Embedded Systems Design: Predictability and Robustness.” <i>Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences</i>. Royal Society of London, 2008. <a href=\"https://doi.org/10.1098/rsta.2008.0141\">https://doi.org/10.1098/rsta.2008.0141</a>.","ista":"Henzinger TA. 2008. Two challenges in embedded systems design: Predictability and robustness. Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences. 366(1881), 3727–3736.","apa":"Henzinger, T. A. (2008). Two challenges in embedded systems design: Predictability and robustness. <i>Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences</i>. Royal Society of London. <a href=\"https://doi.org/10.1098/rsta.2008.0141\">https://doi.org/10.1098/rsta.2008.0141</a>"},"main_file_link":[{"url":"http://pub.ist.ac.at/%7Etah/Publications/two_challenges_in_embedded_systems_design.pdf","open_access":"0"}],"status":"public","doi":"10.1098/rsta.2008.0141","date_created":"2018-12-11T12:09:13Z","publication_status":"published","_id":"4509"},{"year":"2008","quality_controlled":0,"day":"01","main_file_link":[{"url":"http://pub.ist.ac.at/%7Etah/Publications/proving_non-termination.pdf","open_access":"0"}],"_id":"4521","publication_status":"published","date_created":"2018-12-11T12:09:17Z","doi":"10.1145/1328438.1328459","status":"public","type":"conference","month":"01","date_updated":"2021-01-12T07:59:25Z","publisher":"ACM","citation":{"apa":"Gupta, A., Henzinger, T. A., Majumdar, R., Rybalchenko, A., &#38; Xu, R. (2008). Proving non-termination (pp. 147–158). Presented at the POPL: Principles of Programming Languages, ACM. <a href=\"https://doi.org/10.1145/1328438.1328459\">https://doi.org/10.1145/1328438.1328459</a>","ista":"Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R. 2008. Proving non-termination. POPL: Principles of Programming Languages, 147–158.","chicago":"Gupta, Ashutosh, Thomas A Henzinger, Ritankar Majumdar, Andrey Rybalchenko, and Ru Xu. “Proving Non-Termination,” 147–58. ACM, 2008. <a href=\"https://doi.org/10.1145/1328438.1328459\">https://doi.org/10.1145/1328438.1328459</a>.","ama":"Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R. Proving non-termination. In: ACM; 2008:147-158. doi:<a href=\"https://doi.org/10.1145/1328438.1328459\">10.1145/1328438.1328459</a>","mla":"Gupta, Ashutosh, et al. <i>Proving Non-Termination</i>. ACM, 2008, pp. 147–58, doi:<a href=\"https://doi.org/10.1145/1328438.1328459\">10.1145/1328438.1328459</a>.","ieee":"A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, and R. Xu, “Proving non-termination,” presented at the POPL: Principles of Programming Languages, 2008, pp. 147–158.","short":"A. Gupta, T.A. Henzinger, R. Majumdar, A. Rybalchenko, R. Xu, in:, ACM, 2008, pp. 147–158."},"extern":1,"conference":{"name":"POPL: Principles of Programming Languages"},"page":"147 - 158","abstract":[{"lang":"eng","text":"The search for proof and the search for counterexamples (bugs) are complementary activities that need to be pursued concurrently in order to maximize the practical success rate of verification tools.While this is well-understood in safety verification, the current focus of liveness verification has been almost exclusively on the search for termination proofs. A counterexample to termination is an infinite programexecution. In this paper, we propose a method to search for such counterexamples. The search proceeds in two phases. We first dynamically enumerate lasso-shaped candidate paths for counterexamples, and then statically prove their feasibility. We illustrate the utility of our nontermination prover, called TNT, on several nontrivial examples, some of which require bit-level reasoning about integer representations."}],"date_published":"2008-01-01T00:00:00Z","title":"Proving non-termination","author":[{"full_name":"Ashutosh Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","last_name":"Gupta"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Majumdar, Ritankar S","first_name":"Ritankar","last_name":"Majumdar"},{"full_name":"Rybalchenko, Andrey","last_name":"Rybalchenko","first_name":"Andrey"},{"last_name":"Xu","first_name":"Ru","full_name":"Xu, Ru-Gang"}],"publist_id":"208"},{"year":"2008","language":[{"iso":"eng"}],"day":"31","oa_version":"None","acknowledgement":"978-0-549-83679-7","_id":"4524","publication_status":"published","date_created":"2018-12-11T12:09:18Z","status":"public","type":"dissertation","date_updated":"2021-01-12T07:59:26Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"01","publisher":"University of California, Berkeley","citation":{"ista":"Ghosal A. 2008. A hierarchical coordination language for reliable real-time tasks. University of California, Berkeley.","apa":"Ghosal, A. (2008). <i>A hierarchical coordination language for reliable real-time tasks</i>. University of California, Berkeley.","ieee":"A. Ghosal, “A hierarchical coordination language for reliable real-time tasks,” University of California, Berkeley, 2008.","mla":"Ghosal, Arkadeb. <i>A Hierarchical Coordination Language for Reliable Real-Time Tasks</i>. University of California, Berkeley, 2008, pp. 1–210.","short":"A. Ghosal, A Hierarchical Coordination Language for Reliable Real-Time Tasks, University of California, Berkeley, 2008.","chicago":"Ghosal, Arkadeb. “A Hierarchical Coordination Language for Reliable Real-Time Tasks.” University of California, Berkeley, 2008.","ama":"Ghosal A. A hierarchical coordination language for reliable real-time tasks. 2008:1-210."},"extern":"1","supervisor":[{"first_name":"Alberto","last_name":"Sangiovanni-Vincentelli","full_name":"Sangiovanni-Vincentelli, Alberto"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"},{"full_name":"Lee, Edward","first_name":"Edward","last_name":"Lee"},{"last_name":"Hedrick","first_name":"Karl","full_name":"Hedrick, Karl"}],"article_processing_charge":"No","page":"1 - 210","abstract":[{"lang":"eng","text":"Complex requirements, time-to-market pressure and regulatory constraints have made the designing of embedded systems extremely challenging. This is evident by the increase in effort and expenditure for design of safety-driven real-time control-dominated applications like automotive and avionic controllers. Design processes are often challenged by lack of proper programming tools for specifying and verifying critical requirements (e.g. timing and reliability) of such applications. Platform based design, an approach for designing embedded systems, addresses the above concerns by separating requirement from architecture. The requirement specifies the intended behavior of an application while the architecture specifies the guarantees (e.g. execution speed, failure rate etc). An implementation, a mapping of the requirement on the architecture, is then analyzed for correctness. The orthogonalization of concerns makes the specification and analyses simpler. An effective use of such design methodology has been proposed in Logical Execution Time (LET) model of real-time tasks. The model separates the timing requirements (specified by release and termination instances of a task) from the architecture guarantees (specified by worst-case execution time of the task).\r\n\r\nThis dissertation proposes a coordination language, Hierarchical Timing Language (HTL), that captures the timing and reliability requirements of real-time applications. An implementation of the program on an architecture is then analyzed to check whether desired timing and reliability requirements are met or not. The core framework extends the LET model by accounting for reliability and refinement. The reliability model separates the reliability requirements of tasks from the reliability guarantees of the architecture. The requirement expresses the desired long-term reliability while the architecture provides a short-term reliability guarantee (e.g. failure rate for each iteration). The analysis checks if the short-term guarantee ensures the desired long-term reliability. The refinement model allows replacing a task by another task during program execution. Refinement preserves schedulability and reliability, i.e., if a refined task is schedulable and reliable for an implementation, then the refining task is also schedulable and reliable for the implementation. Refinement helps in concise specification without overloading analysis.\r\n\r\nThe work presents the formal model, the analyses (both with and without refinement), and a compiler for HTL programs. The compiler checks composition and refinement constraints, performs schedulability and reliability analyses, and generates code for implementation of an HTL program on a virtual machine. Three real-time controllers, one each from automatic control, automotive control and avionic control, are used to illustrate the steps in modeling and analyzing HTL programs."}],"date_published":"2008-01-31T00:00:00Z","title":"A hierarchical coordination language for reliable real-time tasks","publist_id":"199","author":[{"full_name":"Ghosal, Arkadeb","first_name":"Arkadeb","last_name":"Ghosal"}]},{"extern":1,"intvolume":"      5054","conference":{"name":"FMSB: Formal Methods in Systems Biology"},"page":"17 - 32","date_published":"2008-05-26T00:00:00Z","abstract":[{"lang":"eng","text":"We introduce bounded asynchrony, a notion of concurrency tailored to the modeling of biological cell-cell interactions. Bounded asynchrony is the result of a scheduler that bounds the number of steps that one process gets ahead of other processes; this allows the components of a system to move independently while keeping them coupled. Bounded asynchrony accurately reproduces the experimental observations made about certain cell-cell interactions: its constrained nondeterminism captures the variability observed in cells that, although equally potent, assume distinct fates. Real-life cells are not “scheduled”, but we show that distributed real-time behavior can lead to component interactions that are observationally equivalent to bounded asynchrony; this provides a possible mechanistic explanation for the phenomena observed during cell fate specification.\nWe use model checking to determine cell fates. The nondeterminism of bounded asynchrony causes state explosion during model checking, but partial-order methods are not directly applicable. We present a new algorithm that reduces the number of states that need to be explored: our optimization takes advantage of the bounded-asynchronous progress and the spatially local interactions of components that model cells. We compare our own communication-based reduction with partial-order reduction (on a restricted form of bounded asynchrony) and experiments illustrate that our algorithm leads to significant savings."}],"alternative_title":["LNCS"],"volume":5054,"publist_id":"196","author":[{"full_name":"Fisher, Jasmin","last_name":"Fisher","first_name":"Jasmin"},{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Maria Mateescu","id":"3B43276C-F248-11E8-B48F-1D18A9856A87","first_name":"Maria","last_name":"Mateescu"},{"full_name":"Piterman, Nir","last_name":"Piterman","first_name":"Nir"}],"title":"Bounded asynchrony: Concurrency for modeling cell-cell interactions","day":"26","quality_controlled":0,"year":"2008","date_created":"2018-12-11T12:09:19Z","status":"public","doi":"10.1007/978-3-540-68413-8_2","_id":"4527","publication_status":"published","acknowledgement":"Supported in part by the Swiss National Science Foundation (grant 205321-111840).","main_file_link":[{"open_access":"0","url":"http://pub.ist.ac.at/%7Etah/Publications/bounded_asynchrony.pdf"}],"publisher":"Springer","citation":{"chicago":"Fisher, Jasmin, Thomas A Henzinger, Maria Mateescu, and Nir Piterman. “Bounded Asynchrony: Concurrency for Modeling Cell-Cell Interactions,” 5054:17–32. Springer, 2008. <a href=\"https://doi.org/10.1007/978-3-540-68413-8_2\">https://doi.org/10.1007/978-3-540-68413-8_2</a>.","ama":"Fisher J, Henzinger TA, Mateescu M, Piterman N. Bounded asynchrony: Concurrency for modeling cell-cell interactions. In: Vol 5054. Springer; 2008:17-32. doi:<a href=\"https://doi.org/10.1007/978-3-540-68413-8_2\">10.1007/978-3-540-68413-8_2</a>","ieee":"J. Fisher, T. A. Henzinger, M. Mateescu, and N. Piterman, “Bounded asynchrony: Concurrency for modeling cell-cell interactions,” presented at the FMSB: Formal Methods in Systems Biology, 2008, vol. 5054, pp. 17–32.","mla":"Fisher, Jasmin, et al. <i>Bounded Asynchrony: Concurrency for Modeling Cell-Cell Interactions</i>. Vol. 5054, Springer, 2008, pp. 17–32, doi:<a href=\"https://doi.org/10.1007/978-3-540-68413-8_2\">10.1007/978-3-540-68413-8_2</a>.","short":"J. Fisher, T.A. Henzinger, M. Mateescu, N. Piterman, in:, Springer, 2008, pp. 17–32.","apa":"Fisher, J., Henzinger, T. A., Mateescu, M., &#38; Piterman, N. (2008). Bounded asynchrony: Concurrency for modeling cell-cell interactions (Vol. 5054, pp. 17–32). Presented at the FMSB: Formal Methods in Systems Biology, Springer. <a href=\"https://doi.org/10.1007/978-3-540-68413-8_2\">https://doi.org/10.1007/978-3-540-68413-8_2</a>","ista":"Fisher J, Henzinger TA, Mateescu M, Piterman N. 2008. Bounded asynchrony: Concurrency for modeling cell-cell interactions. FMSB: Formal Methods in Systems Biology, LNCS, vol. 5054, 17–32."},"date_updated":"2021-01-12T07:59:27Z","month":"05","type":"conference"},{"intvolume":"        19","extern":1,"page":"549 - 563","abstract":[{"lang":"eng","text":"We consider the equivalence problem for labeled Markov chains (LMCs), where each state is labeled with an observation. Two LMCs are equivalent if every finite sequence of observations has the same probability of occurrence in the two LMCs. We show that equivalence can be decided in polynomial time, using a reduction to the equivalence problem for probabilistic automata, which is known to be solvable in polynomial time. We provide an alternative algorithm to solve the equivalence problem, which is based on a new definition of bisimulation for probabilistic automata. We also extend the technique to decide the equivalence of weighted probabilistic automata."}],"publication":"International Journal of Foundations of Computer Science","volume":19,"date_published":"2008-06-01T00:00:00Z","title":"Equivalence of labeled Markov chains","author":[{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"},{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724"},{"full_name":"Raskin, Jean-François","last_name":"Raskin","first_name":"Jean"}],"publist_id":"192","year":"2008","day":"01","issue":"3","quality_controlled":0,"main_file_link":[{"open_access":"0","url":"http://pub.ist.ac.at/%7Etah/Publications/equivalence_of_labeled_markov_chains.pdf"}],"status":"public","date_created":"2018-12-11T12:09:20Z","doi":"10.1142/S0129054108005814 ","publication_status":"published","_id":"4532","month":"06","date_updated":"2021-01-12T07:59:30Z","type":"journal_article","publisher":"World Scientific Publishing","citation":{"ieee":"L. Doyen, T. A. Henzinger, and J. Raskin, “Equivalence of labeled Markov chains,” <i>International Journal of Foundations of Computer Science</i>, vol. 19, no. 3. World Scientific Publishing, pp. 549–563, 2008.","mla":"Doyen, Laurent, et al. “Equivalence of Labeled Markov Chains.” <i>International Journal of Foundations of Computer Science</i>, vol. 19, no. 3, World Scientific Publishing, 2008, pp. 549–63, doi:<a href=\"https://doi.org/10.1142/S0129054108005814 \">10.1142/S0129054108005814 </a>.","short":"L. Doyen, T.A. Henzinger, J. Raskin, International Journal of Foundations of Computer Science 19 (2008) 549–563.","chicago":"Doyen, Laurent, Thomas A Henzinger, and Jean Raskin. “Equivalence of Labeled Markov Chains.” <i>International Journal of Foundations of Computer Science</i>. World Scientific Publishing, 2008. <a href=\"https://doi.org/10.1142/S0129054108005814 \">https://doi.org/10.1142/S0129054108005814 </a>.","ama":"Doyen L, Henzinger TA, Raskin J. Equivalence of labeled Markov chains. <i>International Journal of Foundations of Computer Science</i>. 2008;19(3):549-563. doi:<a href=\"https://doi.org/10.1142/S0129054108005814 \">10.1142/S0129054108005814 </a>","ista":"Doyen L, Henzinger TA, Raskin J. 2008. Equivalence of labeled Markov chains. International Journal of Foundations of Computer Science. 19(3), 549–563.","apa":"Doyen, L., Henzinger, T. A., &#38; Raskin, J. (2008). Equivalence of labeled Markov chains. <i>International Journal of Foundations of Computer Science</i>. World Scientific Publishing. <a href=\"https://doi.org/10.1142/S0129054108005814 \">https://doi.org/10.1142/S0129054108005814 </a>"}},{"type":"conference","date_updated":"2021-01-12T07:59:30Z","month":"10","publisher":"ACM","citation":{"apa":"Doyen, L., Henzinger, T. A., Jobstmann, B., &#38; Petrov, T. (2008). Interface theories with component reuse (pp. 79–88). Presented at the EMSOFT: Embedded Software , ACM. <a href=\"https://doi.org/10.1145/1450058.1450070\">https://doi.org/10.1145/1450058.1450070</a>","ista":"Doyen L, Henzinger TA, Jobstmann B, Petrov T. 2008. Interface theories with component reuse. EMSOFT: Embedded Software , 79–88.","chicago":"Doyen, Laurent, Thomas A Henzinger, Barbara Jobstmann, and Tatjana Petrov. “Interface Theories with Component Reuse,” 79–88. ACM, 2008. <a href=\"https://doi.org/10.1145/1450058.1450070\">https://doi.org/10.1145/1450058.1450070</a>.","ama":"Doyen L, Henzinger TA, Jobstmann B, Petrov T. Interface theories with component reuse. In: ACM; 2008:79-88. doi:<a href=\"https://doi.org/10.1145/1450058.1450070\">10.1145/1450058.1450070</a>","mla":"Doyen, Laurent, et al. <i>Interface Theories with Component Reuse</i>. ACM, 2008, pp. 79–88, doi:<a href=\"https://doi.org/10.1145/1450058.1450070\">10.1145/1450058.1450070</a>.","ieee":"L. Doyen, T. A. Henzinger, B. Jobstmann, and T. Petrov, “Interface theories with component reuse,” presented at the EMSOFT: Embedded Software , 2008, pp. 79–88.","short":"L. Doyen, T.A. Henzinger, B. Jobstmann, T. Petrov, in:, ACM, 2008, pp. 79–88."},"main_file_link":[{"url":"http://pub.ist.ac.at/%7Etah/Publications/interface_theories_with_component_reuse.pdf","open_access":"0"}],"_id":"4533","publication_status":"published","doi":"10.1145/1450058.1450070","status":"public","date_created":"2018-12-11T12:09:21Z","year":"2008","quality_controlled":0,"day":"01","title":"Interface theories with component reuse","publist_id":"193","author":[{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Barbara","last_name":"Jobstmann","full_name":"Jobstmann, Barbara"},{"orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","full_name":"Tatjana Petrov","last_name":"Petrov","first_name":"Tatjana"}],"abstract":[{"text":"Interface theories have been proposed to support incremental design and independent implementability. Incremental design means that the compatibility checking of interfaces can proceed for partial system descriptions, without knowing the interfaces of all components. Independent implementability means that compatible interfaces can be refined separately, maintaining compatibility. We show that these interface theories provide no formal support for component reuse, meaning that the same component cannot be used to implement several different interfaces in a design. We add a new operation to interface theories in order to support such reuse. For example, different interfaces for the same component may refer to different aspects such as functionality, timing, and power consumption. We give both stateless and stateful examples for interface theories with component reuse. To illustrate component reuse in interface-based design, we show how the stateful theory provides a natural framework for specifying and refining PCI bus clients.","lang":"eng"}],"date_published":"2008-10-01T00:00:00Z","conference":{"name":"EMSOFT: Embedded Software "},"page":"79 - 88","extern":1}]