---
_id: '4547'
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.
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.
author:
- first_name: Krishnendu
  full_name: Krishnendu Chatterjee
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Jean
  full_name: Raskin, Jean-François
  last_name: Raskin
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.
  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.
date_created: 2018-12-11T12:09:25Z
date_published: 2007-07-27T00:00:00Z
date_updated: 2021-01-12T07:59:36Z
day: '27'
doi: 10.2168/LMCS-3(3:4)2007
extern: 1
intvolume: '         3'
issue: 184
month: '07'
page: 1 - 23
publication: Logical Methods in Computer Science
publication_status: published
publisher: International Federation of Computational Logic
publist_id: '167'
quality_controlled: 0
status: public
title: Algorithms for omega-regular games with imperfect information
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
volume: 3
year: '2007'
...
---
_id: '4559'
abstract:
- lang: eng
  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.

    We 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.

    We 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.

    Finally, 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.
acknowledgement: Technical Report No. UCB/EECS-2007-122
author:
- first_name: Krishnendu
  full_name: Krishnendu Chatterjee
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
citation:
  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.
  ieee: K. Chatterjee, “Stochastic ω-Regular Games,” University of California, Berkeley,
    2007.
  ista: Chatterjee K. 2007. Stochastic ω-Regular Games. University of California,
    Berkeley.
  mla: Chatterjee, Krishnendu. <i>Stochastic ω-Regular Games</i>. University of California,
    Berkeley, 2007, pp. 1–247.
  short: K. Chatterjee, Stochastic ω-Regular Games, University of California, Berkeley,
    2007.
date_created: 2018-12-11T12:09:29Z
date_published: 2007-10-08T00:00:00Z
date_updated: 2021-01-12T07:59:42Z
day: '08'
extern: 1
main_file_link:
- open_access: '0'
  url: http://chess.eecs.berkeley.edu/pubs/462.html
month: '10'
page: 1 - 247
publication_status: published
publisher: University of California, Berkeley
publist_id: '150'
quality_controlled: 0
status: public
title: Stochastic ω-Regular Games
type: dissertation
year: '2007'
...
---
_id: '4566'
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."
article_processing_charge: No
author:
- first_name: Arindam
  full_name: Chakrabarti, Arindam
  last_name: Chakrabarti
citation:
  ama: Chakrabarti A. A framework for compositional design and analysis of systems.
    2007:1-244.
  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.
  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.
  mla: Chakrabarti, Arindam. <i>A Framework for Compositional Design and Analysis
    of Systems</i>. University of California, Berkeley, 2007, pp. 1–244.
  short: A. Chakrabarti, A Framework for Compositional Design and Analysis of Systems,
    University of California, Berkeley, 2007.
date_created: 2018-12-11T12:09:31Z
date_published: 2007-12-20T00:00:00Z
date_updated: 2021-01-12T07:59:45Z
day: '20'
extern: '1'
language:
- iso: eng
month: '12'
oa_version: None
page: 1 - 244
publication_status: published
publisher: University of California, Berkeley
publist_id: '145'
status: public
supervisor:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
- first_name: George
  full_name: Necula, George
  last_name: Necula
- first_name: Edward
  full_name: Lee, Edward
  last_name: Lee
- first_name: Jack
  full_name: Silver, Jack
  last_name: Silver
title: A framework for compositional design and analysis of systems
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2007'
...
---
_id: '4567'
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.
author:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ranjit
  full_name: Jhala, Ranjit
  last_name: Jhala
- first_name: Ritankar
  full_name: Majumdar, Ritankar S
  last_name: Majumdar
citation:
  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>'
  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>'
  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>.'
  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.'
  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>.'
  short: D. Beyer, T.A. Henzinger, R. Jhala, R. Majumdar, International Journal on
    Software Tools for Technology Transfer 9 (2007) 505–525.
