---
_id: '2048'
abstract:
- lang: eng
  text: Leakage resilient cryptography attempts to incorporate side-channel leakage
    into the black-box security model and designs cryptographic schemes that are provably
    secure within it. Informally, a scheme is leakage-resilient if it remains secure
    even if an adversary learns a bounded amount of arbitrary information about the
    schemes internal state. Unfortunately, most leakage resilient schemes are unnecessarily
    complicated in order to achieve strong provable security guarantees. As advocated
    by Yu et al. [CCS’10], this mostly is an artefact of the security proof and in
    practice much simpler construction may already suffice to protect against realistic
    side-channel attacks. In this paper, we show that indeed for simpler constructions
    leakage-resilience can be obtained when we aim for relaxed security notions where
    the leakage-functions and/or the inputs to the primitive are chosen non-adaptively.
    For example, we show that a three round Feistel network instantiated with a leakage
    resilient PRF yields a leakage resilient PRP if the inputs are chosen non-adaptively
    (This complements the result of Dodis and Pietrzak [CRYPTO’10] who show that if
    a adaptive queries are allowed, a superlogarithmic number of rounds is necessary.)
    We also show that a minor variation of the classical GGM construction gives a
    leakage resilient PRF if both, the leakage-function and the inputs, are chosen
    non-adaptively.
acknowledgement: "Sebastian Faust acknowledges support from the Danish National Research
  Foundation and The National Science Foundation of China (under the grant 61061130540)
  for the Sino-Danish Center for the Theory of Interactive Computation, within part
  of this work was performed; and from the CFEM research center, supported by the
  Danish Strategic Research Council. \r\nSupported by the European Research Council/ERC
  Starting Grant 259668-PSPC.\r\n"
alternative_title:
- LNCS
author:
- first_name: Sebastian
  full_name: Faust, Sebastian
  last_name: Faust
- first_name: Krzysztof Z
  full_name: Pietrzak, Krzysztof Z
  id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
  last_name: Pietrzak
  orcid: 0000-0002-9139-1654
- first_name: Joachim
  full_name: Schipper, Joachim
  id: 7BE863D4-E9CF-11E9-9EDB-90527418172C
  last_name: Schipper
citation:
  ama: 'Faust S, Pietrzak KZ, Schipper J. Practical leakage-resilient symmetric cryptography.
    In: <i> Conference Proceedings CHES 2012</i>. Vol 7428. Springer; 2012:213-232.
    doi:<a href="https://doi.org/10.1007/978-3-642-33027-8_13">10.1007/978-3-642-33027-8_13</a>'
  apa: 'Faust, S., Pietrzak, K. Z., &#38; Schipper, J. (2012). Practical leakage-resilient
    symmetric cryptography. In <i> Conference proceedings CHES 2012</i> (Vol. 7428,
    pp. 213–232). Leuven, Belgium: Springer. <a href="https://doi.org/10.1007/978-3-642-33027-8_13">https://doi.org/10.1007/978-3-642-33027-8_13</a>'
  chicago: Faust, Sebastian, Krzysztof Z Pietrzak, and Joachim Schipper. “Practical
    Leakage-Resilient Symmetric Cryptography.” In <i> Conference Proceedings CHES
    2012</i>, 7428:213–32. Springer, 2012. <a href="https://doi.org/10.1007/978-3-642-33027-8_13">https://doi.org/10.1007/978-3-642-33027-8_13</a>.
  ieee: S. Faust, K. Z. Pietrzak, and J. Schipper, “Practical leakage-resilient symmetric
    cryptography,” in <i> Conference proceedings CHES 2012</i>, Leuven, Belgium, 2012,
    vol. 7428, pp. 213–232.
  ista: 'Faust S, Pietrzak KZ, Schipper J. 2012. Practical leakage-resilient symmetric
    cryptography.  Conference proceedings CHES 2012. CHES: Cryptographic Hardware
    and Embedded Systems, LNCS, vol. 7428, 213–232.'
  mla: Faust, Sebastian, et al. “Practical Leakage-Resilient Symmetric Cryptography.”
    <i> Conference Proceedings CHES 2012</i>, vol. 7428, Springer, 2012, pp. 213–32,
    doi:<a href="https://doi.org/10.1007/978-3-642-33027-8_13">10.1007/978-3-642-33027-8_13</a>.
  short: S. Faust, K.Z. Pietrzak, J. Schipper, in:,  Conference Proceedings CHES 2012,
    Springer, 2012, pp. 213–232.
conference:
  end_date: 2012-09-12
  location: Leuven, Belgium
  name: 'CHES: Cryptographic Hardware and Embedded Systems'
  start_date: 2012-09-09
date_created: 2018-12-11T11:55:25Z
date_published: 2012-09-01T00:00:00Z
date_updated: 2021-01-12T06:54:58Z
day: '01'
department:
- _id: KrPi
doi: 10.1007/978-3-642-33027-8_13
ec_funded: 1
intvolume: '      7428'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://www.iacr.org/archive/ches2012/74280211/74280211.pdf
month: '09'
oa: 1
oa_version: Preprint
page: 213 - 232
project:
- _id: 258C570E-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '259668'
  name: Provable Security for Physical Cryptography
publication: ' Conference proceedings CHES 2012'
publication_status: published
publisher: Springer
publist_id: '5003'
quality_controlled: '1'
scopus_import: 1
status: public
title: Practical leakage-resilient symmetric cryptography
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7428
year: '2012'
...
---
_id: '2049'
abstract:
- lang: eng
  text: "We propose a new authentication protocol that is provably secure based on
    a ring variant of the learning parity with noise (LPN) problem. The protocol follows
    the design principle of the LPN-based protocol from Eurocrypt’11 (Kiltz et al.),
    and like it, is a two round protocol secure against active attacks. Moreover,
    our protocol has small communication complexity and a very small footprint which
    makes it applicable in scenarios that involve low-cost, resource-constrained devices.\r\n\r\nPerformance-wise,
    our protocol is more efficient than previous LPN-based schemes, such as the many
    variants of the Hopper-Blum (HB) protocol and the aforementioned protocol from
    Eurocrypt’11. Our implementation results show that it is even comparable to the
    standard challenge-and-response protocols based on the AES block-cipher. Our basic
    protocol is roughly 20 times slower than AES, but with the advantage of having
    10 times smaller code size. Furthermore, if a few hundred bytes of non-volatile
    memory are available to allow the storage of some off-line pre-computations, then
    the online phase of our protocols is only twice as slow as AES.\r\n"
acknowledgement: "Supported by the European Research Council / ERC Starting Grant
  (259668- PSPC)\r\nWe would like to thank the anonymous referees of this confer-
  ence and those of the ECRYPT Workshop on Lightweight Cryptography for very useful
  comments, and in particular for the suggestion that the scheme is somewhat vulnerable
  to a man-in-the-middle attack whenever an adversary observes two reader challenges
  that are the same. We hope that the attack we described in Appendix A corresponds
  to what the reviewer had in mind. We also thank Tanja Lange for pointing us to the
  pa- per of [Kir11] and for discussions of some of her recent work. "
alternative_title:
- LNCS
author:
- first_name: Stefan
  full_name: Heyse, Stefan
  last_name: Heyse
- first_name: Eike
  full_name: Kiltz, Eike
  last_name: Kiltz
- first_name: Vadim
  full_name: Lyubashevsky, Vadim
  last_name: Lyubashevsky
- first_name: Christof
  full_name: Paar, Christof
  last_name: Paar
- first_name: Krzysztof Z
  full_name: Pietrzak, Krzysztof Z
  id: 3E04A7AA-F248-11E8-B48F-1D18A9856A87
  last_name: Pietrzak
  orcid: 0000-0002-9139-1654
citation:
  ama: 'Heyse S, Kiltz E, Lyubashevsky V, Paar C, Pietrzak KZ. Lapin: An efficient
    authentication protocol based on ring-LPN. In: <i> Conference Proceedings FSE
    2012</i>. Vol 7549. Springer; 2012:346-365. doi:<a href="https://doi.org/10.1007/978-3-642-34047-5_20">10.1007/978-3-642-34047-5_20</a>'
  apa: 'Heyse, S., Kiltz, E., Lyubashevsky, V., Paar, C., &#38; Pietrzak, K. Z. (2012).
    Lapin: An efficient authentication protocol based on ring-LPN. In <i> Conference
    proceedings FSE 2012</i> (Vol. 7549, pp. 346–365). Washington, DC, USA: Springer.
    <a href="https://doi.org/10.1007/978-3-642-34047-5_20">https://doi.org/10.1007/978-3-642-34047-5_20</a>'
  chicago: 'Heyse, Stefan, Eike Kiltz, Vadim Lyubashevsky, Christof Paar, and Krzysztof
    Z Pietrzak. “Lapin: An Efficient Authentication Protocol Based on Ring-LPN.” In
    <i> Conference Proceedings FSE 2012</i>, 7549:346–65. Springer, 2012. <a href="https://doi.org/10.1007/978-3-642-34047-5_20">https://doi.org/10.1007/978-3-642-34047-5_20</a>.'
  ieee: 'S. Heyse, E. Kiltz, V. Lyubashevsky, C. Paar, and K. Z. Pietrzak, “Lapin:
    An efficient authentication protocol based on ring-LPN,” in <i> Conference proceedings
    FSE 2012</i>, Washington, DC, USA, 2012, vol. 7549, pp. 346–365.'
  ista: 'Heyse S, Kiltz E, Lyubashevsky V, Paar C, Pietrzak KZ. 2012. Lapin: An efficient
    authentication protocol based on ring-LPN.  Conference proceedings FSE 2012. FSE:
    Fast Software Encryption, LNCS, vol. 7549, 346–365.'
  mla: 'Heyse, Stefan, et al. “Lapin: An Efficient Authentication Protocol Based on
    Ring-LPN.” <i> Conference Proceedings FSE 2012</i>, vol. 7549, Springer, 2012,
    pp. 346–65, doi:<a href="https://doi.org/10.1007/978-3-642-34047-5_20">10.1007/978-3-642-34047-5_20</a>.'
  short: S. Heyse, E. Kiltz, V. Lyubashevsky, C. Paar, K.Z. Pietrzak, in:,  Conference
    Proceedings FSE 2012, Springer, 2012, pp. 346–365.
conference:
  end_date: 2012-03-21
  location: Washington, DC, USA
  name: 'FSE: Fast Software Encryption'
  start_date: 2012-03-19
date_created: 2018-12-11T11:55:25Z
date_published: 2012-03-01T00:00:00Z
date_updated: 2021-01-12T06:54:58Z
day: '01'
department:
- _id: KrPi
doi: 10.1007/978-3-642-34047-5_20
ec_funded: 1
intvolume: '      7549'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://www.iacr.org/archive/fse2012/75490350/75490350.pdf
month: '03'
oa: 1
oa_version: Preprint
page: 346 - 365
project:
- _id: 258C570E-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '259668'
  name: Provable Security for Physical Cryptography
