--- _id: '3984' abstract: - lang: eng text: We combine topological and geometric methods to construct a multiresolution representation for a function over a two-dimensional domain. In a preprocessing stage, we create the Morse-Smale complex of the function and progressively simplify its topology by cancelling pairs of critical points. Based on a simple notion of dependency among these cancellations, we construct a hierarchical data structure supporting traversal and reconstruction operations similarly to traditional geometry-based representations. We use this data structure to extract topologically valid approximations that satisfy error bounds provided at runtime. author: - first_name: Peer full_name: Bremer, Peer-Timo last_name: Bremer - first_name: Herbert full_name: Herbert Edelsbrunner id: 3FB178DA-F248-11E8-B48F-1D18A9856A87 last_name: Edelsbrunner orcid: 0000-0002-9823-6833 - first_name: Bernd full_name: Hamann, Bernd last_name: Hamann - first_name: Valerio full_name: Pascucci, Valerio last_name: Pascucci citation: ama: Bremer P, Edelsbrunner H, Hamann B, Pascucci V. A topological hierarchy for functions on triangulated surfaces. IEEE Transactions on Visualization and Computer Graphics. 2004;10(4):385-396. doi:10.1109/TVCG.2004.3 apa: Bremer, P., Edelsbrunner, H., Hamann, B., & Pascucci, V. (2004). A topological hierarchy for functions on triangulated surfaces. IEEE Transactions on Visualization and Computer Graphics. IEEE. https://doi.org/10.1109/TVCG.2004.3 chicago: Bremer, Peer, Herbert Edelsbrunner, Bernd Hamann, and Valerio Pascucci. “A Topological Hierarchy for Functions on Triangulated Surfaces.” IEEE Transactions on Visualization and Computer Graphics. IEEE, 2004. https://doi.org/10.1109/TVCG.2004.3. ieee: P. Bremer, H. Edelsbrunner, B. Hamann, and V. Pascucci, “A topological hierarchy for functions on triangulated surfaces,” IEEE Transactions on Visualization and Computer Graphics, vol. 10, no. 4. IEEE, pp. 385–396, 2004. ista: Bremer P, Edelsbrunner H, Hamann B, Pascucci V. 2004. A topological hierarchy for functions on triangulated surfaces. IEEE Transactions on Visualization and Computer Graphics. 10(4), 385–396. mla: Bremer, Peer, et al. “A Topological Hierarchy for Functions on Triangulated Surfaces.” IEEE Transactions on Visualization and Computer Graphics, vol. 10, no. 4, IEEE, 2004, pp. 385–96, doi:10.1109/TVCG.2004.3. short: P. Bremer, H. Edelsbrunner, B. Hamann, V. Pascucci, IEEE Transactions on Visualization and Computer Graphics 10 (2004) 385–396. date_created: 2018-12-11T12:06:16Z date_published: 2004-07-01T00:00:00Z date_updated: 2021-01-12T07:53:39Z day: '01' doi: 10.1109/TVCG.2004.3 extern: 1 intvolume: ' 10' issue: '4' month: '07' page: 385 - 396 publication: IEEE Transactions on Visualization and Computer Graphics publication_status: published publisher: IEEE publist_id: '2139' quality_controlled: 0 status: public title: A topological hierarchy for functions on triangulated surfaces type: journal_article volume: 10 year: '2004' ... --- _id: '3987' abstract: - lang: eng text: 'We consider scientific data sets that describe density functions over three-dimensional geometric domains. Such data sets are often large and coarsened representations are needed for visualization and analysis. Assuming a tetrahedral mesh representation, we construct such representations with a simplification algorithm that combines three goals: the approximation of the function, the preservation of the mesh topology, and the improvement of the mesh quality. The third goal is achieved with a novel extension of the well-known quadric error metric. We perform a number of computational experiments to understand the effect of mesh quality improvement on the density map approximation. In addition, we study the effect of geometric simplification on the topological features of the function by monitoring its critical points.' author: - first_name: Vijay full_name: Natarajan, Vijay last_name: Natarajan - first_name: Herbert full_name: Herbert Edelsbrunner id: 3FB178DA-F248-11E8-B48F-1D18A9856A87 last_name: Edelsbrunner orcid: 0000-0002-9823-6833 citation: ama: Natarajan V, Edelsbrunner H. Simplification of three-dimensional density maps. IEEE Transactions on Visualization and Computer Graphics. 2004;10(5):587-597. doi:10.1109/TVCG.2004.32 apa: Natarajan, V., & Edelsbrunner, H. (2004). Simplification of three-dimensional density maps. IEEE Transactions on Visualization and Computer Graphics. IEEE. https://doi.org/10.1109/TVCG.2004.32 chicago: Natarajan, Vijay, and Herbert Edelsbrunner. “Simplification of Three-Dimensional Density Maps.” IEEE Transactions on Visualization and Computer Graphics. IEEE, 2004. https://doi.org/10.1109/TVCG.2004.32. ieee: V. Natarajan and H. Edelsbrunner, “Simplification of three-dimensional density maps,” IEEE Transactions on Visualization and Computer Graphics, vol. 10, no. 5. IEEE, pp. 587–597, 2004. ista: Natarajan V, Edelsbrunner H. 2004. Simplification of three-dimensional density maps. IEEE Transactions on Visualization and Computer Graphics. 10(5), 587–597. mla: Natarajan, Vijay, and Herbert Edelsbrunner. “Simplification of Three-Dimensional Density Maps.” IEEE Transactions on Visualization and Computer Graphics, vol. 10, no. 5, IEEE, 2004, pp. 587–97, doi:10.1109/TVCG.2004.32. short: V. Natarajan, H. Edelsbrunner, IEEE Transactions on Visualization and Computer Graphics 10 (2004) 587–597. date_created: 2018-12-11T12:06:17Z date_published: 2004-07-12T00:00:00Z date_updated: 2021-01-12T07:53:40Z day: '12' doi: 10.1109/TVCG.2004.32 extern: 1 intvolume: ' 10' issue: '5' month: '07' page: 587 - 597 publication: IEEE Transactions on Visualization and Computer Graphics publication_status: published publisher: IEEE publist_id: '2142' quality_controlled: 0 status: public title: Simplification of three-dimensional density maps type: journal_article volume: 10 year: '2004' ... --- _id: '3985' abstract: - lang: eng text: Given a Morse function f over a 2-manifold with or without boundary, the Reeb graph is obtained by contracting the connected components of the level sets to points. We prove tight upper and lower bounds on the number of loops in the Reeb graph that depend on the genus, the number of boundary components, and whether or not the 2-manifold is orientable. We also give an algorithm that constructs the Reeb graph in time O(n log n), where n is the number of edges in the triangulation used to represent the 2-manifold and the Morse function. acknowledgement: Partially supported by NSF under Grants EIA-99-72879 and CCR-00-86013. author: - first_name: Kree full_name: Cole-McLaughlin, Kree last_name: Cole Mclaughlin - first_name: Herbert full_name: Herbert Edelsbrunner id: 3FB178DA-F248-11E8-B48F-1D18A9856A87 last_name: Edelsbrunner orcid: 0000-0002-9823-6833 - first_name: John full_name: Harer, John last_name: Harer - first_name: Vijay full_name: Natarajan, Vijay last_name: Natarajan - first_name: Valerio full_name: Pascucci, Valerio last_name: Pascucci citation: ama: Cole Mclaughlin K, Edelsbrunner H, Harer J, Natarajan V, Pascucci V. Loops in Reeb graphs of 2-manifolds. Discrete & Computational Geometry. 2004;32(2):231-244. doi:10.1007/s00454-004-1122-6 apa: Cole Mclaughlin, K., Edelsbrunner, H., Harer, J., Natarajan, V., & Pascucci, V. (2004). Loops in Reeb graphs of 2-manifolds. Discrete & Computational Geometry. Springer. https://doi.org/10.1007/s00454-004-1122-6 chicago: Cole Mclaughlin, Kree, Herbert Edelsbrunner, John Harer, Vijay Natarajan, and Valerio Pascucci. “Loops in Reeb Graphs of 2-Manifolds.” Discrete & Computational Geometry. Springer, 2004. https://doi.org/10.1007/s00454-004-1122-6. ieee: K. Cole Mclaughlin, H. Edelsbrunner, J. Harer, V. Natarajan, and V. Pascucci, “Loops in Reeb graphs of 2-manifolds,” Discrete & Computational Geometry, vol. 32, no. 2. Springer, pp. 231–244, 2004. ista: Cole Mclaughlin K, Edelsbrunner H, Harer J, Natarajan V, Pascucci V. 2004. Loops in Reeb graphs of 2-manifolds. Discrete & Computational Geometry. 32(2), 231–244. mla: Cole Mclaughlin, Kree, et al. “Loops in Reeb Graphs of 2-Manifolds.” Discrete & Computational Geometry, vol. 32, no. 2, Springer, 2004, pp. 231–44, doi:10.1007/s00454-004-1122-6. short: K. Cole Mclaughlin, H. Edelsbrunner, J. Harer, V. Natarajan, V. Pascucci, Discrete & Computational Geometry 32 (2004) 231–244. date_created: 2018-12-11T12:06:16Z date_published: 2004-07-01T00:00:00Z date_updated: 2021-01-12T07:53:39Z day: '01' doi: 10.1007/s00454-004-1122-6 extern: 1 intvolume: ' 32' issue: '2' month: '07' page: 231 - 244 publication: Discrete & Computational Geometry publication_status: published publisher: Springer publist_id: '2140' quality_controlled: 0 status: public title: Loops in Reeb graphs of 2-manifolds type: journal_article volume: 32 year: '2004' ... --- _id: '3989' abstract: - lang: eng text: We introduce local and global comparison measures for a collection of k less than or equal to d real-valued smooth functions on a common d-dimensional Riemannian manifold. For k = d = 2 we relate the measures to the set of critical points of one function restricted to the level sets of the other. The definition of the measures extends to piecewise linear functions for which they ace easy to compute. The computation of the measures forms the centerpiece of a software tool which we use to study scientific datasets. author: - first_name: Herbert full_name: Herbert Edelsbrunner id: 3FB178DA-F248-11E8-B48F-1D18A9856A87 last_name: Edelsbrunner orcid: 0000-0002-9823-6833 - first_name: John full_name: Harer, John last_name: Harer - first_name: Vijay full_name: Natarajan, Vijay last_name: Natarajan - first_name: Valerio full_name: Pascucci, Valerio last_name: Pascucci citation: ama: 'Edelsbrunner H, Harer J, Natarajan V, Pascucci V. Local and global comparison of continuous functions. In: IEEE; 2004:275-280. doi:10.1109/VISUAL.2004.68' apa: 'Edelsbrunner, H., Harer, J., Natarajan, V., & Pascucci, V. (2004). Local and global comparison of continuous functions (pp. 275–280). Presented at the VIS: IEEE Visualization, IEEE. https://doi.org/10.1109/VISUAL.2004.68' chicago: Edelsbrunner, Herbert, John Harer, Vijay Natarajan, and Valerio Pascucci. “Local and Global Comparison of Continuous Functions,” 275–80. IEEE, 2004. https://doi.org/10.1109/VISUAL.2004.68. ieee: 'H. Edelsbrunner, J. Harer, V. Natarajan, and V. Pascucci, “Local and global comparison of continuous functions,” presented at the VIS: IEEE Visualization, 2004, pp. 275–280.' ista: 'Edelsbrunner H, Harer J, Natarajan V, Pascucci V. 2004. Local and global comparison of continuous functions. VIS: IEEE Visualization, 275–280.' mla: Edelsbrunner, Herbert, et al. Local and Global Comparison of Continuous Functions. IEEE, 2004, pp. 275–80, doi:10.1109/VISUAL.2004.68. short: H. Edelsbrunner, J. Harer, V. Natarajan, V. Pascucci, in:, IEEE, 2004, pp. 275–280. conference: name: 'VIS: IEEE Visualization' date_created: 2018-12-11T12:06:18Z date_published: 2004-10-01T00:00:00Z date_updated: 2021-01-12T07:53:41Z day: '01' doi: 10.1109/VISUAL.2004.68 extern: 1 month: '10' page: 275 - 280 publication_status: published publisher: IEEE publist_id: '2137' quality_controlled: 0 status: public title: Local and global comparison of continuous functions type: conference year: '2004' ... --- _id: '4172' abstract: - lang: eng text: 'During vertebrate gastrulation, a relatively limited number of blastodermal cells undergoes a stereotypical set of cellular movements that leads to formation of the three germ layers: ectoderm, mesoderm and endoderm. Gastrulation, therefore, provides a unique developmental system in which to study cell movements in vivo in a fairly simple cellular context. Recent advances have been made in elucidating the cellular and molecular mechanisms that underlie cell movements during zebrafish gastrulation. These findings can be compared with observations made in other model systems to identify potential general mechanisms of cell migration during development.' article_processing_charge: No author: - first_name: Juan full_name: Montero, Juan last_name: Montero - first_name: Carl-Philipp J full_name: Heisenberg, Carl-Philipp J id: 39427864-F248-11E8-B48F-1D18A9856A87 last_name: Heisenberg orcid: 0000-0002-0912-4566 citation: ama: 'Montero J, Heisenberg C-PJ. Gastrulation dynamics: cells move into focus. Trends in Cell Biology. 2004;14(11):620-627. doi:10.1016/j.tcb.2004.09.008' apa: 'Montero, J., & Heisenberg, C.-P. J. (2004). Gastrulation dynamics: cells move into focus. Trends in Cell Biology. Cell Press. https://doi.org/10.1016/j.tcb.2004.09.008' chicago: 'Montero, Juan, and Carl-Philipp J Heisenberg. “Gastrulation Dynamics: Cells Move into Focus.” Trends in Cell Biology. Cell Press, 2004. https://doi.org/10.1016/j.tcb.2004.09.008.' ieee: 'J. Montero and C.-P. J. Heisenberg, “Gastrulation dynamics: cells move into focus,” Trends in Cell Biology, vol. 14, no. 11. Cell Press, pp. 620–627, 2004.' ista: 'Montero J, Heisenberg C-PJ. 2004. Gastrulation dynamics: cells move into focus. Trends in Cell Biology. 14(11), 620–627.' mla: 'Montero, Juan, and Carl-Philipp J. Heisenberg. “Gastrulation Dynamics: Cells Move into Focus.” Trends in Cell Biology, vol. 14, no. 11, Cell Press, 2004, pp. 620–27, doi:10.1016/j.tcb.2004.09.008.' short: J. Montero, C.-P.J. Heisenberg, Trends in Cell Biology 14 (2004) 620–627. date_created: 2018-12-11T12:07:23Z date_published: 2004-11-01T00:00:00Z date_updated: 2021-01-12T07:55:02Z day: '01' doi: 10.1016/j.tcb.2004.09.008 extern: '1' intvolume: ' 14' issue: '11' language: - iso: eng month: '11' oa_version: None page: 620 - 627 publication: Trends in Cell Biology publication_status: published publisher: Cell Press publist_id: '1948' status: public title: 'Gastrulation dynamics: cells move into focus' type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 14 year: '2004' ... --- _id: '4238' abstract: - lang: eng text: The dynamical basis of tumoral growth has been controversial. Many models have been proposed to explain cancer development. The descriptions employ exponential, potential, logistic or Gompertzian growth laws. Some of these models are concerned with the interaction between cancer and the immunological, system. Among other properties, these models are concerned with the microscopic behavior of tumors and the emergence of cancer. We propose a modification of a previous model by Stepanova, which describes the specific immunological response against cancer. The modification consists of the substitution of a Gompertian law for the exponential rate used for tumoral growth. This modification is motivated by the numerous works confirming that Gompertz's equation correctly describes solid tumor growth. The modified model predicts that near zero, tumors always tend to grow. Immunological contraposition never suffices to induce a complete regression of the tumor. Instead, a stable microscopic equilibrium between cancer and immunological activity can be attained. In other words, our model predicts that the theory of immune surveillance is plausible. A macroscopic equilibrium in which the system develops cancer is also possible. In this case, immunological activity is depleted. This is consistent with the phenomena of cancer tolerance. Both equilibrium points can coexist or can exist without the other. In all cases the fixed point at zero tumor size is unstable. Since immunity cannot induce a complete tumor regression, a therapy is required. We include constant-dose therapies and show that they are insufficient. Final levels of immunocompetent cells and tumoral cells are finite, thus post-treatment regrowth of the tumor is certain. We also evaluate late-intensification therapies which are successful. They induce an asymptotic regression to zero tumor size. Immune response is also suppressed by the therapy, and thus plays a negligible role in the remission. We conclude that treatment evaluation should be successful without taking into account immunological effects. (C) 2003 Elsevier Ltd. All rights reserved. article_processing_charge: No author: - first_name: Harold full_name: de Vladar, Harold id: 2A181218-F248-11E8-B48F-1D18A9856A87 last_name: de Vladar orcid: 0000-0002-5985-7653 - first_name: J. full_name: González, J. last_name: González citation: ama: de Vladar H, González J. Dynamic response of cancer under the influence of immunological activity and therapy. Journal of Theoretical Biology. 2004;227(3):335-348. doi:3801 apa: de Vladar, H., & González, J. (2004). Dynamic response of cancer under the influence of immunological activity and therapy. Journal of Theoretical Biology. Elsevier. https://doi.org/3801 chicago: Vladar, Harold de, and J. González. “Dynamic Response of Cancer under the Influence of Immunological Activity and Therapy.” Journal of Theoretical Biology. Elsevier, 2004. https://doi.org/3801. ieee: H. de Vladar and J. González, “Dynamic response of cancer under the influence of immunological activity and therapy,” Journal of Theoretical Biology, vol. 227, no. 3. Elsevier, pp. 335–348, 2004. ista: de Vladar H, González J. 2004. Dynamic response of cancer under the influence of immunological activity and therapy. Journal of Theoretical Biology. 227(3), 335–348. mla: de Vladar, Harold, and J. González. “Dynamic Response of Cancer under the Influence of Immunological Activity and Therapy.” Journal of Theoretical Biology, vol. 227, no. 3, Elsevier, 2004, pp. 335–48, doi:3801. short: H. de Vladar, J. González, Journal of Theoretical Biology 227 (2004) 335–348. date_created: 2018-12-11T12:07:46Z date_published: 2004-01-01T00:00:00Z date_updated: 2021-01-12T07:55:31Z day: '01' doi: '3801' extern: '1' intvolume: ' 227' issue: '3' language: - iso: eng month: '01' oa_version: None page: 335 - 348 publication: Journal of Theoretical Biology publication_status: published publisher: Elsevier publist_id: '1876' status: public title: Dynamic response of cancer under the influence of immunological activity and therapy type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 227 year: '2004' ... --- _id: '4230' alternative_title: - Cellular Origin and Life in Extreme Habitats and Astrobiology author: - first_name: Harold full_name: Harold Vladar id: 2A181218-F248-11E8-B48F-1D18A9856A87 last_name: Vladar orcid: 0000-0002-5985-7653 - first_name: Roberto full_name: Cipriani, Roberto last_name: Cipriani - first_name: Benjamin full_name: Scharifker, Benjamin last_name: Scharifker - first_name: Jose full_name: Bubis, Jose last_name: Bubis citation: ama: 'de Vladar H, Cipriani R, Scharifker B, Bubis J. A mechanism for the prebiotic emergence of proteins. In: Hanslmeier A, Kempe S, Seckbach J, eds. Life in the Universe From the Miller Experiment to the Search for Life on Other Worlds. Springer; 2004:83-87.' apa: de Vladar, H., Cipriani, R., Scharifker, B., & Bubis, J. (2004). A mechanism for the prebiotic emergence of proteins. In A. Hanslmeier, S. Kempe, & J. Seckbach (Eds.), Life in the Universe From the Miller Experiment to the Search for Life on Other Worlds (pp. 83–87). Springer. chicago: Vladar, Harold de, Roberto Cipriani, Benjamin Scharifker, and Jose Bubis. “A Mechanism for the Prebiotic Emergence of Proteins.” In Life in the Universe From the Miller Experiment to the Search for Life on Other Worlds, edited by A. Hanslmeier, S. Kempe, and J. Seckbach, 83–87. Springer, 2004. ieee: H. de Vladar, R. Cipriani, B. Scharifker, and J. Bubis, “A mechanism for the prebiotic emergence of proteins,” in Life in the Universe From the Miller Experiment to the Search for Life on Other Worlds, A. Hanslmeier, S. Kempe, and J. Seckbach, Eds. Springer, 2004, pp. 83–87. ista: 'de Vladar H, Cipriani R, Scharifker B, Bubis J. 2004.A mechanism for the prebiotic emergence of proteins. In: Life in the Universe From the Miller Experiment to the Search for Life on Other Worlds. Cellular Origin and Life in Extreme Habitats and Astrobiology, , 83–87.' mla: de Vladar, Harold, et al. “A Mechanism for the Prebiotic Emergence of Proteins.” Life in the Universe From the Miller Experiment to the Search for Life on Other Worlds, edited by A. Hanslmeier et al., Springer, 2004, pp. 83–87. short: H. de Vladar, R. Cipriani, B. Scharifker, J. Bubis, in:, A. Hanslmeier, S. Kempe, J. Seckbach (Eds.), Life in the Universe From the Miller Experiment to the Search for Life on Other Worlds, Springer, 2004, pp. 83–87. date_created: 2018-12-11T12:07:44Z date_published: 2004-12-31T00:00:00Z date_updated: 2021-01-12T07:55:28Z day: '31' editor: - first_name: A. full_name: Hanslmeier,A. last_name: Hanslmeier - first_name: S. full_name: Kempe,S. last_name: Kempe - first_name: J. full_name: Seckbach,J. last_name: Seckbach extern: 1 month: '12' page: 83 - 87 publication: Life in the Universe From the Miller Experiment to the Search for Life on Other Worlds publication_status: published publisher: Springer publist_id: '1884' quality_controlled: 0 status: public title: A mechanism for the prebiotic emergence of proteins type: book_chapter year: '2004' ... --- _id: '4236' article_processing_charge: No author: - first_name: Harold full_name: de Vladar, Harold id: 2A181218-F248-11E8-B48F-1D18A9856A87 last_name: de Vladar orcid: 0000-0002-5985-7653 citation: ama: de Vladar H. Métodos no lineales y sus aplicaciones en dinámicas aleatorias de poblaciones celulares. 2004. doi:3810 apa: de Vladar, H. (2004). Métodos no lineales y sus aplicaciones en dinámicas aleatorias de poblaciones celulares. Centro de estudios avazados, IVIC. https://doi.org/3810 chicago: Vladar, Harold de. “Métodos No Lineales y Sus Aplicaciones En Dinámicas Aleatorias de Poblaciones Celulares.” Centro de estudios avazados, IVIC, 2004. https://doi.org/3810. ieee: H. de Vladar, “Métodos no lineales y sus aplicaciones en dinámicas aleatorias de poblaciones celulares,” Centro de estudios avazados, IVIC, 2004. ista: de Vladar H. 2004. Métodos no lineales y sus aplicaciones en dinámicas aleatorias de poblaciones celulares. Centro de estudios avazados, IVIC. mla: de Vladar, Harold. Métodos No Lineales y Sus Aplicaciones En Dinámicas Aleatorias de Poblaciones Celulares. Centro de estudios avazados, IVIC, 2004, doi:3810. short: H. de Vladar, Métodos No Lineales y Sus Aplicaciones En Dinámicas Aleatorias de Poblaciones Celulares, Centro de estudios avazados, IVIC, 2004. date_created: 2018-12-11T12:07:46Z date_published: 2004-01-01T00:00:00Z date_updated: 2021-01-12T07:55:30Z day: '01' doi: '3810' extern: '1' language: - iso: eng month: '01' oa_version: None publication_status: published publisher: Centro de estudios avazados, IVIC publist_id: '1877' status: public title: Métodos no lineales y sus aplicaciones en dinámicas aleatorias de poblaciones celulares type: dissertation user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2004' ... --- _id: '4372' alternative_title: - LNCS 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 citation: ama: 'Maler O, Nickovic D. Monitoring Temporal Properties of Continuous Signals. In: Springer; 2004:152-166. doi:1572' apa: 'Maler, O., & Nickovic, D. (2004). Monitoring Temporal Properties of Continuous Signals (pp. 152–166). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Springer. https://doi.org/1572' chicago: Maler, Oded, and Dejan Nickovic. “Monitoring Temporal Properties of Continuous Signals,” 152–66. Springer, 2004. https://doi.org/1572. ieee: 'O. Maler and D. Nickovic, “Monitoring Temporal Properties of Continuous Signals,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, 2004, pp. 152–166.' ista: 'Maler O, Nickovic D. 2004. Monitoring Temporal Properties of Continuous Signals. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, , 152–166.' mla: Maler, Oded, and Dejan Nickovic. Monitoring Temporal Properties of Continuous Signals. Springer, 2004, pp. 152–66, doi:1572. short: O. Maler, D. Nickovic, in:, Springer, 2004, pp. 152–166. conference: name: 'FORMATS: Formal Modeling and Analysis of Timed Systems' date_created: 2018-12-11T12:08:31Z date_published: 2004-12-14T00:00:00Z date_updated: 2021-01-12T07:56:29Z day: '14' doi: '1572' extern: 1 month: '12' page: 152 - 166 publication_status: published publisher: Springer publist_id: '1088' quality_controlled: 0 status: public title: Monitoring Temporal Properties of Continuous Signals type: conference year: '2004' ... --- _id: '4424' abstract: - lang: eng text: "The enormous cost and ubiquity of software errors necessitates the need for techniques and tools that can precisely analyze large systems and prove that they meet given specifications, or if they don't, return counterexample behaviors showing how the system fails. Recent advances in model checking, decision procedures, program analysis and type systems, and a shift of focus to partial specifications common to several systems (e.g., memory safety and race freedom) have resulted in several practical verification methods. However, these methods are either precise or they are scalable, depending on whether they track the values of variables or only a fixed small set of dataflow facts (e.g., types), and are usually insufficient for precisely verifying large programs.\r\n\r\nWe describe a new technique called Lazy Abstraction (LA) which achieves both precision and scalability by localizing the use of precise information. LA automatically builds, explores and refines a single abstract model of the program in a way that different parts of the model exhibit different degrees of precision, namely just enough to verify the desired property. The algorithm automatically mines the information required by partitioning mechanical proofs of unsatisfiability of spurious counterexamples into Craig Interpolants. For multithreaded systems, we give a new technique based on analyzing the behavior of a single thread executing in a context which is an abstraction of the other (arbitrarily many) threads. We define novel context models and show how to automatically infer them and analyze the full system (thread + context) using LA.\r\n\r\nLA is implemented in BLAST. We have run BLAST on Windows and Linux Device Drivers to verify API conformance properties, and have used it to find (or guarantee the absence of) data races in multithreaded Networked Embedded Systems (NESC) applications. BLAST is able to prove the absence of races in several cases where earlier methods, which depend on lock-based synchronization, fail." article_processing_charge: No author: - first_name: Ranjit full_name: Jhala, Ranjit last_name: Jhala citation: ama: Jhala R. Program verification by lazy abstraction. 2004:1-165. apa: Jhala, R. (2004). Program verification by lazy abstraction. University of California, Berkeley. chicago: Jhala, Ranjit. “Program Verification by Lazy Abstraction.” University of California, Berkeley, 2004. ieee: R. Jhala, “Program verification by lazy abstraction,” University of California, Berkeley, 2004. ista: Jhala R. 2004. Program verification by lazy abstraction. University of California, Berkeley. mla: Jhala, Ranjit. Program Verification by Lazy Abstraction. University of California, Berkeley, 2004, pp. 1–165. short: R. Jhala, Program Verification by Lazy Abstraction, University of California, Berkeley, 2004. date_created: 2018-12-11T12:08:47Z date_published: 2004-12-01T00:00:00Z date_updated: 2021-01-12T07:56:52Z day: '01' extern: '1' language: - iso: eng month: '12' oa_version: None page: 1 - 165 publication_status: published publisher: University of California, Berkeley publist_id: '307' status: public supervisor: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 title: Program verification by lazy abstraction type: dissertation user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2004' ...