date_created: 2018-12-11T12:09:31Z
date_published: 2007-10-01T00:00:00Z
date_updated: 2021-01-12T07:59:45Z
day: '01'
doi: 10.1007/s10009-007-0044-z
extern: 1
intvolume: '         9'
issue: '5'
month: '10'
page: 505 - 525
publication: International Journal on Software Tools for Technology Transfer
publication_status: published
publisher: Springer
publist_id: '139'
quality_controlled: 0
status: public
title: 'The software model checker BLAST: Applications to software engineering'
type: journal_article
volume: 9
year: '2007'
...
---
_id: '4570'
abstract:
- lang: eng
  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.
acknowledgement: This research was supported in part by the NSF grant CCR-0225610
  and by the Swiss National Science Foundation.
alternative_title:
- LNCS
author:
- first_name: Thomas
  full_name: Brihaye, Thomas
  last_name: Brihaye
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Vinayak
  full_name: Prabhu, Vinayak S
  last_name: Prabhu
- first_name: Jean
  full_name: Raskin, Jean-François
  last_name: Raskin
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.
conference:
  name: 'ICALP: Automata, Languages and Programming'
date_created: 2018-12-11T12:09:32Z
date_published: 2007-06-29T00:00:00Z
date_updated: 2021-01-12T07:59:47Z
day: '29'
doi: 10.1007/978-3-540-73420-8_71
extern: 1
intvolume: '      4596'
month: '06'
page: 825 - 837
publication_status: published
publisher: Springer
publist_id: '142'
quality_controlled: 0
status: public
title: Minimum-time reachability in timed games
type: conference
volume: 4596
year: '2007'
...
---
_id: '4571'
abstract:
- lang: eng
  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.
author:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ritankar
  full_name: Majumdar, Ritankar S
  last_name: Majumdar
- first_name: Andrey
  full_name: Rybalchenko, Andrey
  last_name: Rybalchenko
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.
conference:
  name: 'PLDI: Programming Languages Design and Implementation'
date_created: 2018-12-11T12:09:32Z
date_published: 2007-06-01T00:00:00Z
date_updated: 2021-01-12T07:59:48Z
day: '01'
doi: 10.1145/1250734.1250769
extern: 1
month: '06'
page: 300 - 309
publication_status: published
publisher: ACM
publist_id: '137'
quality_controlled: 0
status: public
title: Path invariants
type: conference
year: '2007'
...
---
_id: '4572'
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.
acknowledgement: This research was sponsored in part by the grants NSF-CCF-0427202
  and NSF-CCF-0546170.
alternative_title:
- LNCS
author:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ritankar
  full_name: Majumdar, Ritankar S
  last_name: Majumdar
- first_name: Andrey
  full_name: Rybalchenko, Andrey
  last_name: Rybalchenko
citation:
  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>'
  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>'
  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>.
  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.'
  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>.
  short: D. Beyer, T.A. Henzinger, R. Majumdar, A. Rybalchenko, in:, Springer, 2007,
    pp. 378–394.
conference:
  name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
date_created: 2018-12-11T12:09:32Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:48Z
day: '01'
doi: 10.1007/978-3-540-69738-1_27
extern: 1
intvolume: '      4349'
month: '01'
page: 378 - 394
publication_status: published
publisher: Springer
publist_id: '138'
quality_controlled: 0
status: public
title: Invariant synthesis for combined theories
type: conference
volume: 4349
year: '2007'
...
---
_id: '4573'
abstract:
- lang: eng
  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.
acknowledgement: This research was supported in part by the grant SFU/PRG 06-3, and
  by the Swiss National Science Foundation.
alternative_title:
- LNCS
author:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Grégory
  full_name: Théoduloz, Grégory
  last_name: Théoduloz
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>'
  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>.'
  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.'
  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.
conference:
  name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:09:33Z
date_published: 2007-07-02T00:00:00Z
date_updated: 2021-01-12T07:59:48Z
day: '02'
doi: 10.1007/978-3-540-73368-3_51
extern: 1
intvolume: '      4590'
month: '07'
page: 504 - 518
publication_status: published
publisher: Springer
publist_id: '135'
quality_controlled: 0
status: public
title: 'Configurable software verification: Concretizing the convergence of model
  checking and program analysis'