publication: ' Conference proceedings FSE 2012'
publication_status: published
publisher: Springer
publist_id: '5002'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Lapin: An efficient authentication protocol based on ring-LPN'
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7549
year: '2012'
...
---
_id: '1384'
abstract:
- lang: eng
  text: 'Software model checking, as an undecidable problem, has three possible outcomes:
    (1) the program satisfies the specification, (2) the program does not satisfy
    the specification, and (3) the model checker fails. The third outcome usually
    manifests itself in a space-out, time-out, or one component of the verification
    tool giving up; in all of these failing cases, significant computation is performed
    by the verification tool before the failure, but no result is reported. We propose
    to reformulate the model-checking problem as follows, in order to have the verification
    tool report a summary of the performed work even in case of failure: given a program
    and a specification, the model checker returns a condition Ψ - usually a state
    predicate - such that the program satisfies the specification under the condition
    Ψ - that is, as long as the program does not leave the states in which Ψ is satisfied.
    In our experiments, we investigated as one major application of conditional model
    checking the sequential combination of model checkers with information passing.
    We give the condition that one model checker produces, as input to a second conditional
    model checker, such that the verification problem for the second is restricted
    to the part of the state space that is not covered by the condition, i.e., the
    second model checker works on the problems that the first model checker could
    not solve. Our experiments demonstrate that repeated application of conditional
    model checkers, passing information from one model checker to the next, can significantly
    improve the verification results and performance, i.e., we can now verify programs
    that we could not verify before.'
acknowledgement: This  research  was  supported  by  the  Canadian  NSERC grant   RGPIN   341819-07,    the   ERC   Advanced   Grant
  QUAREM, and the Austrian Science Fund NFN RiSE.
article_number: '57'
author:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- 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: Mehmet
  full_name: Keremoglu, Mehmet
  last_name: Keremoglu
- first_name: Philipp
  full_name: Wendler, Philipp
  last_name: Wendler
citation:
  ama: 'Beyer D, Henzinger TA, Keremoglu M, Wendler P. Conditional model checking:
    A technique to pass information between verifiers. In: <i>Proceedings of the ACM
    SIGSOFT 20th International Symposium on the Foundations of Software Engineering</i>.
    ACM; 2012. doi:<a href="https://doi.org/10.1145/2393596.2393664">10.1145/2393596.2393664</a>'
  apa: 'Beyer, D., Henzinger, T. A., Keremoglu, M., &#38; Wendler, P. (2012). Conditional
    model checking: A technique to pass information between verifiers. In <i>Proceedings
    of the ACM SIGSOFT 20th International Symposium on the Foundations of Software
    Engineering</i>. Cary, NC, USA: ACM. <a href="https://doi.org/10.1145/2393596.2393664">https://doi.org/10.1145/2393596.2393664</a>'
  chicago: 'Beyer, Dirk, Thomas A Henzinger, Mehmet Keremoglu, and Philipp Wendler.
    “Conditional Model Checking: A Technique to Pass Information between Verifiers.”
    In <i>Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations
    of Software Engineering</i>. ACM, 2012. <a href="https://doi.org/10.1145/2393596.2393664">https://doi.org/10.1145/2393596.2393664</a>.'
  ieee: 'D. Beyer, T. A. Henzinger, M. Keremoglu, and P. Wendler, “Conditional model
    checking: A technique to pass information between verifiers,” in <i>Proceedings
    of the ACM SIGSOFT 20th International Symposium on the Foundations of Software
    Engineering</i>, Cary, NC, USA, 2012.'
  ista: 'Beyer D, Henzinger TA, Keremoglu M, Wendler P. 2012. Conditional model checking:
    A technique to pass information between verifiers. Proceedings of the ACM SIGSOFT
    20th International Symposium on the Foundations of Software Engineering. FSE:
    Foundations of Software Engineering, 57.'
  mla: 'Beyer, Dirk, et al. “Conditional Model Checking: A Technique to Pass Information
    between Verifiers.” <i>Proceedings of the ACM SIGSOFT 20th International Symposium
    on the Foundations of Software Engineering</i>, 57, ACM, 2012, doi:<a href="https://doi.org/10.1145/2393596.2393664">10.1145/2393596.2393664</a>.'
  short: D. Beyer, T.A. Henzinger, M. Keremoglu, P. Wendler, in:, Proceedings of the
    ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering,
    ACM, 2012.
conference:
  end_date: 2012-11-16
  location: Cary, NC, USA
  name: 'FSE: Foundations of Software Engineering'
  start_date: 2012-11-11
date_created: 2018-12-11T11:51:42Z
date_published: 2012-11-01T00:00:00Z
date_updated: 2021-01-12T06:50:18Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2393596.2393664
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1109.6926
month: '11'
oa: 1
oa_version: Preprint
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations
  of Software Engineering
publication_status: published
publisher: ACM
publist_id: '5826'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Conditional model checking: A technique to pass information between verifiers'
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2012'
...
---
_id: '5396'
abstract:
- lang: eng
  text: We consider the problem of inference in agraphical model with binary variables.
    While in theory it is arguably preferable to compute marginal probabilities, in
    practice researchers often use MAP inference due to the availability of efficient
    discrete optimization algorithms. We bridge the gap between the two approaches
    by introducing the Discrete  Marginals technique in which approximate marginals
    are obtained by minimizing an objective function with unary and pair-wise terms
    over a discretized domain. This allows the use of techniques originally devel-oped
    for MAP-MRF inference and learning. We explore two ways to set up the objective
    function - by discretizing the Bethe free energy and by learning it  from training
    data. Experimental results show that for certain types of graphs a learned function
    can out-perform the  Bethe approximation. We also establish a link between the
    Bethe free energy and submodular functions.
alternative_title:
- IST Austria Technical Report
author:
- first_name: Filip
  full_name: Korc, Filip
  id: 476A2FD6-F248-11E8-B48F-1D18A9856A87
  last_name: Korc
- first_name: Vladimir
  full_name: Kolmogorov, Vladimir
  id: 3D50B0BA-F248-11E8-B48F-1D18A9856A87
  last_name: Kolmogorov
- first_name: Christoph
  full_name: Lampert, Christoph
  id: 40C20FD2-F248-11E8-B48F-1D18A9856A87
  last_name: Lampert
  orcid: 0000-0001-8622-7887
citation:
  ama: Korc F, Kolmogorov V, Lampert C. <i>Approximating Marginals Using Discrete
    Energy Minimization</i>. IST Austria; 2012. doi:<a href="https://doi.org/10.15479/AT:IST-2012-0003">10.15479/AT:IST-2012-0003</a>
  apa: Korc, F., Kolmogorov, V., &#38; Lampert, C. (2012). <i>Approximating marginals
    using discrete energy minimization</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2012-0003">https://doi.org/10.15479/AT:IST-2012-0003</a>
  chicago: Korc, Filip, Vladimir Kolmogorov, and Christoph Lampert. <i>Approximating
    Marginals Using Discrete Energy Minimization</i>. IST Austria, 2012. <a href="https://doi.org/10.15479/AT:IST-2012-0003">https://doi.org/10.15479/AT:IST-2012-0003</a>.
  ieee: F. Korc, V. Kolmogorov, and C. Lampert, <i>Approximating marginals using discrete
    energy minimization</i>. IST Austria, 2012.
  ista: Korc F, Kolmogorov V, Lampert C. 2012. Approximating marginals using discrete
    energy minimization, IST Austria, 13p.
  mla: Korc, Filip, et al. <i>Approximating Marginals Using Discrete Energy Minimization</i>.
    IST Austria, 2012, doi:<a href="https://doi.org/10.15479/AT:IST-2012-0003">10.15479/AT:IST-2012-0003</a>.
  short: F. Korc, V. Kolmogorov, C. Lampert, Approximating Marginals Using Discrete
    Energy Minimization, IST Austria, 2012.
date_created: 2018-12-12T11:39:06Z
date_published: 2012-07-23T00:00:00Z
date_updated: 2023-02-23T11:13:22Z
day: '23'
ddc:
- '000'
department:
- _id: VlKo
- _id: ChLa
doi: 10.15479/AT:IST-2012-0003
file:
- access_level: open_access
  checksum: 7e0ba85ad123b13223aaf6cdde2d288c
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:29Z
  date_updated: 2020-07-14T12:46:44Z
  file_id: '5490'
  file_name: IST-2012-0003_IST-2012-0003.pdf
  file_size: 618744
  relation: main_file
file_date_updated: 2020-07-14T12:46:44Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '13'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '36'
related_material:
  record:
  - id: '3124'
    relation: earlier_version
    status: public
status: public
title: Approximating marginals using discrete energy minimization
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2012'
...
---
_id: '5398'
abstract:
- lang: eng
  text: This document is created as a part of the project “Repository for Research
    Data on IST Austria”. It summarises the actual state of research data at IST Austria,
    based on survey results. It supports the choice of appropriate software, which
    would best fit the requirements of their users, the researchers.
author:
- first_name: Jana
  full_name: Porsche, Jana
  id: 3252EDC2-F248-11E8-B48F-1D18A9856A87
  last_name: Porsche
citation:
  ama: Porsche J. <i>Actual State of Research Data @ ISTAustria</i>. IST Austria;
    2012.
  apa: Porsche, J. (2012). <i>Actual state of research data @ ISTAustria</i>. IST
    Austria.
  chicago: Porsche, Jana. <i>Actual State of Research Data @ ISTAustria</i>. IST Austria,
    2012.
  ieee: J. Porsche, <i>Actual state of research data @ ISTAustria</i>. IST Austria,
    2012.
  ista: Porsche J. 2012. Actual state of research data @ ISTAustria, IST Austria,p.
  mla: Porsche, Jana. <i>Actual State of Research Data @ ISTAustria</i>. IST Austria,
    2012.
  short: J. Porsche, Actual State of Research Data @ ISTAustria, IST Austria, 2012.
date_created: 2018-12-12T11:39:06Z
date_published: 2012-11-12T00:00:00Z
date_updated: 2020-07-14T23:04:49Z
day: '12'
ddc:
- '020'
department:
- _id: E-Lib
file:
- access_level: open_access
  checksum: e0a7c041eea1ca4b70ab6f9ec5177f4e
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:11Z
  date_updated: 2020-07-14T12:46:44Z
  file_id: '5472'
  file_name: IST-2012-103-v1+1_Actual_state_of_research_data_@_IST_Austria.pdf
  file_size: 238544
  relation: main_file
file_date_updated: 2020-07-14T12:46:44Z
has_accepted_license: '1'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Published Version
publication_status: published
publisher: IST Austria
pubrep_id: '103'
status: public
title: Actual state of research data @ ISTAustria
type: report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2012'
...
---
_id: '5745'
article_processing_charge: No
author:
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  last_name: Gupta
citation:
  ama: 'Gupta A. Improved Single Pass Algorithms for Resolution Proof Reduction. In:
    <i>Automated Technology for Verification and Analysis</i>. Vol 7561. LNCS. Berlin,
    Heidelberg: Springer Berlin Heidelberg; 2012:107-121. doi:<a href="https://doi.org/10.1007/978-3-642-33386-6_10">10.1007/978-3-642-33386-6_10</a>'
  apa: 'Gupta, A. (2012). Improved Single Pass Algorithms for Resolution Proof Reduction.
    In <i>Automated Technology for Verification and Analysis</i> (Vol. 7561, pp. 107–121).
    Berlin, Heidelberg: Springer Berlin Heidelberg. <a href="https://doi.org/10.1007/978-3-642-33386-6_10">https://doi.org/10.1007/978-3-642-33386-6_10</a>'
  chicago: 'Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof
    Reduction.” In <i>Automated Technology for Verification and Analysis</i>, 7561:107–21.
    LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012. <a href="https://doi.org/10.1007/978-3-642-33386-6_10">https://doi.org/10.1007/978-3-642-33386-6_10</a>.'
  ieee: 'A. Gupta, “Improved Single Pass Algorithms for Resolution Proof Reduction,”
    in <i>Automated Technology for Verification and Analysis</i>, vol. 7561, Berlin,
    Heidelberg: Springer Berlin Heidelberg, 2012, pp. 107–121.'
  ista: 'Gupta A. 2012.Improved Single Pass Algorithms for Resolution Proof Reduction.
    In: Automated Technology for Verification and Analysis. vol. 7561, 107–121.'
  mla: Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.”
    <i>Automated Technology for Verification and Analysis</i>, vol. 7561, Springer
    Berlin Heidelberg, 2012, pp. 107–21, doi:<a href="https://doi.org/10.1007/978-3-642-33386-6_10">10.1007/978-3-642-33386-6_10</a>.
  short: A. Gupta, in:, Automated Technology for Verification and Analysis, Springer
    Berlin Heidelberg, Berlin, Heidelberg, 2012, pp. 107–121.
