[{"publication_status":"published","date_created":"2018-12-11T12:08:33Z","conference":{"start_date":"2010-07-05","name":"CLOUD: Cloud Computing","location":"Miami, USA","end_date":"2010-07-10"},"_id":"4381","pubrep_id":"47","month":"08","scopus_import":1,"citation":{"short":"T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, IEEE, 2010, pp. 83–90.","ama":"Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. FlexPRICE: Flexible provisioning of resources in a cloud environment. In: IEEE; 2010:83-90. doi:<a href=\"https://doi.org/10.1109/CLOUD.2010.71\">10.1109/CLOUD.2010.71</a>","ieee":"T. A. Henzinger, A. Tomar, V. Singh, T. Wies, and D. Zufferey, “FlexPRICE: Flexible provisioning of resources in a cloud environment,” presented at the CLOUD: Cloud Computing, Miami, USA, 2010, pp. 83–90.","apa":"Henzinger, T. A., Tomar, A., Singh, V., Wies, T., &#38; Zufferey, D. (2010). FlexPRICE: Flexible provisioning of resources in a cloud environment (pp. 83–90). Presented at the CLOUD: Cloud Computing, Miami, USA: IEEE. <a href=\"https://doi.org/10.1109/CLOUD.2010.71\">https://doi.org/10.1109/CLOUD.2010.71</a>","mla":"Henzinger, Thomas A., et al. <i>FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment</i>. IEEE, 2010, pp. 83–90, doi:<a href=\"https://doi.org/10.1109/CLOUD.2010.71\">10.1109/CLOUD.2010.71</a>.","chicago":"Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien Zufferey. “FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment,” 83–90. IEEE, 2010. <a href=\"https://doi.org/10.1109/CLOUD.2010.71\">https://doi.org/10.1109/CLOUD.2010.71</a>.","ista":"Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. FlexPRICE: Flexible provisioning of resources in a cloud environment. CLOUD: Cloud Computing, 83–90."},"type":"conference","abstract":[{"lang":"eng","text":"Cloud computing aims to give users virtually unlimited pay-per-use computing resources without the burden of managing the underlying infrastructure. We claim that, in order to realize the full potential of cloud computing, the user must be presented with a pricing model that offers flexibility at the requirements level, such as a choice between different degrees of execution speed and the cloud provider must be presented with a programming model that offers flexibility at the execution level, such as a choice between different scheduling policies. In such a flexible framework, with each job, the user purchases a virtual computer with the desired speed and cost characteristics, and the cloud provider can optimize the utilization of resources across a stream of jobs from different users. We designed a flexible framework to test our hypothesis, which is called FlexPRICE (Flexible Provisioning of Resources in a Cloud Environment) and works as follows. A user presents a job to the cloud. The cloud finds different schedules to execute the job and presents a set of quotes to the user in terms of price and duration for the execution. The user then chooses a particular quote and the cloud is obliged to execute the job according to the chosen quote. FlexPRICE thus hides the complexity of the actual scheduling decisions from the user, but still provides enough flexibility to meet the users actual demands. We implemented FlexPRICE in a simulator called PRICES that allows us to experiment with our framework. We observe that FlexPRICE provides a wide range of execution options-from fast and expensive to slow and cheap-- for the whole spectrum of data-intensive and computation-intensive jobs. We also observe that the set of quotes computed by FlexPRICE do not vary as the number of simultaneous jobs increases."}],"quality_controlled":"1","department":[{"_id":"ToHe"}],"corr_author":"1","publisher":"IEEE","oa_version":"Submitted Version","publist_id":"1077","author":[{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"full_name":"Tomar, Anmol","last_name":"Tomar","id":"3D8D36B6-F248-11E8-B48F-1D18A9856A87","first_name":"Anmol"},{"first_name":"Vasu","last_name":"Singh","full_name":"Singh, Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Wies","full_name":"Wies, Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas"},{"first_name":"Damien","orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","full_name":"Zufferey, Damien","last_name":"Zufferey"}],"title":"FlexPRICE: Flexible provisioning of resources in a cloud environment","date_updated":"2024-10-09T20:54:00Z","page":"83 - 90","language":[{"iso":"eng"}],"status":"public","has_accepted_license":"1","article_processing_charge":"No","file_date_updated":"2020-07-14T12:46:28Z","oa":1,"file":[{"checksum":"98e534675339a8e2beca08890d048145","content_type":"application/pdf","relation":"main_file","date_updated":"2020-07-14T12:46:28Z","file_id":"5188","access_level":"open_access","creator":"system","file_size":467436,"date_created":"2018-12-12T10:16:03Z","file_name":"IST-2012-47-v1+1_FlexPRICE-_Flexible_provisioning_of_resources_in_a_cloud_environment.pdf"}],"day":"26","doi":"10.1109/CLOUD.2010.71","date_published":"2010-08-26T00:00:00Z","year":"2010","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","ddc":["004"]},{"has_accepted_license":"1","file_date_updated":"2020-07-14T12:46:28Z","status":"public","language":[{"iso":"eng"}],"page":"263 - 272","date_updated":"2024-10-21T06:03:05Z","author":[{"first_name":"Rachid","last_name":"Guerraoui","full_name":"Guerraoui, Rachid"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Michal","last_name":"Kapalka","full_name":"Kapalka, Michal"},{"full_name":"Singh, Vasu","last_name":"Singh","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","first_name":"Vasu"}],"title":"Transactions in the jungle","oa_version":"Submitted Version","publist_id":"1076","ddc":["005"],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","year":"2010","date_published":"2010-06-13T00:00:00Z","oa":1,"file":[{"file_id":"5080","date_updated":"2020-07-14T12:46:28Z","relation":"main_file","content_type":"application/pdf","checksum":"f2ad6c00a6304da34bf21bcdcfd36c4b","file_size":246409,"creator":"system","date_created":"2018-12-12T10:14:28Z","file_name":"IST-2012-46-v1+1_Transactions_in_the_jungle.pdf","access_level":"open_access"}],"day":"13","doi":"10.1145/1810479.1810529","scopus_import":"1","month":"06","_id":"4382","pubrep_id":"46","conference":{"end_date":"2010-06-15","location":"Santorini, Greece","name":"SPAA: ACM Symposium on Parallel Algorithms and Architectures","start_date":"2010-06-13"},"date_created":"2018-12-11T12:08:34Z","publication_status":"published","publisher":"ACM","department":[{"_id":"ToHe"}],"quality_controlled":"1","citation":{"chicago":"Guerraoui, Rachid, Thomas A Henzinger, Michal Kapalka, and Vasu Singh. “Transactions in the Jungle,” 263–72. ACM, 2010. <a href=\"https://doi.org/10.1145/1810479.1810529\">https://doi.org/10.1145/1810479.1810529</a>.","ista":"Guerraoui R, Henzinger TA, Kapalka M, Singh V. 2010. Transactions in the jungle. SPAA: ACM Symposium on Parallel Algorithms and Architectures, 263–272.","mla":"Guerraoui, Rachid, et al. <i>Transactions in the Jungle</i>. ACM, 2010, pp. 263–72, doi:<a href=\"https://doi.org/10.1145/1810479.1810529\">10.1145/1810479.1810529</a>.","ieee":"R. Guerraoui, T. A. Henzinger, M. Kapalka, and V. Singh, “Transactions in the jungle,” presented at the SPAA: ACM Symposium on Parallel Algorithms and Architectures, Santorini, Greece, 2010, pp. 263–272.","ama":"Guerraoui R, Henzinger TA, Kapalka M, Singh V. Transactions in the jungle. In: ACM; 2010:263-272. doi:<a href=\"https://doi.org/10.1145/1810479.1810529\">10.1145/1810479.1810529</a>","apa":"Guerraoui, R., Henzinger, T. A., Kapalka, M., &#38; Singh, V. (2010). Transactions in the jungle (pp. 263–272). Presented at the SPAA: ACM Symposium on Parallel Algorithms and Architectures, Santorini, Greece: ACM. <a href=\"https://doi.org/10.1145/1810479.1810529\">https://doi.org/10.1145/1810479.1810529</a>","short":"R. Guerraoui, T.A. Henzinger, M. Kapalka, V. Singh, in:, ACM, 2010, pp. 263–272."},"type":"conference","abstract":[{"text":"Transactional memory (TM) has shown potential to simplify the task of writing concurrent programs. Inspired by classical work on databases, formal definitions of the semantics of TM executions have been proposed. Many of these definitions assumed that accesses to shared data are solely performed through transactions. In practice, due to legacy code and concurrency libraries, transactions in a TM have to share data with non-transactional operations. The semantics of such interaction, while widely discussed by practitioners, lacks a clear formal specification. Those interactions can vary, sometimes in subtle ways, between TM implementations and underlying memory models. We propose a correctness condition for TMs, parametrized opacity, to formally capture the now folklore notion of strong atomicity by stipulating the two following intuitive requirements: first, every transaction appears as if it is executed instantaneously with respect to other transactions and non-transactional operations, and second, non-transactional operations conform to the given underlying memory model. We investigate the inherent cost of implementing parametrized opacity. We first prove that parametrized opacity requires either instrumenting non-transactional operations (for most memory models) or writing to memory by transactions using potentially expensive read-modify-write instructions (such as compare-and-swap). Then, we show that for a class of practical relaxed memory models, parametrized opacity can indeed be implemented with constant-time instrumentation of non-transactional writes and no instrumentation of non-transactional reads. We show that, in practice, parametrizing the notion of correctness allows developing more efficient TM implementations.","lang":"eng"}]},{"scopus_import":1,"month":"07","_id":"4388","pubrep_id":"43","alternative_title":["LNCS"],"external_id":{"arxiv":["1004.2367"]},"conference":{"name":"CAV: Computer Aided Verification","location":"Edinburgh, UK","start_date":"2010-07-15","end_date":"2010-07-17"},"date_created":"2018-12-11T12:08:36Z","publication_status":"published","corr_author":"1","publisher":"Springer","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"volume":6174,"quality_controlled":"1","citation":{"short":"K. Chatterjee, T.A. Henzinger, B. Jobstmann, A. Radhakrishna, in:, Springer, 2010, pp. 665–669.","ista":"Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. 2010. GIST: A solver for probabilistic games. CAV: Computer Aided Verification, LNCS, vol. 6174, 665–669.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Arjun Radhakrishna. “GIST: A Solver for Probabilistic Games,” 6174:665–69. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-14295-6_57\">https://doi.org/10.1007/978-3-642-14295-6_57</a>.","mla":"Chatterjee, Krishnendu, et al. <i>GIST: A Solver for Probabilistic Games</i>. Vol. 6174, Springer, 2010, pp. 665–69, doi:<a href=\"https://doi.org/10.1007/978-3-642-14295-6_57\">10.1007/978-3-642-14295-6_57</a>.","apa":"Chatterjee, K., Henzinger, T. A., Jobstmann, B., &#38; Radhakrishna, A. (2010). GIST: A solver for probabilistic games (Vol. 6174, pp. 665–669). Presented at the CAV: Computer Aided Verification, Edinburgh, UK: Springer. <a href=\"https://doi.org/10.1007/978-3-642-14295-6_57\">https://doi.org/10.1007/978-3-642-14295-6_57</a>","ama":"Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. GIST: A solver for probabilistic games. In: Vol 6174. Springer; 2010:665-669. doi:<a href=\"https://doi.org/10.1007/978-3-642-14295-6_57\">10.1007/978-3-642-14295-6_57</a>","ieee":"K. Chatterjee, T. A. Henzinger, B. Jobstmann, and A. Radhakrishna, “GIST: A solver for probabilistic games,” presented at the CAV: Computer Aided Verification, Edinburgh, UK, 2010, vol. 6174, pp. 665–669."},"abstract":[{"text":"GIST is a tool that (a) solves the qualitative analysis problem of turn-based probabilistic games with ω-regular objectives; and (b) synthesizes reasonable environment assumptions for synthesis of unrealizable specifications. Our tool provides the first and efficient implementations of several reduction-based techniques to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic games for synthesizing environment assumptions for unrealizable specifications.","lang":"eng"}],"type":"conference","has_accepted_license":"1","article_processing_charge":"No","file_date_updated":"2020-07-14T12:46:28Z","status":"public","language":[{"iso":"eng"}],"date_updated":"2024-10-09T20:54:00Z","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5393"}]},"page":"665 - 669","title":"GIST: A solver for probabilistic games","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"full_name":"Jobstmann, Barbara","last_name":"Jobstmann","first_name":"Barbara"},{"id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","last_name":"Radhakrishna","full_name":"Radhakrishna, Arjun","first_name":"Arjun"}],"publist_id":"1068","oa_version":"Submitted Version","ddc":["004"],"project":[{"grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FP7","grant_number":"214373","_id":"25F1337C-B435-11E9-9278-68D0E5697425","name":"Design for Embedded Systems"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","arxiv":1,"year":"2010","ec_funded":1,"date_published":"2010-07-01T00:00:00Z","intvolume":"      6174","file":[{"date_created":"2018-12-12T10:16:33Z","file_name":"IST-2012-43-v1+1_GIST-_A_solver_for_probabilistic_games.pdf","file_size":293605,"creator":"system","access_level":"open_access","file_id":"5221","date_updated":"2020-07-14T12:46:28Z","relation":"main_file","content_type":"application/pdf","checksum":"0b2ef8c4037ffccc6902d93081af24f7"}],"oa":1,"doi":"10.1007/978-3-642-14295-6_57","day":"01"},{"publist_id":"1069","oa_version":"Submitted Version","language":[{"iso":"eng"}],"status":"public","has_accepted_license":"1","file_date_updated":"2020-07-14T12:46:28Z","title":"Robustness of sequential circuits","author":[{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Axel","full_name":"Legay, Axel","last_name":"Legay"},{"first_name":"Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan","last_name":"Nickovic"}],"date_updated":"2021-01-12T07:56:36Z","page":"77 - 84","year":"2010","oa":1,"file":[{"access_level":"open_access","creator":"system","file_size":159920,"date_created":"2018-12-12T10:09:10Z","file_name":"IST-2012-44-v1+1_Robustness_of_sequential_circuits.pdf","content_type":"application/pdf","checksum":"42b2952bfc6b6974617bd554842b904a","relation":"main_file","date_updated":"2020-07-14T12:46:28Z","file_id":"4733"}],"day":"23","doi":"10.1109/ACSD.2010.26","date_published":"2010-08-23T00:00:00Z","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","ddc":["004"],"conference":{"name":"ACSD: Application of Concurrency to System Design"},"publication_status":"published","date_created":"2018-12-11T12:08:36Z","month":"08","scopus_import":1,"_id":"4389","pubrep_id":"44","citation":{"ista":"Doyen L, Henzinger TA, Legay A, Nickovic D. 2010. Robustness of sequential circuits. ACSD: Application of Concurrency to System Design, 77–84.","chicago":"Doyen, Laurent, Thomas A Henzinger, Axel Legay, and Dejan Nickovic. “Robustness of Sequential Circuits,” 77–84. IEEE, 2010. <a href=\"https://doi.org/10.1109/ACSD.2010.26\">https://doi.org/10.1109/ACSD.2010.26</a>.","mla":"Doyen, Laurent, et al. <i>Robustness of Sequential Circuits</i>. IEEE, 2010, pp. 77–84, doi:<a href=\"https://doi.org/10.1109/ACSD.2010.26\">10.1109/ACSD.2010.26</a>.","ama":"Doyen L, Henzinger TA, Legay A, Nickovic D. Robustness of sequential circuits. In: IEEE; 2010:77-84. doi:<a href=\"https://doi.org/10.1109/ACSD.2010.26\">10.1109/ACSD.2010.26</a>","apa":"Doyen, L., Henzinger, T. A., Legay, A., &#38; Nickovic, D. (2010). Robustness of sequential circuits (pp. 77–84). Presented at the ACSD: Application of Concurrency to System Design, IEEE. <a href=\"https://doi.org/10.1109/ACSD.2010.26\">https://doi.org/10.1109/ACSD.2010.26</a>","ieee":"L. Doyen, T. A. Henzinger, A. Legay, and D. Nickovic, “Robustness of sequential circuits,” presented at the ACSD: Application of Concurrency to System Design, 2010, pp. 77–84.","short":"L. Doyen, T.A. Henzinger, A. Legay, D. Nickovic, in:, IEEE, 2010, pp. 77–84."},"abstract":[{"text":"Digital components play a central role in the design of complex embedded systems. These components are interconnected with other, possibly analog, devices and the physical environment. This environment cannot be entirely captured and can provide inaccurate input data to the component. It is thus important for digital components to have a robust behavior, i.e. the presence of a small change in the input sequences should not result in a drastic change in the output sequences. In this paper, we study a notion of robustness for sequential circuits. However, since sequential circuits may have parts that are naturally discontinuous (e.g., digital controllers with switching behavior), we need a flexible framework that accommodates this fact and leaves discontinuous parts of the circuit out from the robustness analysis. As a consequence, we consider sequential circuits that have their input variables partitioned into two disjoint sets: control and disturbance variables. Our contributions are (1) a definition of robustness for sequential circuits as a form of continuity with respect to disturbance variables, (2) the characterization of the exact class of sequential circuits that are robust according to our definition, (3) an algorithm to decide whether a sequential circuit is robust or not.","lang":"eng"}],"type":"conference","quality_controlled":"1","publisher":"IEEE","department":[{"_id":"ToHe"}]},{"department":[{"_id":"ToHe"}],"volume":6174,"corr_author":"1","publisher":"Springer","quality_controlled":"1","abstract":[{"text":"Concurrent data structures with fine-grained synchronization are notoriously difficult to implement correctly. The difficulty of reasoning about these implementations does not stem from the number of variables or the program size, but rather from the large number of possible interleavings. These implementations are therefore prime candidates for model checking. We introduce an algorithm for verifying linearizability of singly-linked heap-based concurrent data structures. We consider a model consisting of an unbounded heap where each vertex stores an element from an unbounded data domain, with a restricted set of operations for testing and updating pointers and data elements. Our main result is that linearizability is decidable for programs that invoke a fixed number of methods, possibly in parallel. This decidable fragment covers many of the common implementation techniques — fine-grained locking, lazy synchronization, and lock-free synchronization. We also show how the technique can be used to verify optimistic implementations with the help of programmer annotations. We developed a verification tool CoLT and evaluated it on a representative sample of Java implementations of the concurrent set data structure. The tool verified linearizability of a number of implementations, found a known error in a lock-free implementation and proved that the corrected version is linearizable.","lang":"eng"}],"type":"conference","citation":{"short":"P. Cerny, A. Radhakrishna, D. Zufferey, S. Chaudhuri, R. Alur, in:, Springer, 2010, pp. 465–479.","ieee":"P. Cerny, A. Radhakrishna, D. Zufferey, S. Chaudhuri, and R. Alur, “Model checking of linearizability of concurrent list implementations,” presented at the CAV: Computer Aided Verification, Edinburgh, UK, 2010, vol. 6174, pp. 465–479.","ama":"Cerny P, Radhakrishna A, Zufferey D, Chaudhuri S, Alur R. Model checking of linearizability of concurrent list implementations. In: Vol 6174. Springer; 2010:465-479. doi:<a href=\"https://doi.org/10.1007/978-3-642-14295-6_41\">10.1007/978-3-642-14295-6_41</a>","apa":"Cerny, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., &#38; Alur, R. (2010). Model checking of linearizability of concurrent list implementations (Vol. 6174, pp. 465–479). Presented at the CAV: Computer Aided Verification, Edinburgh, UK: Springer. <a href=\"https://doi.org/10.1007/978-3-642-14295-6_41\">https://doi.org/10.1007/978-3-642-14295-6_41</a>","chicago":"Cerny, Pavol, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, and Rajeev Alur. “Model Checking of Linearizability of Concurrent List Implementations,” 6174:465–79. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-14295-6_41\">https://doi.org/10.1007/978-3-642-14295-6_41</a>.","ista":"Cerny P, Radhakrishna A, Zufferey D, Chaudhuri S, Alur R. 2010. Model checking of linearizability of concurrent list implementations. CAV: Computer Aided Verification, LNCS, vol. 6174, 465–479.","mla":"Cerny, Pavol, et al. <i>Model Checking of Linearizability of Concurrent List Implementations</i>. Vol. 6174, Springer, 2010, pp. 465–79, doi:<a href=\"https://doi.org/10.1007/978-3-642-14295-6_41\">10.1007/978-3-642-14295-6_41</a>."},"_id":"4390","pubrep_id":"27","scopus_import":"1","month":"07","date_created":"2018-12-11T12:08:36Z","publication_status":"published","alternative_title":["LNCS"],"conference":{"end_date":"2010-07-17","name":"CAV: Computer Aided Verification","location":"Edinburgh, UK","start_date":"2010-07-15"},"ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":"      6174","date_published":"2010-07-01T00:00:00Z","doi":"10.1007/978-3-642-14295-6_41","day":"01","file":[{"relation":"main_file","checksum":"2eb211ce40b3c4988bce3a3592980704","content_type":"application/pdf","file_id":"7873","date_updated":"2020-07-14T12:46:28Z","access_level":"open_access","file_size":3633276,"creator":"dernst","file_name":"2010_CAV_Cerny.pdf","date_created":"2020-05-19T16:31:56Z"}],"oa":1,"year":"2010","date_updated":"2024-10-21T06:03:05Z","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5391"}]},"page":"465 - 479","author":[{"first_name":"Pavol","last_name":"Cerny","full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Radhakrishna","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","first_name":"Arjun"},{"id":"4397AC76-F248-11E8-B48F-1D18A9856A87","full_name":"Zufferey, Damien","last_name":"Zufferey","orcid":"0000-0002-3197-8736","first_name":"Damien"},{"first_name":"Swarat","full_name":"Chaudhuri, Swarat","last_name":"Chaudhuri"},{"full_name":"Alur, Rajeev","last_name":"Alur","first_name":"Rajeev"}],"title":"Model checking of linearizability of concurrent list implementations","file_date_updated":"2020-07-14T12:46:28Z","article_processing_charge":"No","has_accepted_license":"1","status":"public","language":[{"iso":"eng"}],"oa_version":"Submitted Version","publist_id":"1066"},{"year":"2010","ec_funded":1,"date_published":"2010-07-29T00:00:00Z","intvolume":"      6200","day":"29","doi":"10.1007/978-3-642-13754-9_3","project":[{"call_identifier":"FP7","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543"},{"name":"Design for Embedded Systems","_id":"25F1337C-B435-11E9-9278-68D0E5697425","grant_number":"214373","call_identifier":"FP7"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","publication":"Time For Verification: Essays in Memory of Amir Pnueli","series_title":"Essays in Memory of Amir Pnueli","publist_id":"1064","oa_version":"None","editor":[{"full_name":"Manna, Zohar","last_name":"Manna","first_name":"Zohar"},{"full_name":"Peled, Doron","last_name":"Peled","first_name":"Doron"}],"language":[{"iso":"eng"}],"status":"public","date_updated":"2024-10-09T20:53:58Z","page":"42 - 60","author":[{"first_name":"Pavol","last_name":"Cerny","full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"first_name":"Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna"}],"title":"Quantitative Simulation Games","quality_controlled":"1","citation":{"short":"P. Cerny, T.A. Henzinger, A. Radhakrishna, in:, Z. Manna, D. Peled (Eds.), Time For Verification: Essays in Memory of Amir Pnueli, Springer, 2010, pp. 42–60.","ieee":"P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Quantitative Simulation Games,” in <i>Time For Verification: Essays in Memory of Amir Pnueli</i>, vol. 6200, Z. Manna and D. Peled, Eds. Springer, 2010, pp. 42–60.","apa":"Cerny, P., Henzinger, T. A., &#38; Radhakrishna, A. (2010). Quantitative Simulation Games. In Z. Manna &#38; D. Peled (Eds.), <i>Time For Verification: Essays in Memory of Amir Pnueli</i> (Vol. 6200, pp. 42–60). Springer. <a href=\"https://doi.org/10.1007/978-3-642-13754-9_3\">https://doi.org/10.1007/978-3-642-13754-9_3</a>","ama":"Cerny P, Henzinger TA, Radhakrishna A. Quantitative Simulation Games. In: Manna Z, Peled D, eds. <i>Time For Verification: Essays in Memory of Amir Pnueli</i>. Vol 6200. Essays in Memory of Amir Pnueli. Springer; 2010:42-60. doi:<a href=\"https://doi.org/10.1007/978-3-642-13754-9_3\">10.1007/978-3-642-13754-9_3</a>","ista":"Cerny P, Henzinger TA, Radhakrishna A. 2010.Quantitative Simulation Games. In: Time For Verification: Essays in Memory of Amir Pnueli. LNCS, vol. 6200, 42–60.","chicago":"Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Quantitative Simulation Games.” In <i>Time For Verification: Essays in Memory of Amir Pnueli</i>, edited by Zohar Manna and Doron Peled, 6200:42–60. Essays in Memory of Amir Pnueli. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-13754-9_3\">https://doi.org/10.1007/978-3-642-13754-9_3</a>.","mla":"Cerny, Pavol, et al. “Quantitative Simulation Games.” <i>Time For Verification: Essays in Memory of Amir Pnueli</i>, edited by Zohar Manna and Doron Peled, vol. 6200, Springer, 2010, pp. 42–60, doi:<a href=\"https://doi.org/10.1007/978-3-642-13754-9_3\">10.1007/978-3-642-13754-9_3</a>."},"type":"book_chapter","abstract":[{"text":"While a boolean notion of correctness is given by a preorder on systems and properties, a quantitative notion of correctness is defined by a distance function on systems and properties, where the distance between a system and a property provides a measure of “fit” or “desirability.” In this article, we explore several ways how the simulation preorder can be generalized to a distance function. This is done by equipping the classical simulation game between a system and a property with quantitative objectives. In particular, for systems that satisfy a property, a quantitative simulation game can measure the “robustness” of the satisfaction, that is, how much the system can deviate from its nominal behavior while still satisfying the property. For systems that violate a property, a quantitative simulation game can measure the “seriousness” of the violation, that is, how much the property has to be modified so that it is satisfied by the system. These distances can be computed in polynomial time, since the computation reduces to the value problem in limit average games with constant weights. Finally, we demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes. ","lang":"eng"}],"corr_author":"1","publisher":"Springer","department":[{"_id":"ToHe"}],"volume":6200,"alternative_title":["LNCS"],"date_created":"2018-12-11T12:08:37Z","publication_status":"published","scopus_import":1,"month":"07","_id":"4392"},{"abstract":[{"lang":"eng","text":"Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by real-valued distance functions between systems, where the distance between implementation and specification provides a measure of “fit” or “desirability.” We extend the simulation preorder to the quantitative setting, by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specifications. The distances can be computed in polynomial time for safety specifications, and for liveness specifications given by weak fairness constraints. We show that the distance functions satisfy the triangle inequality, that the distance between two systems does not increase under parallel composition with a third system, and that the distance between two systems can be bounded from above and below by distances between abstractions of the two systems. These properties suggest that our simulation distances provide an appropriate basis for a quantitative theory of discrete systems. We also demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes."}],"type":"conference","citation":{"short":"P. Cerny, T.A. Henzinger, A. Radhakrishna, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 235–268.","apa":"Cerny, P., Henzinger, T. A., &#38; Radhakrishna, A. (2010). Simulation distances (Vol. 6269, pp. 235–268). Presented at the CONCUR: Concurrency Theory, Paris, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/978-3-642-15375-4_18\">https://doi.org/10.1007/978-3-642-15375-4_18</a>","ieee":"P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Simulation distances,” presented at the CONCUR: Concurrency Theory, Paris, France, 2010, vol. 6269, pp. 235–268.","ama":"Cerny P, Henzinger TA, Radhakrishna A. Simulation distances. In: Vol 6269. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2010:235-268. doi:<a href=\"https://doi.org/10.1007/978-3-642-15375-4_18\">10.1007/978-3-642-15375-4_18</a>","mla":"Cerny, Pavol, et al. <i>Simulation Distances</i>. Vol. 6269, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 235–68, doi:<a href=\"https://doi.org/10.1007/978-3-642-15375-4_18\">10.1007/978-3-642-15375-4_18</a>.","ista":"Cerny P, Henzinger TA, Radhakrishna A. 2010. Simulation distances. CONCUR: Concurrency Theory, LNCS, vol. 6269, 235–268.","chicago":"Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Simulation Distances,” 6269:235–68. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. <a href=\"https://doi.org/10.1007/978-3-642-15375-4_18\">https://doi.org/10.1007/978-3-642-15375-4_18</a>."},"quality_controlled":"1","corr_author":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","volume":6269,"department":[{"_id":"ToHe"}],"conference":{"location":"Paris, France","name":"CONCUR: Concurrency Theory","start_date":"2010-08-31","end_date":"2010-09-03"},"alternative_title":["LNCS"],"publication_status":"published","date_created":"2018-12-11T12:08:37Z","month":"11","scopus_import":1,"_id":"4393","pubrep_id":"42","ec_funded":1,"acknowledgement":"This work was partially supported by the European Union project COMBEST and the European Network of Excellence ArtistDesign.","year":"2010","day":"01","doi":"10.1007/978-3-642-15375-4_18","file":[{"date_updated":"2020-07-14T12:46:28Z","file_id":"5130","checksum":"ea567903676ba8afe0507ee11313dce5","content_type":"application/pdf","relation":"main_file","creator":"system","file_size":198913,"file_name":"IST-2012-42-v1+1_Simulation_distances.pdf","date_created":"2018-12-12T10:15:12Z","access_level":"open_access"}],"oa":1,"intvolume":"      6269","date_published":"2010-11-01T00:00:00Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","project":[{"call_identifier":"FP7","grant_number":"215543","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","name":"COMponent-Based Embedded Systems design Techniques"},{"name":"Design for Embedded Systems","_id":"25F1337C-B435-11E9-9278-68D0E5697425","grant_number":"214373","call_identifier":"FP7"}],"ddc":["005"],"oa_version":"Submitted Version","publist_id":"1065","status":"public","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:46:28Z","has_accepted_license":"1","title":"Simulation distances","author":[{"id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","full_name":"Cerny, Pavol","last_name":"Cerny","first_name":"Pavol"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"first_name":"Arjun","full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"}],"date_updated":"2025-09-30T07:46:05Z","related_material":{"record":[{"status":"public","id":"5389","relation":"earlier_version"},{"relation":"later_version","id":"3249","status":"public"}]},"page":"235 - 268"},{"conference":{"location":"Pahos, Cyprus","name":"CC: Compiler Construction","start_date":"2010-03-20","end_date":"2010-03-28"},"alternative_title":["LNCS"],"publication_status":"published","editor":[{"full_name":"Gupta, Rajiv","last_name":"Gupta","first_name":"Rajiv"}],"oa_version":"None","publist_id":"1063","date_created":"2018-12-11T12:08:38Z","language":[{"iso":"eng"}],"month":"04","status":"public","author":[{"first_name":"Sebastian","full_name":"Burckhardt, Sebastian","last_name":"Burckhardt"},{"first_name":"Madanlal","last_name":"Musuvathi","full_name":"Musuvathi, Madanlal"},{"first_name":"Vasu","last_name":"Singh","full_name":"Singh, Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87"}],"title":"Verifying local transformations on relaxed memory models","page":"104 - 123","_id":"4395","date_updated":"2021-01-12T07:56:39Z","year":"2010","citation":{"ieee":"S. Burckhardt, M. Musuvathi, and V. Singh, “Verifying local transformations on relaxed memory models,” presented at the CC: Compiler Construction, Pahos, Cyprus, 2010, vol. 6011, pp. 104–123.","apa":"Burckhardt, S., Musuvathi, M., &#38; Singh, V. (2010). Verifying local transformations on relaxed memory models. In R. Gupta (Ed.) (Vol. 6011, pp. 104–123). Presented at the CC: Compiler Construction, Pahos, Cyprus: Springer. <a href=\"https://doi.org/10.1007/978-3-642-11970-5_7\">https://doi.org/10.1007/978-3-642-11970-5_7</a>","ama":"Burckhardt S, Musuvathi M, Singh V. Verifying local transformations on relaxed memory models. In: Gupta R, ed. Vol 6011. Springer; 2010:104-123. doi:<a href=\"https://doi.org/10.1007/978-3-642-11970-5_7\">10.1007/978-3-642-11970-5_7</a>","chicago":"Burckhardt, Sebastian, Madanlal Musuvathi, and Vasu Singh. “Verifying Local Transformations on Relaxed Memory Models.” edited by Rajiv Gupta, 6011:104–23. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-11970-5_7\">https://doi.org/10.1007/978-3-642-11970-5_7</a>.","ista":"Burckhardt S, Musuvathi M, Singh V. 2010. Verifying local transformations on relaxed memory models. CC: Compiler Construction, LNCS, vol. 6011, 104–123.","mla":"Burckhardt, Sebastian, et al. <i>Verifying Local Transformations on Relaxed Memory Models</i>. Edited by Rajiv Gupta, vol. 6011, Springer, 2010, pp. 104–23, doi:<a href=\"https://doi.org/10.1007/978-3-642-11970-5_7\">10.1007/978-3-642-11970-5_7</a>.","short":"S. Burckhardt, M. Musuvathi, V. Singh, in:, R. Gupta (Ed.), Springer, 2010, pp. 104–123."},"doi":"10.1007/978-3-642-11970-5_7","abstract":[{"lang":"eng","text":"The problem of locally transforming or translating programs without altering their semantics is central to the construction of correct compilers. For concurrent shared-memory programs this task is challenging because (1) concurrent threads can observe transformations that would be undetectable in a sequential program, and (2) contemporary multiprocessors commonly use relaxed memory models that complicate the reasoning. In this paper, we present a novel proof methodology for verifying that a local program transformation is sound with respect to a specific hardware memory model, in the sense that it is not observable in any context. The methodology is based on a structural induction and relies on a novel compositional denotational semantics for relaxed memory models that formalizes (1) the behaviors of program fragments as a set of traces, and (2) the effect of memory model relaxations as local trace rewrite operations. To apply this methodology in practice, we implemented a semi- automated tool called Traver and used it to verify/falsify several compiler transformations for a number of different hardware memory models."}],"extern":"1","day":"21","type":"conference","date_published":"2010-04-21T00:00:00Z","quality_controlled":"1","intvolume":"      6011","publisher":"Springer","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","volume":6011},{"volume":6013,"department":[{"_id":"ToHe"}],"publisher":"Springer","abstract":[{"text":"Shape analysis is a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structure. We present a stepwise approach to the selection of instrumentation predicates for a TVLA-based shape analysis, which takes us a step closer towards the fully automatic verification of data structures. The approach uses two techniques to guide the refinement of shape abstractions: (1) during program exploration, an explicit heap analysis collects sample instances of the heap structures, which are used to identify the data structures that are manipulated by the program; and (2) during abstraction refinement along an infeasible error path, we consider different possible heap abstractions and choose the coarsest one that eliminates the infeasible path. We have implemented this combined approach for automatic shape refinement as an extension of the software model checker BLAST. Example programs from a data-structure library that manipulate doubly-linked lists and trees were successfully verified by our tool.","lang":"eng"}],"type":"conference","citation":{"ama":"Beyer D, Henzinger TA, Théoduloz G, Zufferey D. Shape refinement through explicit heap analysis. In: Rosenblum D, Taenzer G, eds. Vol 6013. Springer; 2010:263-277. doi:<a href=\"https://doi.org/10.1007/978-3-642-12029-9_19\">10.1007/978-3-642-12029-9_19</a>","ieee":"D. Beyer, T. A. Henzinger, G. Théoduloz, and D. Zufferey, “Shape refinement through explicit heap analysis,” presented at the FASE: Fundamental Approaches To Software Engineering, Paphos, Cyprus, 2010, vol. 6013, pp. 263–277.","apa":"Beyer, D., Henzinger, T. A., Théoduloz, G., &#38; Zufferey, D. (2010). Shape refinement through explicit heap analysis. In D. Rosenblum &#38; G. Taenzer (Eds.) (Vol. 6013, pp. 263–277). Presented at the FASE: Fundamental Approaches To Software Engineering, Paphos, Cyprus: Springer. <a href=\"https://doi.org/10.1007/978-3-642-12029-9_19\">https://doi.org/10.1007/978-3-642-12029-9_19</a>","mla":"Beyer, Dirk, et al. <i>Shape Refinement through Explicit Heap Analysis</i>. Edited by David Rosenblum and Gabriele Taenzer, vol. 6013, Springer, 2010, pp. 263–77, doi:<a href=\"https://doi.org/10.1007/978-3-642-12029-9_19\">10.1007/978-3-642-12029-9_19</a>.","ista":"Beyer D, Henzinger TA, Théoduloz G, Zufferey D. 2010. Shape refinement through explicit heap analysis. FASE: Fundamental Approaches To Software Engineering, LNCS, vol. 6013, 263–277.","chicago":"Beyer, Dirk, Thomas A Henzinger, Grégory Théoduloz, and Damien Zufferey. “Shape Refinement through Explicit Heap Analysis.” edited by David Rosenblum and Gabriele Taenzer, 6013:263–77. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-12029-9_19\">https://doi.org/10.1007/978-3-642-12029-9_19</a>.","short":"D. Beyer, T.A. Henzinger, G. Théoduloz, D. Zufferey, in:, D. Rosenblum, G. Taenzer (Eds.), Springer, 2010, pp. 263–277."},"quality_controlled":"1","pubrep_id":"41","_id":"4396","month":"04","scopus_import":1,"publication_status":"published","date_created":"2018-12-11T12:08:38Z","conference":{"end_date":"2010-03-28","name":"FASE: Fundamental Approaches To Software Engineering","location":"Paphos, Cyprus","start_date":"2010-03-20"},"alternative_title":["LNCS"],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"ddc":["004"],"doi":"10.1007/978-3-642-12029-9_19","day":"21","oa":1,"file":[{"file_id":"5332","date_updated":"2020-07-14T12:46:29Z","relation":"main_file","checksum":"7d26e59a9681487d7283eba337292b2c","content_type":"application/pdf","date_created":"2018-12-12T10:18:13Z","file_name":"IST-2012-41-v1+1_Shape_refinement_through_explicit_heap_analysis.pdf","file_size":312147,"creator":"system","access_level":"open_access"}],"intvolume":"      6013","date_published":"2010-04-21T00:00:00Z","year":"2010","author":[{"full_name":"Beyer, Dirk","last_name":"Beyer","first_name":"Dirk"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"last_name":"Théoduloz","full_name":"Théoduloz, Grégory","first_name":"Grégory"},{"first_name":"Damien","full_name":"Zufferey, Damien","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3197-8736"}],"title":"Shape refinement through explicit heap analysis","page":"263 - 277","date_updated":"2021-01-12T07:56:40Z","language":[{"iso":"eng"}],"status":"public","file_date_updated":"2020-07-14T12:46:29Z","has_accepted_license":"1","editor":[{"first_name":"David","full_name":"Rosenblum, David","last_name":"Rosenblum"},{"first_name":"Gabriele","full_name":"Taenzer, Gabriele","last_name":"Taenzer"}],"oa_version":"Submitted Version","publist_id":"1061"},{"citation":{"ama":"Wies T, Zufferey D, Henzinger TA. Forward analysis of depth-bounded processes. In: Ong L, ed. Vol 6014. Springer; 2010:94-108. doi:<a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">10.1007/978-3-642-12032-9_8</a>","ieee":"T. Wies, D. Zufferey, and T. A. Henzinger, “Forward analysis of depth-bounded processes,” presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Paphos, Cyprus, 2010, vol. 6014, pp. 94–108.","apa":"Wies, T., Zufferey, D., &#38; Henzinger, T. A. (2010). Forward analysis of depth-bounded processes. In L. Ong (Ed.) (Vol. 6014, pp. 94–108). Presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Paphos, Cyprus: Springer. <a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">https://doi.org/10.1007/978-3-642-12032-9_8</a>","mla":"Wies, Thomas, et al. <i>Forward Analysis of Depth-Bounded Processes</i>. Edited by Luke Ong, vol. 6014, Springer, 2010, pp. 94–108, doi:<a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">10.1007/978-3-642-12032-9_8</a>.","ista":"Wies T, Zufferey D, Henzinger TA. 2010. Forward analysis of depth-bounded processes. FoSSaCS: Foundations of Software Science and Computation Structures, LNCS, vol. 6014, 94–108.","chicago":"Wies, Thomas, Damien Zufferey, and Thomas A Henzinger. “Forward Analysis of Depth-Bounded Processes.” edited by Luke Ong, 6014:94–108. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">https://doi.org/10.1007/978-3-642-12032-9_8</a>.","short":"T. Wies, D. Zufferey, T.A. Henzinger, in:, L. Ong (Ed.), Springer, 2010, pp. 94–108."},"abstract":[{"lang":"eng","text":"Depth-bounded processes form the most expressive known fragment of the π-calculus for which interesting verification problems are still decidable. In this paper we develop an adequate domain of limits for the well-structured transition systems that are induced by depth-bounded processes. An immediate consequence of our result is that there exists a forward algorithm that decides the covering problem for this class. Unlike backward algorithms, the forward algorithm terminates even if the depth of the process is not known a priori. More importantly, our result suggests a whole spectrum of forward algorithms that enable the effective verification of a large class of mobile systems."}],"type":"conference","quality_controlled":"1","volume":6014,"department":[{"_id":"ToHe"}],"publisher":"Springer","corr_author":"1","publication_status":"published","date_created":"2018-12-11T12:08:27Z","conference":{"location":"Paphos, Cyprus","name":"FoSSaCS: Foundations of Software Science and Computation Structures","start_date":"2010-03-20","end_date":"2010-03-28"},"alternative_title":["LNCS"],"pubrep_id":"50","_id":"4361","month":"03","scopus_import":1,"file":[{"content_type":"application/pdf","checksum":"3e610de84937d821316362658239134a","relation":"main_file","date_updated":"2020-07-14T12:46:27Z","file_id":"4677","access_level":"open_access","creator":"system","file_size":240766,"date_created":"2018-12-12T10:08:17Z","file_name":"IST-2012-50-v1+1_Forward_analysis_of_depth-bounded_processes.pdf"}],"oa":1,"doi":"10.1007/978-3-642-12032-9_8","day":"01","date_published":"2010-03-01T00:00:00Z","intvolume":"      6014","year":"2010","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","ddc":["004"],"editor":[{"last_name":"Ong","full_name":"Ong, Luke","first_name":"Luke"}],"oa_version":"Submitted Version","publist_id":"1099","title":"Forward analysis of depth-bounded processes","author":[{"first_name":"Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Wies, Thomas","last_name":"Wies"},{"orcid":"0000-0002-3197-8736","last_name":"Zufferey","full_name":"Zufferey, Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","first_name":"Damien"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"date_updated":"2026-04-09T14:35:23Z","related_material":{"record":[{"relation":"dissertation_contains","id":"1405","status":"public"}]},"page":"94 - 108","status":"public","language":[{"iso":"eng"}],"has_accepted_license":"1","file_date_updated":"2020-07-14T12:46:27Z"},{"alternative_title":["ISTA Thesis"],"publication_status":"published","date_created":"2018-12-11T12:06:08Z","oa_version":"None","publist_id":"2165","language":[{"iso":"eng"}],"month":"07","status":"public","article_processing_charge":"No","title":"Dendritic cell migration across basement membranes in the skin","author":[{"last_name":"Pflicke","full_name":"Pflicke, Holger","id":"CAA57A9A-5B61-11E9-B130-E0C1E1F2C83D","first_name":"Holger"}],"_id":"3962","date_updated":"2026-04-09T14:37:07Z","degree_awarded":"PhD","publication_identifier":{"issn":["2663-337X"]},"year":"2010","type":"dissertation","day":"01","citation":{"short":"H. Pflicke,   Dendritic Cell Migration across Basement Membranes in the Skin, Institute of Science and Technology Austria, 2010.","ama":"Pflicke H.   Dendritic cell migration across basement membranes in the skin. 2010.","ieee":"H. Pflicke, “  Dendritic cell migration across basement membranes in the skin,” Institute of Science and Technology Austria, 2010.","apa":"Pflicke, H. (2010). <i>  Dendritic cell migration across basement membranes in the skin</i>. Institute of Science and Technology Austria.","chicago":"Pflicke, Holger. “  Dendritic Cell Migration across Basement Membranes in the Skin.” Institute of Science and Technology Austria, 2010.","ista":"Pflicke H. 2010.   Dendritic cell migration across basement membranes in the skin. Institute of Science and Technology Austria.","mla":"Pflicke, Holger. <i>  Dendritic Cell Migration across Basement Membranes in the Skin</i>. Institute of Science and Technology Austria, 2010."},"date_published":"2010-07-01T00:00:00Z","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","publisher":"Institute of Science and Technology Austria","corr_author":"1","OA_place":"publisher","supervisor":[{"first_name":"Carl-Philipp J","id":"39427864-F248-11E8-B48F-1D18A9856A87","last_name":"Heisenberg","full_name":"Heisenberg, Carl-Philipp J","orcid":"0000-0002-0912-4566"}],"department":[{"_id":"CaHe"},{"_id":"GradSch"}]},{"quality_controlled":"1","citation":{"short":"X. Yang, P.S. Riseborough, K.A. Modic, R.A. Fisher, C.P. Oppeil, T.R. Finlayson, J.C. Cooley, J.L. Smith, P.A. Goddard, A.V. Silhanek, J.C. Lashley, in:, Journal of Physics: Conference Series, IOP Publishing, 2009.","ista":"Yang X, Riseborough PS, Modic KA, Fisher RA, Oppeil CP, Finlayson TR, Cooley JC, Smith JL, Goddard PA, Silhanek AV, Lashley JC. 2009. Influence of magnetic fields on structural martensitic transitions. Journal of Physics: Conference Series. ICM: International Conference on Magnetism, JPCS, vol. 200, 032062.","chicago":"Yang, Xiaodong, Peter S Riseborough, Kimberly A Modic, R A Fisher, C P Oppeil, T R Finlayson, J C Cooley, et al. “Influence of Magnetic Fields on Structural Martensitic Transitions.” In <i>Journal of Physics: Conference Series</i>, Vol. 200. IOP Publishing, 2009. <a href=\"https://doi.org/10.1088/1742-6596/200/3/032062\">https://doi.org/10.1088/1742-6596/200/3/032062</a>.","mla":"Yang, Xiaodong, et al. “Influence of Magnetic Fields on Structural Martensitic Transitions.” <i>Journal of Physics: Conference Series</i>, vol. 200, no. 3, 032062, IOP Publishing, 2009, doi:<a href=\"https://doi.org/10.1088/1742-6596/200/3/032062\">10.1088/1742-6596/200/3/032062</a>.","apa":"Yang, X., Riseborough, P. S., Modic, K. A., Fisher, R. A., Oppeil, C. P., Finlayson, T. R., … Lashley, J. C. (2009). Influence of magnetic fields on structural martensitic transitions. In <i>Journal of Physics: Conference Series</i> (Vol. 200). Karlsruhe, Germany: IOP Publishing. <a href=\"https://doi.org/10.1088/1742-6596/200/3/032062\">https://doi.org/10.1088/1742-6596/200/3/032062</a>","ama":"Yang X, Riseborough PS, Modic KA, et al. Influence of magnetic fields on structural martensitic transitions. In: <i>Journal of Physics: Conference Series</i>. Vol 200. IOP Publishing; 2009. doi:<a href=\"https://doi.org/10.1088/1742-6596/200/3/032062\">10.1088/1742-6596/200/3/032062</a>","ieee":"X. Yang <i>et al.</i>, “Influence of magnetic fields on structural martensitic transitions,” in <i>Journal of Physics: Conference Series</i>, Karlsruhe, Germany, 2009, vol. 200, no. 3."},"type":"conference","extern":"1","abstract":[{"text":"We propose a model which suggests that structural martensitic transitions are related to significant changes in the electronic structure, and are effected by high-magnetic fields. The magnetic field dependence is considered unusual as many influential investigations of martensitic transitions have emphasized that the structural transitions are primarily lattice dynamical and are driven by the entropy due to the phonons. We provide a theoretical framework which can be used to describe the effect of high magnetic field on the transition and lattice dynamics in which the field dependence originates from the dielectric constant. The model is compared with some recent experimental results.","lang":"eng"}],"publisher":"IOP Publishing","volume":200,"alternative_title":["JPCS"],"conference":{"start_date":"2009-07-26","name":"ICM: International Conference on Magnetism","location":"Karlsruhe, Germany","end_date":"2009-07-31"},"date_created":"2022-08-08T08:43:04Z","publication_status":"published","scopus_import":"1","issue":"3","month":"07","_id":"11752","publication_identifier":{"issn":["1742-6588"],"eissn":["1742-6596"]},"year":"2009","article_number":"032062","date_published":"2009-07-01T00:00:00Z","intvolume":"       200","doi":"10.1088/1742-6596/200/3/032062","day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication":"Journal of Physics: Conference Series","oa_version":"None","article_processing_charge":"No","language":[{"iso":"eng"}],"status":"public","related_material":{"record":[{"id":"7080","relation":"later_version","status":"public"}]},"date_updated":"2023-02-23T12:58:33Z","title":"Influence of magnetic fields on structural martensitic transitions","author":[{"last_name":"Yang","full_name":"Yang, Xiaodong","first_name":"Xiaodong"},{"first_name":"Peter S","last_name":"Riseborough","full_name":"Riseborough, Peter S"},{"orcid":"0000-0001-9760-3147","id":"13C26AC0-EB69-11E9-87C6-5F3BE6697425","last_name":"Modic","full_name":"Modic, Kimberly A","first_name":"Kimberly A"},{"first_name":"R A","full_name":"Fisher, R A","last_name":"Fisher"},{"first_name":"C P","last_name":"Oppeil","full_name":"Oppeil, C P"},{"first_name":"T R","last_name":"Finlayson","full_name":"Finlayson, T R"},{"first_name":"J C","last_name":"Cooley","full_name":"Cooley, J C"},{"first_name":"J L","full_name":"Smith, J L","last_name":"Smith"},{"last_name":"Goddard","full_name":"Goddard, P A","first_name":"P A"},{"first_name":"A V","full_name":"Silhanek, A V","last_name":"Silhanek"},{"first_name":"J C","last_name":"Lashley","full_name":"Lashley, J C"}]},{"oa_version":"None","related_material":{"record":[{"status":"public","relation":"later_version","id":"11902"}]},"date_updated":"2024-11-06T12:24:12Z","page":"575-582","title":"Bidder optimal assignments for general utilities","author":[{"full_name":"Dütting, Paul","last_name":"Dütting","first_name":"Paul"},{"first_name":"Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"full_name":"Weber, Ingmar","last_name":"Weber","first_name":"Ingmar"}],"article_processing_charge":"No","status":"public","language":[{"iso":"eng"}],"date_published":"2009-12-01T00:00:00Z","intvolume":"      5929","doi":"10.1007/978-3-642-10841-9_58","day":"01","publication_identifier":{"isbn":["9783642108402"],"issn":["1611-3349"]},"year":"2009","publication":"5th International Workshop on Internet and Network Economics","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2022-08-11T12:33:38Z","publication_status":"published","alternative_title":["LNCS"],"conference":{"start_date":"2009-12-14","name":"WINE: International Conference on Web and Internet Economics","location":"Rome, Italy","end_date":"2009-12-18"},"_id":"11799","scopus_import":"1","month":"12","quality_controlled":"1","citation":{"ama":"Dütting P, Henzinger M, Weber I. Bidder optimal assignments for general utilities. In: <i>5th International Workshop on Internet and Network Economics</i>. Vol 5929. Springer Nature; 2009:575-582. doi:<a href=\"https://doi.org/10.1007/978-3-642-10841-9_58\">10.1007/978-3-642-10841-9_58</a>","ieee":"P. Dütting, M. Henzinger, and I. Weber, “Bidder optimal assignments for general utilities,” in <i>5th International Workshop on Internet and Network Economics</i>, Rome, Italy, 2009, vol. 5929, pp. 575–582.","apa":"Dütting, P., Henzinger, M., &#38; Weber, I. (2009). Bidder optimal assignments for general utilities. In <i>5th International Workshop on Internet and Network Economics</i> (Vol. 5929, pp. 575–582). Rome, Italy: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-10841-9_58\">https://doi.org/10.1007/978-3-642-10841-9_58</a>","chicago":"Dütting, Paul, Monika Henzinger, and Ingmar Weber. “Bidder Optimal Assignments for General Utilities.” In <i>5th International Workshop on Internet and Network Economics</i>, 5929:575–82. Springer Nature, 2009. <a href=\"https://doi.org/10.1007/978-3-642-10841-9_58\">https://doi.org/10.1007/978-3-642-10841-9_58</a>.","ista":"Dütting P, Henzinger M, Weber I. 2009. Bidder optimal assignments for general utilities. 5th International Workshop on Internet and Network Economics. WINE: International Conference on Web and Internet Economics, LNCS, vol. 5929, 575–582.","mla":"Dütting, Paul, et al. “Bidder Optimal Assignments for General Utilities.” <i>5th International Workshop on Internet and Network Economics</i>, vol. 5929, Springer Nature, 2009, pp. 575–82, doi:<a href=\"https://doi.org/10.1007/978-3-642-10841-9_58\">10.1007/978-3-642-10841-9_58</a>.","short":"P. Dütting, M. Henzinger, I. Weber, in:, 5th International Workshop on Internet and Network Economics, Springer Nature, 2009, pp. 575–582."},"abstract":[{"text":"We study the problem of matching bidders to items where each bidder i has general, strictly monotonic utility functions u i,j (p j ) expressing her utility of being matched to item j at price p j . For this setting we prove that a bidder optimal outcome always exists, even when the utility functions are non-linear and non-continuous. Furthermore, we give an algorithm to find such a solution. Although the running time of this algorithm is exponential in the number of items, it is polynomial in the number of bidders.","lang":"eng"}],"extern":"1","type":"conference","volume":5929,"publisher":"Springer Nature"},{"date_published":"2009-04-01T00:00:00Z","quality_controlled":"1","citation":{"mla":"Baykan, Eda, et al. “Purely URL-Based Topic Classification.” <i>18th International World Wide Web Conference</i>, Association for Computing Machinery, 2009, pp. 1109–10, doi:<a href=\"https://doi.org/10.1145/1526709.1526880\">10.1145/1526709.1526880</a>.","ista":"Baykan E, Henzinger M, Marian L, Weber I. 2009. Purely URL-based topic classification. 18th International World Wide Web Conference. WWW: Conference on World Wide Web, 1109–1110.","chicago":"Baykan, Eda, Monika Henzinger, Ludmila Marian, and Ingmar Weber. “Purely URL-Based Topic Classification.” In <i>18th International World Wide Web Conference</i>, 1109–10. Association for Computing Machinery, 2009. <a href=\"https://doi.org/10.1145/1526709.1526880\">https://doi.org/10.1145/1526709.1526880</a>.","apa":"Baykan, E., Henzinger, M., Marian, L., &#38; Weber, I. (2009). Purely URL-based topic classification. In <i>18th International World Wide Web Conference</i> (pp. 1109–1110). New York, NY, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/1526709.1526880\">https://doi.org/10.1145/1526709.1526880</a>","ama":"Baykan E, Henzinger M, Marian L, Weber I. Purely URL-based topic classification. In: <i>18th International World Wide Web Conference</i>. Association for Computing Machinery; 2009:1109-1110. doi:<a href=\"https://doi.org/10.1145/1526709.1526880\">10.1145/1526709.1526880</a>","ieee":"E. Baykan, M. Henzinger, L. Marian, and I. Weber, “Purely URL-based topic classification,” in <i>18th International World Wide Web Conference</i>, New York, NY, United States, 2009, pp. 1109–1110.","short":"E. Baykan, M. Henzinger, L. Marian, I. Weber, in:, 18th International World Wide Web Conference, Association for Computing Machinery, 2009, pp. 1109–1110."},"type":"conference","extern":"1","doi":"10.1145/1526709.1526880","day":"01","abstract":[{"lang":"eng","text":"Given only the URL of a web page, can we identify its topic? This is the question that we examine in this paper. Usually, web pages are classified using their content, but a URL-only classifier is preferable, (i) when speed is crucial, (ii) to enable content filtering before an (objection-able) web page is downloaded, (iii) when a page's content is hidden in images, (iv) to annotate hyperlinks in a personalized web browser, without fetching the target page, and (v) when a focused crawler wants to infer the topic of a target page before devoting bandwidth to download it. We apply a machine learning approach to the topic identification task and evaluate its performance in extensive experiments on categorized web pages from the Open Directory Project (ODP). When training separate binary classifiers for each topic, we achieve typical F-measure values between 80 and 85, and a typical precision of around 85. We also ran experiments on a small data set of university web pages. For the task of classifying these pages into faculty, student, course and project pages, our methods improve over previous approaches by 13.8 points of F-measure."}],"publication_identifier":{"isbn":["978-1-60558-487-4"]},"year":"2009","publication":"18th International World Wide Web Conference","publisher":"Association for Computing Machinery","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"None","date_created":"2022-08-17T11:49:53Z","publication_status":"published","conference":{"end_date":"2009-04-24","start_date":"2009-04-20","name":"WWW: Conference on World Wide Web","location":"New York, NY, United States"},"_id":"11905","page":"1109-1110","date_updated":"2024-11-06T12:24:48Z","title":"Purely URL-based topic classification","author":[{"last_name":"Baykan","full_name":"Baykan, Eda","first_name":"Eda"},{"first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H","last_name":"Henzinger","orcid":"0000-0002-5008-6530"},{"first_name":"Ludmila","full_name":"Marian, Ludmila","last_name":"Marian"},{"first_name":"Ingmar","full_name":"Weber, Ingmar","last_name":"Weber"}],"article_processing_charge":"No","scopus_import":"1","status":"public","month":"04","language":[{"iso":"eng"}]},{"quality_controlled":"1","date_published":"2009-04-01T00:00:00Z","abstract":[{"lang":"eng","text":"In the origin detection problem an algorithm is given a set S of documents, ordered by creation time, and a query document D. It needs to output for every consecutive sequence of k alphanumeric terms in D the earliest document in $S$ in which the sequence appeared (if such a document exists). Algorithms for the origin detection problem can, for example, be used to detect the \"origin\" of text segments in D and thus to detect novel content in D. They can also find the document from which the author of D has copied the most (or show that D is mostly original.) We concentrate on solutions that use only a fixed amount of memory. We propose novel algorithms for this problem and evaluate them together with a large number of previously published algorithms. Our results show that (1) detecting the origin of text segments efficiently can be done with very high accuracy even when the space used is less than 1% of the size of the documents in $S$, (2) the precision degrades smoothly with the amount of available space, (3) various estimation techniques can be used to increase the performance of the algorithms."}],"type":"conference","extern":"1","doi":"10.1145/1526709.1526719","day":"01","citation":{"ama":"Abdel Hamid O, Behzadi B, Christoph S, Henzinger M. Detecting the origin of text segments efficiently. In: <i>18th International World Wide Web Conference</i>. Association for Computing Machinery; 2009:61-70. doi:<a href=\"https://doi.org/10.1145/1526709.1526719\">10.1145/1526709.1526719</a>","apa":"Abdel Hamid, O., Behzadi, B., Christoph, S., &#38; Henzinger, M. (2009). Detecting the origin of text segments efficiently. In <i>18th International World Wide Web Conference</i> (pp. 61–70). Madrid, Spain: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/1526709.1526719\">https://doi.org/10.1145/1526709.1526719</a>","ieee":"O. Abdel Hamid, B. Behzadi, S. Christoph, and M. Henzinger, “Detecting the origin of text segments efficiently,” in <i>18th International World Wide Web Conference</i>, Madrid, Spain, 2009, pp. 61–70.","chicago":"Abdel Hamid, Ossama, Behshad Behzadi, Stefan Christoph, and Monika Henzinger. “Detecting the Origin of Text Segments Efficiently.” In <i>18th International World Wide Web Conference</i>, 61–70. Association for Computing Machinery, 2009. <a href=\"https://doi.org/10.1145/1526709.1526719\">https://doi.org/10.1145/1526709.1526719</a>.","ista":"Abdel Hamid O, Behzadi B, Christoph S, Henzinger M. 2009. Detecting the origin of text segments efficiently. 18th International World Wide Web Conference. WWW: International Conference on World Wide Web, 61–70.","mla":"Abdel Hamid, Ossama, et al. “Detecting the Origin of Text Segments Efficiently.” <i>18th International World Wide Web Conference</i>, Association for Computing Machinery, 2009, pp. 61–70, doi:<a href=\"https://doi.org/10.1145/1526709.1526719\">10.1145/1526709.1526719</a>.","short":"O. Abdel Hamid, B. Behzadi, S. Christoph, M. Henzinger, in:, 18th International World Wide Web Conference, Association for Computing Machinery, 2009, pp. 61–70."},"year":"2009","publication_identifier":{"isbn":["978-160558487-4"]},"publication":"18th International World Wide Web Conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Association for Computing Machinery","date_created":"2022-08-17T11:54:30Z","oa_version":"None","publication_status":"published","conference":{"end_date":"2009-04-24","start_date":"2009-04-20","name":"WWW: International Conference on World Wide Web","location":"Madrid, Spain"},"_id":"11906","date_updated":"2024-11-06T12:25:00Z","page":"61-70","author":[{"full_name":"Abdel Hamid, Ossama","last_name":"Abdel Hamid","first_name":"Ossama"},{"full_name":"Behzadi, Behshad","last_name":"Behzadi","first_name":"Behshad"},{"first_name":"Stefan","full_name":"Christoph, Stefan","last_name":"Christoph"},{"orcid":"0000-0002-5008-6530","last_name":"Henzinger","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H"}],"title":"Detecting the origin of text segments efficiently","scopus_import":"1","article_processing_charge":"No","month":"04","status":"public","language":[{"iso":"eng"}]},{"volume":3,"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","main_file_link":[{"url":"https://doi.org/10.4230/LIPIcs.STACS.2009.1809","open_access":"1"}],"abstract":[{"lang":"eng","text":"As the World Wide Web is growing rapidly, it is getting increasingly challenging to gather representative information about it. Instead of crawling the web exhaustively one has to resort to other techniques like sampling to determine the properties of the web. A uniform random sample of the web would be useful to determine the percentage of web pages in a specific language, on a topic or in a top level domain. Unfortunately, no approach has been shown to sample the web pages in an unbiased way. Three promising web sampling algorithms are based on random walks. They each have been evaluated individually, but making a comparison on different data sets is not possible. We directly compare these algorithms in this paper. We performed three random walks on the web under the same conditions and analyzed their outcomes in detail. We discuss the strengths and the weaknesses of each algorithm and propose improvements based on experimental results."}],"extern":"1","type":"conference","citation":{"ama":"Baykan  Eda, Henzinger M, Keller SF, de Castelberg S, Kinzler M. A comparison of techniques for sampling web pages. In: <i>26th International Symposium on Theoretical Aspects of Computer Science</i>. Vol 3. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2009:13-30. doi:<a href=\"https://doi.org/10.4230/LIPICS.STACS.2009.1809\">10.4230/LIPICS.STACS.2009.1809</a>","apa":"Baykan,  Eda, Henzinger, M., Keller, S. F., de Castelberg, S., &#38; Kinzler, M. (2009). A comparison of techniques for sampling web pages. In <i>26th International Symposium on Theoretical Aspects of Computer Science</i> (Vol. 3, pp. 13–30). Freiburg, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPICS.STACS.2009.1809\">https://doi.org/10.4230/LIPICS.STACS.2009.1809</a>","ieee":"Eda Baykan, M. Henzinger, S. F. Keller, S. de Castelberg, and M. Kinzler, “A comparison of techniques for sampling web pages,” in <i>26th International Symposium on Theoretical Aspects of Computer Science</i>, Freiburg, Germany, 2009, vol. 3, pp. 13–30.","chicago":"Baykan,  Eda, Monika Henzinger, Stefan F. Keller, Sebastian de Castelberg, and Markus Kinzler. “A Comparison of Techniques for Sampling Web Pages.” In <i>26th International Symposium on Theoretical Aspects of Computer Science</i>, 3:13–30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2009. <a href=\"https://doi.org/10.4230/LIPICS.STACS.2009.1809\">https://doi.org/10.4230/LIPICS.STACS.2009.1809</a>.","ista":"Baykan  Eda, Henzinger M, Keller SF, de Castelberg S, Kinzler M. 2009. A comparison of techniques for sampling web pages. 26th International Symposium on Theoretical Aspects of Computer Science. STACS: Symposium on Theoretical Aspects of Computer Science, LIPIcs, vol. 3, 13–30.","mla":"Baykan,  Eda, et al. “A Comparison of Techniques for Sampling Web Pages.” <i>26th International Symposium on Theoretical Aspects of Computer Science</i>, vol. 3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2009, pp. 13–30, doi:<a href=\"https://doi.org/10.4230/LIPICS.STACS.2009.1809\">10.4230/LIPICS.STACS.2009.1809</a>.","short":"Eda Baykan, M. Henzinger, S.F. Keller, S. de Castelberg, M. Kinzler, in:, 26th International Symposium on Theoretical Aspects of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2009, pp. 13–30."},"quality_controlled":"1","_id":"11912","month":"02","scopus_import":"1","publication_status":"published","date_created":"2022-08-18T06:57:25Z","conference":{"start_date":"2009-02-26","name":"STACS: Symposium on Theoretical Aspects of Computer Science","location":"Freiburg, Germany","end_date":"2009-02-28"},"external_id":{"arxiv":["0902.1604"]},"alternative_title":["LIPIcs"],"publication":"26th International Symposium on Theoretical Aspects of Computer Science","arxiv":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","doi":"10.4230/LIPICS.STACS.2009.1809","oa":1,"intvolume":"         3","date_published":"2009-02-01T00:00:00Z","publication_identifier":{"isbn":["978-3-939897-09-5"],"issn":["1868-8969"]},"year":"2009","author":[{"last_name":"Baykan","full_name":"Baykan,  Eda","first_name":" Eda"},{"first_name":"Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"full_name":"Keller, Stefan F.","last_name":"Keller","first_name":"Stefan F."},{"last_name":"de Castelberg","full_name":"de Castelberg, Sebastian","first_name":"Sebastian"},{"first_name":"Markus","full_name":"Kinzler, Markus","last_name":"Kinzler"}],"title":"A comparison of techniques for sampling web pages","date_updated":"2024-11-06T12:25:24Z","page":"13-30","status":"public","language":[{"iso":"eng"}],"article_processing_charge":"No","oa_version":"Published Version"},{"publisher":"Society for Neuroscience","volume":29,"publication":"Journal of Neuroscience","year":"2009","citation":{"short":"N. Guetg, R. Seddik, R. Vigot, R. Tureček, M. Gassmann, K. Vogt, H. Bräuner Osborne, R. Shigemoto, O. Kretz, M. Frotscher, Á. Kulik, B. Bettler, Journal of Neuroscience 29 (2009) 1414–1423.","ama":"Guetg N, Seddik R, Vigot R, et al. The GABA B1a isoform mediates heterosynaptic depression at hippocampal mossy fiber synapses. <i>Journal of Neuroscience</i>. 2009;29(5):1414-1423. doi:<a href=\"https://doi.org/10.1523/JNEUROSCI.3697-08.2009\">10.1523/JNEUROSCI.3697-08.2009</a>","apa":"Guetg, N., Seddik, R., Vigot, R., Tureček, R., Gassmann, M., Vogt, K., … Bettler, B. (2009). The GABA B1a isoform mediates heterosynaptic depression at hippocampal mossy fiber synapses. <i>Journal of Neuroscience</i>. Society for Neuroscience. <a href=\"https://doi.org/10.1523/JNEUROSCI.3697-08.2009\">https://doi.org/10.1523/JNEUROSCI.3697-08.2009</a>","ieee":"N. Guetg <i>et al.</i>, “The GABA B1a isoform mediates heterosynaptic depression at hippocampal mossy fiber synapses,” <i>Journal of Neuroscience</i>, vol. 29, no. 5. Society for Neuroscience, pp. 1414–1423, 2009.","mla":"Guetg, Nicole, et al. “The GABA B1a Isoform Mediates Heterosynaptic Depression at Hippocampal Mossy Fiber Synapses.” <i>Journal of Neuroscience</i>, vol. 29, no. 5, Society for Neuroscience, 2009, pp. 1414–23, doi:<a href=\"https://doi.org/10.1523/JNEUROSCI.3697-08.2009\">10.1523/JNEUROSCI.3697-08.2009</a>.","ista":"Guetg N, Seddik R, Vigot R, Tureček R, Gassmann M, Vogt K, Bräuner Osborne H, Shigemoto R, Kretz O, Frotscher M, Kulik Á, Bettler B. 2009. The GABA B1a isoform mediates heterosynaptic depression at hippocampal mossy fiber synapses. Journal of Neuroscience. 29(5), 1414–1423.","chicago":"Guetg, Nicole, Riad Seddik, Réjan Vigot, Rostislav Tureček, Martin Gassmann, Kaspar Vogt, Hans Bräuner Osborne, et al. “The GABA B1a Isoform Mediates Heterosynaptic Depression at Hippocampal Mossy Fiber Synapses.” <i>Journal of Neuroscience</i>. Society for Neuroscience, 2009. <a href=\"https://doi.org/10.1523/JNEUROSCI.3697-08.2009\">https://doi.org/10.1523/JNEUROSCI.3697-08.2009</a>."},"abstract":[{"lang":"eng","text":"GABA B receptor subtypes are based on the subunit isoforms GABA B1a and GABA B1b, which associate with GABA B2 subunits to form pharmacologically indistinguishable GABA B(1a,2) and GABA B(1b,2) receptors. Studies with mice selectively expressing GABA B1a or GABA B1b subunits revealed that GABA B(1a,2) receptors are more abundant than GABA B(1b,2) receptors at glutamatergic terminals. Accordingly, it was found that GABA B(1a,2) receptors are more efficient than GABA B(1b,2) receptors in inhibiting glutamate release when maximally activated by exogenous application of the agonist baclofen. Here, we used a combination of genetic, ultrastructural and electrophysiological approaches to analyze to what extent GABA B(1a,2) and GABA B(1b,2) receptors inhibit glutamate release in response to physiological activation. We first show that at hippocampal mossy fiber (MF)-CA3 pyramidal neuron synapses more GABA B1a than GABA B1b protein is present at presynaptic sites, consistent with the findings at other glutamatergic synapses. In the presence of baclofen at concentrations ≥1 μM, both GABA B(1a,2) and GABA B(1b,2) receptors contribute to presynaptic inhibition of glutamate release. However, at lower concentrations of baclofen, selectively GABA B(1a,2) receptors contribute to presynaptic inhibition. Remarkably, exclusively GABA B(1a,2) receptors inhibit glutamate release in response to synaptically released GABA. Specifically, we demonstrate that selectively GABA B(1a,2) receptors mediate heterosynaptic depression of MF transmission, a physiological phenomenon involving transsynaptic inhibition of glutamate release via presynaptic GABA B receptors. Our data demonstrate that the difference in GABA B1a and GABA B1b protein levels at MF terminals is sufficient to produce a strictly GABA B1a-specific effect under physiological conditions. This consolidates that the differential subcellular localization of the GABA B1a and GABA B1b proteins is of regulatory relevance. "}],"type":"journal_article","doi":"10.1523/JNEUROSCI.3697-08.2009","extern":1,"day":"04","date_published":"2009-02-04T00:00:00Z","intvolume":"        29","quality_controlled":0,"month":"02","status":"public","issue":"5","author":[{"first_name":"Nicole","last_name":"Guetg","full_name":"Guetg, Nicole"},{"first_name":"Riad","full_name":"Seddik, Riad","last_name":"Seddik"},{"first_name":"Réjan","last_name":"Vigot","full_name":"Vigot, Réjan"},{"first_name":"Rostislav","last_name":"Tureček","full_name":"Tureček, Rostislav"},{"first_name":"Martin","full_name":"Gassmann, Martin","last_name":"Gassmann"},{"first_name":"Kaspar","full_name":"Vogt, Kaspar E","last_name":"Vogt"},{"last_name":"Bräuner Osborne","full_name":"Bräuner-Osborne, Hans","first_name":"Hans"},{"orcid":"0000-0001-8761-9444","full_name":"Ryuichi Shigemoto","last_name":"Shigemoto","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","first_name":"Ryuichi"},{"last_name":"Kretz","full_name":"Kretz, Oliver","first_name":"Oliver"},{"first_name":"Michael","last_name":"Frotscher","full_name":"Frotscher, Michael"},{"first_name":"Ákos","full_name":"Kulik, Ákos","last_name":"Kulik"},{"first_name":"Bernhard","full_name":"Bettler, Bernhard","last_name":"Bettler"}],"title":"The GABA B1a isoform mediates heterosynaptic depression at hippocampal mossy fiber synapses","date_updated":"2021-01-12T06:59:01Z","_id":"2680","page":"1414 - 1423","publication_status":"published","publist_id":"4216","date_created":"2018-12-11T11:59:02Z"},{"year":"2009","extern":1,"day":"12","doi":"10.1002/adma.200802312","type":"journal_article","abstract":[{"text":"The living cell imaging using a two-photon microscope using gold nanoplates and nanoparticle aggregates was demonstrated. The dimensions of the nanoplates were determined through scanning electron microscopy (SEM) and atomic force microscopy. The height of a 100 nm base-length nanotriangle was around 10 nm, while the height of 300 nm base-length nanotriangle was around 12 nm. A spectrophotometer was also used to determine the extinction spectra of gold nanoparticle colloids. Two-photon-induced photoluminescence (TPIPL) under far-field excitation was tested for gold nanoplates on a glass substrate using two-photon laser scanning microscopy (TPLSM). It was observed that living-cell microscopic imaging can be carried out with TPIPL from gold nanoplates and aggregated nanosphere. This method provided a platform for developing tools for biological and biomedical studies.","lang":"eng"}],"citation":{"short":"Y. Jiang, N. Horimoto, K. Imura, K. Matsui, R. Shigemoto, Advanced Materials 21 (2009) 2309–2313.","chicago":"Jiang, Yuqiang, Noriko Horimoto, Kohei Imura, Ko Matsui, and Ryuichi Shigemoto. “Bioimaging with Two-Photon-Induced Luminescence from Triangular Nanoplates and Nanoparticle Aggregates of Gold.” <i>Advanced Materials</i>. Wiley-Blackwell, 2009. <a href=\"https://doi.org/10.1002/adma.200802312\">https://doi.org/10.1002/adma.200802312</a>.","ista":"Jiang Y, Horimoto N, Imura K, Matsui K, Shigemoto R. 2009. Bioimaging with two-photon-induced luminescence from triangular nanoplates and nanoparticle aggregates of gold. Advanced Materials. 21(22), 2309–2313.","mla":"Jiang, Yuqiang, et al. “Bioimaging with Two-Photon-Induced Luminescence from Triangular Nanoplates and Nanoparticle Aggregates of Gold.” <i>Advanced Materials</i>, vol. 21, no. 22, Wiley-Blackwell, 2009, pp. 2309–13, doi:<a href=\"https://doi.org/10.1002/adma.200802312\">10.1002/adma.200802312</a>.","ama":"Jiang Y, Horimoto N, Imura K, Matsui K, Shigemoto R. Bioimaging with two-photon-induced luminescence from triangular nanoplates and nanoparticle aggregates of gold. <i>Advanced Materials</i>. 2009;21(22):2309-2313. doi:<a href=\"https://doi.org/10.1002/adma.200802312\">10.1002/adma.200802312</a>","ieee":"Y. Jiang, N. Horimoto, K. Imura, K. Matsui, and R. Shigemoto, “Bioimaging with two-photon-induced luminescence from triangular nanoplates and nanoparticle aggregates of gold,” <i>Advanced Materials</i>, vol. 21, no. 22. Wiley-Blackwell, pp. 2309–2313, 2009.","apa":"Jiang, Y., Horimoto, N., Imura, K., Matsui, K., &#38; Shigemoto, R. (2009). Bioimaging with two-photon-induced luminescence from triangular nanoplates and nanoparticle aggregates of gold. <i>Advanced Materials</i>. Wiley-Blackwell. <a href=\"https://doi.org/10.1002/adma.200802312\">https://doi.org/10.1002/adma.200802312</a>"},"intvolume":"        21","quality_controlled":0,"date_published":"2009-06-12T00:00:00Z","publisher":"Wiley-Blackwell","volume":21,"publication":"Advanced Materials","publication_status":"published","date_created":"2018-12-11T11:59:02Z","publist_id":"4214","month":"06","status":"public","issue":"22","title":"Bioimaging with two-photon-induced luminescence from triangular nanoplates and nanoparticle aggregates of gold","author":[{"first_name":"Yuqiang","full_name":"Jiang, Yuqiang","last_name":"Jiang"},{"first_name":"Noriko","full_name":"Horimoto, Noriko N","last_name":"Horimoto"},{"first_name":"Kohei","last_name":"Imura","full_name":"Imura, Kohei"},{"full_name":"Matsui, Ko","last_name":"Matsui","first_name":"Ko"},{"orcid":"0000-0001-8761-9444","last_name":"Shigemoto","full_name":"Ryuichi Shigemoto","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","first_name":"Ryuichi"}],"_id":"2682","page":"2309 - 2313","date_updated":"2021-01-12T06:59:01Z"},{"publication":"Neuron","volume":61,"publisher":"Elsevier","date_published":"2009-03-26T00:00:00Z","quality_controlled":0,"intvolume":"        61","citation":{"ama":"Pan B, Dong Y, Ito W, Yanagawa Y, Shigemoto R, Morozov A. Selective gating of glutamatergic inputs to excitatory neurons of amygdala by presynaptic GABAb receptor. <i>Neuron</i>. 2009;61(6):917-929. doi:<a href=\"https://doi.org/10.1016/j.neuron.2009.01.029\">10.1016/j.neuron.2009.01.029</a>","ieee":"B. Pan, Y. Dong, W. Ito, Y. Yanagawa, R. Shigemoto, and A. Morozov, “Selective gating of glutamatergic inputs to excitatory neurons of amygdala by presynaptic GABAb receptor,” <i>Neuron</i>, vol. 61, no. 6. Elsevier, pp. 917–929, 2009.","apa":"Pan, B., Dong, Y., Ito, W., Yanagawa, Y., Shigemoto, R., &#38; Morozov, A. (2009). Selective gating of glutamatergic inputs to excitatory neurons of amygdala by presynaptic GABAb receptor. <i>Neuron</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.neuron.2009.01.029\">https://doi.org/10.1016/j.neuron.2009.01.029</a>","mla":"Pan, Bingxing, et al. “Selective Gating of Glutamatergic Inputs to Excitatory Neurons of Amygdala by Presynaptic GABAb Receptor.” <i>Neuron</i>, vol. 61, no. 6, Elsevier, 2009, pp. 917–29, doi:<a href=\"https://doi.org/10.1016/j.neuron.2009.01.029\">10.1016/j.neuron.2009.01.029</a>.","ista":"Pan B, Dong Y, Ito W, Yanagawa Y, Shigemoto R, Morozov A. 2009. Selective gating of glutamatergic inputs to excitatory neurons of amygdala by presynaptic GABAb receptor. Neuron. 61(6), 917–929.","chicago":"Pan, Bingxing, Yu Dong, Wataru Ito, Yuchio Yanagawa, Ryuichi Shigemoto, and Alexei Morozov. “Selective Gating of Glutamatergic Inputs to Excitatory Neurons of Amygdala by Presynaptic GABAb Receptor.” <i>Neuron</i>. Elsevier, 2009. <a href=\"https://doi.org/10.1016/j.neuron.2009.01.029\">https://doi.org/10.1016/j.neuron.2009.01.029</a>.","short":"B. Pan, Y. Dong, W. Ito, Y. Yanagawa, R. Shigemoto, A. Morozov, Neuron 61 (2009) 917–929."},"abstract":[{"lang":"eng","text":"GABAb receptor (GABAbR)-mediated suppression of glutamate release is critical for limiting glutamatergic transmission across the central nervous system (CNS). Here we show that, upon tetanic stimulation of afferents to lateral amygdala, presynaptic GABAbR-mediated inhibition only occurs in glutamatergic inputs to principle neurons (PNs), not to interneurons (INs), despite the presence of GABAbR in terminals to both types of neurons. The selectivity is caused by differential local GABA accumulation; it requires GABA reuptake and parallels distinct spatial distributions of presynaptic GABAbR in terminals to PNs and INs. Moreover, GABAbR-mediated suppression of theta-burst-induced long-term potentiation (LTP) occurs only in the inputs to PNs, not to INs. Thus, target-cell-specific control of glutamate release by presynaptic GABAbR orchestrates the inhibitory dominance inside amygdala and might contribute to prevention of nonadaptive defensive behaviors."}],"doi":"10.1016/j.neuron.2009.01.029","day":"26","type":"journal_article","extern":1,"year":"2009","page":"917 - 929","_id":"2683","date_updated":"2021-01-12T06:59:02Z","title":"Selective gating of glutamatergic inputs to excitatory neurons of amygdala by presynaptic GABAb receptor","author":[{"last_name":"Pan","full_name":"Pan, Bingxing","first_name":"Bingxing"},{"last_name":"Dong","full_name":"Dong, Yu-Lin","first_name":"Yu"},{"first_name":"Wataru","last_name":"Ito","full_name":"Ito, Wataru"},{"last_name":"Yanagawa","full_name":"Yanagawa, Yuchio","first_name":"Yuchio"},{"orcid":"0000-0001-8761-9444","full_name":"Ryuichi Shigemoto","last_name":"Shigemoto","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","first_name":"Ryuichi"},{"first_name":"Alexei","full_name":"Morozov, Alexei A","last_name":"Morozov"}],"issue":"6","status":"public","month":"03","publist_id":"4215","date_created":"2018-12-11T11:59:03Z","publication_status":"published"},{"publication_status":"published","publist_id":"4212","date_created":"2018-12-11T11:59:03Z","author":[{"first_name":"Walter","full_name":"Walter Kaufmann","last_name":"Kaufmann","id":"3F99E422-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-9735-5315"},{"first_name":"Francesco","last_name":"Ferraguti","full_name":"Ferraguti, Francesco"},{"first_name":"Yugo","last_name":"Fukazawa","full_name":"Fukazawa, Yugo"},{"last_name":"Kasugai","full_name":"Kasugai, Yu","first_name":"Yu"},{"first_name":"Ryuichi","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","full_name":"Ryuichi Shigemoto","last_name":"Shigemoto","orcid":"0000-0001-8761-9444"},{"first_name":"Petter","full_name":"Laake, Petter","last_name":"Laake"},{"first_name":"Joseph","last_name":"Sexton","full_name":"Sexton, Joseph A"},{"last_name":"Ruth","full_name":"Ruth, Peter","first_name":"Peter"},{"last_name":"Wietzorrek","full_name":"Wietzorrek, Georg","first_name":"Georg"},{"first_name":"Hans","last_name":"Knaus","full_name":"Knaus, Hans G"},{"last_name":"Storm","full_name":"Storm, Johan F","first_name":"Johan"},{"full_name":"Ottersen, Ole P","last_name":"Ottersen","first_name":"Ole"}],"title":"Large-conductance calcium-activated potassium channels in Purkinje cell plasma membranes are clustered at sites of hypolemmal microdomains","_id":"2684","date_updated":"2023-02-23T10:53:41Z","page":"215 - 230","month":"07","status":"public","issue":"2","citation":{"short":"W. Kaufmann, F. Ferraguti, Y. Fukazawa, Y. Kasugai, R. Shigemoto, P. Laake, J. Sexton, P. Ruth, G. Wietzorrek, H. Knaus, J. Storm, O. Ottersen, Journal of Comparative Neurology 515 (2009) 215–230.","mla":"Kaufmann, Walter, et al. “Large-Conductance Calcium-Activated Potassium Channels in Purkinje Cell Plasma Membranes Are Clustered at Sites of Hypolemmal Microdomains.” <i>Journal of Comparative Neurology</i>, vol. 515, no. 2, Wiley-Blackwell, 2009, pp. 215–30, doi:<a href=\"https://doi.org/10.1002/cne.22066\">10.1002/cne.22066</a>.","ista":"Kaufmann W, Ferraguti F, Fukazawa Y, Kasugai Y, Shigemoto R, Laake P, Sexton J, Ruth P, Wietzorrek G, Knaus H, Storm J, Ottersen O. 2009. Large-conductance calcium-activated potassium channels in Purkinje cell plasma membranes are clustered at sites of hypolemmal microdomains. Journal of Comparative Neurology. 515(2), 215–230.","chicago":"Kaufmann, Walter, Francesco Ferraguti, Yugo Fukazawa, Yu Kasugai, Ryuichi Shigemoto, Petter Laake, Joseph Sexton, et al. “Large-Conductance Calcium-Activated Potassium Channels in Purkinje Cell Plasma Membranes Are Clustered at Sites of Hypolemmal Microdomains.” <i>Journal of Comparative Neurology</i>. Wiley-Blackwell, 2009. <a href=\"https://doi.org/10.1002/cne.22066\">https://doi.org/10.1002/cne.22066</a>.","ama":"Kaufmann W, Ferraguti F, Fukazawa Y, et al. Large-conductance calcium-activated potassium channels in Purkinje cell plasma membranes are clustered at sites of hypolemmal microdomains. <i>Journal of Comparative Neurology</i>. 2009;515(2):215-230. doi:<a href=\"https://doi.org/10.1002/cne.22066\">10.1002/cne.22066</a>","apa":"Kaufmann, W., Ferraguti, F., Fukazawa, Y., Kasugai, Y., Shigemoto, R., Laake, P., … Ottersen, O. (2009). Large-conductance calcium-activated potassium channels in Purkinje cell plasma membranes are clustered at sites of hypolemmal microdomains. <i>Journal of Comparative Neurology</i>. Wiley-Blackwell. <a href=\"https://doi.org/10.1002/cne.22066\">https://doi.org/10.1002/cne.22066</a>","ieee":"W. Kaufmann <i>et al.</i>, “Large-conductance calcium-activated potassium channels in Purkinje cell plasma membranes are clustered at sites of hypolemmal microdomains,” <i>Journal of Comparative Neurology</i>, vol. 515, no. 2. Wiley-Blackwell, pp. 215–230, 2009."},"abstract":[{"text":"Calcium-activated potassium channels have been shown to be critically involved in neuronal function, but an elucidation of their detailed roles awaits identification of the microdomains where they are located. This study was undertaken to unravel the precise subcellular distribution of the large-conductance calcium-activated potassium channels (called BK, KCa1.1, or Slo1) in the somatodendritic compartment of cerebellar Purkinje cells by means of postembedding immunogold cytochemistry and SDS-digested freeze-fracture replica labeling (SDS-FRL). We found BK channels to be unevenly distributed over the Purkinje cell plasma membrane. At distal dendritic compartments, BK channels were scattered over the plasma membrane of dendritic shafts and spines but absent from postsynaptic densities. At the soma and proximal dendrites, BK channels formed two distinct pools. One pool was scattered over the plasma membrane, whereas the other pool was clustered in plasma membrane domains overlying subsurface cisterns. The labeling density ratio of clustered to scattered channels was about 60:1, established in SDS-FRL. Subsurface cisterns, also called hypolemmal cisterns, are subcompartments of the endoplasmic reticulum likely representing calciosomes that unload and refill Ca2+ independently. Purkinje cell subsurface cisterns are enriched in inositol 1,4,5-triphosphate receptors that mediate the effects of several neurotransmitters, hormones, and growth factors by releasing Ca2+ into the cytosol, generating local Ca2+ sparks. Such increases in cytosolic [Ca2+] may be sufficient for BK channel activation. Clustered BK channels in the plasma membrane may thus participate in building a functional unit (plasmerosome) with the underlying calciosome that contributes significantly to local signaling in Purkinje cells.","lang":"eng"}],"day":"10","extern":1,"type":"journal_article","doi":"10.1002/cne.22066","date_published":"2009-07-10T00:00:00Z","intvolume":"       515","quality_controlled":0,"year":"2009","volume":515,"publication":"Journal of Comparative Neurology","publisher":"Wiley-Blackwell"}]