type: conference
volume: 4590
year: '2007'
...
---
_id: '4575'
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.'
acknowledgement: This research was supported in part by the NSF grant CCR-0225610
  and by the Swiss National Science Foundation.
author:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- first_name: Arindam
  full_name: Chakrabarti, Arindam
  last_name: Chakrabarti
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Sanjit
  full_name: Seshia, Sanjit A
  last_name: Seshia
citation:
  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>'
  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>'
  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>.
  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.'
  ista: 'Beyer D, Chakrabarti A, Henzinger TA, Seshia S. 2007. An application of web-service
    interfaces. ICWS: International Conference on Web Service, 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>.
  short: D. Beyer, A. Chakrabarti, T.A. Henzinger, S. Seshia, in:, IEEE, 2007, pp.
    831–838.
conference:
  name: 'ICWS: International Conference on Web Service'
date_created: 2018-12-11T12:09:33Z
date_published: 2007-07-30T00:00:00Z
date_updated: 2021-01-12T07:59:49Z
day: '30'
doi: '10.1109/ICWS.2007.32 '
extern: 1
month: '07'
page: 831 - 838
publication_status: published
publisher: IEEE
publist_id: '134'
quality_controlled: 0
status: public
title: An application of web-service interfaces
type: conference
year: '2007'
...
---
_id: '4626'
abstract:
- lang: eng
  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.'
author:
- first_name: Luca
  full_name: de Alfaro, Luca
  last_name: De Alfaro
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Orna
  full_name: Kupferman, Orna
  last_name: Kupferman
citation:
  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>
  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>.
  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.
  ista: De Alfaro L, Henzinger TA, Kupferman O. 2007. Concurrent reachability games.
    Theoretical Computer Science. 386(3), 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>.
  short: L. De Alfaro, T.A. Henzinger, O. Kupferman, Theoretical Computer Science
    386 (2007) 188–217.
date_created: 2018-12-11T12:09:49Z
date_published: 2007-11-01T00:00:00Z
date_updated: 2021-01-12T08:00:37Z
day: '01'
doi: 10.1016/j.tcs.2007.07.008
extern: 1
intvolume: '       386'
issue: '3'
month: '11'
page: 188 - 217
publication: Theoretical Computer Science
publication_status: published
publisher: Elsevier
publist_id: '81'
quality_controlled: 0
status: public
title: Concurrent reachability games
type: journal_article
volume: 386
year: '2007'
...
---
_id: '8488'
abstract:
- lang: eng
  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.
article_processing_charge: No
article_type: original
author:
- first_name: Paul
  full_name: Schanda, Paul
  id: 7B541462-FAF6-11E9-A490-E8DFE5697425
  last_name: Schanda
  orcid: 0000-0002-9350-7606
- first_name: Hélène
  full_name: Van Melckebeke, Hélène
  last_name: Van Melckebeke
- first_name: Bernhard
  full_name: Brutscher, Bernhard
  last_name: Brutscher
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>.
  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.
  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.
  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>.
  short: P. Schanda, H. Van Melckebeke, B. Brutscher, Journal of the American Chemical
    Society 128 (2006) 9042–9043.
date_created: 2020-09-18T10:13:36Z
date_published: 2006-06-21T00:00:00Z
date_updated: 2021-01-12T08:19:37Z
day: '21'
doi: 10.1021/ja062025p
extern: '1'
intvolume: '       128'
issue: '28'
keyword:
- Colloid and Surface Chemistry
- Biochemistry
- General Chemistry
- Catalysis
language:
- iso: eng
month: '06'
oa_version: None
page: 9042-9043
publication: Journal of the American Chemical Society
publication_identifier:
  issn:
  - 0002-7863
  - 1520-5126