conference:
  end_date: 2012-10-06
  location: Thiruvananthapuram, Kerala, India
  name: ATVA 2012
  start_date: 2012-10-03
date_created: 2018-12-18T13:01:46Z
date_published: 2012-01-01T00:00:00Z
date_updated: 2023-09-05T14:15:29Z
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-33386-6_10
ec_funded: 1
file:
- access_level: open_access
  checksum: 68415837a315de3cc4d120f6019d752c
  content_type: application/pdf
  creator: dernst
  date_created: 2018-12-18T13:07:35Z
  date_updated: 2020-07-14T12:47:10Z
  file_id: '5746'
  file_name: 2012_ATVA_Gupta.pdf
  file_size: 465502
  relation: main_file
file_date_updated: 2020-07-14T12:47:10Z
has_accepted_license: '1'
intvolume: '      7561'
language:
- iso: eng
oa: 1
oa_version: None
page: 107-121
place: Berlin, Heidelberg
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
publication: Automated Technology for Verification and Analysis
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783642333859'
  - '9783642333866'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Berlin Heidelberg
pubrep_id: '180'
quality_controlled: '1'
series_title: LNCS
status: public
title: Improved Single Pass Algorithms for Resolution Proof Reduction
type: book_chapter
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7561
year: '2012'
...
---
_id: '6588'
abstract:
- lang: eng
  text: First we note that the best polynomial approximation to vertical bar x vertical
    bar on the set, which consists of an interval on the positive half-axis and a
    point on the negative half-axis, can be given by means of the classical Chebyshev
    polynomials. Then we explore the cases when a solution of the related problem
    on two intervals can be given in elementary functions.
acknowledgement: "This work is supported by the Austrian Science Fund (FWF), Project
  P22025-N18.\r\n"
article_processing_charge: No
article_type: original
author:
- first_name: Florian
  full_name: Pausinger, Florian
  id: 2A77D7A2-F248-11E8-B48F-1D18A9856A87
  last_name: Pausinger
  orcid: 0000-0002-8379-3768
citation:
  ama: Pausinger F. Elementary solutions of the Bernstein problem on two intervals.
    <i>Journal of Mathematical Physics, Analysis, Geometry</i>. 2012;8(1):63-78.
  apa: Pausinger, F. (2012). Elementary solutions of the Bernstein problem on two
    intervals. <i>Journal of Mathematical Physics, Analysis, Geometry</i>. B. Verkin
    Institute for Low Temperature Physics and Engineering.
  chicago: Pausinger, Florian. “Elementary Solutions of the Bernstein Problem on Two
    Intervals.” <i>Journal of Mathematical Physics, Analysis, Geometry</i>. B. Verkin
    Institute for Low Temperature Physics and Engineering, 2012.
  ieee: F. Pausinger, “Elementary solutions of the Bernstein problem on two intervals,”
    <i>Journal of Mathematical Physics, Analysis, Geometry</i>, vol. 8, no. 1. B.
    Verkin Institute for Low Temperature Physics and Engineering, pp. 63–78, 2012.
  ista: Pausinger F. 2012. Elementary solutions of the Bernstein problem on two intervals.
    Journal of Mathematical Physics, Analysis, Geometry. 8(1), 63–78.
  mla: Pausinger, Florian. “Elementary Solutions of the Bernstein Problem on Two Intervals.”
    <i>Journal of Mathematical Physics, Analysis, Geometry</i>, vol. 8, no. 1, B.
    Verkin Institute for Low Temperature Physics and Engineering, 2012, pp. 63–78.
  short: F. Pausinger, Journal of Mathematical Physics, Analysis, Geometry 8 (2012)
    63–78.
date_created: 2019-06-27T08:16:56Z
date_published: 2012-01-01T00:00:00Z
date_updated: 2023-10-16T09:41:31Z
day: '01'
department:
- _id: HeEd
external_id:
  isi:
  - '000301173600004'
intvolume: '         8'
isi: 1
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://mi.mathnet.ru/eng/jmag525
month: '01'
oa: 1
oa_version: Published Version
page: 63-78
publication: Journal of Mathematical Physics, Analysis, Geometry
publication_identifier:
  issn:
  - 1812-9471
publication_status: published
publisher: B. Verkin Institute for Low Temperature Physics and Engineering
quality_controlled: '1'
scopus_import: '1'
status: public
title: Elementary solutions of the Bernstein problem on two intervals
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8
year: '2012'
...
---
_id: '9451'
abstract:
- lang: eng
  text: The Arabidopsis thaliana central cell, the companion cell of the egg, undergoes
    DNA demethylation before fertilization, but the targeting preferences, mechanism,
    and biological significance of this process remain unclear. Here, we show that
    active DNA demethylation mediated by the DEMETER DNA glycosylase accounts for
    all of the demethylation in the central cell and preferentially targets small,
    AT-rich, and nucleosome-depleted euchromatic transposable elements. The vegetative
    cell, the companion cell of sperm, also undergoes DEMETER-dependent demethylation
    of similar sequences, and lack of DEMETER in vegetative cells causes reduced small
    RNA–directed DNA methylation of transposons in sperm. Our results demonstrate
    that demethylation in companion cells reinforces transposon methylation in plant
    gametes and likely contributes to stable silencing of transposable elements across
    generations.
article_processing_charge: No
article_type: original
author:
- first_name: Christian A.
  full_name: Ibarra, Christian A.
  last_name: Ibarra
- first_name: Xiaoqi
  full_name: Feng, Xiaoqi
  last_name: Feng
- first_name: Vera K.
  full_name: Schoft, Vera K.
  last_name: Schoft
- first_name: Tzung-Fu
  full_name: Hsieh, Tzung-Fu
  last_name: Hsieh
- first_name: Rie
  full_name: Uzawa, Rie
  last_name: Uzawa
- first_name: Jessica A.
  full_name: Rodrigues, Jessica A.
  last_name: Rodrigues
- first_name: Assaf
  full_name: Zemach, Assaf
  last_name: Zemach
- first_name: Nina
  full_name: Chumak, Nina
  last_name: Chumak
- first_name: Adriana
  full_name: Machlicova, Adriana
  last_name: Machlicova
- first_name: Toshiro
  full_name: Nishimura, Toshiro
  last_name: Nishimura
- first_name: Denisse
  full_name: Rojas, Denisse
  last_name: Rojas
- first_name: Robert L.
  full_name: Fischer, Robert L.
  last_name: Fischer
- first_name: Hisashi
  full_name: Tamaru, Hisashi
  last_name: Tamaru
- first_name: Daniel
  full_name: Zilberman, Daniel
  id: 6973db13-dd5f-11ea-814e-b3e5455e9ed1
  last_name: Zilberman
  orcid: 0000-0002-0123-8649
citation:
  ama: Ibarra CA, Feng X, Schoft VK, et al. Active DNA demethylation in plant companion
    cells reinforces transposon methylation in gametes. <i>Science</i>. 2012;337(6100):1360-1364.
    doi:<a href="https://doi.org/10.1126/science.1224839">10.1126/science.1224839</a>
  apa: Ibarra, C. A., Feng, X., Schoft, V. K., Hsieh, T.-F., Uzawa, R., Rodrigues,
    J. A., … Zilberman, D. (2012). Active DNA demethylation in plant companion cells
    reinforces transposon methylation in gametes. <i>Science</i>. American Association
    for the Advancement of Science. <a href="https://doi.org/10.1126/science.1224839">https://doi.org/10.1126/science.1224839</a>
  chicago: Ibarra, Christian A., Xiaoqi Feng, Vera K. Schoft, Tzung-Fu Hsieh, Rie
    Uzawa, Jessica A. Rodrigues, Assaf Zemach, et al. “Active DNA Demethylation in
    Plant Companion Cells Reinforces Transposon Methylation in Gametes.” <i>Science</i>.
    American Association for the Advancement of Science, 2012. <a href="https://doi.org/10.1126/science.1224839">https://doi.org/10.1126/science.1224839</a>.
  ieee: C. A. Ibarra <i>et al.</i>, “Active DNA demethylation in plant companion cells
    reinforces transposon methylation in gametes,” <i>Science</i>, vol. 337, no. 6100.
    American Association for the Advancement of Science, pp. 1360–1364, 2012.
  ista: Ibarra CA, Feng X, Schoft VK, Hsieh T-F, Uzawa R, Rodrigues JA, Zemach A,
    Chumak N, Machlicova A, Nishimura T, Rojas D, Fischer RL, Tamaru H, Zilberman
    D. 2012. Active DNA demethylation in plant companion cells reinforces transposon
    methylation in gametes. Science. 337(6100), 1360–1364.
  mla: Ibarra, Christian A., et al. “Active DNA Demethylation in Plant Companion Cells
    Reinforces Transposon Methylation in Gametes.” <i>Science</i>, vol. 337, no. 6100,
    American Association for the Advancement of Science, 2012, pp. 1360–64, doi:<a
    href="https://doi.org/10.1126/science.1224839">10.1126/science.1224839</a>.
  short: C.A. Ibarra, X. Feng, V.K. Schoft, T.-F. Hsieh, R. Uzawa, J.A. Rodrigues,
    A. Zemach, N. Chumak, A. Machlicova, T. Nishimura, D. Rojas, R.L. Fischer, H.
    Tamaru, D. Zilberman, Science 337 (2012) 1360–1364.
date_created: 2021-06-04T07:51:31Z
date_published: 2012-09-14T00:00:00Z
date_updated: 2021-12-14T08:28:51Z
day: '14'
ddc:
- '580'
department:
- _id: DaZi
doi: 10.1126/science.1224839
extern: '1'
external_id:
  pmid:
  - '22984074'
has_accepted_license: '1'
intvolume: '       337'
issue: '6100'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC4034762/
month: '09'
oa: 1
oa_version: Published Version
page: 1360-1364
pmid: 1
publication: Science
publication_identifier:
  eissn:
  - 1095-9203
  issn:
  - 0036-8075
