---
_id: '4344'
author:
- first_name: Patrick
full_name: Patrick Danowski
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(2007):130-136. doi:45
apa: Danowski, P., & Heller, L. (2007). Bibliothek 2.0 ? Wird alles anders?
Bibliothek - Forschung Und Praxis. De Gruyter. https://doi.org/45
chicago: Danowski, Patrick, and Lambert Heller. “Bibliothek 2.0 ? Wird Alles Anders?”
Bibliothek - Forschung Und Praxis. De Gruyter, 2007. https://doi.org/45.
ieee: P. Danowski and L. Heller, “Bibliothek 2.0 ? Wird alles anders?,” Bibliothek
- Forschung Und Praxis, vol. 31, no. 2007. De Gruyter, pp. 130–136, 2007.
ista: Danowski P, Heller L. 2007. Bibliothek 2.0 ? Wird alles anders? Bibliothek
- Forschung Und Praxis. 31(2007), 130–136.
mla: Danowski, Patrick, and Lambert Heller. “Bibliothek 2.0 ? Wird Alles Anders?”
Bibliothek - Forschung Und Praxis, vol. 31, no. 2007, De Gruyter, 2007,
pp. 130–36, doi:45.
short: P. Danowski, L. Heller, Bibliothek - Forschung Und Praxis 31 (2007) 130–136.
date_created: 2018-12-11T12:08:22Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:17Z
day: '01'
doi: '45'
extern: 1
intvolume: ' 31'
issue: '2007'
main_file_link:
- open_access: '0'
url: http://www.bibliothek-saur.de/2007_2/130-136.pdf
month: '01'
page: 130 - 136
publication: Bibliothek - Forschung Und Praxis
publication_status: published
publisher: De Gruyter
publist_id: '1230'
quality_controlled: 0
status: public
title: Bibliothek 2.0 ? Wird alles anders?
type: journal_article
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'
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'
alternative_title:
- LNCS
author:
- first_name: Dejan
full_name: Dejan Nickovic
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: Springer; 2007:304-319. doi:1567'
apa: 'Nickovic, D., & Maler, O. (2007). AMT: a property-based monitoring tool
for analog systems (pp. 304–319). Presented at the FORMATS: Formal Modeling and
Analysis of Timed Systems, Springer. https://doi.org/1567'
chicago: 'Nickovic, Dejan, and Oded Maler. “AMT: A Property-Based Monitoring Tool
for Analog Systems,” 304–19. Springer, 2007. https://doi.org/1567.'
ieee: 'D. Nickovic and O. Maler, “AMT: a property-based monitoring tool for analog
systems,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems,
2007, pp. 304–319.'
ista: 'Nickovic D, Maler O. 2007. AMT: a property-based monitoring tool for analog
systems. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, , 304–319.'
mla: 'Nickovic, Dejan, and Oded Maler. AMT: A Property-Based Monitoring Tool
for Analog Systems. Springer, 2007, pp. 304–19, doi:1567.'
short: D. Nickovic, O. Maler, in:, Springer, 2007, pp. 304–319.
conference:
name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
date_created: 2018-12-11T12:08:30Z
date_published: 2007-09-20T00:00:00Z
date_updated: 2021-01-12T07:56:27Z
day: '20'
doi: '1567'
extern: 1
month: '09'
page: 304 - 319
publication_status: published
publisher: Springer
publist_id: '1089'
quality_controlled: 0
status: public
title: 'AMT: a property-based monitoring tool for analog systems'
type: conference
year: '2007'
...
---
_id: '4370'
alternative_title:
- Lecture Notes in Computer Science
author:
- first_name: Oded
full_name: Maler, Oded
last_name: Maler
- first_name: Dejan
full_name: Dejan Nickovic
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: Springer; 2007:95-107. doi:1568'
apa: 'Maler, O., Nickovic, D., & Pnueli, A. (2007). On synthesizing controllers
from bounded-response properties (pp. 95–107). Presented at the CAV: Computer
Aided Verification, Springer. https://doi.org/1568'
chicago: Maler, Oded, Dejan Nickovic, and Amir Pnueli. “On Synthesizing Controllers
from Bounded-Response Properties,” 95–107. Springer, 2007. https://doi.org/1568.
ieee: 'O. Maler, D. Nickovic, and A. Pnueli, “On synthesizing controllers from bounded-response
properties,” presented at the CAV: Computer Aided Verification, 2007, pp. 95–107.'
ista: 'Maler O, Nickovic D, Pnueli A. 2007. On synthesizing controllers from bounded-response
properties. CAV: Computer Aided Verification, Lecture Notes in Computer Science,
, 95–107.'
mla: Maler, Oded, et al. On Synthesizing Controllers from Bounded-Response Properties.
Springer, 2007, pp. 95–107, doi:1568.
short: O. Maler, D. Nickovic, A. Pnueli, in:, Springer, 2007, pp. 95–107.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:30Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:28Z
day: '01'
doi: '1568'
extern: 1
month: '01'
page: 95 - 107
publication_status: published
publisher: Springer
publist_id: '1086'
quality_controlled: 0
status: public
title: On synthesizing controllers from bounded-response properties
type: conference
year: '2007'
...
---
_id: '4394'
alternative_title:
- LNCS 4349
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: Thomas Wies
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 C.
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: Springer; 2007:74-88.
doi:1552'
apa: 'Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., & Rinard, M. (2007). Using
First-Order Theorem Provers in the Jahob Data Structure Verification System (pp.
74–88). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation,
Springer. https://doi.org/1552'
chicago: Bouillaguet, Charles, Viktor Kuncak, Thomas Wies, Karen Zee, and Martin
Rinard. “Using First-Order Theorem Provers in the Jahob Data Structure Verification
System,” 74–88. Springer, 2007. https://doi.org/1552.
ieee: 'C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M. Rinard, “Using First-Order
Theorem Provers in the Jahob Data Structure Verification System,” presented at
the VMCAI: Verification, Model Checking and Abstract Interpretation, 2007, 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. VMCAI: Verification,
Model Checking and Abstract Interpretation, LNCS 4349, , 74–88.'
mla: Bouillaguet, Charles, et al. Using First-Order Theorem Provers in the Jahob
Data Structure Verification System. Springer, 2007, pp. 74–88, doi:1552.
short: C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, M. Rinard, in:, Springer, 2007,
pp. 74–88.
conference:
name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
date_created: 2018-12-11T12:08:37Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:39Z
day: '01'
doi: '1552'
extern: 1
month: '01'
page: 74 - 88
publication_status: published
publisher: Springer
publist_id: '1062'
quality_controlled: 0
status: public
title: Using First-Order Theorem Provers in the Jahob Data Structure Verification
System
type: conference
year: '2007'
...
---
_id: '4398'
alternative_title:
- LNCS 4590
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 W.
last_name: O'Hearn
- first_name: Thomas
full_name: Thomas Wies
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: Springer; 2007:178-192. doi:1553'
apa: 'Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P., Wies, T.,
& Yang, H. (2007). Shape Analysis for Composite Data Structures (pp. 178–192).
Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/1553'
chicago: Berdine, Josh, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O’Hearn,
Thomas Wies, and Hongseok Yang. “Shape Analysis for Composite Data Structures,”
178–92. Springer, 2007. https://doi.org/1553.
ieee: 'J. Berdine et al., “Shape Analysis for Composite Data Structures,”
presented at the CAV: Computer Aided Verification, 2007, 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. CAV: Computer Aided Verification,
LNCS 4590, , 178–192.'
mla: Berdine, Josh, et al. Shape Analysis for Composite Data Structures.
Springer, 2007, pp. 178–92, doi:1553.
short: J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O’Hearn, T. Wies, H. Yang,
in:, Springer, 2007, pp. 178–192.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:39Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:40Z
day: '01'
doi: '1553'
extern: 1
month: '01'
page: 178 - 192
publication_status: published
publisher: Springer
publist_id: '1058'
quality_controlled: 0
status: public
title: Shape Analysis for Composite Data Structures
type: conference
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'
alternative_title:
- LNCS
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Pavol
full_name: Pavol Cerny
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: Springer; 2007:664-678. doi:1544'
apa: 'Alur, R., Cerny, P., & Chaudhuri, S. (2007). Model Checking on Trees with
Path Equivalences (pp. 664–678). Presented at the TACAS: Tools and Algorithms
for the Construction and Analysis of Systems, Springer. https://doi.org/1544'
chicago: Alur, Rajeev, Pavol Cerny, and Swarat Chaudhuri. “Model Checking on Trees
with Path Equivalences,” 664–78. Springer, 2007. https://doi.org/1544.
ieee: 'R. Alur, P. Cerny, and S. Chaudhuri, “Model Checking on Trees with Path Equivalences,”
presented at the TACAS: Tools and Algorithms for the Construction and Analysis
of Systems, 2007, pp. 664–678.'
ista: 'Alur R, Cerny P, Chaudhuri S. 2007. Model Checking on Trees with Path Equivalences.
TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS,
, 664–678.'
mla: Alur, Rajeev, et al. Model Checking on Trees with Path Equivalences.
Springer, 2007, pp. 664–78, doi:1544.
short: R. Alur, P. Cerny, S. Chaudhuri, in:, Springer, 2007, pp. 664–678.
conference:
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
date_created: 2018-12-11T12:08:40Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:43Z
day: '01'
doi: '1544'
extern: 1
month: '01'
page: 664 - 678
publication_status: published
publisher: Springer
publist_id: '1055'
quality_controlled: 0
status: public
title: Model Checking on Trees with Path Equivalences
type: conference
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'
...
---
_id: '4446'
abstract:
- lang: eng
text: The Embedded Machine is a virtual machine that mediates in real time the interaction
between software processes and physical processes. It separates the compilation
of embedded programs into two phases. The first phase, the platform-independent
compiler phase, generates E code (code executed by the Embedded Machine), which
supervises the timing, not the scheduling of, application tasks relative to external
events such as clock ticks and sensor interrupts. E code is portable and, given
an input behavior, exhibits predictable (i.e., deterministic) timing and output
behavior. The second phase, the platform-dependent compiler phase, checks the
time safety of the E code, that is, whether platform performance (determined by
the hardware) and platform utilization (determined by the scheduler of the operating
system) enable its timely execution. We have used the Embedded Machine to compile
and execute high-performance control applications written in Giotto, such as the
flight control system of an autonomous model helicopter.
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Christoph
full_name: Kirsch, Christoph M
last_name: Kirsch
citation:
ama: 'Henzinger TA, Kirsch C. The embedded machine: Predictable, portable real-time
code. ACM Transactions on Programming Languages and Systems (TOPLAS). 2007;29(393).
doi:10.1145/1286821.1286824'
apa: 'Henzinger, T. A., & Kirsch, C. (2007). The embedded machine: Predictable,
portable real-time code. ACM Transactions on Programming Languages and Systems
(TOPLAS). ACM. https://doi.org/10.1145/1286821.1286824'
chicago: 'Henzinger, Thomas A, and Christoph Kirsch. “The Embedded Machine: Predictable,
Portable Real-Time Code.” ACM Transactions on Programming Languages and Systems
(TOPLAS). ACM, 2007. https://doi.org/10.1145/1286821.1286824.'
ieee: 'T. A. Henzinger and C. Kirsch, “The embedded machine: Predictable, portable
real-time code,” ACM Transactions on Programming Languages and Systems (TOPLAS),
vol. 29, no. 393. ACM, 2007.'
ista: 'Henzinger TA, Kirsch C. 2007. The embedded machine: Predictable, portable
real-time code. ACM Transactions on Programming Languages and Systems (TOPLAS).
29(393).'
mla: 'Henzinger, Thomas A., and Christoph Kirsch. “The Embedded Machine: Predictable,
Portable Real-Time Code.” ACM Transactions on Programming Languages and Systems
(TOPLAS), vol. 29, no. 393, ACM, 2007, doi:10.1145/1286821.1286824.'
short: T.A. Henzinger, C. Kirsch, ACM Transactions on Programming Languages and
Systems (TOPLAS) 29 (2007).
date_created: 2018-12-11T12:08:53Z
date_published: 2007-10-01T00:00:00Z
date_updated: 2021-01-12T07:57:01Z
day: '01'
doi: 10.1145/1286821.1286824
extern: 1
intvolume: ' 29'
issue: 393
month: '10'
publication: ACM Transactions on Programming Languages and Systems (TOPLAS)
publication_status: published
publisher: ACM
publist_id: '286'
quality_controlled: 0
status: public
title: 'The embedded machine: Predictable, portable real-time code'
type: journal_article
volume: 29
year: '2007'
...
---
_id: '4511'
abstract:
- lang: eng
text: 'In the traditional view, a language is a set of words, i.e., a function from
words to boolean values. We call this view “qualitative,” because each word either
belongs to or does not belong to a language. Let Σ be an alphabet, and let us
consider infinite words over Σ. Formally, a qualitative language over Σ is a function
A: B . There are many applications of qualitative languages. For example, qualitative
languages are used to specify the legal behaviors of systems, and zero-sum objectives
of games played on graphs. In the former case, each behavior of a system is either
legal or illegal; in the latter case, each outcome of a game is either winning
or losing. For defining languages, it is convenient to use finite acceptors (or
generators). In particular, qualitative languages are often defined using finite-state
machines (so-called ω-automata) whose transitions are labeled by letters from
Σ. For example, the states of an ω-automaton may represent states of a system,
and the transition labels may represent atomic observables of a behavior. There
is a rich and well-studied theory of finite-state acceptors of qualitative languages,
namely, the theory of theω-regular languages.'
acknowledgement: This research was supported in part by the Swiss National Science
Foundation and by the NSF grant CCR-0225610.
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Henzinger TA. Quantitative generalizations of languages. In: Vol 4588. Springer;
2007:20-22. doi:10.1007/978-3-540-73208-2_2'
apa: 'Henzinger, T. A. (2007). Quantitative generalizations of languages (Vol. 4588,
pp. 20–22). Presented at the DLT: Developments in Language Theory, Springer. https://doi.org/10.1007/978-3-540-73208-2_2'
chicago: Henzinger, Thomas A. “Quantitative Generalizations of Languages,” 4588:20–22.
Springer, 2007. https://doi.org/10.1007/978-3-540-73208-2_2.
ieee: 'T. A. Henzinger, “Quantitative generalizations of languages,” presented at
the DLT: Developments in Language Theory, 2007, vol. 4588, pp. 20–22.'
ista: 'Henzinger TA. 2007. Quantitative generalizations of languages. DLT: Developments
in Language Theory, LNCS, vol. 4588, 20–22.'
mla: Henzinger, Thomas A. Quantitative Generalizations of Languages. Vol.
4588, Springer, 2007, pp. 20–22, doi:10.1007/978-3-540-73208-2_2.
short: T.A. Henzinger, in:, Springer, 2007, pp. 20–22.
conference:
name: 'DLT: Developments in Language Theory'
date_created: 2018-12-11T12:09:14Z
date_published: 2007-06-21T00:00:00Z
date_updated: 2021-01-12T07:59:21Z
day: '21'
doi: 10.1007/978-3-540-73208-2_2
extern: 1
intvolume: ' 4588'
month: '06'
page: 20 - 22
publication_status: published
publisher: Springer
publist_id: '218'
quality_controlled: 0
status: public
title: Quantitative generalizations of languages
type: conference
volume: 4588
year: '2007'
...
---
_id: '4514'
abstract:
- lang: eng
text: 'Digital technology is increasingly deployed in safety-critical situations.
This calls for systematic design and verification methodologies that can cope
with three major sources of system complexity: concurrency, real time, and uncertainty.
We advocate a two-step process: formal modeling followed by algorithmic analysis
(or, “model building” followed by “model checking”). We model the concurrent components
of a reactive system as potential collaborators or adversaries in a multi-player
game with temporal objectives, such as system safety. The real-time aspect of
embedded systems requires models that combine discrete state transitions and continuous
state evolutions. Uncertainty in the environment is naturally modeled by probabilistic
state changes. As a result, we obtain three orthogonal extensions of the basic
state-transition graph model for reactive systems —game graphs, timed graphs,
and stochastic graphs— as well as combinations thereof. In this short text, we
provide a uniform exposition of the underlying definitions. For verification algorithms,
we refer the reader to the literature.'
acknowledgement: This research was supported in part by the Swiss National Science
Foundation, and by the NSF ITR grant CCR-0225610.
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Henzinger TA. Games, time, and probability: Graph models for system design
and analysis. In: Vol 4362. Springer; 2007:103-110. doi:10.1007/978-3-540-69507-3_7'
apa: 'Henzinger, T. A. (2007). Games, time, and probability: Graph models for system
design and analysis (Vol. 4362, pp. 103–110). Presented at the SOFSEM: Current
Trends in Theory and Practice of Computer Science, Springer. https://doi.org/10.1007/978-3-540-69507-3_7'
chicago: 'Henzinger, Thomas A. “Games, Time, and Probability: Graph Models for System
Design and Analysis,” 4362:103–10. Springer, 2007. https://doi.org/10.1007/978-3-540-69507-3_7.'
ieee: 'T. A. Henzinger, “Games, time, and probability: Graph models for system design
and analysis,” presented at the SOFSEM: Current Trends in Theory and Practice
of Computer Science, 2007, vol. 4362, pp. 103–110.'
ista: 'Henzinger TA. 2007. Games, time, and probability: Graph models for system
design and analysis. SOFSEM: Current Trends in Theory and Practice of Computer
Science, LNCS, vol. 4362, 103–110.'
mla: 'Henzinger, Thomas A. Games, Time, and Probability: Graph Models for System
Design and Analysis. Vol. 4362, Springer, 2007, pp. 103–10, doi:10.1007/978-3-540-69507-3_7.'
short: T.A. Henzinger, in:, Springer, 2007, pp. 103–110.
conference:
name: 'SOFSEM: Current Trends in Theory and Practice of Computer Science'
date_created: 2018-12-11T12:09:15Z
date_published: 2007-01-04T00:00:00Z
date_updated: 2021-01-12T07:59:22Z
day: '04'
doi: 10.1007/978-3-540-69507-3_7
extern: 1
intvolume: ' 4362'
month: '01'
page: 103 - 110
publication_status: published
publisher: Springer
publist_id: '217'
quality_controlled: 0
status: public
title: 'Games, time, and probability: Graph models for system design and analysis'
type: conference
volume: 4362
year: '2007'
...
---
_id: '4529'
abstract:
- lang: eng
text: Computational modeling of biological systems is becoming increasingly important
in efforts to better understand complex biological behaviors. In this review,
we distinguish between two types of biological models—mathematical and computational—which
differ in their representations of biological phenomena. We call the approach
of constructing computational models of biological systems 'executable biology',
as it focuses on the design of executable computer algorithms that mimic biological
phenomena. We survey the main modeling efforts in this direction, emphasize the
applicability and benefits of executable models in biological research and highlight
some of the challenges that executable biology poses for biology and computer
science. We claim that for executable biology to reach its full potential as a
mainstream biological technique, formal and algorithmic approaches must be integrated
into biological research. This will drive biology toward a more precise engineering
discipline.
author:
- first_name: Jasmin
full_name: Fisher, Jasmin
last_name: Fisher
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: Fisher J, Henzinger TA. Executable cell biology. Nature Biotechnology.
2007;25:1239-1249. doi:10.1038/nbt1356
apa: Fisher, J., & Henzinger, T. A. (2007). Executable cell biology. Nature
Biotechnology. Nature Publishing Group. https://doi.org/10.1038/nbt1356
chicago: Fisher, Jasmin, and Thomas A Henzinger. “Executable Cell Biology.” Nature
Biotechnology. Nature Publishing Group, 2007. https://doi.org/10.1038/nbt1356.
ieee: J. Fisher and T. A. Henzinger, “Executable cell biology,” Nature Biotechnology,
vol. 25. Nature Publishing Group, pp. 1239–1249, 2007.
ista: Fisher J, Henzinger TA. 2007. Executable cell biology. Nature Biotechnology.
25, 1239–1249.
mla: Fisher, Jasmin, and Thomas A. Henzinger. “Executable Cell Biology.” Nature
Biotechnology, vol. 25, Nature Publishing Group, 2007, pp. 1239–49, doi:10.1038/nbt1356.
short: J. Fisher, T.A. Henzinger, Nature Biotechnology 25 (2007) 1239–1249.
date_created: 2018-12-11T12:09:19Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:28Z
day: '01'
doi: 10.1038/nbt1356
extern: 1
intvolume: ' 25'
month: '01'
page: 1239 - 1249
publication: Nature Biotechnology
publication_status: published
publisher: Nature Publishing Group
publist_id: '198'
quality_controlled: 0
status: public
title: Executable cell biology
type: journal_article
volume: 25
year: '2007'
...
---
_id: '4530'
abstract:
- lang: eng
text: This book constitutes the refereed proceedings of the 21st International Workshop
on Computer Science Logic, CSL 2007, held as the 16th Annual Conference of the
EACSL in Lausanne, Switzerland. The 36 revised full papers presented together
with the abstracts of six invited lectures are organized in topical sections on
logic and games, expressiveness, games and trees, logic and deduction, lambda
calculus, finite model theory, linear logic, proof theory, and game semantics.
alternative_title:
- LNCS
author:
- first_name: Jacques
full_name: Duparc, Jacques
last_name: Duparc
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Duparc J, Henzinger TA. CSL: Computer Science Logic . Vol 4646. Springer;
2007. doi:10.1007/978-3-540-74915-8'
apa: 'Duparc, J., & Henzinger, T. A. (2007). CSL: Computer Science Logic
. CSL: Computer Science Logic (Vol. 4646). Springer. https://doi.org/10.1007/978-3-540-74915-8'
chicago: 'Duparc, Jacques, and Thomas A Henzinger. CSL: Computer Science Logic
. CSL: Computer Science Logic. Vol. 4646. Springer, 2007. https://doi.org/10.1007/978-3-540-74915-8.'
ieee: 'J. Duparc and T. A. Henzinger, CSL: Computer Science Logic , vol.
4646. Springer, 2007.'
ista: 'Duparc J, Henzinger TA. 2007. CSL: Computer Science Logic , Springer,p.'
mla: 'Duparc, Jacques, and Thomas A. Henzinger. “CSL: Computer Science Logic .”
CSL: Computer Science Logic, vol. 4646, Springer, 2007, doi:10.1007/978-3-540-74915-8.'
short: 'J. Duparc, T.A. Henzinger, CSL: Computer Science Logic , Springer, 2007.'
date_created: 2018-12-11T12:09:20Z
date_published: 2007-09-01T00:00:00Z
date_updated: 2019-08-02T12:38:32Z
day: '01'
doi: 10.1007/978-3-540-74915-8
extern: 1
intvolume: ' 4646'
month: '09'
publication: 'CSL: Computer Science Logic'
publication_status: published
publisher: Springer
publist_id: '194'
quality_controlled: 0
status: public
title: 'CSL: Computer Science Logic '
type: conference_editor
volume: 4646
year: '2007'
...
---
_id: '4531'
abstract:
- lang: eng
text: Caenorhabditis elegans vulval development provides an important paradigm for
studying the process of cell fate determination and pattern formation during animal
development. Although many genes controlling vulval cell fate specification have
been identified, how they orchestrate themselves to generate a robust and invariant
pattern of cell fates is not yet completely understood. Here, we have developed
a dynamic computational model incorporating the current mechanistic understanding
of gene interactions during this patterning process. A key feature of our model
is the inclusion of multiple modes of crosstalk between the epidermal growth factor
receptor (EGFR) and LIN-12/Notch signaling pathways, which together determine
the fates of the six vulval precursor cells (VPCs). Computational analysis, using
the model-checking technique, provides new biological insights into the regulatory
network governing VPC fate specification and predicts novel negative feedback
loops. In addition, our analysis shows that most mutations affecting vulval development
lead to stable fate patterns in spite of variations in synchronicity between VPCs.
Computational searches for the basis of this robustness show that a sequential
activation of the EGFR-mediated inductive signaling and LIN-12 / Notch-mediated
lateral signaling pathways is key to achieve a stable cell fate pattern. We demonstrate
experimentally a time-delay between the activation of the inductive and lateral
signaling pathways in wild-type animals and the loss of sequential signaling in
mutants showing unstable fate patterns; thus, validating two key predictions provided
by our modeling work. The insights gained by our modeling study further substantiate
the usefulness of executing and analyzing mechanistic models to investigate complex
biological behaviors.
acknowledgement: This work was supported in part by the Swiss National Science Foundation
(grant 205321–111840).
author:
- first_name: Jasmin
full_name: Fisher, Jasmin
last_name: Fisher
- first_name: Nir
full_name: Piterman, Nir
last_name: Piterman
- first_name: Alex
full_name: Hajnal, Alex
last_name: Hajnal
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: Fisher J, Piterman N, Hajnal A, Henzinger TA. Predictive modeling of signaling
crosstalk during C. elegans vulval development. PLoS Computational Biology.
2007;3(5):e92. doi:10.1371/journal.pcbi.0030092
apa: Fisher, J., Piterman, N., Hajnal, A., & Henzinger, T. A. (2007). Predictive
modeling of signaling crosstalk during C. elegans vulval development. PLoS
Computational Biology. Public Library of Science. https://doi.org/10.1371/journal.pcbi.0030092
chicago: Fisher, Jasmin, Nir Piterman, Alex Hajnal, and Thomas A Henzinger. “Predictive
Modeling of Signaling Crosstalk during C. Elegans Vulval Development.” PLoS
Computational Biology. Public Library of Science, 2007. https://doi.org/10.1371/journal.pcbi.0030092.
ieee: J. Fisher, N. Piterman, A. Hajnal, and T. A. Henzinger, “Predictive modeling
of signaling crosstalk during C. elegans vulval development,” PLoS Computational
Biology, vol. 3(5):e92. Public Library of Science, 2007.
ista: Fisher J, Piterman N, Hajnal A, Henzinger TA. 2007. Predictive modeling of
signaling crosstalk during C. elegans vulval development. PLoS Computational Biology.
3(5):e92.
mla: Fisher, Jasmin, et al. “Predictive Modeling of Signaling Crosstalk during C.
Elegans Vulval Development.” PLoS Computational Biology, vol. 3(5):e92,
Public Library of Science, 2007, doi:10.1371/journal.pcbi.0030092.
short: J. Fisher, N. Piterman, A. Hajnal, T.A. Henzinger, PLoS Computational Biology
3(5):e92 (2007).
date_created: 2018-12-11T12:09:20Z
date_published: 2007-05-18T00:00:00Z
date_updated: 2021-01-12T07:59:29Z
day: '18'
doi: 10.1371/journal.pcbi.0030092
extern: 1
month: '05'
publication: PLoS Computational Biology
publication_status: published
publisher: Public Library of Science
publist_id: '195'
quality_controlled: 0
status: public
title: Predictive modeling of signaling crosstalk during C. elegans vulval development
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
volume: 3(5):e92
year: '2007'
...
---
_id: '4537'
abstract:
- lang: eng
text: The classical synthesis problem for reactive systems asks, given a proponent
process A and an opponent process B, to refine A so that the closed-loop system
A parallel to B satisfies a given specification Phi. The solution of this problem
requires the computation of a winning strategy for proponent A in a game against
opponent B. We define and study the co-synthesis problem, where the proponent
A consists itself of two independent processes, A = A(1)parallel to A(2), with
specifications Phi(1) and Phi(2), and the goal is to refine both A(1) and A(2)
so that A(1)parallel to A(2)parallel to B satisfies Phi(1) boolean AND Phi(2).
For example, if the opponent B is a fair scheduler for the two processes A(1)
and A(2), and Phi(i) specifies the requirements of mutual exclusion for A(i) (e.g.,
starvation freedom), then the co-synthesis problem asks for the automatic synthesis
of a mutual-exclusion protocol. We show that co-synthesis defined classically,
with the processes A(1) and A(2) either collaborating or competing, does not capture
desirable solutions. Instead, the proper formulation of co-synthesis is the one
where process A, competes with A(2) but not at the price of violating Phi(1),
and vice versa. We call this assume-guarantee synthesis and show that it can be
solved by computing secure-equilibrium strategies. In particular, from mutual-exclusion
requirements the assume-guarantee synthesis algorithm automatically computes Peterson's
protocol.
acknowledgement: This research was supported in part by the Swiss National Science
Foundation and by the NSF grants CCR-0225610 and CCR-0234690.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: 'Chatterjee K, Henzinger TA. Assume-guarantee synthesis. In: Vol 4424. Springer;
2007:261-275. doi:10.1007/978-3-540-71209-1_21'
apa: 'Chatterjee, K., & Henzinger, T. A. (2007). Assume-guarantee synthesis
(Vol. 4424, pp. 261–275). Presented at the TACAS: Tools and Algorithms for the
Construction and Analysis of Systems, Springer. https://doi.org/10.1007/978-3-540-71209-1_21'
chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Assume-Guarantee Synthesis,”
4424:261–75. Springer, 2007. https://doi.org/10.1007/978-3-540-71209-1_21.
ieee: 'K. Chatterjee and T. A. Henzinger, “Assume-guarantee synthesis,” presented
at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
2007, vol. 4424, pp. 261–275.'
ista: 'Chatterjee K, Henzinger TA. 2007. Assume-guarantee synthesis. TACAS: Tools
and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 4424,
261–275.'
mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. Assume-Guarantee Synthesis.
Vol. 4424, Springer, 2007, pp. 261–75, doi:10.1007/978-3-540-71209-1_21.
short: K. Chatterjee, T.A. Henzinger, in:, Springer, 2007, pp. 261–275.
conference:
name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
date_created: 2018-12-11T12:09:22Z
date_published: 2007-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:32Z
day: '01'
doi: 10.1007/978-3-540-71209-1_21
extern: 1
intvolume: ' 4424'
month: '01'
page: 261 - 275
publication_status: published
publisher: Springer
publist_id: '186'
quality_controlled: 0
status: public
title: Assume-guarantee synthesis
type: conference
volume: 4424
year: '2007'
...