publication_status: published
publisher: American Chemical Society
quality_controlled: '1'
status: public
title: Speeding up three-dimensional protein NMR experiments to a few minutes
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 128
year: '2006'
...
---
_id: '8489'
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.
article_processing_charge: No
article_type: original
author:
- first_name: Paul
  full_name: Schanda, Paul
  id: 7B541462-FAF6-11E9-A490-E8DFE5697425
  last_name: Schanda
  orcid: 0000-0002-9350-7606
- first_name: Vincent
  full_name: Forge, Vincent
  last_name: Forge
- first_name: Bernhard
  full_name: Brutscher, Bernhard
  last_name: Brutscher
citation:
  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>
  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>
  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>.
  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.
  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.
  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>.
  short: P. Schanda, V. Forge, B. Brutscher, Magnetic Resonance in Chemistry 44 (2006)
    S177–S184.
date_created: 2020-09-18T10:13:42Z
date_published: 2006-07-06T00:00:00Z
date_updated: 2021-01-12T08:19:37Z
day: '06'
doi: 10.1002/mrc.1825
extern: '1'
intvolume: '        44'
issue: S1
language:
- iso: eng
month: '07'
oa_version: None
page: S177-S184
publication: Magnetic Resonance in Chemistry
publication_identifier:
  issn:
  - 0749-1581
  - 1097-458X
publication_status: published
publisher: Wiley
quality_controlled: '1'
status: public
title: HET-SOFAST NMR for fast detection of structural compactness and heterogeneity
  along polypeptide chains
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 44
year: '2006'
...
---
_id: '8490'
abstract:
- lang: eng
  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.
article_processing_charge: No
article_type: original
author:
- first_name: Paul
  full_name: Schanda, Paul
  id: 7B541462-FAF6-11E9-A490-E8DFE5697425
  last_name: Schanda
  orcid: 0000-0002-9350-7606
- first_name: Bernhard
  full_name: Brutscher, Bernhard
  last_name: Brutscher
citation:
  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>
  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>.
  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.
  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.
date_created: 2020-09-18T10:13:51Z
date_published: 2006-02-01T00:00:00Z
date_updated: 2021-01-12T08:19:38Z
day: '01'
doi: 10.1016/j.jmr.2005.10.007
extern: '1'
intvolume: '       178'
issue: '2'
keyword:
- Nuclear and High Energy Physics
- Biophysics
- Biochemistry
- Condensed Matter Physics
language:
- iso: eng
month: '02'
oa_version: None
page: 334-339
publication: Journal of Magnetic Resonance
publication_identifier:
  issn:
  - 1090-7807
publication_status: published
publisher: Elsevier
status: public
title: Hadamard frequency-encoded SOFAST-HMQC for ultrafast two-dimensional protein
  NMR
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 178
year: '2006'
...
---
_id: '8513'
article_processing_charge: No
article_type: original
author:
- first_name: Vadim
  full_name: Kaloshin, Vadim
  id: FE553552-CDE8-11E9-B324-C0EBE5697425
  last_name: Kaloshin
  orcid: 0000-0002-6051-2628
- first_name: Maria
  full_name: Saprykina, Maria
  last_name: Saprykina
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>
  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>
  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>.
  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.
  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.
  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.
date_created: 2020-09-18T10:48:43Z
date_published: 2006-05-01T00:00:00Z
date_updated: 2021-01-12T08:19:48Z
day: '01'
doi: 10.3934/dcds.2006.15.611
extern: '1'
intvolume: '        15'
issue: '2'
language:
- iso: eng
month: '05'
oa_version: None
page: 611-640
publication: Discrete & Continuous Dynamical Systems - A
publication_identifier:
  issn:
  - 1553-5231
publication_status: published
publisher: American Institute of Mathematical Sciences (AIMS)
quality_controlled: '1'
status: public
title: Generic 3-dimensional volume-preserving diffeomorphisms with superexponential
  growth of number of periodic orbits
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15
year: '2006'
...
---
_id: '8514'
abstract:
- lang: eng
  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$.