publication_status: published
publisher: American Association for the Advancement of Science
quality_controlled: '1'
scopus_import: '1'
status: public
title: Active DNA demethylation in plant companion cells reinforces transposon methylation
  in gametes
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 337
year: '2012'
...
---
_id: '9497'
abstract:
- lang: eng
  text: The regulation of eukaryotic chromatin relies on interactions between many
    epigenetic factors, including histone modifications, DNA methylation, and the
    incorporation of histone variants. H2A.Z, one of the most conserved but enigmatic
    histone variants that is enriched at the transcriptional start sites of genes,
    has been implicated in a variety of chromosomal processes. Recently, we reported
    a genome-wide anticorrelation between H2A.Z and DNA methylation, an epigenetic
    hallmark of heterochromatin that has also been found in the bodies of active genes
    in plants and animals. Here, we investigate the basis of this anticorrelation
    using a novel h2a.z loss-of-function line in Arabidopsis thaliana. Through genome-wide
    bisulfite sequencing, we demonstrate that loss of H2A.Z in Arabidopsis has only
    a minor effect on the level or profile of DNA methylation in genes, and we propose
    that the global anticorrelation between DNA methylation and H2A.Z is primarily
    caused by the exclusion of H2A.Z from methylated DNA. RNA sequencing and genomic
    mapping of H2A.Z show that H2A.Z enrichment across gene bodies, rather than at
    the TSS, is correlated with lower transcription levels and higher measures of
    gene responsiveness. Loss of H2A.Z causes misregulation of many genes that are
    disproportionately associated with response to environmental and developmental
    stimuli. We propose that H2A.Z deposition in gene bodies promotes variability
    in levels and patterns of gene expression, and that a major function of genic
    DNA methylation is to exclude H2A.Z from constitutively expressed genes.
article_number: e1002988
article_processing_charge: No
article_type: original
author:
- first_name: Devin
  full_name: Coleman-Derr, Devin
  last_name: Coleman-Derr
- first_name: Daniel
  full_name: Zilberman, Daniel
  id: 6973db13-dd5f-11ea-814e-b3e5455e9ed1
  last_name: Zilberman
  orcid: 0000-0002-0123-8649
citation:
  ama: Coleman-Derr D, Zilberman D. Deposition of histone variant H2A.Z within gene
    bodies regulates responsive genes. <i>PLoS Genetics</i>. 2012;8(10). doi:<a href="https://doi.org/10.1371/journal.pgen.1002988">10.1371/journal.pgen.1002988</a>
  apa: Coleman-Derr, D., &#38; Zilberman, D. (2012). Deposition of histone variant
    H2A.Z within gene bodies regulates responsive genes. <i>PLoS Genetics</i>. Public
    Library of Science. <a href="https://doi.org/10.1371/journal.pgen.1002988">https://doi.org/10.1371/journal.pgen.1002988</a>
  chicago: Coleman-Derr, Devin, and Daniel Zilberman. “Deposition of Histone Variant
    H2A.Z within Gene Bodies Regulates Responsive Genes.” <i>PLoS Genetics</i>. Public
    Library of Science, 2012. <a href="https://doi.org/10.1371/journal.pgen.1002988">https://doi.org/10.1371/journal.pgen.1002988</a>.
  ieee: D. Coleman-Derr and D. Zilberman, “Deposition of histone variant H2A.Z within
    gene bodies regulates responsive genes,” <i>PLoS Genetics</i>, vol. 8, no. 10.
    Public Library of Science, 2012.
  ista: Coleman-Derr D, Zilberman D. 2012. Deposition of histone variant H2A.Z within
    gene bodies regulates responsive genes. PLoS Genetics. 8(10), e1002988.
  mla: Coleman-Derr, Devin, and Daniel Zilberman. “Deposition of Histone Variant H2A.Z
    within Gene Bodies Regulates Responsive Genes.” <i>PLoS Genetics</i>, vol. 8,
    no. 10, e1002988, Public Library of Science, 2012, doi:<a href="https://doi.org/10.1371/journal.pgen.1002988">10.1371/journal.pgen.1002988</a>.
  short: D. Coleman-Derr, D. Zilberman, PLoS Genetics 8 (2012).
date_created: 2021-06-07T10:55:27Z
date_published: 2012-10-11T00:00:00Z
date_updated: 2021-12-14T08:29:57Z
day: '11'
department:
- _id: DaZi
doi: 10.1371/journal.pgen.1002988
extern: '1'
external_id:
  pmid:
  - '23071449'
intvolume: '         8'
issue: '10'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1371/journal.pgen.1002988
month: '10'
oa: 1
oa_version: Published Version
pmid: 1
publication: PLoS Genetics
publication_identifier:
  eissn:
  - 1553-7404
  issn:
  - 1553-7390
publication_status: published
publisher: Public Library of Science
quality_controlled: '1'
scopus_import: '1'
status: public
title: Deposition of histone variant H2A.Z within gene bodies regulates responsive
  genes
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 8
year: '2012'
...
---
_id: '9499'
abstract:
- lang: eng
  text: EMBRYONIC FLOWER1 (EMF1) is a plant-specific gene crucial to Arabidopsis vegetative
    development. Loss of function mutants in the EMF1 gene mimic the phenotype caused
    by mutations in Polycomb Group protein (PcG) genes, which encode epigenetic repressors
    that regulate many aspects of eukaryotic development. In Arabidopsis, Polycomb
    Repressor Complex 2 (PRC2), made of PcG proteins, catalyzes trimethylation of
    lysine 27 on histone H3 (H3K27me3) and PRC1-like proteins catalyze H2AK119 ubiquitination.
    Despite functional similarity to PcG proteins, EMF1 lacks sequence homology with
    known PcG proteins; thus, its role in the PcG mechanism is unclear. To study the
    EMF1 functions and its mechanism of action, we performed genome-wide mapping of
    EMF1 binding and H3K27me3 modification sites in Arabidopsis seedlings. The EMF1
    binding pattern is similar to that of H3K27me3 modification on the chromosomal
    and genic level. ChIPOTLe peak finding and clustering analyses both show that
    the highly trimethylated genes also have high enrichment levels of EMF1 binding,
    termed EMF1_K27 genes. EMF1 interacts with regulatory genes, which are silenced
    to allow vegetative growth, and with genes specifying cell fates during growth
    and differentiation. H3K27me3 marks not only these genes but also some genes that
    are involved in endosperm development and maternal effects. Transcriptome analysis,
    coupled with the H3K27me3 pattern, of EMF1_K27 genes in emf1 and PRC2 mutants
    showed that EMF1 represses gene activities via diverse mechanisms and plays a
    novel role in the PcG mechanism.
article_number: e1002512
article_processing_charge: No
article_type: original
author:
- first_name: Sang Yeol
  full_name: Kim, Sang Yeol
  last_name: Kim
- first_name: Jungeun
  full_name: Lee, Jungeun
  last_name: Lee
- first_name: Leor
  full_name: Eshed-Williams, Leor
  last_name: Eshed-Williams
- first_name: Daniel
  full_name: Zilberman, Daniel
  id: 6973db13-dd5f-11ea-814e-b3e5455e9ed1
  last_name: Zilberman
  orcid: 0000-0002-0123-8649
- first_name: Z. Renee
  full_name: Sung, Z. Renee
  last_name: Sung
citation:
  ama: Kim SY, Lee J, Eshed-Williams L, Zilberman D, Sung ZR. EMF1 and PRC2 cooperate
    to repress key regulators of Arabidopsis development. <i>PLoS Genetics</i>. 2012;8(3).
    doi:<a href="https://doi.org/10.1371/journal.pgen.1002512">10.1371/journal.pgen.1002512</a>
  apa: Kim, S. Y., Lee, J., Eshed-Williams, L., Zilberman, D., &#38; Sung, Z. R. (2012).
    EMF1 and PRC2 cooperate to repress key regulators of Arabidopsis development.
    <i>PLoS Genetics</i>. Public Library of Science. <a href="https://doi.org/10.1371/journal.pgen.1002512">https://doi.org/10.1371/journal.pgen.1002512</a>
  chicago: Kim, Sang Yeol, Jungeun Lee, Leor Eshed-Williams, Daniel Zilberman, and
    Z. Renee Sung. “EMF1 and PRC2 Cooperate to Repress Key Regulators of Arabidopsis
    Development.” <i>PLoS Genetics</i>. Public Library of Science, 2012. <a href="https://doi.org/10.1371/journal.pgen.1002512">https://doi.org/10.1371/journal.pgen.1002512</a>.
  ieee: S. Y. Kim, J. Lee, L. Eshed-Williams, D. Zilberman, and Z. R. Sung, “EMF1
    and PRC2 cooperate to repress key regulators of Arabidopsis development,” <i>PLoS
    Genetics</i>, vol. 8, no. 3. Public Library of Science, 2012.
  ista: Kim SY, Lee J, Eshed-Williams L, Zilberman D, Sung ZR. 2012. EMF1 and PRC2
    cooperate to repress key regulators of Arabidopsis development. PLoS Genetics.
    8(3), e1002512.
  mla: Kim, Sang Yeol, et al. “EMF1 and PRC2 Cooperate to Repress Key Regulators of
    Arabidopsis Development.” <i>PLoS Genetics</i>, vol. 8, no. 3, e1002512, Public
    Library of Science, 2012, doi:<a href="https://doi.org/10.1371/journal.pgen.1002512">10.1371/journal.pgen.1002512</a>.
  short: S.Y. Kim, J. Lee, L. Eshed-Williams, D. Zilberman, Z.R. Sung, PLoS Genetics
    8 (2012).
date_created: 2021-06-07T11:07:56Z
date_published: 2012-03-22T00:00:00Z
date_updated: 2021-12-14T08:31:14Z
day: '22'
department:
- _id: DaZi
doi: 10.1371/journal.pgen.1002512
extern: '1'
external_id:
  pmid:
  - '22457632'
intvolume: '         8'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1371/journal.pgen.1002512
month: '03'
oa: 1
oa_version: Published Version
pmid: 1
publication: PLoS Genetics
publication_identifier:
  eissn:
  - 1553-7404
  issn:
  - 1553-7390
publication_status: published
publisher: Public Library of Science
quality_controlled: '1'
scopus_import: '1'
status: public
title: EMF1 and PRC2 cooperate to repress key regulators of Arabidopsis development
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 8
year: '2012'
...
---
_id: '9528'
abstract:
- lang: eng
  text: Accumulating evidence points toward diverse functions for plant chromatin.
    Remarkable progress has been made over the last few years in elucidating the mechanisms
    for a number of these functions. Activity of the histone demethylase IBM1 accurately
    targets DNA methylation to silent repeats and transposable elements, not to genes.
    A genetic screen uncovered the surprising role of H2A.Z-containing nucleosomes
    in sensing precise differences in ambient temperature and consequent gene regulation.
    Precise maintenance of chromosome number is assured by a histone modification
    that suppresses inappropriate DNA replication and by centromeric histone H3 regulation
    of chromosome segregation. Histones and noncoding RNAs regulate FLOWERING LOCUS
    C, the expression of which quantitatively measures the duration of cold exposure,
    functioning as memory of winter. These findings are a testament to the power of
    using plants to research chromatin organization, and demonstrate examples of how
    chromatin functions to achieve biological accuracy, precision, and memory.
article_processing_charge: No
article_type: review
author:
- first_name: Jason T.
  full_name: Huff, Jason T.
  last_name: Huff
- first_name: Daniel
  full_name: Zilberman, Daniel
  id: 6973db13-dd5f-11ea-814e-b3e5455e9ed1
  last_name: Zilberman
  orcid: 0000-0002-0123-8649
