[{"date_published":"2007-01-01T00:00:00Z","day":"01","publisher":"Springer","publist_id":"1055","date_created":"2018-12-11T12:08:40Z","publication_status":"published","doi":"1544","extern":1,"citation":{"chicago":"Alur, Rajeev, Pavol Cerny, and Swarat Chaudhuri. “Model Checking on Trees with Path Equivalences,” 664–78. Springer, 2007. <a href=\"https://doi.org/1544\">https://doi.org/1544</a>.","apa":"Alur, R., Cerny, P., &#38; Chaudhuri, S. (2007). Model Checking on Trees with Path Equivalences (pp. 664–678). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Springer. <a href=\"https://doi.org/1544\">https://doi.org/1544</a>","ama":"Alur R, Cerny P, Chaudhuri S. Model Checking on Trees with Path Equivalences. In: Springer; 2007:664-678. doi:<a href=\"https://doi.org/1544\">1544</a>","short":"R. Alur, P. Cerny, S. Chaudhuri, in:, Springer, 2007, pp. 664–678.","mla":"Alur, Rajeev, et al. <i>Model Checking on Trees with Path Equivalences</i>. Springer, 2007, pp. 664–78, doi:<a href=\"https://doi.org/1544\">1544</a>.","ista":"Alur R, Cerny P, Chaudhuri S. 2007. Model Checking on Trees with Path Equivalences. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, , 664–678.","ieee":"R. Alur, P. Cerny, and S. Chaudhuri, “Model Checking on Trees with Path Equivalences,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, 2007, pp. 664–678."},"alternative_title":["LNCS"],"author":[{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"},{"last_name":"Cerny","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","first_name":"Pavol","full_name":"Pavol Cerny"},{"last_name":"Chaudhuri","first_name":"Swarat","full_name":"Chaudhuri,Swarat"}],"status":"public","quality_controlled":0,"page":"664 - 678","month":"01","year":"2007","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"_id":"4402","type":"conference","date_updated":"2021-01-12T07:56:43Z","title":"Model Checking on Trees with Path Equivalences"},{"title":"Qualitative networks: A symbolic approach to analyze biological signaling networks","main_file_link":[{"url":"http://www.biomedcentral.com/1752-0509/1/4","open_access":"0"}],"_id":"4405","type":"journal_article","date_updated":"2021-01-12T07:56:44Z","month":"01","year":"2007","intvolume":"         1","issue":"4","extern":1,"citation":{"ama":"Schaub M, Henzinger TA, Fisher J. Qualitative networks: A symbolic approach to analyze biological signaling networks. <i>BMC Systems Biology</i>. 2007;1(4). doi:<a href=\"https://doi.org/10.1186/1752-0509-1-4\">10.1186/1752-0509-1-4</a>","chicago":"Schaub, Marc, Thomas A Henzinger, and Jasmin Fisher. “Qualitative Networks: A Symbolic Approach to Analyze Biological Signaling Networks.” <i>BMC Systems Biology</i>. BioMed Central, 2007. <a href=\"https://doi.org/10.1186/1752-0509-1-4\">https://doi.org/10.1186/1752-0509-1-4</a>.","apa":"Schaub, M., Henzinger, T. A., &#38; Fisher, J. (2007). Qualitative networks: A symbolic approach to analyze biological signaling networks. <i>BMC Systems Biology</i>. BioMed Central. <a href=\"https://doi.org/10.1186/1752-0509-1-4\">https://doi.org/10.1186/1752-0509-1-4</a>","ista":"Schaub M, Henzinger TA, Fisher J. 2007. Qualitative networks: A symbolic approach to analyze biological signaling networks. BMC Systems Biology. 1(4).","ieee":"M. Schaub, T. A. Henzinger, and J. Fisher, “Qualitative networks: A symbolic approach to analyze biological signaling networks,” <i>BMC Systems Biology</i>, vol. 1, no. 4. BioMed Central, 2007.","mla":"Schaub, Marc, et al. “Qualitative Networks: A Symbolic Approach to Analyze Biological Signaling Networks.” <i>BMC Systems Biology</i>, vol. 1, no. 4, BioMed Central, 2007, doi:<a href=\"https://doi.org/10.1186/1752-0509-1-4\">10.1186/1752-0509-1-4</a>.","short":"M. Schaub, T.A. Henzinger, J. Fisher, BMC Systems Biology 1 (2007)."},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"author":[{"first_name":"Marc","full_name":"Schaub, Marc A","last_name":"Schaub"},{"first_name":"Thomas A","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"last_name":"Fisher","full_name":"Fisher, Jasmin","first_name":"Jasmin"}],"status":"public","quality_controlled":0,"volume":1,"date_created":"2018-12-11T12:08:41Z","publication_status":"published","doi":"10.1186/1752-0509-1-4","publist_id":"325","abstract":[{"text":"Background\nA central goal of Systems Biology is to model and analyze biological signaling pathways that interact with one another to form complex networks. Here we introduce Qualitative networks, an extension of Boolean networks. With this framework, we use formal verification methods to check whether a model is consistent with the laboratory experimental observations on which it is based. If the model does not conform to the data, we suggest a revised model and the new hypotheses are tested in-silico.\n\nResults\nWe consider networks in which elements range over a small finite domain allowing more flexibility than Boolean values, and add target functions that allow to model a rich set of behaviors. We propose a symbolic algorithm for analyzing the steady state of these networks, allowing us to scale up to a system consisting of 144 elements and state spaces of approximately 1086 states. We illustrate the usefulness of this approach through a model of the interaction between the Notch and the Wnt signaling pathways in mammalian skin, and its extensive analysis.\n\nConclusion\nWe introduce an approach for constructing computational models of biological systems that extends the framework of Boolean networks and uses formal verification methods for the analysis of the model. This approach can scale to multicellular models of complex pathways, and is therefore a useful tool for the analysis of complex biological systems. The hypotheses formulated during in-silico testing suggest new avenues to explore experimentally. Hence, this approach has the potential to efficiently complement experimental studies in biology.","lang":"eng"}],"publication":"BMC Systems Biology","date_published":"2007-01-08T00:00:00Z","publisher":"BioMed Central","day":"08"},{"page":"273 - 292","year":"2007","acknowledgement":"This research is partially supported by the Clore Fellowship Programme. Supported in part by the Swiss National Science Foundation.","intvolume":"      4444","month":"03","date_updated":"2021-01-12T07:56:49Z","type":"book_chapter","_id":"4417","title":"Abstract counterexample-based refinement for powerset domains","day":"30","publisher":"Springer","date_published":"2007-03-30T00:00:00Z","publication":"Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday","abstract":[{"lang":"eng","text":"Counterexample-guided abstraction refinement (CEGAR) is a powerful technique to scale automatic program analysis techniques to large programs. However, so far it has been used primarily for model checking in the context of predicate abstraction. We formalize CEGAR for general powerset domains. If a spurious abstract counterexample needs to be removed through abstraction refinement, there are often several choices, such as which program location(s) to refine, which abstract domain(s) to use at different locations, and which abstract values to compute. We define several plausible preference orderings on abstraction refinements, such as refining as “late” as possible and as “coarse” as possible. We present generic algorithms for finding refinements that are optimal with respect to the different preference orderings. We also compare the different orderings with respect to desirable properties, including the property if locally optimal refinements compose to a global optimum. Finally, we point out some difficulties with CEGAR for non-powerset domains."}],"publist_id":"314","doi":"10.1007/978-3-540-71322-7_13","date_created":"2018-12-11T12:08:45Z","publication_status":"published","volume":4444,"alternative_title":["LNCS"],"status":"public","quality_controlled":0,"author":[{"last_name":"Manevich","first_name":"Roman","full_name":"Manevich, Roman"},{"last_name":"Field","first_name":"John","full_name":"Field, John"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Thomas Henzinger"},{"first_name":"Ganesan","full_name":"Ramalingam, Ganesan","last_name":"Ramalingam"},{"last_name":"Sagiv","full_name":"Sagiv, Mooly","first_name":"Mooly"}],"extern":1,"citation":{"ama":"Manevich R, Field J, Henzinger TA, Ramalingam G, Sagiv M. Abstract counterexample-based refinement for powerset domains. In: <i>Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday</i>. Vol 4444. Springer; 2007:273-292. doi:<a href=\"https://doi.org/10.1007/978-3-540-71322-7_13\">10.1007/978-3-540-71322-7_13</a>","chicago":"Manevich, Roman, John Field, Thomas A Henzinger, Ganesan Ramalingam, and Mooly Sagiv. “Abstract Counterexample-Based Refinement for Powerset Domains.” In <i>Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday</i>, 4444:273–92. Springer, 2007. <a href=\"https://doi.org/10.1007/978-3-540-71322-7_13\">https://doi.org/10.1007/978-3-540-71322-7_13</a>.","apa":"Manevich, R., Field, J., Henzinger, T. A., Ramalingam, G., &#38; Sagiv, M. (2007). Abstract counterexample-based refinement for powerset domains. In <i>Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday</i> (Vol. 4444, pp. 273–292). Springer. <a href=\"https://doi.org/10.1007/978-3-540-71322-7_13\">https://doi.org/10.1007/978-3-540-71322-7_13</a>","ista":"Manevich R, Field J, Henzinger TA, Ramalingam G, Sagiv M. 2007.Abstract counterexample-based refinement for powerset domains. In: Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday. LNCS, vol. 4444, 273–292.","ieee":"R. Manevich, J. Field, T. A. Henzinger, G. Ramalingam, and M. Sagiv, “Abstract counterexample-based refinement for powerset domains,” in <i>Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday</i>, vol. 4444, Springer, 2007, pp. 273–292.","mla":"Manevich, Roman, et al. “Abstract Counterexample-Based Refinement for Powerset Domains.” <i>Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday</i>, vol. 4444, Springer, 2007, pp. 273–92, doi:<a href=\"https://doi.org/10.1007/978-3-540-71322-7_13\">10.1007/978-3-540-71322-7_13</a>.","short":"R. Manevich, J. Field, T.A. Henzinger, G. Ramalingam, M. Sagiv, in:, Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday, Springer, 2007, pp. 273–292."}},{"doi":"10.1145/1286821.1286824","date_created":"2018-12-11T12:08:53Z","publication_status":"published","volume":29,"status":"public","author":[{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Thomas Henzinger","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Christoph","full_name":"Kirsch, Christoph M","last_name":"Kirsch"}],"quality_controlled":0,"citation":{"chicago":"Henzinger, Thomas A, and Christoph Kirsch. “The Embedded Machine: Predictable, Portable Real-Time Code.” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. ACM, 2007. <a href=\"https://doi.org/10.1145/1286821.1286824\">https://doi.org/10.1145/1286821.1286824</a>.","apa":"Henzinger, T. A., &#38; Kirsch, C. (2007). The embedded machine: Predictable, portable real-time code. <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. ACM. <a href=\"https://doi.org/10.1145/1286821.1286824\">https://doi.org/10.1145/1286821.1286824</a>","ama":"Henzinger TA, Kirsch C. The embedded machine: Predictable, portable real-time code. <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. 2007;29(393). doi:<a href=\"https://doi.org/10.1145/1286821.1286824\">10.1145/1286821.1286824</a>","short":"T.A. Henzinger, C. Kirsch, ACM Transactions on Programming Languages and Systems (TOPLAS) 29 (2007).","mla":"Henzinger, Thomas A., and Christoph Kirsch. “The Embedded Machine: Predictable, Portable Real-Time Code.” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>, vol. 29, no. 393, ACM, 2007, doi:<a href=\"https://doi.org/10.1145/1286821.1286824\">10.1145/1286821.1286824</a>.","ista":"Henzinger TA, Kirsch C. 2007. The embedded machine: Predictable, portable real-time code. ACM Transactions on Programming Languages and Systems (TOPLAS). 29(393).","ieee":"T. A. Henzinger and C. Kirsch, “The embedded machine: Predictable, portable real-time code,” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>, vol. 29, no. 393. ACM, 2007."},"extern":1,"publisher":"ACM","day":"01","date_published":"2007-10-01T00:00:00Z","publication":"ACM Transactions on Programming Languages and Systems (TOPLAS)","abstract":[{"lang":"eng","text":"The Embedded Machine is a virtual machine that mediates in real time the interaction between software processes and physical processes. It separates the compilation of embedded programs into two phases. The first phase, the platform-independent compiler phase, generates E code (code executed by the Embedded Machine), which supervises the timing, not the scheduling of, application tasks relative to external events such as clock ticks and sensor interrupts. E code is portable and, given an input behavior, exhibits predictable (i.e., deterministic) timing and output behavior. The second phase, the platform-dependent compiler phase, checks the time safety of the E code, that is, whether platform performance (determined by the hardware) and platform utilization (determined by the scheduler of the operating system) enable its timely execution. We have used the Embedded Machine to compile and execute high-performance control applications written in Giotto, such as the flight control system of an autonomous model helicopter."}],"publist_id":"286","date_updated":"2021-01-12T07:57:01Z","type":"journal_article","_id":"4446","title":"The embedded machine: Predictable, portable real-time code","issue":393,"intvolume":"        29","year":"2007","month":"10"},{"conference":{"name":"DLT: Developments in Language Theory"},"date_updated":"2021-01-12T07:59:21Z","_id":"4511","type":"conference","title":"Quantitative generalizations of languages","page":"20 - 22","month":"06","acknowledgement":"This research was supported in part by the Swiss National Science Foundation and by the NSF grant CCR-0225610.","intvolume":"      4588","year":"2007","date_created":"2018-12-11T12:09:14Z","publication_status":"published","volume":4588,"doi":"10.1007/978-3-540-73208-2_2","quality_controlled":0,"alternative_title":["LNCS"],"status":"public","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724"}],"citation":{"short":"T.A. Henzinger, in:, Springer, 2007, pp. 20–22.","mla":"Henzinger, Thomas A. <i>Quantitative Generalizations of Languages</i>. Vol. 4588, Springer, 2007, pp. 20–22, doi:<a href=\"https://doi.org/10.1007/978-3-540-73208-2_2\">10.1007/978-3-540-73208-2_2</a>.","ieee":"T. A. Henzinger, “Quantitative generalizations of languages,” presented at the DLT: Developments in Language Theory, 2007, vol. 4588, pp. 20–22.","ista":"Henzinger TA. 2007. Quantitative generalizations of languages. DLT: Developments in Language Theory, LNCS, vol. 4588, 20–22.","chicago":"Henzinger, Thomas A. “Quantitative Generalizations of Languages,” 4588:20–22. Springer, 2007. <a href=\"https://doi.org/10.1007/978-3-540-73208-2_2\">https://doi.org/10.1007/978-3-540-73208-2_2</a>.","apa":"Henzinger, T. A. (2007). Quantitative generalizations of languages (Vol. 4588, pp. 20–22). Presented at the DLT: Developments in Language Theory, Springer. <a href=\"https://doi.org/10.1007/978-3-540-73208-2_2\">https://doi.org/10.1007/978-3-540-73208-2_2</a>","ama":"Henzinger TA. Quantitative generalizations of languages. In: Vol 4588. Springer; 2007:20-22. doi:<a href=\"https://doi.org/10.1007/978-3-540-73208-2_2\">10.1007/978-3-540-73208-2_2</a>"},"extern":1,"date_published":"2007-06-21T00:00:00Z","publisher":"Springer","day":"21","publist_id":"218","abstract":[{"text":"In the traditional view, a language is a set of words, i.e., a function from words to boolean values. We call this view “qualitative,” because each word either belongs to or does not belong to a language. Let Σ be an alphabet, and let us consider infinite words over Σ. Formally, a qualitative language over Σ is a function A: B . There are many applications of qualitative languages. For example, qualitative languages are used to specify the legal behaviors of systems, and zero-sum objectives of games played on graphs. In the former case, each behavior of a system is either legal or illegal; in the latter case, each outcome of a game is either winning or losing. For defining languages, it is convenient to use finite acceptors (or generators). In particular, qualitative languages are often defined using finite-state machines (so-called ω-automata) whose transitions are labeled by letters from Σ. For example, the states of an ω-automaton may represent states of a system, and the transition labels may represent atomic observables of a behavior. There is a rich and well-studied theory of finite-state acceptors of qualitative languages, namely, the theory of theω-regular languages.","lang":"eng"}]},{"doi":"10.1007/978-3-540-69507-3_7","date_created":"2018-12-11T12:09:15Z","publication_status":"published","volume":4362,"quality_controlled":0,"author":[{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A"}],"alternative_title":["LNCS"],"status":"public","extern":1,"citation":{"mla":"Henzinger, Thomas A. <i>Games, Time, and Probability: Graph Models for System Design and Analysis</i>. Vol. 4362, Springer, 2007, pp. 103–10, doi:<a href=\"https://doi.org/10.1007/978-3-540-69507-3_7\">10.1007/978-3-540-69507-3_7</a>.","short":"T.A. Henzinger, in:, Springer, 2007, pp. 103–110.","ista":"Henzinger TA. 2007. Games, time, and probability: Graph models for system design and analysis. SOFSEM: Current Trends in Theory and Practice of Computer Science, LNCS, vol. 4362, 103–110.","ieee":"T. A. Henzinger, “Games, time, and probability: Graph models for system design and analysis,” presented at the SOFSEM: Current Trends in Theory and Practice of Computer Science, 2007, vol. 4362, pp. 103–110.","apa":"Henzinger, T. A. (2007). Games, time, and probability: Graph models for system design and analysis (Vol. 4362, pp. 103–110). Presented at the SOFSEM: Current Trends in Theory and Practice of Computer Science, Springer. <a href=\"https://doi.org/10.1007/978-3-540-69507-3_7\">https://doi.org/10.1007/978-3-540-69507-3_7</a>","chicago":"Henzinger, Thomas A. “Games, Time, and Probability: Graph Models for System Design and Analysis,” 4362:103–10. Springer, 2007. <a href=\"https://doi.org/10.1007/978-3-540-69507-3_7\">https://doi.org/10.1007/978-3-540-69507-3_7</a>.","ama":"Henzinger TA. Games, time, and probability: Graph models for system design and analysis. In: Vol 4362. Springer; 2007:103-110. doi:<a href=\"https://doi.org/10.1007/978-3-540-69507-3_7\">10.1007/978-3-540-69507-3_7</a>"},"day":"04","publisher":"Springer","date_published":"2007-01-04T00:00:00Z","abstract":[{"text":"Digital technology is increasingly deployed in safety-critical situations. This calls for systematic design and verification methodologies that can cope with three major sources of system complexity: concurrency, real time, and uncertainty. We advocate a two-step process: formal modeling followed by algorithmic analysis (or, “model building” followed by “model checking”). We model the concurrent components of a reactive system as potential collaborators or adversaries in a multi-player game with temporal objectives, such as system safety. The real-time aspect of embedded systems requires models that combine discrete state transitions and continuous state evolutions. Uncertainty in the environment is naturally modeled by probabilistic state changes. As a result, we obtain three orthogonal extensions of the basic state-transition graph model for reactive systems —game graphs, timed graphs, and stochastic graphs— as well as combinations thereof. In this short text, we provide a uniform exposition of the underlying definitions. For verification algorithms, we refer the reader to the literature.","lang":"eng"}],"publist_id":"217","date_updated":"2021-01-12T07:59:22Z","_id":"4514","type":"conference","conference":{"name":"SOFSEM: Current Trends in Theory and Practice of Computer Science"},"title":"Games, time, and probability: Graph models for system design and analysis","page":"103 - 110","intvolume":"      4362","year":"2007","acknowledgement":"This research was supported in part by the Swiss National Science Foundation, and by the NSF ITR grant CCR-0225610.","month":"01"},{"quality_controlled":0,"author":[{"full_name":"Fisher, Jasmin","first_name":"Jasmin","last_name":"Fisher"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Thomas Henzinger","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"status":"public","extern":1,"citation":{"mla":"Fisher, Jasmin, and Thomas A. Henzinger. “Executable Cell Biology.” <i>Nature Biotechnology</i>, vol. 25, Nature Publishing Group, 2007, pp. 1239–49, doi:<a href=\"https://doi.org/10.1038/nbt1356\">10.1038/nbt1356</a>.","short":"J. Fisher, T.A. Henzinger, Nature Biotechnology 25 (2007) 1239–1249.","ieee":"J. Fisher and T. A. Henzinger, “Executable cell biology,” <i>Nature Biotechnology</i>, vol. 25. Nature Publishing Group, pp. 1239–1249, 2007.","ista":"Fisher J, Henzinger TA. 2007. Executable cell biology. Nature Biotechnology. 25, 1239–1249.","apa":"Fisher, J., &#38; Henzinger, T. A. (2007). Executable cell biology. <i>Nature Biotechnology</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/nbt1356\">https://doi.org/10.1038/nbt1356</a>","chicago":"Fisher, Jasmin, and Thomas A Henzinger. “Executable Cell Biology.” <i>Nature Biotechnology</i>. Nature Publishing Group, 2007. <a href=\"https://doi.org/10.1038/nbt1356\">https://doi.org/10.1038/nbt1356</a>.","ama":"Fisher J, Henzinger TA. Executable cell biology. <i>Nature Biotechnology</i>. 2007;25:1239-1249. doi:<a href=\"https://doi.org/10.1038/nbt1356\">10.1038/nbt1356</a>"},"publication_status":"published","date_created":"2018-12-11T12:09:19Z","volume":25,"doi":"10.1038/nbt1356","publist_id":"198","abstract":[{"lang":"eng","text":"Computational modeling of biological systems is becoming increasingly important in efforts to better understand complex biological behaviors. In this review, we distinguish between two types of biological models—mathematical and computational—which differ in their representations of biological phenomena. We call the approach of constructing computational models of biological systems 'executable biology', as it focuses on the design of executable computer algorithms that mimic biological phenomena. We survey the main modeling efforts in this direction, emphasize the applicability and benefits of executable models in biological research and highlight some of the challenges that executable biology poses for biology and computer science. We claim that for executable biology to reach its full potential as a mainstream biological technique, formal and algorithmic approaches must be integrated into biological research. This will drive biology toward a more precise engineering discipline."}],"date_published":"2007-01-01T00:00:00Z","publication":"Nature Biotechnology","day":"01","publisher":"Nature Publishing Group","title":"Executable cell biology","date_updated":"2021-01-12T07:59:28Z","_id":"4529","type":"journal_article","month":"01","intvolume":"        25","year":"2007","page":"1239 - 1249"},{"month":"09","year":"2007","intvolume":"      4646","title":"CSL: Computer Science Logic ","date_updated":"2019-08-02T12:38:32Z","_id":"4530","type":"conference_editor","publist_id":"194","abstract":[{"text":"This book constitutes the refereed proceedings of the 21st International Workshop on Computer Science Logic, CSL 2007, held as the 16th Annual Conference of the EACSL in Lausanne, Switzerland. The 36 revised full papers presented together with the abstracts of six invited lectures are organized in topical sections on logic and games, expressiveness, games and trees, logic and deduction, lambda calculus, finite model theory, linear logic, proof theory, and game semantics.","lang":"eng"}],"date_published":"2007-09-01T00:00:00Z","publication":"CSL: Computer Science Logic","day":"01","publisher":"Springer","status":"public","author":[{"full_name":"Duparc, Jacques","first_name":"Jacques","last_name":"Duparc"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Thomas Henzinger"}],"alternative_title":["LNCS"],"quality_controlled":0,"citation":{"short":"J. Duparc, T.A. Henzinger, CSL: Computer Science Logic , Springer, 2007.","mla":"Duparc, Jacques, and Thomas A. Henzinger. “CSL: Computer Science Logic .” <i>CSL: Computer Science Logic</i>, vol. 4646, Springer, 2007, doi:<a href=\"https://doi.org/10.1007/978-3-540-74915-8\">10.1007/978-3-540-74915-8</a>.","ista":"Duparc J, Henzinger TA. 2007. CSL: Computer Science Logic , Springer,p.","ieee":"J. Duparc and T. A. Henzinger, <i>CSL: Computer Science Logic </i>, vol. 4646. Springer, 2007.","chicago":"Duparc, Jacques, and Thomas A Henzinger. <i>CSL: Computer Science Logic </i>. <i>CSL: Computer Science Logic</i>. Vol. 4646. Springer, 2007. <a href=\"https://doi.org/10.1007/978-3-540-74915-8\">https://doi.org/10.1007/978-3-540-74915-8</a>.","apa":"Duparc, J., &#38; Henzinger, T. A. (2007). <i>CSL: Computer Science Logic </i>. <i>CSL: Computer Science Logic</i> (Vol. 4646). Springer. <a href=\"https://doi.org/10.1007/978-3-540-74915-8\">https://doi.org/10.1007/978-3-540-74915-8</a>","ama":"Duparc J, Henzinger TA. <i>CSL: Computer Science Logic </i>. Vol 4646. Springer; 2007. doi:<a href=\"https://doi.org/10.1007/978-3-540-74915-8\">10.1007/978-3-540-74915-8</a>"},"extern":1,"date_created":"2018-12-11T12:09:20Z","publication_status":"published","volume":4646,"doi":"10.1007/978-3-540-74915-8"},{"publication_status":"published","date_created":"2018-12-11T12:09:20Z","volume":"3(5):e92","doi":"10.1371/journal.pcbi.0030092","quality_controlled":0,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"author":[{"first_name":"Jasmin","full_name":"Fisher, Jasmin","last_name":"Fisher"},{"first_name":"Nir","full_name":"Piterman, Nir","last_name":"Piterman"},{"last_name":"Hajnal","full_name":"Hajnal, Alex","first_name":"Alex"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Thomas Henzinger"}],"status":"public","extern":1,"citation":{"chicago":"Fisher, Jasmin, Nir Piterman, Alex Hajnal, and Thomas A Henzinger. “Predictive Modeling of Signaling Crosstalk during C. Elegans Vulval Development.” <i>PLoS Computational Biology</i>. Public Library of Science, 2007. <a href=\"https://doi.org/10.1371/journal.pcbi.0030092\">https://doi.org/10.1371/journal.pcbi.0030092</a>.","apa":"Fisher, J., Piterman, N., Hajnal, A., &#38; Henzinger, T. A. (2007). Predictive modeling of signaling crosstalk during C. elegans vulval development. <i>PLoS Computational Biology</i>. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pcbi.0030092\">https://doi.org/10.1371/journal.pcbi.0030092</a>","ama":"Fisher J, Piterman N, Hajnal A, Henzinger TA. Predictive modeling of signaling crosstalk during C. elegans vulval development. <i>PLoS Computational Biology</i>. 2007;3(5):e92. doi:<a href=\"https://doi.org/10.1371/journal.pcbi.0030092\">10.1371/journal.pcbi.0030092</a>","mla":"Fisher, Jasmin, et al. “Predictive Modeling of Signaling Crosstalk during C. Elegans Vulval Development.” <i>PLoS Computational Biology</i>, vol. 3(5):e92, Public Library of Science, 2007, doi:<a href=\"https://doi.org/10.1371/journal.pcbi.0030092\">10.1371/journal.pcbi.0030092</a>.","short":"J. Fisher, N. Piterman, A. Hajnal, T.A. Henzinger, PLoS Computational Biology 3(5):e92 (2007).","ieee":"J. Fisher, N. Piterman, A. Hajnal, and T. A. Henzinger, “Predictive modeling of signaling crosstalk during C. elegans vulval development,” <i>PLoS Computational Biology</i>, vol. 3(5):e92. Public Library of Science, 2007.","ista":"Fisher J, Piterman N, Hajnal A, Henzinger TA. 2007. Predictive modeling of signaling crosstalk during C. elegans vulval development. PLoS Computational Biology. 3(5):e92."},"date_published":"2007-05-18T00:00:00Z","publication":"PLoS Computational Biology","day":"18","publisher":"Public Library of Science","publist_id":"195","abstract":[{"lang":"eng","text":"Caenorhabditis elegans vulval development provides an important paradigm for studying the process of cell fate determination and pattern formation during animal development. Although many genes controlling vulval cell fate specification have been identified, how they orchestrate themselves to generate a robust and invariant pattern of cell fates is not yet completely understood. Here, we have developed a dynamic computational model incorporating the current mechanistic understanding of gene interactions during this patterning process. A key feature of our model is the inclusion of multiple modes of crosstalk between the epidermal growth factor receptor (EGFR) and LIN-12/Notch signaling pathways, which together determine the fates of the six vulval precursor cells (VPCs). Computational analysis, using the model-checking technique, provides new biological insights into the regulatory network governing VPC fate specification and predicts novel negative feedback loops. In addition, our analysis shows that most mutations affecting vulval development lead to stable fate patterns in spite of variations in synchronicity between VPCs. Computational searches for the basis of this robustness show that a sequential activation of the EGFR-mediated inductive signaling and LIN-12 / Notch-mediated lateral signaling pathways is key to achieve a stable cell fate pattern. We demonstrate experimentally a time-delay between the activation of the inductive and lateral signaling pathways in wild-type animals and the loss of sequential signaling in mutants showing unstable fate patterns; thus, validating two key predictions provided by our modeling work. The insights gained by our modeling study further substantiate the usefulness of executing and analyzing mechanistic models to investigate complex biological behaviors."}],"date_updated":"2021-01-12T07:59:29Z","type":"journal_article","_id":"4531","title":"Predictive modeling of signaling crosstalk during C. elegans vulval development","month":"05","year":"2007","acknowledgement":"This work was supported in part by the Swiss National Science Foundation (grant 205321–111840)."},{"conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"date_updated":"2021-01-12T07:59:32Z","_id":"4537","type":"conference","title":"Assume-guarantee synthesis","page":"261 - 275","month":"01","intvolume":"      4424","acknowledgement":"This research was supported in part by the Swiss National Science Foundation and by the NSF grants CCR-0225610 and CCR-0234690.","year":"2007","date_created":"2018-12-11T12:09:22Z","publication_status":"published","volume":4424,"doi":"10.1007/978-3-540-71209-1_21","alternative_title":["LNCS"],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Krishnendu Chatterjee","orcid":"0000-0002-4561-241X"},{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"status":"public","quality_controlled":0,"extern":1,"citation":{"ista":"Chatterjee K, Henzinger TA. 2007. Assume-guarantee synthesis. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 4424, 261–275.","ieee":"K. Chatterjee and T. A. Henzinger, “Assume-guarantee synthesis,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, 2007, vol. 4424, pp. 261–275.","mla":"Chatterjee, Krishnendu, and Thomas A. Henzinger. <i>Assume-Guarantee Synthesis</i>. Vol. 4424, Springer, 2007, pp. 261–75, doi:<a href=\"https://doi.org/10.1007/978-3-540-71209-1_21\">10.1007/978-3-540-71209-1_21</a>.","short":"K. Chatterjee, T.A. Henzinger, in:, Springer, 2007, pp. 261–275.","ama":"Chatterjee K, Henzinger TA. Assume-guarantee synthesis. In: Vol 4424. Springer; 2007:261-275. doi:<a href=\"https://doi.org/10.1007/978-3-540-71209-1_21\">10.1007/978-3-540-71209-1_21</a>","chicago":"Chatterjee, Krishnendu, and Thomas A Henzinger. “Assume-Guarantee Synthesis,” 4424:261–75. Springer, 2007. <a href=\"https://doi.org/10.1007/978-3-540-71209-1_21\">https://doi.org/10.1007/978-3-540-71209-1_21</a>.","apa":"Chatterjee, K., &#38; Henzinger, T. A. (2007). Assume-guarantee synthesis (Vol. 4424, pp. 261–275). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Springer. <a href=\"https://doi.org/10.1007/978-3-540-71209-1_21\">https://doi.org/10.1007/978-3-540-71209-1_21</a>"},"date_published":"2007-01-01T00:00:00Z","day":"01","publisher":"Springer","publist_id":"186","abstract":[{"lang":"eng","text":"The classical synthesis problem for reactive systems asks, given a proponent process A and an opponent process B, to refine A so that the closed-loop system A parallel to B satisfies a given specification Phi. The solution of this problem requires the computation of a winning strategy for proponent A in a game against opponent B. We define and study the co-synthesis problem, where the proponent A consists itself of two independent processes, A = A(1)parallel to A(2), with specifications Phi(1) and Phi(2), and the goal is to refine both A(1) and A(2) so that A(1)parallel to A(2)parallel to B satisfies Phi(1) boolean AND Phi(2). For example, if the opponent B is a fair scheduler for the two processes A(1) and A(2), and Phi(i) specifies the requirements of mutual exclusion for A(i) (e.g., starvation freedom), then the co-synthesis problem asks for the automatic synthesis of a mutual-exclusion protocol. We show that co-synthesis defined classically, with the processes A(1) and A(2) either collaborating or competing, does not capture desirable solutions. Instead, the proper formulation of co-synthesis is the one where process A, competes with A(2) but not at the price of violating Phi(1), and vice versa. We call this assume-guarantee synthesis and show that it can be solved by computing secure-equilibrium strategies. In particular, from mutual-exclusion requirements the assume-guarantee synthesis algorithm automatically computes Peterson's protocol."}]},{"issue":184,"page":"1 - 23","month":"07","acknowledgement":"This research was supported in part by the NSF grants CCR-0225610 and CCR-0234690 by the SNSF under the Indo-Swiss Joint Research Programme and by the FRFC project “Centre Fédéré en Vérification” funded by the FNRS under grant 2.4530.02.","intvolume":"         3","year":"2007","date_updated":"2021-01-12T07:59:36Z","type":"journal_article","_id":"4547","title":"Algorithms for omega-regular games with imperfect information","date_published":"2007-07-27T00:00:00Z","publication":"Logical Methods in Computer Science","day":"27","publisher":"International Federation of Computational Logic","publist_id":"167","abstract":[{"lang":"eng","text":"We study observation-based strategies for two-player turn-based games on graphs with omega-regular objectives. An observation-based strategy relies on imperfect information about the history of a play, namely, on the past sequence of observations. Such games occur in the synthesis of a controller that does not see the private state of the plant. Our main results are twofold. First, we give a fixed-point algorithm for computing the set of states from which a player can win with a deterministic observation-based strategy for any omega-regular objective. The fixed point is computed in the lattice of antichains of state sets. This algorithm has the advantages of being directed by the objective and of avoiding an explicit subset construction on the game graph. Second, we give an algorithm for computing the set of states from which a player can win with probability 1 with a randomized observation-based strategy for a Buechi objective. This set is of interest because in the absence of perfect information, randomized strategies are more powerful than deterministic ones. We show that our algorithms are optimal by proving matching lower bounds."}],"date_created":"2018-12-11T12:09:25Z","publication_status":"published","volume":3,"doi":"10.2168/LMCS-3(3:4)2007","author":[{"full_name":"Krishnendu Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Raskin, Jean-François","first_name":"Jean","last_name":"Raskin"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"quality_controlled":0,"status":"public","citation":{"apa":"Chatterjee, K., Doyen, L., Henzinger, T. A., &#38; Raskin, J. (2007). Algorithms for omega-regular games with imperfect information. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.2168/LMCS-3(3:4)2007\">https://doi.org/10.2168/LMCS-3(3:4)2007</a>","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Thomas A Henzinger, and Jean Raskin. “Algorithms for Omega-Regular Games with Imperfect Information.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2007. <a href=\"https://doi.org/10.2168/LMCS-3(3:4)2007\">https://doi.org/10.2168/LMCS-3(3:4)2007</a>.","ama":"Chatterjee K, Doyen L, Henzinger TA, Raskin J. Algorithms for omega-regular games with imperfect information. <i>Logical Methods in Computer Science</i>. 2007;3(184):1-23. doi:<a href=\"https://doi.org/10.2168/LMCS-3(3:4)2007\">10.2168/LMCS-3(3:4)2007</a>","mla":"Chatterjee, Krishnendu, et al. “Algorithms for Omega-Regular Games with Imperfect Information.” <i>Logical Methods in Computer Science</i>, vol. 3, no. 184, International Federation of Computational Logic, 2007, pp. 1–23, doi:<a href=\"https://doi.org/10.2168/LMCS-3(3:4)2007\">10.2168/LMCS-3(3:4)2007</a>.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, J. Raskin, Logical Methods in Computer Science 3 (2007) 1–23.","ieee":"K. Chatterjee, L. Doyen, T. A. Henzinger, and J. Raskin, “Algorithms for omega-regular games with imperfect information,” <i>Logical Methods in Computer Science</i>, vol. 3, no. 184. International Federation of Computational Logic, pp. 1–23, 2007.","ista":"Chatterjee K, Doyen L, Henzinger TA, Raskin J. 2007. Algorithms for omega-regular games with imperfect information. Logical Methods in Computer Science. 3(184), 1–23."},"extern":1},{"status":"public","quality_controlled":0,"author":[{"full_name":"Krishnendu Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"}],"citation":{"ieee":"K. Chatterjee, “Stochastic ω-Regular Games,” University of California, Berkeley, 2007.","ista":"Chatterjee K. 2007. Stochastic ω-Regular Games. University of California, Berkeley.","short":"K. Chatterjee, Stochastic ω-Regular Games, University of California, Berkeley, 2007.","mla":"Chatterjee, Krishnendu. <i>Stochastic ω-Regular Games</i>. University of California, Berkeley, 2007, pp. 1–247.","ama":"Chatterjee K. Stochastic ω-Regular Games. 2007:1-247.","apa":"Chatterjee, K. (2007). <i>Stochastic ω-Regular Games</i>. University of California, Berkeley.","chicago":"Chatterjee, Krishnendu. “Stochastic ω-Regular Games.” University of California, Berkeley, 2007."},"extern":1,"date_created":"2018-12-11T12:09:29Z","publication_status":"published","publist_id":"150","abstract":[{"text":"We study games played on graphs with omega-regular conditions specified as parity, Rabin, Streett or Muller conditions. These games have applications in the verification, synthesis, modeling, testing, and compatibility checking of reactive systems. Important distinctions between graph games are as follows: (a) turn-based vs. concurrent games, depending on whether at a state of the game only a single player makes a move, or players make moves simultaneously; (b) deterministic vs. stochastic, depending on whether the transition function is a deterministic or a probabilistic function over successor states; and (c) zero-sum vs. non-zero-sum, depending on whether the objectives of the players are strictly conflicting or not.\n\nWe establish that the decision problem for turn-based stochastic zero-sum games with Rabin, Streett, and Muller objectives are NP-complete, coNP-complete, and PSPACE-complete, respectively, substantially improving the previously known 3EXPTIME bound. We also present strategy improvement style algorithms for turn-based stochastic Rabin and Streett games. In the case of concurrent stochastic zero-sum games with parity objectives we obtain a PSPACE bound, again improving the previously known 3EXPTIME bound. As a consequence, concurrent stochastic zero-sum games with Rabin, Streett, and Muller objectives can be solved in EXPSPACE, improving the previously known 4EXPTIME bound. We also present an elementary and combinatorial proof of the existence of memoryless \\epsilon-optimal strategies in concurrent stochastic games with reachability objectives, for all real \\epsilon&gt;0, where an \\epsilon-optimal strategy achieves the value of the game with in \\epsilon against all strategies of the opponent. We also use the proof techniques to present a strategy improvement style algorithm for concurrent stochastic reachability games.\n\nWe then go beyond \\omega-regular objectives and study the complexity of an important class of quantitative objectives, namely, limit-average objectives. In the case of limit-average games, the states of the graph is labeled with rewards and the goal is to maximize the long-run average of the rewards. We show that concurrent stochastic zero-sum games with limit-average objectives can be solved in EXPTIME.\n\nFinally, we introduce a new notion of equilibrium, called secure equilibrium, in non-zero-sum games which captures the notion of conditional competitiveness. We prove the existence of unique maximal secure equilibrium payoff profiles in turn-based deterministic games, and present algorithms to compute such payoff profiles. We also show how the notion of secure equilibrium extends the assume-guarantee style of reasoning in the game theoretic framework.","lang":"eng"}],"date_published":"2007-10-08T00:00:00Z","day":"08","publisher":"University of California, Berkeley","title":"Stochastic ω-Regular Games","main_file_link":[{"url":"http://chess.eecs.berkeley.edu/pubs/462.html","open_access":"0"}],"date_updated":"2021-01-12T07:59:42Z","_id":"4559","type":"dissertation","month":"10","year":"2007","acknowledgement":"Technical Report No. UCB/EECS-2007-122","page":"1 - 247"},{"article_processing_charge":"No","title":"A framework for compositional design and analysis of systems","type":"dissertation","_id":"4566","date_updated":"2021-01-12T07:59:45Z","year":"2007","month":"12","page":"1 - 244","oa_version":"None","extern":"1","citation":{"chicago":"Chakrabarti, Arindam. “A Framework for Compositional Design and Analysis of Systems.” University of California, Berkeley, 2007.","apa":"Chakrabarti, A. (2007). <i>A framework for compositional design and analysis of systems</i>. University of California, Berkeley.","ama":"Chakrabarti A. A framework for compositional design and analysis of systems. 2007:1-244.","short":"A. Chakrabarti, A Framework for Compositional Design and Analysis of Systems, University of California, Berkeley, 2007.","mla":"Chakrabarti, Arindam. <i>A Framework for Compositional Design and Analysis of Systems</i>. University of California, Berkeley, 2007, pp. 1–244.","ista":"Chakrabarti A. 2007. A framework for compositional design and analysis of systems. University of California, Berkeley.","ieee":"A. Chakrabarti, “A framework for compositional design and analysis of systems,” University of California, Berkeley, 2007."},"author":[{"last_name":"Chakrabarti","first_name":"Arindam","full_name":"Chakrabarti, Arindam"}],"status":"public","supervisor":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000-0002-2985-7724"},{"last_name":"Necula","first_name":"George","full_name":"Necula, George"},{"last_name":"Lee","full_name":"Lee, Edward","first_name":"Edward"},{"first_name":"Jack","full_name":"Silver, Jack","last_name":"Silver"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2018-12-11T12:09:31Z","publication_status":"published","abstract":[{"lang":"eng","text":"Complex system design today calls for compositional design and implementation. However each component is designed with certain assumptions about the environment it is meant to operate in, and delivering certain guarantees if those assumptions are satisfied; numerous inter-component interaction errors are introduced in the manual and error-prone integration process as there is little support in design environments for machine-readably representing these assumptions and guarantees and automatically checking consistency during integration.\r\n\r\nBased on Interface Automata we propose a framework for compositional design and analysis of systems: a set of domain-specific automata-theoretic type systems for compositional system specification and analysis by behavioral specification of open systems. We focus on three different domains: component-based hardware systems communicating on bidirectional wires. concurrent distributed recursive message-passing software systems, and embedded software system components operating in resource-constrained environments. For these domains we present approaches to formally represent the assumptions and conditional guarantees between interacting open system components. Composition of such components produces new components with the appropriate assumptions and guarantees. We check satisfaction of temporal logic specifications by such components, and the substitutability of one component with another in an arbitrary context. Using this framework one can analyze large systems incrementally without needing extensive summary information to close the system at each stage. Furthermore, we focus only on the inter-component interaction behavior without dealing with the full implementation details of each component. Many of the merits of automata-theoretic model-checking are combined with the compositionality afforded by type-system based techniques. We also present an integer-based extension of the conventional boolean verification framework motivated by our interface formalism for embedded software components.\r\n\r\nOur algorithms for checking the behavioral compatibility of component interfaces are available in our tool Chic, which can be used as a plug-in for the Java IDE JBuilder and the heterogenous modeling and design environment Ptolemy II.\r\n\r\nFinally, we address the complementary problem of partitioning a large system into meaningful coherent components by analyzing the interaction patterns between its basic elements. We demonstrate the usefulness of our partitioning approach by evaluating its efficacy in improving unit-test branch coverage for a large software system implemented in C."}],"language":[{"iso":"eng"}],"publist_id":"145","day":"20","publisher":"University of California, Berkeley","date_published":"2007-12-20T00:00:00Z"},{"author":[{"full_name":"Beyer, Dirk","first_name":"Dirk","last_name":"Beyer"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A"},{"last_name":"Jhala","full_name":"Jhala, Ranjit","first_name":"Ranjit"},{"full_name":"Majumdar, Ritankar S","first_name":"Ritankar","last_name":"Majumdar"}],"status":"public","quality_controlled":0,"citation":{"short":"D. Beyer, T.A. Henzinger, R. Jhala, R. Majumdar, International Journal on Software Tools for Technology Transfer 9 (2007) 505–525.","mla":"Beyer, Dirk, et al. “The Software Model Checker BLAST: Applications to Software Engineering.” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 9, no. 5, Springer, 2007, pp. 505–25, doi:<a href=\"https://doi.org/10.1007/s10009-007-0044-z\">10.1007/s10009-007-0044-z</a>.","ista":"Beyer D, Henzinger TA, Jhala R, Majumdar R. 2007. The software model checker BLAST: Applications to software engineering. International Journal on Software Tools for Technology Transfer. 9(5), 505–525.","ieee":"D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, “The software model checker BLAST: Applications to software engineering,” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 9, no. 5. Springer, pp. 505–525, 2007.","chicago":"Beyer, Dirk, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “The Software Model Checker BLAST: Applications to Software Engineering.” <i>International Journal on Software Tools for Technology Transfer</i>. Springer, 2007. <a href=\"https://doi.org/10.1007/s10009-007-0044-z\">https://doi.org/10.1007/s10009-007-0044-z</a>.","apa":"Beyer, D., Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2007). The software model checker BLAST: Applications to software engineering. <i>International Journal on Software Tools for Technology Transfer</i>. Springer. <a href=\"https://doi.org/10.1007/s10009-007-0044-z\">https://doi.org/10.1007/s10009-007-0044-z</a>","ama":"Beyer D, Henzinger TA, Jhala R, Majumdar R. The software model checker BLAST: Applications to software engineering. <i>International Journal on Software Tools for Technology Transfer</i>. 2007;9(5):505-525. doi:<a href=\"https://doi.org/10.1007/s10009-007-0044-z\">10.1007/s10009-007-0044-z</a>"},"extern":1,"publication_status":"published","date_created":"2018-12-11T12:09:31Z","volume":9,"doi":"10.1007/s10009-007-0044-z","publist_id":"139","abstract":[{"lang":"eng","text":"BLAST is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, BLAST either statically proves that the program satisfies the safety property, or provides an execution path that exhibits a violation of the property (or, since the problem is undecidable, does not terminate). BLAST constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. This paper gives an introduction to BLAST and demonstrates, through two case studies, how it can be applied to program verification and test-case generation. In the first case study, we use BLAST to statically prove memory safety for C programs. We use CCured, a type-based memory-safety analyzer, to annotate a program with run-time assertions that check for safe memory operations. Then, we use BLAST to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate execution scenarios that violate the assertions for the remaining run-time checks. In our second case study, we use BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. Given a C program and a target predicate p, BLAST determines the program locations q for which there exists a program execution that reaches q with p true, and automatically generates a set of test vectors that cause such executions. Our experiments show that BLAST can provide automated, precise, and scalable analysis for C programs."}],"date_published":"2007-10-01T00:00:00Z","publication":"International Journal on Software Tools for Technology Transfer","publisher":"Springer","day":"01","title":"The software model checker BLAST: Applications to software engineering","date_updated":"2021-01-12T07:59:45Z","_id":"4567","type":"journal_article","month":"10","intvolume":"         9","year":"2007","issue":"5","page":"505 - 525"},{"page":"825 - 837","acknowledgement":"This research was supported in part by the NSF grant CCR-0225610 and by the Swiss National Science Foundation.","intvolume":"      4596","year":"2007","month":"06","type":"conference","_id":"4570","date_updated":"2021-01-12T07:59:47Z","conference":{"name":"ICALP: Automata, Languages and Programming"},"title":"Minimum-time reachability in timed games","day":"29","publisher":"Springer","date_published":"2007-06-29T00:00:00Z","abstract":[{"text":"We consider the minimum-time reachability problem in concurrent two-player timed automaton game structures. We show how to compute the minimum time needed by a player to reach a target location against all possible choices of the opponent. We do not put any syntactic restriction on the game structure, nor do we require any player to guarantee time divergence. We only require players to use receptive strategies which do not block time. The minimal time is computed in part using a fixpoint expression, which we show can be evaluated on equivalence classes of a non-trivial extension of the clock-region equivalence relation for timed automata.","lang":"eng"}],"publist_id":"142","doi":"10.1007/978-3-540-73420-8_71","volume":4596,"date_created":"2018-12-11T12:09:32Z","publication_status":"published","citation":{"ama":"Brihaye T, Henzinger TA, Prabhu V, Raskin J. Minimum-time reachability in timed games. In: Vol 4596. Springer; 2007:825-837. doi:<a href=\"https://doi.org/10.1007/978-3-540-73420-8_71\">10.1007/978-3-540-73420-8_71</a>","apa":"Brihaye, T., Henzinger, T. A., Prabhu, V., &#38; Raskin, J. (2007). Minimum-time reachability in timed games (Vol. 4596, pp. 825–837). Presented at the ICALP: Automata, Languages and Programming, Springer. <a href=\"https://doi.org/10.1007/978-3-540-73420-8_71\">https://doi.org/10.1007/978-3-540-73420-8_71</a>","chicago":"Brihaye, Thomas, Thomas A Henzinger, Vinayak Prabhu, and Jean Raskin. “Minimum-Time Reachability in Timed Games,” 4596:825–37. Springer, 2007. <a href=\"https://doi.org/10.1007/978-3-540-73420-8_71\">https://doi.org/10.1007/978-3-540-73420-8_71</a>.","ieee":"T. Brihaye, T. A. Henzinger, V. Prabhu, and J. Raskin, “Minimum-time reachability in timed games,” presented at the ICALP: Automata, Languages and Programming, 2007, vol. 4596, pp. 825–837.","ista":"Brihaye T, Henzinger TA, Prabhu V, Raskin J. 2007. Minimum-time reachability in timed games. ICALP: Automata, Languages and Programming, LNCS, vol. 4596, 825–837.","mla":"Brihaye, Thomas, et al. <i>Minimum-Time Reachability in Timed Games</i>. Vol. 4596, Springer, 2007, pp. 825–37, doi:<a href=\"https://doi.org/10.1007/978-3-540-73420-8_71\">10.1007/978-3-540-73420-8_71</a>.","short":"T. Brihaye, T.A. Henzinger, V. Prabhu, J. Raskin, in:, Springer, 2007, pp. 825–837."},"extern":1,"quality_controlled":0,"author":[{"last_name":"Brihaye","first_name":"Thomas","full_name":"Brihaye, Thomas"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Thomas Henzinger"},{"full_name":"Prabhu, Vinayak S","first_name":"Vinayak","last_name":"Prabhu"},{"last_name":"Raskin","first_name":"Jean","full_name":"Raskin, Jean-François"}],"alternative_title":["LNCS"],"status":"public"},{"publisher":"ACM","day":"01","date_published":"2007-06-01T00:00:00Z","abstract":[{"text":"The success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose a method for automated abstraction refinement which overcomes some limitations of current predicate discovery schemes. In current schemes, the cause of a false alarm is identified as an infeasible error path, and the abstraction is refined in order to remove that path. By contrast, we view the cause of a false alarm -the spurious counterexample- as a full-fledged program, namely, a fragment of the original program whose control-flow graph may contain loops and represent unbounded computations. There are two advantages to using such path programs as counterexamples for abstraction refinement. First, we can bring the whole machinery of program analysis to bear on path programs, which are typically small compared to the original program. Specifically, we use constraint-based invariant generation to automatically infer invariants of path programs-so-called path invariants. Second, we use path invariants for abstraction refinement in order to remove not one infeasibility at a time, but at once all (possibly infinitely many) infeasible error computations that are represented by a path program. Unlike previous predicate discovery schemes, our method handles loops without unrolling them; it infers abstractions that involve universal quantification and naturally incorporates disjunctive reasoning.","lang":"eng"}],"publist_id":"137","doi":"10.1145/1250734.1250769","date_created":"2018-12-11T12:09:32Z","publication_status":"published","citation":{"ama":"Beyer D, Henzinger TA, Majumdar R, Rybalchenko A. Path invariants. In: ACM; 2007:300-309. doi:<a href=\"https://doi.org/10.1145/1250734.1250769\">10.1145/1250734.1250769</a>","apa":"Beyer, D., Henzinger, T. A., Majumdar, R., &#38; Rybalchenko, A. (2007). Path invariants (pp. 300–309). Presented at the PLDI: Programming Languages Design and Implementation, ACM. <a href=\"https://doi.org/10.1145/1250734.1250769\">https://doi.org/10.1145/1250734.1250769</a>","chicago":"Beyer, Dirk, Thomas A Henzinger, Ritankar Majumdar, and Andrey Rybalchenko. “Path Invariants,” 300–309. ACM, 2007. <a href=\"https://doi.org/10.1145/1250734.1250769\">https://doi.org/10.1145/1250734.1250769</a>.","ieee":"D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko, “Path invariants,” presented at the PLDI: Programming Languages Design and Implementation, 2007, pp. 300–309.","ista":"Beyer D, Henzinger TA, Majumdar R, Rybalchenko A. 2007. Path invariants. PLDI: Programming Languages Design and Implementation, 300–309.","mla":"Beyer, Dirk, et al. <i>Path Invariants</i>. ACM, 2007, pp. 300–09, doi:<a href=\"https://doi.org/10.1145/1250734.1250769\">10.1145/1250734.1250769</a>.","short":"D. Beyer, T.A. Henzinger, R. Majumdar, A. Rybalchenko, in:, ACM, 2007, pp. 300–309."},"extern":1,"quality_controlled":0,"author":[{"first_name":"Dirk","full_name":"Beyer, Dirk","last_name":"Beyer"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A"},{"full_name":"Majumdar, Ritankar S","first_name":"Ritankar","last_name":"Majumdar"},{"full_name":"Rybalchenko, Andrey","first_name":"Andrey","last_name":"Rybalchenko"}],"status":"public","page":"300 - 309","year":"2007","month":"06","_id":"4571","type":"conference","date_updated":"2021-01-12T07:59:48Z","conference":{"name":"PLDI: Programming Languages Design and Implementation"},"title":"Path invariants"},{"doi":"10.1007/978-3-540-69738-1_27","date_created":"2018-12-11T12:09:32Z","publication_status":"published","volume":4349,"alternative_title":["LNCS"],"status":"public","quality_controlled":0,"author":[{"last_name":"Beyer","first_name":"Dirk","full_name":"Beyer, Dirk"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Thomas Henzinger","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ritankar","full_name":"Majumdar, Ritankar S","last_name":"Majumdar"},{"full_name":"Rybalchenko, Andrey","first_name":"Andrey","last_name":"Rybalchenko"}],"citation":{"short":"D. Beyer, T.A. Henzinger, R. Majumdar, A. Rybalchenko, in:, Springer, 2007, pp. 378–394.","mla":"Beyer, Dirk, et al. <i>Invariant Synthesis for Combined Theories</i>. Vol. 4349, Springer, 2007, pp. 378–94, doi:<a href=\"https://doi.org/10.1007/978-3-540-69738-1_27\">10.1007/978-3-540-69738-1_27</a>.","ieee":"D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko, “Invariant synthesis for combined theories,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, 2007, vol. 4349, pp. 378–394.","ista":"Beyer D, Henzinger TA, Majumdar R, Rybalchenko A. 2007. Invariant synthesis for combined theories. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 4349, 378–394.","chicago":"Beyer, Dirk, Thomas A Henzinger, Ritankar Majumdar, and Andrey Rybalchenko. “Invariant Synthesis for Combined Theories,” 4349:378–94. Springer, 2007. <a href=\"https://doi.org/10.1007/978-3-540-69738-1_27\">https://doi.org/10.1007/978-3-540-69738-1_27</a>.","apa":"Beyer, D., Henzinger, T. A., Majumdar, R., &#38; Rybalchenko, A. (2007). Invariant synthesis for combined theories (Vol. 4349, pp. 378–394). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Springer. <a href=\"https://doi.org/10.1007/978-3-540-69738-1_27\">https://doi.org/10.1007/978-3-540-69738-1_27</a>","ama":"Beyer D, Henzinger TA, Majumdar R, Rybalchenko A. Invariant synthesis for combined theories. In: Vol 4349. Springer; 2007:378-394. doi:<a href=\"https://doi.org/10.1007/978-3-540-69738-1_27\">10.1007/978-3-540-69738-1_27</a>"},"extern":1,"publisher":"Springer","day":"01","date_published":"2007-01-01T00:00:00Z","abstract":[{"lang":"eng","text":"We present a constraint-based algorithm for the synthesis of invariants expressed in the combined theory of linear arithmetic and uninterpreted function symbols. Given a set of programmer-specified invariant templates, our algorithm reduces the invariant synthesis problem to a sequence of arithmetic constraint satisfaction queries. Since the combination of linear arithmetic and uninterpreted functions is a widely applied predicate domain for program verification, our algorithm provides a powerful tool to statically and automatically reason about program correctness. The algorithm can also be used for the synthesis of invariants over arrays and set data structures, because satisfiability questions for the theories of sets and arrays can be reduced to the theory of linear arithmetic with uninterpreted functions. We have implemented our algorithm and used it to find invariants for a low-level memory allocator written in C."}],"publist_id":"138","date_updated":"2021-01-12T07:59:48Z","_id":"4572","type":"conference","conference":{"name":"VMCAI: Verification, Model Checking and Abstract Interpretation"},"title":"Invariant synthesis for combined theories","page":"378 - 394","acknowledgement":"This research was sponsored in part by the grants NSF-CCF-0427202 and NSF-CCF-0546170.","year":"2007","intvolume":"      4349","month":"01"},{"page":"504 - 518","month":"07","intvolume":"      4590","acknowledgement":"This research was supported in part by the grant SFU/PRG 06-3, and by the Swiss National Science Foundation.","year":"2007","conference":{"name":"CAV: Computer Aided Verification"},"type":"conference","_id":"4573","date_updated":"2021-01-12T07:59:48Z","title":"Configurable software verification: Concretizing the convergence of model checking and program analysis","date_published":"2007-07-02T00:00:00Z","publisher":"Springer","day":"02","publist_id":"135","abstract":[{"text":"In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers are still mostly concerned with precision, e.g., the removal of spurious counterexamples; for this purpose they build and refine reachability trees. Lattice-based program analyzers, on the other hand, are primarily concerned with efficiency. We designed an algorithm and built a tool that can be configured to perform not only a purely tree-based or a purely lattice-based analysis, but offers many intermediate settings that have not been evaluated before. The algorithm and tool take one or more abstract interpreters, such as a predicate abstraction and a shape analysis, and configure their execution and interaction using several parameters. Our experiments show that such customization may lead to dramatic improvements in the precision-efficiency spectrum.","lang":"eng"}],"volume":4590,"date_created":"2018-12-11T12:09:33Z","publication_status":"published","doi":"10.1007/978-3-540-73368-3_51","citation":{"mla":"Beyer, Dirk, et al. <i>Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis</i>. Vol. 4590, Springer, 2007, pp. 504–18, doi:<a href=\"https://doi.org/10.1007/978-3-540-73368-3_51\">10.1007/978-3-540-73368-3_51</a>.","short":"D. Beyer, T.A. Henzinger, G. Théoduloz, in:, Springer, 2007, pp. 504–518.","ieee":"D. Beyer, T. A. Henzinger, and G. Théoduloz, “Configurable software verification: Concretizing the convergence of model checking and program analysis,” presented at the CAV: Computer Aided Verification, 2007, vol. 4590, pp. 504–518.","ista":"Beyer D, Henzinger TA, Théoduloz G. 2007. Configurable software verification: Concretizing the convergence of model checking and program analysis. CAV: Computer Aided Verification, LNCS, vol. 4590, 504–518.","apa":"Beyer, D., Henzinger, T. A., &#38; Théoduloz, G. (2007). Configurable software verification: Concretizing the convergence of model checking and program analysis (Vol. 4590, pp. 504–518). Presented at the CAV: Computer Aided Verification, Springer. <a href=\"https://doi.org/10.1007/978-3-540-73368-3_51\">https://doi.org/10.1007/978-3-540-73368-3_51</a>","chicago":"Beyer, Dirk, Thomas A Henzinger, and Grégory Théoduloz. “Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis,” 4590:504–18. Springer, 2007. <a href=\"https://doi.org/10.1007/978-3-540-73368-3_51\">https://doi.org/10.1007/978-3-540-73368-3_51</a>.","ama":"Beyer D, Henzinger TA, Théoduloz G. Configurable software verification: Concretizing the convergence of model checking and program analysis. In: Vol 4590. Springer; 2007:504-518. doi:<a href=\"https://doi.org/10.1007/978-3-540-73368-3_51\">10.1007/978-3-540-73368-3_51</a>"},"extern":1,"author":[{"last_name":"Beyer","first_name":"Dirk","full_name":"Beyer, Dirk"},{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Théoduloz","first_name":"Grégory","full_name":"Théoduloz, Grégory"}],"alternative_title":["LNCS"],"status":"public","quality_controlled":0},{"title":"An application of web-service interfaces","conference":{"name":"ICWS: International Conference on Web Service"},"date_updated":"2021-01-12T07:59:49Z","type":"conference","_id":"4575","month":"07","acknowledgement":"This research was supported in part by the NSF grant CCR-0225610 and by the Swiss National Science Foundation.","year":"2007","page":"831 - 838","quality_controlled":0,"status":"public","author":[{"full_name":"Beyer, Dirk","first_name":"Dirk","last_name":"Beyer"},{"last_name":"Chakrabarti","first_name":"Arindam","full_name":"Chakrabarti, Arindam"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Thomas Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Seshia, Sanjit A","first_name":"Sanjit","last_name":"Seshia"}],"citation":{"short":"D. Beyer, A. Chakrabarti, T.A. Henzinger, S. Seshia, in:, IEEE, 2007, pp. 831–838.","mla":"Beyer, Dirk, et al. <i>An Application of Web-Service Interfaces</i>. IEEE, 2007, pp. 831–38, doi:<a href=\"https://doi.org/10.1109/ICWS.2007.32 \">10.1109/ICWS.2007.32 </a>.","ista":"Beyer D, Chakrabarti A, Henzinger TA, Seshia S. 2007. An application of web-service interfaces. ICWS: International Conference on Web Service, 831–838.","ieee":"D. Beyer, A. Chakrabarti, T. A. Henzinger, and S. Seshia, “An application of web-service interfaces,” presented at the ICWS: International Conference on Web Service, 2007, pp. 831–838.","chicago":"Beyer, Dirk, Arindam Chakrabarti, Thomas A Henzinger, and Sanjit Seshia. “An Application of Web-Service Interfaces,” 831–38. IEEE, 2007. <a href=\"https://doi.org/10.1109/ICWS.2007.32 \">https://doi.org/10.1109/ICWS.2007.32 </a>.","apa":"Beyer, D., Chakrabarti, A., Henzinger, T. A., &#38; Seshia, S. (2007). An application of web-service interfaces (pp. 831–838). Presented at the ICWS: International Conference on Web Service, IEEE. <a href=\"https://doi.org/10.1109/ICWS.2007.32 \">https://doi.org/10.1109/ICWS.2007.32 </a>","ama":"Beyer D, Chakrabarti A, Henzinger TA, Seshia S. An application of web-service interfaces. In: IEEE; 2007:831-838. doi:<a href=\"https://doi.org/10.1109/ICWS.2007.32 \">10.1109/ICWS.2007.32 </a>"},"extern":1,"publication_status":"published","date_created":"2018-12-11T12:09:33Z","doi":"10.1109/ICWS.2007.32 ","publist_id":"134","abstract":[{"lang":"eng","text":"We present a case study to illustrate our formalism for the specification and verification of the method-invocation behavior of web-service applications constructed from asynchronously interacting multi-threaded distributed components. Our model is expressive enough to allow the representation of recursion and dynamic thread creation, and yet permits the algorithmic analysis of the following two questions: (1) Does a given service satisfy a safety specification? (2) Can a given service be substituted by a another service in an arbitrary context? Our case study is based on the Amazon.com E-Commerce Services (ECS) platform."}],"date_published":"2007-07-30T00:00:00Z","publisher":"IEEE","day":"30"},{"page":"188 - 217","issue":"3","intvolume":"       386","year":"2007","month":"11","type":"journal_article","_id":"4626","date_updated":"2021-01-12T08:00:37Z","title":"Concurrent reachability games","publisher":"Elsevier","day":"01","publication":"Theoretical Computer Science","date_published":"2007-11-01T00:00:00Z","abstract":[{"text":"We consider concurrent two-player games with reachability objectives. In such games, at each round, player 1 and player 2 independently and simultaneously choose moves, and the two choices determine the next state of the game. The objective of player 1 is to reach a set of target states; the objective of player 2 is to prevent this. These are zero-sum games, and the reachability objective is one of the most basic objectives: determining the set of states from which player 1 can win the game is a fundamental problem in control theory and system verification. There are three types of winning states, according to the degree of certainty with which player 1 can reach the target. From type-1 states, player 1 has a deterministic strategy to always reach the target. From type-2 states, player 1 has a randomized strategy to reach the target with probability 1. From type-3 states, player 1 has for every real ε&gt;0 a randomized strategy to reach the target with probability greater than 1−ε. We show that for finite state spaces, all three sets of winning states can be computed in polynomial time: type-1 states in linear time, and type-2 and type-3 states in quadratic time. The algorithms to compute the three sets of winning states also enable the construction of the winning and spoiling strategies.","lang":"eng"}],"publist_id":"81","doi":"10.1016/j.tcs.2007.07.008","volume":386,"date_created":"2018-12-11T12:09:49Z","publication_status":"published","citation":{"apa":"De Alfaro, L., Henzinger, T. A., &#38; Kupferman, O. (2007). Concurrent reachability games. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2007.07.008\">https://doi.org/10.1016/j.tcs.2007.07.008</a>","chicago":"De Alfaro, Luca, Thomas A Henzinger, and Orna Kupferman. “Concurrent Reachability Games.” <i>Theoretical Computer Science</i>. Elsevier, 2007. <a href=\"https://doi.org/10.1016/j.tcs.2007.07.008\">https://doi.org/10.1016/j.tcs.2007.07.008</a>.","ama":"De Alfaro L, Henzinger TA, Kupferman O. Concurrent reachability games. <i>Theoretical Computer Science</i>. 2007;386(3):188-217. doi:<a href=\"https://doi.org/10.1016/j.tcs.2007.07.008\">10.1016/j.tcs.2007.07.008</a>","short":"L. De Alfaro, T.A. Henzinger, O. Kupferman, Theoretical Computer Science 386 (2007) 188–217.","mla":"De Alfaro, Luca, et al. “Concurrent Reachability Games.” <i>Theoretical Computer Science</i>, vol. 386, no. 3, Elsevier, 2007, pp. 188–217, doi:<a href=\"https://doi.org/10.1016/j.tcs.2007.07.008\">10.1016/j.tcs.2007.07.008</a>.","ista":"De Alfaro L, Henzinger TA, Kupferman O. 2007. Concurrent reachability games. Theoretical Computer Science. 386(3), 188–217.","ieee":"L. De Alfaro, T. A. Henzinger, and O. Kupferman, “Concurrent reachability games,” <i>Theoretical Computer Science</i>, vol. 386, no. 3. Elsevier, pp. 188–217, 2007."},"extern":1,"quality_controlled":0,"author":[{"full_name":"de Alfaro, Luca","first_name":"Luca","last_name":"De Alfaro"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Thomas Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"status":"public"}]