article_processing_charge: No
article_type: original
author:
- first_name: WILLIAM
  full_name: OTT, WILLIAM
  last_name: OTT
- first_name: BRIAN
  full_name: HUNT, BRIAN
  last_name: HUNT
- first_name: Vadim
  full_name: Kaloshin, Vadim
  id: FE553552-CDE8-11E9-B324-C0EBE5697425
  last_name: Kaloshin
  orcid: 0000-0002-6051-2628
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>.
  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.
  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.
  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.
date_created: 2020-09-18T10:48:52Z
date_published: 2006-06-01T00:00:00Z
date_updated: 2021-01-12T08:19:48Z
day: '01'
doi: 10.1017/s0143385705000714
extern: '1'
intvolume: '        26'
issue: '3'
language:
- iso: eng
month: '06'
oa_version: None
page: 869-891
publication: Ergodic Theory and Dynamical Systems
publication_identifier:
  issn:
  - 0143-3857
  - 1469-4417
publication_status: published
publisher: Cambridge University Press
quality_controlled: '1'
status: public
title: The effect of projections on fractal sets and measures in Banach spaces
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 26
year: '2006'
...
---
_id: '8515'
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."
article_processing_charge: No
author:
- first_name: Vadim
  full_name: Kaloshin, Vadim
  id: FE553552-CDE8-11E9-B324-C0EBE5697425
  last_name: Kaloshin
  orcid: 0000-0002-6051-2628
- first_name: D.
  full_name: DOLGOPYAT, D.
  last_name: DOLGOPYAT
- first_name: L.
  full_name: KORALOV, L.
  last_name: KORALOV
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>'
  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>'
  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>.
  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.
  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>.
  short: V. Kaloshin, D. DOLGOPYAT, L. KORALOV, in:, XIVth International Congress
    on Mathematical Physics, World Scientific, 2006, pp. 290–295.
conference:
  end_date: 2003-08-02
  location: Lisbon, Portugal
  name: International Congress on Mathematical Physics
  start_date: 2003-07-28
date_created: 2020-09-18T10:48:59Z
date_published: 2006-03-01T00:00:00Z
date_updated: 2021-01-12T08:19:49Z
day: '01'
doi: 10.1142/9789812704016_0026
extern: '1'
language:
- iso: eng
month: '03'
oa_version: None
page: 290-295
publication: XIVth International Congress on Mathematical Physics
publication_identifier:
  isbn:
  - '9789812562012'
  - '9789812704016'
publication_status: published
publisher: World Scientific
quality_controlled: '1'
status: public
title: Long time behaviour of periodic stochastic flows
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2006'
...
---
_id: '854'
abstract:
- lang: eng
  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.
acknowledgement: |-
  FAK is supported by the NSF Graduate Research Fellowship.
  We 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.
author:
- first_name: Evgeny
  full_name: Rogaev, Evgeny I
  last_name: Rogaev
- first_name: Yuri
  full_name: Moliaka, Yuri K
  last_name: Moliaka
- first_name: Boris
  full_name: Malyarchuk, Boris A
  last_name: Malyarchuk
- first_name: Fyodor
  full_name: Fyodor Kondrashov
  id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
  last_name: Kondrashov
  orcid: 0000-0001-8243-4694
- first_name: Miroslava
  full_name: Derenko, Miroslava V
  last_name: Derenko
- first_name: Ilya
  full_name: Chumakov, Ilya M
  last_name: Chumakov
- first_name: Anastasia
  full_name: Grigorenko, Anastasia P
  last_name: Grigorenko
citation:
  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>
  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>.
  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.
  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>.
  short: E. Rogaev, Y. Moliaka, B. Malyarchuk, F. Kondrashov, M. Derenko, I. Chumakov,
    A. Grigorenko, PLoS Biology 4 (2006) 0403–0410.