citation:
  ama: Huff JT, Zilberman D. Regulation of biological accuracy, precision, and memory
    by plant chromatin organization. <i>Current Opinion in Genetics and Development</i>.
    2012;22(2):132-138. doi:<a href="https://doi.org/10.1016/j.gde.2012.01.007">10.1016/j.gde.2012.01.007</a>
  apa: Huff, J. T., &#38; Zilberman, D. (2012). Regulation of biological accuracy,
    precision, and memory by plant chromatin organization. <i>Current Opinion in Genetics
    and Development</i>. Elsevier. <a href="https://doi.org/10.1016/j.gde.2012.01.007">https://doi.org/10.1016/j.gde.2012.01.007</a>
  chicago: Huff, Jason T., and Daniel Zilberman. “Regulation of Biological Accuracy,
    Precision, and Memory by Plant Chromatin Organization.” <i>Current Opinion in
    Genetics and Development</i>. Elsevier, 2012. <a href="https://doi.org/10.1016/j.gde.2012.01.007">https://doi.org/10.1016/j.gde.2012.01.007</a>.
  ieee: J. T. Huff and D. Zilberman, “Regulation of biological accuracy, precision,
    and memory by plant chromatin organization,” <i>Current Opinion in Genetics and
    Development</i>, vol. 22, no. 2. Elsevier, pp. 132–138, 2012.
  ista: Huff JT, Zilberman D. 2012. Regulation of biological accuracy, precision,
    and memory by plant chromatin organization. Current Opinion in Genetics and Development.
    22(2), 132–138.
  mla: Huff, Jason T., and Daniel Zilberman. “Regulation of Biological Accuracy, Precision,
    and Memory by Plant Chromatin Organization.” <i>Current Opinion in Genetics and
    Development</i>, vol. 22, no. 2, Elsevier, 2012, pp. 132–38, doi:<a href="https://doi.org/10.1016/j.gde.2012.01.007">10.1016/j.gde.2012.01.007</a>.
  short: J.T. Huff, D. Zilberman, Current Opinion in Genetics and Development 22 (2012)
    132–138.
date_created: 2021-06-08T08:58:52Z
date_published: 2012-04-01T00:00:00Z
date_updated: 2021-12-14T08:32:38Z
department:
- _id: DaZi
doi: 10.1016/j.gde.2012.01.007
extern: '1'
external_id:
  pmid:
  - '22336527'
intvolume: '        22'
issue: '2'
language:
- iso: eng
month: '04'
oa_version: None
page: 132-138
pmid: 1
publication: Current Opinion in Genetics and Development
publication_identifier:
  issn:
  - 0959-437X
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Regulation of biological accuracy, precision, and memory by plant chromatin
  organization
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 22
year: '2012'
...
---
_id: '9535'
abstract:
- lang: eng
  text: The most well-studied function of DNA methylation in eukaryotic cells is the
    transcriptional silencing of genes and transposons. More recent results showed
    that many eukaryotes methylate the bodies of genes as well and that this methylation
    correlates with transcriptional activity rather than repression. The purpose of
    gene body methylation remains mysterious, but is potentially related to the histone
    variant H2A.Z. Studies in plants and animals have shown that the genome-wide distributions
    of H2A.Z and DNA methylation are strikingly anticorrelated. Furthermore, we and
    other investigators have shown that this relationship is likely to be the result
    of an ancient but unknown mechanism by which DNA methylation prevents the incorporation
    of H2A.Z. Recently, we discovered strong correlations between the presence of
    H2A.Z within gene bodies, the degree to which a gene's expression varies across
    tissue types or environmental conditions, and transcriptional misregulation in
    an h2a.z mutant. We propose that one basal function of gene body methylation is
    the establishment of constitutive expression patterns within housekeeping genes
    by excluding H2A.Z from their bodies.
article_processing_charge: No
article_type: review
author:
- first_name: D.
  full_name: Coleman-Derr, D.
  last_name: Coleman-Derr
- first_name: Daniel
  full_name: Zilberman, Daniel
  id: 6973db13-dd5f-11ea-814e-b3e5455e9ed1
  last_name: Zilberman
  orcid: 0000-0002-0123-8649
citation:
  ama: Coleman-Derr D, Zilberman D. DNA methylation, H2A.Z, and the regulation of
    constitutive expression. <i>Cold Spring Harbor Symposia on Quantitative Biology</i>.
    2012;77:147-154. doi:<a href="https://doi.org/10.1101/sqb.2012.77.014944">10.1101/sqb.2012.77.014944</a>
  apa: Coleman-Derr, D., &#38; Zilberman, D. (2012). DNA methylation, H2A.Z, and the
    regulation of constitutive expression. <i>Cold Spring Harbor Symposia on Quantitative
    Biology</i>. Cold Spring Harbor Laboratory Press. <a href="https://doi.org/10.1101/sqb.2012.77.014944">https://doi.org/10.1101/sqb.2012.77.014944</a>
  chicago: Coleman-Derr, D., and Daniel Zilberman. “DNA Methylation, H2A.Z, and the
    Regulation of Constitutive Expression.” <i>Cold Spring Harbor Symposia on Quantitative
    Biology</i>. Cold Spring Harbor Laboratory Press, 2012. <a href="https://doi.org/10.1101/sqb.2012.77.014944">https://doi.org/10.1101/sqb.2012.77.014944</a>.
  ieee: D. Coleman-Derr and D. Zilberman, “DNA methylation, H2A.Z, and the regulation
    of constitutive expression,” <i>Cold Spring Harbor Symposia on Quantitative Biology</i>,
    vol. 77. Cold Spring Harbor Laboratory Press, pp. 147–154, 2012.
  ista: Coleman-Derr D, Zilberman D. 2012. DNA methylation, H2A.Z, and the regulation
    of constitutive expression. Cold Spring Harbor Symposia on Quantitative Biology.
    77, 147–154.
  mla: Coleman-Derr, D., and Daniel Zilberman. “DNA Methylation, H2A.Z, and the Regulation
    of Constitutive Expression.” <i>Cold Spring Harbor Symposia on Quantitative Biology</i>,
    vol. 77, Cold Spring Harbor Laboratory Press, 2012, pp. 147–54, doi:<a href="https://doi.org/10.1101/sqb.2012.77.014944">10.1101/sqb.2012.77.014944</a>.
  short: D. Coleman-Derr, D. Zilberman, Cold Spring Harbor Symposia on Quantitative
    Biology 77 (2012) 147–154.
date_created: 2021-06-08T13:01:23Z
date_published: 2012-12-18T00:00:00Z
date_updated: 2021-12-14T08:33:09Z
day: '18'
department:
- _id: DaZi
doi: 10.1101/sqb.2012.77.014944
extern: '1'
external_id:
  pmid:
  - '23250988'
intvolume: '        77'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1101/sqb.2012.77.014944
month: '12'
oa: 1
oa_version: Published Version
page: 147-154
pmid: 1
publication: Cold Spring Harbor Symposia on Quantitative Biology
publication_identifier:
  eissn:
  - 1943-4456
  issn:
  - 0091-7451
publication_status: published
publisher: Cold Spring Harbor Laboratory Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: DNA methylation, H2A.Z, and the regulation of constitutive expression
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 77
year: '2012'
...
---
_id: '9755'
abstract:
- lang: eng
  text: Due to the omnipresent risk of epidemics, insect societies have evolved sophisticated
    disease defences at the individual and colony level. An intriguing yet little
    understood phenomenon is that social contact to pathogen-exposed individuals reduces
    susceptibility of previously naive nestmates to this pathogen. We tested whether
    such social immunisation in Lasius ants against the entomopathogenic fungus Metarhizium
    anisopliae is based on active upregulation of the immune system of nestmates following
    contact to an infectious individual or passive protection via transfer of immune
    effectors among group members—that is, active versus passive immunisation. We
    found no evidence for involvement of passive immunisation via transfer of antimicrobials
    among colony members. Instead, intensive allogrooming behaviour between naive
    and pathogen-exposed ants before fungal conidia firmly attached to their cuticle
    suggested passage of the pathogen from the exposed individuals to their nestmates.
    By tracing fluorescence-labelled conidia we indeed detected frequent pathogen
    transfer to the nestmates, where they caused low-level infections as revealed
    by growth of small numbers of fungal colony forming units from their dissected
    body content. These infections rarely led to death, but instead promoted an enhanced
    ability to inhibit fungal growth and an active upregulation of immune genes involved
    in antifungal defences (defensin and prophenoloxidase, PPO). Contrarily, there
    was no upregulation of the gene cathepsin L, which is associated with antibacterial
    and antiviral defences, and we found no increased antibacterial activity of nestmates
    of fungus-exposed ants. This indicates that social immunisation after fungal exposure
    is specific, similar to recent findings for individual-level immune priming in
    invertebrates. Epidemiological modeling further suggests that active social immunisation
    is adaptive, as it leads to faster elimination of the disease and lower death
    rates than passive immunisation. Interestingly, humans have also utilised the
    protective effect of low-level infections to fight smallpox by intentional transfer
    of low pathogen doses (“variolation” or “inoculation”).
article_processing_charge: No
author:
- first_name: Matthias
  full_name: Konrad, Matthias
  id: 46528076-F248-11E8-B48F-1D18A9856A87
  last_name: Konrad
- first_name: Meghan
  full_name: Vyleta, Meghan
  id: 418901AA-F248-11E8-B48F-1D18A9856A87
  last_name: Vyleta
- first_name: Fabian
  full_name: Theis, Fabian
  last_name: Theis
- first_name: Miriam
  full_name: Stock, Miriam
  id: 42462816-F248-11E8-B48F-1D18A9856A87
  last_name: Stock
- first_name: Martina
  full_name: Klatt, Martina
  id: E60F29C6-E9AE-11E9-AF6E-D190C7302F38
  last_name: Klatt
- first_name: Verena
  full_name: Drescher, Verena
  last_name: Drescher
- first_name: Carsten
  full_name: Marr, Carsten
  last_name: Marr
- first_name: Line V
  full_name: Ugelvig, Line V
  id: 3DC97C8E-F248-11E8-B48F-1D18A9856A87
  last_name: Ugelvig
  orcid: 0000-0003-1832-8883
- first_name: Sylvia
  full_name: Cremer, Sylvia
  id: 2F64EC8C-F248-11E8-B48F-1D18A9856A87
  last_name: Cremer
  orcid: 0000-0002-2193-3868
citation:
  ama: 'Konrad M, Vyleta M, Theis F, et al. Data from: Social transfer of pathogenic
    fungus promotes active immunisation in ant colonies. 2012. doi:<a href="https://doi.org/10.5061/dryad.sv37s">10.5061/dryad.sv37s</a>'
  apa: 'Konrad, M., Vyleta, M., Theis, F., Stock, M., Klatt, M., Drescher, V., … Cremer,
    S. (2012). Data from: Social transfer of pathogenic fungus promotes active immunisation
    in ant colonies. Dryad. <a href="https://doi.org/10.5061/dryad.sv37s">https://doi.org/10.5061/dryad.sv37s</a>'
  chicago: 'Konrad, Matthias, Meghan Vyleta, Fabian Theis, Miriam Stock, Martina Klatt,
    Verena Drescher, Carsten Marr, Line V Ugelvig, and Sylvia Cremer. “Data from:
    Social Transfer of Pathogenic Fungus Promotes Active Immunisation in Ant Colonies.”
    Dryad, 2012. <a href="https://doi.org/10.5061/dryad.sv37s">https://doi.org/10.5061/dryad.sv37s</a>.'
  ieee: 'M. Konrad <i>et al.</i>, “Data from: Social transfer of pathogenic fungus
    promotes active immunisation in ant colonies.” Dryad, 2012.'
  ista: 'Konrad M, Vyleta M, Theis F, Stock M, Klatt M, Drescher V, Marr C, Ugelvig
    LV, Cremer S. 2012. Data from: Social transfer of pathogenic fungus promotes active
    immunisation in ant colonies, Dryad, <a href="https://doi.org/10.5061/dryad.sv37s">10.5061/dryad.sv37s</a>.'
  mla: 'Konrad, Matthias, et al. <i>Data from: Social Transfer of Pathogenic Fungus
    Promotes Active Immunisation in Ant Colonies</i>. Dryad, 2012, doi:<a href="https://doi.org/10.5061/dryad.sv37s">10.5061/dryad.sv37s</a>.'
  short: M. Konrad, M. Vyleta, F. Theis, M. Stock, M. Klatt, V. Drescher, C. Marr,
    L.V. Ugelvig, S. Cremer, (2012).
