---
_id: '4226'
abstract:
- lang: eng
text: 'In the developing fly wing, secreted morphogens such as Decapentaplegic (Dpp)
and Wingless (Wg) form gradients of concentration providing positional information.
Dpp forms a longer-range gradient than Wg. To understand how the range is controlled,
we measured the four key kinetic parameters governing morphogen spreading: the
production rate, the effective diffusion coefficient, the degradation rate, and
the immobile fraction. The four parameters had different values for Dpp versus
Wg. In addition, Dynamin-dependent endocytosis was required for spreading of Dpp,
but not Wg. Thus, the cellular mechanisms of Dpp and Wingless spreading are different:
Dpp spreading requires endocytic, intracellular trafficking.'
author:
- first_name: Anna
full_name: Anna Kicheva
id: 3959A2A0-F248-11E8-B48F-1D18A9856A87
last_name: Kicheva
orcid: 0000-0003-4509-4998
- first_name: Periklis
full_name: Pantazis, Periklis
last_name: Pantazis
- first_name: Tobias
full_name: Bollenbach, Tobias
last_name: Bollenbach
- first_name: Yannis
full_name: Kalaidzidis, Yannis
last_name: Kalaidzidis
- first_name: Thomas
full_name: Bittig, Thomas
last_name: Bittig
- first_name: Frank
full_name: Julicher, Frank
last_name: Julicher
- first_name: Marcos
full_name: Gonzalez-Gaitan, Marcos
last_name: Gonzalez Gaitan
citation:
ama: Kicheva A, Pantazis P, Bollenbach T, et al. Kinetics of morphogen gradient
formation. Science. 2007;315(5811):521-525. doi:10.1126/science.1135774
apa: Kicheva, A., Pantazis, P., Bollenbach, T., Kalaidzidis, Y., Bittig, T., Julicher,
F., & Gonzalez Gaitan, M. (2007). Kinetics of morphogen gradient formation.
Science. American Association for the Advancement of Science. https://doi.org/10.1126/science.1135774
chicago: Kicheva, Anna, Periklis Pantazis, Tobias Bollenbach, Yannis Kalaidzidis,
Thomas Bittig, Frank Julicher, and Marcos Gonzalez Gaitan. “Kinetics of Morphogen
Gradient Formation.” Science. American Association for the Advancement
of Science, 2007. https://doi.org/10.1126/science.1135774.
ieee: A. Kicheva et al., “Kinetics of morphogen gradient formation,” Science,
vol. 315, no. 5811. American Association for the Advancement of Science, pp. 521–525,
2007.
ista: Kicheva A, Pantazis P, Bollenbach T, Kalaidzidis Y, Bittig T, Julicher F,
Gonzalez Gaitan M. 2007. Kinetics of morphogen gradient formation. Science. 315(5811),
521–525.
mla: Kicheva, Anna, et al. “Kinetics of Morphogen Gradient Formation.” Science,
vol. 315, no. 5811, American Association for the Advancement of Science, 2007,
pp. 521–25, doi:10.1126/science.1135774.
short: A. Kicheva, P. Pantazis, T. Bollenbach, Y. Kalaidzidis, T. Bittig, F. Julicher,
M. Gonzalez Gaitan, Science 315 (2007) 521–525.
date_created: 2018-12-11T12:07:42Z
date_published: 2007-01-26T00:00:00Z
date_updated: 2021-01-12T07:55:26Z
day: '26'
doi: 10.1126/science.1135774
extern: 1
intvolume: ' 315'
issue: '5811'
month: '01'
page: 521 - 525
publication: Science
publication_status: published
publisher: American Association for the Advancement of Science
publist_id: '1892'
quality_controlled: 0
status: public
title: Kinetics of morphogen gradient formation
type: journal_article
volume: 315
year: '2007'
...
---
_id: '4233'
article_processing_charge: No
author:
- first_name: Harold
full_name: Vladar, Harold
id: 2A181218-F248-11E8-B48F-1D18A9856A87
last_name: Vladar
orcid: 0000-0002-5985-7653
citation:
ama: 'de Vladar H. Alternativas prebióticas para la síntesis de amino- ácidos y
otras moléculas relacionadas. In: Falcón N, Loyo De Sardi Y, eds. Consejo de Desarrollo
Cientifico y Tecnologico; 2007:91-109.'
apa: 'de Vladar, H. (2007). Alternativas prebióticas para la síntesis de amino-
ácidos y otras moléculas relacionadas. In N. Falcón & Y. Loyo De Sardi (Eds.)
(pp. 91–109). Presented at the Ab Initio: Orígenes Del Universo, La Vida, Y La
Inteligencia, Consejo de Desarrollo Cientifico y Tecnologico.'
chicago: Vladar, Harold de. “Alternativas Prebióticas Para La Síntesis de Amino-
Ácidos y Otras Moléculas Relacionadas.” edited by N. Falcón and Y. Loyo De Sardi,
91–109. Consejo de Desarrollo Cientifico y Tecnologico, 2007.
ieee: 'H. de Vladar, “Alternativas prebióticas para la síntesis de amino- ácidos
y otras moléculas relacionadas,” presented at the Ab Initio: Orígenes Del Universo,
La Vida, Y La Inteligencia, 2007, pp. 91–109.'
ista: 'de Vladar H. 2007. Alternativas prebióticas para la síntesis de amino- ácidos
y otras moléculas relacionadas. Ab Initio: Orígenes Del Universo, La Vida, Y La
Inteligencia, 91–109.'
mla: de Vladar, Harold. Alternativas Prebióticas Para La Síntesis de Amino- Ácidos
y Otras Moléculas Relacionadas. Edited by N. Falcón and Y. Loyo De Sardi,
Consejo de Desarrollo Cientifico y Tecnologico, 2007, pp. 91–109.
short: H. de Vladar, in:, N. Falcón, Y. Loyo De Sardi (Eds.), Consejo de Desarrollo
Cientifico y Tecnologico, 2007, pp. 91–109.
conference:
name: 'Ab Initio: Orígenes Del Universo, La Vida, Y La Inteligencia'
date_created: 2018-12-11T12:07:45Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2025-07-01T13:09:25Z
day: '01'
editor:
- first_name: N.
full_name: Falcón, N.
last_name: Falcón
- first_name: Y.
full_name: Loyo De Sardi, Y.
last_name: Loyo De Sardi
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 91 - 109
publication_status: published
publisher: Consejo de Desarrollo Cientifico y Tecnologico
publist_id: '1880'
status: public
title: Alternativas prebióticas para la síntesis de amino- ácidos y otras moléculas
relacionadas
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2007'
...
---
_id: '4234'
abstract:
- lang: eng
text: We study a generalised model of population growth in which the state variable
is population growth rate instead of population size. Stochastic parametric perturbations,
modelling phenotypic variability, lead to a Langevin system with two sources of
multiplicative noise. The stationary probability distributions have two characteristic
power-law scales. Numerical simulations show that noise suppresses the explosion
of the growth rate which occurs in the deterministic counterpart. Instead, in
different parameter regimes populations will grow with "anomalous" stochastic
rates and (i) stabilise at "random carrying capacities", or (ii) go
extinct in random times. Using logistic fits to reconstruct the simulated data,
we find that even highly significant estimations do not recover or reflect information
about the deterministic part of the process. Therefore, the logistic interpretation
is not biologically meaningful. These results have implications for distinct model-aided
calculations in biological situations because these kinds of estimations could
lead to spurious conclusions. (c) 2006 Elsevier B.V. All rights reserved.
article_processing_charge: No
arxiv: 1
author:
- first_name: Harold
full_name: de Vladar, Harold
id: 2A181218-F248-11E8-B48F-1D18A9856A87
last_name: de Vladar
orcid: 0000-0002-5985-7653
- first_name: I.
full_name: Pen, I.
last_name: Pen
citation:
ama: de Vladar H, Pen I. Determinism, noise, and spurious estimations in a generalised
model of population growth. Physica A. 2007;373:477-485. doi:10.1016/j.physa.2006.06.025
apa: de Vladar, H., & Pen, I. (2007). Determinism, noise, and spurious estimations
in a generalised model of population growth. Physica A. Elsevier. https://doi.org/10.1016/j.physa.2006.06.025
chicago: Vladar, Harold de, and I. Pen. “Determinism, Noise, and Spurious Estimations
in a Generalised Model of Population Growth.” Physica A. Elsevier, 2007.
https://doi.org/10.1016/j.physa.2006.06.025.
ieee: H. de Vladar and I. Pen, “Determinism, noise, and spurious estimations in
a generalised model of population growth,” Physica A, vol. 373. Elsevier,
pp. 477–485, 2007.
ista: de Vladar H, Pen I. 2007. Determinism, noise, and spurious estimations in
a generalised model of population growth. Physica A. 373, 477–485.
mla: de Vladar, Harold, and I. Pen. “Determinism, Noise, and Spurious Estimations
in a Generalised Model of Population Growth.” Physica A, vol. 373, Elsevier,
2007, pp. 477–85, doi:10.1016/j.physa.2006.06.025.
short: H. de Vladar, I. Pen, Physica A 373 (2007) 477–485.
date_created: 2018-12-11T12:07:45Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:55:30Z
day: '01'
doi: 10.1016/j.physa.2006.06.025
extern: '1'
external_id:
arxiv:
- abs/q-bio/0602018
intvolume: ' 373'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/q-bio/0602018
month: '01'
oa: 1
oa_version: Preprint
page: 477 - 485
publication: Physica A
publication_status: published
publisher: Elsevier
publist_id: '1881'
status: public
title: Determinism, noise, and spurious estimations in a generalised model of population
growth
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 373
year: '2007'
...
---
_id: '4246'
abstract:
- lang: eng
text: Gaia theory, which describes the life–environment system of the Earth as stable
and self-regulating, has remained at the fringes of mainstream biological science
owing to its historically inadequate definition and apparent incompatibility with
individual-level natural selection. The key issue is whether and why the biosphere
might tend towards stability and self-regulation. We review the various ways in
which these issues have been addressed by evolutionary and ecological theory,
and relate these to ‘Gaia theory’. We then ask how this theory extends the perspectives
offered by these disciplines, and how it might be tested by novel modelling approaches
and laboratory experiments using emergent technologies.
author:
- first_name: Andrew
full_name: Free, Andrew
last_name: Free
- first_name: Nicholas H
full_name: Nicholas Barton
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: Free A, Barton NH. Do evolution and ecology need the Gaia hypothesis? Trends
in Ecology and Evolution. 2007;22(11):611-619. doi:10.1016/j.tree.2007.07.007
apa: Free, A., & Barton, N. H. (2007). Do evolution and ecology need the Gaia
hypothesis? Trends in Ecology and Evolution. Cell Press. https://doi.org/10.1016/j.tree.2007.07.007
chicago: Free, Andrew, and Nicholas H Barton. “Do Evolution and Ecology Need the
Gaia Hypothesis?” Trends in Ecology and Evolution. Cell Press, 2007. https://doi.org/10.1016/j.tree.2007.07.007.
ieee: A. Free and N. H. Barton, “Do evolution and ecology need the Gaia hypothesis?,”
Trends in Ecology and Evolution, vol. 22, no. 11. Cell Press, pp. 611–619,
2007.
ista: Free A, Barton NH. 2007. Do evolution and ecology need the Gaia hypothesis?
Trends in Ecology and Evolution. 22(11), 611–619.
mla: Free, Andrew, and Nicholas H. Barton. “Do Evolution and Ecology Need the Gaia
Hypothesis?” Trends in Ecology and Evolution, vol. 22, no. 11, Cell Press,
2007, pp. 611–19, doi:10.1016/j.tree.2007.07.007.
short: A. Free, N.H. Barton, Trends in Ecology and Evolution 22 (2007) 611–619.
date_created: 2018-12-11T12:07:49Z
date_published: 2007-11-01T00:00:00Z
date_updated: 2021-01-12T07:55:35Z
day: '01'
doi: 10.1016/j.tree.2007.07.007
extern: 1
intvolume: ' 22'
issue: '11'
month: '11'
page: 611 - 619
publication: Trends in Ecology and Evolution
publication_status: published
publisher: Cell Press
publist_id: '1856'
quality_controlled: 0
status: public
title: Do evolution and ecology need the Gaia hypothesis?
type: journal_article
volume: 22
year: '2007'
...
---
_id: '4247'
abstract:
- lang: eng
text: Evolution at multiple gene positions is complicated. Direct selection on one
gene disturbs the evolutionary dynamics of associated genes. Recent years have
seen the development of a multilocus methodology for modeling evolution at arbitrary
numbers of gene positions with arbitrary dominance and epistatic relations, mode
of inheritance, genetic linkage, and recombination. We show that the approach
is conceptually analogous to social evolutionary methodology, which focuses on
selection acting on associated individuals. In doing so, we (1) make explicit
the links between the multilocus methodology and the foundations of social evolution
theory, namely, Price’s theorem and Hamilton’s rule; (2) relate the multilocus
approach to levels‐of‐selection and neighbor‐modulated‐fitness approaches in social
evolution; (3) highlight the equivalence between genetical hitchhiking and kin
selection; (4) demonstrate that the multilocus methodology allows for social evolutionary
analyses involving coevolution of multiple traits and genetical associations between
nonrelatives, including individuals of different species; (5) show that this methodology
helps solve problems of dynamic sufficiency in social evolution theory; (6) form
links between invasion criteria in multilocus systems and Hamilton’s rule of kin
selection; (7) illustrate the generality and exactness of Hamilton’s rule, which
has previously been described as an approximate, heuristic result.
author:
- first_name: Andy
full_name: Gardner, Andy
last_name: Gardner
- first_name: Stuart
full_name: West, Stuart A
last_name: West
- first_name: Nicholas H
full_name: Nicholas Barton
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: Gardner A, West S, Barton NH. The relation between multilocus population genetics
and social evolution theory. American Naturalist. 2007;169(2):207-226.
doi:10.1086/510602
apa: Gardner, A., West, S., & Barton, N. H. (2007). The relation between multilocus
population genetics and social evolution theory. American Naturalist. University
of Chicago Press. https://doi.org/10.1086/510602
chicago: Gardner, Andy, Stuart West, and Nicholas H Barton. “The Relation between
Multilocus Population Genetics and Social Evolution Theory.” American Naturalist.
University of Chicago Press, 2007. https://doi.org/10.1086/510602.
ieee: A. Gardner, S. West, and N. H. Barton, “The relation between multilocus population
genetics and social evolution theory,” American Naturalist, vol. 169, no.
2. University of Chicago Press, pp. 207–226, 2007.
ista: Gardner A, West S, Barton NH. 2007. The relation between multilocus population
genetics and social evolution theory. American Naturalist. 169(2), 207–226.
mla: Gardner, Andy, et al. “The Relation between Multilocus Population Genetics
and Social Evolution Theory.” American Naturalist, vol. 169, no. 2, University
of Chicago Press, 2007, pp. 207–26, doi:10.1086/510602.
short: A. Gardner, S. West, N.H. Barton, American Naturalist 169 (2007) 207–226.
date_created: 2018-12-11T12:07:50Z
date_published: 2007-02-01T00:00:00Z
date_updated: 2021-01-12T07:55:35Z
day: '01'
doi: 10.1086/510602
extern: 1
intvolume: ' 169'
issue: '2'
month: '02'
page: 207 - 226
publication: American Naturalist
publication_status: published
publisher: University of Chicago Press
publist_id: '1857'
quality_controlled: 0
status: public
title: The relation between multilocus population genetics and social evolution theory
type: journal_article
volume: 169
year: '2007'
...
---
_id: '4342'
abstract:
- lang: eng
text: "Library 2.0 and user-generated content are two terms, which are closely connected.
In the\r\n\r\npresentation, I will briefly define both terms. Two example projects
where user- generated content and libraries interact will be presented. The cooperation
of Wikipedia and the Personennamendatei, the German cooperative name authority
files is the first. The second will be Wikisource where users provide transcribed
source material. Another important area of user-generated content is social tagging
where users index different resources. And if the users will do so much in the
future, is there still a place for librarians? But in the future user\r\n\r\nand
librarians become partners and the library will provide the platform: the library
2.0."
author:
- first_name: Patrick
full_name: Danowski, Patrick
id: 2EBD1598-F248-11E8-B48F-1D18A9856A87
last_name: Danowski
orcid: 0000-0002-6026-4409
citation:
ama: 'Danowski P. Library 2.0 and User-Generated Content - What can the users do
for us? In: IFLA; 2007. doi:601'
apa: 'Danowski, P. (2007). Library 2.0 and User-Generated Content - What can the
users do for us? Presented at the WLIC: World Library and Information Congress,
Durban, South Africa: IFLA. https://doi.org/601'
chicago: Danowski, Patrick. “Library 2.0 and User-Generated Content - What Can the
Users Do for Us?” IFLA, 2007. https://doi.org/601.
ieee: 'P. Danowski, “Library 2.0 and User-Generated Content - What can the users
do for us?,” presented at the WLIC: World Library and Information Congress, Durban,
South Africa, 2007.'
ista: 'Danowski P. 2007. Library 2.0 and User-Generated Content - What can the users
do for us? WLIC: World Library and Information Congress.'
mla: Danowski, Patrick. Library 2.0 and User-Generated Content - What Can the
Users Do for Us? IFLA, 2007, doi:601.
short: P. Danowski, in:, IFLA, 2007.
conference:
end_date: 2007-08-23
location: Durban, South Africa
name: 'WLIC: World Library and Information Congress'
start_date: 2007-08-19
date_created: 2018-12-11T12:08:22Z
date_published: 2007-05-25T00:00:00Z
date_updated: 2021-01-12T07:56:16Z
day: '25'
doi: '601'
extern: '1'
language:
- iso: eng
main_file_link:
- url: http://www.ifla.org/IV/ifla73/papers/113-Danowski-en.pdf
month: '05'
oa_version: None
publication_status: published
publisher: IFLA
publist_id: '1232'
status: public
title: Library 2.0 and User-Generated Content - What can the users do for us?
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2007'
...
---
_id: '4343'
abstract:
- lang: eng
text: 'Wikipedia and libraries share the same goal: simple and fast knowledge transfer.
Through linking different information resources on the Internet, knowledge gets
comprehensively accessible. The co-operation with the Personennamendatei, the
German authority file for names of persons is an example for linking between Wikipedia
and library catalogs. The article highlights, how this co-operation works and
what the benefits are.'
- lang: ger
text: 'Wikipedia und Bibliotheken haben das gleiche Ziel: die einfache und schnelle
Wissensvermittlung. Mit der Vernetzung der unterschiedlichen Informationsangebote
im Internet wird Wissen umfassend zugänglich gemacht. Ein Beispiel für die Vernetzung
zwischen Wikipedia und Bibliothekskatalogen ist die Kooperation mit der Personennamendatei,
der Normdatei für Personennamen. Der Artikel möchte beleuchten, wie diese Kooperation
funktioniert und welchen Nutzen sie hat.'
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: Barbara
full_name: Pfeifer, Barbara
last_name: Pfeifer
citation:
ama: 'Danowski P, Pfeifer B. Wikipedia und Normdateien: Wege der Vernetzung am Beispiel
der Kooperation mit der Personennamendatei. Bibliothek - Forschung und Praxis.
2007;31(2):149-155. doi:10.1515/BFUP.2007.149'
apa: 'Danowski, P., & Pfeifer, B. (2007). Wikipedia und Normdateien: Wege der
Vernetzung am Beispiel der Kooperation mit der Personennamendatei. Bibliothek
- Forschung Und Praxis. De Gruyter. https://doi.org/10.1515/BFUP.2007.149'
chicago: 'Danowski, Patrick, and Barbara Pfeifer. “Wikipedia Und Normdateien: Wege
Der Vernetzung Am Beispiel Der Kooperation Mit Der Personennamendatei.” Bibliothek
- Forschung Und Praxis. De Gruyter, 2007. https://doi.org/10.1515/BFUP.2007.149.'
ieee: 'P. Danowski and B. Pfeifer, “Wikipedia und Normdateien: Wege der Vernetzung
am Beispiel der Kooperation mit der Personennamendatei,” Bibliothek - Forschung
und Praxis, vol. 31, no. 2. De Gruyter, pp. 149–155, 2007.'
ista: 'Danowski P, Pfeifer B. 2007. Wikipedia und Normdateien: Wege der Vernetzung
am Beispiel der Kooperation mit der Personennamendatei. Bibliothek - Forschung
und Praxis. 31(2), 149–155.'
mla: 'Danowski, Patrick, and Barbara Pfeifer. “Wikipedia Und Normdateien: Wege Der
Vernetzung Am Beispiel Der Kooperation Mit Der Personennamendatei.” Bibliothek
- Forschung Und Praxis, vol. 31, no. 2, De Gruyter, 2007, pp. 149–55, doi:10.1515/BFUP.2007.149.'
short: P. Danowski, B. Pfeifer, Bibliothek - Forschung Und Praxis 31 (2007) 149–155.
date_created: 2018-12-11T12:08:22Z
date_published: 2007-08-01T00:00:00Z
date_updated: 2025-07-01T13:08:51Z
day: '01'
doi: 10.1515/BFUP.2007.149
extern: '1'
intvolume: ' 31'
issue: '2'
language:
- iso: eng
month: '08'
oa_version: None
page: 149 - 155
publication: Bibliothek - Forschung und Praxis
publication_status: published
publisher: De Gruyter
publist_id: '1231'
status: public
title: 'Wikipedia und Normdateien: Wege der Vernetzung am Beispiel der Kooperation
mit der Personennamendatei'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 31
year: '2007'
...
---
_id: '4344'
abstract:
- lang: ger
text: Anknüpfend an ihren Aufsatz „Bibliothek 2.0 – Die Zukunft der Bibliothek?“
(2006) geben Patrick Danowski und Lambert Heller, verantwortlich für das Schwerpunktthema
der vorliegenden Ausgabe, einen Überblick über den erreichten Diskussionsstand
über verschiedene Teilaspekte der Bibliothek 2.0 unter besonderer Berücksichtigung
der deutschen Fachöffentlichkeit. Einige charakteristische Fragen und Probleme
der Weiterentwicklung, Öffnung und Vernetzung bibliothekarischer Dienste und Informationen
werden angesprochen.
- lang: eng
text: Following up their article „Bibliothek 2.0 – Die Zukunft der Bibliothek?“
(„Library 2.0 – The future of the library?“) (2006), Patrick Danowski and Lambert
Heller, responsible for the main focus of this issue, give an outline of some
recently discussed library 2.0 topics, especially in respect to the professional
community in germany. Some characteristic questions and problems of the development,
opening and networking of library Services and information are mentioned.
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: Lambert
full_name: Heller, Lambert
last_name: Heller
citation:
ama: Danowski P, Heller L. Bibliothek 2.0? Wird alles anders? Bibliothek - Forschung
und Praxis. 2007;31(2):130-136. doi:10.1515/BFUP.2007.130
apa: Danowski, P., & Heller, L. (2007). Bibliothek 2.0? Wird alles anders? Bibliothek
- Forschung Und Praxis. De Gruyter. https://doi.org/10.1515/BFUP.2007.130
chicago: Danowski, Patrick, and Lambert Heller. “Bibliothek 2.0? Wird Alles Anders?”
Bibliothek - Forschung Und Praxis. De Gruyter, 2007. https://doi.org/10.1515/BFUP.2007.130.
ieee: P. Danowski and L. Heller, “Bibliothek 2.0? Wird alles anders?,” Bibliothek
- Forschung und Praxis, vol. 31, no. 2. De Gruyter, pp. 130–136, 2007.
ista: Danowski P, Heller L. 2007. Bibliothek 2.0? Wird alles anders? Bibliothek
- Forschung und Praxis. 31(2), 130–136.
mla: Danowski, Patrick, and Lambert Heller. “Bibliothek 2.0? Wird Alles Anders?”
Bibliothek - Forschung Und Praxis, vol. 31, no. 2, De Gruyter, 2007, pp.
130–36, doi:10.1515/BFUP.2007.130.
short: P. Danowski, L. Heller, Bibliothek - Forschung Und Praxis 31 (2007) 130–136.
date_created: 2018-12-11T12:08:22Z
date_published: 2007-08-01T00:00:00Z
date_updated: 2025-07-01T13:06:48Z
day: '01'
doi: 10.1515/BFUP.2007.130
extern: '1'
intvolume: ' 31'
issue: '2'
language:
- iso: eng
month: '08'
oa_version: None
page: 130 - 136
publication: Bibliothek - Forschung und Praxis
publication_status: published
publisher: De Gruyter
publist_id: '1230'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Bibliothek 2.0? Wird alles anders?
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 31
year: '2007'
...
---
_id: '4353'
abstract:
- lang: eng
text: 'BACKGROUND: The invention of the Genome Sequence 20 DNA Sequencing System
(454 parallel sequencing platform) has enabled the rapid and high-volume production
of sequence data. Until now, however, individual emulsion PCR (emPCR) reactions
and subsequent sequencing runs have been unable to combine template DNA from multiple
individuals, as homologous sequences cannot be subsequently assigned to their
original sources. METHODOLOGY: We use conventional PCR with 5''-nucleotide tagged
primers to generate homologous DNA amplification products from multiple specimens,
followed by sequencing through the high-throughput Genome Sequence 20 DNA Sequencing
System (GS20, Roche/454 Life Sciences). Each DNA sequence is subsequently traced
back to its individual source through 5''tag-analysis. CONCLUSIONS: We demonstrate
that this new approach enables the assignment of virtually all the generated DNA
sequences to the correct source once sequencing anomalies are accounted for (miss-assignment
rate<0.4%). Therefore, the method enables accurate sequencing and assignment
of homologous DNA sequences from multiple sources in single high-throughput GS20
run. We observe a bias in the distribution of the differently tagged primers that
is dependent on the 5'' nucleotide of the tag. In particular, primers 5'' labelled
with a cytosine are heavily overrepresented among the final sequences, while those
5'' labelled with a thymine are strongly underrepresented. A weaker bias also
exists with regards to the distribution of the sequences as sorted by the second
nucleotide of the dinucleotide tags. As the results are based on a single GS20
run, the general applicability of the approach requires confirmation. However,
our experiments demonstrate that 5''primer tagging is a useful method in which
the sequencing power of the GS20 can be applied to PCR-based assays of multiple
homologous PCR products. The new approach will be of value to a broad range of
research areas, such as those of comparative genomics, complete mitochondrial
analyses, population genetics, and phylogenetics.'
acknowledgement: JB and EW were supported by the Wellcome Trust, UK, the Carlsberg
Foundation, DK, and the National Science Foundation, DK. MTPG acknowledges the Marie
Curie Actions FP6-MEIF-CT-2005-025002 ‘FORMAPLEX’ grant for funding his research.
JPB and RN were funded by the Danish FSS and the National Science Foundation, DK.
None of the sponsors or funders have had any influence on the data or manuscript
presented here.
author:
- first_name: Jonas
full_name: Binladen, Jonas
last_name: Binladen
- first_name: M Thomas
full_name: Gilbert, M Thomas
last_name: Gilbert
- first_name: Jonathan P
full_name: Jonathan Bollback
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
- first_name: Frank
full_name: Panitz, Frank
last_name: Panitz
- first_name: Christian
full_name: Bendixen, Christian
last_name: Bendixen
- first_name: Rasmus
full_name: Nielsen, Rasmus
last_name: Nielsen
- first_name: Eske
full_name: Willerslev, Eske
last_name: Willerslev
citation:
ama: Binladen J, Gilbert MT, Bollback JP, et al. The use of coded PCR primers enables
high-throughput sequencing of multiple homolog amplification products by 454 parallel
sequencing. PLoS One. 2007;2(2). doi:10.1371/journal.pone.0000197
apa: Binladen, J., Gilbert, M. T., Bollback, J. P., Panitz, F., Bendixen, C., Nielsen,
R., & Willerslev, E. (2007). The use of coded PCR primers enables high-throughput
sequencing of multiple homolog amplification products by 454 parallel sequencing.
PLoS One. Public Library of Science. https://doi.org/10.1371/journal.pone.0000197
chicago: Binladen, Jonas, M Thomas Gilbert, Jonathan P Bollback, Frank Panitz, Christian
Bendixen, Rasmus Nielsen, and Eske Willerslev. “The Use of Coded PCR Primers Enables
High-Throughput Sequencing of Multiple Homolog Amplification Products by 454 Parallel
Sequencing.” PLoS One. Public Library of Science, 2007. https://doi.org/10.1371/journal.pone.0000197.
ieee: J. Binladen et al., “The use of coded PCR primers enables high-throughput
sequencing of multiple homolog amplification products by 454 parallel sequencing,”
PLoS One, vol. 2, no. 2. Public Library of Science, 2007.
ista: Binladen J, Gilbert MT, Bollback JP, Panitz F, Bendixen C, Nielsen R, Willerslev
E. 2007. The use of coded PCR primers enables high-throughput sequencing of multiple
homolog amplification products by 454 parallel sequencing. PLoS One. 2(2).
mla: Binladen, Jonas, et al. “The Use of Coded PCR Primers Enables High-Throughput
Sequencing of Multiple Homolog Amplification Products by 454 Parallel Sequencing.”
PLoS One, vol. 2, no. 2, Public Library of Science, 2007, doi:10.1371/journal.pone.0000197.
short: J. Binladen, M.T. Gilbert, J.P. Bollback, F. Panitz, C. Bendixen, R. Nielsen,
E. Willerslev, PLoS One 2 (2007).
date_created: 2018-12-11T12:08:25Z
date_published: 2007-02-14T00:00:00Z
date_updated: 2021-01-12T07:56:21Z
day: '14'
doi: 10.1371/journal.pone.0000197
extern: 1
intvolume: ' 2'
issue: '2'
license: https://creativecommons.org/licenses/by/4.0/
month: '02'
publication: PLoS One
publication_status: published
publisher: Public Library of Science
publist_id: '1105'
quality_controlled: 0
status: public
title: The use of coded PCR primers enables high-throughput sequencing of multiple
homolog amplification products by 454 parallel sequencing
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
volume: 2
year: '2007'
...
---
_id: '4354'
abstract:
- lang: eng
text: Homology search is one of the most ubiquitous bioinformatic tasks, yet it
is unknown how effective the currently available tools are for identifying noncoding
RNAs (ncRNAs). In this work, we use reliable ncRNA data sets to assess the effectiveness
of methods such as BLAST, FASTA, HMMer, and Infernal. Surprisingly, the most popular
homology search methods are often the least accurate. As a result, many studies
have used inappropriate tools for their analyses. On the basis of our results,
we suggest homology search strategies using the currently available tools and
some directions for future development.
author:
- first_name: Eva
full_name: Freyhult, Eva K
last_name: Freyhult
- first_name: Jonathan P
full_name: Jonathan Bollback
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
- first_name: Paul
full_name: Gardner, Paul P
last_name: Gardner
citation:
ama: 'Freyhult E, Bollback JP, Gardner P. Exploring genomic dark matter: a critical
assessment of the performance of homology search methods on noncoding RNA. Genome
Research. 2007;17(1):117-125. doi:10.1101/gr.5890907'
apa: 'Freyhult, E., Bollback, J. P., & Gardner, P. (2007). Exploring genomic
dark matter: a critical assessment of the performance of homology search methods
on noncoding RNA. Genome Research. Cold Spring Harbor Laboratory Press.
https://doi.org/10.1101/gr.5890907'
chicago: 'Freyhult, Eva, Jonathan P Bollback, and Paul Gardner. “Exploring Genomic
Dark Matter: A Critical Assessment of the Performance of Homology Search Methods
on Noncoding RNA.” Genome Research. Cold Spring Harbor Laboratory Press,
2007. https://doi.org/10.1101/gr.5890907.'
ieee: 'E. Freyhult, J. P. Bollback, and P. Gardner, “Exploring genomic dark matter:
a critical assessment of the performance of homology search methods on noncoding
RNA,” Genome Research, vol. 17, no. 1. Cold Spring Harbor Laboratory Press,
pp. 117–25, 2007.'
ista: 'Freyhult E, Bollback JP, Gardner P. 2007. Exploring genomic dark matter:
a critical assessment of the performance of homology search methods on noncoding
RNA. Genome Research. 17(1), 117–25.'
mla: 'Freyhult, Eva, et al. “Exploring Genomic Dark Matter: A Critical Assessment
of the Performance of Homology Search Methods on Noncoding RNA.” Genome Research,
vol. 17, no. 1, Cold Spring Harbor Laboratory Press, 2007, pp. 117–25, doi:10.1101/gr.5890907.'
short: E. Freyhult, J.P. Bollback, P. Gardner, Genome Research 17 (2007) 117–25.
date_created: 2018-12-11T12:08:25Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:21Z
day: '01'
doi: 10.1101/gr.5890907
extern: 1
intvolume: ' 17'
issue: '1'
main_file_link:
- open_access: '0'
url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC1716261
month: '01'
page: 117 - 25
publication: Genome Research
publication_status: published
publisher: Cold Spring Harbor Laboratory Press
publist_id: '1106'
quality_controlled: 0
status: public
title: 'Exploring genomic dark matter: a critical assessment of the performance of
homology search methods on noncoding RNA'
type: journal_article
volume: 17
year: '2007'
...
---
_id: '4355'
abstract:
- lang: eng
text: When a beneficial mutation is fixed in a population that lacks recombination,
the genetic background linked to that mutation is fixed. As a result, beneficial
mutations on different backgrounds experience competition, or "clonal interference,"
that can cause asexual populations to evolve more slowly than their sexual counterparts.
Factors such as a large population size (N) and high mutation rates (mu) increase
the number of competing beneficial mutations, and hence are expected to increase
the intensity of clonal interference. However, recent theory suggests that, with
very large values of Nmu, the severity of clonal interference may instead decline.
The reason is that, with large Nmu, genomes including both beneficial mutations
are rapidly created by recurrent mutation, obviating the need for recombination.
Here, we analyze data from experimentally evolved asexual populations of a bacteriophage
and find that, in these nonrecombining populations with very large Nmu, recurrent
mutation does appear to ameliorate this cost of asexuality.
acknowledgement: R01 GM069801-08/GM/NIGMS NIH HHS/United States
author:
- first_name: Jonathan P
full_name: Jonathan Bollback
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
- first_name: John
full_name: Huelsenbeck, John P
last_name: Huelsenbeck
citation:
ama: Bollback JP, Huelsenbeck J. Clonal interference is alleviated by high mutation
rates in large populations. Molecular Biology and Evolution. 2007;24(6):1397-1406.
doi:10.1093/molbev/msm056
apa: Bollback, J. P., & Huelsenbeck, J. (2007). Clonal interference is alleviated
by high mutation rates in large populations. Molecular Biology and Evolution.
Oxford University Press. https://doi.org/10.1093/molbev/msm056
chicago: Bollback, Jonathan P, and John Huelsenbeck. “Clonal Interference Is Alleviated
by High Mutation Rates in Large Populations.” Molecular Biology and Evolution.
Oxford University Press, 2007. https://doi.org/10.1093/molbev/msm056.
ieee: J. P. Bollback and J. Huelsenbeck, “Clonal interference is alleviated by high
mutation rates in large populations,” Molecular Biology and Evolution,
vol. 24, no. 6. Oxford University Press, pp. 1397–1406, 2007.
ista: Bollback JP, Huelsenbeck J. 2007. Clonal interference is alleviated by high
mutation rates in large populations. Molecular Biology and Evolution. 24(6), 1397–1406.
mla: Bollback, Jonathan P., and John Huelsenbeck. “Clonal Interference Is Alleviated
by High Mutation Rates in Large Populations.” Molecular Biology and Evolution,
vol. 24, no. 6, Oxford University Press, 2007, pp. 1397–406, doi:10.1093/molbev/msm056.
short: J.P. Bollback, J. Huelsenbeck, Molecular Biology and Evolution 24 (2007)
1397–1406.
date_created: 2018-12-11T12:08:26Z
date_published: 2007-03-22T00:00:00Z
date_updated: 2021-01-12T07:56:22Z
day: '22'
doi: 10.1093/molbev/msm056
extern: 1
intvolume: ' 24'
issue: '6'
month: '03'
page: 1397 - 1406
publication: Molecular Biology and Evolution
publication_status: published
publisher: Oxford University Press
publist_id: '1104'
quality_controlled: 0
status: public
title: Clonal interference is alleviated by high mutation rates in large populations
type: journal_article
volume: 24
year: '2007'
...
---
_id: '4356'
abstract:
- lang: eng
text: We used a comparative genomics approach to identify genes that are under positive
selection in six strains of Escherichia coli and Shigella flexneri, including
five strains that are human pathogens. We find that positive selection targets
a wide range of different functions in the E. coli genome, including cell surface
proteins such as beta barrel porins, presumably because of the involvement of
these genes in evolutionary arms races with other bacteria, phages, and/or the
host immune system. Structural mapping of positively selected sites on trans-membrane
beta barrel porins reveals that the residues under positive selection occur almost
exclusively in the extracellular region of the proteins that are enriched with
sites known to be targets of phages, colicins, or the host immune system. More
surprisingly, we also find a number of other categories of genes that show very
strong evidence for positive selection, such as the enigmatic rhs elements and
transposases. Based on structural evidence, we hypothesize that the selection
acting on transposases is related to the genomic conflict between transposable
elements and the host genome.
author:
- first_name: Lise
full_name: Petersen, Lise
last_name: Petersen
- first_name: Jonathan P
full_name: Jonathan Bollback
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
- first_name: Matt
full_name: Dimmic, Matt
last_name: Dimmic
- first_name: Melissa
full_name: Hubisz, Melissa
last_name: Hubisz
- first_name: Rasmus
full_name: Nielsen, Rasmus
last_name: Nielsen
citation:
ama: Petersen L, Bollback JP, Dimmic M, Hubisz M, Nielsen R. Genes under positive
selection in Escherichia coli. Genome Research. 2007;17(9):1336-1343. doi:10.1101/gr.6254707
apa: Petersen, L., Bollback, J. P., Dimmic, M., Hubisz, M., & Nielsen, R. (2007).
Genes under positive selection in Escherichia coli. Genome Research. Cold
Spring Harbor Laboratory Press. https://doi.org/10.1101/gr.6254707
chicago: Petersen, Lise, Jonathan P Bollback, Matt Dimmic, Melissa Hubisz, and Rasmus
Nielsen. “Genes under Positive Selection in Escherichia Coli.” Genome Research.
Cold Spring Harbor Laboratory Press, 2007. https://doi.org/10.1101/gr.6254707.
ieee: L. Petersen, J. P. Bollback, M. Dimmic, M. Hubisz, and R. Nielsen, “Genes
under positive selection in Escherichia coli,” Genome Research, vol. 17,
no. 9. Cold Spring Harbor Laboratory Press, pp. 1336–1343, 2007.
ista: Petersen L, Bollback JP, Dimmic M, Hubisz M, Nielsen R. 2007. Genes under
positive selection in Escherichia coli. Genome Research. 17(9), 1336–1343.
mla: Petersen, Lise, et al. “Genes under Positive Selection in Escherichia Coli.”
Genome Research, vol. 17, no. 9, Cold Spring Harbor Laboratory Press, 2007,
pp. 1336–43, doi:10.1101/gr.6254707.
short: L. Petersen, J.P. Bollback, M. Dimmic, M. Hubisz, R. Nielsen, Genome Research
17 (2007) 1336–1343.
date_created: 2018-12-11T12:08:26Z
date_published: 2007-08-03T00:00:00Z
date_updated: 2021-01-12T07:56:22Z
day: '03'
doi: 10.1101/gr.6254707
extern: 1
intvolume: ' 17'
issue: '9'
month: '08'
page: 1336 - 1343
publication: Genome Research
publication_status: published
publisher: Cold Spring Harbor Laboratory Press
publist_id: '1103'
quality_controlled: 0
status: public
title: Genes under positive selection in Escherichia coli
type: journal_article
volume: 17
year: '2007'
...
---
_id: '4368'
abstract:
- lang: eng
text: In this paper we describe AMT, a tool for monitoring temporal properties of
continuous signals. We first introduce Stl/Psl, a specification formalism based
on the industrial standard language Psl and the real-time temporal logic Mitl,
extended with constructs that allow describing behaviors of real-valued variables.
The tool automatically builds property observers from an Stl/Psl specification
and checks, in an offline or incremental fashion, whether simulation traces satisfy
the property. The AMT tool is validated through a Flash memory case-study.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
citation:
ama: 'Nickovic D, Maler O. AMT: A property-based monitoring tool for analog systems.
In: 5th International Conference on Formal Modeling and Analysis of Timed Systems.
Vol 4763. Springer; 2007:304-319. doi:10.1007/978-3-540-75454-1_22'
apa: 'Nickovic, D., & Maler, O. (2007). AMT: A property-based monitoring tool
for analog systems. In 5th International Conference on Formal Modeling and
Analysis of Timed Systems (Vol. 4763, pp. 304–319). Salzburg, Austria: Springer.
https://doi.org/10.1007/978-3-540-75454-1_22'
chicago: 'Nickovic, Dejan, and Oded Maler. “AMT: A Property-Based Monitoring Tool
for Analog Systems.” In 5th International Conference on Formal Modeling and
Analysis of Timed Systems, 4763:304–19. Springer, 2007. https://doi.org/10.1007/978-3-540-75454-1_22.'
ieee: 'D. Nickovic and O. Maler, “AMT: A property-based monitoring tool for analog
systems,” in 5th International Conference on Formal Modeling and Analysis of
Timed Systems, Salzburg, Austria, 2007, vol. 4763, pp. 304–319.'
ista: 'Nickovic D, Maler O. 2007. AMT: A property-based monitoring tool for analog
systems. 5th International Conference on Formal Modeling and Analysis of Timed
Systems. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 4763,
304–319.'
mla: 'Nickovic, Dejan, and Oded Maler. “AMT: A Property-Based Monitoring Tool for
Analog Systems.” 5th International Conference on Formal Modeling and Analysis
of Timed Systems, vol. 4763, Springer, 2007, pp. 304–19, doi:10.1007/978-3-540-75454-1_22.'
short: D. Nickovic, O. Maler, in:, 5th International Conference on Formal Modeling
and Analysis of Timed Systems, Springer, 2007, pp. 304–319.
conference:
end_date: 2007-10-05
location: Salzburg, Austria
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
start_date: 2007-10-03
date_created: 2018-12-11T12:08:30Z
date_published: 2007-09-20T00:00:00Z
date_updated: 2025-07-01T13:02:22Z
day: '20'
doi: 10.1007/978-3-540-75454-1_22
extern: '1'
intvolume: ' 4763'
language:
- iso: eng
month: '09'
oa_version: None
page: 304 - 319
publication: 5th International Conference on Formal Modeling and Analysis of Timed
Systems
publication_status: published
publisher: Springer
publist_id: '1089'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'AMT: A property-based monitoring tool for analog systems'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 4763
year: '2007'
...
---
_id: '4370'
abstract:
- lang: eng
text: In this paper we propose a complete chain for synthesizing controllers from
high-level specifications. From real-time properties expressed in the logic mtl
we generate, under bounded-variability assumptions, deterministic timed automata
to which we apply safety synthesis algorithms to derive a controller that satisfies
the properties by construction. Some preliminary experimental results are reported.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
- first_name: Amir
full_name: Pnueli, Amir
last_name: Pnueli
citation:
ama: 'Maler O, Nickovic D, Pnueli A. On synthesizing controllers from bounded-response
properties. In: 19th International Conference on Computer Aided Verification.
Vol 4590. Springer; 2007:95-107. doi:10.1007/978-3-540-73368-3_12'
apa: 'Maler, O., Nickovic, D., & Pnueli, A. (2007). On synthesizing controllers
from bounded-response properties. In 19th International Conference on Computer
Aided Verification (Vol. 4590, pp. 95–107). Berlin, Germany: Springer. https://doi.org/10.1007/978-3-540-73368-3_12'
chicago: Maler, Oded, Dejan Nickovic, and Amir Pnueli. “On Synthesizing Controllers
from Bounded-Response Properties.” In 19th International Conference on Computer
Aided Verification, 4590:95–107. Springer, 2007. https://doi.org/10.1007/978-3-540-73368-3_12.
ieee: O. Maler, D. Nickovic, and A. Pnueli, “On synthesizing controllers from bounded-response
properties,” in 19th International Conference on Computer Aided Verification,
Berlin, Germany, 2007, vol. 4590, pp. 95–107.
ista: 'Maler O, Nickovic D, Pnueli A. 2007. On synthesizing controllers from bounded-response
properties. 19th International Conference on Computer Aided Verification. CAV:
Computer Aided Verification, LNCS, vol. 4590, 95–107.'
mla: Maler, Oded, et al. “On Synthesizing Controllers from Bounded-Response Properties.”
19th International Conference on Computer Aided Verification, vol. 4590,
Springer, 2007, pp. 95–107, doi:10.1007/978-3-540-73368-3_12.
short: O. Maler, D. Nickovic, A. Pnueli, in:, 19th International Conference on Computer
Aided Verification, Springer, 2007, pp. 95–107.
conference:
end_date: 2007-07-07
location: Berlin, Germany
name: 'CAV: Computer Aided Verification'
start_date: 2007-07-03
date_created: 2018-12-11T12:08:30Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2025-07-01T12:59:28Z
day: '01'
doi: 10.1007/978-3-540-73368-3_12
extern: '1'
intvolume: ' 4590'
language:
- iso: eng
month: '01'
oa_version: None
page: 95 - 107
publication: 19th International Conference on Computer Aided Verification
publication_status: published
publisher: Springer
publist_id: '1086'
quality_controlled: '1'
scopus_import: '1'
status: public
title: On synthesizing controllers from bounded-response properties
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 4590
year: '2007'
...
---
_id: '4394'
abstract:
- lang: eng
text: "This paper presents our integration of efficient resolution-based theorem
provers into the Jahob data structure verification system. Our experimental results
show that this approach enables Jahob to automatically verify the correctness
of a range of complex dynamically instantiable data structures, such as hash tables
and search trees, without the need for interactive theorem proving or techniques
tailored to individual data structures.\r\n\r\nOur primary technical results include:
(1) a translation from higher-order logic to first-order logic that enables the
application of resolution-based theorem provers and (2) a proof that eliminating
type (sort) information in formulas is both sound and complete, even in the presence
of a generic equality operator. Our experimental results show that the elimination
of type information often dramatically decreases the time required to prove the
resulting formulas.\r\n\r\nThese techniques enabled us to verify complex correctness
properties of Java programs such as a mutable set implemented as an imperative
linked list, a finite map implemented as a functional ordered tree, a hash table
with a mutable array, and a simple library system example that uses these container
data structures. Our system verifies (in a matter of minutes) that data structure
operations correctly update the finite map, that they preserve data structure
invariants (such as ordering of elements, membership in appropriate hash table
buckets, or relationships between sets and relations), and that there are no run-time
errors such as null dereferences or array out of bounds accesses."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Charles
full_name: Bouillaguet, Charles
last_name: Bouillaguet
- first_name: Viktor
full_name: Kuncak, Viktor
last_name: Kuncak
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Karen
full_name: Zee, Karen
last_name: Zee
- first_name: Martin
full_name: Rinard, Martin
last_name: Rinard
citation:
ama: 'Bouillaguet C, Kuncak V, Wies T, Zee K, Rinard M. Using first-order theorem
provers in the Jahob data structure verification system. In: 8th International
Conference on Verification, Model Checking, and Abstract Interpretation. Vol
4349. Springer; 2007:74-88. doi:10.1007/978-3-540-69738-1_5'
apa: 'Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., & Rinard, M. (2007). Using
first-order theorem provers in the Jahob data structure verification system. In
8th International Conference on Verification, Model Checking, and Abstract
Interpretation (Vol. 4349, pp. 74–88). Nice, France: Springer. https://doi.org/10.1007/978-3-540-69738-1_5'
chicago: Bouillaguet, Charles, Viktor Kuncak, Thomas Wies, Karen Zee, and Martin
Rinard. “Using First-Order Theorem Provers in the Jahob Data Structure Verification
System.” In 8th International Conference on Verification, Model Checking, and
Abstract Interpretation, 4349:74–88. Springer, 2007. https://doi.org/10.1007/978-3-540-69738-1_5.
ieee: C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M. Rinard, “Using first-order
theorem provers in the Jahob data structure verification system,” in 8th International
Conference on Verification, Model Checking, and Abstract Interpretation, Nice,
France, 2007, vol. 4349, pp. 74–88.
ista: 'Bouillaguet C, Kuncak V, Wies T, Zee K, Rinard M. 2007. Using first-order
theorem provers in the Jahob data structure verification system. 8th International
Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI:
Verification, Model Checking and Abstract Interpretation, LNCS, vol. 4349, 74–88.'
mla: Bouillaguet, Charles, et al. “Using First-Order Theorem Provers in the Jahob
Data Structure Verification System.” 8th International Conference on Verification,
Model Checking, and Abstract Interpretation, vol. 4349, Springer, 2007, pp.
74–88, doi:10.1007/978-3-540-69738-1_5.
short: C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, M. Rinard, in:, 8th International
Conference on Verification, Model Checking, and Abstract Interpretation, Springer,
2007, pp. 74–88.
conference:
end_date: 2007-01-16
location: Nice, France
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
start_date: 2007-01-14
date_created: 2018-12-11T12:08:37Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2025-07-01T12:57:14Z
day: '01'
doi: 10.1007/978-3-540-69738-1_5
extern: '1'
intvolume: ' 4349'
language:
- iso: eng
month: '01'
oa_version: None
page: 74 - 88
publication: 8th International Conference on Verification, Model Checking, and Abstract
Interpretation
publication_status: published
publisher: Springer
publist_id: '1062'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Using first-order theorem provers in the Jahob data structure verification
system
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 4349
year: '2007'
...
---
_id: '4398'
abstract:
- lang: eng
text: 'We propose a shape analysis that adapts to some of the complex composite
data structures found in industrial systems-level programs. Examples of such data
structures include “cyclic doubly-linked lists of acyclic singly-linked lists”,
“singly-linked lists of cyclic doubly-linked lists with back-pointers to head
nodes”, etc. The analysis introduces the use of generic higher-order inductive
predicates describing spatial relationships together with a method of synthesizing
new parameterized spatial predicates which can be used in combination with the
higher-order predicates. In order to evaluate the proposed approach for realistic
programs we have performed experiments on examples drawn from device drivers:
the analysis proved safety of the data structure manipulation of several routines
belonging to an IEEE 1394 (firewire) driver, and also found several previously
unknown memory safety bugs.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Josh
full_name: Berdine, Josh
last_name: Berdine
- first_name: Cristiano
full_name: Calcagno, Cristiano
last_name: Calcagno
- first_name: Byron
full_name: Cook, Byron
last_name: Cook
- first_name: Dino
full_name: Distefano, Dino
last_name: Distefano
- first_name: Peter
full_name: O'Hearn, Peter
last_name: O'Hearn
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Hongseok
full_name: Yang, Hongseok
last_name: Yang
citation:
ama: 'Berdine J, Calcagno C, Cook B, et al. Shape analysis for composite data structures.
In: 19th International Conference on Computer Aided Verification. Vol 4590.
Springer; 2007:178-192. doi:10.1007/978-3-540-73368-3_22'
apa: 'Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P., Wies, T.,
& Yang, H. (2007). Shape analysis for composite data structures. In 19th
International Conference on Computer Aided Verification (Vol. 4590, pp. 178–192).
Berlin, Germany: Springer. https://doi.org/10.1007/978-3-540-73368-3_22'
chicago: Berdine, Josh, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O’Hearn,
Thomas Wies, and Hongseok Yang. “Shape Analysis for Composite Data Structures.”
In 19th International Conference on Computer Aided Verification, 4590:178–92.
Springer, 2007. https://doi.org/10.1007/978-3-540-73368-3_22.
ieee: J. Berdine et al., “Shape analysis for composite data structures,”
in 19th International Conference on Computer Aided Verification, Berlin,
Germany, 2007, vol. 4590, pp. 178–192.
ista: 'Berdine J, Calcagno C, Cook B, Distefano D, O’Hearn P, Wies T, Yang H. 2007.
Shape analysis for composite data structures. 19th International Conference on
Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 4590,
178–192.'
mla: Berdine, Josh, et al. “Shape Analysis for Composite Data Structures.” 19th
International Conference on Computer Aided Verification, vol. 4590, Springer,
2007, pp. 178–92, doi:10.1007/978-3-540-73368-3_22.
short: J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O’Hearn, T. Wies, H. Yang,
in:, 19th International Conference on Computer Aided Verification, Springer, 2007,
pp. 178–192.
conference:
end_date: 2007-07-07
location: Berlin, Germany
name: 'CAV: Computer Aided Verification'
start_date: 2007-07-03
date_created: 2018-12-11T12:08:39Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2025-07-01T12:54:23Z
day: '01'
doi: 10.1007/978-3-540-73368-3_22
extern: '1'
intvolume: ' 4590'
language:
- iso: eng
month: '01'
oa_version: None
page: 178 - 192
publication: 19th International Conference on Computer Aided Verification
publication_status: published
publisher: Springer
publist_id: '1058'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Shape analysis for composite data structures
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 4590
year: '2007'
...
---
_id: '4399'
abstract:
- lang: eng
text: 'A temporal interface for a software component is a finite automaton that
specifies the legal sequences of calls to functions that are provided by the component.
We compare and evaluate three different algorithms for automatically extracting
temporal interfaces from program code: (1) a game algorithm that computes the
interface as a representation of the most general environment strategy to avoid
a safety violation; (2) a learning algorithm that repeatedly queries the program
to construct the minimal interface automaton; and (3) a CEGAR algorithm that iteratively
refines an abstract interface hypothesis by adding relevant program variables.
For comparison purposes, we present and implement the three algorithms in a unifying
formal setting. While the three algorithms compute the same output and have similar
worst-case complexities, their actual running times may differ considerably for
a given input program. On the theoretical side, we provide for each of the three
algorithms a family of input programs on which that algorithm outperforms the
two alternatives. On the practical side, we evaluate the three algorithms experimentally
on a variety of Java libraries. '
acknowledgement: This research was supported in part by the grant SFU/PRG 06-3, and
by the Swiss National Science Foundation.
alternative_title:
- LNCS
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Vasu
full_name: Vasu Singh
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: 'Beyer D, Henzinger TA, Singh V. Algorithms for interface synthesis. In: Vol
4590. Springer; 2007:4-19. doi:10.1007/978-3-540-73368-3_4'
apa: 'Beyer, D., Henzinger, T. A., & Singh, V. (2007). Algorithms for interface
synthesis (Vol. 4590, pp. 4–19). Presented at the CAV: Computer Aided Verification,
Springer. https://doi.org/10.1007/978-3-540-73368-3_4'
chicago: Beyer, Dirk, Thomas A Henzinger, and Vasu Singh. “Algorithms for Interface
Synthesis,” 4590:4–19. Springer, 2007. https://doi.org/10.1007/978-3-540-73368-3_4.
ieee: 'D. Beyer, T. A. Henzinger, and V. Singh, “Algorithms for interface synthesis,”
presented at the CAV: Computer Aided Verification, 2007, vol. 4590, pp. 4–19.'
ista: 'Beyer D, Henzinger TA, Singh V. 2007. Algorithms for interface synthesis.
CAV: Computer Aided Verification, LNCS, vol. 4590, 4–19.'
mla: Beyer, Dirk, et al. Algorithms for Interface Synthesis. Vol. 4590, Springer,
2007, pp. 4–19, doi:10.1007/978-3-540-73368-3_4.
short: D. Beyer, T.A. Henzinger, V. Singh, in:, Springer, 2007, pp. 4–19.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:39Z
date_published: 2007-07-02T00:00:00Z
date_updated: 2021-01-12T07:56:41Z
day: '02'
doi: 10.1007/978-3-540-73368-3_4
extern: 1
intvolume: ' 4590'
month: '07'
page: 4 - 19
publication_status: published
publisher: Springer
publist_id: '1059'
quality_controlled: 0
status: public
title: Algorithms for interface synthesis
type: conference
volume: 4590
year: '2007'
...
---
_id: '4402'
abstract:
- lang: eng
text: 'For specifying and verifying branching-time requirements, a reactive system
is traditionally modeled as a labeled tree, where a path in the tree encodes a
possible execution of the system. We propose to enrich such tree models with “jump-edges”
that capture observational indistinguishability: for an agent a, an a-labeled
edge is added between two nodes if the observable behaviors of the agent a along
the paths to these nodes are identical. We show that it is possible to specify
information flow properties and partial information games in temporal logics interpreted
on this enriched structure. We study complexity and decidability of the model
checking problem for these logics. We show that it is PSPACE-complete and EXPTIME-complete
respectively for fragments of CTL and μ-calculus-like logics. These fragments
are expressive enough to allow specifications of information flow properties such
as “agent A does not reveal x (a secret) until agent B reveals y (a password)”
and of partial information games.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Swarat
full_name: Chaudhuri, Swarat
last_name: Chaudhuri
citation:
ama: 'Alur R, Cerny P, Chaudhuri S. Model checking on trees with path equivalences.
In: 13th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems. Vol 4424. Springer; 2007:664-678. doi:10.1007/978-3-540-71209-1_51'
apa: 'Alur, R., Cerny, P., & Chaudhuri, S. (2007). Model checking on trees with
path equivalences. In 13th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems (Vol. 4424, pp. 664–678). Braga,
Portugal: Springer. https://doi.org/10.1007/978-3-540-71209-1_51'
chicago: Alur, Rajeev, Pavol Cerny, and Swarat Chaudhuri. “Model Checking on Trees
with Path Equivalences.” In 13th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, 4424:664–78. Springer, 2007.
https://doi.org/10.1007/978-3-540-71209-1_51.
ieee: R. Alur, P. Cerny, and S. Chaudhuri, “Model checking on trees with path equivalences,”
in 13th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems, Braga, Portugal, 2007, vol. 4424, pp. 664–678.
ista: 'Alur R, Cerny P, Chaudhuri S. 2007. Model checking on trees with path equivalences.
13th International Conference on Tools and Algorithms for the Construction and
Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis
of Systems, LNCS, vol. 4424, 664–678.'
mla: Alur, Rajeev, et al. “Model Checking on Trees with Path Equivalences.” 13th
International Conference on Tools and Algorithms for the Construction and Analysis
of Systems, vol. 4424, Springer, 2007, pp. 664–78, doi:10.1007/978-3-540-71209-1_51.
short: R. Alur, P. Cerny, S. Chaudhuri, in:, 13th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems, Springer, 2007, pp.
664–678.
conference:
end_date: 2007-04-01
location: Braga, Portugal
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
start_date: 2007-03-24
date_created: 2018-12-11T12:08:40Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2025-07-01T12:51:33Z
day: '01'
doi: 10.1007/978-3-540-71209-1_51
extern: '1'
intvolume: ' 4424'
language:
- iso: eng
month: '01'
oa_version: None
page: 664 - 678
publication: 13th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems
publication_status: published
publisher: Springer
publist_id: '1055'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Model checking on trees with path equivalences
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 4424
year: '2007'
...
---
_id: '4405'
abstract:
- lang: eng
text: |-
Background
A central goal of Systems Biology is to model and analyze biological signaling pathways that interact with one another to form complex networks. Here we introduce Qualitative networks, an extension of Boolean networks. With this framework, we use formal verification methods to check whether a model is consistent with the laboratory experimental observations on which it is based. If the model does not conform to the data, we suggest a revised model and the new hypotheses are tested in-silico.
Results
We consider networks in which elements range over a small finite domain allowing more flexibility than Boolean values, and add target functions that allow to model a rich set of behaviors. We propose a symbolic algorithm for analyzing the steady state of these networks, allowing us to scale up to a system consisting of 144 elements and state spaces of approximately 1086 states. We illustrate the usefulness of this approach through a model of the interaction between the Notch and the Wnt signaling pathways in mammalian skin, and its extensive analysis.
Conclusion
We introduce an approach for constructing computational models of biological systems that extends the framework of Boolean networks and uses formal verification methods for the analysis of the model. This approach can scale to multicellular models of complex pathways, and is therefore a useful tool for the analysis of complex biological systems. The hypotheses formulated during in-silico testing suggest new avenues to explore experimentally. Hence, this approach has the potential to efficiently complement experimental studies in biology.
author:
- first_name: Marc
full_name: Schaub, Marc A
last_name: Schaub
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jasmin
full_name: Fisher, Jasmin
last_name: Fisher
citation:
ama: 'Schaub M, Henzinger TA, Fisher J. Qualitative networks: A symbolic approach
to analyze biological signaling networks. BMC Systems Biology. 2007;1(4).
doi:10.1186/1752-0509-1-4'
apa: 'Schaub, M., Henzinger, T. A., & Fisher, J. (2007). Qualitative networks:
A symbolic approach to analyze biological signaling networks. BMC Systems Biology.
BioMed Central. https://doi.org/10.1186/1752-0509-1-4'
chicago: 'Schaub, Marc, Thomas A Henzinger, and Jasmin Fisher. “Qualitative Networks:
A Symbolic Approach to Analyze Biological Signaling Networks.” BMC Systems
Biology. BioMed Central, 2007. https://doi.org/10.1186/1752-0509-1-4.'
ieee: 'M. Schaub, T. A. Henzinger, and J. Fisher, “Qualitative networks: A symbolic
approach to analyze biological signaling networks,” BMC Systems Biology,
vol. 1, no. 4. BioMed Central, 2007.'
ista: 'Schaub M, Henzinger TA, Fisher J. 2007. Qualitative networks: A symbolic
approach to analyze biological signaling networks. BMC Systems Biology. 1(4).'
mla: 'Schaub, Marc, et al. “Qualitative Networks: A Symbolic Approach to Analyze
Biological Signaling Networks.” BMC Systems Biology, vol. 1, no. 4, BioMed
Central, 2007, doi:10.1186/1752-0509-1-4.'
short: M. Schaub, T.A. Henzinger, J. Fisher, BMC Systems Biology 1 (2007).
date_created: 2018-12-11T12:08:41Z
date_published: 2007-01-08T00:00:00Z
date_updated: 2021-01-12T07:56:44Z
day: '08'
doi: 10.1186/1752-0509-1-4
extern: 1
intvolume: ' 1'
issue: '4'
main_file_link:
- open_access: '0'
url: http://www.biomedcentral.com/1752-0509/1/4
month: '01'
publication: BMC Systems Biology
publication_status: published
publisher: BioMed Central
publist_id: '325'
quality_controlled: 0
status: public
title: 'Qualitative networks: A symbolic approach to analyze biological signaling
networks'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
volume: 1
year: '2007'
...
---
_id: '4417'
abstract:
- lang: eng
text: Counterexample-guided abstraction refinement (CEGAR) is a powerful technique
to scale automatic program analysis techniques to large programs. However, so
far it has been used primarily for model checking in the context of predicate
abstraction. We formalize CEGAR for general powerset domains. If a spurious abstract
counterexample needs to be removed through abstraction refinement, there are often
several choices, such as which program location(s) to refine, which abstract domain(s)
to use at different locations, and which abstract values to compute. We define
several plausible preference orderings on abstraction refinements, such as refining
as “late” as possible and as “coarse” as possible. We present generic algorithms
for finding refinements that are optimal with respect to the different preference
orderings. We also compare the different orderings with respect to desirable properties,
including the property if locally optimal refinements compose to a global optimum.
Finally, we point out some difficulties with CEGAR for non-powerset domains.
acknowledgement: This research is partially supported by the Clore Fellowship Programme.
Supported in part by the Swiss National Science Foundation.
alternative_title:
- LNCS
author:
- first_name: Roman
full_name: Manevich, Roman
last_name: Manevich
- first_name: John
full_name: Field, John
last_name: Field
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ganesan
full_name: Ramalingam, Ganesan
last_name: Ramalingam
- first_name: Mooly
full_name: Sagiv, Mooly
last_name: Sagiv
citation:
ama: 'Manevich R, Field J, Henzinger TA, Ramalingam G, Sagiv M. Abstract counterexample-based
refinement for powerset domains. In: Program Analysis and Compilation, Theory
and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th
Birthday. Vol 4444. Springer; 2007:273-292. doi:10.1007/978-3-540-71322-7_13'
apa: 'Manevich, R., Field, J., Henzinger, T. A., Ramalingam, G., & Sagiv, M.
(2007). Abstract counterexample-based refinement for powerset domains. In Program
Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm
on the Occasion of His 60th Birthday (Vol. 4444, pp. 273–292). Springer. https://doi.org/10.1007/978-3-540-71322-7_13'
chicago: 'Manevich, Roman, John Field, Thomas A Henzinger, Ganesan Ramalingam, and
Mooly Sagiv. “Abstract Counterexample-Based Refinement for Powerset Domains.”
In Program Analysis and Compilation, Theory and Practice: Essays Dedicated
to Reinhard Wilhelm on the Occasion of His 60th Birthday, 4444:273–92. Springer,
2007. https://doi.org/10.1007/978-3-540-71322-7_13.'
ieee: 'R. Manevich, J. Field, T. A. Henzinger, G. Ramalingam, and M. Sagiv, “Abstract
counterexample-based refinement for powerset domains,” in Program Analysis
and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on
the Occasion of His 60th Birthday, vol. 4444, Springer, 2007, pp. 273–292.'
ista: 'Manevich R, Field J, Henzinger TA, Ramalingam G, Sagiv M. 2007.Abstract counterexample-based
refinement for powerset domains. In: Program Analysis and Compilation, Theory
and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th
Birthday. LNCS, vol. 4444, 273–292.'
mla: 'Manevich, Roman, et al. “Abstract Counterexample-Based Refinement for Powerset
Domains.” Program Analysis and Compilation, Theory and Practice: Essays Dedicated
to Reinhard Wilhelm on the Occasion of His 60th Birthday, vol. 4444, Springer,
2007, pp. 273–92, doi:10.1007/978-3-540-71322-7_13.'
short: 'R. Manevich, J. Field, T.A. Henzinger, G. Ramalingam, M. Sagiv, in:, Program
Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm
on the Occasion of His 60th Birthday, Springer, 2007, pp. 273–292.'
date_created: 2018-12-11T12:08:45Z
date_published: 2007-03-30T00:00:00Z
date_updated: 2021-01-12T07:56:49Z
day: '30'
doi: 10.1007/978-3-540-71322-7_13
extern: 1
intvolume: ' 4444'
month: '03'
page: 273 - 292
publication: 'Program Analysis and Compilation, Theory and Practice: Essays Dedicated
to Reinhard Wilhelm on the Occasion of His 60th Birthday'
publication_status: published
publisher: Springer
publist_id: '314'
quality_controlled: 0
status: public
title: Abstract counterexample-based refinement for powerset domains
type: book_chapter
volume: 4444
year: '2007'
...