date_created: 2018-12-11T11:48:51Z
date_published: 2006-03-01T00:00:00Z
date_updated: 2021-01-12T08:19:58Z
day: '01'
doi: 10.1371/journal.pbio.0040073
extern: 1
intvolume: '         4'
issue: '3'
month: '03'
page: 0403 - 0410
publication: PLoS Biology
publication_status: published
publisher: Public Library of Science
publist_id: '6794'
quality_controlled: 0
status: public
title: Complete mitochondrial genome and phylogeny of pleistocene mammoth Mammuthus
  primigenius
type: journal_article
volume: 4
year: '2006'
...
---
_id: '868'
abstract:
- lang: eng
  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.'
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.
author:
- first_name: Fyodor
  full_name: Fyodor Kondrashov
  id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
  last_name: Kondrashov
  orcid: 0000-0001-8243-4694
- first_name: Eugene
  full_name: Koonin, Eugene V
  last_name: Koonin
- first_name: Igor
  full_name: Morgunov, Igor G
  last_name: Morgunov
- first_name: Tatiana
  full_name: Finogenova, Tatiana V
  last_name: Finogenova
- first_name: Marie
  full_name: Kondrashova, Marie N
  last_name: Kondrashova
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>.
  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.
  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.
  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>.
  short: F. Kondrashov, E. Koonin, I. Morgunov, T. Finogenova, M. Kondrashova, Biology
    Direct 1 (2006).
date_created: 2018-12-11T11:48:56Z
date_published: 2006-10-23T00:00:00Z
date_updated: 2021-01-12T08:20:31Z
day: '23'
doi: 10.1186/1745-6150-1-31
extern: 1
intvolume: '         1'
month: '10'
publication: Biology Direct
publication_status: published
publisher: BioMed Central
publist_id: '6778'
quality_controlled: 0
status: public
title: Evolution of glyoxylate cycle enzymes in Metazoa Evidence of multiple horizontal
  transfer events and pseudogene formation
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
volume: 1
year: '2006'
...
---
_id: '869'
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.
acknowledgement: This research was supported in part by the Intramural Research Program
  of the NIH, National Library of Medicine.
author:
- first_name: Fyodor
  full_name: Fyodor Kondrashov
  id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
  last_name: Kondrashov
  orcid: 0000-0001-8243-4694
- first_name: Aleksey
  full_name: Ogurtsov, Aleksey Yu
  last_name: Ogurtsov
- first_name: Alexey
  full_name: Kondrashov, Alexey S
  last_name: Kondrashov
citation:
  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>
  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>.
  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.
  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.
  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.
date_created: 2018-12-11T11:48:56Z
date_published: 2006-06-21T00:00:00Z
date_updated: 2021-01-12T08:20:33Z
day: '21'
doi: 10.1016/j.jtbi.2005.10.020
extern: 1
intvolume: '       240'
issue: '4'
month: '06'
page: 616 - 626
publication: Journal of Theoretical Biology
publication_status: published
publisher: Elsevier
publist_id: '6779'
quality_controlled: 0
status: public
title: Selection in favor of nucleotides G and C diversifies evolution rates and levels
  of polymorphism at mammalian synonymous sites
type: journal_article
volume: 240
year: '2006'
...
---
_id: '873'
abstract:
- lang: eng
  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.
author:
- first_name: Fyodor
  full_name: Fyodor Kondrashov
  id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
  last_name: Kondrashov
  orcid: 0000-0001-8243-4694
- first_name: Alexey
  full_name: Kondrashov, Alexey S
  last_name: Kondrashov
citation:
  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>.
  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.
date_created: 2018-12-11T11:48:57Z
date_published: 2006-03-21T00:00:00Z
date_updated: 2021-01-12T08:20:47Z
day: '21'
doi: 10.1016/j.jtbi.2005.08.033
extern: 1
intvolume: '       239'
issue: '2'
month: '03'
page: 141 - 151
publication: Journal of Theoretical Biology
publication_status: published
publisher: Elsevier
publist_id: '6773'
quality_controlled: 0
status: public
title: Role of selection in fixation of gene duplications
type: journal_article
volume: 239
year: '2006'
...