date_created: 2021-07-30T08:39:13Z
date_published: 2012-09-27T00:00:00Z
date_updated: 2023-02-23T11:18:41Z
day: '27'
department:
- _id: SyCr
doi: 10.5061/dryad.sv37s
main_file_link:
- open_access: '1'
  url: https://doi.org/10.5061/dryad.sv37s
month: '09'
oa: 1
oa_version: Published Version
publisher: Dryad
related_material:
  record:
  - id: '3242'
    relation: used_in_publication
    status: public
status: public
title: 'Data from: Social transfer of pathogenic fungus promotes active immunisation
  in ant colonies'
type: research_data_reference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2012'
...
---
_id: '9757'
abstract:
- lang: eng
  text: To fight infectious diseases, host immune defences are employed at multiple
    levels. Sanitary behaviour, such as pathogen avoidance and removal, acts as a
    first line of defence to prevent infection [1] before activation of the physiological
    immune system. Insect societies have evolved a wide range of collective hygiene
    measures and intensive health care towards pathogen-exposed group members [2].
    One of the most common behaviours is allogrooming, in which nestmates remove infectious
    particles from the body surfaces of exposed individuals [3]. Here we show that,
    in invasive garden ants, grooming of fungus-exposed brood is effective beyond
    the sheer mechanical removal of fungal conidiospores as it also includes chemical
    disinfection through the application of poison produced by the ants themselves.
    Formic acid is the main active component of the poison. It inhibits fungal growth
    of conidiospores remaining on the brood surface after grooming and also those
    collected in the mouth of the grooming ant. This dual function is achieved by
    uptake of the poison droplet into the mouth through acidopore self-grooming and
    subsequent application onto the infectious brood via brood grooming. This extraordinary
    behaviour extends current understanding of grooming and the establishment of social
    immunity in insect societies.
article_processing_charge: No
author:
- first_name: Simon
  full_name: Tragust, Simon
  id: 35A7A418-F248-11E8-B48F-1D18A9856A87
  last_name: Tragust
- first_name: Barbara
  full_name: Mitteregger, Barbara
  id: 479DDAAC-E9CD-11E9-9B5F-82450873F7A1
  last_name: Mitteregger
- first_name: Vanessa
  full_name: Barone, Vanessa
  id: 419EECCC-F248-11E8-B48F-1D18A9856A87
  last_name: Barone
  orcid: 0000-0003-2676-3367
- first_name: Matthias
  full_name: Konrad, Matthias
  id: 46528076-F248-11E8-B48F-1D18A9856A87
  last_name: Konrad
- first_name: Line V
  full_name: Ugelvig, Line V
  id: 3DC97C8E-F248-11E8-B48F-1D18A9856A87
  last_name: Ugelvig
  orcid: 0000-0003-1832-8883
- first_name: Sylvia
  full_name: Cremer, Sylvia
  id: 2F64EC8C-F248-11E8-B48F-1D18A9856A87
  last_name: Cremer
  orcid: 0000-0002-2193-3868
citation:
  ama: 'Tragust S, Mitteregger B, Barone V, Konrad M, Ugelvig LV, Cremer S. Data from:
    Ants disinfect fungus-exposed brood by oral uptake and spread of their poison.
    2012. doi:<a href="https://doi.org/10.5061/dryad.61649">10.5061/dryad.61649</a>'
  apa: 'Tragust, S., Mitteregger, B., Barone, V., Konrad, M., Ugelvig, L. V., &#38;
    Cremer, S. (2012). Data from: Ants disinfect fungus-exposed brood by oral uptake
    and spread of their poison. Dryad. <a href="https://doi.org/10.5061/dryad.61649">https://doi.org/10.5061/dryad.61649</a>'
  chicago: 'Tragust, Simon, Barbara Mitteregger, Vanessa Barone, Matthias Konrad,
    Line V Ugelvig, and Sylvia Cremer. “Data from: Ants Disinfect Fungus-Exposed Brood
    by Oral Uptake and Spread of Their Poison.” Dryad, 2012. <a href="https://doi.org/10.5061/dryad.61649">https://doi.org/10.5061/dryad.61649</a>.'
  ieee: 'S. Tragust, B. Mitteregger, V. Barone, M. Konrad, L. V. Ugelvig, and S. Cremer,
    “Data from: Ants disinfect fungus-exposed brood by oral uptake and spread of their
    poison.” Dryad, 2012.'
  ista: 'Tragust S, Mitteregger B, Barone V, Konrad M, Ugelvig LV, Cremer S. 2012.
    Data from: Ants disinfect fungus-exposed brood by oral uptake and spread of their
    poison, Dryad, <a href="https://doi.org/10.5061/dryad.61649">10.5061/dryad.61649</a>.'
  mla: 'Tragust, Simon, et al. <i>Data from: Ants Disinfect Fungus-Exposed Brood by
    Oral Uptake and Spread of Their Poison</i>. Dryad, 2012, doi:<a href="https://doi.org/10.5061/dryad.61649">10.5061/dryad.61649</a>.'
  short: S. Tragust, B. Mitteregger, V. Barone, M. Konrad, L.V. Ugelvig, S. Cremer,
    (2012).
date_created: 2021-07-30T12:31:31Z
date_published: 2012-12-14T00:00:00Z
date_updated: 2023-02-23T11:04:28Z
day: '14'
department:
- _id: SyCr
doi: 10.5061/dryad.61649
main_file_link:
- open_access: '1'
  url: https://doi.org/10.5061/dryad.61649
month: '12'
oa: 1
oa_version: Published Version
publisher: Dryad
related_material:
  record:
  - id: '2926'
    relation: used_in_publication
    status: public
status: public
title: 'Data from: Ants disinfect fungus-exposed brood by oral uptake and spread of
  their poison'
type: research_data_reference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2012'
...
---
_id: '9758'
abstract:
- lang: eng
  text: 'We propose a two-step procedure for estimating multiple migration rates in
    an approximate Bayesian computation (ABC) framework, accounting for global nuisance
    parameters. The approach is not limited to migration, but generally of interest
    for inference problems with multiple parameters and a modular structure (e.g.
    independent sets of demes or loci). We condition on a known, but complex demographic
    model of a spatially subdivided population, motivated by the reintroduction of
    Alpine ibex (Capra ibex) into Switzerland. In the first step, the global parameters
    ancestral mutation rate and male mating skew have been estimated for the whole
    population in Aeschbacher et al. (Genetics 2012; 192: 1027). In the second step,
    we estimate in this study the migration rates independently for clusters of demes
    putatively connected by migration. For large clusters (many migration rates),
    ABC faces the problem of too many summary statistics. We therefore assess by simulation
    if estimation per pair of demes is a valid alternative. We find that the trade-off
    between reduced dimensionality for the pairwise estimation on the one hand and
    lower accuracy due to the assumption of pairwise independence on the other depends
    on the number of migration rates to be inferred: the accuracy of the pairwise
    approach increases with the number of parameters, relative to the joint estimation
    approach. To distinguish between low and zero migration, we perform ABC-type model
    comparison between a model with migration and one without. Applying the approach
    to microsatellite data from Alpine ibex, we find no evidence for substantial gene
    flow via migration, except for one pair of demes in one direction.'
article_processing_charge: No
author:
- first_name: Simon
  full_name: Aeschbacher, Simon
  id: 2D35326E-F248-11E8-B48F-1D18A9856A87
  last_name: Aeschbacher
- first_name: Andreas
  full_name: Futschik, Andreas
  last_name: Futschik
- first_name: Mark
  full_name: Beaumont, Mark
  last_name: Beaumont
citation:
  ama: 'Aeschbacher S, Futschik A, Beaumont M. Data from: Approximate Bayesian computation
    for modular inference problems with many parameters: the example of migration
    rates. 2012. doi:<a href="https://doi.org/10.5061/dryad.274b1">10.5061/dryad.274b1</a>'
  apa: 'Aeschbacher, S., Futschik, A., &#38; Beaumont, M. (2012). Data from: Approximate
    Bayesian computation for modular inference problems with many parameters: the
    example of migration rates. Dryad. <a href="https://doi.org/10.5061/dryad.274b1">https://doi.org/10.5061/dryad.274b1</a>'
  chicago: 'Aeschbacher, Simon, Andreas Futschik, and Mark Beaumont. “Data from: Approximate
    Bayesian Computation for Modular Inference Problems with Many Parameters: The
    Example of Migration Rates.” Dryad, 2012. <a href="https://doi.org/10.5061/dryad.274b1">https://doi.org/10.5061/dryad.274b1</a>.'
  ieee: 'S. Aeschbacher, A. Futschik, and M. Beaumont, “Data from: Approximate Bayesian
    computation for modular inference problems with many parameters: the example of
    migration rates.” Dryad, 2012.'
  ista: 'Aeschbacher S, Futschik A, Beaumont M. 2012. Data from: Approximate Bayesian
    computation for modular inference problems with many parameters: the example of
    migration rates, Dryad, <a href="https://doi.org/10.5061/dryad.274b1">10.5061/dryad.274b1</a>.'
  mla: 'Aeschbacher, Simon, et al. <i>Data from: Approximate Bayesian Computation
    for Modular Inference Problems with Many Parameters: The Example of Migration
    Rates</i>. Dryad, 2012, doi:<a href="https://doi.org/10.5061/dryad.274b1">10.5061/dryad.274b1</a>.'
  short: S. Aeschbacher, A. Futschik, M. Beaumont, (2012).
date_created: 2021-07-30T12:36:39Z
date_published: 2012-11-14T00:00:00Z
date_updated: 2023-02-23T11:05:19Z
day: '14'
department:
- _id: NiBa
doi: 10.5061/dryad.274b1
main_file_link:
- open_access: '1'
  url: https://doi.org/10.5061/dryad.274b1
month: '11'
oa: 1
oa_version: Published Version
publisher: Dryad
related_material:
  record:
  - id: '2944'
    relation: used_in_publication
    status: public
status: public
title: 'Data from: Approximate Bayesian computation for modular inference problems
  with many parameters: the example of migration rates'
