[{"title":"Algorithms for omega-regular games with imperfect information","type":"journal_article","_id":"4547","date_updated":"2021-01-12T07:59:36Z","intvolume":"         3","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.","year":"2007","month":"07","page":"1 - 23","issue":184,"extern":1,"citation":{"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>","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>.","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.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, J. Raskin, Logical Methods in Computer Science 3 (2007) 1–23.","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>."},"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)"},"status":"public","author":[{"first_name":"Krishnendu","full_name":"Krishnendu Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A"},{"full_name":"Raskin, Jean-François","first_name":"Jean","last_name":"Raskin"}],"quality_controlled":0,"doi":"10.2168/LMCS-3(3:4)2007","license":"https://creativecommons.org/licenses/by/4.0/","volume":3,"publication_status":"published","date_created":"2018-12-11T12:09:25Z","abstract":[{"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.","lang":"eng"}],"publist_id":"167","publisher":"International Federation of Computational Logic","day":"27","publication":"Logical Methods in Computer Science","date_published":"2007-07-27T00:00:00Z"},{"page":"1 - 247","acknowledgement":"Technical Report No. UCB/EECS-2007-122","year":"2007","month":"10","date_updated":"2021-01-12T07:59:42Z","_id":"4559","type":"dissertation","main_file_link":[{"url":"http://chess.eecs.berkeley.edu/pubs/462.html","open_access":"0"}],"title":"Stochastic ω-Regular Games","day":"08","publisher":"University of California, Berkeley","date_published":"2007-10-08T00:00:00Z","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"}],"publist_id":"150","date_created":"2018-12-11T12:09:29Z","publication_status":"published","author":[{"orcid":"0000-0002-4561-241X","full_name":"Krishnendu Chatterjee","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"quality_controlled":0,"status":"public","citation":{"chicago":"Chatterjee, Krishnendu. “Stochastic ω-Regular Games.” University of California, Berkeley, 2007.","apa":"Chatterjee, K. (2007). <i>Stochastic ω-Regular Games</i>. University of California, Berkeley.","ama":"Chatterjee K. Stochastic ω-Regular Games. 2007:1-247.","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.","ieee":"K. Chatterjee, “Stochastic ω-Regular Games,” University of California, Berkeley, 2007.","ista":"Chatterjee K. 2007. Stochastic ω-Regular Games. University of California, Berkeley."},"extern":1},{"page":"1 - 244","year":"2007","month":"12","date_updated":"2021-01-12T07:59:45Z","type":"dissertation","_id":"4566","article_processing_charge":"No","title":"A framework for compositional design and analysis of systems","publisher":"University of California, Berkeley","day":"20","date_published":"2007-12-20T00:00:00Z","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","date_created":"2018-12-11T12:09:31Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","supervisor":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000-0002-2985-7724"},{"full_name":"Necula, George","first_name":"George","last_name":"Necula"},{"full_name":"Lee, Edward","first_name":"Edward","last_name":"Lee"},{"first_name":"Jack","full_name":"Silver, Jack","last_name":"Silver"}],"oa_version":"None","status":"public","author":[{"last_name":"Chakrabarti","full_name":"Chakrabarti, Arindam","first_name":"Arindam"}],"extern":"1","citation":{"apa":"Chakrabarti, A. (2007). <i>A framework for compositional design and analysis of systems</i>. University of California, Berkeley.","chicago":"Chakrabarti, Arindam. “A Framework for Compositional Design and Analysis of Systems.” University of California, Berkeley, 2007.","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.","ieee":"A. Chakrabarti, “A framework for compositional design and analysis of systems,” University of California, Berkeley, 2007.","ista":"Chakrabarti A. 2007. A framework for compositional design and analysis of systems. University of California, Berkeley."}},{"date_created":"2018-12-11T12:09:31Z","publication_status":"published","volume":9,"doi":"10.1007/s10009-007-0044-z","author":[{"first_name":"Dirk","full_name":"Beyer, Dirk","last_name":"Beyer"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724"},{"full_name":"Jhala, Ranjit","first_name":"Ranjit","last_name":"Jhala"},{"first_name":"Ritankar","full_name":"Majumdar, Ritankar S","last_name":"Majumdar"}],"quality_controlled":0,"status":"public","extern":1,"citation":{"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>","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>.","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.","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."},"date_published":"2007-10-01T00:00:00Z","publication":"International Journal on Software Tools for Technology Transfer","day":"01","publisher":"Springer","publist_id":"139","abstract":[{"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.","lang":"eng"}],"date_updated":"2021-01-12T07:59:45Z","type":"journal_article","_id":"4567","title":"The software model checker BLAST: Applications to software engineering","issue":"5","page":"505 - 525","month":"10","year":"2007","intvolume":"         9"},{"doi":"10.1007/978-3-540-73420-8_71","date_created":"2018-12-11T12:09:32Z","publication_status":"published","volume":4596,"quality_controlled":0,"author":[{"first_name":"Thomas","full_name":"Brihaye, Thomas","last_name":"Brihaye"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724"},{"full_name":"Prabhu, Vinayak S","first_name":"Vinayak","last_name":"Prabhu"},{"first_name":"Jean","full_name":"Raskin, Jean-François","last_name":"Raskin"}],"alternative_title":["LNCS"],"status":"public","citation":{"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>.","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>","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>","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.","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.","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."},"extern":1,"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","date_updated":"2021-01-12T07:59:47Z","type":"conference","_id":"4570","conference":{"name":"ICALP: Automata, Languages and Programming"},"title":"Minimum-time reachability in timed games","page":"825 - 837","intvolume":"      4596","year":"2007","acknowledgement":"This research was supported in part by the NSF grant CCR-0225610 and by the Swiss National Science Foundation.","month":"06"},{"year":"2007","month":"06","page":"300 - 309","title":"Path invariants","_id":"4571","type":"conference","date_updated":"2021-01-12T07:59:48Z","conference":{"name":"PLDI: Programming Languages Design and Implementation"},"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","day":"01","publisher":"ACM","date_published":"2007-06-01T00:00:00Z","extern":1,"citation":{"short":"D. Beyer, T.A. Henzinger, R. Majumdar, A. Rybalchenko, in:, ACM, 2007, pp. 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>.","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.","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>.","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>","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>"},"quality_controlled":0,"status":"public","author":[{"first_name":"Dirk","full_name":"Beyer, Dirk","last_name":"Beyer"},{"first_name":"Thomas A","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"first_name":"Ritankar","full_name":"Majumdar, Ritankar S","last_name":"Majumdar"},{"full_name":"Rybalchenko, Andrey","first_name":"Andrey","last_name":"Rybalchenko"}],"doi":"10.1145/1250734.1250769","date_created":"2018-12-11T12:09:32Z","publication_status":"published"},{"month":"01","acknowledgement":"This research was sponsored in part by the grants NSF-CCF-0427202 and NSF-CCF-0546170.","intvolume":"      4349","year":"2007","page":"378 - 394","title":"Invariant synthesis for combined theories","conference":{"name":"VMCAI: Verification, Model Checking and Abstract Interpretation"},"type":"conference","_id":"4572","date_updated":"2021-01-12T07:59:48Z","publist_id":"138","abstract":[{"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.","lang":"eng"}],"date_published":"2007-01-01T00:00:00Z","publisher":"Springer","day":"01","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>.","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.","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.","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,"status":"public","quality_controlled":0,"alternative_title":["LNCS"],"author":[{"first_name":"Dirk","full_name":"Beyer, Dirk","last_name":"Beyer"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724"},{"full_name":"Majumdar, Ritankar S","first_name":"Ritankar","last_name":"Majumdar"},{"first_name":"Andrey","full_name":"Rybalchenko, Andrey","last_name":"Rybalchenko"}],"volume":4349,"date_created":"2018-12-11T12:09:32Z","publication_status":"published","doi":"10.1007/978-3-540-69738-1_27"},{"day":"02","publisher":"Springer","date_published":"2007-07-02T00:00:00Z","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"}],"publist_id":"135","doi":"10.1007/978-3-540-73368-3_51","date_created":"2018-12-11T12:09:33Z","publication_status":"published","volume":4590,"alternative_title":["LNCS"],"author":[{"last_name":"Beyer","full_name":"Beyer, Dirk","first_name":"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":"Grégory","full_name":"Théoduloz, Grégory","last_name":"Théoduloz"}],"quality_controlled":0,"status":"public","extern":1,"citation":{"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>","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>.","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>","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.","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.","short":"D. Beyer, T.A. Henzinger, G. Théoduloz, in:, Springer, 2007, pp. 504–518.","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>."},"page":"504 - 518","acknowledgement":"This research was supported in part by the grant SFU/PRG 06-3, and by the Swiss National Science Foundation.","year":"2007","intvolume":"      4590","month":"07","date_updated":"2021-01-12T07:59:48Z","_id":"4573","type":"conference","conference":{"name":"CAV: Computer Aided Verification"},"title":"Configurable software verification: Concretizing the convergence of model checking and program analysis"},{"date_published":"2007-07-30T00:00:00Z","publisher":"IEEE","day":"30","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."}],"publication_status":"published","date_created":"2018-12-11T12:09:33Z","doi":"10.1109/ICWS.2007.32 ","citation":{"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>.","short":"D. Beyer, A. Chakrabarti, T.A. Henzinger, S. Seshia, in:, IEEE, 2007, pp. 831–838.","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,"quality_controlled":0,"status":"public","author":[{"last_name":"Beyer","first_name":"Dirk","full_name":"Beyer, Dirk"},{"first_name":"Arindam","full_name":"Chakrabarti, Arindam","last_name":"Chakrabarti"},{"first_name":"Thomas A","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"last_name":"Seshia","full_name":"Seshia, Sanjit A","first_name":"Sanjit"}],"page":"831 - 838","month":"07","year":"2007","acknowledgement":"This research was supported in part by the NSF grant CCR-0225610 and by the Swiss National Science Foundation.","conference":{"name":"ICWS: International Conference on Web Service"},"type":"conference","_id":"4575","date_updated":"2021-01-12T07:59:49Z","title":"An application of web-service interfaces"},{"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","publisher":"Elsevier","day":"01","date_published":"2007-11-01T00:00:00Z","publication":"Theoretical Computer Science","status":"public","author":[{"last_name":"De Alfaro","full_name":"de Alfaro, Luca","first_name":"Luca"},{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"}],"quality_controlled":0,"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,"doi":"10.1016/j.tcs.2007.07.008","date_created":"2018-12-11T12:09:49Z","publication_status":"published","volume":386,"year":"2007","intvolume":"       386","month":"11","page":"188 - 217","issue":"3","title":"Concurrent reachability games","date_updated":"2021-01-12T08:00:37Z","_id":"4626","type":"journal_article"},{"doi":"10.1021/ja062025p","article_type":"original","volume":128,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","date_created":"2020-09-18T10:13:36Z","oa_version":"None","keyword":["Colloid and Surface Chemistry","Biochemistry","General Chemistry","Catalysis"],"citation":{"ama":"Schanda P, Van Melckebeke H, Brutscher B. Speeding up three-dimensional protein NMR experiments to a few minutes. <i>Journal of the American Chemical Society</i>. 2006;128(28):9042-9043. doi:<a href=\"https://doi.org/10.1021/ja062025p\">10.1021/ja062025p</a>","apa":"Schanda, P., Van Melckebeke, H., &#38; Brutscher, B. (2006). Speeding up three-dimensional protein NMR experiments to a few minutes. <i>Journal of the American Chemical Society</i>. American Chemical Society. <a href=\"https://doi.org/10.1021/ja062025p\">https://doi.org/10.1021/ja062025p</a>","chicago":"Schanda, Paul, Hélène Van Melckebeke, and Bernhard Brutscher. “Speeding up Three-Dimensional Protein NMR Experiments to a Few Minutes.” <i>Journal of the American Chemical Society</i>. American Chemical Society, 2006. <a href=\"https://doi.org/10.1021/ja062025p\">https://doi.org/10.1021/ja062025p</a>.","ista":"Schanda P, Van Melckebeke H, Brutscher B. 2006. Speeding up three-dimensional protein NMR experiments to a few minutes. Journal of the American Chemical Society. 128(28), 9042–9043.","ieee":"P. Schanda, H. Van Melckebeke, and B. Brutscher, “Speeding up three-dimensional protein NMR experiments to a few minutes,” <i>Journal of the American Chemical Society</i>, vol. 128, no. 28. American Chemical Society, pp. 9042–9043, 2006.","short":"P. Schanda, H. Van Melckebeke, B. Brutscher, Journal of the American Chemical Society 128 (2006) 9042–9043.","mla":"Schanda, Paul, et al. “Speeding up Three-Dimensional Protein NMR Experiments to a Few Minutes.” <i>Journal of the American Chemical Society</i>, vol. 128, no. 28, American Chemical Society, 2006, pp. 9042–43, doi:<a href=\"https://doi.org/10.1021/ja062025p\">10.1021/ja062025p</a>."},"extern":"1","quality_controlled":"1","author":[{"full_name":"Schanda, Paul","first_name":"Paul","orcid":"0000-0002-9350-7606","id":"7B541462-FAF6-11E9-A490-E8DFE5697425","last_name":"Schanda"},{"first_name":"Hélène","full_name":"Van Melckebeke, Hélène","last_name":"Van Melckebeke"},{"full_name":"Brutscher, Bernhard","first_name":"Bernhard","last_name":"Brutscher"}],"status":"public","day":"21","publisher":"American Chemical Society","publication":"Journal of the American Chemical Society","date_published":"2006-06-21T00:00:00Z","abstract":[{"text":"We demonstrate for different protein samples that three-dimensional HNCO and HNCA correlation spectra may be recorded in a few minutes acquisition time using the band-selective excitation short-transient sequences presented here. This opens new perspectives for the NMR structural investigation of unstable protein samples and real-time site-resolved studies of protein kinetics.","lang":"eng"}],"language":[{"iso":"eng"}],"_id":"8488","type":"journal_article","date_updated":"2021-01-12T08:19:37Z","title":"Speeding up three-dimensional protein NMR experiments to a few minutes","article_processing_charge":"No","page":"9042-9043","issue":"28","publication_identifier":{"issn":["0002-7863","1520-5126"]},"year":"2006","intvolume":"       128","month":"06"},{"doi":"10.1002/mrc.1825","article_type":"original","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2020-09-18T10:13:42Z","publication_status":"published","volume":44,"oa_version":"None","quality_controlled":"1","status":"public","author":[{"orcid":"0000-0002-9350-7606","full_name":"Schanda, Paul","first_name":"Paul","last_name":"Schanda","id":"7B541462-FAF6-11E9-A490-E8DFE5697425"},{"full_name":"Forge, Vincent","first_name":"Vincent","last_name":"Forge"},{"full_name":"Brutscher, Bernhard","first_name":"Bernhard","last_name":"Brutscher"}],"citation":{"chicago":"Schanda, Paul, Vincent Forge, and Bernhard Brutscher. “HET-SOFAST NMR for Fast Detection of Structural Compactness and Heterogeneity along Polypeptide Chains.” <i>Magnetic Resonance in Chemistry</i>. Wiley, 2006. <a href=\"https://doi.org/10.1002/mrc.1825\">https://doi.org/10.1002/mrc.1825</a>.","apa":"Schanda, P., Forge, V., &#38; Brutscher, B. (2006). HET-SOFAST NMR for fast detection of structural compactness and heterogeneity along polypeptide chains. <i>Magnetic Resonance in Chemistry</i>. Wiley. <a href=\"https://doi.org/10.1002/mrc.1825\">https://doi.org/10.1002/mrc.1825</a>","ama":"Schanda P, Forge V, Brutscher B. HET-SOFAST NMR for fast detection of structural compactness and heterogeneity along polypeptide chains. <i>Magnetic Resonance in Chemistry</i>. 2006;44(S1):S177-S184. doi:<a href=\"https://doi.org/10.1002/mrc.1825\">10.1002/mrc.1825</a>","short":"P. Schanda, V. Forge, B. Brutscher, Magnetic Resonance in Chemistry 44 (2006) S177–S184.","mla":"Schanda, Paul, et al. “HET-SOFAST NMR for Fast Detection of Structural Compactness and Heterogeneity along Polypeptide Chains.” <i>Magnetic Resonance in Chemistry</i>, vol. 44, no. S1, Wiley, 2006, pp. S177–84, doi:<a href=\"https://doi.org/10.1002/mrc.1825\">10.1002/mrc.1825</a>.","ista":"Schanda P, Forge V, Brutscher B. 2006. HET-SOFAST NMR for fast detection of structural compactness and heterogeneity along polypeptide chains. Magnetic Resonance in Chemistry. 44(S1), S177–S184.","ieee":"P. Schanda, V. Forge, and B. Brutscher, “HET-SOFAST NMR for fast detection of structural compactness and heterogeneity along polypeptide chains,” <i>Magnetic Resonance in Chemistry</i>, vol. 44, no. S1. Wiley, pp. S177–S184, 2006."},"extern":"1","day":"06","publisher":"Wiley","date_published":"2006-07-06T00:00:00Z","publication":"Magnetic Resonance in Chemistry","abstract":[{"lang":"eng","text":"Structure elucidation of proteins by either NMR or X‐ray crystallography often requires the screening of a large number of samples for promising protein constructs and optimum solution conditions. For large‐scale screening of protein samples in solution, robust methods are needed that allow a rapid assessment of the folding of a polypeptide under diverse sample conditions. Here we present HET‐SOFAST NMR, a highly sensitive new method for semi‐quantitative characterization of the structural compactness and heterogeneity of polypeptide chains in solution. On the basis of one‐dimensional 1H HET‐SOFAST NMR data, obtained on well‐folded, molten globular, partially‐ and completely unfolded proteins, we define empirical thresholds that can be used as quantitative benchmarks for protein compactness. For 15N‐enriched protein samples, two‐dimensional 1H‐15N HET‐SOFAST correlation spectra provide site‐specific information about the structural heterogeneity along the polypeptide chain."}],"language":[{"iso":"eng"}],"date_updated":"2021-01-12T08:19:37Z","type":"journal_article","_id":"8489","title":"HET-SOFAST NMR for fast detection of structural compactness and heterogeneity along polypeptide chains","article_processing_charge":"No","page":"S177-S184","publication_identifier":{"issn":["0749-1581","1097-458X"]},"issue":"S1","year":"2006","intvolume":"        44","month":"07"},{"status":"public","author":[{"last_name":"Schanda","id":"7B541462-FAF6-11E9-A490-E8DFE5697425","orcid":"0000-0002-9350-7606","first_name":"Paul","full_name":"Schanda, Paul"},{"first_name":"Bernhard","full_name":"Brutscher, Bernhard","last_name":"Brutscher"}],"keyword":["Nuclear and High Energy Physics","Biophysics","Biochemistry","Condensed Matter Physics"],"extern":"1","citation":{"mla":"Schanda, Paul, and Bernhard Brutscher. “Hadamard Frequency-Encoded SOFAST-HMQC for Ultrafast Two-Dimensional Protein NMR.” <i>Journal of Magnetic Resonance</i>, vol. 178, no. 2, Elsevier, 2006, pp. 334–39, doi:<a href=\"https://doi.org/10.1016/j.jmr.2005.10.007\">10.1016/j.jmr.2005.10.007</a>.","short":"P. Schanda, B. Brutscher, Journal of Magnetic Resonance 178 (2006) 334–339.","ieee":"P. Schanda and B. Brutscher, “Hadamard frequency-encoded SOFAST-HMQC for ultrafast two-dimensional protein NMR,” <i>Journal of Magnetic Resonance</i>, vol. 178, no. 2. Elsevier, pp. 334–339, 2006.","ista":"Schanda P, Brutscher B. 2006. Hadamard frequency-encoded SOFAST-HMQC for ultrafast two-dimensional protein NMR. Journal of Magnetic Resonance. 178(2), 334–339.","apa":"Schanda, P., &#38; Brutscher, B. (2006). Hadamard frequency-encoded SOFAST-HMQC for ultrafast two-dimensional protein NMR. <i>Journal of Magnetic Resonance</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jmr.2005.10.007\">https://doi.org/10.1016/j.jmr.2005.10.007</a>","chicago":"Schanda, Paul, and Bernhard Brutscher. “Hadamard Frequency-Encoded SOFAST-HMQC for Ultrafast Two-Dimensional Protein NMR.” <i>Journal of Magnetic Resonance</i>. Elsevier, 2006. <a href=\"https://doi.org/10.1016/j.jmr.2005.10.007\">https://doi.org/10.1016/j.jmr.2005.10.007</a>.","ama":"Schanda P, Brutscher B. Hadamard frequency-encoded SOFAST-HMQC for ultrafast two-dimensional protein NMR. <i>Journal of Magnetic Resonance</i>. 2006;178(2):334-339. doi:<a href=\"https://doi.org/10.1016/j.jmr.2005.10.007\">10.1016/j.jmr.2005.10.007</a>"},"oa_version":"None","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2020-09-18T10:13:51Z","publication_status":"published","volume":178,"doi":"10.1016/j.jmr.2005.10.007","article_type":"original","language":[{"iso":"eng"}],"abstract":[{"text":"We demonstrate the feasibility of recording 1H–15N correlation spectra of proteins in only one second of acquisition time. The experiment combines recently proposed SOFAST-HMQC with Hadamard-type 15N frequency encoding. This allows site-resolved real-time NMR studies of kinetic processes in proteins with an increased time resolution. The sensitivity of the experiment is sufficient to be applicable to a wide range of molecular systems available at millimolar concentration on a high magnetic field spectrometer.","lang":"eng"}],"date_published":"2006-02-01T00:00:00Z","publication":"Journal of Magnetic Resonance","day":"01","publisher":"Elsevier","title":"Hadamard frequency-encoded SOFAST-HMQC for ultrafast two-dimensional protein NMR","article_processing_charge":"No","date_updated":"2021-01-12T08:19:38Z","_id":"8490","type":"journal_article","month":"02","year":"2006","intvolume":"       178","publication_identifier":{"issn":["1090-7807"]},"issue":"2","page":"334-339"},{"year":"2006","intvolume":"        15","month":"05","page":"611-640","publication_identifier":{"issn":["1553-5231"]},"issue":"2","article_processing_charge":"No","title":"Generic 3-dimensional volume-preserving diffeomorphisms with superexponential growth of number of periodic orbits","date_updated":"2021-01-12T08:19:48Z","type":"journal_article","_id":"8513","language":[{"iso":"eng"}],"day":"01","publisher":"American Institute of Mathematical Sciences (AIMS)","date_published":"2006-05-01T00:00:00Z","publication":"Discrete & Continuous Dynamical Systems - A","oa_version":"None","author":[{"orcid":"0000-0002-6051-2628","first_name":"Vadim","full_name":"Kaloshin, Vadim","last_name":"Kaloshin","id":"FE553552-CDE8-11E9-B324-C0EBE5697425"},{"first_name":"Maria","full_name":"Saprykina, Maria","last_name":"Saprykina"}],"quality_controlled":"1","status":"public","citation":{"ama":"Kaloshin V, Saprykina M. Generic 3-dimensional volume-preserving diffeomorphisms with superexponential growth of number of periodic orbits. <i>Discrete &#38; Continuous Dynamical Systems - A</i>. 2006;15(2):611-640. doi:<a href=\"https://doi.org/10.3934/dcds.2006.15.611\">10.3934/dcds.2006.15.611</a>","chicago":"Kaloshin, Vadim, and Maria Saprykina. “Generic 3-Dimensional Volume-Preserving Diffeomorphisms with Superexponential Growth of Number of Periodic Orbits.” <i>Discrete &#38; Continuous Dynamical Systems - A</i>. American Institute of Mathematical Sciences (AIMS), 2006. <a href=\"https://doi.org/10.3934/dcds.2006.15.611\">https://doi.org/10.3934/dcds.2006.15.611</a>.","apa":"Kaloshin, V., &#38; Saprykina, M. (2006). Generic 3-dimensional volume-preserving diffeomorphisms with superexponential growth of number of periodic orbits. <i>Discrete &#38; Continuous Dynamical Systems - A</i>. American Institute of Mathematical Sciences (AIMS). <a href=\"https://doi.org/10.3934/dcds.2006.15.611\">https://doi.org/10.3934/dcds.2006.15.611</a>","ista":"Kaloshin V, Saprykina M. 2006. Generic 3-dimensional volume-preserving diffeomorphisms with superexponential growth of number of periodic orbits. Discrete &#38; Continuous Dynamical Systems - A. 15(2), 611–640.","ieee":"V. Kaloshin and M. Saprykina, “Generic 3-dimensional volume-preserving diffeomorphisms with superexponential growth of number of periodic orbits,” <i>Discrete &#38; Continuous Dynamical Systems - A</i>, vol. 15, no. 2. American Institute of Mathematical Sciences (AIMS), pp. 611–640, 2006.","mla":"Kaloshin, Vadim, and Maria Saprykina. “Generic 3-Dimensional Volume-Preserving Diffeomorphisms with Superexponential Growth of Number of Periodic Orbits.” <i>Discrete &#38; Continuous Dynamical Systems - A</i>, vol. 15, no. 2, American Institute of Mathematical Sciences (AIMS), 2006, pp. 611–40, doi:<a href=\"https://doi.org/10.3934/dcds.2006.15.611\">10.3934/dcds.2006.15.611</a>.","short":"V. Kaloshin, M. Saprykina, Discrete &#38; Continuous Dynamical Systems - A 15 (2006) 611–640."},"extern":"1","article_type":"original","doi":"10.3934/dcds.2006.15.611","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2020-09-18T10:48:43Z","volume":15},{"oa_version":"None","status":"public","quality_controlled":"1","author":[{"last_name":"OTT","full_name":"OTT, WILLIAM","first_name":"WILLIAM"},{"full_name":"HUNT, BRIAN","first_name":"BRIAN","last_name":"HUNT"},{"orcid":"0000-0002-6051-2628","first_name":"Vadim","full_name":"Kaloshin, Vadim","last_name":"Kaloshin","id":"FE553552-CDE8-11E9-B324-C0EBE5697425"}],"extern":"1","citation":{"ama":"OTT W, HUNT B, Kaloshin V. The effect of projections on fractal sets and measures in Banach spaces. <i>Ergodic Theory and Dynamical Systems</i>. 2006;26(3):869-891. doi:<a href=\"https://doi.org/10.1017/s0143385705000714\">10.1017/s0143385705000714</a>","apa":"OTT, W., HUNT, B., &#38; Kaloshin, V. (2006). The effect of projections on fractal sets and measures in Banach spaces. <i>Ergodic Theory and Dynamical Systems</i>. Cambridge University Press. <a href=\"https://doi.org/10.1017/s0143385705000714\">https://doi.org/10.1017/s0143385705000714</a>","chicago":"OTT, WILLIAM, BRIAN HUNT, and Vadim Kaloshin. “The Effect of Projections on Fractal Sets and Measures in Banach Spaces.” <i>Ergodic Theory and Dynamical Systems</i>. Cambridge University Press, 2006. <a href=\"https://doi.org/10.1017/s0143385705000714\">https://doi.org/10.1017/s0143385705000714</a>.","ista":"OTT W, HUNT B, Kaloshin V. 2006. The effect of projections on fractal sets and measures in Banach spaces. Ergodic Theory and Dynamical Systems. 26(3), 869–891.","ieee":"W. OTT, B. HUNT, and V. Kaloshin, “The effect of projections on fractal sets and measures in Banach spaces,” <i>Ergodic Theory and Dynamical Systems</i>, vol. 26, no. 3. Cambridge University Press, pp. 869–891, 2006.","mla":"OTT, WILLIAM, et al. “The Effect of Projections on Fractal Sets and Measures in Banach Spaces.” <i>Ergodic Theory and Dynamical Systems</i>, vol. 26, no. 3, Cambridge University Press, 2006, pp. 869–91, doi:<a href=\"https://doi.org/10.1017/s0143385705000714\">10.1017/s0143385705000714</a>.","short":"W. OTT, B. HUNT, V. Kaloshin, Ergodic Theory and Dynamical Systems 26 (2006) 869–891."},"doi":"10.1017/s0143385705000714","article_type":"original","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2020-09-18T10:48:52Z","publication_status":"published","volume":26,"abstract":[{"text":"We study the extent to which the Hausdorff dimension of a compact subset of an infinite-dimensional Banach space is affected by a typical mapping into a finite-dimensional space. It is possible that the dimension drops under all such mappings, but the amount by which it typically drops is controlled by the ‘thickness exponent’ of the set, which was defined by Hunt and Kaloshin (Nonlinearity12 (1999), 1263–1275). More precisely, let $X$ be a compact subset of a Banach space $B$ with thickness exponent $\\tau$ and Hausdorff dimension $d$. Let $M$ be any subspace of the (locally) Lipschitz functions from $B$ to $\\mathbb{R}^{m}$ that contains the space of bounded linear functions. We prove that for almost every (in the sense of prevalence) function $f \\in M$, the Hausdorff dimension of $f(X)$ is at least $\\min\\{ m, d / (1 + \\tau) \\}$. We also prove an analogous result for a certain part of the dimension spectra of Borel probability measures supported on $X$. The factor $1 / (1 + \\tau)$ can be improved to $1 / (1 + \\tau / 2)$ if $B$ is a Hilbert space. Since dimension cannot increase under a (locally) Lipschitz function, these theorems become dimension preservation results when $\\tau = 0$. We conjecture that many of the attractors associated with the evolution equations of mathematical physics have thickness exponent zero. We also discuss the sharpness of our results in the case $\\tau > 0$.","lang":"eng"}],"language":[{"iso":"eng"}],"publisher":"Cambridge University Press","day":"01","date_published":"2006-06-01T00:00:00Z","publication":"Ergodic Theory and Dynamical Systems","title":"The effect of projections on fractal sets and measures in Banach spaces","article_processing_charge":"No","date_updated":"2021-01-12T08:19:48Z","_id":"8514","type":"journal_article","year":"2006","intvolume":"        26","month":"06","page":"869-891","publication_identifier":{"issn":["0143-3857","1469-4417"]},"issue":"3"},{"abstract":[{"lang":"eng","text":"We consider the evolution of a set carried by a space periodic incompressible stochastic flow in a Euclidean space. We\r\nreport on three main results obtained in [8, 9, 10] concerning long time behaviour for a typical realization of the stochastic flow. First, at time t most of the particles are at a distance of order √t away from the origin. Moreover, we prove a Central Limit Theorem for the evolution of a measure carried by the flow, which holds for almost every realization of the flow. Second, we show the existence of a zero measure full Hausdorff dimension set of points, which\r\nescape to infinity at a linear rate. Third, in the 2-dimensional case, we study the set of points visited by the original set by time t. Such a set, when scaled down by the factor of t, has a limiting non random shape."}],"language":[{"iso":"eng"}],"day":"01","publisher":"World Scientific","date_published":"2006-03-01T00:00:00Z","publication":"XIVth International Congress on Mathematical Physics","oa_version":"None","status":"public","quality_controlled":"1","author":[{"orcid":"0000-0002-6051-2628","full_name":"Kaloshin, Vadim","first_name":"Vadim","last_name":"Kaloshin","id":"FE553552-CDE8-11E9-B324-C0EBE5697425"},{"full_name":"DOLGOPYAT, D.","first_name":"D.","last_name":"DOLGOPYAT"},{"last_name":"KORALOV","first_name":"L.","full_name":"KORALOV, L."}],"citation":{"ama":"Kaloshin V, DOLGOPYAT D, KORALOV L. Long time behaviour of periodic stochastic flows. In: <i>XIVth International Congress on Mathematical Physics</i>. World Scientific; 2006:290-295. doi:<a href=\"https://doi.org/10.1142/9789812704016_0026\">10.1142/9789812704016_0026</a>","chicago":"Kaloshin, Vadim, D. DOLGOPYAT, and L. KORALOV. “Long Time Behaviour of Periodic Stochastic Flows.” In <i>XIVth International Congress on Mathematical Physics</i>, 290–95. World Scientific, 2006. <a href=\"https://doi.org/10.1142/9789812704016_0026\">https://doi.org/10.1142/9789812704016_0026</a>.","apa":"Kaloshin, V., DOLGOPYAT, D., &#38; KORALOV, L. (2006). Long time behaviour of periodic stochastic flows. In <i>XIVth International Congress on Mathematical Physics</i> (pp. 290–295). Lisbon, Portugal: World Scientific. <a href=\"https://doi.org/10.1142/9789812704016_0026\">https://doi.org/10.1142/9789812704016_0026</a>","ieee":"V. Kaloshin, D. DOLGOPYAT, and L. KORALOV, “Long time behaviour of periodic stochastic flows,” in <i>XIVth International Congress on Mathematical Physics</i>, Lisbon, Portugal, 2006, pp. 290–295.","ista":"Kaloshin V, DOLGOPYAT D, KORALOV L. 2006. Long time behaviour of periodic stochastic flows. XIVth International Congress on Mathematical Physics. International Congress on Mathematical Physics, 290–295.","short":"V. Kaloshin, D. DOLGOPYAT, L. KORALOV, in:, XIVth International Congress on Mathematical Physics, World Scientific, 2006, pp. 290–295.","mla":"Kaloshin, Vadim, et al. “Long Time Behaviour of Periodic Stochastic Flows.” <i>XIVth International Congress on Mathematical Physics</i>, World Scientific, 2006, pp. 290–95, doi:<a href=\"https://doi.org/10.1142/9789812704016_0026\">10.1142/9789812704016_0026</a>."},"extern":"1","doi":"10.1142/9789812704016_0026","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2020-09-18T10:48:59Z","publication_status":"published","year":"2006","month":"03","page":"290-295","publication_identifier":{"isbn":["9789812562012","9789812704016"]},"title":"Long time behaviour of periodic stochastic flows","article_processing_charge":"No","date_updated":"2021-01-12T08:19:49Z","type":"conference","_id":"8515","conference":{"location":"Lisbon, Portugal","name":"International Congress on Mathematical Physics","end_date":"2003-08-02","start_date":"2003-07-28"}},{"date_updated":"2021-01-12T08:19:58Z","_id":"854","type":"journal_article","title":"Complete mitochondrial genome and phylogeny of pleistocene mammoth Mammuthus primigenius","page":"0403 - 0410","issue":"3","intvolume":"         4","year":"2006","acknowledgement":"FAK is supported by the NSF Graduate Research Fellowship.\nWe thank the Natural History Museum, North-Eastern Research Center, Far Eastern Branch of the Russian Academy of Sciences for photographic material ofM. primigenius leg, V. A. Nikishina for artwork and technical support, Y.B. Yurov, G. Dvoryanchikov, N. Riazanskaya and T. Kolesnikova for technical support, K. Mehren and C. Gray for elephant specimens, and V. Y. Solovyev for help with artwork of animal images.","month":"03","doi":"10.1371/journal.pbio.0040073","publication_status":"published","date_created":"2018-12-11T11:48:51Z","volume":4,"author":[{"first_name":"Evgeny","full_name":"Rogaev, Evgeny I","last_name":"Rogaev"},{"first_name":"Yuri","full_name":"Moliaka, Yuri K","last_name":"Moliaka"},{"last_name":"Malyarchuk","full_name":"Malyarchuk, Boris A","first_name":"Boris"},{"orcid":"0000-0001-8243-4694","first_name":"Fyodor","full_name":"Fyodor Kondrashov","last_name":"Kondrashov","id":"44FDEF62-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Derenko, Miroslava V","first_name":"Miroslava","last_name":"Derenko"},{"last_name":"Chumakov","full_name":"Chumakov, Ilya M","first_name":"Ilya"},{"last_name":"Grigorenko","first_name":"Anastasia","full_name":"Grigorenko, Anastasia P"}],"quality_controlled":0,"status":"public","citation":{"short":"E. Rogaev, Y. Moliaka, B. Malyarchuk, F. Kondrashov, M. Derenko, I. Chumakov, A. Grigorenko, PLoS Biology 4 (2006) 0403–0410.","mla":"Rogaev, Evgeny, et al. “Complete Mitochondrial Genome and Phylogeny of Pleistocene Mammoth Mammuthus Primigenius.” <i>PLoS Biology</i>, vol. 4, no. 3, Public Library of Science, 2006, pp. 0403–10, doi:<a href=\"https://doi.org/10.1371/journal.pbio.0040073\">10.1371/journal.pbio.0040073</a>.","ieee":"E. Rogaev <i>et al.</i>, “Complete mitochondrial genome and phylogeny of pleistocene mammoth Mammuthus primigenius,” <i>PLoS Biology</i>, vol. 4, no. 3. Public Library of Science, pp. 0403–0410, 2006.","ista":"Rogaev E, Moliaka Y, Malyarchuk B, Kondrashov F, Derenko M, Chumakov I, Grigorenko A. 2006. Complete mitochondrial genome and phylogeny of pleistocene mammoth Mammuthus primigenius. PLoS Biology. 4(3), 0403–0410.","apa":"Rogaev, E., Moliaka, Y., Malyarchuk, B., Kondrashov, F., Derenko, M., Chumakov, I., &#38; Grigorenko, A. (2006). Complete mitochondrial genome and phylogeny of pleistocene mammoth Mammuthus primigenius. <i>PLoS Biology</i>. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pbio.0040073\">https://doi.org/10.1371/journal.pbio.0040073</a>","chicago":"Rogaev, Evgeny, Yuri Moliaka, Boris Malyarchuk, Fyodor Kondrashov, Miroslava Derenko, Ilya Chumakov, and Anastasia Grigorenko. “Complete Mitochondrial Genome and Phylogeny of Pleistocene Mammoth Mammuthus Primigenius.” <i>PLoS Biology</i>. Public Library of Science, 2006. <a href=\"https://doi.org/10.1371/journal.pbio.0040073\">https://doi.org/10.1371/journal.pbio.0040073</a>.","ama":"Rogaev E, Moliaka Y, Malyarchuk B, et al. Complete mitochondrial genome and phylogeny of pleistocene mammoth Mammuthus primigenius. <i>PLoS Biology</i>. 2006;4(3):0403-0410. doi:<a href=\"https://doi.org/10.1371/journal.pbio.0040073\">10.1371/journal.pbio.0040073</a>"},"extern":1,"day":"01","publisher":"Public Library of Science","date_published":"2006-03-01T00:00:00Z","publication":"PLoS Biology","abstract":[{"text":"Phylogenetic relationships between the extinct woolly mammoth (Mammuthus primigenius), and the Asian (Elephas maximus) and African savanna (Loxodonta africana) elephants remain unresolved. Here, we report the sequence of the complete mitochondrial genome (16,842 base pairs) of a woolly mammoth extracted from permafrost-preserved remains from the Pleistocene epoch - the oldest mitochondrial genome sequence determined to date. We demonstrate that well-preserved mitochondrial genome fragments, as long as ∼1,600-1700 base pairs, can be retrieved from pre-Holocene remains of an extinct species. Phylogenetic reconstruction of the Elephantinae clade suggests that M. primigenius and E. maximus are sister species that diverged soon after their common ancestor split from the L. africana lineage. Low nucleotide diversity found between independently determined mitochondrial genomic sequences of woolly mammoths separated geographically and in time suggests that north-eastern Siberia was occupied by a relatively homogeneous population of M. primigenius throughout the late Pleistocene.","lang":"eng"}],"publist_id":"6794"},{"title":"Evolution of glyoxylate cycle enzymes in Metazoa Evidence of multiple horizontal transfer events and pseudogene formation","type":"journal_article","_id":"868","date_updated":"2021-01-12T08:20:31Z","month":"10","intvolume":"         1","acknowledgement":"The authors thank Alexey Kondrashov for suggesting the possibility of non- orthologous gene displacement in glyoxylate cycle specific enzymes and for critical reading of this manuscript. FAK is a National Science Foundation Graduate Fellow.","year":"2006","citation":{"ama":"Kondrashov F, Koonin E, Morgunov I, Finogenova T, Kondrashova M. Evolution of glyoxylate cycle enzymes in Metazoa Evidence of multiple horizontal transfer events and pseudogene formation. <i>Biology Direct</i>. 2006;1. doi:<a href=\"https://doi.org/10.1186/1745-6150-1-31\">10.1186/1745-6150-1-31</a>","apa":"Kondrashov, F., Koonin, E., Morgunov, I., Finogenova, T., &#38; Kondrashova, M. (2006). Evolution of glyoxylate cycle enzymes in Metazoa Evidence of multiple horizontal transfer events and pseudogene formation. <i>Biology Direct</i>. BioMed Central. <a href=\"https://doi.org/10.1186/1745-6150-1-31\">https://doi.org/10.1186/1745-6150-1-31</a>","chicago":"Kondrashov, Fyodor, Eugene Koonin, Igor Morgunov, Tatiana Finogenova, and Marie Kondrashova. “Evolution of Glyoxylate Cycle Enzymes in Metazoa Evidence of Multiple Horizontal Transfer Events and Pseudogene Formation.” <i>Biology Direct</i>. BioMed Central, 2006. <a href=\"https://doi.org/10.1186/1745-6150-1-31\">https://doi.org/10.1186/1745-6150-1-31</a>.","ista":"Kondrashov F, Koonin E, Morgunov I, Finogenova T, Kondrashova M. 2006. Evolution of glyoxylate cycle enzymes in Metazoa Evidence of multiple horizontal transfer events and pseudogene formation. Biology Direct. 1.","ieee":"F. Kondrashov, E. Koonin, I. Morgunov, T. Finogenova, and M. Kondrashova, “Evolution of glyoxylate cycle enzymes in Metazoa Evidence of multiple horizontal transfer events and pseudogene formation,” <i>Biology Direct</i>, vol. 1. BioMed Central, 2006.","short":"F. Kondrashov, E. Koonin, I. Morgunov, T. Finogenova, M. Kondrashova, Biology Direct 1 (2006).","mla":"Kondrashov, Fyodor, et al. “Evolution of Glyoxylate Cycle Enzymes in Metazoa Evidence of Multiple Horizontal Transfer Events and Pseudogene Formation.” <i>Biology Direct</i>, vol. 1, BioMed Central, 2006, doi:<a href=\"https://doi.org/10.1186/1745-6150-1-31\">10.1186/1745-6150-1-31</a>."},"extern":1,"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)"},"status":"public","author":[{"orcid":"0000-0001-8243-4694","full_name":"Fyodor Kondrashov","first_name":"Fyodor","last_name":"Kondrashov","id":"44FDEF62-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Koonin, Eugene V","first_name":"Eugene","last_name":"Koonin"},{"last_name":"Morgunov","full_name":"Morgunov, Igor G","first_name":"Igor"},{"full_name":"Finogenova, Tatiana V","first_name":"Tatiana","last_name":"Finogenova"},{"last_name":"Kondrashova","full_name":"Kondrashova, Marie N","first_name":"Marie"}],"quality_controlled":0,"volume":1,"publication_status":"published","date_created":"2018-12-11T11:48:56Z","doi":"10.1186/1745-6150-1-31","publist_id":"6778","abstract":[{"text":"Background: The glyoxylate cycle is thought to be present in bacteria, protists, plants, fungi, and nematodes, but not in other Metazoa. However, activity of the glyoxylate cycle enzymes, malate synthase (MS) and isocitrate lyase (ICL), in animal tissues has been reported. In order to clarify the status of the MS and ICL genes in animals and get an insight into their evolution, we undertook a comparative-genomic study. Results: Using sequence similarity searches, we identified MS genes in arthropods, echinoderms, and vertebrates, including platypus and opossum, but not in the numerous sequenced genomes of placental mammals. The regions of the placental mammals' genomes expected to code for malate synthase, as determined by comparison of the gene orders in vertebrate genomes, show clear similarity to the opossum MS sequence but contain stop codons, indicating that the MS gene became a pseudogene in placental mammals. By contrast, the ICL gene is undetectable in animals other than the nematodes that possess a bifunctional, fused ICL-MS gene. Examination of phylogenetic trees of MS and ICL suggests multiple horizontal gene transfer events that probably went in both directions between several bacterial and eukaryotic lineages. The strongest evidence was obtained for the acquisition of the bifunctional ICL-MS gene from an as yet unknown bacterial source with the corresponding operonic organization by the common ancestor of the nematodes. Conclusion: The distribution of the MS and ICL genes in animals suggests that either they encode alternative enzymes of the glyoxylate cycle that are not orthologous to the known MS and ICL or the animal MS acquired a new function that remains to be characterized. Regardless of the ultimate solution to this conundrum, the genes for the glyoxylate cycle enzymes present a remarkable variety of evolutionary events including unusual horizontal gene transfer from bacteria to animals.","lang":"eng"}],"publication":"Biology Direct","date_published":"2006-10-23T00:00:00Z","publisher":"BioMed Central","day":"23"},{"abstract":[{"lang":"eng","text":"The impact of synonymous nucleotide substitutions on fitness in mammals remains controversial. Despite some indications of selective constraint, synonymous sites are often assumed to be neutral, and the rate of their evolution is used as a proxy for mutation rate. We subdivide all sites into four classes in terms of the mutable CpG context, nonCpG, postC, preG, and postCpreG, and compare four-fold synonymous sites and intron sites residing outside transposable elements. The distribution of the rate of evolution across all synonymous sites is trimodal. Rate of evolution at nonCpG synonymous sites, not preceded by C and not followed by G, is ∼10% below that at such intron sites. In contrast, rate of evolution at postCpreG synonymous sites is ∼30% above that at such intron sites. Finally, synonymous and intron postC and preG sites evolve at similar rates. The relationship between the levels of polymorphism at the corresponding synonymous and intron sites is very similar to that between their rates of evolution. Within every class, synonymous sites are occupied by G or C much more often than intron sites, whose nucleotide composition is consistent with neutral mutation-drift equilibrium. These patterns suggest that synonymous sites are under weak selection in favor of G and C, with the average coefficient s∼0.25/Ne∼10-5, where Ne is the effective population size. Such selection decelerates evolution and reduces variability at sites with symmetric mutation, but has the opposite effects at sites where the favored nucleotides are more mutable. The amino-acid composition of proteins dictates that many synonymous sites are CpGprone, which causes them, on average, to evolve faster and to be more polymorphic than intron sites. An average genotype carries ∼107 suboptimal nucleotides at synonymous sites, implying synergistic epistasis in selection against them."}],"publist_id":"6779","publisher":"Elsevier","day":"21","publication":"Journal of Theoretical Biology","date_published":"2006-06-21T00:00:00Z","extern":1,"citation":{"mla":"Kondrashov, Fyodor, et al. “Selection in Favor of Nucleotides G and C Diversifies Evolution Rates and Levels of Polymorphism at Mammalian Synonymous Sites.” <i>Journal of Theoretical Biology</i>, vol. 240, no. 4, Elsevier, 2006, pp. 616–26, doi:<a href=\"https://doi.org/10.1016/j.jtbi.2005.10.020\">10.1016/j.jtbi.2005.10.020</a>.","short":"F. Kondrashov, A. Ogurtsov, A. Kondrashov, Journal of Theoretical Biology 240 (2006) 616–626.","ista":"Kondrashov F, Ogurtsov A, Kondrashov A. 2006. Selection in favor of nucleotides G and C diversifies evolution rates and levels of polymorphism at mammalian synonymous sites. Journal of Theoretical Biology. 240(4), 616–626.","ieee":"F. Kondrashov, A. Ogurtsov, and A. Kondrashov, “Selection in favor of nucleotides G and C diversifies evolution rates and levels of polymorphism at mammalian synonymous sites,” <i>Journal of Theoretical Biology</i>, vol. 240, no. 4. Elsevier, pp. 616–626, 2006.","apa":"Kondrashov, F., Ogurtsov, A., &#38; Kondrashov, A. (2006). Selection in favor of nucleotides G and C diversifies evolution rates and levels of polymorphism at mammalian synonymous sites. <i>Journal of Theoretical Biology</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jtbi.2005.10.020\">https://doi.org/10.1016/j.jtbi.2005.10.020</a>","chicago":"Kondrashov, Fyodor, Aleksey Ogurtsov, and Alexey Kondrashov. “Selection in Favor of Nucleotides G and C Diversifies Evolution Rates and Levels of Polymorphism at Mammalian Synonymous Sites.” <i>Journal of Theoretical Biology</i>. Elsevier, 2006. <a href=\"https://doi.org/10.1016/j.jtbi.2005.10.020\">https://doi.org/10.1016/j.jtbi.2005.10.020</a>.","ama":"Kondrashov F, Ogurtsov A, Kondrashov A. Selection in favor of nucleotides G and C diversifies evolution rates and levels of polymorphism at mammalian synonymous sites. <i>Journal of Theoretical Biology</i>. 2006;240(4):616-626. doi:<a href=\"https://doi.org/10.1016/j.jtbi.2005.10.020\">10.1016/j.jtbi.2005.10.020</a>"},"author":[{"full_name":"Fyodor Kondrashov","first_name":"Fyodor","orcid":"0000-0001-8243-4694","id":"44FDEF62-F248-11E8-B48F-1D18A9856A87","last_name":"Kondrashov"},{"full_name":"Ogurtsov, Aleksey Yu","first_name":"Aleksey","last_name":"Ogurtsov"},{"last_name":"Kondrashov","first_name":"Alexey","full_name":"Kondrashov, Alexey S"}],"quality_controlled":0,"status":"public","doi":"10.1016/j.jtbi.2005.10.020","volume":240,"date_created":"2018-12-11T11:48:56Z","publication_status":"published","acknowledgement":"This research was supported in part by the Intramural Research Program of the NIH, National Library of Medicine.","intvolume":"       240","year":"2006","month":"06","page":"616 - 626","issue":"4","title":"Selection in favor of nucleotides G and C diversifies evolution rates and levels of polymorphism at mammalian synonymous sites","_id":"869","type":"journal_article","date_updated":"2021-01-12T08:20:33Z"},{"year":"2006","intvolume":"       239","month":"03","page":"141 - 151","issue":"2","title":"Role of selection in fixation of gene duplications","type":"journal_article","_id":"873","date_updated":"2021-01-12T08:20:47Z","abstract":[{"text":"New genes commonly appear through complete or partial duplications of pre-existing genes. Duplications of long DNA segments are constantly produced by rare mutations, may become fixed in a population by selection or random drift, and are subject to divergent evolution of the paralogous sequences after fixation, although gene conversion can impede this process. New data shed some light on each of these processes. Mutations which involve duplications can occur through at least two different mechanisms, backward strand slippage during DNA replication and unequal crossing-over. The background rate of duplication of a complete gene in humans is 10-9-10-10 per generation, although many genes located within hot-spots of large-scale mutation are duplicated much more often. Many gene duplications affect fitness strongly, and are responsible, through gene dosage effects, for a number of genetic diseases. However, high levels of intrapopulation polymorphism caused by presence or absence of long, gene-containing DNA segments imply that some duplications are not under strong selection. The polymorphism to fixation ratios appear to be approximately the same for gene duplications and for presumably selectively neutral nucleotide substitutions, which, according to the McDonald-Kreitman test, is consistent with selective neutrality of duplications. However, this pattern can also be due to negative selection against most of segregating duplications and positive selection for at least some duplications which become fixed. Patterns in post-fixation evolution of duplicated genes do not easily reveal the causes of fixations. Many gene duplications which became fixed recently in a variety of organisms were positively selected because the increased expression of the corresponding genes was beneficial. The effects of gene dosage provide a unified framework for studying all phases of the life history of a gene duplication. Application of well-known methods of evolutionary genetics to accumulating data on new, polymorphic, and fixed duplication will enhance our understanding of the role of natural selection in the evolution by gene duplication.","lang":"eng"}],"publist_id":"6773","publisher":"Elsevier","day":"21","publication":"Journal of Theoretical Biology","date_published":"2006-03-21T00:00:00Z","citation":{"ieee":"F. Kondrashov and A. Kondrashov, “Role of selection in fixation of gene duplications,” <i>Journal of Theoretical Biology</i>, vol. 239, no. 2. Elsevier, pp. 141–151, 2006.","ista":"Kondrashov F, Kondrashov A. 2006. Role of selection in fixation of gene duplications. Journal of Theoretical Biology. 239(2), 141–151.","mla":"Kondrashov, Fyodor, and Alexey Kondrashov. “Role of Selection in Fixation of Gene Duplications.” <i>Journal of Theoretical Biology</i>, vol. 239, no. 2, Elsevier, 2006, pp. 141–51, doi:<a href=\"https://doi.org/10.1016/j.jtbi.2005.08.033\">10.1016/j.jtbi.2005.08.033</a>.","short":"F. Kondrashov, A. Kondrashov, Journal of Theoretical Biology 239 (2006) 141–151.","ama":"Kondrashov F, Kondrashov A. Role of selection in fixation of gene duplications. <i>Journal of Theoretical Biology</i>. 2006;239(2):141-151. doi:<a href=\"https://doi.org/10.1016/j.jtbi.2005.08.033\">10.1016/j.jtbi.2005.08.033</a>","apa":"Kondrashov, F., &#38; Kondrashov, A. (2006). Role of selection in fixation of gene duplications. <i>Journal of Theoretical Biology</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jtbi.2005.08.033\">https://doi.org/10.1016/j.jtbi.2005.08.033</a>","chicago":"Kondrashov, Fyodor, and Alexey Kondrashov. “Role of Selection in Fixation of Gene Duplications.” <i>Journal of Theoretical Biology</i>. Elsevier, 2006. <a href=\"https://doi.org/10.1016/j.jtbi.2005.08.033\">https://doi.org/10.1016/j.jtbi.2005.08.033</a>."},"extern":1,"quality_controlled":0,"author":[{"id":"44FDEF62-F248-11E8-B48F-1D18A9856A87","last_name":"Kondrashov","first_name":"Fyodor","full_name":"Fyodor Kondrashov","orcid":"0000-0001-8243-4694"},{"last_name":"Kondrashov","full_name":"Kondrashov, Alexey S","first_name":"Alexey"}],"status":"public","doi":"10.1016/j.jtbi.2005.08.033","volume":239,"publication_status":"published","date_created":"2018-12-11T11:48:57Z"}]