[{"month":"08","status":"public","publication":"20th IAPR International Conference","date_updated":"2022-01-27T15:34:25Z","language":[{"iso":"eng"}],"extern":"1","intvolume":"     10502","alternative_title":["LNCS"],"date_published":"2017-08-22T00:00:00Z","type":"conference","volume":10502,"publisher":"Springer Nature","author":[{"full_name":"Dwivedi, Shivam","first_name":"Shivam","last_name":"Dwivedi"},{"last_name":"Gupta","first_name":"Aniket","full_name":"Gupta, Aniket"},{"first_name":"Siddhant","last_name":"Roy","full_name":"Roy, Siddhant"},{"first_name":"Ranita","last_name":"Biswas","orcid":"0000-0002-5372-7890","id":"3C2B033E-F248-11E8-B48F-1D18A9856A87","full_name":"Biswas, Ranita"},{"last_name":"Bhowmick","first_name":"Partha","full_name":"Bhowmick, Partha"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","conference":{"location":"Vienna, Austria","name":"DGCI: International Conference on Discrete Geometry for Computer Imagery","end_date":"2017-09-21","start_date":"2017-09-19"},"_id":"5801","date_created":"2019-01-08T20:42:22Z","year":"2017","place":"Cham","citation":{"ista":"Dwivedi S, Gupta A, Roy S, Biswas R, Bhowmick P. 2017. Fast and Efficient Incremental Algorithms for Circular and Spherical Propagation in Integer Space. 20th IAPR International Conference. DGCI: International Conference on Discrete Geometry for Computer Imagery, LNCS, vol. 10502, 347–359.","ieee":"S. Dwivedi, A. Gupta, S. Roy, R. Biswas, and P. Bhowmick, “Fast and Efficient Incremental Algorithms for Circular and Spherical Propagation in Integer Space,” in <i>20th IAPR International Conference</i>, Vienna, Austria, 2017, vol. 10502, pp. 347–359.","ama":"Dwivedi S, Gupta A, Roy S, Biswas R, Bhowmick P. Fast and Efficient Incremental Algorithms for Circular and Spherical Propagation in Integer Space. In: <i>20th IAPR International Conference</i>. Vol 10502. Cham: Springer Nature; 2017:347-359. doi:<a href=\"https://doi.org/10.1007/978-3-319-66272-5_28\">10.1007/978-3-319-66272-5_28</a>","mla":"Dwivedi, Shivam, et al. “Fast and Efficient Incremental Algorithms for Circular and Spherical Propagation in Integer Space.” <i>20th IAPR International Conference</i>, vol. 10502, Springer Nature, 2017, pp. 347–59, doi:<a href=\"https://doi.org/10.1007/978-3-319-66272-5_28\">10.1007/978-3-319-66272-5_28</a>.","short":"S. Dwivedi, A. Gupta, S. Roy, R. Biswas, P. Bhowmick, in:, 20th IAPR International Conference, Springer Nature, Cham, 2017, pp. 347–359.","chicago":"Dwivedi, Shivam, Aniket Gupta, Siddhant Roy, Ranita Biswas, and Partha Bhowmick. “Fast and Efficient Incremental Algorithms for Circular and Spherical Propagation in Integer Space.” In <i>20th IAPR International Conference</i>, 10502:347–59. Cham: Springer Nature, 2017. <a href=\"https://doi.org/10.1007/978-3-319-66272-5_28\">https://doi.org/10.1007/978-3-319-66272-5_28</a>.","apa":"Dwivedi, S., Gupta, A., Roy, S., Biswas, R., &#38; Bhowmick, P. (2017). Fast and Efficient Incremental Algorithms for Circular and Spherical Propagation in Integer Space. In <i>20th IAPR International Conference</i> (Vol. 10502, pp. 347–359). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-319-66272-5_28\">https://doi.org/10.1007/978-3-319-66272-5_28</a>"},"abstract":[{"text":"Space filling circles and spheres have various applications in mathematical imaging and physical modeling. In this paper, we first show how the thinnest (i.e., 2-minimal) model of digital sphere can be augmented to a space filling model by fixing certain “simple voxels” and “filler voxels” associated with it. Based on elementary number-theoretic properties of such voxels, we design an efficient incremental algorithm for generation of these space filling spheres with successively increasing radius. The novelty of the proposed technique is established further through circular space filling on 3D digital plane. As evident from a preliminary set of experimental result, this can particularly be useful for parallel computing of 3D Voronoi diagrams in the digital space.","lang":"eng"}],"title":"Fast and Efficient Incremental Algorithms for Circular and Spherical Propagation in Integer Space","publication_status":"published","quality_controlled":"1","article_processing_charge":"No","oa_version":"None","doi":"10.1007/978-3-319-66272-5_28","page":"347-359","publication_identifier":{"eisbn":["978-3-319-66272-5"],"isbn":["978-3-319-66271-8"],"eissn":["1611-3349"],"issn":["0302-9743"]},"day":"22"},{"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","publisher":"Springer Nature","author":[{"last_name":"Andres","first_name":"Eric","full_name":"Andres, Eric"},{"first_name":"Ranita","last_name":"Biswas","orcid":"0000-0002-5372-7890","id":"3C2B033E-F248-11E8-B48F-1D18A9856A87","full_name":"Biswas, Ranita"},{"last_name":"Bhowmick","first_name":"Partha","full_name":"Bhowmick, Partha"}],"volume":10502,"date_published":"2017-08-22T00:00:00Z","type":"conference","extern":"1","intvolume":"     10502","alternative_title":["LNCS"],"language":[{"iso":"eng"}],"publication":"20th IAPR International Conference","status":"public","date_updated":"2022-01-27T15:38:35Z","month":"08","day":"22","publication_identifier":{"eissn":["1611-3349"],"eisbn":["978-3-319-66272-5"],"isbn":["978-3-319-66271-8"],"issn":["0302-9743"]},"page":"388-398","doi":"10.1007/978-3-319-66272-5_31","oa_version":"None","article_processing_charge":"No","title":"Digital primitives defined by weighted focal set","quality_controlled":"1","publication_status":"published","abstract":[{"lang":"eng","text":"This papers introduces a definition of digital primitives based on focal points and weighted distances (with positive weights). The proposed definition is applicable to general dimensions and covers in its gamut various regular curves and surfaces like circles, ellipses, digital spheres and hyperspheres, ellipsoids and k-ellipsoids, Cartesian k-ovals, etc. Several interesting properties are presented for this class of digital primitives such as space partitioning, topological separation, and connectivity properties. To demonstrate further the potential of this new way of defining digital primitives, we propose, as extension, another class of digital conics defined by focus-directrix combination."}],"place":"Cham","year":"2017","citation":{"mla":"Andres, Eric, et al. “Digital Primitives Defined by Weighted Focal Set.” <i>20th IAPR International Conference</i>, vol. 10502, Springer Nature, 2017, pp. 388–98, doi:<a href=\"https://doi.org/10.1007/978-3-319-66272-5_31\">10.1007/978-3-319-66272-5_31</a>.","apa":"Andres, E., Biswas, R., &#38; Bhowmick, P. (2017). Digital primitives defined by weighted focal set. In <i>20th IAPR International Conference</i> (Vol. 10502, pp. 388–398). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-319-66272-5_31\">https://doi.org/10.1007/978-3-319-66272-5_31</a>","short":"E. Andres, R. Biswas, P. Bhowmick, in:, 20th IAPR International Conference, Springer Nature, Cham, 2017, pp. 388–398.","chicago":"Andres, Eric, Ranita Biswas, and Partha Bhowmick. “Digital Primitives Defined by Weighted Focal Set.” In <i>20th IAPR International Conference</i>, 10502:388–98. Cham: Springer Nature, 2017. <a href=\"https://doi.org/10.1007/978-3-319-66272-5_31\">https://doi.org/10.1007/978-3-319-66272-5_31</a>.","ama":"Andres E, Biswas R, Bhowmick P. Digital primitives defined by weighted focal set. In: <i>20th IAPR International Conference</i>. Vol 10502. Cham: Springer Nature; 2017:388-398. doi:<a href=\"https://doi.org/10.1007/978-3-319-66272-5_31\">10.1007/978-3-319-66272-5_31</a>","ista":"Andres E, Biswas R, Bhowmick P. 2017. Digital primitives defined by weighted focal set. 20th IAPR International Conference. DGCI: International Conference on Discrete Geometry for Computer Imagery, LNCS, vol. 10502, 388–398.","ieee":"E. Andres, R. Biswas, and P. Bhowmick, “Digital primitives defined by weighted focal set,” in <i>20th IAPR International Conference</i>, Vienna, Austria, 2017, vol. 10502, pp. 388–398."},"_id":"5802","date_created":"2019-01-08T20:42:39Z","conference":{"end_date":"2017-09-21","name":"DGCI: International Conference on Discrete Geometry for Computer Imagery","location":"Vienna, Austria","start_date":"2017-09-19"}},{"intvolume":"      9667","department":[{"_id":"HeEd"}],"publication":"Computational Topology in Image Context","date_updated":"2022-01-28T08:01:22Z","author":[{"full_name":"Sen, Nabhasmita","first_name":"Nabhasmita","last_name":"Sen"},{"id":"3C2B033E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-5372-7890","full_name":"Biswas, Ranita","first_name":"Ranita","last_name":"Biswas"},{"last_name":"Bhowmick","first_name":"Partha","full_name":"Bhowmick, Partha"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","volume":9667,"year":"2016","place":"Cham","citation":{"ama":"Sen N, Biswas R, Bhowmick P. On some local topological properties of naive discrete sphere. In: <i>Computational Topology in Image Context</i>. Vol 9667. Cham: Springer Nature; 2016:253-264. doi:<a href=\"https://doi.org/10.1007/978-3-319-39441-1_23\">10.1007/978-3-319-39441-1_23</a>","ista":"Sen N, Biswas R, Bhowmick P. 2016.On some local topological properties of naive discrete sphere. In: Computational Topology in Image Context. LNCS, vol. 9667, 253–264.","ieee":"N. Sen, R. Biswas, and P. Bhowmick, “On some local topological properties of naive discrete sphere,” in <i>Computational Topology in Image Context</i>, vol. 9667, Cham: Springer Nature, 2016, pp. 253–264.","mla":"Sen, Nabhasmita, et al. “On Some Local Topological Properties of Naive Discrete Sphere.” <i>Computational Topology in Image Context</i>, vol. 9667, Springer Nature, 2016, pp. 253–64, doi:<a href=\"https://doi.org/10.1007/978-3-319-39441-1_23\">10.1007/978-3-319-39441-1_23</a>.","short":"N. Sen, R. Biswas, P. Bhowmick, in:, Computational Topology in Image Context, Springer Nature, Cham, 2016, pp. 253–264.","apa":"Sen, N., Biswas, R., &#38; Bhowmick, P. (2016). On some local topological properties of naive discrete sphere. In <i>Computational Topology in Image Context</i> (Vol. 9667, pp. 253–264). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-319-39441-1_23\">https://doi.org/10.1007/978-3-319-39441-1_23</a>","chicago":"Sen, Nabhasmita, Ranita Biswas, and Partha Bhowmick. “On Some Local Topological Properties of Naive Discrete Sphere.” In <i>Computational Topology in Image Context</i>, 9667:253–64. Cham: Springer Nature, 2016. <a href=\"https://doi.org/10.1007/978-3-319-39441-1_23\">https://doi.org/10.1007/978-3-319-39441-1_23</a>."},"abstract":[{"text":"Discretization of sphere in the integer space follows a particular discretization scheme, which, in principle, conforms to some topological model. This eventually gives rise to interesting topological properties of a discrete spherical surface, which need to be investigated for its analytical characterization. This paper presents some novel results on the local topological properties of the naive model of discrete sphere. They follow from the bijection of each quadraginta octant of naive sphere with its projection map called f -map on the corresponding functional plane and from the characterization of certain jumps in the f-map. As an application, we have shown how these properties can be used in designing an efficient reconstruction algorithm for a naive spherical surface from an input voxel set when it is sparse or noisy.","lang":"eng"}],"conference":{"end_date":"2016-06-17","name":"CTIC: Computational Topology in Image Context","location":"Marseille, France","start_date":"2016-06-15"},"_id":"5805","date_created":"2019-01-08T20:44:24Z","doi":"10.1007/978-3-319-39441-1_23","publication_identifier":{"isbn":["978-3-319-39440-4"],"eisbn":["978-3-319-39441-1"],"eissn":["1611-3349"],"issn":["0302-9743"]},"publication_status":"published","title":"On some local topological properties of naive discrete sphere","article_processing_charge":"No","oa_version":"None","language":[{"iso":"eng"}],"extern":"1","alternative_title":["LNCS"],"month":"06","status":"public","publisher":"Springer Nature","date_published":"2016-06-02T00:00:00Z","type":"book_chapter","page":"253-264","day":"02","quality_controlled":"1"},{"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","publisher":"Springer Nature","author":[{"full_name":"Biswas, Ranita","orcid":"0000-0002-5372-7890","id":"3C2B033E-F248-11E8-B48F-1D18A9856A87","last_name":"Biswas","first_name":"Ranita"},{"full_name":"Bhowmick, Partha","first_name":"Partha","last_name":"Bhowmick"},{"last_name":"Brimkov","first_name":"Valentin E.","full_name":"Brimkov, Valentin E."}],"volume":9448,"date_published":"2016-01-06T00:00:00Z","type":"book_chapter","extern":"1","intvolume":"      9448","language":[{"iso":"eng"}],"status":"public","publication":"Combinatorial image analysis","date_updated":"2022-01-28T08:13:03Z","month":"01","department":[{"_id":"HeEd"}],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["978-3-319-26145-4"],"isbn":["978-3-319-26144-7"]},"day":"06","page":"86-100","doi":"10.1007/978-3-319-26145-4_7","article_processing_charge":"No","oa_version":"None","publication_status":"published","quality_controlled":"1","title":"On the connectivity and smoothness of discrete spherical circles","abstract":[{"lang":"eng","text":"A discrete spherical circle is a topologically well-connected 3D circle in the integer space, which belongs to a discrete sphere as well as a discrete plane. It is one of the most important 3D geometric primitives, but has not possibly yet been studied up to its merit. This paper is a maiden exposition of some of its elementary properties, which indicates a sense of its profound theoretical prospects in the framework of digital geometry. We have shown how different types of discretization can lead to forbidden and admissible classes, when one attempts to define the discretization of a spherical circle in terms of intersection between a discrete sphere and a discrete plane. Several fundamental theoretical results have been presented, the algorithm for construction of discrete spherical circles has been discussed, and some test results have been furnished to demonstrate its practicality and usefulness."}],"place":"Cham","year":"2016","citation":{"ista":"Biswas R, Bhowmick P, Brimkov VE. 2016.On the connectivity and smoothness of discrete spherical circles. In: Combinatorial image analysis. vol. 9448, 86–100.","ieee":"R. Biswas, P. Bhowmick, and V. E. Brimkov, “On the connectivity and smoothness of discrete spherical circles,” in <i>Combinatorial image analysis</i>, vol. 9448, Cham: Springer Nature, 2016, pp. 86–100.","ama":"Biswas R, Bhowmick P, Brimkov VE. On the connectivity and smoothness of discrete spherical circles. In: <i>Combinatorial Image Analysis</i>. Vol 9448. Cham: Springer Nature; 2016:86-100. doi:<a href=\"https://doi.org/10.1007/978-3-319-26145-4_7\">10.1007/978-3-319-26145-4_7</a>","mla":"Biswas, Ranita, et al. “On the Connectivity and Smoothness of Discrete Spherical Circles.” <i>Combinatorial Image Analysis</i>, vol. 9448, Springer Nature, 2016, pp. 86–100, doi:<a href=\"https://doi.org/10.1007/978-3-319-26145-4_7\">10.1007/978-3-319-26145-4_7</a>.","short":"R. Biswas, P. Bhowmick, V.E. Brimkov, in:, Combinatorial Image Analysis, Springer Nature, Cham, 2016, pp. 86–100.","chicago":"Biswas, Ranita, Partha Bhowmick, and Valentin E. Brimkov. “On the Connectivity and Smoothness of Discrete Spherical Circles.” In <i>Combinatorial Image Analysis</i>, 9448:86–100. Cham: Springer Nature, 2016. <a href=\"https://doi.org/10.1007/978-3-319-26145-4_7\">https://doi.org/10.1007/978-3-319-26145-4_7</a>.","apa":"Biswas, R., Bhowmick, P., &#38; Brimkov, V. E. (2016). On the connectivity and smoothness of discrete spherical circles. In <i>Combinatorial image analysis</i> (Vol. 9448, pp. 86–100). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-319-26145-4_7\">https://doi.org/10.1007/978-3-319-26145-4_7</a>"},"_id":"5809","date_created":"2019-01-08T20:45:19Z","conference":{"location":"Kolkata, India","name":"IWCIA: International Workshop on Combinatorial Image Analysis","end_date":"2015-11-27","start_date":"2015-11-24"}},{"publisher":"Springer","date_published":"2016-08-12T00:00:00Z","type":"book_chapter","alternative_title":["Methods in Molecular Biology"],"language":[{"iso":"eng"}],"status":"public","publist_id":"6281","month":"08","day":"12","page":"203 - 216","quality_controlled":"1","project":[{"_id":"25CD3DD2-B435-11E9-9278-68D0E5697425","name":"Localization of ion channels and receptors by two and three-dimensional immunoelectron microscopic approaches","call_identifier":"FP7","grant_number":"604102"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"orcid":"0000-0001-7429-7896","id":"2E55CDF2-F248-11E8-B48F-1D18A9856A87","full_name":"Harada, Harumi","first_name":"Harumi","last_name":"Harada"},{"last_name":"Shigemoto","first_name":"Ryuichi","full_name":"Shigemoto, Ryuichi","orcid":"0000-0001-8761-9444","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87"}],"volume":1474,"acknowledged_ssus":[{"_id":"EM-Fac"}],"intvolume":"      1474","publication":"High-Resolution Imaging of Cellular Proteins","ec_funded":1,"date_updated":"2023-09-05T14:09:01Z","department":[{"_id":"RySh"}],"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"]},"acknowledgement":"We thank Prof. Elek Molnár for providing us a pan-AMPAR anti-body used in Fig.2 and Dr. Ludek Lovicar for technical assistance in scanning electron microscope imaging. This work was supported by the European Union (HBP—Project Ref. 604102). ","doi":"10.1007/978-1-4939-6352-2_12","article_processing_charge":"No","oa_version":"None","publication_status":"published","title":"Immunogold protein localization on grid-glued freeze-fracture replicas","abstract":[{"lang":"eng","text":"Immunogold labeling of freeze-fracture replicas has recently been used for high-resolution visualization of protein localization in electron microscopy. This method has higher labeling efficiency than conventional immunogold methods for membrane molecules allowing precise quantitative measurements. However, one of the limitations of freeze-fracture replica immunolabeling is difficulty in keeping structural orientation and identifying labeled profiles in complex tissues like brain. The difficulty is partly due to fragmentation of freeze-fracture replica preparations during labeling procedures and limited morphological clues on the replica surface. To overcome these issues, we introduce here a grid-glued replica method combined with SEM observation. This method allows histological staining before dissolving the tissue and easy handling of replicas during immunogold labeling, and keeps the whole replica surface intact without fragmentation. The procedure described here is also useful for matched double-replica analysis allowing further identification of labeled profiles in corresponding P-face and E-face."}],"year":"2016","citation":{"mla":"Harada, Harumi, and Ryuichi Shigemoto. “Immunogold Protein Localization on Grid-Glued Freeze-Fracture Replicas.” <i>High-Resolution Imaging of Cellular Proteins</i>, vol. 1474, Springer, 2016, pp. 203–16, doi:<a href=\"https://doi.org/10.1007/978-1-4939-6352-2_12\">10.1007/978-1-4939-6352-2_12</a>.","chicago":"Harada, Harumi, and Ryuichi Shigemoto. “Immunogold Protein Localization on Grid-Glued Freeze-Fracture Replicas.” In <i>High-Resolution Imaging of Cellular Proteins</i>, 1474:203–16. Springer, 2016. <a href=\"https://doi.org/10.1007/978-1-4939-6352-2_12\">https://doi.org/10.1007/978-1-4939-6352-2_12</a>.","short":"H. Harada, R. Shigemoto, in:, High-Resolution Imaging of Cellular Proteins, Springer, 2016, pp. 203–216.","apa":"Harada, H., &#38; Shigemoto, R. (2016). Immunogold protein localization on grid-glued freeze-fracture replicas. In <i>High-Resolution Imaging of Cellular Proteins</i> (Vol. 1474, pp. 203–216). Springer. <a href=\"https://doi.org/10.1007/978-1-4939-6352-2_12\">https://doi.org/10.1007/978-1-4939-6352-2_12</a>","ista":"Harada H, Shigemoto R. 2016.Immunogold protein localization on grid-glued freeze-fracture replicas. In: High-Resolution Imaging of Cellular Proteins. Methods in Molecular Biology, vol. 1474, 203–216.","ieee":"H. Harada and R. Shigemoto, “Immunogold protein localization on grid-glued freeze-fracture replicas,” in <i>High-Resolution Imaging of Cellular Proteins</i>, vol. 1474, Springer, 2016, pp. 203–216.","ama":"Harada H, Shigemoto R. Immunogold protein localization on grid-glued freeze-fracture replicas. In: <i>High-Resolution Imaging of Cellular Proteins</i>. Vol 1474. Springer; 2016:203-216. doi:<a href=\"https://doi.org/10.1007/978-1-4939-6352-2_12\">10.1007/978-1-4939-6352-2_12</a>"},"_id":"1094","date_created":"2018-12-11T11:50:06Z"},{"conference":{"start_date":"2014-01-19","name":"VMCAI: Verifcation, Model Checking, and Abstract Interpretation","location":"San Diego, CA, United States","end_date":"2014-01-21"},"date_created":"2022-03-18T13:01:22Z","_id":"10884","citation":{"ama":"Aminof B, Jacobs S, Khalimov A, Rubin S. Parameterized model checking of token-passing systems. In: <i>Verification, Model Checking, and Abstract Interpretation</i>. Vol 8318. Springer Nature; 2014:262-281. doi:<a href=\"https://doi.org/10.1007/978-3-642-54013-4_15\">10.1007/978-3-642-54013-4_15</a>","ista":"Aminof B, Jacobs S, Khalimov A, Rubin S. 2014. Parameterized model checking of token-passing systems. Verification, Model Checking, and Abstract Interpretation. VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 8318, 262–281.","ieee":"B. Aminof, S. Jacobs, A. Khalimov, and S. Rubin, “Parameterized model checking of token-passing systems,” in <i>Verification, Model Checking, and Abstract Interpretation</i>, San Diego, CA, United States, 2014, vol. 8318, pp. 262–281.","mla":"Aminof, Benjamin, et al. “Parameterized Model Checking of Token-Passing Systems.” <i>Verification, Model Checking, and Abstract Interpretation</i>, vol. 8318, Springer Nature, 2014, pp. 262–81, doi:<a href=\"https://doi.org/10.1007/978-3-642-54013-4_15\">10.1007/978-3-642-54013-4_15</a>.","short":"B. Aminof, S. Jacobs, A. Khalimov, S. Rubin, in:, Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2014, pp. 262–281.","chicago":"Aminof, Benjamin, Swen Jacobs, Ayrat Khalimov, and Sasha Rubin. “Parameterized Model Checking of Token-Passing Systems.” In <i>Verification, Model Checking, and Abstract Interpretation</i>, 8318:262–81. Springer Nature, 2014. <a href=\"https://doi.org/10.1007/978-3-642-54013-4_15\">https://doi.org/10.1007/978-3-642-54013-4_15</a>.","apa":"Aminof, B., Jacobs, S., Khalimov, A., &#38; Rubin, S. (2014). Parameterized model checking of token-passing systems. In <i>Verification, Model Checking, and Abstract Interpretation</i> (Vol. 8318, pp. 262–281). San Diego, CA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-54013-4_15\">https://doi.org/10.1007/978-3-642-54013-4_15</a>"},"year":"2014","abstract":[{"lang":"eng","text":"We revisit the parameterized model checking problem for token-passing systems and specifications in indexed CTL  ∗ \\X. Emerson and Namjoshi (1995, 2003) have shown that parameterized model checking of indexed CTL  ∗ \\X in uni-directional token rings can be reduced to checking rings up to some cutoff size. Clarke et al. (2004) have shown a similar result for general topologies and indexed LTL \\X, provided processes cannot choose the directions for sending or receiving the token.\r\nWe unify and substantially extend these results by systematically exploring fragments of indexed CTL  ∗ \\X with respect to general topologies. For each fragment we establish whether a cutoff exists, and for some concrete topologies, such as rings, cliques and stars, we infer small cutoffs. Finally, we show that the problem becomes undecidable, and thus no cutoffs exist, if processes are allowed to choose the directions in which they send or from which they receive the token."}],"title":"Parameterized model checking of token-passing systems","publication_status":"published","oa_version":"Preprint","article_processing_charge":"No","scopus_import":"1","doi":"10.1007/978-3-642-54013-4_15","main_file_link":[{"open_access":"1","url":" https://doi.org/10.48550/arXiv.1311.4425"}],"publication_identifier":{"eisbn":["9783642540134"],"isbn":["9783642540127"],"eissn":["1611-3349"],"issn":["0302-9743"]},"acknowledgement":"This work was supported by the Austrian Science Fund through grant P23499-N23\r\nand through the RiSE network (S11403, S11405, S11406, S11407-N23); ERC Starting Grant (279307: Graph Games); Vienna Science and Technology Fund (WWTF)\r\ngrants PROSEED, ICT12-059, and VRG11-005.","department":[{"_id":"KrCh"}],"date_updated":"2022-05-17T08:36:01Z","ec_funded":1,"publication":"Verification, Model Checking, and Abstract Interpretation","arxiv":1,"intvolume":"      8318","volume":8318,"oa":1,"author":[{"id":"4A55BD00-F248-11E8-B48F-1D18A9856A87","full_name":"Aminof, Benjamin","first_name":"Benjamin","last_name":"Aminof"},{"first_name":"Swen","last_name":"Jacobs","full_name":"Jacobs, Swen"},{"full_name":"Khalimov, Ayrat","first_name":"Ayrat","last_name":"Khalimov"},{"first_name":"Sasha","last_name":"Rubin","id":"2EC51194-F248-11E8-B48F-1D18A9856A87","full_name":"Rubin, Sasha"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307"}],"quality_controlled":"1","page":"262-281","day":"30","month":"01","status":"public","language":[{"iso":"eng"}],"alternative_title":["LNCS"],"type":"conference","external_id":{"arxiv":["1311.4425"]},"date_published":"2014-01-30T00:00:00Z","publisher":"Springer Nature"},{"doi":"10.1007/978-3-642-54013-4_5","scopus_import":"1","acknowledgement":" Supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No\r\nS11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783642540134"],"isbn":["9783642540127"]},"publication_status":"published","title":"Doomsday equilibria for omega-regular games","article_processing_charge":"No","oa_version":"Preprint","year":"2014","citation":{"mla":"Chatterjee, Krishnendu, et al. “Doomsday Equilibria for Omega-Regular Games.” <i>VMCAI 2014: Verification, Model Checking, and Abstract Interpretation</i>, vol. 8318, Springer Nature, 2014, pp. 78–97, doi:<a href=\"https://doi.org/10.1007/978-3-642-54013-4_5\">10.1007/978-3-642-54013-4_5</a>.","short":"K. Chatterjee, L. Doyen, E. Filiot, J.-F. Raskin, in:, VMCAI 2014: Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2014, pp. 78–97.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Emmanuel Filiot, and Jean-François Raskin. “Doomsday Equilibria for Omega-Regular Games.” In <i>VMCAI 2014: Verification, Model Checking, and Abstract Interpretation</i>, 8318:78–97. Springer Nature, 2014. <a href=\"https://doi.org/10.1007/978-3-642-54013-4_5\">https://doi.org/10.1007/978-3-642-54013-4_5</a>.","apa":"Chatterjee, K., Doyen, L., Filiot, E., &#38; Raskin, J.-F. (2014). Doomsday equilibria for omega-regular games. In <i>VMCAI 2014: Verification, Model Checking, and Abstract Interpretation</i> (Vol. 8318, pp. 78–97). San Diego, CA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-54013-4_5\">https://doi.org/10.1007/978-3-642-54013-4_5</a>","ista":"Chatterjee K, Doyen L, Filiot E, Raskin J-F. 2014. Doomsday equilibria for omega-regular games. VMCAI 2014: Verification, Model Checking, and Abstract Interpretation. VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 8318, 78–97.","ieee":"K. Chatterjee, L. Doyen, E. Filiot, and J.-F. Raskin, “Doomsday equilibria for omega-regular games,” in <i>VMCAI 2014: Verification, Model Checking, and Abstract Interpretation</i>, San Diego, CA, United States, 2014, vol. 8318, pp. 78–97.","ama":"Chatterjee K, Doyen L, Filiot E, Raskin J-F. Doomsday equilibria for omega-regular games. In: <i>VMCAI 2014: Verification, Model Checking, and Abstract Interpretation</i>. Vol 8318. Springer Nature; 2014:78-97. doi:<a href=\"https://doi.org/10.1007/978-3-642-54013-4_5\">10.1007/978-3-642-54013-4_5</a>"},"abstract":[{"text":"Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information games.\r\nIn this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile such that all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players objective, then the objective of every player is violated.\r\nWe present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of ω-regular objectives, both for imperfect-information games, and for perfect-information games.We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect-information games.","lang":"eng"}],"conference":{"end_date":"2014-01-21","location":"San Diego, CA, United States","name":"VMCAI: Verifcation, Model Checking, and Abstract Interpretation","start_date":"2014-01-19"},"_id":"10885","date_created":"2022-03-18T13:03:15Z","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"last_name":"Filiot","first_name":"Emmanuel","full_name":"Filiot, Emmanuel"},{"full_name":"Raskin, Jean-François","last_name":"Raskin","first_name":"Jean-François"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"relation":"later_version","status":"public","id":"681"}]},"volume":8318,"arxiv":1,"intvolume":"      8318","department":[{"_id":"KrCh"}],"publication":"VMCAI 2014: Verification, Model Checking, and Abstract Interpretation","ec_funded":1,"date_updated":"2023-02-23T12:52:24Z","page":"78-97","day":"30","quality_controlled":"1","project":[{"call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407","call_identifier":"FWF"},{"grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"publisher":"Springer Nature","external_id":{"arxiv":["1311.3238"]},"date_published":"2014-01-30T00:00:00Z","type":"conference","language":[{"iso":"eng"}],"alternative_title":["LNCS"],"month":"01","status":"public"},{"page":"117-127","day":"08","quality_controlled":"1","publisher":"Springer Nature","date_published":"2014-11-08T00:00:00Z","type":"conference","language":[{"iso":"eng"}],"alternative_title":["LNCS"],"month":"11","status":"public","doi":"10.1007/978-3-319-13075-0_10","scopus_import":"1","publication_identifier":{"issn":["0302-9743"],"eisbn":["9783319130750"],"isbn":["9783319130743"],"eissn":["1611-3349"]},"acknowledgement":"T. Biedl was supported by NSERC and the Ross and Muriel Cheriton Fellowship. P. Palfrader was supported by Austrian Science Fund (FWF): P25816-N15.","title":"Planar matchings for weighted straight skeletons","publication_status":"published","oa_version":"None","article_processing_charge":"No","year":"2014","citation":{"mla":"Biedl, Therese, et al. “Planar Matchings for Weighted Straight Skeletons.” <i>25th International Symposium, ISAAC 2014</i>, vol. 8889, Springer Nature, 2014, pp. 117–27, doi:<a href=\"https://doi.org/10.1007/978-3-319-13075-0_10\">10.1007/978-3-319-13075-0_10</a>.","short":"T. Biedl, S. Huber, P. Palfrader, in:, 25th International Symposium, ISAAC 2014, Springer Nature, 2014, pp. 117–127.","chicago":"Biedl, Therese, Stefan Huber, and Peter Palfrader. “Planar Matchings for Weighted Straight Skeletons.” In <i>25th International Symposium, ISAAC 2014</i>, 8889:117–27. Springer Nature, 2014. <a href=\"https://doi.org/10.1007/978-3-319-13075-0_10\">https://doi.org/10.1007/978-3-319-13075-0_10</a>.","apa":"Biedl, T., Huber, S., &#38; Palfrader, P. (2014). Planar matchings for weighted straight skeletons. In <i>25th International Symposium, ISAAC 2014</i> (Vol. 8889, pp. 117–127). Jeonju, Korea: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-319-13075-0_10\">https://doi.org/10.1007/978-3-319-13075-0_10</a>","ama":"Biedl T, Huber S, Palfrader P. Planar matchings for weighted straight skeletons. In: <i>25th International Symposium, ISAAC 2014</i>. Vol 8889. Springer Nature; 2014:117-127. doi:<a href=\"https://doi.org/10.1007/978-3-319-13075-0_10\">10.1007/978-3-319-13075-0_10</a>","ista":"Biedl T, Huber S, Palfrader P. 2014. Planar matchings for weighted straight skeletons. 25th International Symposium, ISAAC 2014. ISAAC: International Symposium on Algorithms and Computation, LNCS, vol. 8889, 117–127.","ieee":"T. Biedl, S. Huber, and P. Palfrader, “Planar matchings for weighted straight skeletons,” in <i>25th International Symposium, ISAAC 2014</i>, Jeonju, Korea, 2014, vol. 8889, pp. 117–127."},"abstract":[{"text":"In this paper, we introduce planar matchings on directed pseudo-line arrangements, which yield a planar set of pseudo-line segments such that only matching-partners are adjacent. By translating the planar matching problem into a corresponding stable roommates problem we show that such matchings always exist.\r\nUsing our new framework, we establish, for the first time, a complete, rigorous definition of weighted straight skeletons, which are based on a so-called wavefront propagation process. We present a generalized and unified approach to treat structural changes in the wavefront that focuses on the restoration of weak planarity by finding planar matchings.","lang":"eng"}],"conference":{"location":"Jeonju, Korea","name":"ISAAC: International Symposium on Algorithms and Computation","end_date":"2014-12-17","start_date":"2014-12-15"},"_id":"10892","date_created":"2022-03-21T07:09:03Z","author":[{"full_name":"Biedl, Therese","last_name":"Biedl","first_name":"Therese"},{"first_name":"Stefan","last_name":"Huber","orcid":"0000-0002-8871-5814","id":"4700A070-F248-11E8-B48F-1D18A9856A87","full_name":"Huber, Stefan"},{"first_name":"Peter","last_name":"Palfrader","full_name":"Palfrader, Peter"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"id":"481","relation":"later_version","status":"public"}]},"volume":8889,"intvolume":"      8889","department":[{"_id":"HeEd"}],"publication":"25th International Symposium, ISAAC 2014","date_updated":"2023-02-23T12:20:55Z"},{"day":"01","page":"137-143","quality_controlled":"1","language":[{"iso":"eng"}],"status":"public","month":"09","publisher":"Springer Berlin Heidelberg","date_published":"2014-09-01T00:00:00Z","type":"conference","abstract":[{"text":"PHAT is a C++ library for the computation of persistent homology by matrix reduction. We aim for a simple generic design that decouples algorithms from data structures without sacrificing efficiency or user-friendliness. This makes PHAT a versatile platform for experimenting with algorithmic ideas and comparing them to state of the art implementations.","lang":"eng"}],"year":"2014","place":"Berlin, Heidelberg","citation":{"ieee":"U. Bauer, M. Kerber, J. Reininghaus, and H. Wagner, “PHAT – Persistent Homology Algorithms Toolbox,” in <i>ICMS 2014: International Congress on Mathematical Software</i>, Seoul, South Korea, 2014, vol. 8592, pp. 137–143.","ista":"Bauer U, Kerber M, Reininghaus J, Wagner H. 2014. PHAT – Persistent Homology Algorithms Toolbox. ICMS 2014: International Congress on Mathematical Software. ICMS: International Congress on Mathematical SoftwareLNCS vol. 8592, 137–143.","ama":"Bauer U, Kerber M, Reininghaus J, Wagner H. PHAT – Persistent Homology Algorithms Toolbox. In: <i>ICMS 2014: International Congress on Mathematical Software</i>. Vol 8592. LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg; 2014:137-143. doi:<a href=\"https://doi.org/10.1007/978-3-662-44199-2_24\">10.1007/978-3-662-44199-2_24</a>","apa":"Bauer, U., Kerber, M., Reininghaus, J., &#38; Wagner, H. (2014). PHAT – Persistent Homology Algorithms Toolbox. In <i>ICMS 2014: International Congress on Mathematical Software</i> (Vol. 8592, pp. 137–143). Berlin, Heidelberg: Springer Berlin Heidelberg. <a href=\"https://doi.org/10.1007/978-3-662-44199-2_24\">https://doi.org/10.1007/978-3-662-44199-2_24</a>","chicago":"Bauer, Ulrich, Michael Kerber, Jan Reininghaus, and Hubert Wagner. “PHAT – Persistent Homology Algorithms Toolbox.” In <i>ICMS 2014: International Congress on Mathematical Software</i>, 8592:137–43. LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg, 2014. <a href=\"https://doi.org/10.1007/978-3-662-44199-2_24\">https://doi.org/10.1007/978-3-662-44199-2_24</a>.","short":"U. Bauer, M. Kerber, J. Reininghaus, H. Wagner, in:, ICMS 2014: International Congress on Mathematical Software, Springer Berlin Heidelberg, Berlin, Heidelberg, 2014, pp. 137–143.","mla":"Bauer, Ulrich, et al. “PHAT – Persistent Homology Algorithms Toolbox.” <i>ICMS 2014: International Congress on Mathematical Software</i>, vol. 8592, Springer Berlin Heidelberg, 2014, pp. 137–43, doi:<a href=\"https://doi.org/10.1007/978-3-662-44199-2_24\">10.1007/978-3-662-44199-2_24</a>."},"_id":"10894","date_created":"2022-03-21T07:12:16Z","conference":{"start_date":"2014-08-05","location":"Seoul, South Korea","name":"ICMS: International Congress on Mathematical Software","end_date":"2014-08-09"},"publication_identifier":{"eisbn":["9783662441992"],"isbn":["9783662441985"],"eissn":["1611-3349"],"issn":["0302-9743"]},"doi":"10.1007/978-3-662-44199-2_24","scopus_import":"1","article_processing_charge":"No","oa_version":"None","publication_status":"published","title":"PHAT – Persistent Homology Algorithms Toolbox","intvolume":"      8592","publication":"ICMS 2014: International Congress on Mathematical Software","date_updated":"2023-09-20T09:42:40Z","department":[{"_id":"HeEd"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"id":"2ADD483A-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9683-0724","full_name":"Bauer, Ulrich","first_name":"Ulrich","last_name":"Bauer"},{"first_name":"Michael","last_name":"Kerber","full_name":"Kerber, Michael"},{"first_name":"Jan","last_name":"Reininghaus","id":"4505473A-F248-11E8-B48F-1D18A9856A87","full_name":"Reininghaus, Jan"},{"full_name":"Wagner, Hubert","first_name":"Hubert","last_name":"Wagner"}],"related_material":{"record":[{"id":"1433","relation":"later_version","status":"public"}]},"volume":8592,"series_title":"LNCS"},{"publication":"Computer Aided Verification","ec_funded":1,"date_updated":"2023-09-05T14:16:07Z","department":[{"_id":"ToHe"}],"intvolume":"      8044","oa":1,"volume":8044,"series_title":"CAV","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"first_name":"Cezara","last_name":"Dragoi","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","full_name":"Dragoi, Cezara"},{"last_name":"Gupta","first_name":"Ashutosh","full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"_id":"5747","date_created":"2018-12-18T13:10:21Z","file":[{"checksum":"a901cc6b71db08b61c0d4c0cbacc6287","file_id":"5748","creator":"dernst","content_type":"application/pdf","file_size":236480,"date_updated":"2020-07-14T12:47:10Z","date_created":"2018-12-18T13:13:33Z","relation":"main_file","file_name":"2013_CAV_Dragoi.pdf","access_level":"open_access"}],"conference":{"start_date":"2013-07-13","location":"Saint Petersburg, Russia","name":"CAV 2013","end_date":"2013-07-19"},"place":"Berlin, Heidelberg","year":"2013","citation":{"ieee":"C. Dragoi, A. Gupta, and T. A. Henzinger, “Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates,” in <i>Computer Aided Verification</i>, vol. 8044, Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 174–190.","ista":"Dragoi C, Gupta A, Henzinger TA. 2013.Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In: Computer Aided Verification. vol. 8044, 174–190.","ama":"Dragoi C, Gupta A, Henzinger TA. Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In: <i>Computer Aided Verification</i>. Vol 8044. CAV. Berlin, Heidelberg: Springer Berlin Heidelberg; 2013:174-190. doi:<a href=\"https://doi.org/10.1007/978-3-642-39799-8_11\">10.1007/978-3-642-39799-8_11</a>","mla":"Dragoi, Cezara, et al. “Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates.” <i>Computer Aided Verification</i>, vol. 8044, Springer Berlin Heidelberg, 2013, pp. 174–90, doi:<a href=\"https://doi.org/10.1007/978-3-642-39799-8_11\">10.1007/978-3-642-39799-8_11</a>.","short":"C. Dragoi, A. Gupta, T.A. Henzinger, in:, Computer Aided Verification, Springer Berlin Heidelberg, Berlin, Heidelberg, 2013, pp. 174–190.","chicago":"Dragoi, Cezara, Ashutosh Gupta, and Thomas A Henzinger. “Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates.” In <i>Computer Aided Verification</i>, 8044:174–90. CAV. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013. <a href=\"https://doi.org/10.1007/978-3-642-39799-8_11\">https://doi.org/10.1007/978-3-642-39799-8_11</a>.","apa":"Dragoi, C., Gupta, A., &#38; Henzinger, T. A. (2013). Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In <i>Computer Aided Verification</i> (Vol. 8044, pp. 174–190). Berlin, Heidelberg: Springer Berlin Heidelberg. <a href=\"https://doi.org/10.1007/978-3-642-39799-8_11\">https://doi.org/10.1007/978-3-642-39799-8_11</a>"},"file_date_updated":"2020-07-14T12:47:10Z","article_processing_charge":"No","oa_version":"None","title":"Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates","publication_status":"published","publication_identifier":{"issn":["0302-9743"],"isbn":["9783642397981","9783642397998"],"eissn":["1611-3349"]},"doi":"10.1007/978-3-642-39799-8_11","scopus_import":"1","status":"public","language":[{"iso":"eng"}],"ddc":["005"],"date_published":"2013-01-01T00:00:00Z","type":"book_chapter","publisher":"Springer Berlin Heidelberg","has_accepted_license":"1","project":[{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF"}],"pubrep_id":"195","quality_controlled":"1","page":"174-190"},{"article_processing_charge":"No","oa_version":"None","publication_status":"published","title":"Persistent homology in image processing","publication_identifier":{"issn":["0302-9743"],"eisbn":["9783642382215"],"isbn":["9783642382208"],"eissn":["1611-3349"]},"acknowledgement":"This research is partially supported by the European Science Foundation (ESF) under the Research Network Programme, the European Union under the Toposys Project FP7-ICT-318493-STREP, the Russian Government under the Mega Project 11.G34.31.0053.","scopus_import":"1","doi":"10.1007/978-3-642-38221-5_19","date_created":"2022-03-21T07:30:33Z","_id":"10897","conference":{"end_date":"2013-05-17","name":"GbRPR: Graph-based Representations in Pattern Recognition","location":"Vienna, Austria","start_date":"2013-05-15"},"abstract":[{"lang":"eng","text":"Taking images is an efficient way to collect data about the physical world. It can be done fast and in exquisite detail. By definition, image processing is the field that concerns itself with the computation aimed at harnessing the information contained in images [10]. This talk is concerned with topological information. Our main thesis is that persistent homology [5] is a useful method to quantify and summarize topological information, building a bridge that connects algebraic topology with applications. We provide supporting evidence for this thesis by touching upon four technical developments in the overlap between persistent homology and image processing."}],"citation":{"mla":"Edelsbrunner, Herbert. “Persistent Homology in Image Processing.” <i>Graph-Based Representations in Pattern Recognition</i>, vol. 7877, Springer Nature, 2013, pp. 182–83, doi:<a href=\"https://doi.org/10.1007/978-3-642-38221-5_19\">10.1007/978-3-642-38221-5_19</a>.","short":"H. Edelsbrunner, in:, Graph-Based Representations in Pattern Recognition, Springer Nature, Berlin, Heidelberg, 2013, pp. 182–183.","chicago":"Edelsbrunner, Herbert. “Persistent Homology in Image Processing.” In <i>Graph-Based Representations in Pattern Recognition</i>, 7877:182–83. LNCS. Berlin, Heidelberg: Springer Nature, 2013. <a href=\"https://doi.org/10.1007/978-3-642-38221-5_19\">https://doi.org/10.1007/978-3-642-38221-5_19</a>.","apa":"Edelsbrunner, H. (2013). Persistent homology in image processing. In <i>Graph-Based Representations in Pattern Recognition</i> (Vol. 7877, pp. 182–183). Berlin, Heidelberg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-38221-5_19\">https://doi.org/10.1007/978-3-642-38221-5_19</a>","ama":"Edelsbrunner H. Persistent homology in image processing. In: <i>Graph-Based Representations in Pattern Recognition</i>. Vol 7877. LNCS. Berlin, Heidelberg: Springer Nature; 2013:182-183. doi:<a href=\"https://doi.org/10.1007/978-3-642-38221-5_19\">10.1007/978-3-642-38221-5_19</a>","ista":"Edelsbrunner H. 2013. Persistent homology in image processing. Graph-Based Representations in Pattern Recognition. GbRPR: Graph-based Representations in Pattern RecognitionLNCS vol. 7877, 182–183.","ieee":"H. Edelsbrunner, “Persistent homology in image processing,” in <i>Graph-Based Representations in Pattern Recognition</i>, Vienna, Austria, 2013, vol. 7877, pp. 182–183."},"year":"2013","place":"Berlin, Heidelberg","volume":7877,"series_title":"LNCS","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"last_name":"Edelsbrunner","first_name":"Herbert","full_name":"Edelsbrunner, Herbert","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9823-6833"}],"date_updated":"2023-09-05T15:10:20Z","ec_funded":1,"publication":"Graph-Based Representations in Pattern Recognition","department":[{"_id":"HeEd"}],"intvolume":"      7877","quality_controlled":"1","day":"01","page":"182-183","project":[{"name":"Topological Complex Systems","_id":"255D761E-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"318493"}],"type":"conference","date_published":"2013-06-01T00:00:00Z","publisher":"Springer Nature","status":"public","month":"06","language":[{"iso":"eng"}]},{"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Chaubal, Siddhesh","first_name":"Siddhesh","last_name":"Chaubal"},{"first_name":"Sasha","last_name":"Rubin","id":"2EC51194-F248-11E8-B48F-1D18A9856A87","full_name":"Rubin, Sasha"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","series_title":"LNCS","volume":7810,"intvolume":"      7810","department":[{"_id":"KrCh"}],"date_updated":"2023-09-05T15:10:38Z","ec_funded":1,"publication":"7th International Conference on Language and Automata Theory and Applications","scopus_import":"1","doi":"10.1007/978-3-642-37064-9_20","acknowledgement":"The research was supported by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award. Thanks to Gabriele Puppis for suggesting the problem of identifying a deterministic transducer to compute the optimal cost, and to Martin Chmelik for his comments on the introduction.","publication_identifier":{"issn":["0302-9743"],"isbn":["9783642370632"],"eisbn":["9783642370649"],"eissn":["1611-3349"]},"publication_status":"published","title":"How to travel between languages","article_processing_charge":"No","oa_version":"None","citation":{"ama":"Chatterjee K, Chaubal S, Rubin S. How to travel between languages. In: <i>7th International Conference on Language and Automata Theory and Applications</i>. Vol 7810. LNCS. Berlin, Heidelberg: Springer Nature; 2013:214-225. doi:<a href=\"https://doi.org/10.1007/978-3-642-37064-9_20\">10.1007/978-3-642-37064-9_20</a>","ista":"Chatterjee K, Chaubal S, Rubin S. 2013. How to travel between languages. 7th International Conference on Language and Automata Theory and Applications. LATA: Conference on Language and Automata Theory and ApplicationsLNCS, LNCS, vol. 7810, 214–225.","ieee":"K. Chatterjee, S. Chaubal, and S. Rubin, “How to travel between languages,” in <i>7th International Conference on Language and Automata Theory and Applications</i>, Bilbao, Spain, 2013, vol. 7810, pp. 214–225.","mla":"Chatterjee, Krishnendu, et al. “How to Travel between Languages.” <i>7th International Conference on Language and Automata Theory and Applications</i>, vol. 7810, Springer Nature, 2013, pp. 214–25, doi:<a href=\"https://doi.org/10.1007/978-3-642-37064-9_20\">10.1007/978-3-642-37064-9_20</a>.","chicago":"Chatterjee, Krishnendu, Siddhesh Chaubal, and Sasha Rubin. “How to Travel between Languages.” In <i>7th International Conference on Language and Automata Theory and Applications</i>, 7810:214–25. LNCS. Berlin, Heidelberg: Springer Nature, 2013. <a href=\"https://doi.org/10.1007/978-3-642-37064-9_20\">https://doi.org/10.1007/978-3-642-37064-9_20</a>.","apa":"Chatterjee, K., Chaubal, S., &#38; Rubin, S. (2013). How to travel between languages. In <i>7th International Conference on Language and Automata Theory and Applications</i> (Vol. 7810, pp. 214–225). Berlin, Heidelberg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-37064-9_20\">https://doi.org/10.1007/978-3-642-37064-9_20</a>","short":"K. Chatterjee, S. Chaubal, S. Rubin, in:, 7th International Conference on Language and Automata Theory and Applications, Springer Nature, Berlin, Heidelberg, 2013, pp. 214–225."},"year":"2013","place":"Berlin, Heidelberg","abstract":[{"lang":"eng","text":"We consider how to edit strings from a source language so that the edited strings belong to a target language, where the languages are given as deterministic finite automata. Non-streaming (or offline) transducers perform edits given the whole source string. We show that the class of deterministic one-pass transducers with registers along with increment and min operation suffices for computing optimal edit distance, whereas the same class of transducers without the min operation is not sufficient. Streaming (or online) transducers perform edits as the letters of the source string are received. We present a polynomial time algorithm for the partial-repair problem that given a bound α asks for the construction of a deterministic streaming transducer (if one exists) that ensures that the ‘maximum fraction’ η of the strings of the source language are edited, within cost α, to the target language."}],"conference":{"name":"LATA: Conference on Language and Automata Theory and Applications","location":"Bilbao, Spain","end_date":"2013-04-05","start_date":"2013-04-02"},"date_created":"2022-03-21T07:56:21Z","_id":"10902","publisher":"Springer Nature","type":"conference","date_published":"2013-04-15T00:00:00Z","language":[{"iso":"eng"}],"alternative_title":["LNCS"],"month":"04","status":"public","page":"214-225","day":"15","quality_controlled":"1","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}]},{"date_published":"2012-01-01T00:00:00Z","type":"book_chapter","publisher":"Springer Berlin Heidelberg","status":"public","language":[{"iso":"eng"}],"ddc":["005"],"quality_controlled":"1","page":"107-121","has_accepted_license":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989"}],"pubrep_id":"180","series_title":"LNCS","oa":1,"volume":7561,"author":[{"last_name":"Gupta","first_name":"Ashutosh","full_name":"Gupta, Ashutosh"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","department":[{"_id":"ToHe"}],"publication":"Automated Technology for Verification and Analysis","ec_funded":1,"date_updated":"2023-09-05T14:15:29Z","intvolume":"      7561","title":"Improved Single Pass Algorithms for Resolution Proof Reduction","publication_status":"published","file_date_updated":"2020-07-14T12:47:10Z","article_processing_charge":"No","oa_version":"None","doi":"10.1007/978-3-642-33386-6_10","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783642333859","9783642333866"]},"conference":{"end_date":"2012-10-06","name":"ATVA 2012","location":"Thiruvananthapuram, Kerala, India","start_date":"2012-10-03"},"_id":"5745","file":[{"file_size":465502,"date_updated":"2020-07-14T12:47:10Z","date_created":"2018-12-18T13:07:35Z","relation":"main_file","access_level":"open_access","file_name":"2012_ATVA_Gupta.pdf","checksum":"68415837a315de3cc4d120f6019d752c","content_type":"application/pdf","creator":"dernst","file_id":"5746"}],"date_created":"2018-12-18T13:01:46Z","year":"2012","place":"Berlin, Heidelberg","citation":{"ama":"Gupta A. Improved Single Pass Algorithms for Resolution Proof Reduction. In: <i>Automated Technology for Verification and Analysis</i>. Vol 7561. LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg; 2012:107-121. doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">10.1007/978-3-642-33386-6_10</a>","ista":"Gupta A. 2012.Improved Single Pass Algorithms for Resolution Proof Reduction. In: Automated Technology for Verification and Analysis. vol. 7561, 107–121.","ieee":"A. Gupta, “Improved Single Pass Algorithms for Resolution Proof Reduction,” in <i>Automated Technology for Verification and Analysis</i>, vol. 7561, Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 107–121.","mla":"Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” <i>Automated Technology for Verification and Analysis</i>, vol. 7561, Springer Berlin Heidelberg, 2012, pp. 107–21, doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">10.1007/978-3-642-33386-6_10</a>.","short":"A. Gupta, in:, Automated Technology for Verification and Analysis, Springer Berlin Heidelberg, Berlin, Heidelberg, 2012, pp. 107–121.","chicago":"Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” In <i>Automated Technology for Verification and Analysis</i>, 7561:107–21. LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">https://doi.org/10.1007/978-3-642-33386-6_10</a>.","apa":"Gupta, A. (2012). Improved Single Pass Algorithms for Resolution Proof Reduction. In <i>Automated Technology for Verification and Analysis</i> (Vol. 7561, pp. 107–121). Berlin, Heidelberg: Springer Berlin Heidelberg. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">https://doi.org/10.1007/978-3-642-33386-6_10</a>"}},{"intvolume":"      7561","department":[{"_id":"ToHe"}],"publication":"Automated Technology for Verification and Analysis","date_updated":"2023-09-05T14:07:24Z","author":[{"full_name":"Bouajjani, Ahmed","first_name":"Ahmed","last_name":"Bouajjani"},{"last_name":"Dragoi","first_name":"Cezara","full_name":"Dragoi, Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Constantin","last_name":"Enea","full_name":"Enea, Constantin"},{"last_name":"Sighireanu","first_name":"Mihaela","full_name":"Sighireanu, Mihaela"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","series_title":"LNCS","volume":7561,"place":"Berlin, Heidelberg","year":"2012","citation":{"short":"A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Automated Technology for Verification and Analysis, Springer, Berlin, Heidelberg, 2012, pp. 167–182.","apa":"Bouajjani, A., Dragoi, C., Enea, C., &#38; Sighireanu, M. (2012). Accurate invariant checking for programs manipulating lists and arrays with infinite data. In <i>Automated Technology for Verification and Analysis</i> (Vol. 7561, pp. 167–182). Berlin, Heidelberg: Springer. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">https://doi.org/10.1007/978-3-642-33386-6_14</a>","chicago":"Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” In <i>Automated Technology for Verification and Analysis</i>, 7561:167–82. LNCS. Berlin, Heidelberg: Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">https://doi.org/10.1007/978-3-642-33386-6_14</a>.","mla":"Bouajjani, Ahmed, et al. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” <i>Automated Technology for Verification and Analysis</i>, vol. 7561, Springer, 2012, pp. 167–82, doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">10.1007/978-3-642-33386-6_14</a>.","ama":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. Accurate invariant checking for programs manipulating lists and arrays with infinite data. In: <i>Automated Technology for Verification and Analysis</i>. Vol 7561. LNCS. Berlin, Heidelberg: Springer; 2012:167-182. doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">10.1007/978-3-642-33386-6_14</a>","ista":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Accurate invariant checking for programs manipulating lists and arrays with infinite data. Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and AnalysisLNCS, LNCS, vol. 7561, 167–182.","ieee":"A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Accurate invariant checking for programs manipulating lists and arrays with infinite data,” in <i>Automated Technology for Verification and Analysis</i>, Thiruvananthapuram, India, 2012, vol. 7561, pp. 167–182."},"abstract":[{"text":"We propose a logic-based framework for automated reasoning about sequential programs manipulating singly-linked lists and arrays with unbounded data. We introduce the logic SLAD, which allows combining shape constraints, written in a fragment of Separation Logic, with data and size constraints. We address the problem of checking the entailment between SLAD formulas, which is crucial in performing pre-post condition reasoning. Although this problem is undecidable in general for SLAD, we propose a sound and powerful procedure that is able to solve this problem for a large class of formulas, beyond the capabilities of existing techniques and tools. We prove that this procedure is complete, i.e., it is actually a decision procedure for this problem, for an important fragment of SLAD including known decidable logics. We implemented this procedure and shown its preciseness and its efficiency on a significant benchmark of formulas.","lang":"eng"}],"conference":{"end_date":"2012-10-06","location":"Thiruvananthapuram, India","name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2012-10-03"},"_id":"10903","date_created":"2022-03-21T07:58:39Z","doi":"10.1007/978-3-642-33386-6_14","scopus_import":"1","acknowledgement":"This work has been partially supported by the French ANR project Veridyc","publication_identifier":{"eisbn":["9783642333866"],"isbn":["9783642333859"],"eissn":["1611-3349"],"issn":["0302-9743"]},"title":"Accurate invariant checking for programs manipulating lists and arrays with infinite data","publication_status":"published","article_processing_charge":"No","oa_version":"None","language":[{"iso":"eng"}],"alternative_title":["LNCS"],"month":"10","status":"public","publisher":"Springer","date_published":"2012-10-15T00:00:00Z","type":"conference","page":"167-182","day":"15","quality_controlled":"1"},{"publication_status":"published","title":"Polynomial-time algorithms for energy games with special weight structures","oa_version":"Preprint","article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.08234"}],"doi":"10.1007/978-3-642-33090-2_27","scopus_import":"1","acknowledgement":"Supported by the Austrian Science Fund (FWF): P23499-N23, the Austrian Science Fund (FWF): S11407-N23 (RiSE), an ERC Start Grant (279307: Graph Games), and a Microsoft Faculty Fellows Award","publication_identifier":{"issn":["0302-9743"],"isbn":["9783642330896"],"eisbn":["9783642330902"],"eissn":["1611-3349"]},"conference":{"end_date":"2012-09-12","name":"ESA: European Symposium on Algorithms","location":"Ljubljana, Slovenia","start_date":"2012-09-10"},"_id":"10905","date_created":"2022-03-21T08:01:45Z","year":"2012","citation":{"mla":"Chatterjee, Krishnendu, et al. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” <i>Algorithms – ESA 2012</i>, vol. 7501, Springer, 2012, pp. 301–12, doi:<a href=\"https://doi.org/10.1007/978-3-642-33090-2_27\">10.1007/978-3-642-33090-2_27</a>.","short":"K. Chatterjee, M.H. Henzinger, S. Krinninger, D. Nanongkai, in:, Algorithms – ESA 2012, Springer, 2012, pp. 301–312.","apa":"Chatterjee, K., Henzinger, M. H., Krinninger, S., &#38; Nanongkai, D. (2012). Polynomial-time algorithms for energy games with special weight structures. In <i>Algorithms – ESA 2012</i> (Vol. 7501, pp. 301–312). Ljubljana, Slovenia: Springer. <a href=\"https://doi.org/10.1007/978-3-642-33090-2_27\">https://doi.org/10.1007/978-3-642-33090-2_27</a>","chicago":"Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, and Danupon Nanongkai. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” In <i>Algorithms – ESA 2012</i>, 7501:301–12. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-33090-2_27\">https://doi.org/10.1007/978-3-642-33090-2_27</a>.","ista":"Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. 2012. Polynomial-time algorithms for energy games with special weight structures. Algorithms – ESA 2012. ESA: European Symposium on Algorithms, LNCS, vol. 7501, 301–312.","ieee":"K. Chatterjee, M. H. Henzinger, S. Krinninger, and D. Nanongkai, “Polynomial-time algorithms for energy games with special weight structures,” in <i>Algorithms – ESA 2012</i>, Ljubljana, Slovenia, 2012, vol. 7501, pp. 301–312.","ama":"Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. Polynomial-time algorithms for energy games with special weight structures. In: <i>Algorithms – ESA 2012</i>. Vol 7501. Springer; 2012:301-312. doi:<a href=\"https://doi.org/10.1007/978-3-642-33090-2_27\">10.1007/978-3-642-33090-2_27</a>"},"abstract":[{"text":"Energy games belong to a class of turn-based two-player infinite-duration games played on a weighted directed graph. It is one of the rare and intriguing combinatorial problems that lie in NP ∩ co−NP, but are not known to be in P. While the existence of polynomial-time algorithms has been a major open problem for decades, there is no algorithm that solves any non-trivial subclass in polynomial time.\r\nIn this paper, we give several results based on the weight structures of the graph. First, we identify a notion of penalty and present a polynomial-time algorithm when the penalty is large. Our algorithm is the first polynomial-time algorithm on a large class of weighted graphs. It includes several counter examples that show that many previous algorithms, such as value iteration and random facet algorithms, require at least sub-exponential time. Our main technique is developing the first non-trivial approximation algorithm and showing how to convert it to an exact algorithm. Moreover, we show that in a practical case in verification where weights are clustered around a constant number of values, the energy game problem can be solved in polynomial time. We also show that the problem is still as hard as in general when the clique-width is bounded or the graph is strongly ergodic, suggesting that restricting graph structures need not help.","lang":"eng"}],"related_material":{"record":[{"id":"535","status":"public","relation":"later_version"}]},"oa":1,"volume":7501,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Henzinger","first_name":"Monika H","full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"last_name":"Krinninger","first_name":"Sebastian","full_name":"Krinninger, Sebastian"},{"last_name":"Nanongkai","first_name":"Danupon","full_name":"Nanongkai, Danupon"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","department":[{"_id":"KrCh"}],"publication":"Algorithms – ESA 2012","date_updated":"2023-09-05T14:09:30Z","ec_funded":1,"arxiv":1,"intvolume":"      7501","quality_controlled":"1","page":"301-312","day":"01","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"external_id":{"arxiv":["1604.08234"]},"date_published":"2012-10-01T00:00:00Z","type":"conference","publisher":"Springer","month":"10","status":"public","language":[{"iso":"eng"}],"alternative_title":["LNCS"]},{"quality_controlled":"1","day":"01","page":"549-551","type":"conference","date_published":"2012-04-01T00:00:00Z","publisher":"Springer","status":"public","month":"04","alternative_title":["LNCS"],"language":[{"iso":"eng"}],"article_processing_charge":"No","oa_version":"Published Version","publication_status":"published","title":"HSF(C): A software verifier based on Horn clauses","publication_identifier":{"eissn":["1611-3349"],"eisbn":["9783642287565"],"isbn":["9783642287558"],"issn":["0302-9743"]},"scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/978-3-642-28756-5_46"}],"doi":"10.1007/978-3-642-28756-5_46","date_created":"2022-03-21T08:03:30Z","_id":"10906","conference":{"start_date":"2012-03-24","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Tallinn, Estonia","end_date":"2012-04-01"},"editor":[{"full_name":"Flanagan, Cormac","last_name":"Flanagan","first_name":"Cormac"},{"last_name":"König","first_name":"Barbara","full_name":"König, Barbara"}],"abstract":[{"text":"HSF(C) is a tool that automates verification of safety and liveness properties for C programs. This paper describes the verification approach taken by HSF(C) and provides instructions on how to install and use the tool.","lang":"eng"}],"citation":{"chicago":"Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, edited by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">https://doi.org/10.1007/978-3-642-28756-5_46</a>.","short":"S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko, in:, C. Flanagan, B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, Heidelberg, 2012, pp. 549–551.","apa":"Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., &#38; Rybalchenko, A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan &#38; B. König (Eds.), <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. <a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">https://doi.org/10.1007/978-3-642-28756-5_46</a>","mla":"Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn Clauses.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51, doi:<a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">10.1007/978-3-642-28756-5_46</a>.","ama":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. HSF(C): A software verifier based on Horn clauses. In: Flanagan C, König B, eds. <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 7214. LNCS. Berlin, Heidelberg: Springer; 2012:549-551. doi:<a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">10.1007/978-3-642-28756-5_46</a>","ista":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. 2012. HSF(C): A software verifier based on Horn clauses. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of SystemsLNCS, LNCS, vol. 7214, 549–551.","ieee":"S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko, “HSF(C): A software verifier based on Horn clauses,” in <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, Tallinn, Estonia, 2012, vol. 7214, pp. 549–551."},"year":"2012","place":"Berlin, Heidelberg","volume":7214,"oa":1,"series_title":"LNCS","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"full_name":"Grebenshchikov, Sergey","first_name":"Sergey","last_name":"Grebenshchikov"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh","first_name":"Ashutosh","last_name":"Gupta"},{"last_name":"Lopes","first_name":"Nuno P.","full_name":"Lopes, Nuno P."},{"full_name":"Popeea, Corneliu","last_name":"Popeea","first_name":"Corneliu"},{"full_name":"Rybalchenko, Andrey","last_name":"Rybalchenko","first_name":"Andrey"}],"date_updated":"2023-09-05T14:09:54Z","publication":"Tools and Algorithms for the Construction and Analysis of Systems","department":[{"_id":"ToHe"}],"intvolume":"      7214"},{"quality_controlled":"1","day":"01","page":"215-224","type":"conference","date_published":"2011-06-01T00:00:00Z","publisher":"Springer","status":"public","month":"06","alternative_title":["LNCS"],"language":[{"iso":"eng"}],"article_processing_charge":"No","oa_version":"None","publication_status":"published","title":"Spatio-temporal extraction of articulated models in a graph pyramid","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783642208430"],"eisbn":["9783642208447"],"issn":["0302-9743"]},"acknowledgement":"This work has been partially supported by the Austrian Science Fund under grants S9103-N13 and P18716-N13.","scopus_import":"1","doi":"10.1007/978-3-642-20844-7_22","date_created":"2022-03-21T08:08:35Z","_id":"10907","conference":{"start_date":"2011-05-18","end_date":"2011-05-20","location":"Münster, Germany","name":"GbRPR: Graph-based Representations in Pattern Recognition"},"editor":[{"full_name":"Jiang, Xiaoyi","first_name":"Xiaoyi","last_name":"Jiang"},{"full_name":"Ferrer, Miquel","first_name":"Miquel","last_name":"Ferrer"},{"full_name":"Torsello, Andrea","last_name":"Torsello","first_name":"Andrea"}],"abstract":[{"text":"This paper presents a method to create a model of an articulated object using the planar motion in an initialization video. The model consists of rigid parts connected by points of articulation. The rigid parts are described by the positions of salient feature-points tracked throughout the video. Following a filtering step that identifies points that belong to different objects, rigid parts are found by a grouping process in a graph pyramid. Valid articulation points are selected by verifying multiple hypotheses for each pair of parts.","lang":"eng"}],"citation":{"ama":"Artner NM, Ion A, Kropatsch WG. Spatio-temporal extraction of articulated models in a graph pyramid. In: Jiang X, Ferrer M, Torsello A, eds. <i>Graph-Based Representations in Pattern Recognition</i>. Vol 6658. LNIP. Berlin, Heidelberg: Springer; 2011:215-224. doi:<a href=\"https://doi.org/10.1007/978-3-642-20844-7_22\">10.1007/978-3-642-20844-7_22</a>","ista":"Artner NM, Ion A, Kropatsch WG. 2011. Spatio-temporal extraction of articulated models in a graph pyramid. Graph-Based Representations in Pattern Recognition. GbRPR: Graph-based Representations in Pattern RecognitionLNIP, LNCS, vol. 6658, 215–224.","ieee":"N. M. Artner, A. Ion, and W. G. Kropatsch, “Spatio-temporal extraction of articulated models in a graph pyramid,” in <i>Graph-Based Representations in Pattern Recognition</i>, Münster, Germany, 2011, vol. 6658, pp. 215–224.","mla":"Artner, Nicole M., et al. “Spatio-Temporal Extraction of Articulated Models in a Graph Pyramid.” <i>Graph-Based Representations in Pattern Recognition</i>, edited by Xiaoyi Jiang et al., vol. 6658, Springer, 2011, pp. 215–24, doi:<a href=\"https://doi.org/10.1007/978-3-642-20844-7_22\">10.1007/978-3-642-20844-7_22</a>.","chicago":"Artner, Nicole M., Adrian Ion, and Walter G. Kropatsch. “Spatio-Temporal Extraction of Articulated Models in a Graph Pyramid.” In <i>Graph-Based Representations in Pattern Recognition</i>, edited by Xiaoyi Jiang, Miquel Ferrer, and Andrea Torsello, 6658:215–24. LNIP. Berlin, Heidelberg: Springer, 2011. <a href=\"https://doi.org/10.1007/978-3-642-20844-7_22\">https://doi.org/10.1007/978-3-642-20844-7_22</a>.","short":"N.M. Artner, A. Ion, W.G. Kropatsch, in:, X. Jiang, M. Ferrer, A. Torsello (Eds.), Graph-Based Representations in Pattern Recognition, Springer, Berlin, Heidelberg, 2011, pp. 215–224.","apa":"Artner, N. M., Ion, A., &#38; Kropatsch, W. G. (2011). Spatio-temporal extraction of articulated models in a graph pyramid. In X. Jiang, M. Ferrer, &#38; A. Torsello (Eds.), <i>Graph-Based Representations in Pattern Recognition</i> (Vol. 6658, pp. 215–224). Berlin, Heidelberg: Springer. <a href=\"https://doi.org/10.1007/978-3-642-20844-7_22\">https://doi.org/10.1007/978-3-642-20844-7_22</a>"},"year":"2011","place":"Berlin, Heidelberg","volume":6658,"series_title":"LNIP","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","author":[{"full_name":"Artner, Nicole M.","first_name":"Nicole M.","last_name":"Artner"},{"last_name":"Ion","first_name":"Adrian","full_name":"Ion, Adrian","id":"29F89302-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kropatsch, Walter G.","first_name":"Walter G.","last_name":"Kropatsch"}],"date_updated":"2023-09-05T14:10:15Z","publication":"Graph-Based Representations in Pattern Recognition","department":[{"_id":"HeEd"}],"intvolume":"      6658"},{"page":"103-118","day":"01","quality_controlled":"1","language":[{"iso":"eng"}],"month":"05","status":"public","publisher":"Springer Nature","date_published":"2010-05-01T00:00:00Z","type":"conference","year":"2010","place":"Berlin, Heidelberg","citation":{"ista":"Blanc R, Henzinger TA, Hottelier T, Kovács L. 2010. ABC: Algebraic Bound Computation for loops. Logic for Programming, Artificial Intelligence, and Reasoning. LPAR: Conference on Logic for Programming, Artificial Intelligence and ReasoningLNCS vol. 6355, 103–118.","ieee":"R. Blanc, T. A. Henzinger, T. Hottelier, and L. Kovács, “ABC: Algebraic Bound Computation for loops,” in <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>, Dakar, Senegal, 2010, vol. 6355, pp. 103–118.","ama":"Blanc R, Henzinger TA, Hottelier T, Kovács L. ABC: Algebraic Bound Computation for loops. In: Clarke EM, Voronkov A, eds. <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>. Vol 6355. LNCS. Berlin, Heidelberg: Springer Nature; 2010:103-118. doi:<a href=\"https://doi.org/10.1007/978-3-642-17511-4_7\">10.1007/978-3-642-17511-4_7</a>","chicago":"Blanc, Régis, Thomas A Henzinger, Thibaud Hottelier, and Laura Kovács. “ABC: Algebraic Bound Computation for Loops.” In <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>, edited by Edmund M Clarke and Andrei Voronkov, 6355:103–18. LNCS. Berlin, Heidelberg: Springer Nature, 2010. <a href=\"https://doi.org/10.1007/978-3-642-17511-4_7\">https://doi.org/10.1007/978-3-642-17511-4_7</a>.","short":"R. Blanc, T.A. Henzinger, T. Hottelier, L. Kovács, in:, E.M. Clarke, A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning, Springer Nature, Berlin, Heidelberg, 2010, pp. 103–118.","apa":"Blanc, R., Henzinger, T. A., Hottelier, T., &#38; Kovács, L. (2010). ABC: Algebraic Bound Computation for loops. In E. M. Clarke &#38; A. Voronkov (Eds.), <i>Logic for Programming, Artificial Intelligence, and Reasoning</i> (Vol. 6355, pp. 103–118). Berlin, Heidelberg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-17511-4_7\">https://doi.org/10.1007/978-3-642-17511-4_7</a>","mla":"Blanc, Régis, et al. “ABC: Algebraic Bound Computation for Loops.” <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>, edited by Edmund M Clarke and Andrei Voronkov, vol. 6355, Springer Nature, 2010, pp. 103–18, doi:<a href=\"https://doi.org/10.1007/978-3-642-17511-4_7\">10.1007/978-3-642-17511-4_7</a>."},"abstract":[{"text":"We present ABC, a software tool for automatically computing symbolic upper bounds on the number of iterations of nested program loops. The system combines static analysis of programs with symbolic summation techniques to derive loop invariant relations between program variables. Iteration bounds are obtained from the inferred invariants, by replacing variables with bounds on their greatest values. We have successfully applied ABC to a large number of examples. The derived symbolic bounds express non-trivial polynomial relations over loop variables. We also report on results to automatically infer symbolic expressions over harmonic numbers as upper bounds on loop iteration counts.","lang":"eng"}],"editor":[{"full_name":"Clarke, Edmund M","last_name":"Clarke","first_name":"Edmund M"},{"last_name":"Voronkov","first_name":"Andrei","full_name":"Voronkov, Andrei"}],"conference":{"start_date":"2010-04-25","end_date":"2010-05-01","name":"LPAR: Conference on Logic for Programming, Artificial Intelligence and Reasoning","location":"Dakar, Senegal"},"_id":"10908","date_created":"2022-03-21T08:14:35Z","main_file_link":[{"url":"https://infoscience.epfl.ch/record/186096","open_access":"1"}],"doi":"10.1007/978-3-642-17511-4_7","scopus_import":"1","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783642175107"],"eisbn":["9783642175114"]},"acknowledgement":"This work was supported in part by the Swiss NSF. The fourth author is supported by an FWF Hertha Firnberg Research grant (T425-N23).","publication_status":"published","title":"ABC: Algebraic Bound Computation for loops","oa_version":"Submitted Version","article_processing_charge":"No","intvolume":"      6355","department":[{"_id":"ToHe"}],"publication":"Logic for Programming, Artificial Intelligence, and Reasoning","date_updated":"2022-06-13T07:44:21Z","author":[{"full_name":"Blanc, Régis","first_name":"Régis","last_name":"Blanc"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"first_name":"Thibaud","last_name":"Hottelier","full_name":"Hottelier, Thibaud"},{"full_name":"Kovács, Laura","first_name":"Laura","last_name":"Kovács"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","series_title":"LNCS","oa":1,"volume":6355},{"oa_version":"None","article_processing_charge":"No","title":"The past, present, and future of web search engines","quality_controlled":"1","publication_status":"published","day":"01","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"]},"page":"3","doi":"10.1007/978-3-540-27836-8_2","scopus_import":"1","_id":"11800","date_created":"2022-08-11T12:38:58Z","conference":{"end_date":"2004-07-16","name":"ICALP: International Colloquium on Automata, Languages, and Programming","location":"Turku, Finland","start_date":"2004-07-12"},"abstract":[{"text":"Web search engines have emerged as one of the central applications on the Internet. In fact, search has become one of the most important activities that people engage in on the the Internet. Even beyond becoming the number one source of information, a growing number of businesses are depending on web search engines for customer acquisition.\r\n\r\nThe first generation of web search engines used text-only retrieval techniques. Google revolutionized the field by deploying the PageRank technology – an eigenvector-based analysis of the hyperlink structure – to analyze the web in order to produce relevant results. Moving forward, our goal is to achieve a better understanding of a page with a view towards producing even more relevant results.","lang":"eng"}],"year":"2004","citation":{"ista":"Henzinger MH. 2004. The past, present, and future of web search engines. 31st International Colloquium on Automata, Languages and Programming. ICALP: International Colloquium on Automata, Languages, and Programming, LNCS, vol. 3142, 3.","ieee":"M. H. Henzinger, “The past, present, and future of web search engines,” in <i>31st International Colloquium on Automata, Languages and Programming</i>, Turku, Finland, 2004, vol. 3142, p. 3.","ama":"Henzinger MH. The past, present, and future of web search engines. In: <i>31st International Colloquium on Automata, Languages and Programming</i>. Vol 3142. Springer Nature; 2004:3. doi:<a href=\"https://doi.org/10.1007/978-3-540-27836-8_2\">10.1007/978-3-540-27836-8_2</a>","mla":"Henzinger, Monika H. “The Past, Present, and Future of Web Search Engines.” <i>31st International Colloquium on Automata, Languages and Programming</i>, vol. 3142, Springer Nature, 2004, p. 3, doi:<a href=\"https://doi.org/10.1007/978-3-540-27836-8_2\">10.1007/978-3-540-27836-8_2</a>.","chicago":"Henzinger, Monika H. “The Past, Present, and Future of Web Search Engines.” In <i>31st International Colloquium on Automata, Languages and Programming</i>, 3142:3. Springer Nature, 2004. <a href=\"https://doi.org/10.1007/978-3-540-27836-8_2\">https://doi.org/10.1007/978-3-540-27836-8_2</a>.","short":"M.H. Henzinger, in:, 31st International Colloquium on Automata, Languages and Programming, Springer Nature, 2004, p. 3.","apa":"Henzinger, M. H. (2004). The past, present, and future of web search engines. In <i>31st International Colloquium on Automata, Languages and Programming</i> (Vol. 3142, p. 3). Turku, Finland: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-540-27836-8_2\">https://doi.org/10.1007/978-3-540-27836-8_2</a>"},"volume":3142,"date_published":"2004-07-01T00:00:00Z","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer Nature","author":[{"first_name":"Monika H","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H"}],"status":"public","publication":"31st International Colloquium on Automata, Languages and Programming","date_updated":"2023-02-13T11:45:25Z","month":"07","extern":"1","intvolume":"      3142","alternative_title":["LNCS"],"language":[{"iso":"eng"}]},{"language":[{"iso":"eng"}],"alternative_title":["LNCS"],"intvolume":"      3221","extern":"1","month":"09","status":"public","publication":"2th Annual European Symposium on Algorithms","date_updated":"2023-02-13T11:47:26Z","publisher":"Springer Nature","author":[{"first_name":"Monika H","last_name":"Henzinger","orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2004-09-01T00:00:00Z","type":"conference","volume":3221,"year":"2004","citation":{"mla":"Henzinger, Monika H. “Algorithmic Aspects of Web Search Engines.” <i>2th Annual European Symposium on Algorithms</i>, vol. 3221, Springer Nature, 2004, p. 3, doi:<a href=\"https://doi.org/10.1007/978-3-540-30140-0_2\">10.1007/978-3-540-30140-0_2</a>.","chicago":"Henzinger, Monika H. “Algorithmic Aspects of Web Search Engines.” In <i>2th Annual European Symposium on Algorithms</i>, 3221:3. Springer Nature, 2004. <a href=\"https://doi.org/10.1007/978-3-540-30140-0_2\">https://doi.org/10.1007/978-3-540-30140-0_2</a>.","short":"M.H. Henzinger, in:, 2th Annual European Symposium on Algorithms, Springer Nature, 2004, p. 3.","apa":"Henzinger, M. H. (2004). Algorithmic aspects of web search engines. In <i>2th Annual European Symposium on Algorithms</i> (Vol. 3221, p. 3). Bergen, Norway: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-540-30140-0_2\">https://doi.org/10.1007/978-3-540-30140-0_2</a>","ama":"Henzinger MH. Algorithmic aspects of web search engines. In: <i>2th Annual European Symposium on Algorithms</i>. Vol 3221. Springer Nature; 2004:3. doi:<a href=\"https://doi.org/10.1007/978-3-540-30140-0_2\">10.1007/978-3-540-30140-0_2</a>","ista":"Henzinger MH. 2004. Algorithmic aspects of web search engines. 2th Annual European Symposium on Algorithms. ESA: European Symposium on Algorithms, LNCS, vol. 3221, 3.","ieee":"M. H. Henzinger, “Algorithmic aspects of web search engines,” in <i>2th Annual European Symposium on Algorithms</i>, Bergen, Norway, 2004, vol. 3221, p. 3."},"abstract":[{"text":"Web search engines have emerged as one of the central applications on the internet. In fact, search has become one of the most important activities that people engage in on the Internet. Even beyond becoming the number one source of information, a growing number of businesses are depending on web search engines for customer acquisition. In this talk I will brief review the history of web search engines: The first generation of web search engines used text-only retrieval techniques. Google revolutionized the field by deploying the PageRank technology – an eigenvector-based analysis of the hyperlink structure- to analyze the web in order to produce relevant results. Moving forward, our goal is to achieve a better understanding of a page with a view towards producing even more relevant results.\r\n\r\nGoogle is powered by a large number of PCs. Using this infrastructure and striving to be as efficient as possible poses challenging systems problems but also various algorithmic challenges. I will discuss some of them in my talk.","lang":"eng"}],"conference":{"location":"Bergen, Norway","name":"ESA: European Symposium on Algorithms","end_date":"2004-09-17","start_date":"2004-09-14"},"_id":"11801","date_created":"2022-08-11T13:18:05Z","doi":"10.1007/978-3-540-30140-0_2","page":"3","scopus_import":"1","day":"01","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":[" 3540230254"]},"quality_controlled":"1","title":"Algorithmic aspects of web search engines","publication_status":"published","article_processing_charge":"No","oa_version":"None"}]