[{"publist_id":"1230","publication":"Bibliothek - Forschung Und Praxis","date_published":"2007-01-01T00:00:00Z","publisher":"De Gruyter","day":"01","extern":1,"citation":{"mla":"Danowski, Patrick, and Lambert Heller. “Bibliothek 2.0 ? Wird Alles Anders?” <i>Bibliothek - Forschung Und Praxis</i>, vol. 31, no. 2007, De Gruyter, 2007, pp. 130–36, doi:<a href=\"https://doi.org/45\">45</a>.","short":"P. Danowski, L. Heller, Bibliothek - Forschung Und Praxis 31 (2007) 130–136.","ista":"Danowski P, Heller L. 2007. Bibliothek 2.0 ? Wird alles anders? Bibliothek - Forschung Und Praxis. 31(2007), 130–136.","ieee":"P. Danowski and L. Heller, “Bibliothek 2.0 ? Wird alles anders?,” <i>Bibliothek - Forschung Und Praxis</i>, vol. 31, no. 2007. De Gruyter, pp. 130–136, 2007.","chicago":"Danowski, Patrick, and Lambert Heller. “Bibliothek 2.0 ? Wird Alles Anders?” <i>Bibliothek - Forschung Und Praxis</i>. De Gruyter, 2007. <a href=\"https://doi.org/45\">https://doi.org/45</a>.","apa":"Danowski, P., &#38; Heller, L. (2007). Bibliothek 2.0 ? Wird alles anders? <i>Bibliothek - Forschung Und Praxis</i>. De Gruyter. <a href=\"https://doi.org/45\">https://doi.org/45</a>","ama":"Danowski P, Heller L. Bibliothek 2.0 ? Wird alles anders? <i>Bibliothek - Forschung Und Praxis</i>. 2007;31(2007):130-136. doi:<a href=\"https://doi.org/45\">45</a>"},"quality_controlled":0,"author":[{"orcid":"0000-0002-6026-4409","full_name":"Patrick Danowski","first_name":"Patrick","last_name":"Danowski","id":"2EBD1598-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Heller,Lambert","first_name":"Lambert","last_name":"Heller"}],"status":"public","volume":31,"date_created":"2018-12-11T12:08:22Z","publication_status":"published","doi":"45","month":"01","year":"2007","intvolume":"        31","issue":"2007","page":"130 - 136","title":"Bibliothek 2.0 ? Wird alles anders?","main_file_link":[{"open_access":"0","url":"http://www.bibliothek-saur.de/2007_2/130-136.pdf"}],"type":"journal_article","_id":"4344","date_updated":"2021-01-12T07:56:17Z"},{"volume":2,"publication_status":"published","date_created":"2018-12-11T12:08:25Z","doi":"10.1371/journal.pone.0000197","license":"https://creativecommons.org/licenses/by/4.0/","citation":{"mla":"Binladen, Jonas, et al. “The Use of Coded PCR Primers Enables High-Throughput Sequencing of Multiple Homolog Amplification Products by 454 Parallel Sequencing.” <i>PLoS One</i>, vol. 2, no. 2, Public Library of Science, 2007, doi:<a href=\"https://doi.org/10.1371/journal.pone.0000197\">10.1371/journal.pone.0000197</a>.","short":"J. Binladen, M.T. Gilbert, J.P. Bollback, F. Panitz, C. Bendixen, R. Nielsen, E. Willerslev, PLoS One 2 (2007).","ieee":"J. Binladen <i>et al.</i>, “The use of coded PCR primers enables high-throughput sequencing of multiple homolog amplification products by 454 parallel sequencing,” <i>PLoS One</i>, 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).","apa":"Binladen, J., Gilbert, M. T., Bollback, J. P., Panitz, F., Bendixen, C., Nielsen, R., &#38; Willerslev, E. (2007). The use of coded PCR primers enables high-throughput sequencing of multiple homolog amplification products by 454 parallel sequencing. <i>PLoS One</i>. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pone.0000197\">https://doi.org/10.1371/journal.pone.0000197</a>","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.” <i>PLoS One</i>. Public Library of Science, 2007. <a href=\"https://doi.org/10.1371/journal.pone.0000197\">https://doi.org/10.1371/journal.pone.0000197</a>.","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. <i>PLoS One</i>. 2007;2(2). doi:<a href=\"https://doi.org/10.1371/journal.pone.0000197\">10.1371/journal.pone.0000197</a>"},"extern":1,"status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"author":[{"full_name":"Binladen, Jonas","first_name":"Jonas","last_name":"Binladen"},{"last_name":"Gilbert","full_name":"Gilbert, M Thomas","first_name":"M Thomas"},{"id":"2C6FA9CC-F248-11E8-B48F-1D18A9856A87","last_name":"Bollback","first_name":"Jonathan P","full_name":"Jonathan Bollback","orcid":"0000-0002-4624-4612"},{"first_name":"Frank","full_name":"Panitz, Frank","last_name":"Panitz"},{"last_name":"Bendixen","full_name":"Bendixen, Christian","first_name":"Christian"},{"full_name":"Nielsen, Rasmus","first_name":"Rasmus","last_name":"Nielsen"},{"last_name":"Willerslev","first_name":"Eske","full_name":"Willerslev, Eske"}],"quality_controlled":0,"publication":"PLoS One","date_published":"2007-02-14T00:00:00Z","publisher":"Public Library of Science","day":"14","publist_id":"1105","abstract":[{"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&amp;lt;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.","lang":"eng"}],"_id":"4353","type":"journal_article","date_updated":"2021-01-12T07:56:21Z","title":"The use of coded PCR primers enables high-throughput sequencing of multiple homolog amplification products by 454 parallel sequencing","issue":"2","month":"02","year":"2007","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.","intvolume":"         2"},{"volume":17,"date_created":"2018-12-11T12:08:25Z","publication_status":"published","doi":"10.1101/gr.5890907","extern":1,"citation":{"short":"E. Freyhult, J.P. Bollback, P. Gardner, Genome Research 17 (2007) 117–25.","mla":"Freyhult, Eva, et al. “Exploring Genomic Dark Matter: A Critical Assessment of the Performance of Homology Search Methods on Noncoding RNA.” <i>Genome Research</i>, vol. 17, no. 1, Cold Spring Harbor Laboratory Press, 2007, pp. 117–25, doi:<a href=\"https://doi.org/10.1101/gr.5890907\">10.1101/gr.5890907</a>.","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,” <i>Genome Research</i>, 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.","apa":"Freyhult, E., Bollback, J. P., &#38; Gardner, P. (2007). Exploring genomic dark matter: a critical assessment of the performance of homology search methods on noncoding RNA. <i>Genome Research</i>. Cold Spring Harbor Laboratory Press. <a href=\"https://doi.org/10.1101/gr.5890907\">https://doi.org/10.1101/gr.5890907</a>","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.” <i>Genome Research</i>. Cold Spring Harbor Laboratory Press, 2007. <a href=\"https://doi.org/10.1101/gr.5890907\">https://doi.org/10.1101/gr.5890907</a>.","ama":"Freyhult E, Bollback JP, Gardner P. Exploring genomic dark matter: a critical assessment of the performance of homology search methods on noncoding RNA. <i>Genome Research</i>. 2007;17(1):117-125. doi:<a href=\"https://doi.org/10.1101/gr.5890907\">10.1101/gr.5890907</a>"},"status":"public","author":[{"full_name":"Freyhult, Eva K","first_name":"Eva","last_name":"Freyhult"},{"first_name":"Jonathan P","full_name":"Jonathan Bollback","orcid":"0000-0002-4624-4612","id":"2C6FA9CC-F248-11E8-B48F-1D18A9856A87","last_name":"Bollback"},{"first_name":"Paul","full_name":"Gardner, Paul P","last_name":"Gardner"}],"quality_controlled":0,"publication":"Genome Research","date_published":"2007-01-01T00:00:00Z","publisher":"Cold Spring Harbor Laboratory Press","day":"01","publist_id":"1106","abstract":[{"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.","lang":"eng"}],"_id":"4354","type":"journal_article","date_updated":"2021-01-12T07:56:21Z","title":"Exploring genomic dark matter: a critical assessment of the performance of homology search methods on noncoding RNA","main_file_link":[{"url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC1716261","open_access":"0"}],"issue":"1","page":"117 - 25","month":"01","year":"2007","intvolume":"        17"},{"month":"03","year":"2007","intvolume":"        24","acknowledgement":"R01 GM069801-08/GM/NIGMS NIH HHS/United States","issue":"6","page":"1397 - 1406","title":"Clonal interference is alleviated by high mutation rates in large populations","_id":"4355","type":"journal_article","date_updated":"2021-01-12T07:56:22Z","publist_id":"1104","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 &quot;clonal interference,&quot; 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."}],"publication":"Molecular Biology and Evolution","date_published":"2007-03-22T00:00:00Z","publisher":"Oxford University Press","day":"22","extern":1,"citation":{"short":"J.P. Bollback, J. Huelsenbeck, Molecular Biology and Evolution 24 (2007) 1397–1406.","mla":"Bollback, Jonathan P., and John Huelsenbeck. “Clonal Interference Is Alleviated by High Mutation Rates in Large Populations.” <i>Molecular Biology and Evolution</i>, vol. 24, no. 6, Oxford University Press, 2007, pp. 1397–406, doi:<a href=\"https://doi.org/10.1093/molbev/msm056\">10.1093/molbev/msm056</a>.","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.","ieee":"J. P. Bollback and J. Huelsenbeck, “Clonal interference is alleviated by high mutation rates in large populations,” <i>Molecular Biology and Evolution</i>, vol. 24, no. 6. Oxford University Press, pp. 1397–1406, 2007.","chicago":"Bollback, Jonathan P, and John Huelsenbeck. “Clonal Interference Is Alleviated by High Mutation Rates in Large Populations.” <i>Molecular Biology and Evolution</i>. Oxford University Press, 2007. <a href=\"https://doi.org/10.1093/molbev/msm056\">https://doi.org/10.1093/molbev/msm056</a>.","apa":"Bollback, J. P., &#38; Huelsenbeck, J. (2007). Clonal interference is alleviated by high mutation rates in large populations. <i>Molecular Biology and Evolution</i>. Oxford University Press. <a href=\"https://doi.org/10.1093/molbev/msm056\">https://doi.org/10.1093/molbev/msm056</a>","ama":"Bollback JP, Huelsenbeck J. Clonal interference is alleviated by high mutation rates in large populations. <i>Molecular Biology and Evolution</i>. 2007;24(6):1397-1406. doi:<a href=\"https://doi.org/10.1093/molbev/msm056\">10.1093/molbev/msm056</a>"},"status":"public","author":[{"full_name":"Jonathan Bollback","first_name":"Jonathan P","orcid":"0000-0002-4624-4612","id":"2C6FA9CC-F248-11E8-B48F-1D18A9856A87","last_name":"Bollback"},{"last_name":"Huelsenbeck","first_name":"John","full_name":"Huelsenbeck, John P"}],"quality_controlled":0,"volume":24,"date_created":"2018-12-11T12:08:26Z","publication_status":"published","doi":"10.1093/molbev/msm056"},{"publist_id":"1103","abstract":[{"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.","lang":"eng"}],"publication":"Genome Research","date_published":"2007-08-03T00:00:00Z","publisher":"Cold Spring Harbor Laboratory Press","day":"03","citation":{"ama":"Petersen L, Bollback JP, Dimmic M, Hubisz M, Nielsen R. Genes under positive selection in Escherichia coli. <i>Genome Research</i>. 2007;17(9):1336-1343. doi:<a href=\"https://doi.org/10.1101/gr.6254707\">10.1101/gr.6254707</a>","chicago":"Petersen, Lise, Jonathan P Bollback, Matt Dimmic, Melissa Hubisz, and Rasmus Nielsen. “Genes under Positive Selection in Escherichia Coli.” <i>Genome Research</i>. Cold Spring Harbor Laboratory Press, 2007. <a href=\"https://doi.org/10.1101/gr.6254707\">https://doi.org/10.1101/gr.6254707</a>.","apa":"Petersen, L., Bollback, J. P., Dimmic, M., Hubisz, M., &#38; Nielsen, R. (2007). Genes under positive selection in Escherichia coli. <i>Genome Research</i>. Cold Spring Harbor Laboratory Press. <a href=\"https://doi.org/10.1101/gr.6254707\">https://doi.org/10.1101/gr.6254707</a>","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.","ieee":"L. Petersen, J. P. Bollback, M. Dimmic, M. Hubisz, and R. Nielsen, “Genes under positive selection in Escherichia coli,” <i>Genome Research</i>, vol. 17, no. 9. Cold Spring Harbor Laboratory Press, pp. 1336–1343, 2007.","short":"L. Petersen, J.P. Bollback, M. Dimmic, M. Hubisz, R. Nielsen, Genome Research 17 (2007) 1336–1343.","mla":"Petersen, Lise, et al. “Genes under Positive Selection in Escherichia Coli.” <i>Genome Research</i>, vol. 17, no. 9, Cold Spring Harbor Laboratory Press, 2007, pp. 1336–43, doi:<a href=\"https://doi.org/10.1101/gr.6254707\">10.1101/gr.6254707</a>."},"extern":1,"quality_controlled":0,"author":[{"last_name":"Petersen","full_name":"Petersen, Lise","first_name":"Lise"},{"orcid":"0000-0002-4624-4612","full_name":"Jonathan Bollback","first_name":"Jonathan P","last_name":"Bollback","id":"2C6FA9CC-F248-11E8-B48F-1D18A9856A87"},{"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"}],"status":"public","volume":17,"publication_status":"published","date_created":"2018-12-11T12:08:26Z","doi":"10.1101/gr.6254707","month":"08","intvolume":"        17","year":"2007","issue":"9","page":"1336 - 1343","title":"Genes under positive selection in Escherichia coli","type":"journal_article","_id":"4356","date_updated":"2021-01-12T07:56:22Z"},{"doi":"1567","date_created":"2018-12-11T12:08:30Z","publication_status":"published","alternative_title":["LNCS"],"author":[{"last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Dejan Nickovic","first_name":"Dejan"},{"first_name":"Oded","full_name":"Maler, Oded","last_name":"Maler"}],"status":"public","quality_controlled":0,"extern":1,"citation":{"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. <i>AMT: A Property-Based Monitoring Tool for Analog Systems</i>. Springer, 2007, pp. 304–19, doi:<a href=\"https://doi.org/1567\">1567</a>.","short":"D. Nickovic, O. Maler, in:, Springer, 2007, pp. 304–319.","ama":"Nickovic D, Maler O. AMT: a property-based monitoring tool for analog systems. In: Springer; 2007:304-319. doi:<a href=\"https://doi.org/1567\">1567</a>","apa":"Nickovic, D., &#38; 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. <a href=\"https://doi.org/1567\">https://doi.org/1567</a>","chicago":"Nickovic, Dejan, and Oded Maler. “AMT: A Property-Based Monitoring Tool for Analog Systems,” 304–19. Springer, 2007. <a href=\"https://doi.org/1567\">https://doi.org/1567</a>."},"publisher":"Springer","day":"20","date_published":"2007-09-20T00:00:00Z","publist_id":"1089","date_updated":"2021-01-12T07:56:27Z","_id":"4368","type":"conference","conference":{"name":"FORMATS: Formal Modeling and Analysis of Timed Systems"},"title":"AMT: a property-based monitoring tool for analog systems","page":"304 - 319","year":"2007","month":"09"},{"year":"2007","month":"01","page":"95 - 107","title":"On synthesizing controllers from bounded-response properties","date_updated":"2021-01-12T07:56:28Z","_id":"4370","type":"conference","conference":{"name":"CAV: Computer Aided Verification"},"publist_id":"1086","day":"01","publisher":"Springer","date_published":"2007-01-01T00:00:00Z","quality_controlled":0,"alternative_title":["Lecture Notes in Computer Science"],"author":[{"last_name":"Maler","first_name":"Oded","full_name":"Maler, Oded"},{"first_name":"Dejan","full_name":"Dejan Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic"},{"full_name":"Pnueli,Amir","first_name":"Amir","last_name":"Pnueli"}],"status":"public","citation":{"short":"O. Maler, D. Nickovic, A. Pnueli, in:, Springer, 2007, pp. 95–107.","mla":"Maler, Oded, et al. <i>On Synthesizing Controllers from Bounded-Response Properties</i>. Springer, 2007, pp. 95–107, doi:<a href=\"https://doi.org/1568\">1568</a>.","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.","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.","apa":"Maler, O., Nickovic, D., &#38; Pnueli, A. (2007). On synthesizing controllers from bounded-response properties (pp. 95–107). Presented at the CAV: Computer Aided Verification, Springer. <a href=\"https://doi.org/1568\">https://doi.org/1568</a>","chicago":"Maler, Oded, Dejan Nickovic, and Amir Pnueli. “On Synthesizing Controllers from Bounded-Response Properties,” 95–107. Springer, 2007. <a href=\"https://doi.org/1568\">https://doi.org/1568</a>.","ama":"Maler O, Nickovic D, Pnueli A. On synthesizing controllers from bounded-response properties. In: Springer; 2007:95-107. doi:<a href=\"https://doi.org/1568\">1568</a>"},"extern":1,"doi":"1568","publication_status":"published","date_created":"2018-12-11T12:08:30Z"},{"page":"74 - 88","year":"2007","month":"01","date_updated":"2021-01-12T07:56:39Z","_id":"4394","type":"conference","conference":{"name":"VMCAI: Verification, Model Checking and Abstract Interpretation"},"title":"Using First-Order Theorem Provers in the Jahob Data Structure Verification System","publisher":"Springer","day":"01","date_published":"2007-01-01T00:00:00Z","publist_id":"1062","doi":"1552","date_created":"2018-12-11T12:08:37Z","publication_status":"published","alternative_title":["LNCS 4349"],"quality_controlled":0,"status":"public","author":[{"first_name":"Charles","full_name":"Bouillaguet,Charles","last_name":"Bouillaguet"},{"first_name":"Viktor","full_name":"Kuncak, Viktor","last_name":"Kuncak"},{"last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","full_name":"Thomas Wies"},{"last_name":"Zee","first_name":"Karen","full_name":"Zee,Karen"},{"last_name":"Rinard","first_name":"Martin","full_name":"Rinard,Martin C."}],"extern":1,"citation":{"mla":"Bouillaguet, Charles, et al. <i>Using First-Order Theorem Provers in the Jahob Data Structure Verification System</i>. Springer, 2007, pp. 74–88, doi:<a href=\"https://doi.org/1552\">1552</a>.","short":"C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, M. Rinard, in:, Springer, 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.","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.","apa":"Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., &#38; 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. <a href=\"https://doi.org/1552\">https://doi.org/1552</a>","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. <a href=\"https://doi.org/1552\">https://doi.org/1552</a>.","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:<a href=\"https://doi.org/1552\">1552</a>"}},{"type":"conference","_id":"4398","date_updated":"2021-01-12T07:56:40Z","conference":{"name":"CAV: Computer Aided Verification"},"title":"Shape Analysis for Composite Data Structures","page":"178 - 192","year":"2007","month":"01","doi":"1553","date_created":"2018-12-11T12:08:39Z","publication_status":"published","extern":1,"citation":{"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. <a href=\"https://doi.org/1553\">https://doi.org/1553</a>.","apa":"Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P., Wies, T., &#38; Yang, H. (2007). Shape Analysis for Composite Data Structures (pp. 178–192). Presented at the CAV: Computer Aided Verification, Springer. <a href=\"https://doi.org/1553\">https://doi.org/1553</a>","ama":"Berdine J, Calcagno C, Cook B, et al. Shape Analysis for Composite Data Structures. In: Springer; 2007:178-192. doi:<a href=\"https://doi.org/1553\">1553</a>","mla":"Berdine, Josh, et al. <i>Shape Analysis for Composite Data Structures</i>. Springer, 2007, pp. 178–92, doi:<a href=\"https://doi.org/1553\">1553</a>.","short":"J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O’Hearn, T. Wies, H. Yang, in:, Springer, 2007, pp. 178–192.","ieee":"J. Berdine <i>et al.</i>, “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."},"status":"public","quality_controlled":0,"author":[{"last_name":"Berdine","full_name":"Berdine,Josh","first_name":"Josh"},{"last_name":"Calcagno","full_name":"Calcagno,Cristiano","first_name":"Cristiano"},{"full_name":"Cook,Byron","first_name":"Byron","last_name":"Cook"},{"last_name":"Distefano","full_name":"Distefano,Dino","first_name":"Dino"},{"first_name":"Peter","full_name":"O'Hearn,Peter W.","last_name":"O'Hearn"},{"full_name":"Thomas Wies","first_name":"Thomas","last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Yang,Hongseok","first_name":"Hongseok","last_name":"Yang"}],"alternative_title":["LNCS 4590"],"day":"01","publisher":"Springer","date_published":"2007-01-01T00:00:00Z","publist_id":"1058"},{"conference":{"name":"CAV: Computer Aided Verification"},"_id":"4399","type":"conference","date_updated":"2021-01-12T07:56:41Z","title":"Algorithms for interface synthesis","page":"4 - 19","month":"07","year":"2007","intvolume":"      4590","acknowledgement":"This research was supported in part by the grant SFU/PRG 06-3, and by the Swiss National Science Foundation.","volume":4590,"publication_status":"published","date_created":"2018-12-11T12:08:39Z","doi":"10.1007/978-3-540-73368-3_4","citation":{"mla":"Beyer, Dirk, et al. <i>Algorithms for Interface Synthesis</i>. Vol. 4590, Springer, 2007, pp. 4–19, doi:<a href=\"https://doi.org/10.1007/978-3-540-73368-3_4\">10.1007/978-3-540-73368-3_4</a>.","short":"D. Beyer, T.A. Henzinger, V. Singh, in:, Springer, 2007, pp. 4–19.","ista":"Beyer D, Henzinger TA, Singh V. 2007. Algorithms for interface synthesis. CAV: Computer Aided Verification, LNCS, vol. 4590, 4–19.","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.","chicago":"Beyer, Dirk, Thomas A Henzinger, and Vasu Singh. “Algorithms for Interface Synthesis,” 4590:4–19. Springer, 2007. <a href=\"https://doi.org/10.1007/978-3-540-73368-3_4\">https://doi.org/10.1007/978-3-540-73368-3_4</a>.","apa":"Beyer, D., Henzinger, T. A., &#38; Singh, V. (2007). Algorithms for interface synthesis (Vol. 4590, pp. 4–19). Presented at the CAV: Computer Aided Verification, Springer. <a href=\"https://doi.org/10.1007/978-3-540-73368-3_4\">https://doi.org/10.1007/978-3-540-73368-3_4</a>","ama":"Beyer D, Henzinger TA, Singh V. Algorithms for interface synthesis. In: Vol 4590. Springer; 2007:4-19. doi:<a href=\"https://doi.org/10.1007/978-3-540-73368-3_4\">10.1007/978-3-540-73368-3_4</a>"},"extern":1,"status":"public","alternative_title":["LNCS"],"author":[{"first_name":"Dirk","full_name":"Beyer, Dirk","last_name":"Beyer"},{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Singh","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","first_name":"Vasu","full_name":"Vasu Singh"}],"quality_controlled":0,"date_published":"2007-07-02T00:00:00Z","publisher":"Springer","day":"02","publist_id":"1059","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. "}]},{"publist_id":"1055","date_published":"2007-01-01T00:00:00Z","day":"01","publisher":"Springer","author":[{"first_name":"Rajeev","full_name":"Alur, Rajeev","last_name":"Alur"},{"last_name":"Cerny","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","full_name":"Pavol Cerny","first_name":"Pavol"},{"first_name":"Swarat","full_name":"Chaudhuri,Swarat","last_name":"Chaudhuri"}],"status":"public","alternative_title":["LNCS"],"quality_controlled":0,"extern":1,"citation":{"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.","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.","short":"R. Alur, P. Cerny, S. Chaudhuri, in:, Springer, 2007, pp. 664–678.","mla":"Alur, Rajeev, et al. <i>Model Checking on Trees with Path Equivalences</i>. Springer, 2007, pp. 664–78, doi:<a href=\"https://doi.org/1544\">1544</a>.","ama":"Alur R, Cerny P, Chaudhuri S. Model Checking on Trees with Path Equivalences. In: Springer; 2007:664-678. doi:<a href=\"https://doi.org/1544\">1544</a>","apa":"Alur, R., Cerny, P., &#38; 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. <a href=\"https://doi.org/1544\">https://doi.org/1544</a>","chicago":"Alur, Rajeev, Pavol Cerny, and Swarat Chaudhuri. “Model Checking on Trees with Path Equivalences,” 664–78. Springer, 2007. <a href=\"https://doi.org/1544\">https://doi.org/1544</a>."},"publication_status":"published","date_created":"2018-12-11T12:08:40Z","doi":"1544","month":"01","year":"2007","page":"664 - 678","title":"Model Checking on Trees with Path Equivalences","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"date_updated":"2021-01-12T07:56:43Z","_id":"4402","type":"conference"},{"intvolume":"         1","year":"2007","month":"01","issue":"4","main_file_link":[{"open_access":"0","url":"http://www.biomedcentral.com/1752-0509/1/4"}],"title":"Qualitative networks: A symbolic approach to analyze biological signaling networks","type":"journal_article","_id":"4405","date_updated":"2021-01-12T07:56:44Z","abstract":[{"lang":"eng","text":"Background\nA 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.\n\nResults\nWe 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.\n\nConclusion\nWe 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."}],"publist_id":"325","publisher":"BioMed Central","day":"08","publication":"BMC Systems Biology","date_published":"2007-01-08T00:00:00Z","extern":1,"citation":{"mla":"Schaub, Marc, et al. “Qualitative Networks: A Symbolic Approach to Analyze Biological Signaling Networks.” <i>BMC Systems Biology</i>, vol. 1, no. 4, BioMed Central, 2007, doi:<a href=\"https://doi.org/10.1186/1752-0509-1-4\">10.1186/1752-0509-1-4</a>.","short":"M. Schaub, T.A. Henzinger, J. Fisher, BMC Systems Biology 1 (2007).","ista":"Schaub M, Henzinger TA, Fisher J. 2007. Qualitative networks: A symbolic approach to analyze biological signaling networks. BMC Systems Biology. 1(4).","ieee":"M. Schaub, T. A. Henzinger, and J. Fisher, “Qualitative networks: A symbolic approach to analyze biological signaling networks,” <i>BMC Systems Biology</i>, vol. 1, no. 4. BioMed Central, 2007.","apa":"Schaub, M., Henzinger, T. A., &#38; Fisher, J. (2007). Qualitative networks: A symbolic approach to analyze biological signaling networks. <i>BMC Systems Biology</i>. BioMed Central. <a href=\"https://doi.org/10.1186/1752-0509-1-4\">https://doi.org/10.1186/1752-0509-1-4</a>","chicago":"Schaub, Marc, Thomas A Henzinger, and Jasmin Fisher. “Qualitative Networks: A Symbolic Approach to Analyze Biological Signaling Networks.” <i>BMC Systems Biology</i>. BioMed Central, 2007. <a href=\"https://doi.org/10.1186/1752-0509-1-4\">https://doi.org/10.1186/1752-0509-1-4</a>.","ama":"Schaub M, Henzinger TA, Fisher J. Qualitative networks: A symbolic approach to analyze biological signaling networks. <i>BMC Systems Biology</i>. 2007;1(4). doi:<a href=\"https://doi.org/10.1186/1752-0509-1-4\">10.1186/1752-0509-1-4</a>"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"quality_controlled":0,"author":[{"last_name":"Schaub","first_name":"Marc","full_name":"Schaub, Marc A"},{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Fisher","full_name":"Fisher, Jasmin","first_name":"Jasmin"}],"status":"public","doi":"10.1186/1752-0509-1-4","volume":1,"publication_status":"published","date_created":"2018-12-11T12:08:41Z"},{"date_published":"2007-03-30T00:00:00Z","publication":"Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday","day":"30","publisher":"Springer","publist_id":"314","abstract":[{"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.","lang":"eng"}],"publication_status":"published","date_created":"2018-12-11T12:08:45Z","volume":4444,"doi":"10.1007/978-3-540-71322-7_13","quality_controlled":0,"status":"public","author":[{"last_name":"Manevich","full_name":"Manevich, Roman","first_name":"Roman"},{"full_name":"Field, John","first_name":"John","last_name":"Field"},{"orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ramalingam","first_name":"Ganesan","full_name":"Ramalingam, Ganesan"},{"last_name":"Sagiv","first_name":"Mooly","full_name":"Sagiv, Mooly"}],"alternative_title":["LNCS"],"extern":1,"citation":{"ama":"Manevich R, Field J, Henzinger TA, Ramalingam G, Sagiv M. Abstract counterexample-based refinement for powerset domains. In: <i>Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday</i>. Vol 4444. Springer; 2007:273-292. doi:<a href=\"https://doi.org/10.1007/978-3-540-71322-7_13\">10.1007/978-3-540-71322-7_13</a>","apa":"Manevich, R., Field, J., Henzinger, T. A., Ramalingam, G., &#38; Sagiv, M. (2007). Abstract counterexample-based refinement for powerset domains. In <i>Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday</i> (Vol. 4444, pp. 273–292). Springer. <a href=\"https://doi.org/10.1007/978-3-540-71322-7_13\">https://doi.org/10.1007/978-3-540-71322-7_13</a>","chicago":"Manevich, Roman, John Field, Thomas A Henzinger, Ganesan Ramalingam, and Mooly Sagiv. “Abstract Counterexample-Based Refinement for Powerset Domains.” In <i>Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday</i>, 4444:273–92. Springer, 2007. <a href=\"https://doi.org/10.1007/978-3-540-71322-7_13\">https://doi.org/10.1007/978-3-540-71322-7_13</a>.","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.","ieee":"R. Manevich, J. Field, T. A. Henzinger, G. Ramalingam, and M. Sagiv, “Abstract counterexample-based refinement for powerset domains,” in <i>Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday</i>, vol. 4444, Springer, 2007, pp. 273–292.","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.","mla":"Manevich, Roman, et al. “Abstract Counterexample-Based Refinement for Powerset Domains.” <i>Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday</i>, vol. 4444, Springer, 2007, pp. 273–92, doi:<a href=\"https://doi.org/10.1007/978-3-540-71322-7_13\">10.1007/978-3-540-71322-7_13</a>."},"page":"273 - 292","month":"03","acknowledgement":"This research is partially supported by the Clore Fellowship Programme. Supported in part by the Swiss National Science Foundation.","intvolume":"      4444","year":"2007","date_updated":"2021-01-12T07:56:49Z","type":"book_chapter","_id":"4417","title":"Abstract counterexample-based refinement for powerset domains"},{"abstract":[{"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.","lang":"eng"}],"publist_id":"286","day":"01","publisher":"ACM","date_published":"2007-10-01T00:00:00Z","publication":"ACM Transactions on Programming Languages and Systems (TOPLAS)","status":"public","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Thomas Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Kirsch, Christoph M","first_name":"Christoph","last_name":"Kirsch"}],"quality_controlled":0,"citation":{"ieee":"T. A. Henzinger and C. Kirsch, “The embedded machine: Predictable, portable real-time code,” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>, 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).","short":"T.A. Henzinger, C. Kirsch, ACM Transactions on Programming Languages and Systems (TOPLAS) 29 (2007).","mla":"Henzinger, Thomas A., and Christoph Kirsch. “The Embedded Machine: Predictable, Portable Real-Time Code.” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>, vol. 29, no. 393, ACM, 2007, doi:<a href=\"https://doi.org/10.1145/1286821.1286824\">10.1145/1286821.1286824</a>.","ama":"Henzinger TA, Kirsch C. The embedded machine: Predictable, portable real-time code. <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. 2007;29(393). doi:<a href=\"https://doi.org/10.1145/1286821.1286824\">10.1145/1286821.1286824</a>","chicago":"Henzinger, Thomas A, and Christoph Kirsch. “The Embedded Machine: Predictable, Portable Real-Time Code.” <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. ACM, 2007. <a href=\"https://doi.org/10.1145/1286821.1286824\">https://doi.org/10.1145/1286821.1286824</a>.","apa":"Henzinger, T. A., &#38; Kirsch, C. (2007). The embedded machine: Predictable, portable real-time code. <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>. ACM. <a href=\"https://doi.org/10.1145/1286821.1286824\">https://doi.org/10.1145/1286821.1286824</a>"},"extern":1,"doi":"10.1145/1286821.1286824","publication_status":"published","date_created":"2018-12-11T12:08:53Z","volume":29,"year":"2007","intvolume":"        29","month":"10","issue":393,"title":"The embedded machine: Predictable, portable real-time code","date_updated":"2021-01-12T07:57:01Z","type":"journal_article","_id":"4446"},{"conference":{"name":"DLT: Developments in Language Theory"},"_id":"4511","type":"conference","date_updated":"2021-01-12T07:59:21Z","title":"Quantitative generalizations of languages","page":"20 - 22","month":"06","acknowledgement":"This research was supported in part by the Swiss National Science Foundation and by the NSF grant CCR-0225610.","intvolume":"      4588","year":"2007","volume":4588,"date_created":"2018-12-11T12:09:14Z","publication_status":"published","doi":"10.1007/978-3-540-73208-2_2","citation":{"ama":"Henzinger TA. Quantitative generalizations of languages. In: Vol 4588. Springer; 2007:20-22. doi:<a href=\"https://doi.org/10.1007/978-3-540-73208-2_2\">10.1007/978-3-540-73208-2_2</a>","apa":"Henzinger, T. A. (2007). Quantitative generalizations of languages (Vol. 4588, pp. 20–22). Presented at the DLT: Developments in Language Theory, Springer. <a href=\"https://doi.org/10.1007/978-3-540-73208-2_2\">https://doi.org/10.1007/978-3-540-73208-2_2</a>","chicago":"Henzinger, Thomas A. “Quantitative Generalizations of Languages,” 4588:20–22. Springer, 2007. <a href=\"https://doi.org/10.1007/978-3-540-73208-2_2\">https://doi.org/10.1007/978-3-540-73208-2_2</a>.","ista":"Henzinger TA. 2007. Quantitative generalizations of languages. DLT: Developments in Language Theory, LNCS, vol. 4588, 20–22.","ieee":"T. A. Henzinger, “Quantitative generalizations of languages,” presented at the DLT: Developments in Language Theory, 2007, vol. 4588, pp. 20–22.","mla":"Henzinger, Thomas A. <i>Quantitative Generalizations of Languages</i>. Vol. 4588, Springer, 2007, pp. 20–22, doi:<a href=\"https://doi.org/10.1007/978-3-540-73208-2_2\">10.1007/978-3-540-73208-2_2</a>.","short":"T.A. Henzinger, in:, Springer, 2007, pp. 20–22."},"extern":1,"alternative_title":["LNCS"],"quality_controlled":0,"status":"public","author":[{"first_name":"Thomas A","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"}],"date_published":"2007-06-21T00:00:00Z","day":"21","publisher":"Springer","publist_id":"218","abstract":[{"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.","lang":"eng"}]},{"publisher":"Springer","day":"04","date_published":"2007-01-04T00:00:00Z","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."}],"publist_id":"217","doi":"10.1007/978-3-540-69507-3_7","publication_status":"published","date_created":"2018-12-11T12:09:15Z","volume":4362,"quality_controlled":0,"author":[{"full_name":"Thomas Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"}],"alternative_title":["LNCS"],"status":"public","citation":{"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. <a href=\"https://doi.org/10.1007/978-3-540-69507-3_7\">https://doi.org/10.1007/978-3-540-69507-3_7</a>","chicago":"Henzinger, Thomas A. “Games, Time, and Probability: Graph Models for System Design and Analysis,” 4362:103–10. Springer, 2007. <a href=\"https://doi.org/10.1007/978-3-540-69507-3_7\">https://doi.org/10.1007/978-3-540-69507-3_7</a>.","ama":"Henzinger TA. Games, time, and probability: Graph models for system design and analysis. In: Vol 4362. Springer; 2007:103-110. doi:<a href=\"https://doi.org/10.1007/978-3-540-69507-3_7\">10.1007/978-3-540-69507-3_7</a>","mla":"Henzinger, Thomas A. <i>Games, Time, and Probability: Graph Models for System Design and Analysis</i>. Vol. 4362, Springer, 2007, pp. 103–10, doi:<a href=\"https://doi.org/10.1007/978-3-540-69507-3_7\">10.1007/978-3-540-69507-3_7</a>.","short":"T.A. Henzinger, in:, Springer, 2007, pp. 103–110.","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."},"extern":1,"page":"103 - 110","year":"2007","acknowledgement":"This research was supported in part by the Swiss National Science Foundation, and by the NSF ITR grant CCR-0225610.","intvolume":"      4362","month":"01","date_updated":"2021-01-12T07:59:22Z","type":"conference","_id":"4514","conference":{"name":"SOFSEM: Current Trends in Theory and Practice of Computer Science"},"title":"Games, time, and probability: Graph models for system design and analysis"},{"date_published":"2007-01-01T00:00:00Z","publication":"Nature Biotechnology","publisher":"Nature Publishing Group","day":"01","publist_id":"198","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."}],"publication_status":"published","date_created":"2018-12-11T12:09:19Z","volume":25,"doi":"10.1038/nbt1356","quality_controlled":0,"status":"public","author":[{"full_name":"Fisher, Jasmin","first_name":"Jasmin","last_name":"Fisher"},{"first_name":"Thomas A","full_name":"Thomas Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"}],"extern":1,"citation":{"chicago":"Fisher, Jasmin, and Thomas A Henzinger. “Executable Cell Biology.” <i>Nature Biotechnology</i>. Nature Publishing Group, 2007. <a href=\"https://doi.org/10.1038/nbt1356\">https://doi.org/10.1038/nbt1356</a>.","apa":"Fisher, J., &#38; Henzinger, T. A. (2007). Executable cell biology. <i>Nature Biotechnology</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/nbt1356\">https://doi.org/10.1038/nbt1356</a>","ama":"Fisher J, Henzinger TA. Executable cell biology. <i>Nature Biotechnology</i>. 2007;25:1239-1249. doi:<a href=\"https://doi.org/10.1038/nbt1356\">10.1038/nbt1356</a>","short":"J. Fisher, T.A. Henzinger, Nature Biotechnology 25 (2007) 1239–1249.","mla":"Fisher, Jasmin, and Thomas A. Henzinger. “Executable Cell Biology.” <i>Nature Biotechnology</i>, vol. 25, Nature Publishing Group, 2007, pp. 1239–49, doi:<a href=\"https://doi.org/10.1038/nbt1356\">10.1038/nbt1356</a>.","ieee":"J. Fisher and T. A. Henzinger, “Executable cell biology,” <i>Nature Biotechnology</i>, vol. 25. Nature Publishing Group, pp. 1239–1249, 2007.","ista":"Fisher J, Henzinger TA. 2007. Executable cell biology. Nature Biotechnology. 25, 1239–1249."},"page":"1239 - 1249","month":"01","year":"2007","intvolume":"        25","date_updated":"2021-01-12T07:59:28Z","type":"journal_article","_id":"4529","title":"Executable cell biology"},{"month":"09","year":"2007","intvolume":"      4646","title":"CSL: Computer Science Logic ","date_updated":"2019-08-02T12:38:32Z","type":"conference_editor","_id":"4530","publist_id":"194","abstract":[{"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.","lang":"eng"}],"date_published":"2007-09-01T00:00:00Z","publication":"CSL: Computer Science Logic","publisher":"Springer","day":"01","author":[{"last_name":"Duparc","first_name":"Jacques","full_name":"Duparc, Jacques"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Thomas Henzinger"}],"status":"public","alternative_title":["LNCS"],"quality_controlled":0,"extern":1,"citation":{"ista":"Duparc J, Henzinger TA. 2007. CSL: Computer Science Logic , Springer,p.","ieee":"J. Duparc and T. A. Henzinger, <i>CSL: Computer Science Logic </i>, vol. 4646. Springer, 2007.","mla":"Duparc, Jacques, and Thomas A. Henzinger. “CSL: Computer Science Logic .” <i>CSL: Computer Science Logic</i>, vol. 4646, Springer, 2007, doi:<a href=\"https://doi.org/10.1007/978-3-540-74915-8\">10.1007/978-3-540-74915-8</a>.","short":"J. Duparc, T.A. Henzinger, CSL: Computer Science Logic , Springer, 2007.","ama":"Duparc J, Henzinger TA. <i>CSL: Computer Science Logic </i>. Vol 4646. Springer; 2007. doi:<a href=\"https://doi.org/10.1007/978-3-540-74915-8\">10.1007/978-3-540-74915-8</a>","apa":"Duparc, J., &#38; Henzinger, T. A. (2007). <i>CSL: Computer Science Logic </i>. <i>CSL: Computer Science Logic</i> (Vol. 4646). Springer. <a href=\"https://doi.org/10.1007/978-3-540-74915-8\">https://doi.org/10.1007/978-3-540-74915-8</a>","chicago":"Duparc, Jacques, and Thomas A Henzinger. <i>CSL: Computer Science Logic </i>. <i>CSL: Computer Science Logic</i>. Vol. 4646. Springer, 2007. <a href=\"https://doi.org/10.1007/978-3-540-74915-8\">https://doi.org/10.1007/978-3-540-74915-8</a>."},"date_created":"2018-12-11T12:09:20Z","publication_status":"published","volume":4646,"doi":"10.1007/978-3-540-74915-8"},{"publication_status":"published","date_created":"2018-12-11T12:09:20Z","volume":"3(5):e92","doi":"10.1371/journal.pcbi.0030092","quality_controlled":0,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"author":[{"full_name":"Fisher, Jasmin","first_name":"Jasmin","last_name":"Fisher"},{"last_name":"Piterman","full_name":"Piterman, Nir","first_name":"Nir"},{"last_name":"Hajnal","full_name":"Hajnal, Alex","first_name":"Alex"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Thomas Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724"}],"status":"public","citation":{"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.","ieee":"J. Fisher, N. Piterman, A. Hajnal, and T. A. Henzinger, “Predictive modeling of signaling crosstalk during C. elegans vulval development,” <i>PLoS Computational Biology</i>, vol. 3(5):e92. Public Library of Science, 2007.","short":"J. Fisher, N. Piterman, A. Hajnal, T.A. Henzinger, PLoS Computational Biology 3(5):e92 (2007).","mla":"Fisher, Jasmin, et al. “Predictive Modeling of Signaling Crosstalk during C. Elegans Vulval Development.” <i>PLoS Computational Biology</i>, vol. 3(5):e92, Public Library of Science, 2007, doi:<a href=\"https://doi.org/10.1371/journal.pcbi.0030092\">10.1371/journal.pcbi.0030092</a>.","ama":"Fisher J, Piterman N, Hajnal A, Henzinger TA. Predictive modeling of signaling crosstalk during C. elegans vulval development. <i>PLoS Computational Biology</i>. 2007;3(5):e92. doi:<a href=\"https://doi.org/10.1371/journal.pcbi.0030092\">10.1371/journal.pcbi.0030092</a>","apa":"Fisher, J., Piterman, N., Hajnal, A., &#38; Henzinger, T. A. (2007). Predictive modeling of signaling crosstalk during C. elegans vulval development. <i>PLoS Computational Biology</i>. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pcbi.0030092\">https://doi.org/10.1371/journal.pcbi.0030092</a>","chicago":"Fisher, Jasmin, Nir Piterman, Alex Hajnal, and Thomas A Henzinger. “Predictive Modeling of Signaling Crosstalk during C. Elegans Vulval Development.” <i>PLoS Computational Biology</i>. Public Library of Science, 2007. <a href=\"https://doi.org/10.1371/journal.pcbi.0030092\">https://doi.org/10.1371/journal.pcbi.0030092</a>."},"extern":1,"date_published":"2007-05-18T00:00:00Z","publication":"PLoS Computational Biology","publisher":"Public Library of Science","day":"18","publist_id":"195","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."}],"date_updated":"2021-01-12T07:59:29Z","_id":"4531","type":"journal_article","title":"Predictive modeling of signaling crosstalk during C. elegans vulval development","month":"05","acknowledgement":"This work was supported in part by the Swiss National Science Foundation (grant 205321–111840).","year":"2007"},{"month":"01","intvolume":"      4424","year":"2007","acknowledgement":"This research was supported in part by the Swiss National Science Foundation and by the NSF grants CCR-0225610 and CCR-0234690.","page":"261 - 275","title":"Assume-guarantee synthesis","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"date_updated":"2021-01-12T07:59:32Z","_id":"4537","type":"conference","publist_id":"186","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."}],"date_published":"2007-01-01T00:00:00Z","publisher":"Springer","day":"01","status":"public","alternative_title":["LNCS"],"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Krishnendu Chatterjee","first_name":"Krishnendu"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Thomas Henzinger"}],"quality_controlled":0,"extern":1,"citation":{"short":"K. Chatterjee, T.A. Henzinger, in:, Springer, 2007, pp. 261–275.","mla":"Chatterjee, Krishnendu, and Thomas A. Henzinger. <i>Assume-Guarantee Synthesis</i>. Vol. 4424, Springer, 2007, pp. 261–75, doi:<a href=\"https://doi.org/10.1007/978-3-540-71209-1_21\">10.1007/978-3-540-71209-1_21</a>.","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.","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.","apa":"Chatterjee, K., &#38; 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. <a href=\"https://doi.org/10.1007/978-3-540-71209-1_21\">https://doi.org/10.1007/978-3-540-71209-1_21</a>","chicago":"Chatterjee, Krishnendu, and Thomas A Henzinger. “Assume-Guarantee Synthesis,” 4424:261–75. Springer, 2007. <a href=\"https://doi.org/10.1007/978-3-540-71209-1_21\">https://doi.org/10.1007/978-3-540-71209-1_21</a>.","ama":"Chatterjee K, Henzinger TA. Assume-guarantee synthesis. In: Vol 4424. Springer; 2007:261-275. doi:<a href=\"https://doi.org/10.1007/978-3-540-71209-1_21\">10.1007/978-3-540-71209-1_21</a>"},"date_created":"2018-12-11T12:09:22Z","publication_status":"published","volume":4424,"doi":"10.1007/978-3-540-71209-1_21"}]