type: research_data_reference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2012'
...
---
_id: '10896'
abstract:
- lang: eng
  text: Under physiological conditions the brain, via the purine salvage pathway,
    reuses the preformed purine bases hypoxanthine, derived from ATP degradation,
    and adenine (Ade), derived from polyamine synthesis, to restore its ATP pool.
    However, the massive degradation of ATP during ischemia, although providing valuable
    neuroprotective adenosine, results in the accumulation and loss of diffusible
    purine metabolites and thereby leads to a protracted reduction in the post-ischemic
    ATP pool size. In vivo, this may both limit the ability to deploy ATP-dependent
    reparative mechanisms and reduce the subsequent availability of adenosine, whilst
    in brain slices results in tissue with substantially lower levels of ATP than
    in vivo. In the present review, we describe the mechanisms by which brain tissue
    replenishes its ATP, how this can be improved with the clinically tolerated chemicals
    D-ribose and adenine, and the functional, and potential therapeutic, implications
    of doing so.
acknowledgement: We are grateful to Research into Ageing/Ageing UK and The Dunhill
  Trust for funding SzN’s graduate studies, and to Prof Nicholas Dale for his valuable
  input.
article_processing_charge: No
author:
- first_name: Stephanie
  full_name: zur Nedden, Stephanie
  id: 3C77F464-F248-11E8-B48F-1D18A9856A87
  last_name: zur Nedden
- first_name: Alexander S.
  full_name: Doney, Alexander S.
  last_name: Doney
- first_name: Bruno G.
  full_name: Frenguelli, Bruno G.
  last_name: Frenguelli
citation:
  ama: 'zur Nedden S, Doney AS, Frenguelli BG. The double-edged sword: Gaining Adenosine
    at the expense of ATP. How to balance the books. In: Masino S, Boison D, eds.
    <i>Adenosine</i>. 1st ed. New York: Springer; 2012:109-129. doi:<a href="https://doi.org/10.1007/978-1-4614-3903-5_6">10.1007/978-1-4614-3903-5_6</a>'
  apa: 'zur Nedden, S., Doney, A. S., &#38; Frenguelli, B. G. (2012). The double-edged
    sword: Gaining Adenosine at the expense of ATP. How to balance the books. In S.
    Masino &#38; D. Boison (Eds.), <i>Adenosine</i> (1st ed., pp. 109–129). New York:
    Springer. <a href="https://doi.org/10.1007/978-1-4614-3903-5_6">https://doi.org/10.1007/978-1-4614-3903-5_6</a>'
  chicago: 'Nedden, Stephanie zur, Alexander S. Doney, and Bruno G. Frenguelli. “The
    Double-Edged Sword: Gaining Adenosine at the Expense of ATP. How to Balance the
    Books.” In <i>Adenosine</i>, edited by Susan Masino and Detlev Boison, 1st ed.,
    109–29. New York: Springer, 2012. <a href="https://doi.org/10.1007/978-1-4614-3903-5_6">https://doi.org/10.1007/978-1-4614-3903-5_6</a>.'
  ieee: 'S. zur Nedden, A. S. Doney, and B. G. Frenguelli, “The double-edged sword:
    Gaining Adenosine at the expense of ATP. How to balance the books,” in <i>Adenosine</i>,
    1st ed., S. Masino and D. Boison, Eds. New York: Springer, 2012, pp. 109–129.'
  ista: 'zur Nedden S, Doney AS, Frenguelli BG. 2012.The double-edged sword: Gaining
    Adenosine at the expense of ATP. How to balance the books. In: Adenosine. , 109–129.'
  mla: 'zur Nedden, Stephanie, et al. “The Double-Edged Sword: Gaining Adenosine at
    the Expense of ATP. How to Balance the Books.” <i>Adenosine</i>, edited by Susan
    Masino and Detlev Boison, 1st ed., Springer, 2012, pp. 109–29, doi:<a href="https://doi.org/10.1007/978-1-4614-3903-5_6">10.1007/978-1-4614-3903-5_6</a>.'
  short: S. zur Nedden, A.S. Doney, B.G. Frenguelli, in:, S. Masino, D. Boison (Eds.),
    Adenosine, 1st ed., Springer, New York, 2012, pp. 109–129.
date_created: 2022-03-21T07:16:12Z
date_published: 2012-07-23T00:00:00Z
date_updated: 2022-06-21T11:51:58Z
day: '23'
department:
- _id: HaJa
doi: 10.1007/978-1-4614-3903-5_6
edition: '1'
editor:
- first_name: Susan
  full_name: Masino, Susan
  last_name: Masino
- first_name: Detlev
  full_name: Boison, Detlev
  last_name: Boison
language:
- iso: eng
month: '07'
oa_version: None
page: 109-129
place: New York
publication: Adenosine
publication_identifier:
  eisbn:
  - '9781461439035'
  isbn:
  - '9781461439028'
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'The double-edged sword: Gaining Adenosine at the expense of ATP. How to balance
  the books'
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2012'
...
---
_id: '10903'
abstract:
- lang: eng
  text: We propose a logic-based framework for automated reasoning about sequential
    programs manipulating singly-linked lists and arrays with unbounded data. We introduce
    the logic SLAD, which allows combining shape constraints, written in a fragment
    of Separation Logic, with data and size constraints. We address the problem of
    checking the entailment between SLAD formulas, which is crucial in performing
    pre-post condition reasoning. Although this problem is undecidable in general
    for SLAD, we propose a sound and powerful procedure that is able to solve this
    problem for a large class of formulas, beyond the capabilities of existing techniques
    and tools. We prove that this procedure is complete, i.e., it is actually a decision
    procedure for this problem, for an important fragment of SLAD including known
    decidable logics. We implemented this procedure and shown its preciseness and
    its efficiency on a significant benchmark of formulas.
acknowledgement: This work has been partially supported by the French ANR project
  Veridyc
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ahmed
  full_name: Bouajjani, Ahmed
  last_name: Bouajjani
- first_name: Cezara
  full_name: Dragoi, Cezara
  id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
  last_name: Dragoi
- first_name: Constantin
  full_name: Enea, Constantin
  last_name: Enea
- first_name: Mihaela
  full_name: Sighireanu, Mihaela
  last_name: Sighireanu
citation:
  ama: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. Accurate invariant checking for
    programs manipulating lists and arrays with infinite data. In: <i>Automated Technology
    for Verification and Analysis</i>. Vol 7561. LNCS. Berlin, Heidelberg: Springer;
    2012:167-182. doi:<a href="https://doi.org/10.1007/978-3-642-33386-6_14">10.1007/978-3-642-33386-6_14</a>'
  apa: 'Bouajjani, A., Dragoi, C., Enea, C., &#38; Sighireanu, M. (2012). Accurate
    invariant checking for programs manipulating lists and arrays with infinite data.
    In <i>Automated Technology for Verification and Analysis</i> (Vol. 7561, pp. 167–182).
    Berlin, Heidelberg: Springer. <a href="https://doi.org/10.1007/978-3-642-33386-6_14">https://doi.org/10.1007/978-3-642-33386-6_14</a>'
  chicago: 'Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu.
    “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite
    Data.” In <i>Automated Technology for Verification and Analysis</i>, 7561:167–82.
    LNCS. Berlin, Heidelberg: Springer, 2012. <a href="https://doi.org/10.1007/978-3-642-33386-6_14">https://doi.org/10.1007/978-3-642-33386-6_14</a>.'
  ieee: A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Accurate invariant checking
    for programs manipulating lists and arrays with infinite data,” in <i>Automated
    Technology for Verification and Analysis</i>, Thiruvananthapuram, India, 2012,
    vol. 7561, pp. 167–182.
  ista: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Accurate invariant checking
    for programs manipulating lists and arrays with infinite data. Automated Technology
    for Verification and Analysis. ATVA: Automated Technology for Verification and
    AnalysisLNCS, LNCS, vol. 7561, 167–182.'
  mla: Bouajjani, Ahmed, et al. “Accurate Invariant Checking for Programs Manipulating
    Lists and Arrays with Infinite Data.” <i>Automated Technology for Verification
    and Analysis</i>, vol. 7561, Springer, 2012, pp. 167–82, doi:<a href="https://doi.org/10.1007/978-3-642-33386-6_14">10.1007/978-3-642-33386-6_14</a>.
  short: A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Automated Technology
    for Verification and Analysis, Springer, Berlin, Heidelberg, 2012, pp. 167–182.
conference:
  end_date: 2012-10-06
  location: Thiruvananthapuram, India
  name: 'ATVA: Automated Technology for Verification and Analysis'
  start_date: 2012-10-03
date_created: 2022-03-21T07:58:39Z
date_published: 2012-10-15T00:00:00Z
date_updated: 2023-09-05T14:07:24Z
day: '15'
department:
- _id: ToHe
doi: 10.1007/978-3-642-33386-6_14
intvolume: '      7561'
language:
- iso: eng
month: '10'
oa_version: None
page: 167-182
place: Berlin, Heidelberg
publication: Automated Technology for Verification and Analysis
publication_identifier:
  eisbn:
  - '9783642333866'
  eissn:
  - 1611-3349
  isbn:
  - '9783642333859'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Accurate invariant checking for programs manipulating lists and arrays with
  infinite data
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7561
year: '2012'
...
---
_id: '10904'
abstract:
- lang: eng
  text: Multi-dimensional mean-payoff and energy games provide the mathematical foundation
    for the quantitative study of reactive systems, and play a central role in the
    emerging quantitative theory of verification and synthesis. In this work, we study
    the strategy synthesis problem for games with such multi-dimensional objectives
    along with a parity condition, a canonical way to express ω-regular conditions.
    While in general, the winning strategies in such games may require infinite memory,
    for synthesis the most relevant problem is the construction of a finite-memory
    winning strategy (if one exists). Our main contributions are as follows. First,
    we show a tight exponential bound (matching upper and lower bounds) on the memory
    required for finite-memory winning strategies in both multi-dimensional mean-payoff
    and energy games along with parity objectives. This significantly improves the
    triple exponential upper bound for multi energy games (without parity) that could
    be derived from results in literature for games on VASS (vector addition systems
    with states). Second, we present an optimal symbolic and incremental algorithm
    to compute a finite-memory winning strategy (if one exists) in such games. Finally,
    we give a complete characterization of when finite memory of strategies can be
    traded off for randomness. In particular, we show that for one-dimension mean-payoff
    parity games, randomized memoryless strategies are as powerful as their pure finite-memory
    counterparts.
acknowledgement: 'Author supported by Austrian Science Fund (FWF) Grant No P 23499-N23,
  FWF NFN Grant No S11407 (RiSE), ERC Start Grant (279307: Graph Games), Microsoft
  faculty fellowship.'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Mickael
  full_name: Randour, Mickael
  last_name: Randour
- first_name: Jean-François
  full_name: Raskin, Jean-François
  last_name: Raskin
