---
_id: '2297'
abstract:
- lang: eng
text: We present an overview of mathematical results on the low temperature properties
of dilute quantum gases, which have been obtained in the past few years. The presentation
includes a discussion of Bose-Einstein condensation, the excitation spectrum for
trapped gases and its relation to superfluidity, as well as the appearance of
quantized vortices in rotating systems. All these properties are intensely being
studied in current experiments on cold atomic gases. We will give a description
of the mathematics involved in understanding these phenomena, starting from the
underlying many-body Schrödinger equation.
arxiv: 1
author:
- first_name: Robert
full_name: Seiringer, Robert
id: 4AFD0470-F248-11E8-B48F-1D18A9856A87
last_name: Seiringer
orcid: 0000-0002-6781-0521
citation:
ama: 'Seiringer R. Hot topics in cold gases: A mathematical physics perspective.
Japanese Journal of Mathematics. 2013;8(2):185-232. doi:10.1007/s11537-013-1264-5'
apa: 'Seiringer, R. (2013). Hot topics in cold gases: A mathematical physics perspective.
Japanese Journal of Mathematics. Springer. https://doi.org/10.1007/s11537-013-1264-5'
chicago: 'Seiringer, Robert. “Hot Topics in Cold Gases: A Mathematical Physics Perspective.”
Japanese Journal of Mathematics. Springer, 2013. https://doi.org/10.1007/s11537-013-1264-5.'
ieee: 'R. Seiringer, “Hot topics in cold gases: A mathematical physics perspective,”
Japanese Journal of Mathematics, vol. 8, no. 2. Springer, pp. 185–232,
2013.'
ista: 'Seiringer R. 2013. Hot topics in cold gases: A mathematical physics perspective.
Japanese Journal of Mathematics. 8(2), 185–232.'
mla: 'Seiringer, Robert. “Hot Topics in Cold Gases: A Mathematical Physics Perspective.”
Japanese Journal of Mathematics, vol. 8, no. 2, Springer, 2013, pp. 185–232,
doi:10.1007/s11537-013-1264-5.'
short: R. Seiringer, Japanese Journal of Mathematics 8 (2013) 185–232.
date_created: 2018-12-11T11:56:50Z
date_published: 2013-09-24T00:00:00Z
date_updated: 2021-01-12T06:56:36Z
day: '24'
department:
- _id: RoSe
doi: 10.1007/s11537-013-1264-5
external_id:
arxiv:
- '0908.3686'
intvolume: ' 8'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/0908.3686
month: '09'
oa: 1
oa_version: Preprint
page: 185 - 232
publication: Japanese Journal of Mathematics
publication_status: published
publisher: Springer
publist_id: '4631'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Hot topics in cold gases: A mathematical physics perspective'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8
year: '2013'
...
---
_id: '2298'
abstract:
- lang: eng
text: "We present a shape analysis for programs that manipulate overlaid data structures
which share sets of objects. The abstract domain contains Separation Logic formulas
that (1) combine a per-object separating conjunction with a per-field separating
conjunction and (2) constrain a set of variables interpreted as sets of objects.
The definition of the abstract domain operators is based on a notion of homomorphism
between formulas, viewed as graphs, used recently to define optimal decision procedures
for fragments of the Separation Logic. Based on a Frame Rule that supports the
two versions of the separating conjunction, the analysis is able to reason in
a modular manner about non-overlaid data structures and then, compose information
only at a few program points, e.g., procedure returns. We have implemented this
analysis in a prototype tool and applied it on several interesting case studies
that manipulate overlaid and nested linked lists.\r\n"
alternative_title:
- LNCS
author:
- 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: 'Dragoi C, Enea C, Sighireanu M. Local shape analysis for overlaid data structures.
In: Vol 7935. Springer; 2013:150-171. doi:10.1007/978-3-642-38856-9_10'
apa: 'Dragoi, C., Enea, C., & Sighireanu, M. (2013). Local shape analysis for
overlaid data structures (Vol. 7935, pp. 150–171). Presented at the SAS: Static
Analysis Symposium, Seattle, WA, United States: Springer. https://doi.org/10.1007/978-3-642-38856-9_10'
chicago: Dragoi, Cezara, Constantin Enea, and Mihaela Sighireanu. “Local Shape Analysis
for Overlaid Data Structures,” 7935:150–71. Springer, 2013. https://doi.org/10.1007/978-3-642-38856-9_10.
ieee: 'C. Dragoi, C. Enea, and M. Sighireanu, “Local shape analysis for overlaid
data structures,” presented at the SAS: Static Analysis Symposium, Seattle, WA,
United States, 2013, vol. 7935, pp. 150–171.'
ista: 'Dragoi C, Enea C, Sighireanu M. 2013. Local shape analysis for overlaid data
structures. SAS: Static Analysis Symposium, LNCS, vol. 7935, 150–171.'
mla: Dragoi, Cezara, et al. Local Shape Analysis for Overlaid Data Structures.
Vol. 7935, Springer, 2013, pp. 150–71, doi:10.1007/978-3-642-38856-9_10.
short: C. Dragoi, C. Enea, M. Sighireanu, in:, Springer, 2013, pp. 150–171.
conference:
end_date: 2013-06-22
location: Seattle, WA, United States
name: 'SAS: Static Analysis Symposium'
start_date: 2013-06-20
date_created: 2018-12-11T11:56:50Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2021-01-12T06:56:36Z
day: '01'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-38856-9_10
ec_funded: 1
file:
- access_level: open_access
checksum: 907edd33a5892e3af093365f1fd57ed7
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:36Z
date_updated: 2020-07-14T12:45:37Z
file_id: '4824'
file_name: IST-2014-196-v1+1_sas13.pdf
file_size: 299004
relation: main_file
file_date_updated: 2020-07-14T12:45:37Z
has_accepted_license: '1'
intvolume: ' 7935'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 150 - 171
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '4630'
pubrep_id: '196'
quality_controlled: '1'
scopus_import: 1
status: public
title: Local shape analysis for overlaid data structures
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7935
year: '2013'
...
---
_id: '2299'
abstract:
- lang: eng
text: 'The standard hardware design flow involves: (a) design of an integrated circuit
using a hardware description language, (b) extensive functional and formal verification,
and (c) logical synthesis. However, the above-mentioned processes consume significant
effort and time. An alternative approach is to use a formal specification language
as a high-level hardware description language and synthesize hardware from formal
specifications. Our work is a case study of the synthesis of the widely and industrially
used AMBA AHB protocol from formal specifications. Bloem et al. presented the
first formal specifications for the AMBA AHB Arbiter and synthesized the AHB Arbiter
circuit. However, in the first formal specification some important assumptions
were missing. Our contributions are as follows: (a) We present detailed formal
specifications for the AHB Arbiter incorporating the missing details, and obtain
significant improvements in the synthesis results (both with respect to the number
of gates in the synthesized circuit and with respect to the time taken to synthesize
the circuit), and (b) we present formal specifications to generate compact circuits
for the remaining two main components of AMBA AHB, namely, AHB Master and AHB
Slave. Thus with systematic description we are able to automatically and completely
synthesize an important and widely used industrial protocol.'
author:
- first_name: Yashdeep
full_name: Godhal, Yashdeep
id: 5B547124-EB61-11E9-8887-89D9C04DBDF5
last_name: Godhal
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Godhal Y, Chatterjee K, Henzinger TA. Synthesis of AMBA AHB from formal specification:
A case study. International Journal on Software Tools for Technology Transfer.
2013;15(5-6):585-601. doi:10.1007/s10009-011-0207-9'
apa: 'Godhal, Y., Chatterjee, K., & Henzinger, T. A. (2013). Synthesis of AMBA
AHB from formal specification: A case study. International Journal on Software
Tools for Technology Transfer. Springer. https://doi.org/10.1007/s10009-011-0207-9'
chicago: 'Godhal, Yashdeep, Krishnendu Chatterjee, and Thomas A Henzinger. “Synthesis
of AMBA AHB from Formal Specification: A Case Study.” International Journal
on Software Tools for Technology Transfer. Springer, 2013. https://doi.org/10.1007/s10009-011-0207-9.'
ieee: 'Y. Godhal, K. Chatterjee, and T. A. Henzinger, “Synthesis of AMBA AHB from
formal specification: A case study,” International Journal on Software Tools
for Technology Transfer, vol. 15, no. 5–6. Springer, pp. 585–601, 2013.'
ista: 'Godhal Y, Chatterjee K, Henzinger TA. 2013. Synthesis of AMBA AHB from formal
specification: A case study. International Journal on Software Tools for Technology
Transfer. 15(5–6), 585–601.'
mla: 'Godhal, Yashdeep, et al. “Synthesis of AMBA AHB from Formal Specification:
A Case Study.” International Journal on Software Tools for Technology Transfer,
vol. 15, no. 5–6, Springer, 2013, pp. 585–601, doi:10.1007/s10009-011-0207-9.'
short: Y. Godhal, K. Chatterjee, T.A. Henzinger, International Journal on Software
Tools for Technology Transfer 15 (2013) 585–601.
date_created: 2018-12-11T11:56:51Z
date_published: 2013-10-01T00:00:00Z
date_updated: 2021-01-12T06:56:37Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/s10009-011-0207-9
file:
- access_level: open_access
checksum: 57b06a732dd8d6349190dba6b5b0d33b
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:53Z
date_updated: 2020-07-14T12:45:37Z
file_id: '4910'
file_name: IST-2012-87-v1+1_Synthesis_of_AMBA_AHB_from_formal_specifications-_A_case_study.pdf
file_size: 277372
relation: main_file
file_date_updated: 2020-07-14T12:45:37Z
has_accepted_license: '1'
intvolume: ' 15'
issue: 5-6
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 585 - 601
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: International Journal on Software Tools for Technology Transfer
publication_status: published
publisher: Springer
publist_id: '4629'
pubrep_id: '87'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Synthesis of AMBA AHB from formal specification: A case study'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15
year: '2013'
...
---
_id: '2300'
abstract:
- lang: eng
text: We consider Ising models in two and three dimensions with nearest neighbor
ferromagnetic interactions and long-range, power law decaying, antiferromagnetic
interactions. If the strength of the ferromagnetic coupling J is larger than a
critical value Jc, then the ground state is homogeneous and ferromagnetic. As
the critical value is approached from smaller values of J, it is believed that
the ground state consists of a periodic array of stripes (d=2) or slabs (d=3),
all of the same size and alternating magnetization. Here we prove rigorously that
the ground state energy per site converges to that of the optimal periodic striped
or slabbed state, in the limit that J tends to the ferromagnetic transition point.
While this theorem does not prove rigorously that the ground state is precisely
striped or slabbed, it does prove that in any suitably large box the ground state
is striped or slabbed with high probability.
article_number: '064401'
arxiv: 1
author:
- first_name: Alessandro
full_name: Giuliani, Alessandro
last_name: Giuliani
- first_name: Élliott
full_name: Lieb, Élliott
last_name: Lieb
- first_name: Robert
full_name: Seiringer, Robert
id: 4AFD0470-F248-11E8-B48F-1D18A9856A87
last_name: Seiringer
orcid: 0000-0002-6781-0521
citation:
ama: Giuliani A, Lieb É, Seiringer R. Realization of stripes and slabs in two and
three dimensions. Physical Review B. 2013;88(6). doi:10.1103/PhysRevB.88.064401
apa: Giuliani, A., Lieb, É., & Seiringer, R. (2013). Realization of stripes
and slabs in two and three dimensions. Physical Review B. American Physical
Society. https://doi.org/10.1103/PhysRevB.88.064401
chicago: Giuliani, Alessandro, Élliott Lieb, and Robert Seiringer. “Realization
of Stripes and Slabs in Two and Three Dimensions.” Physical Review B. American
Physical Society, 2013. https://doi.org/10.1103/PhysRevB.88.064401.
ieee: A. Giuliani, É. Lieb, and R. Seiringer, “Realization of stripes and slabs
in two and three dimensions,” Physical Review B, vol. 88, no. 6. American
Physical Society, 2013.
ista: Giuliani A, Lieb É, Seiringer R. 2013. Realization of stripes and slabs in
two and three dimensions. Physical Review B. 88(6), 064401.
mla: Giuliani, Alessandro, et al. “Realization of Stripes and Slabs in Two and Three
Dimensions.” Physical Review B, vol. 88, no. 6, 064401, American Physical
Society, 2013, doi:10.1103/PhysRevB.88.064401.
short: A. Giuliani, É. Lieb, R. Seiringer, Physical Review B 88 (2013).
date_created: 2018-12-11T11:56:51Z
date_published: 2013-08-01T00:00:00Z
date_updated: 2021-01-12T06:56:38Z
day: '01'
department:
- _id: RoSe
doi: 10.1103/PhysRevB.88.064401
external_id:
arxiv:
- '1305.5323'
intvolume: ' 88'
issue: '6'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1305.5323
month: '08'
oa: 1
oa_version: Preprint
publication: Physical Review B
publication_status: published
publisher: American Physical Society
publist_id: '4627'
quality_controlled: '1'
scopus_import: 1
status: public
title: Realization of stripes and slabs in two and three dimensions
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 88
year: '2013'
...
---
_id: '2301'
abstract:
- lang: eng
text: We describe the design and implementation of P, a domain-specific language
to write asynchronous event driven code. P allows the programmer to specify the
system as a collection of interacting state machines, which communicate with each
other using events. P unifies modeling and programming into one activity for the
programmer. Not only can a P program be compiled into executable code, but it
can also be tested using model checking techniques. P allows the programmer to
specify the environment, used to "close" the system during testing,
as nondeterministic ghost machines. Ghost machines are erased during compilation
to executable code; a type system ensures that the erasure is semantics preserving.
The P language is designed so that a P program can be checked for responsiveness-the
ability to handle every event in a timely manner. By default, a machine needs
to handle every event that arrives in every state. But handling every event in
every state is impractical. The language provides a notion of deferred events
where the programmer can annotate when she wants to delay processing an event.
The default safety checker looks for presence of unhan-dled events. The language
also provides default liveness checks that an event cannot be potentially deferred
forever. P was used to implement and verify the core of the USB device driver
stack that ships with Microsoft Windows 8. The resulting driver is more reliable
and performs better than its prior incarnation (which did not use P); we have
more confidence in the robustness of its design due to the language abstractions
and verification provided by P.
author:
- first_name: Ankush
full_name: Desai, Ankush
last_name: Desai
- first_name: Vivek
full_name: Gupta, Vivek
last_name: Gupta
- first_name: Ethan
full_name: Jackson, Ethan
last_name: Jackson
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
- first_name: Damien
full_name: Zufferey, Damien
id: 4397AC76-F248-11E8-B48F-1D18A9856A87
last_name: Zufferey
orcid: 0000-0002-3197-8736
citation:
ama: 'Desai A, Gupta V, Jackson E, Qadeer S, Rajamani S, Zufferey D. P: Safe asynchronous
event-driven programming. In: Proceedings of the 34th ACM SIGPLAN Conference
on Programming Language Design and Implementation. ACM; 2013:321-331. doi:10.1145/2491956.2462184'
apa: 'Desai, A., Gupta, V., Jackson, E., Qadeer, S., Rajamani, S., & Zufferey,
D. (2013). P: Safe asynchronous event-driven programming. In Proceedings of
the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation
(pp. 321–331). Seattle, WA, United States: ACM. https://doi.org/10.1145/2491956.2462184'
chicago: 'Desai, Ankush, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani,
and Damien Zufferey. “P: Safe Asynchronous Event-Driven Programming.” In Proceedings
of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation,
321–31. ACM, 2013. https://doi.org/10.1145/2491956.2462184.'
ieee: 'A. Desai, V. Gupta, E. Jackson, S. Qadeer, S. Rajamani, and D. Zufferey,
“P: Safe asynchronous event-driven programming,” in Proceedings of the 34th
ACM SIGPLAN Conference on Programming Language Design and Implementation,
Seattle, WA, United States, 2013, pp. 321–331.'
ista: 'Desai A, Gupta V, Jackson E, Qadeer S, Rajamani S, Zufferey D. 2013. P: Safe
asynchronous event-driven programming. Proceedings of the 34th ACM SIGPLAN Conference
on Programming Language Design and Implementation. PLDI: Programming Languages
Design and Implementation, 321–331.'
mla: 'Desai, Ankush, et al. “P: Safe Asynchronous Event-Driven Programming.” Proceedings
of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation,
ACM, 2013, pp. 321–31, doi:10.1145/2491956.2462184.'
short: A. Desai, V. Gupta, E. Jackson, S. Qadeer, S. Rajamani, D. Zufferey, in:,
Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design
and Implementation, ACM, 2013, pp. 321–331.
conference:
end_date: 2013-06-19
location: Seattle, WA, United States
name: 'PLDI: Programming Languages Design and Implementation'
start_date: 2013-06-16
date_created: 2018-12-11T11:56:52Z
date_published: 2013-06-01T00:00:00Z
date_updated: 2021-01-12T06:56:38Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2491956.2462184
ec_funded: 1
language:
- iso: eng
main_file_link:
- url: http://research.microsoft.com/pubs/191069/pldi212_desai.pdf
month: '06'
oa_version: None
page: 321 - 331
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language
Design and Implementation
publication_status: published
publisher: ACM
publist_id: '4626'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'P: Safe asynchronous event-driven programming'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '2303'
abstract:
- lang: eng
text: MADM (Mosaic Analysis with Double Markers) technology offers a genetic approach
in mice to visualize and concomitantly manipulate genetically defined cells at
clonal level and single cell resolution. MADM employs Cre recombinase/loxP-dependent
interchromosomal mitotic recombination to reconstitute two split marker genes—green
GFP and red tdTomato—and can label sparse clones of homozygous mutant cells in
one color and wild-type cells in the other color in an otherwise unlabeled background.
At present, major MADM applications include lineage tracing, single cell labeling,
conditional knockouts in small populations of cells and induction of uniparental
chromosome disomy to assess effects of genomic imprinting. MADM can be applied
universally in the mouse with the sole limitation being the specificity of the
promoter controlling Cre recombinase expression. Here I review recent developments
and extensions of the MADM technique and give an overview of the major discoveries
and progresses enabled by the implementation of the novel genetic MADM tools.
acknowledgement: This work was supported by IST Austria institutional funds.
article_type: review
author:
- first_name: Simon
full_name: Hippenmeyer, Simon
id: 37B36620-F248-11E8-B48F-1D18A9856A87
last_name: Hippenmeyer
orcid: 0000-0003-2279-1061
citation:
ama: Hippenmeyer S. Dissection of gene function at clonal level using mosaic analysis
with double markers. Frontiers in Biology. 2013;8(6):557-568. doi:10.1007/s11515-013-1279-6
apa: Hippenmeyer, S. (2013). Dissection of gene function at clonal level using mosaic
analysis with double markers. Frontiers in Biology. Springer. https://doi.org/10.1007/s11515-013-1279-6
chicago: Hippenmeyer, Simon. “Dissection of Gene Function at Clonal Level Using
Mosaic Analysis with Double Markers.” Frontiers in Biology. Springer, 2013.
https://doi.org/10.1007/s11515-013-1279-6.
ieee: S. Hippenmeyer, “Dissection of gene function at clonal level using mosaic
analysis with double markers,” Frontiers in Biology, vol. 8, no. 6. Springer,
pp. 557–568, 2013.
ista: Hippenmeyer S. 2013. Dissection of gene function at clonal level using mosaic
analysis with double markers. Frontiers in Biology. 8(6), 557–568.
mla: Hippenmeyer, Simon. “Dissection of Gene Function at Clonal Level Using Mosaic
Analysis with Double Markers.” Frontiers in Biology, vol. 8, no. 6, Springer,
2013, pp. 557–68, doi:10.1007/s11515-013-1279-6.
short: S. Hippenmeyer, Frontiers in Biology 8 (2013) 557–568.
date_created: 2018-12-11T11:56:52Z
date_published: 2013-09-03T00:00:00Z
date_updated: 2021-01-12T06:56:39Z
day: '03'
department:
- _id: SiHi
doi: 10.1007/s11515-013-1279-6
intvolume: ' 8'
issue: '6'
language:
- iso: eng
month: '09'
oa_version: None
page: 557 - 568
publication: Frontiers in Biology
publication_status: published
publisher: Springer
publist_id: '4624'
quality_controlled: '1'
scopus_import: 1
status: public
title: Dissection of gene function at clonal level using mosaic analysis with double
markers
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 8
year: '2013'
...
---
_id: '2304'
abstract:
- lang: eng
text: This extended abstract is concerned with the irregularities of distribution
of one-dimensional permuted van der Corput sequences that are generated from linear
permutations. We show how to obtain upper bounds for the discrepancy and diaphony
of these sequences, by relating them to Kronecker sequences and applying earlier
results of Faure and Niederreiter.
acknowledgement: This research is supported by the Graduate school of IST Austria
(Institute of Science and Technology Austria).
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. Van der Corput sequences and linear permutations. Electronic
Notes in Discrete Mathematics. 2013;43:43-50. doi:10.1016/j.endm.2013.07.008
apa: Pausinger, F. (2013). Van der Corput sequences and linear permutations. Electronic
Notes in Discrete Mathematics. Elsevier. https://doi.org/10.1016/j.endm.2013.07.008
chicago: Pausinger, Florian. “Van Der Corput Sequences and Linear Permutations.”
Electronic Notes in Discrete Mathematics. Elsevier, 2013. https://doi.org/10.1016/j.endm.2013.07.008.
ieee: F. Pausinger, “Van der Corput sequences and linear permutations,” Electronic
Notes in Discrete Mathematics, vol. 43. Elsevier, pp. 43–50, 2013.
ista: Pausinger F. 2013. Van der Corput sequences and linear permutations. Electronic
Notes in Discrete Mathematics. 43, 43–50.
mla: Pausinger, Florian. “Van Der Corput Sequences and Linear Permutations.” Electronic
Notes in Discrete Mathematics, vol. 43, Elsevier, 2013, pp. 43–50, doi:10.1016/j.endm.2013.07.008.
short: F. Pausinger, Electronic Notes in Discrete Mathematics 43 (2013) 43–50.
date_created: 2018-12-11T11:56:53Z
date_published: 2013-09-05T00:00:00Z
date_updated: 2021-01-12T06:56:39Z
day: '05'
department:
- _id: HeEd
doi: 10.1016/j.endm.2013.07.008
intvolume: ' 43'
language:
- iso: eng
month: '09'
oa_version: None
page: 43 - 50
publication: Electronic Notes in Discrete Mathematics
publication_status: published
publisher: Elsevier
publist_id: '4623'
quality_controlled: '1'
scopus_import: 1
status: public
title: Van der Corput sequences and linear permutations
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 43
year: '2013'
...
---
_id: '2305'
abstract:
- lang: eng
text: We study the complexity of central controller synthesis problems for finite-state
Markov decision processes, where the objective is to optimize both the expected
mean-payoff performance of the system and its stability. e argue that the basic
theoretical notion of expressing the stability in terms of the variance of the
mean-payoff (called global variance in our paper) is not always sufficient, since
it ignores possible instabilities on respective runs. For this reason we propose
alernative definitions of stability, which we call local and hybrid variance,
and which express how rewards on each run deviate from the run's own mean-payoff
and from the expected mean-payoff, respectively. We show that a strategy ensuring
both the expected mean-payoff and the variance below given bounds requires randomization
and memory, under all the above semantics of variance. We then look at the problem
of determining whether there is a such a strategy. For the global variance, we
show that the problem is in PSPACE, and that the answer can be approximated in
pseudo-polynomial time. For the hybrid variance, the analogous decision problem
is in NP, and a polynomial-time approximating algorithm also exists. For local
variance, we show that the decision problem is in NP. Since the overall performance
can be traded for stability (and vice versa), we also present algorithms for approximating
the associated Pareto curve in all the three cases. Finally, we study a special
case of the decision problems, where we require a given expected mean-payoff together
with zero variance. Here we show that the problems can be all solved in polynomial
time.
arxiv: 1
author:
- first_name: Tomáš
full_name: Brázdil, Tomáš
last_name: Brázdil
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Vojtěch
full_name: Forejt, Vojtěch
last_name: Forejt
- first_name: Antonín
full_name: Kučera, Antonín
last_name: Kučera
citation:
ama: 'Brázdil T, Chatterjee K, Forejt V, Kučera A. Trading performance for stability
in Markov decision processes. In: 28th Annual ACM/IEEE Symposium. IEEE;
2013:331-340. doi:10.1109/LICS.2013.39'
apa: 'Brázdil, T., Chatterjee, K., Forejt, V., & Kučera, A. (2013). Trading
performance for stability in Markov decision processes. In 28th Annual ACM/IEEE
Symposium (pp. 331–340). New Orleans, LA, United States: IEEE. https://doi.org/10.1109/LICS.2013.39'
chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera.
“Trading Performance for Stability in Markov Decision Processes.” In 28th Annual
ACM/IEEE Symposium, 331–40. IEEE, 2013. https://doi.org/10.1109/LICS.2013.39.
ieee: T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera, “Trading performance
for stability in Markov decision processes,” in 28th Annual ACM/IEEE Symposium,
New Orleans, LA, United States, 2013, pp. 331–340.
ista: 'Brázdil T, Chatterjee K, Forejt V, Kučera A. 2013. Trading performance for
stability in Markov decision processes. 28th Annual ACM/IEEE Symposium. LICS:
Logic in Computer Science, 331–340.'
mla: Brázdil, Tomáš, et al. “Trading Performance for Stability in Markov Decision
Processes.” 28th Annual ACM/IEEE Symposium, IEEE, 2013, pp. 331–40, doi:10.1109/LICS.2013.39.
short: T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, in:, 28th Annual ACM/IEEE
Symposium, IEEE, 2013, pp. 331–340.
conference:
end_date: 2013-06-28
location: New Orleans, LA, United States
name: 'LICS: Logic in Computer Science'
start_date: 2013-06-25
date_created: 2018-12-11T11:56:53Z
date_published: 2013-08-01T00:00:00Z
date_updated: 2023-09-20T11:15:30Z
day: '01'
department:
- _id: KrCh
doi: 10.1109/LICS.2013.39
ec_funded: 1
external_id:
arxiv:
- '1305.4103'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1305.4103
month: '08'
oa: 1
oa_version: Preprint
page: 331 - 340
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: 28th Annual ACM/IEEE Symposium
publication_status: published
publisher: IEEE
publist_id: '4622'
quality_controlled: '1'
related_material:
record:
- id: '1294'
relation: later_version
status: public
scopus_import: 1
status: public
title: Trading performance for stability in Markov decision processes
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '2306'
abstract:
- lang: ger
text: Das Buch ist sowohl eine Einführung in die Themen Linked Data, Open Data und
Open Linked Data als es auch den konkreten Bezug auf Bibliotheken behandelt. Hierzu
werden konkrete Anwendungsprojekte beschrieben. Der Band wendet sich dabei sowohl
an Personen aus der Bibliothekspraxis als auch an Personen aus dem Bibliotheksmanagement,
die noch nicht mit dem Thema vertraut sind.
alternative_title:
- Bibliotheks- und Informationspraxis
article_processing_charge: No
author:
- first_name: Patrick
full_name: Danowski, Patrick
id: 2EBD1598-F248-11E8-B48F-1D18A9856A87
last_name: Danowski
orcid: 0000-0002-6026-4409
- first_name: Adrian
full_name: Pohl, Adrian
last_name: Pohl
citation:
ama: Danowski P, Pohl A. (Open) Linked Data in Bibliotheken. Vol 50. De Gruyter;
2013. doi:10.1515/9783110278736
apa: Danowski, P., & Pohl, A. (2013). (Open) Linked Data in Bibliotheken
(Vol. 50). De Gruyter. https://doi.org/10.1515/9783110278736
chicago: Danowski, Patrick, and Adrian Pohl. (Open) Linked Data in Bibliotheken.
Vol. 50. De Gruyter, 2013. https://doi.org/10.1515/9783110278736.
ieee: P. Danowski and A. Pohl, (Open) Linked Data in Bibliotheken, vol. 50.
De Gruyter, 2013.
ista: Danowski P, Pohl A. 2013. (Open) Linked Data in Bibliotheken, De Gruyter,p.
mla: Danowski, Patrick, and Adrian Pohl. (Open) Linked Data in Bibliotheken.
Vol. 50, De Gruyter, 2013, doi:10.1515/9783110278736.
short: P. Danowski, A. Pohl, (Open) Linked Data in Bibliotheken, De Gruyter, 2013.
date_created: 2018-12-11T11:56:53Z
date_published: 2013-09-13T00:00:00Z
date_updated: 2021-12-21T12:17:19Z
day: '13'
ddc:
- '020'
department:
- _id: E-Lib
doi: 10.1515/9783110278736
file:
- access_level: open_access
checksum: 807a408bbee519d792702828a32c6e85
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:49Z
date_updated: 2020-07-14T12:45:38Z
file_id: '4774'
file_name: IST-2017-725-v1+1_[9783110278736_-__Open__Linked_Data_in_Bibliotheken]_Frontmatter.pdf
file_size: 67731
relation: main_file
- access_level: open_access
checksum: 587e95c2ba24307a5a5d5bd1579429d9
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:50Z
date_updated: 2020-07-14T12:45:38Z
file_id: '4775'
file_name: IST-2017-725-v1+2_[9783110278736_-__Open__Linked_Data_in_Bibliotheken]_Inhalt.pdf
file_size: 43563
relation: main_file
- access_level: open_access
checksum: dbcada36bb32d725d9838615706e700f
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:51Z
date_updated: 2020-07-14T12:45:38Z
file_id: '4776'
file_name: IST-2017-725-v1+3_[9783110278736_-__Open__Linked_Data_in_Bibliotheken]_Linked_Open_Data_in_der_Bibliothekswelt__Grundlagen_und_Überblick.pdf
file_size: 11318599
relation: main_file
- access_level: open_access
checksum: 5235712bf0a49ccc8c2cb4f6c2560d43
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:52Z
date_updated: 2020-07-14T12:45:38Z
file_id: '4777'
file_name: IST-2017-725-v1+4_[9783110278736_-__Open__Linked_Data_in_Bibliotheken]_Vokabulare_für_bibliographische_Daten.pdf
file_size: 330210
relation: main_file
- access_level: open_access
checksum: d851cc91f705da80617ac7df33c1c0e1
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:53Z
date_updated: 2020-07-14T12:45:38Z
file_id: '4778'
file_name: IST-2017-725-v1+5_[9783110278736_-__Open__Linked_Data_in_Bibliotheken]_FRBR,_Serials_und_CIDOC_CRM_-_Modellierung_von_fortlaufenden_Sammelwerken_unter_Verwendung_von_FRBRoo.pdf
file_size: 10652088
relation: main_file
- access_level: open_access
checksum: 4e77b182692c58e50fc5251bf23cc584
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:54Z
date_updated: 2020-07-14T12:45:38Z
file_id: '4779'
file_name: IST-2017-725-v1+6_[9783110278736_-__Open__Linked_Data_in_Bibliotheken]_Die_Provenienz_von_Linked_Data.pdf
file_size: 6125273
relation: main_file
- access_level: open_access
checksum: 3debae38064d5099d22f855c353a57ec
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:55Z
date_updated: 2020-07-14T12:45:38Z
file_id: '4780'
file_name: IST-2017-725-v1+7_[9783110278736_-__Open__Linked_Data_in_Bibliotheken]_Forschungsdaten.pdf
file_size: 1893872
relation: main_file
- access_level: open_access
checksum: e630b330dc0b7522d2cf204587030252
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:56Z
date_updated: 2020-07-14T12:45:38Z
file_id: '4781'
file_name: IST-2017-725-v1+8_[9783110278736_-__Open__Linked_Data_in_Bibliotheken]_Datenanreicherung_auf_LOD-Basis.pdf
file_size: 1095929
relation: main_file
- access_level: open_access
checksum: 17edda91271bfcce8e1b6e77ca1c9d11
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:57Z
date_updated: 2020-07-14T12:45:38Z
file_id: '4782'
file_name: IST-2017-725-v1+9_[9783110278736_-__Open__Linked_Data_in_Bibliotheken]_Herausforderung_Wissensvernetzung.pdf
file_size: 149699
relation: main_file
- access_level: open_access
checksum: aacef6734b1de58aeb58024fc47c2373
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:58Z
date_updated: 2020-07-14T12:45:38Z
file_id: '4783'
file_name: IST-2017-725-v1+10_[9783110278736_-__Open__Linked_Data_in_Bibliotheken]_Linked_Open_Data_geht_in_die_Fläche__Der_B3Kat_stellt_seine_Daten_frei.pdf
file_size: 8828405
relation: main_file
- access_level: open_access
checksum: 0619451f7ff3ea641ce0b10c97831f47
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:09:59Z
date_updated: 2020-07-14T12:45:38Z
file_id: '4784'
file_name: IST-2017-725-v1+11_[9783110278736_-__Open__Linked_Data_in_Bibliotheken]_Open_Data_und_Linked_Data_in_einem_Informationssystem_für_die_Archäologie.pdf
file_size: 3191208
relation: main_file
- access_level: open_access
checksum: 44dc8a9fc003f0edd912968958715a23
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:00Z
date_updated: 2020-07-14T12:45:38Z
file_id: '4785'
file_name: IST-2017-725-v1+12_[9783110278736_-__Open__Linked_Data_in_Bibliotheken]_Definition__Offenes_Wissen.pdf
file_size: 78315
relation: main_file
- access_level: open_access
checksum: 48133cecebfd839b77f84f557d530c00
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:01Z
date_updated: 2020-07-14T12:45:38Z
file_id: '4786'
file_name: IST-2017-725-v1+13_[9783110278736_-__Open__Linked_Data_in_Bibliotheken]_Prinzipien_zu_offenen_bibliographischen_Daten.pdf
file_size: 90532
relation: main_file
- access_level: open_access
checksum: a359224ddfdb178fed72b228dcfb699a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:02Z
date_updated: 2020-07-14T12:45:38Z
file_id: '4787'
file_name: IST-2017-725-v1+14_[9783110278736_-__Open__Linked_Data_in_Bibliotheken]_Empfehlungen_zur_Öffnung_bibliothekarischer_Daten.pdf
file_size: 90771
relation: main_file
- access_level: open_access
checksum: 0d2dd31d537c7a495999149d00eaffbf
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:10:03Z
date_updated: 2020-07-14T12:45:38Z
file_id: '4788'
file_name: IST-2017-725-v1+15_[9783110278736_-__Open__Linked_Data_in_Bibliotheken]_Glossar.pdf
file_size: 1830232
relation: main_file
file_date_updated: 2020-07-14T12:45:38Z
has_accepted_license: '1'
intvolume: ' 50'
language:
- iso: ger
license: https://creativecommons.org/licenses/by/4.0/
month: '09'
oa: 1
oa_version: Published Version
publication_identifier:
eisbn:
- 9-783-1102-7873-6
isbn:
- ' 978-3-11-027634-3'
issn:
- 2191-3587
publication_status: published
publisher: De Gruyter
publist_id: '4621'
pubrep_id: '725'
quality_controlled: '1'
status: public
title: (Open) Linked Data in Bibliotheken
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: book
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 50
year: '2013'
...
---
_id: '2315'
abstract:
- lang: eng
text: ' We study the effects of random scatterers on the ground state of the
one-dimensional Lieb-Liniger model of interacting bosons on the unit interval
in the Gross-Pitaevskii regime. We prove that Bose Einstein condensation survives
even a strong random potential with a high density of scatterers. The character
of the wave function of the condensate, however, depends in an essential way on
the interplay between randomness and the strength of the two-body interaction.
For low density of scatterers or strong interactions the wave function extends
over the whole interval. High density of scatterers and weak interaction, on the
other hand, leads to localization of the wave function in a fragmented subset
of the interval. '
article_processing_charge: No
arxiv: 1
author:
- first_name: Robert
full_name: Seiringer, Robert
id: 4AFD0470-F248-11E8-B48F-1D18A9856A87
last_name: Seiringer
orcid: 0000-0002-6781-0521
- first_name: Jakob
full_name: Yngvason, Jakob
last_name: Yngvason
- first_name: Valentin
full_name: Zagrebnov, Valentin
last_name: Zagrebnov
citation:
ama: 'Seiringer R, Yngvason J, Zagrebnov V. Disordered Bose-Einstein condensates
with interaction. In: World Scientific Publishing; 2013:610-619. doi:10.1142/9789814449243_0063'
apa: 'Seiringer, R., Yngvason, J., & Zagrebnov, V. (2013). Disordered Bose-Einstein
condensates with interaction (pp. 610–619). Presented at the ICMP: International
Congress on Mathematical Physics, World Scientific Publishing. https://doi.org/10.1142/9789814449243_0063'
chicago: Seiringer, Robert, Jakob Yngvason, and Valentin Zagrebnov. “Disordered
Bose-Einstein Condensates with Interaction,” 610–19. World Scientific Publishing,
2013. https://doi.org/10.1142/9789814449243_0063.
ieee: 'R. Seiringer, J. Yngvason, and V. Zagrebnov, “Disordered Bose-Einstein condensates
with interaction,” presented at the ICMP: International Congress on Mathematical
Physics, 2013, pp. 610–619.'
ista: 'Seiringer R, Yngvason J, Zagrebnov V. 2013. Disordered Bose-Einstein condensates
with interaction. ICMP: International Congress on Mathematical Physics, 610–619.'
mla: Seiringer, Robert, et al. Disordered Bose-Einstein Condensates with Interaction.
World Scientific Publishing, 2013, pp. 610–19, doi:10.1142/9789814449243_0063.
short: R. Seiringer, J. Yngvason, V. Zagrebnov, in:, World Scientific Publishing,
2013, pp. 610–619.
conference:
name: 'ICMP: International Congress on Mathematical Physics'
date_created: 2018-12-11T11:56:57Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2021-01-12T06:56:43Z
doi: 10.1142/9789814449243_0063
extern: '1'
external_id:
arxiv:
- '1209.4046'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1209.4046
oa: 1
oa_version: None
page: 610-619
publication_status: published
publisher: World Scientific Publishing
publist_id: '4612'
status: public
title: Disordered Bose-Einstein condensates with interaction
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
_id: '2319'
abstract:
- lang: eng
text: In a recent paper [7] we give the first rigorous derivation of the celebrated
Ginzburg-Landau (GL)theory, starting from the microscopic Bardeen- Cooper-Schrieffer
(BCS)model. Here we present our results in the simplified case of a one-dimensional
system of particles interacting via a δ-potential.
author:
- first_name: Rupert
full_name: Frank, Rupert L
last_name: Frank
- first_name: Christian
full_name: Hainzl, Christian
last_name: Hainzl
- first_name: Robert
full_name: Robert Seiringer
id: 4AFD0470-F248-11E8-B48F-1D18A9856A87
last_name: Seiringer
orcid: 0000-0002-6781-0521
- first_name: Jan
full_name: Solovej, Jan P
last_name: Solovej
citation:
ama: 'Frank R, Hainzl C, Seiringer R, Solovej J. Derivation of Ginzburg-Landau
theory for a one-dimensional system with contact interaction. In: Springer; 2013:57-88.
doi:10.1007/978-3-0348-0531-5_3'
apa: 'Frank, R., Hainzl, C., Seiringer, R., & Solovej, J. (2013). Derivation
of Ginzburg-Landau theory for a one-dimensional system with contact interaction
(pp. 57–88). Presented at the OTAMP: Operator Theory, Analysis and Mathematical
Physics, Springer. https://doi.org/10.1007/978-3-0348-0531-5_3'
chicago: Frank, Rupert, Christian Hainzl, Robert Seiringer, and Jan Solovej. “ Derivation
of Ginzburg-Landau Theory for a One-Dimensional System with Contact Interaction,”
57–88. Springer, 2013. https://doi.org/10.1007/978-3-0348-0531-5_3.
ieee: 'R. Frank, C. Hainzl, R. Seiringer, and J. Solovej, “ Derivation of Ginzburg-Landau
theory for a one-dimensional system with contact interaction,” presented at the
OTAMP: Operator Theory, Analysis and Mathematical Physics, 2013, pp. 57–88.'
ista: 'Frank R, Hainzl C, Seiringer R, Solovej J. 2013. Derivation of Ginzburg-Landau
theory for a one-dimensional system with contact interaction. OTAMP: Operator
Theory, Analysis and Mathematical Physics, 57–88.'
mla: Frank, Rupert, et al. Derivation of Ginzburg-Landau Theory for a One-Dimensional
System with Contact Interaction. Springer, 2013, pp. 57–88, doi:10.1007/978-3-0348-0531-5_3.
short: R. Frank, C. Hainzl, R. Seiringer, J. Solovej, in:, Springer, 2013, pp. 57–88.
conference:
name: 'OTAMP: Operator Theory, Analysis and Mathematical Physics'
date_created: 2018-12-11T11:56:58Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2021-01-12T06:56:45Z
day: '01'
doi: 10.1007/978-3-0348-0531-5_3
extern: 1
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1103.1866
month: '01'
oa: 1
page: 57 - 88
publication_status: published
publisher: Springer
publist_id: '4608'
quality_controlled: 0
status: public
title: ' Derivation of Ginzburg-Landau theory for a one-dimensional system with contact
interaction'
type: conference
year: '2013'
...
---
_id: '2327'
abstract:
- lang: eng
text: 'We define the model-measuring problem: given a model M and specification
φ, what is the maximal distance ρ such that all models M′ within distance ρ from
M satisfy (or violate) φ. The model measuring problem presupposes a distance function
on models. We concentrate on automatic distance functions, which are defined by
weighted automata. The model-measuring problem subsumes several generalizations
of the classical model-checking problem, in particular, quantitative model-checking
problems that measure the degree of satisfaction of a specification, and robustness
problems that measure how much a model can be perturbed without violating the
specification. We show that for automatic distance functions, and ω-regular linear-time
and branching-time specifications, the model-measuring problem can be solved.
We use automata-theoretic model-checking methods for model measuring, replacing
the emptiness question for standard word and tree automata by the optimal-weight
question for the weighted versions of these automata. We consider weighted automata
that accumulate weights by maximizing, summing, discounting, and limit averaging.
We give several examples of using the model-measuring problem to compute various
notions of robustness and quantitative satisfaction for temporal specifications.'
alternative_title:
- LNCS
author:
- 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: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
citation:
ama: Henzinger TA, Otop J. From model checking to model measuring. 2013;8052:273-287.
doi:10.1007/978-3-642-40184-8_20
apa: 'Henzinger, T. A., & Otop, J. (2013). From model checking to model measuring.
Presented at the CONCUR: Concurrency Theory, Buenos Aires, Argentina: Springer.
https://doi.org/10.1007/978-3-642-40184-8_20'
chicago: Henzinger, Thomas A, and Jan Otop. “From Model Checking to Model Measuring.”
Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-40184-8_20.
ieee: T. A. Henzinger and J. Otop, “From model checking to model measuring,” vol.
8052. Springer, pp. 273–287, 2013.
ista: Henzinger TA, Otop J. 2013. From model checking to model measuring. 8052,
273–287.
mla: Henzinger, Thomas A., and Jan Otop. From Model Checking to Model Measuring.
Vol. 8052, Springer, 2013, pp. 273–87, doi:10.1007/978-3-642-40184-8_20.
short: T.A. Henzinger, J. Otop, 8052 (2013) 273–287.
conference:
end_date: 2013-08-30
location: Buenos Aires, Argentina
name: 'CONCUR: Concurrency Theory'
start_date: 2013-08-27
date_created: 2018-12-11T11:57:00Z
date_published: 2013-08-01T00:00:00Z
date_updated: 2023-02-23T12:25:26Z
day: '01'
ddc:
- '005'
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-40184-8_20
file:
- access_level: open_access
checksum: 4c04695c4bfdf2119cd4f5d1babc3e8a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:45Z
date_updated: 2020-07-14T12:45:38Z
file_id: '5301'
file_name: IST-2013-129-v1+1_concur.pdf
file_size: 378587
relation: main_file
file_date_updated: 2020-07-14T12:45:38Z
has_accepted_license: '1'
intvolume: ' 8052'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 273 - 287
publication_status: published
publisher: Springer
publist_id: '4599'
pubrep_id: '129'
quality_controlled: '1'
related_material:
record:
- id: '5417'
relation: earlier_version
status: public
series_title: Lecture Notes in Computer Science
status: public
title: From model checking to model measuring
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8052
year: '2013'
...
---
_id: '2328'
abstract:
- lang: eng
text: "Linearizability of concurrent data structures is usually proved by monolithic
simulation arguments relying on identifying the so-called linearization points.
Regrettably, such proofs, whether manual or automatic, are often complicated and
scale poorly to advanced non-blocking concurrency patterns, such as helping and
optimistic updates.\r\nIn response, we propose a more modular way of checking
linearizability of concurrent queue algorithms that does not involve identifying
linearization points. We reduce the task of proving linearizability with respect
to the queue specification to establishing four basic properties, each of which
can be proved independently by simpler arguments. As a demonstration of our approach,
we verify the Herlihy and Wing queue, an algorithm that is challenging to verify
by a simulation proof."
alternative_title:
- LNCS
author:
- 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: Ali
full_name: Sezgin, Ali
id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
last_name: Sezgin
- first_name: Viktor
full_name: Vafeiadis, Viktor
last_name: Vafeiadis
citation:
ama: Henzinger TA, Sezgin A, Vafeiadis V. Aspect-oriented linearizability proofs.
2013;8052:242-256. doi:10.1007/978-3-642-40184-8_18
apa: 'Henzinger, T. A., Sezgin, A., & Vafeiadis, V. (2013). Aspect-oriented
linearizability proofs. Presented at the CONCUR: Concurrency Theory, Buenos Aires,
Argentina: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-642-40184-8_18'
chicago: Henzinger, Thomas A, Ali Sezgin, and Viktor Vafeiadis. “Aspect-Oriented
Linearizability Proofs.” Lecture Notes in Computer Science. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik, 2013. https://doi.org/10.1007/978-3-642-40184-8_18.
ieee: T. A. Henzinger, A. Sezgin, and V. Vafeiadis, “Aspect-oriented linearizability
proofs,” vol. 8052. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 242–256,
2013.
ista: Henzinger TA, Sezgin A, Vafeiadis V. 2013. Aspect-oriented linearizability
proofs. 8052, 242–256.
mla: Henzinger, Thomas A., et al. Aspect-Oriented Linearizability Proofs.
Vol. 8052, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 242–56,
doi:10.1007/978-3-642-40184-8_18.
short: T.A. Henzinger, A. Sezgin, V. Vafeiadis, 8052 (2013) 242–256.
conference:
end_date: 2013-08-30
location: Buenos Aires, Argentina
name: 'CONCUR: Concurrency Theory'
start_date: 2013-08-27
date_created: 2018-12-11T11:57:01Z
date_published: 2013-08-01T00:00:00Z
date_updated: 2023-02-23T10:16:27Z
day: '01'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.1007/978-3-642-40184-8_18
ec_funded: 1
file:
- access_level: open_access
checksum: bdbb520de91751fe0136309ad4ef67e4
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:08:58Z
date_updated: 2020-07-14T12:45:39Z
file_id: '4721'
file_name: IST-2014-197-v1+1_main-queue-verification.pdf
file_size: 337059
relation: main_file
file_date_updated: 2020-07-14T12:45:39Z
has_accepted_license: '1'
intvolume: ' 8052'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 242 - 256
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '4598'
pubrep_id: '197'
quality_controlled: '1'
related_material:
record:
- id: '1832'
relation: later_version
status: public
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Aspect-oriented linearizability proofs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8052
year: '2013'
...
---
_id: '2329'
abstract:
- lang: eng
text: 'Two-player games on graphs are central in many problems in formal verification
and program analysis such as synthesis and verification of open systems. In this
work, we consider both finite-state game graphs, and recursive game graphs (or
pushdown game graphs) that model the control flow of sequential programs with
recursion. The objectives we study are multidimensional mean-payoff objectives,
where the goal of player 1 is to ensure that the mean-payoff is non-negative in
all dimensions. In pushdown games two types of strategies are relevant: (1) global
strategies, that depend on the entire global history; and (2) modular strategies,
that have only local memory and thus do not depend on the context of invocation.
Our main contributions are as follows: (1) We show that finite-state multidimensional
mean-payoff games can be solved in polynomial time if the number of dimensions
and the maximal absolute value of the weights are fixed; whereas if the number
of dimensions is arbitrary, then the problem is known to be coNP-complete. (2)
We show that pushdown graphs with multidimensional mean-payoff objectives can
be solved in polynomial time. For both (1) and (2) our algorithms are based on
hyperplane separation technique. (3) For pushdown games under global strategies
both one and multidimensional mean-payoff objectives problems are known to be
undecidable, and we show that under modular strategies the multidimensional problem
is also undecidable; under modular strategies the one-dimensional problem is NP-complete.
We show that if the number of modules, the number of exits, and the maximal absolute
value of the weights are fixed, then pushdown games under modular strategies with
one-dimensional mean-payoff objectives can be solved in polynomial time, and if
either the number of exits or the number of modules is unbounded, then the problem
is NP-hard. (4) Finally we show that a fixed parameter tractable algorithm for
finite-state multidimensional mean-payoff games or pushdown games under modular
strategies with one-dimensional mean-payoff objectives would imply the fixed parameter
tractability of parity games.'
alternative_title:
- LNCS
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: Yaron
full_name: Velner, Yaron
last_name: Velner
citation:
ama: Chatterjee K, Velner Y. Hyperplane separation technique for multidimensional
mean-payoff games. 2013;8052:500-515. doi:10.1007/978-3-642-40184-8_35
apa: 'Chatterjee, K., & Velner, Y. (2013). Hyperplane separation technique for
multidimensional mean-payoff games. Presented at the CONCUR: Concurrency Theory,
Buenos Aires, Argentinia: Springer. https://doi.org/10.1007/978-3-642-40184-8_35'
chicago: Chatterjee, Krishnendu, and Yaron Velner. “Hyperplane Separation Technique
for Multidimensional Mean-Payoff Games.” Lecture Notes in Computer Science. Springer,
2013. https://doi.org/10.1007/978-3-642-40184-8_35.
ieee: K. Chatterjee and Y. Velner, “Hyperplane separation technique for multidimensional
mean-payoff games,” vol. 8052. Springer, pp. 500–515, 2013.
ista: Chatterjee K, Velner Y. 2013. Hyperplane separation technique for multidimensional
mean-payoff games. 8052, 500–515.
mla: Chatterjee, Krishnendu, and Yaron Velner. Hyperplane Separation Technique
for Multidimensional Mean-Payoff Games. Vol. 8052, Springer, 2013, pp. 500–15,
doi:10.1007/978-3-642-40184-8_35.
short: K. Chatterjee, Y. Velner, 8052 (2013) 500–515.
conference:
end_date: 2013-08-30
location: Buenos Aires, Argentinia
name: 'CONCUR: Concurrency Theory'
start_date: 2013-08-27
date_created: 2018-12-11T11:57:01Z
date_published: 2013-08-01T00:00:00Z
date_updated: 2023-02-23T13:00:42Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-40184-8_35
ec_funded: 1
external_id:
arxiv:
- '1210.3141'
intvolume: ' 8052'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1210.3141
month: '08'
oa: 1
oa_version: Preprint
page: 500 - 515
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_status: published
publisher: Springer
publist_id: '4597'
quality_controlled: '1'
related_material:
record:
- id: '717'
relation: later_version
status: public
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Hyperplane separation technique for multidimensional mean-payoff games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8052
year: '2013'
...
---
_id: '2404'
abstract:
- lang: eng
text: The Lieb-Thirring inequalities give a bound on the negative eigenvalues of
a Schrödinger operator in terms of an Lp-norm of the potential. These are dual
to bounds on the H1-norms of a system of orthonormal functions. Here we extend
these bounds to analogous inequalities for perturbations of the Fermi sea of noninteracting
particles (i.e., for perturbations of the continuous spectrum of the Laplacian
by local potentials).
author:
- first_name: Rupert
full_name: Frank, Rupert L
last_name: Frank
- first_name: Mathieu
full_name: Lewin, Mathieu
last_name: Lewin
- first_name: Élliott
full_name: Lieb, Élliott H
last_name: Lieb
- first_name: Robert
full_name: Robert Seiringer
id: 4AFD0470-F248-11E8-B48F-1D18A9856A87
last_name: Seiringer
orcid: 0000-0002-6781-0521
citation:
ama: Frank R, Lewin M, Lieb É, Seiringer R. A positive density analogue of the Lieb-Thirring
inequality. Duke Mathematical Journal. 2013;162(3):435-495. doi:10.1215/00127094-2019477
apa: Frank, R., Lewin, M., Lieb, É., & Seiringer, R. (2013). A positive density
analogue of the Lieb-Thirring inequality. Duke Mathematical Journal. Duke
University Press. https://doi.org/10.1215/00127094-2019477
chicago: Frank, Rupert, Mathieu Lewin, Élliott Lieb, and Robert Seiringer. “A Positive
Density Analogue of the Lieb-Thirring Inequality.” Duke Mathematical Journal.
Duke University Press, 2013. https://doi.org/10.1215/00127094-2019477.
ieee: R. Frank, M. Lewin, É. Lieb, and R. Seiringer, “A positive density analogue
of the Lieb-Thirring inequality,” Duke Mathematical Journal, vol. 162,
no. 3. Duke University Press, pp. 435–495, 2013.
ista: Frank R, Lewin M, Lieb É, Seiringer R. 2013. A positive density analogue of
the Lieb-Thirring inequality. Duke Mathematical Journal. 162(3), 435–495.
mla: Frank, Rupert, et al. “A Positive Density Analogue of the Lieb-Thirring Inequality.”
Duke Mathematical Journal, vol. 162, no. 3, Duke University Press, 2013,
pp. 435–95, doi:10.1215/00127094-2019477.
short: R. Frank, M. Lewin, É. Lieb, R. Seiringer, Duke Mathematical Journal 162
(2013) 435–495.
date_created: 2018-12-11T11:57:28Z
date_published: 2013-02-01T00:00:00Z
date_updated: 2021-01-12T06:57:17Z
day: '01'
doi: 10.1215/00127094-2019477
extern: 1
intvolume: ' 162'
issue: '3'
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1108.4246
month: '02'
oa: 1
page: 435 - 495
publication: Duke Mathematical Journal
publication_status: published
publisher: Duke University Press
publist_id: '4521'
quality_controlled: 0
status: public
title: A positive density analogue of the Lieb-Thirring inequality
type: journal_article
volume: 162
year: '2013'
...
---
_id: '2405'
abstract:
- lang: eng
text: We consider the bipolaron in the Pekar-Tomasevich approximation and address
the question whether the ground state is spherically symmetric or not. Numerical
analysis has, so far, not completely settled the question. Our contribution is
to prove rigorously that the ground state remains spherical for small values of
the electron-electron Coulomb repulsion.
author:
- first_name: Rupert
full_name: Frank, Rupert L
last_name: Frank
- first_name: Élliott
full_name: Lieb, Élliott H
last_name: Lieb
- first_name: Robert
full_name: Robert Seiringer
id: 4AFD0470-F248-11E8-B48F-1D18A9856A87
last_name: Seiringer
orcid: 0000-0002-6781-0521
citation:
ama: Frank R, Lieb É, Seiringer R. Symmetry of bipolaron bound states for small
Coulomb repulsion. Communications in Mathematical Physics. 2013;319(2):557-573.
doi:10.1007/s00220-012-1604-y
apa: Frank, R., Lieb, É., & Seiringer, R. (2013). Symmetry of bipolaron bound
states for small Coulomb repulsion. Communications in Mathematical Physics.
Springer. https://doi.org/10.1007/s00220-012-1604-y
chicago: Frank, Rupert, Élliott Lieb, and Robert Seiringer. “Symmetry of Bipolaron
Bound States for Small Coulomb Repulsion.” Communications in Mathematical Physics.
Springer, 2013. https://doi.org/10.1007/s00220-012-1604-y.
ieee: R. Frank, É. Lieb, and R. Seiringer, “Symmetry of bipolaron bound states for
small Coulomb repulsion,” Communications in Mathematical Physics, vol.
319, no. 2. Springer, pp. 557–573, 2013.
ista: Frank R, Lieb É, Seiringer R. 2013. Symmetry of bipolaron bound states for
small Coulomb repulsion. Communications in Mathematical Physics. 319(2), 557–573.
mla: Frank, Rupert, et al. “Symmetry of Bipolaron Bound States for Small Coulomb
Repulsion.” Communications in Mathematical Physics, vol. 319, no. 2, Springer,
2013, pp. 557–73, doi:10.1007/s00220-012-1604-y.
short: R. Frank, É. Lieb, R. Seiringer, Communications in Mathematical Physics 319
(2013) 557–573.
date_created: 2018-12-11T11:57:28Z
date_published: 2013-04-01T00:00:00Z
date_updated: 2021-01-12T06:57:17Z
day: '01'
doi: 10.1007/s00220-012-1604-y
extern: 1
intvolume: ' 319'
issue: '2'
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1201.3954
month: '04'
oa: 1
page: 557 - 573
publication: Communications in Mathematical Physics
publication_status: published
publisher: Springer
publist_id: '4522'
quality_controlled: 0
status: public
title: Symmetry of bipolaron bound states for small Coulomb repulsion
type: journal_article
volume: 319
year: '2013'
...
---
_id: '2406'
abstract:
- lang: eng
text: We study the effects of random scatterers on the ground state of the one-dimensional
Lieb-Liniger model of interacting bosons on the unit interval. We prove that,
in the Gross-Pitaevskii limit, Bose Einstein condensation takes place in the whole
parameter range considered. The character of the wave function of the condensate,
however, depends in an essential way on the interplay between randomness and the
strength of the two-body interaction. For low density of scatterers or strong
interactions the wave function extends over the whole interval. High density of
scatterers and weak interaction, on the other hand, leads to localization of the
wave function in a fragmented subset of the unit interval.
author:
- first_name: Robert
full_name: Robert Seiringer
id: 4AFD0470-F248-11E8-B48F-1D18A9856A87
last_name: Seiringer
orcid: 0000-0002-6781-0521
- first_name: Jakob
full_name: Yngvason, Jakob
last_name: Yngvason
- first_name: Valentin
full_name: Zagrebnov, Valentin A
last_name: Zagrebnov
citation:
ama: 'Seiringer R, Yngvason J, Zagrebnov V. Condensation of interacting bosons in
a random potential. European Physical Journal: Special Topics. 2013;217(1):103-107.
doi:10.1140/epjst/e2013-01759-5'
apa: 'Seiringer, R., Yngvason, J., & Zagrebnov, V. (2013). Condensation of interacting
bosons in a random potential. European Physical Journal: Special Topics.
Springer. https://doi.org/10.1140/epjst/e2013-01759-5'
chicago: 'Seiringer, Robert, Jakob Yngvason, and Valentin Zagrebnov. “Condensation
of Interacting Bosons in a Random Potential.” European Physical Journal: Special
Topics. Springer, 2013. https://doi.org/10.1140/epjst/e2013-01759-5.'
ieee: 'R. Seiringer, J. Yngvason, and V. Zagrebnov, “Condensation of interacting
bosons in a random potential,” European Physical Journal: Special Topics,
vol. 217, no. 1. Springer, pp. 103–107, 2013.'
ista: 'Seiringer R, Yngvason J, Zagrebnov V. 2013. Condensation of interacting bosons
in a random potential. European Physical Journal: Special Topics. 217(1), 103–107.'
mla: 'Seiringer, Robert, et al. “Condensation of Interacting Bosons in a Random
Potential.” European Physical Journal: Special Topics, vol. 217, no. 1,
Springer, 2013, pp. 103–07, doi:10.1140/epjst/e2013-01759-5.'
short: 'R. Seiringer, J. Yngvason, V. Zagrebnov, European Physical Journal: Special
Topics 217 (2013) 103–107.'
date_created: 2018-12-11T11:57:29Z
date_published: 2013-02-01T00:00:00Z
date_updated: 2021-01-12T06:57:17Z
day: '01'
doi: 10.1140/epjst/e2013-01759-5
extern: 1
intvolume: ' 217'
issue: '1'
month: '02'
page: 103 - 107
publication: 'European Physical Journal: Special Topics'
publication_status: published
publisher: Springer
publist_id: '4520'
quality_controlled: 0
status: public
title: Condensation of interacting bosons in a random potential
type: journal_article
volume: 217
year: '2013'
...
---
_id: '2408'
abstract:
- lang: eng
text: We investigate the low-energy excitation spectrum of a Bose gas confined in
a trap, with weak long-range repulsive interactions. In particular, we prove that
the spectrum can be described in terms of the eigenvalues of an effective one-particle
operator, as predicted by the Bogoliubov approximation.
author:
- first_name: Philip
full_name: Grech, Philip
last_name: Grech
- first_name: Robert
full_name: Robert Seiringer
id: 4AFD0470-F248-11E8-B48F-1D18A9856A87
last_name: Seiringer
orcid: 0000-0002-6781-0521
citation:
ama: Grech P, Seiringer R. The excitation spectrum for weakly interacting Bosons
in a trap. Communications in Mathematical Physics. 2013;322(2):559-591.
doi:10.1007/s00220-013-1736-8
apa: Grech, P., & Seiringer, R. (2013). The excitation spectrum for weakly interacting
Bosons in a trap. Communications in Mathematical Physics. Springer. https://doi.org/10.1007/s00220-013-1736-8
chicago: Grech, Philip, and Robert Seiringer. “The Excitation Spectrum for Weakly
Interacting Bosons in a Trap.” Communications in Mathematical Physics.
Springer, 2013. https://doi.org/10.1007/s00220-013-1736-8.
ieee: P. Grech and R. Seiringer, “The excitation spectrum for weakly interacting
Bosons in a trap,” Communications in Mathematical Physics, vol. 322, no.
2. Springer, pp. 559–591, 2013.
ista: Grech P, Seiringer R. 2013. The excitation spectrum for weakly interacting
Bosons in a trap. Communications in Mathematical Physics. 322(2), 559–591.
mla: Grech, Philip, and Robert Seiringer. “The Excitation Spectrum for Weakly Interacting
Bosons in a Trap.” Communications in Mathematical Physics, vol. 322, no.
2, Springer, 2013, pp. 559–91, doi:10.1007/s00220-013-1736-8.
short: P. Grech, R. Seiringer, Communications in Mathematical Physics 322 (2013)
559–591.
date_created: 2018-12-11T11:57:29Z
date_published: 2013-09-01T00:00:00Z
date_updated: 2021-01-12T06:57:18Z
day: '01'
doi: 10.1007/s00220-013-1736-8
extern: 1
intvolume: ' 322'
issue: '2'
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1205.5259
month: '09'
oa: 1
page: 559 - 591
publication: Communications in Mathematical Physics
publication_status: published
publisher: Springer
publist_id: '4518'
quality_controlled: 0
status: public
title: The excitation spectrum for weakly interacting Bosons in a trap
type: journal_article
volume: 322
year: '2013'
...
---
_id: '2410'
abstract:
- lang: eng
text: 'Here, we describe a novel virulent bacteriophage that infects Bacillus weihenstephanensis,
isolated from soil in Austria. It is the first phage to be discovered that infects
this species. Here, we present the complete genome sequence of this podovirus. '
author:
- first_name: Rodrigo A
full_name: Fernandes Redondo, Rodrigo A
id: 409D5C96-F248-11E8-B48F-1D18A9856A87
last_name: Fernandes Redondo
orcid: 0000-0002-5837-2793
- first_name: Anne
full_name: Kupczok, Anne
id: 2BB22BC2-F248-11E8-B48F-1D18A9856A87
last_name: Kupczok
- first_name: Gertraud
full_name: Stift, Gertraud
id: 2DB195CA-F248-11E8-B48F-1D18A9856A87
last_name: Stift
- first_name: Jonathan P
full_name: Bollback, Jonathan P
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
citation:
ama: Fernandes Redondo RA, Kupczok A, Stift G, Bollback JP. Complete genome sequence
of the novel phage MG-B1 infecting bacillus weihenstephanensis. Genome Announcements.
2013;1(3). doi:10.1128/genomeA.00216-13
apa: Fernandes Redondo, R. A., Kupczok, A., Stift, G., & Bollback, J. P. (2013).
Complete genome sequence of the novel phage MG-B1 infecting bacillus weihenstephanensis.
Genome Announcements. American Society for Microbiology. https://doi.org/10.1128/genomeA.00216-13
chicago: Fernandes Redondo, Rodrigo A, Anne Kupczok, Gertraud Stift, and Jonathan
P Bollback. “Complete Genome Sequence of the Novel Phage MG-B1 Infecting Bacillus
Weihenstephanensis.” Genome Announcements. American Society for Microbiology,
2013. https://doi.org/10.1128/genomeA.00216-13.
ieee: R. A. Fernandes Redondo, A. Kupczok, G. Stift, and J. P. Bollback, “Complete
genome sequence of the novel phage MG-B1 infecting bacillus weihenstephanensis,”
Genome Announcements, vol. 1, no. 3. American Society for Microbiology,
2013.
ista: Fernandes Redondo RA, Kupczok A, Stift G, Bollback JP. 2013. Complete genome
sequence of the novel phage MG-B1 infecting bacillus weihenstephanensis. Genome
Announcements. 1(3).
mla: Fernandes Redondo, Rodrigo A., et al. “Complete Genome Sequence of the Novel
Phage MG-B1 Infecting Bacillus Weihenstephanensis.” Genome Announcements,
vol. 1, no. 3, American Society for Microbiology, 2013, doi:10.1128/genomeA.00216-13.
short: R.A. Fernandes Redondo, A. Kupczok, G. Stift, J.P. Bollback, Genome Announcements
1 (2013).
date_created: 2018-12-11T11:57:30Z
date_published: 2013-06-13T00:00:00Z
date_updated: 2021-01-12T06:57:19Z
day: '13'
ddc:
- '576'
department:
- _id: JoBo
- _id: LifeSc
doi: 10.1128/genomeA.00216-13
file:
- access_level: open_access
checksum: 0751ec74b695567e0cdf02aaf9c26829
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:36Z
date_updated: 2020-07-14T12:45:40Z
file_id: '5291'
file_name: IST-2015-398-v1+1_Genome_Announc.-2013-Redondo-.pdf
file_size: 130026
relation: main_file
file_date_updated: 2020-07-14T12:45:40Z
has_accepted_license: '1'
intvolume: ' 1'
issue: '3'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
publication: Genome Announcements
publication_status: published
publisher: American Society for Microbiology
publist_id: '4516'
pubrep_id: '398'
quality_controlled: '1'
scopus_import: 1
status: public
title: Complete genome sequence of the novel phage MG-B1 infecting bacillus weihenstephanensis
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 1
year: '2013'
...
---
_id: '2412'
abstract:
- lang: eng
text: 'Background: The CRISPR/Cas system is known to act as an adaptive and heritable
immune system in Eubacteria and Archaea. Immunity is encoded in an array of spacer
sequences. Each spacer can provide specific immunity to invasive elements that
carry the same or a similar sequence. Even in closely related strains, spacer
content is very dynamic and evolves quickly. Standard models of nucleotide evolutioncannot
be applied to quantify its rate of change since processes other than single nucleotide
changes determine its evolution.Methods We present probabilistic models that are
specific for spacer content evolution. They account for the different processes
of insertion and deletion. Insertions can be constrained to occur on one end only
or are allowed to occur throughout the array. One deletion event can affect one
spacer or a whole fragment of adjacent spacers. Parameters of the underlying models
are estimated for a pair of arrays by maximum likelihood using explicit ancestor
enumeration.Results Simulations show that parameters are well estimated on average
under the models presented here. There is a bias in the rate estimation when including
fragment deletions. The models also estimate times between pairs of strains. But
with increasing time, spacer overlap goes to zero, and thus there is an upper
bound on the distance that can be estimated. Spacer content similarities are displayed
in a distance based phylogeny using the estimated times.We use the presented models
to analyze different Yersinia pestis data sets and find that the results among
them are largely congruent. The models also capture the variation in diversity
of spacers among the data sets. A comparison of spacer-based phylogenies and Cas
gene phylogenies shows that they resolve very different time scales for this data
set.Conclusions The simulations and data analyses show that the presented models
are useful for quantifying spacer content evolution and for displaying spacer
content similarities of closely related strains in a phylogeny. This allows for
comparisons of different CRISPR arrays or for comparisons between CRISPR arrays
and nucleotide substitution rates.'
author:
- first_name: Anne
full_name: Kupczok, Anne
id: 2BB22BC2-F248-11E8-B48F-1D18A9856A87
last_name: Kupczok
- first_name: Jonathan P
full_name: Bollback, Jonathan P
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
citation:
ama: Kupczok A, Bollback JP. Probabilistic models for CRISPR spacer content evolution
. BMC Evolutionary Biology. 2013;13(1):54-54. doi:10.1186/1471-2148-13-54
apa: Kupczok, A., & Bollback, J. P. (2013). Probabilistic models for CRISPR
spacer content evolution . BMC Evolutionary Biology. BioMed Central. https://doi.org/10.1186/1471-2148-13-54
chicago: Kupczok, Anne, and Jonathan P Bollback. “Probabilistic Models for CRISPR
Spacer Content Evolution .” BMC Evolutionary Biology. BioMed Central, 2013.
https://doi.org/10.1186/1471-2148-13-54.
ieee: A. Kupczok and J. P. Bollback, “Probabilistic models for CRISPR spacer content
evolution ,” BMC Evolutionary Biology, vol. 13, no. 1. BioMed Central,
pp. 54–54, 2013.
ista: Kupczok A, Bollback JP. 2013. Probabilistic models for CRISPR spacer content
evolution . BMC Evolutionary Biology. 13(1), 54–54.
mla: Kupczok, Anne, and Jonathan P. Bollback. “Probabilistic Models for CRISPR Spacer
Content Evolution .” BMC Evolutionary Biology, vol. 13, no. 1, BioMed Central,
2013, pp. 54–54, doi:10.1186/1471-2148-13-54.
short: A. Kupczok, J.P. Bollback, BMC Evolutionary Biology 13 (2013) 54–54.
date_created: 2018-12-11T11:57:31Z
date_published: 2013-02-26T00:00:00Z
date_updated: 2021-01-12T06:57:20Z
day: '26'
ddc:
- '576'
department:
- _id: JoBo
doi: 10.1186/1471-2148-13-54
file:
- access_level: open_access
checksum: 029c7e0b198c19312b66ecce3cabb22f
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:17:15Z
date_updated: 2020-07-14T12:45:40Z
file_id: '5268'
file_name: IST-2015-397-v1+1_1471-2148-13-54.pdf
file_size: 518729
relation: main_file
file_date_updated: 2020-07-14T12:45:40Z
has_accepted_license: '1'
intvolume: ' 13'
issue: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: 54 - 54
publication: BMC Evolutionary Biology
publication_status: published
publisher: BioMed Central
publist_id: '4514'
pubrep_id: '397'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'Probabilistic models for CRISPR spacer content evolution '
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
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13
year: '2013'
...