[{"citation":{"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.","mla":"Aviv, Adam, et al. “Security Evaluation of ES&#38;S Voting Machines and Election Management System.” <i>17th USENIX Security Symposium</i>, 2008.","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.","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.","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.","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."},"date_published":"2008-07-29T00:00:00Z","oa":1,"year":"2008","publication_status":"published","_id":"4400","article_processing_charge":"No","month":"07","date_updated":"2025-07-02T05:38:10Z","extern":"1","title":"Security evaluation of ES&S voting machines and election management system","type":"conference","author":[{"first_name":"Adam","full_name":"Aviv, Adam","last_name":"Aviv"},{"first_name":"Pavol","last_name":"Cerny","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","full_name":"Cerny, Pavol"},{"last_name":"Clark","full_name":"Clark, Sandy","first_name":"Sandy"},{"full_name":"Cronin, Eric","last_name":"Cronin","first_name":"Eric"},{"last_name":"Shah","full_name":"Shah, Gaurav","first_name":"Gaurav"},{"full_name":"Sherr, Micah","last_name":"Sherr","first_name":"Micah"},{"full_name":"Blaze, Matt","last_name":"Blaze","first_name":"Matt"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"None","day":"29","date_created":"2018-12-11T12:08:39Z","status":"public","language":[{"iso":"eng"}],"publication":"17th USENIX Security Symposium","main_file_link":[{"url":"http://www.usenix.org/event/evt08/tech/full_papers/aviv/aviv.pdf","open_access":"1"}],"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"}],"conference":{"location":"San Jose, CA, United States","start_date":"2008-07-28","end_date":"2008-07-29","name":"USENIX: Security Symposium"},"publist_id":"1057"},{"date_updated":"2022-02-14T14:35:11Z","month":"09","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","author":[{"first_name":"Vinayak","last_name":"Prabhu","full_name":"Prabhu, Vinayak"}],"type":"dissertation","title":"Games for the verification of timed systems","extern":"1","date_published":"2008-09-01T00:00:00Z","oa":1,"year":"2008","citation":{"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.","ista":"Prabhu V. 2008. Games for the verification of timed systems. University of California, Berkeley.","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.","apa":"Prabhu, V. (2008). <i>Games for the verification of timed systems</i>. University of California, Berkeley.","short":"V. Prabhu, Games for the Verification of Timed Systems, University of California, Berkeley, 2008."},"article_processing_charge":"No","publisher":"University of California, Berkeley","_id":"4409","degree_awarded":"PhD","publication_status":"published","abstract":[{"lang":"eng","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."}],"main_file_link":[{"open_access":"1","url":"https://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-97.html"}],"publist_id":"319","page":"1 - 137","status":"public","date_created":"2018-12-11T12:08:42Z","supervisor":[{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"last_name":"Steel","full_name":"Steel, John","first_name":"John"},{"full_name":"Varaiya, Pravin","last_name":"Varaiya","first_name":"Pravin"}],"day":"01","oa_version":"None","language":[{"iso":"eng"}]},{"abstract":[{"lang":"eng","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."}],"page":"1 - 148","publist_id":"316","oa_version":"None","day":"01","supervisor":[{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Edward","full_name":"Lee, Edward","last_name":"Lee"},{"first_name":"Raja","last_name":"Sengupta","full_name":"Sengupta, Raja"}],"date_created":"2018-12-11T12:08:44Z","status":"public","language":[{"iso":"eng"}],"month":"01","date_updated":"2022-02-14T14:08:50Z","extern":"1","title":"Compositionality in deterministic real-time embedded systems","type":"dissertation","acknowledgement":"978-0-549-83480-9","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","author":[{"first_name":"Slobodan","full_name":"Matic, Slobodan","last_name":"Matic"}],"citation":{"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.","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.","apa":"Matic, S. (2008). <i>Compositionality in deterministic real-time embedded systems</i>. University of California, Berkeley.","short":"S. Matic, Compositionality in Deterministic Real-Time Embedded Systems, University of California, Berkeley, 2008."},"date_published":"2008-01-01T00:00:00Z","year":"2008","publication_status":"published","degree_awarded":"PhD","_id":"4415","publisher":"University of California, Berkeley","article_processing_charge":"No"},{"citation":{"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>","short":"T.A. Henzinger, T. Hottelier, L. Kovács, in:, Springer, 2008, pp. 333–342.","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>.","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>","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.","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>.","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."},"date_published":"2008-11-13T00:00:00Z","year":"2008","publication_status":"published","_id":"4452","doi":"10.1007/978-3-540-89439-1_24","publisher":"Springer","month":"11","date_updated":"2021-01-12T07:57:04Z","extern":1,"title":"Valigator: A verification tool with bound and invariant generation","type":"conference","acknowledgement":"This research was supported by the Swiss NSF.","author":[{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger"},{"full_name":"Hottelier, Thibaud","last_name":"Hottelier","first_name":"Thibaud"},{"first_name":"Laura","full_name":"Kovács, Laura","last_name":"Kovács"}],"day":"13","volume":5330,"date_created":"2018-12-11T12:08:55Z","status":"public","quality_controlled":0,"alternative_title":["LNCS"],"main_file_link":[{"open_access":"0","url":"http://pub.ist.ac.at/%7Etah/Publications/valigator.pdf"}],"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"}],"conference":{"name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning"},"page":"333 - 342","intvolume":"      5330","publist_id":"277"},{"publication":"Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences","quality_controlled":0,"status":"public","date_created":"2018-12-11T12:09:13Z","volume":366,"day":"31","publist_id":"219","intvolume":"       366","page":"3727 - 3736","abstract":[{"lang":"eng","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."}],"main_file_link":[{"url":"http://pub.ist.ac.at/%7Etah/Publications/two_challenges_in_embedded_systems_design.pdf","open_access":"0"}],"publisher":"Royal Society of London","doi":"10.1098/rsta.2008.0141","_id":"4509","publication_status":"published","year":"2008","date_published":"2008-07-31T00:00:00Z","citation":{"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>.","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>","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>","short":"T.A. Henzinger, Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences 366 (2008) 3727–3736.","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>.","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.","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."},"author":[{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger"}],"type":"journal_article","title":"Two challenges in embedded systems design: Predictability and robustness","extern":1,"date_updated":"2021-01-12T07:59:19Z","month":"07","issue":"1881"},{"month":"01","date_updated":"2021-01-12T07:59:25Z","type":"conference","author":[{"first_name":"Ashutosh","last_name":"Gupta","full_name":"Ashutosh Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar S"},{"first_name":"Andrey","full_name":"Rybalchenko, Andrey","last_name":"Rybalchenko"},{"full_name":"Xu, Ru-Gang","last_name":"Xu","first_name":"Ru"}],"extern":1,"title":"Proving non-termination","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>","short":"A. Gupta, T.A. Henzinger, R. Majumdar, A. Rybalchenko, R. Xu, in:, ACM, 2008, pp. 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>","ista":"Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R. 2008. Proving non-termination. POPL: Principles of Programming Languages, 147–158.","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."},"date_published":"2008-01-01T00:00:00Z","year":"2008","doi":"10.1145/1328438.1328459","publisher":"ACM","publication_status":"published","_id":"4521","main_file_link":[{"open_access":"0","url":"http://pub.ist.ac.at/%7Etah/Publications/proving_non-termination.pdf"}],"abstract":[{"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.","lang":"eng"}],"publist_id":"208","conference":{"name":"POPL: Principles of Programming Languages"},"page":"147 - 158","status":"public","date_created":"2018-12-11T12:09:17Z","day":"01","quality_controlled":0},{"type":"dissertation","acknowledgement":"978-0-549-83679-7","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Ghosal","full_name":"Ghosal, Arkadeb","first_name":"Arkadeb"}],"extern":"1","title":"A hierarchical coordination language for reliable real-time tasks","month":"01","date_updated":"2021-01-12T07:59:26Z","publisher":"University of California, Berkeley","article_processing_charge":"No","publication_status":"published","_id":"4524","citation":{"ista":"Ghosal A. 2008. A hierarchical coordination language for reliable real-time tasks. University of California, Berkeley.","mla":"Ghosal, Arkadeb. <i>A Hierarchical Coordination Language for Reliable Real-Time Tasks</i>. University of California, Berkeley, 2008, pp. 1–210.","ieee":"A. Ghosal, “A hierarchical coordination language for reliable real-time tasks,” University of California, Berkeley, 2008.","apa":"Ghosal, A. (2008). <i>A hierarchical coordination language for reliable real-time tasks</i>. University of California, Berkeley.","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."},"date_published":"2008-01-31T00:00:00Z","year":"2008","publist_id":"199","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."}],"language":[{"iso":"eng"}],"date_created":"2018-12-11T12:09:18Z","status":"public","oa_version":"None","day":"31","supervisor":[{"first_name":"Alberto","last_name":"Sangiovanni-Vincentelli","full_name":"Sangiovanni-Vincentelli, Alberto"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724"},{"last_name":"Lee","full_name":"Lee, Edward","first_name":"Edward"},{"first_name":"Karl","last_name":"Hedrick","full_name":"Hedrick, Karl"}]},{"date_published":"2008-05-26T00:00:00Z","year":"2008","citation":{"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.","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>","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>","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>."},"_id":"4527","publication_status":"published","publisher":"Springer","doi":"10.1007/978-3-540-68413-8_2","date_updated":"2021-01-12T07:59:27Z","month":"05","title":"Bounded asynchrony: Concurrency for modeling cell-cell interactions","extern":1,"author":[{"full_name":"Fisher, Jasmin","last_name":"Fisher","first_name":"Jasmin"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger"},{"last_name":"Mateescu","id":"3B43276C-F248-11E8-B48F-1D18A9856A87","full_name":"Maria Mateescu","first_name":"Maria"},{"last_name":"Piterman","full_name":"Piterman, Nir","first_name":"Nir"}],"acknowledgement":"Supported in part by the Swiss National Science Foundation (grant 205321-111840).","type":"conference","day":"26","volume":5054,"status":"public","date_created":"2018-12-11T12:09:19Z","quality_controlled":0,"alternative_title":["LNCS"],"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."}],"main_file_link":[{"url":"http://pub.ist.ac.at/%7Etah/Publications/bounded_asynchrony.pdf","open_access":"0"}],"conference":{"name":"FMSB: Formal Methods in Systems Biology"},"page":"17 - 32","intvolume":"      5054","publist_id":"196"},{"publication":"International Journal of Foundations of Computer Science","quality_controlled":0,"status":"public","date_created":"2018-12-11T12:09:20Z","volume":19,"day":"01","publist_id":"192","intvolume":"        19","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."}],"main_file_link":[{"url":"http://pub.ist.ac.at/%7Etah/Publications/equivalence_of_labeled_markov_chains.pdf","open_access":"0"}],"publisher":"World Scientific Publishing","doi":"10.1142/S0129054108005814 ","_id":"4532","publication_status":"published","year":"2008","date_published":"2008-06-01T00:00:00Z","citation":{"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>","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>.","short":"L. Doyen, T.A. Henzinger, J. Raskin, International Journal of Foundations of Computer Science 19 (2008) 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>","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>.","ista":"Doyen L, Henzinger TA, Raskin J. 2008. Equivalence of labeled Markov chains. International Journal of Foundations of Computer Science. 19(3), 549–563."},"author":[{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"first_name":"Jean","last_name":"Raskin","full_name":"Raskin, Jean-François"}],"type":"journal_article","title":"Equivalence of labeled Markov chains","extern":1,"date_updated":"2021-01-12T07:59:30Z","issue":"3","month":"06"},{"day":"01","date_created":"2018-12-11T12:09:21Z","status":"public","quality_controlled":0,"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"}],"main_file_link":[{"open_access":"0","url":"http://pub.ist.ac.at/%7Etah/Publications/interface_theories_with_component_reuse.pdf"}],"page":"79 - 88","conference":{"name":"EMSOFT: Embedded Software "},"publist_id":"193","citation":{"short":"L. Doyen, T.A. Henzinger, B. Jobstmann, T. Petrov, in:, ACM, 2008, pp. 79–88.","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>","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>","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>.","ista":"Doyen L, Henzinger TA, Jobstmann B, Petrov T. 2008. Interface theories with component reuse. EMSOFT: Embedded Software , 79–88.","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.","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>."},"year":"2008","date_published":"2008-10-01T00:00:00Z","publication_status":"published","_id":"4533","doi":"10.1145/1450058.1450070","publisher":"ACM","month":"10","date_updated":"2021-01-12T07:59:30Z","extern":1,"title":"Interface theories with component reuse","type":"conference","author":[{"first_name":"Laurent","full_name":"Doyen, Laurent","last_name":"Doyen"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger","last_name":"Henzinger"},{"first_name":"Barbara","full_name":"Jobstmann, Barbara","last_name":"Jobstmann"},{"id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","full_name":"Tatjana Petrov","last_name":"Petrov","orcid":"0000-0002-9041-0905","first_name":"Tatjana"}]},{"extern":1,"title":"Reduction of stochastic parity to stochastic mean-payoff games","type":"journal_article","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Krishnendu Chatterjee"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A"}],"month":"03","issue":"1","date_updated":"2021-01-12T07:59:30Z","publication_status":"published","_id":"4534","doi":"10.1016/j.ipl.2007.08.035","publisher":"Elsevier","citation":{"ieee":"K. Chatterjee and T. A. Henzinger, “Reduction of stochastic parity to stochastic mean-payoff games,” <i>Information Processing Letters</i>, vol. 106, no. 1. Elsevier, pp. 1–7, 2008.","mla":"Chatterjee, Krishnendu, and Thomas A. Henzinger. “Reduction of Stochastic Parity to Stochastic Mean-Payoff Games.” <i>Information Processing Letters</i>, vol. 106, no. 1, Elsevier, 2008, pp. 1–7, doi:<a href=\"https://doi.org/10.1016/j.ipl.2007.08.035\">10.1016/j.ipl.2007.08.035</a>.","ista":"Chatterjee K, Henzinger TA. 2008. Reduction of stochastic parity to stochastic mean-payoff games. Information Processing Letters. 106(1), 1–7.","ama":"Chatterjee K, Henzinger TA. Reduction of stochastic parity to stochastic mean-payoff games. <i>Information Processing Letters</i>. 2008;106(1):1-7. doi:<a href=\"https://doi.org/10.1016/j.ipl.2007.08.035\">10.1016/j.ipl.2007.08.035</a>","chicago":"Chatterjee, Krishnendu, and Thomas A Henzinger. “Reduction of Stochastic Parity to Stochastic Mean-Payoff Games.” <i>Information Processing Letters</i>. Elsevier, 2008. <a href=\"https://doi.org/10.1016/j.ipl.2007.08.035\">https://doi.org/10.1016/j.ipl.2007.08.035</a>.","short":"K. Chatterjee, T.A. Henzinger, Information Processing Letters 106 (2008) 1–7.","apa":"Chatterjee, K., &#38; Henzinger, T. A. (2008). Reduction of stochastic parity to stochastic mean-payoff games. <i>Information Processing Letters</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ipl.2007.08.035\">https://doi.org/10.1016/j.ipl.2007.08.035</a>"},"date_published":"2008-03-31T00:00:00Z","year":"2008","intvolume":"       106","page":"1 - 7","publist_id":"188","abstract":[{"lang":"eng","text":"A stochastic graph game is played by two players on a game graph with probabilistic transitions. We consider stochastic graph games with ω-regular winning conditions specified as parity objectives, and mean-payoff (or limit-average) objectives. These games lie in NP ∩ coNP. We present a polynomial-time Turing reduction of stochastic parity games to stochastic mean-payoff games."}],"main_file_link":[{"url":"http://pub.ist.ac.at/%7Etah/Publications/reduction_of_stochastic_parity_to_stochastic_mean-payoff_games.pdf","open_access":"0"}],"quality_controlled":0,"publication":"Information Processing Letters","volume":106,"day":"31","status":"public","date_created":"2018-12-11T12:09:21Z"},{"main_file_link":[{"open_access":"0","url":"http://pub.ist.ac.at/%7Etah/Publications/logical_reliability_of_interacting_real-time_tasks.pdf"}],"abstract":[{"lang":"eng","text":"We propose the notion of logical reliability for real-time program tasks that interact through periodically updated program variables. We describe a reliability analysis that checks if the given short-term (e.g., single-period) reliability of a program variable update in an implementation is sufficient to meet the logical reliability requirement (of the program variable) in the long run. We then present a notion of design by refinement where a task can be refined by another task that writes to program variables with less logical reliability. The resulting analysis can be combined with an incremental schedulability analysis for interacting real-time tasks proposed earlier for the Hierarchical Timing Language (HTL), a coordination language for distributed real-time systems. We implemented a logical-reliability-enhanced prototype of the compiler and runtime infrastructure for HTL."}],"page":"909 - 914","conference":{"name":"DATE: Design, Automation and Test in Europe"},"publist_id":"171","day":"01","status":"public","date_created":"2018-12-11T12:09:25Z","quality_controlled":0,"month":"01","date_updated":"2021-01-12T07:59:36Z","extern":1,"title":"Logical reliability of interacting real-time tasks","type":"conference","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Krishnendu Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Ghosal","full_name":"Ghosal, Arkadeb","first_name":"Arkadeb"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger","last_name":"Henzinger"},{"last_name":"Iercan","full_name":"Iercan, Daniel","first_name":"Daniel"},{"first_name":"Christoph","full_name":"Kirsch, Christoph M","last_name":"Kirsch"},{"first_name":"Claudio","last_name":"Pinello","full_name":"Pinello, Claudio"},{"first_name":"Alberto","full_name":"Sangiovanni-Vincentelli, Alberto","last_name":"Sangiovanni Vincentelli"}],"citation":{"apa":"Chatterjee, K., Ghosal, A., Henzinger, T. A., Iercan, D., Kirsch, C., Pinello, C., &#38; Sangiovanni Vincentelli, A. (2008). Logical reliability of interacting real-time tasks (pp. 909–914). Presented at the DATE: Design, Automation and Test in Europe, IEEE. <a href=\"https://doi.org/10.1145/1403375.1403595\">https://doi.org/10.1145/1403375.1403595</a>","short":"K. Chatterjee, A. Ghosal, T.A. Henzinger, D. Iercan, C. Kirsch, C. Pinello, A. Sangiovanni Vincentelli, in:, IEEE, 2008, pp. 909–914.","chicago":"Chatterjee, Krishnendu, Arkadeb Ghosal, Thomas A Henzinger, Daniel Iercan, Christoph Kirsch, Claudio Pinello, and Alberto Sangiovanni Vincentelli. “Logical Reliability of Interacting Real-Time Tasks,” 909–14. IEEE, 2008. <a href=\"https://doi.org/10.1145/1403375.1403595\">https://doi.org/10.1145/1403375.1403595</a>.","ama":"Chatterjee K, Ghosal A, Henzinger TA, et al. Logical reliability of interacting real-time tasks. In: IEEE; 2008:909-914. doi:<a href=\"https://doi.org/10.1145/1403375.1403595\">10.1145/1403375.1403595</a>","ista":"Chatterjee K, Ghosal A, Henzinger TA, Iercan D, Kirsch C, Pinello C, Sangiovanni Vincentelli A. 2008. Logical reliability of interacting real-time tasks. DATE: Design, Automation and Test in Europe, 909–914.","mla":"Chatterjee, Krishnendu, et al. <i>Logical Reliability of Interacting Real-Time Tasks</i>. IEEE, 2008, pp. 909–14, doi:<a href=\"https://doi.org/10.1145/1403375.1403595\">10.1145/1403375.1403595</a>.","ieee":"K. Chatterjee <i>et al.</i>, “Logical reliability of interacting real-time tasks,” presented at the DATE: Design, Automation and Test in Europe, 2008, pp. 909–914."},"date_published":"2008-01-01T00:00:00Z","year":"2008","publication_status":"published","_id":"4546","doi":"10.1145/1403375.1403595","publisher":"IEEE"},{"date_updated":"2021-01-12T07:59:37Z","month":"01","issue":"2","title":"Stochastic limit-average games are in EXPTIME","extern":1,"author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Krishnendu Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Majumdar","full_name":"Majumdar, Ritankar S","first_name":"Ritankar"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"type":"journal_article","date_published":"2008-01-01T00:00:00Z","year":"2008","citation":{"short":"K. Chatterjee, R. Majumdar, T.A. Henzinger, International Journal of Game Theory 37 (2008) 219–234.","apa":"Chatterjee, K., Majumdar, R., &#38; Henzinger, T. A. (2008). Stochastic limit-average games are in EXPTIME. <i>International Journal of Game Theory</i>. Springer. <a href=\"https://doi.org/10.1007/s00182-007-0110-5\">https://doi.org/10.1007/s00182-007-0110-5</a>","ama":"Chatterjee K, Majumdar R, Henzinger TA. Stochastic limit-average games are in EXPTIME. <i>International Journal of Game Theory</i>. 2008;37(2):219-234. doi:<a href=\"https://doi.org/10.1007/s00182-007-0110-5\">10.1007/s00182-007-0110-5</a>","chicago":"Chatterjee, Krishnendu, Ritankar Majumdar, and Thomas A Henzinger. “Stochastic Limit-Average Games Are in EXPTIME.” <i>International Journal of Game Theory</i>. Springer, 2008. <a href=\"https://doi.org/10.1007/s00182-007-0110-5\">https://doi.org/10.1007/s00182-007-0110-5</a>.","ista":"Chatterjee K, Majumdar R, Henzinger TA. 2008. Stochastic limit-average games are in EXPTIME. International Journal of Game Theory. 37(2), 219–234.","ieee":"K. Chatterjee, R. Majumdar, and T. A. Henzinger, “Stochastic limit-average games are in EXPTIME,” <i>International Journal of Game Theory</i>, vol. 37, no. 2. Springer, pp. 219–234, 2008.","mla":"Chatterjee, Krishnendu, et al. “Stochastic Limit-Average Games Are in EXPTIME.” <i>International Journal of Game Theory</i>, vol. 37, no. 2, Springer, 2008, pp. 219–34, doi:<a href=\"https://doi.org/10.1007/s00182-007-0110-5\">10.1007/s00182-007-0110-5</a>."},"_id":"4548","publication_status":"published","publisher":"Springer","doi":"10.1007/s00182-007-0110-5","main_file_link":[{"open_access":"0","url":"http://pub.ist.ac.at/%7Etah/Publications/stochastic_limit-average_games_are_in_exptime.pdf"}],"abstract":[{"text":"The value of a finite-state two-player zero-sum stochastic game with limit-average payoff can be approximated to within ε in time exponential in a polynomial in the size of the game times polynomial in logarithmic in 1/ε, for all ε &gt; 0.","lang":"eng"}],"page":"219 - 234","intvolume":"        37","publist_id":"168","volume":37,"day":"01","date_created":"2018-12-11T12:09:25Z","status":"public","quality_controlled":0,"publication":"International Journal of Game Theory"},{"page":"29 - 38","conference":{"name":"ASE: Automated Software Engineering"},"publist_id":"140","abstract":[{"lang":"eng","text":"We present and evaluate a framework and tool for combining multiple program analyses which allows the dynamic (on-line) adjustment of the precision of each analysis depending on the accumulated results. For example, the explicit tracking of the values of a variable may be switched off in favor of a predicate abstraction when and where the number of different variable values that have been encountered has exceeded a specified threshold. The method is evaluated on verifying the SSH client/server software and shows significant gains compared with predicate abstraction-based model checking."}],"main_file_link":[{"url":"http://pub.ist.ac.at/%7Etah/Publications/program_analysis_with_dynamic_change_of_precision.pdf","open_access":"0"}],"quality_controlled":0,"day":"07","status":"public","date_created":"2018-12-11T12:09:31Z","title":"Program analysis with dynamic change of precision","extern":1,"author":[{"full_name":"Beyer, Dirk","last_name":"Beyer","first_name":"Dirk"},{"last_name":"Henzinger","full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"first_name":"Grégory","last_name":"Théoduloz","full_name":"Théoduloz, Grégory"}],"type":"conference","date_updated":"2021-01-12T07:59:46Z","month":"10","_id":"4568","publication_status":"published","publisher":"ACM","doi":"10.1109/ASE.2008.13","year":"2008","date_published":"2008-10-07T00:00:00Z","citation":{"ieee":"D. Beyer, T. A. Henzinger, and G. Théoduloz, “Program analysis with dynamic change of precision,” presented at the ASE: Automated Software Engineering, 2008, pp. 29–38.","mla":"Beyer, Dirk, et al. <i>Program Analysis with Dynamic Change of Precision</i>. ACM, 2008, pp. 29–38, doi:<a href=\"https://doi.org/10.1109/ASE.2008.13\">10.1109/ASE.2008.13</a>.","ista":"Beyer D, Henzinger TA, Théoduloz G. 2008. Program analysis with dynamic change of precision. ASE: Automated Software Engineering, 29–38.","ama":"Beyer D, Henzinger TA, Théoduloz G. Program analysis with dynamic change of precision. In: ACM; 2008:29-38. doi:<a href=\"https://doi.org/10.1109/ASE.2008.13\">10.1109/ASE.2008.13</a>","chicago":"Beyer, Dirk, Thomas A Henzinger, and Grégory Théoduloz. “Program Analysis with Dynamic Change of Precision,” 29–38. ACM, 2008. <a href=\"https://doi.org/10.1109/ASE.2008.13\">https://doi.org/10.1109/ASE.2008.13</a>.","short":"D. Beyer, T.A. Henzinger, G. Théoduloz, in:, ACM, 2008, pp. 29–38.","apa":"Beyer, D., Henzinger, T. A., &#38; Théoduloz, G. (2008). Program analysis with dynamic change of precision (pp. 29–38). Presented at the ASE: Automated Software Engineering, ACM. <a href=\"https://doi.org/10.1109/ASE.2008.13\">https://doi.org/10.1109/ASE.2008.13</a>"}},{"citation":{"ama":"Sahli M, Roques-Carmes C, Khan Malek C, Gelin JC. Modelling of the filling of micro-cavities of finite geometry by amorphous polymers using hot-embossing. <i>Microsystem Technologies</i>. 2008;14:1545-1551. doi:<a href=\"https://doi.org/10.1007/s00542-008-0565-8\">10.1007/s00542-008-0565-8</a>","chicago":"Sahli, M., Charles Roques-Carmes, C. Khan Malek, and J. C. Gelin. “Modelling of the Filling of Micro-Cavities of Finite Geometry by Amorphous Polymers Using Hot-Embossing.” <i>Microsystem Technologies</i>. Springer Nature, 2008. <a href=\"https://doi.org/10.1007/s00542-008-0565-8\">https://doi.org/10.1007/s00542-008-0565-8</a>.","short":"M. Sahli, C. Roques-Carmes, C. Khan Malek, J.C. Gelin, Microsystem Technologies 14 (2008) 1545–1551.","apa":"Sahli, M., Roques-Carmes, C., Khan Malek, C., &#38; Gelin, J. C. (2008). Modelling of the filling of micro-cavities of finite geometry by amorphous polymers using hot-embossing. <i>Microsystem Technologies</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00542-008-0565-8\">https://doi.org/10.1007/s00542-008-0565-8</a>","ieee":"M. Sahli, C. Roques-Carmes, C. Khan Malek, and J. C. Gelin, “Modelling of the filling of micro-cavities of finite geometry by amorphous polymers using hot-embossing,” <i>Microsystem Technologies</i>, vol. 14. Springer Nature, pp. 1545–1551, 2008.","mla":"Sahli, M., et al. “Modelling of the Filling of Micro-Cavities of Finite Geometry by Amorphous Polymers Using Hot-Embossing.” <i>Microsystem Technologies</i>, vol. 14, Springer Nature, 2008, pp. 1545–51, doi:<a href=\"https://doi.org/10.1007/s00542-008-0565-8\">10.1007/s00542-008-0565-8</a>.","ista":"Sahli M, Roques-Carmes C, Khan Malek C, Gelin JC. 2008. Modelling of the filling of micro-cavities of finite geometry by amorphous polymers using hot-embossing. Microsystem Technologies. 14, 1545–1551."},"date_published":"2008-10-01T00:00:00Z","year":"2008","publication_status":"published","doi":"10.1007/s00542-008-0565-8","publisher":"Springer Nature","article_processing_charge":"No","publication_identifier":{"issn":["0946-7076"],"eissn":["1432-1858"]},"month":"10","date_updated":"2026-04-15T12:53:52Z","title":"Modelling of the filling of micro-cavities of finite geometry by amorphous polymers using hot-embossing","volume":14,"day":"01","oa_version":"None","quality_controlled":"1","abstract":[{"text":"The possibility to fill cavities of finite geometry could be described using an analytical model of the hot-embossing process of viscoelastic polymers. This model is based on the volume conservation during the forming process which allows to predict data concerning the geometrical evolution of the material on one hand, and on the other hand the filling time of cavities in the mould. A particular attention was drawn on the necessary time to fill the cavities depending on their shape or a scale factor for a given cavity shape.","lang":"eng"}],"article_type":"original","OA_type":"closed access","_id":"21512","extern":"1","type":"journal_article","author":[{"full_name":"Sahli, M.","last_name":"Sahli","first_name":"M."},{"full_name":"Roques-Carmes, Charles","id":"e2e68fc9-6505-11ef-a541-eb4e72cc3e82","last_name":"Roques-Carmes","first_name":"Charles"},{"first_name":"C.","full_name":"Khan Malek, C.","last_name":"Khan Malek"},{"first_name":"J. C.","last_name":"Gelin","full_name":"Gelin, J. C."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","date_created":"2026-03-30T12:22:47Z","status":"public","language":[{"iso":"eng"}],"publication":"Microsystem Technologies","ddc":["530"],"page":"1545-1551","intvolume":"        14"},{"_id":"11884","extern":"1","author":[{"first_name":"Monika H","orcid":"0000-0002-5008-6530","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"journal_article","issue":"5837","publication":"Science","language":[{"iso":"eng"}],"status":"public","scopus_import":"1","date_created":"2022-08-17T07:30:07Z","pmid":1,"intvolume":"       317","page":"468-471","publication_status":"published","publisher":"American Association for the Advancement of Science","article_processing_charge":"No","publication_identifier":{"issn":["0036-8075"],"eissn":["1095-9203"]},"doi":"10.1126/science.1126557","date_published":"2007-07-27T00:00:00Z","year":"2007","citation":{"ista":"Henzinger M. 2007. Search technologies for the internet. Science. 317(5837), 468–471.","ieee":"M. Henzinger, “Search technologies for the internet,” <i>Science</i>, vol. 317, no. 5837. American Association for the Advancement of Science, pp. 468–471, 2007.","mla":"Henzinger, Monika. “Search Technologies for the Internet.” <i>Science</i>, vol. 317, no. 5837, American Association for the Advancement of Science, 2007, pp. 468–71, doi:<a href=\"https://doi.org/10.1126/science.1126557\">10.1126/science.1126557</a>.","short":"M. Henzinger, Science 317 (2007) 468–471.","apa":"Henzinger, M. (2007). Search technologies for the internet. <i>Science</i>. American Association for the Advancement of Science. <a href=\"https://doi.org/10.1126/science.1126557\">https://doi.org/10.1126/science.1126557</a>","ama":"Henzinger M. Search technologies for the internet. <i>Science</i>. 2007;317(5837):468-471. doi:<a href=\"https://doi.org/10.1126/science.1126557\">10.1126/science.1126557</a>","chicago":"Henzinger, Monika. “Search Technologies for the Internet.” <i>Science</i>. American Association for the Advancement of Science, 2007. <a href=\"https://doi.org/10.1126/science.1126557\">https://doi.org/10.1126/science.1126557</a>."},"title":"Search technologies for the internet","date_updated":"2024-11-06T12:01:07Z","month":"07","quality_controlled":"1","external_id":{"pmid":["17656714"]},"oa_version":"None","day":"27","volume":317,"abstract":[{"lang":"eng","text":"About 20% of the world's population uses the Web, and a large majority thereof uses Web search engines to find information. As a result, many Web researchers are devoting much effort to improving the speed and capability of search technology."}],"article_type":"review"},{"abstract":[{"text":"How much can smart combinatorial algorithms improve web search engines? To address this question we will describe three algorithms that have had a positive impact on web search engines: The PageRank algorithm, algorithms for finding near-duplicate web pages, and algorithms for index server loadbalancing.","lang":"eng"}],"page":"1022-1026","conference":{"end_date":"2007-01-09","name":"SODA: Symposium on Discrete Algorithms","location":"New Orleans, LA, United States","start_date":"2007-01-07"},"oa_version":"None","day":"01","date_created":"2022-08-18T12:37:03Z","status":"public","scopus_import":"1","quality_controlled":"1","language":[{"iso":"eng"}],"publication":"18th Annual ACM-SIAM Symposium on Discrete Algorithms","month":"01","date_updated":"2024-11-06T11:59:56Z","extern":"1","title":"Combinatorial algorithms for web search engines: three success stories","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","first_name":"Monika H"}],"citation":{"ista":"Henzinger M. 2007. Combinatorial algorithms for web search engines: three success stories. 18th Annual ACM-SIAM Symposium on Discrete Algorithms. SODA: Symposium on Discrete Algorithms, 1022–1026.","mla":"Henzinger, Monika. “Combinatorial Algorithms for Web Search Engines: Three Success Stories.” <i>18th Annual ACM-SIAM Symposium on Discrete Algorithms</i>, Society for Industrial &#38; Applied Mathematics, 2007, pp. 1022–26.","ieee":"M. Henzinger, “Combinatorial algorithms for web search engines: three success stories,” in <i>18th Annual ACM-SIAM Symposium on Discrete Algorithms</i>, New Orleans, LA, United States, 2007, pp. 1022–1026.","apa":"Henzinger, M. (2007). Combinatorial algorithms for web search engines: three success stories. In <i>18th Annual ACM-SIAM Symposium on Discrete Algorithms</i> (pp. 1022–1026). New Orleans, LA, United States: Society for Industrial &#38; Applied Mathematics.","short":"M. Henzinger, in:, 18th Annual ACM-SIAM Symposium on Discrete Algorithms, Society for Industrial &#38; Applied Mathematics, 2007, pp. 1022–1026.","chicago":"Henzinger, Monika. “Combinatorial Algorithms for Web Search Engines: Three Success Stories.” In <i>18th Annual ACM-SIAM Symposium on Discrete Algorithms</i>, 1022–26. Society for Industrial &#38; Applied Mathematics, 2007.","ama":"Henzinger M. Combinatorial algorithms for web search engines: three success stories. In: <i>18th Annual ACM-SIAM Symposium on Discrete Algorithms</i>. Society for Industrial &#38; Applied Mathematics; 2007:1022-1026."},"year":"2007","date_published":"2007-01-01T00:00:00Z","publication_status":"published","_id":"11924","article_processing_charge":"No","publication_identifier":{"isbn":["9780898716245"]},"publisher":"Society for Industrial & Applied Mathematics"},{"article_type":"original","abstract":[{"text":"The development of plant lateral organs is interesting because, although many of the same genes seem to be involved in the early growth of primordia, completely different gene combinations are required for the complete development of organs such as leaves and stamens. Thus, the genes common to the development of most organs, which generally form and polarize the primordial ‘envelope’, must at some stage interact with those that ‘install’ the functional content of the organ – in the case of the stamen, the four microsporangia. Although distinct genetic pathways of organ initiation, polarity establishment and setting up the reproductive cell line can readily be recognized, they do not occur sequentially. Rather, they are activated early and run in parallel. There is evidence for continuing crosstalk between these pathways.","lang":"eng"}],"oa_version":"None","volume":23,"external_id":{"pmid":["17825943"]},"quality_controlled":"1","date_updated":"2023-05-08T10:58:47Z","department":[{"_id":"XiFe"}],"month":"10","title":"Packaging the male germline in plants","date_published":"2007-10-01T00:00:00Z","year":"2007","citation":{"ieee":"X. Feng and H. G. Dickinson, “Packaging the male germline in plants,” <i>Trends in Genetics</i>, vol. 23, no. 10. Elsevier BV, pp. 503–510, 2007.","mla":"Feng, Xiaoqi, and Hugh G. Dickinson. “Packaging the Male Germline in Plants.” <i>Trends in Genetics</i>, vol. 23, no. 10, Elsevier BV, 2007, pp. 503–10, doi:<a href=\"https://doi.org/10.1016/j.tig.2007.08.005\">10.1016/j.tig.2007.08.005</a>.","ista":"Feng X, Dickinson HG. 2007. Packaging the male germline in plants. Trends in Genetics. 23(10), 503–510.","ama":"Feng X, Dickinson HG. Packaging the male germline in plants. <i>Trends in Genetics</i>. 2007;23(10):503-510. doi:<a href=\"https://doi.org/10.1016/j.tig.2007.08.005\">10.1016/j.tig.2007.08.005</a>","chicago":"Feng, Xiaoqi, and Hugh G. Dickinson. “Packaging the Male Germline in Plants.” <i>Trends in Genetics</i>. Elsevier BV, 2007. <a href=\"https://doi.org/10.1016/j.tig.2007.08.005\">https://doi.org/10.1016/j.tig.2007.08.005</a>.","short":"X. Feng, H.G. Dickinson, Trends in Genetics 23 (2007) 503–510.","apa":"Feng, X., &#38; Dickinson, H. G. (2007). Packaging the male germline in plants. <i>Trends in Genetics</i>. Elsevier BV. <a href=\"https://doi.org/10.1016/j.tig.2007.08.005\">https://doi.org/10.1016/j.tig.2007.08.005</a>"},"publication_identifier":{"issn":["0168-9525"]},"article_processing_charge":"No","publisher":"Elsevier BV","doi":"10.1016/j.tig.2007.08.005","publication_status":"published","intvolume":"        23","pmid":1,"page":"503-510","keyword":["Genetics"],"status":"public","date_created":"2023-01-16T09:22:44Z","scopus_import":"1","publication":"Trends in Genetics","language":[{"iso":"eng"}],"issue":"10","acknowledgement":"X.F. holds a Clarendon Scholarship from the University of Oxford. We thank Angela Hay and Jill Harrison for helpful advice and discussion.","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Feng, Xiaoqi","id":"e0164712-22ee-11ed-b12a-d80fcdf35958","last_name":"Feng","orcid":"0000-0002-4008-1234","first_name":"Xiaoqi"},{"first_name":"Hugh G.","full_name":"Dickinson, Hugh G.","last_name":"Dickinson"}],"type":"journal_article","extern":"1","_id":"12201"},{"date_updated":"2021-01-12T06:58:55Z","month":"01","issue":"2","author":[{"full_name":"Tóth, Kinga","last_name":"Tóth","first_name":"Kinga"},{"first_name":"Lucia","last_name":"Wittner","full_name":"Wittner, Lucia"},{"last_name":"Urbán","full_name":"Urbán, Z","first_name":"Z"},{"first_name":"Werner","full_name":"Doyle, Werner K","last_name":"Doyle"},{"first_name":"György","last_name":"Buzsáki","full_name":"Buzsáki, György"},{"last_name":"Shigemoto","full_name":"Ryuichi Shigemoto","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8761-9444","first_name":"Ryuichi"},{"first_name":"Tamás","full_name":"Freund, Tamás F","last_name":"Freund"},{"full_name":"Maglóczky, Zsófia","last_name":"Maglóczky","first_name":"Zsófia"}],"type":"journal_article","title":"Morphology and synaptic input of substance P receptor-immunoreactive interneurons in control and epileptic human hippocampus","extern":1,"year":"2007","date_published":"2007-01-19T00:00:00Z","citation":{"chicago":"Tóth, Kinga, Lucia Wittner, Z Urbán, Werner Doyle, György Buzsáki, Ryuichi Shigemoto, Tamás Freund, and Zsófia Maglóczky. “Morphology and Synaptic Input of Substance P Receptor-Immunoreactive Interneurons in Control and Epileptic Human Hippocampus.” <i>Neuroscience</i>. Elsevier, 2007. <a href=\"https://doi.org/10.1016/j.neuroscience.2006.09.039\">https://doi.org/10.1016/j.neuroscience.2006.09.039</a>.","ama":"Tóth K, Wittner L, Urbán Z, et al. Morphology and synaptic input of substance P receptor-immunoreactive interneurons in control and epileptic human hippocampus. <i>Neuroscience</i>. 2007;144(2):495-508. doi:<a href=\"https://doi.org/10.1016/j.neuroscience.2006.09.039\">10.1016/j.neuroscience.2006.09.039</a>","apa":"Tóth, K., Wittner, L., Urbán, Z., Doyle, W., Buzsáki, G., Shigemoto, R., … Maglóczky, Z. (2007). Morphology and synaptic input of substance P receptor-immunoreactive interneurons in control and epileptic human hippocampus. <i>Neuroscience</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.neuroscience.2006.09.039\">https://doi.org/10.1016/j.neuroscience.2006.09.039</a>","short":"K. Tóth, L. Wittner, Z. Urbán, W. Doyle, G. Buzsáki, R. Shigemoto, T. Freund, Z. Maglóczky, Neuroscience 144 (2007) 495–508.","mla":"Tóth, Kinga, et al. “Morphology and Synaptic Input of Substance P Receptor-Immunoreactive Interneurons in Control and Epileptic Human Hippocampus.” <i>Neuroscience</i>, vol. 144, no. 2, Elsevier, 2007, pp. 495–508, doi:<a href=\"https://doi.org/10.1016/j.neuroscience.2006.09.039\">10.1016/j.neuroscience.2006.09.039</a>.","ieee":"K. Tóth <i>et al.</i>, “Morphology and synaptic input of substance P receptor-immunoreactive interneurons in control and epileptic human hippocampus,” <i>Neuroscience</i>, vol. 144, no. 2. Elsevier, pp. 495–508, 2007.","ista":"Tóth K, Wittner L, Urbán Z, Doyle W, Buzsáki G, Shigemoto R, Freund T, Maglóczky Z. 2007. Morphology and synaptic input of substance P receptor-immunoreactive interneurons in control and epileptic human hippocampus. Neuroscience. 144(2), 495–508."},"publisher":"Elsevier","doi":"10.1016/j.neuroscience.2006.09.039","_id":"2665","publication_status":"published","abstract":[{"text":"Substance P (SP) is known to be a peptide that facilitates epileptic activity of principal cells in the hippocampus. Paradoxically, in other models, it was found to be protective against seizures by activating substance P receptor (SPR)-expressing interneurons. Thus, these cells appear to play an important role in the generation and regulation of epileptic seizures. The number, distribution, morphological features and input characteristics of SPR-immunoreactive cells were analyzed in surgically removed hippocampi of 28 temporal lobe epileptic patients and eight control hippocampi in order to examine their changes in epileptic tissues. SPR is expressed in a subset of inhibitory cells in the control human hippocampus, they are multipolar interneurons with smooth dendrites, present in all hippocampal subfields. This cell population is considerably different from SPR-positive cells of the rat hippocampus. The CA1 (cornu Ammonis subfield 1) region was chosen for the detailed morphological analysis of the SPR-immunoreactive cells because of its extreme vulnerability in epilepsy. The presence of various neurochemical markers identifies functionally distinct interneuron types, such as those responsible for perisomatic, dendritic or interneuron-selective inhibition. We found considerable colocalization of SPR with calbindin but not with parvalbumin, calretinin, cholecystokinin and somatostatin, therefore we suppose that SPR-positive cells participate mainly in dendritic inhibition. In the non-sclerotic CA1 region they are mainly preserved, whereas their number is decreased in the sclerotic cases. In the epileptic samples their morphology is considerably altered, they possessed more dendritic branches, which often became beaded. Analyses of synaptic coverage revealed that the ratio of symmetric synaptic input of SPR-immunoreactive cells has increased in epileptic samples. Our results suggest that SPR-positive cells are preserved while principal cells are present in the CA1 region, but show reactive changes in epilepsy including intense branching and growth of their dendritic arborization.","lang":"eng"}],"publist_id":"4232","page":"495 - 508","intvolume":"       144","date_created":"2018-12-11T11:58:57Z","status":"public","day":"19","volume":144,"publication":"Neuroscience","quality_controlled":0},{"abstract":[{"lang":"eng","text":"GABAB receptors (GABABRs) are involved in early events during neuronal development. The presence of GABABRs in developing oligodendrocytes has not been established. Using immunofluorescent co-localization, we have identified GABABR proteins in O4 marker-positive oligodendrocyte precursor cells (OPCs) in 4-day-old mouse brain periventricular white matter. In culture, OPCs, differentiated oligodendrocytes (DOs) and type 2 astrocytes (ASTs) express both the GABAB1abcdf and GABAB2 subunits of the GABABR. Using semiquantitative PCR analysis with GABABR isoform-selective primers we found that the expression level of GABAB1abd was substantially higher in OPCs or ASTs than in DOs. In contrast, the GABAB2 isoform showed a similar level of expression in OPCs and DOs, and a significantly higher level in ASTs. This indicates that the expression of GABAB1 and GABAB2 subunits are under independent control during oligodendroglial development. Activation of GABABRs using the selective agonist baclofen demonstrated that these receptors are functionally active and negatively coupled to adenylyl cyclase. Manipulation of GABABR activity had no effect on OPC migration in a conventional agarose drop assay, whereas baclofen significantly increased OPC migration in a more sensitive transwell microchamber-based assay. Exposure of cultured OPCs to baclofen increased their proliferation, providing evidence for a functional role of GABABRs in oligodendrocyte development. The presence of GABABRs in developing oligodendrocytes provides a new mechanism for neuronal-glial interactions during development and may offer a novel target for promoting remyelination following white matter injury."}],"publist_id":"4231","intvolume":"       100","page":"822 - 840","status":"public","date_created":"2018-12-11T11:58:57Z","volume":100,"day":"01","publication":"Journal of Neurochemistry","quality_controlled":0,"issue":"3","month":"02","date_updated":"2021-01-12T06:58:55Z","type":"journal_article","author":[{"full_name":"Luyt, Karen","last_name":"Luyt","first_name":"Karen"},{"full_name":"Slade, Timothy P","last_name":"Slade","first_name":"Timothy"},{"last_name":"Dorward","full_name":"Dorward, Jienchi J","first_name":"Jienchi"},{"first_name":"Claire","full_name":"Durant, Claire F","last_name":"Durant"},{"first_name":"Yue","last_name":"Wu","full_name":"Wu, Yue"},{"orcid":"0000-0001-8761-9444","first_name":"Ryuichi","last_name":"Shigemoto","full_name":"Ryuichi Shigemoto","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Mundell","full_name":"Mundell, Stuart J","first_name":"Stuart"},{"last_name":"Váradi","full_name":"Váradi, Anikó","first_name":"Anikó"},{"full_name":"Molnár, Elek","last_name":"Molnár","first_name":"Elek"}],"extern":1,"title":"Developing oligodendrocytes express functional GABAB receptors that stimulate cell proliferation and migration","citation":{"apa":"Luyt, K., Slade, T., Dorward, J., Durant, C., Wu, Y., Shigemoto, R., … Molnár, E. (2007). Developing oligodendrocytes express functional GABAB receptors that stimulate cell proliferation and migration. <i>Journal of Neurochemistry</i>. Wiley-Blackwell. <a href=\"https://doi.org/10.1111/j.1471-4159.2006.04255.x\">https://doi.org/10.1111/j.1471-4159.2006.04255.x</a>","short":"K. Luyt, T. Slade, J. Dorward, C. Durant, Y. Wu, R. Shigemoto, S. Mundell, A. Váradi, E. Molnár, Journal of Neurochemistry 100 (2007) 822–840.","chicago":"Luyt, Karen, Timothy Slade, Jienchi Dorward, Claire Durant, Yue Wu, Ryuichi Shigemoto, Stuart Mundell, Anikó Váradi, and Elek Molnár. “Developing Oligodendrocytes Express Functional GABAB Receptors That Stimulate Cell Proliferation and Migration.” <i>Journal of Neurochemistry</i>. Wiley-Blackwell, 2007. <a href=\"https://doi.org/10.1111/j.1471-4159.2006.04255.x\">https://doi.org/10.1111/j.1471-4159.2006.04255.x</a>.","ama":"Luyt K, Slade T, Dorward J, et al. Developing oligodendrocytes express functional GABAB receptors that stimulate cell proliferation and migration. <i>Journal of Neurochemistry</i>. 2007;100(3):822-840. doi:<a href=\"https://doi.org/10.1111/j.1471-4159.2006.04255.x\">10.1111/j.1471-4159.2006.04255.x</a>","ista":"Luyt K, Slade T, Dorward J, Durant C, Wu Y, Shigemoto R, Mundell S, Váradi A, Molnár E. 2007. Developing oligodendrocytes express functional GABAB receptors that stimulate cell proliferation and migration. Journal of Neurochemistry. 100(3), 822–840.","mla":"Luyt, Karen, et al. “Developing Oligodendrocytes Express Functional GABAB Receptors That Stimulate Cell Proliferation and Migration.” <i>Journal of Neurochemistry</i>, vol. 100, no. 3, Wiley-Blackwell, 2007, pp. 822–40, doi:<a href=\"https://doi.org/10.1111/j.1471-4159.2006.04255.x\">10.1111/j.1471-4159.2006.04255.x</a>.","ieee":"K. Luyt <i>et al.</i>, “Developing oligodendrocytes express functional GABAB receptors that stimulate cell proliferation and migration,” <i>Journal of Neurochemistry</i>, vol. 100, no. 3. Wiley-Blackwell, pp. 822–840, 2007."},"date_published":"2007-02-01T00:00:00Z","year":"2007","doi":"10.1111/j.1471-4159.2006.04255.x","publisher":"Wiley-Blackwell","publication_status":"published","_id":"2666"}]