citation:
  ama: 'Chatterjee K, Randour M, Raskin J-F. Strategy synthesis for multi-dimensional
    quantitative objectives. In: Koutny M, Ulidowski I, eds. <i>CONCUR 2012 - Concurrency
    Theory</i>. Vol 7454. Berlin, Heidelberg: Springer; 2012:115-131. doi:<a href="https://doi.org/10.1007/978-3-642-32940-1_10">10.1007/978-3-642-32940-1_10</a>'
  apa: 'Chatterjee, K., Randour, M., &#38; Raskin, J.-F. (2012). Strategy synthesis
    for multi-dimensional quantitative objectives. In M. Koutny &#38; I. Ulidowski
    (Eds.), <i>CONCUR 2012 - Concurrency Theory</i> (Vol. 7454, pp. 115–131). Berlin,
    Heidelberg: Springer. <a href="https://doi.org/10.1007/978-3-642-32940-1_10">https://doi.org/10.1007/978-3-642-32940-1_10</a>'
  chicago: 'Chatterjee, Krishnendu, Mickael Randour, and Jean-François Raskin. “Strategy
    Synthesis for Multi-Dimensional Quantitative Objectives.” In <i>CONCUR 2012 -
    Concurrency Theory</i>, edited by Maciej Koutny and Irek Ulidowski, 7454:115–31.
    Berlin, Heidelberg: Springer, 2012. <a href="https://doi.org/10.1007/978-3-642-32940-1_10">https://doi.org/10.1007/978-3-642-32940-1_10</a>.'
  ieee: K. Chatterjee, M. Randour, and J.-F. Raskin, “Strategy synthesis for multi-dimensional
    quantitative objectives,” in <i>CONCUR 2012 - Concurrency Theory</i>, Newcastle
    upon Tyne, United Kingdom, 2012, vol. 7454, pp. 115–131.
  ista: 'Chatterjee K, Randour M, Raskin J-F. 2012. Strategy synthesis for multi-dimensional
    quantitative objectives. CONCUR 2012 - Concurrency Theory. CONCUR: Conference
    on Concurrency Theory, LNCS, vol. 7454, 115–131.'
  mla: Chatterjee, Krishnendu, et al. “Strategy Synthesis for Multi-Dimensional Quantitative
    Objectives.” <i>CONCUR 2012 - Concurrency Theory</i>, edited by Maciej Koutny
    and Irek Ulidowski, vol. 7454, Springer, 2012, pp. 115–31, doi:<a href="https://doi.org/10.1007/978-3-642-32940-1_10">10.1007/978-3-642-32940-1_10</a>.
  short: K. Chatterjee, M. Randour, J.-F. Raskin, in:, M. Koutny, I. Ulidowski (Eds.),
    CONCUR 2012 - Concurrency Theory, Springer, Berlin, Heidelberg, 2012, pp. 115–131.
conference:
  end_date: 2012-09-07
  location: Newcastle upon Tyne, United Kingdom
  name: 'CONCUR: Conference on Concurrency Theory'
  start_date: 2012-09-04
date_created: 2022-03-21T08:00:21Z
date_published: 2012-09-15T00:00:00Z
date_updated: 2023-02-23T10:55:06Z
day: '15'
department:
- _id: KrCh
doi: 10.1007/978-3-642-32940-1_10
ec_funded: 1
editor:
- first_name: Maciej
  full_name: Koutny, Maciej
  last_name: Koutny
- first_name: Irek
  full_name: Ulidowski, Irek
  last_name: Ulidowski
external_id:
  arxiv:
  - '1201.5073'
intvolume: '      7454'
language:
- iso: eng
month: '09'
oa_version: Preprint
page: 115-131
place: Berlin, Heidelberg
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication: CONCUR 2012 - Concurrency Theory
publication_identifier:
  eisbn:
  - '9783642329401'
  isbn:
  - '9783642329395'
  issn:
  - 0302-9743
  - 1611-3349
publication_status: published
publisher: Springer
quality_controlled: '1'
related_material:
  record:
  - id: '2716'
    relation: later_version
    status: public
scopus_import: '1'
status: public
title: Strategy synthesis for multi-dimensional quantitative objectives
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7454
year: '2012'
...
---
_id: '10905'
abstract:
- lang: eng
  text: "Energy games belong to a class of turn-based two-player infinite-duration
    games played on a weighted directed graph. It is one of the rare and intriguing
    combinatorial problems that lie in NP ∩ co−NP, but are not known to be in P. While
    the existence of polynomial-time algorithms has been a major open problem for
    decades, there is no algorithm that solves any non-trivial subclass in polynomial
    time.\r\nIn this paper, we give several results based on the weight structures
    of the graph. First, we identify a notion of penalty and present a polynomial-time
    algorithm when the penalty is large. Our algorithm is the first polynomial-time
    algorithm on a large class of weighted graphs. It includes several counter examples
    that show that many previous algorithms, such as value iteration and random facet
    algorithms, require at least sub-exponential time. Our main technique is developing
    the first non-trivial approximation algorithm and showing how to convert it to
    an exact algorithm. Moreover, we show that in a practical case in verification
    where weights are clustered around a constant number of values, the energy game
    problem can be solved in polynomial time. We also show that the problem is still
    as hard as in general when the clique-width is bounded or the graph is strongly
    ergodic, suggesting that restricting graph structures need not help."
acknowledgement: 'Supported by the Austrian Science Fund (FWF): P23499-N23, the Austrian
  Science Fund (FWF): S11407-N23 (RiSE), an ERC Start Grant (279307: Graph Games),
  and a Microsoft Faculty Fellows Award'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Monika H
  full_name: Henzinger, Monika H
  id: 540c9bbd-f2de-11ec-812d-d04a5be85630
  last_name: Henzinger
  orcid: 0000-0002-5008-6530
- first_name: Sebastian
  full_name: Krinninger, Sebastian
  last_name: Krinninger
- first_name: Danupon
  full_name: Nanongkai, Danupon
  last_name: Nanongkai
citation:
  ama: 'Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. Polynomial-time algorithms
    for energy games with special weight structures. In: <i>Algorithms – ESA 2012</i>.
    Vol 7501. Springer; 2012:301-312. doi:<a href="https://doi.org/10.1007/978-3-642-33090-2_27">10.1007/978-3-642-33090-2_27</a>'
  apa: 'Chatterjee, K., Henzinger, M. H., Krinninger, S., &#38; Nanongkai, D. (2012).
    Polynomial-time algorithms for energy games with special weight structures. In
    <i>Algorithms – ESA 2012</i> (Vol. 7501, pp. 301–312). Ljubljana, Slovenia: Springer.
    <a href="https://doi.org/10.1007/978-3-642-33090-2_27">https://doi.org/10.1007/978-3-642-33090-2_27</a>'
  chicago: Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, and Danupon
    Nanongkai. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.”
    In <i>Algorithms – ESA 2012</i>, 7501:301–12. Springer, 2012. <a href="https://doi.org/10.1007/978-3-642-33090-2_27">https://doi.org/10.1007/978-3-642-33090-2_27</a>.
  ieee: K. Chatterjee, M. H. Henzinger, S. Krinninger, and D. Nanongkai, “Polynomial-time
    algorithms for energy games with special weight structures,” in <i>Algorithms
    – ESA 2012</i>, Ljubljana, Slovenia, 2012, vol. 7501, pp. 301–312.
  ista: 'Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. 2012. Polynomial-time
    algorithms for energy games with special weight structures. Algorithms – ESA 2012.
    ESA: European Symposium on Algorithms, LNCS, vol. 7501, 301–312.'
  mla: Chatterjee, Krishnendu, et al. “Polynomial-Time Algorithms for Energy Games
    with Special Weight Structures.” <i>Algorithms – ESA 2012</i>, vol. 7501, Springer,
    2012, pp. 301–12, doi:<a href="https://doi.org/10.1007/978-3-642-33090-2_27">10.1007/978-3-642-33090-2_27</a>.
  short: K. Chatterjee, M.H. Henzinger, S. Krinninger, D. Nanongkai, in:, Algorithms
    – ESA 2012, Springer, 2012, pp. 301–312.
conference:
  end_date: 2012-09-12
  location: Ljubljana, Slovenia
  name: 'ESA: European Symposium on Algorithms'
  start_date: 2012-09-10
date_created: 2022-03-21T08:01:45Z
date_published: 2012-10-01T00:00:00Z
date_updated: 2023-09-05T14:09:30Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-33090-2_27
ec_funded: 1
external_id:
  arxiv:
  - '1604.08234'
intvolume: '      7501'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1604.08234
month: '10'
oa: 1
oa_version: Preprint
page: 301-312
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication: Algorithms – ESA 2012
publication_identifier:
  eisbn:
  - '9783642330902'
  eissn:
  - 1611-3349
  isbn:
  - '9783642330896'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
related_material:
  record:
  - id: '535'
    relation: later_version
    status: public
scopus_import: '1'
status: public
title: Polynomial-time algorithms for energy games with special weight structures
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7501
year: '2012'
...
---
_id: '10906'
abstract:
- lang: eng
  text: HSF(C) is a tool that automates verification of safety and liveness properties
    for C programs. This paper describes the verification approach taken by HSF(C)
    and provides instructions on how to install and use the tool.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Sergey
  full_name: Grebenshchikov, Sergey
  last_name: Grebenshchikov
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  id: 335E5684-F248-11E8-B48F-1D18A9856A87
  last_name: Gupta
- first_name: Nuno P.
  full_name: Lopes, Nuno P.
  last_name: Lopes
- first_name: Corneliu
  full_name: Popeea, Corneliu
  last_name: Popeea
- first_name: Andrey
  full_name: Rybalchenko, Andrey
  last_name: Rybalchenko
citation:
  ama: 'Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. HSF(C): A software
    verifier based on Horn clauses. In: Flanagan C, König B, eds. <i>Tools and Algorithms
    for the Construction and Analysis of Systems</i>. Vol 7214. LNCS. Berlin, Heidelberg:
    Springer; 2012:549-551. doi:<a href="https://doi.org/10.1007/978-3-642-28756-5_46">10.1007/978-3-642-28756-5_46</a>'
  apa: 'Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., &#38; Rybalchenko,
    A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan &#38;
    B. König (Eds.), <i>Tools and Algorithms for the Construction and Analysis of
    Systems</i> (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. <a href="https://doi.org/10.1007/978-3-642-28756-5_46">https://doi.org/10.1007/978-3-642-28756-5_46</a>'
  chicago: 'Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea,
    and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In
    <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, edited
    by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer,
    2012. <a href="https://doi.org/10.1007/978-3-642-28756-5_46">https://doi.org/10.1007/978-3-642-28756-5_46</a>.'
  ieee: 'S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko,
    “HSF(C): A software verifier based on Horn clauses,” in <i>Tools and Algorithms
    for the Construction and Analysis of Systems</i>, Tallinn, Estonia, 2012, vol.
    7214, pp. 549–551.'
  ista: 'Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. 2012. HSF(C):
    A software verifier based on Horn clauses. Tools and Algorithms for the Construction
    and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and
    Analysis of SystemsLNCS, LNCS, vol. 7214, 549–551.'
  mla: 'Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn
    Clauses.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>,
    edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51,
    doi:<a href="https://doi.org/10.1007/978-3-642-28756-5_46">10.1007/978-3-642-28756-5_46</a>.'
  short: S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko, in:,
    C. Flanagan, B. König (Eds.), Tools and Algorithms for the Construction and Analysis
    of Systems, Springer, Berlin, Heidelberg, 2012, pp. 549–551.
conference:
  end_date: 2012-04-01
  location: Tallinn, Estonia
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
  start_date: 2012-03-24
date_created: 2022-03-21T08:03:30Z
date_published: 2012-04-01T00:00:00Z
date_updated: 2023-09-05T14:09:54Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-28756-5_46
editor:
- first_name: Cormac
  full_name: Flanagan, Cormac
  last_name: Flanagan
- first_name: Barbara
  full_name: König, Barbara
  last_name: König
intvolume: '      7214'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1007/978-3-642-28756-5_46
month: '04'
oa: 1
oa_version: Published Version
page: 549-551
place: Berlin, Heidelberg
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
  eisbn:
  - '9783642287565'
  eissn:
  - 1611-3349
  isbn:
  - '9783642287558'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: 'HSF(C): A software verifier based on Horn clauses'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7214
year: '2012'
...
