[{"date_published":"2011-03-28T00:00:00Z","language":[{"iso":"eng"}],"month":"03","pubrep_id":"22","publication_status":"published","day":"28","department":[{"_id":"ChLa"}],"status":"public","date_updated":"2023-02-23T11:22:48Z","year":"2011","date_created":"2018-12-12T11:39:02Z","title":"Enforcing topological constraints in random field image segmentation","citation":{"mla":"Chen, Chao, et al. Enforcing Topological Constraints in Random Field Image Segmentation. IST Austria, 2011, doi:10.15479/AT:IST-2011-0002.","short":"C. Chen, D. Freedman, C. Lampert, Enforcing Topological Constraints in Random Field Image Segmentation, IST Austria, 2011.","ama":"Chen C, Freedman D, Lampert C. Enforcing Topological Constraints in Random Field Image Segmentation. IST Austria; 2011. doi:10.15479/AT:IST-2011-0002","ieee":"C. Chen, D. Freedman, and C. Lampert, Enforcing topological constraints in random field image segmentation. IST Austria, 2011.","apa":"Chen, C., Freedman, D., & Lampert, C. (2011). Enforcing topological constraints in random field image segmentation. IST Austria. https://doi.org/10.15479/AT:IST-2011-0002","chicago":"Chen, Chao, Daniel Freedman, and Christoph Lampert. Enforcing Topological Constraints in Random Field Image Segmentation. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0002.","ista":"Chen C, Freedman D, Lampert C. 2011. Enforcing topological constraints in random field image segmentation, IST Austria, 69p."},"alternative_title":["IST Austria Technical Report"],"ddc":["000"],"oa_version":"Published Version","related_material":{"record":[{"status":"public","id":"3336","relation":"later_version"}]},"_id":"5386","publication_identifier":{"issn":["2664-1690"]},"page":"69","author":[{"first_name":"Chao","id":"3E92416E-F248-11E8-B48F-1D18A9856A87","full_name":"Chen, Chao","last_name":"Chen"},{"first_name":"Daniel","full_name":"Freedman, Daniel","last_name":"Freedman"},{"last_name":"Lampert","id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","full_name":"Lampert, Christoph","first_name":"Christoph","orcid":"0000-0001-8622-7887"}],"oa":1,"publisher":"IST Austria","file":[{"date_updated":"2020-07-14T12:46:41Z","content_type":"application/pdf","file_id":"5495","checksum":"ad64c2add5fe2ad10e9d5c669f3f9526","file_size":26390601,"date_created":"2018-12-12T11:53:34Z","relation":"main_file","file_name":"IST-2011-0002_IST-2011-0002.pdf","access_level":"open_access","creator":"system"}],"type":"technical_report","file_date_updated":"2020-07-14T12:46:41Z","doi":"10.15479/AT:IST-2011-0002","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","has_accepted_license":"1","abstract":[{"lang":"eng","text":"We introduce TopoCut: a new way to integrate knowledge about topological properties (TPs) into random field image segmentation model. Instead of including TPs as additional constraints during minimization of the energy function, we devise an efficient algorithm for modifying the unary potentials such that the resulting segmentation is guaranteed with the desired properties. Our method is more flexible in the sense that it handles more topology constraints than previous methods, which were only able to enforce pairwise or global connectivity. In particular, our method is very fast, making it for the first time possible to enforce global topological properties in practical image segmentation tasks."}]},{"date_updated":"2023-02-23T11:22:16Z","year":"2011","department":[{"_id":"ToHe"}],"status":"public","publication_status":"published","day":"26","month":"04","pubrep_id":"19","language":[{"iso":"eng"}],"date_published":"2011-04-26T00:00:00Z","file_date_updated":"2020-07-14T12:46:40Z","doi":"10.15479/AT:IST-2011-0005","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","has_accepted_license":"1","abstract":[{"text":"We present a new decidable logic called TREX for expressing constraints about imperative tree data structures. In particular, TREX supports a transitive closure operator that can express reachability constraints, which often appear in data structure invariants. We show that our logic is closed under weakest precondition computation, which enables its use for automated software verification. We further show that satisfiability of formulas in TREX is decidable in NP. The low complexity makes it an attractive alternative to more expensive logics such as monadic second-order logic (MSOL) over trees, which have been traditionally used for reasoning about tree data structures.","lang":"eng"}],"file":[{"date_updated":"2020-07-14T12:46:40Z","content_type":"application/pdf","checksum":"b20029184c4a819c5f4466a4a3d238b5","file_id":"5462","creator":"system","file_name":"IST-2011-0005_IST-2011-0005.pdf","access_level":"open_access","relation":"main_file","date_created":"2018-12-12T11:53:01Z","file_size":619053}],"type":"technical_report","author":[{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Wies, Thomas","last_name":"Wies","first_name":"Thomas"},{"first_name":"Marco","full_name":"Muñiz, Marco","last_name":"Muñiz"},{"full_name":"Kuncak, Viktor","last_name":"Kuncak","first_name":"Viktor"}],"oa":1,"publisher":"IST Austria","page":"25","_id":"5383","related_material":{"record":[{"id":"3323","status":"public","relation":"later_version"}]},"publication_identifier":{"issn":["2664-1690"]},"ddc":["000","006"],"oa_version":"Published Version","alternative_title":["IST Austria Technical Report"],"citation":{"chicago":"Wies, Thomas, Marco Muñiz, and Viktor Kuncak. On an Efficient Decision Procedure for Imperative Tree Data Structures. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0005.","ista":"Wies T, Muñiz M, Kuncak V. 2011. On an efficient decision procedure for imperative tree data structures, IST Austria, 25p.","apa":"Wies, T., Muñiz, M., & Kuncak, V. (2011). On an efficient decision procedure for imperative tree data structures. IST Austria. https://doi.org/10.15479/AT:IST-2011-0005","ieee":"T. Wies, M. Muñiz, and V. Kuncak, On an efficient decision procedure for imperative tree data structures. IST Austria, 2011.","ama":"Wies T, Muñiz M, Kuncak V. On an Efficient Decision Procedure for Imperative Tree Data Structures. IST Austria; 2011. doi:10.15479/AT:IST-2011-0005","short":"T. Wies, M. Muñiz, V. Kuncak, On an Efficient Decision Procedure for Imperative Tree Data Structures, IST Austria, 2011.","mla":"Wies, Thomas, et al. On an Efficient Decision Procedure for Imperative Tree Data Structures. IST Austria, 2011, doi:10.15479/AT:IST-2011-0005."},"date_created":"2018-12-12T11:39:01Z","title":"On an efficient decision procedure for imperative tree data structures"},{"month":"04","pubrep_id":"20","date_published":"2011-04-11T00:00:00Z","language":[{"iso":"eng"}],"date_updated":"2023-02-23T11:05:53Z","year":"2011","day":"11","publication_status":"published","status":"public","department":[{"_id":"KrCh"}],"ddc":["000","005"],"oa_version":"Published Version","related_material":{"record":[{"status":"public","id":"2957","relation":"later_version"}]},"_id":"5384","publication_identifier":{"issn":["2664-1690"]},"date_created":"2018-12-12T11:39:01Z","title":"Decidable problems for probabilistic automata on infinite words","alternative_title":["IST Austria Technical Report"],"citation":{"ista":"Chatterjee K, Tracol M. 2011. Decidable problems for probabilistic automata on infinite words, IST Austria, 30p.","chicago":"Chatterjee, Krishnendu, and Mathieu Tracol. Decidable Problems for Probabilistic Automata on Infinite Words. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0004.","ieee":"K. Chatterjee and M. Tracol, Decidable problems for probabilistic automata on infinite words. IST Austria, 2011.","apa":"Chatterjee, K., & Tracol, M. (2011). Decidable problems for probabilistic automata on infinite words. IST Austria. https://doi.org/10.15479/AT:IST-2011-0004","ama":"Chatterjee K, Tracol M. Decidable Problems for Probabilistic Automata on Infinite Words. IST Austria; 2011. doi:10.15479/AT:IST-2011-0004","short":"K. Chatterjee, M. Tracol, Decidable Problems for Probabilistic Automata on Infinite Words, IST Austria, 2011.","mla":"Chatterjee, Krishnendu, and Mathieu Tracol. Decidable Problems for Probabilistic Automata on Infinite Words. IST Austria, 2011, doi:10.15479/AT:IST-2011-0004."},"file":[{"content_type":"application/pdf","date_updated":"2020-07-14T12:46:40Z","relation":"main_file","file_size":570827,"date_created":"2018-12-12T11:54:23Z","creator":"system","access_level":"open_access","file_name":"IST-2011-004_IST-2011-0004.pdf","file_id":"5545","checksum":"f5a0f664fadc335990f5fcf138df19f1"}],"type":"technical_report","file_date_updated":"2020-07-14T12:46:40Z","doi":"10.15479/AT:IST-2011-0004","abstract":[{"lang":"eng","text":"We consider probabilistic automata on infinite words with acceptance defined by parity conditions. We consider three qualitative decision problems: (i) the positive decision problem asks whether there is a word that is accepted with positive probability; (ii) the almost decision problem asks whether there is a word that is accepted with probability 1; and (iii) the limit decision problem asks whether for every ε > 0 there is a word that is accepted with probability at least 1 − ε. We unify and generalize several decidability results for probabilistic automata over infinite words, and identify a robust (closed under union and intersection) subclass of probabilistic automata for which all the qualitative decision problems are decidable for parity conditions. We also show that if the input words are restricted to lasso shape words, then the positive and almost problems are decidable for all probabilistic automata with parity conditions."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","has_accepted_license":"1","page":"30","oa":1,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Tracol","full_name":"Tracol, Mathieu","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87","first_name":"Mathieu"}],"publisher":"IST Austria"},{"article_processing_charge":"No","acknowledgement":"The first author is supported by the Austrian Science Fund (FWF) grant No. P20134-N13. The authors would like to thank Sebastian Nowozin for helpful discussions.","citation":{"mla":"Chen, Chao, et al. “Enforcing Topological Constraints in Random Field Image Segmentation.” CVPR: Computer Vision and Pattern Recognition, IEEE, 2011, pp. 2089–96, doi:10.1109/CVPR.2011.5995503.","short":"C. Chen, D. Freedman, C. Lampert, in:, CVPR: Computer Vision and Pattern Recognition, IEEE, 2011, pp. 2089–2096.","ama":"Chen C, Freedman D, Lampert C. Enforcing topological constraints in random field image segmentation. In: CVPR: Computer Vision and Pattern Recognition. IEEE; 2011:2089-2096. doi:10.1109/CVPR.2011.5995503","apa":"Chen, C., Freedman, D., & Lampert, C. (2011). Enforcing topological constraints in random field image segmentation. In CVPR: Computer Vision and Pattern Recognition (pp. 2089–2096). Colorado Springs, CO, United States: IEEE. https://doi.org/10.1109/CVPR.2011.5995503","ieee":"C. Chen, D. Freedman, and C. Lampert, “Enforcing topological constraints in random field image segmentation,” in CVPR: Computer Vision and Pattern Recognition, Colorado Springs, CO, United States, 2011, pp. 2089–2096.","ista":"Chen C, Freedman D, Lampert C. 2011. Enforcing topological constraints in random field image segmentation. CVPR: Computer Vision and Pattern Recognition. CVPR: Conference on Computer Vision and Pattern Recognition, 2089–2096.","chicago":"Chen, Chao, Daniel Freedman, and Christoph Lampert. “Enforcing Topological Constraints in Random Field Image Segmentation.” In CVPR: Computer Vision and Pattern Recognition, 2089–96. IEEE, 2011. https://doi.org/10.1109/CVPR.2011.5995503."},"date_created":"2018-12-11T12:02:45Z","title":"Enforcing topological constraints in random field image segmentation","quality_controlled":"1","_id":"3336","related_material":{"record":[{"relation":"earlier_version","id":"5386","status":"public"}]},"publication_identifier":{"eisbn":["978-1-4577-0395-9"],"isbn":["978-1-4577-0394-2"]},"oa_version":"None","author":[{"last_name":"Chen","id":"3E92416E-F248-11E8-B48F-1D18A9856A87","full_name":"Chen, Chao","first_name":"Chao"},{"last_name":"Freedman","full_name":"Freedman, Daniel","first_name":"Daniel"},{"first_name":"Christoph","orcid":"0000-0001-8622-7887","last_name":"Lampert","id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","full_name":"Lampert, Christoph"}],"publisher":"IEEE","page":"2089 - 2096","doi":"10.1109/CVPR.2011.5995503","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"We introduce TopoCut: a new way to integrate knowledge about topological properties (TPs) into random field image segmentation model. Instead of including TPs as additional constraints during minimization of the energy function, we devise an efficient algorithm for modifying the unary potentials such that the resulting segmentation is guaranteed with the desired properties. Our method is more flexible in the sense that it handles more topology constraints than previous methods, which were only able to enforce pairwise or global connectivity. In particular, our method is very fast, making it for the first time possible to enforce global topological properties in practical image segmentation tasks.","lang":"eng"}],"type":"conference","scopus_import":"1","language":[{"iso":"eng"}],"conference":{"location":"Colorado Springs, CO, United States","name":"CVPR: Conference on Computer Vision and Pattern Recognition","end_date":"2011-06-25","start_date":"2011-06-20"},"date_published":"2011-07-22T00:00:00Z","month":"07","publication":"CVPR: Computer Vision and Pattern Recognition","department":[{"_id":"HeEd"},{"_id":"ChLa"}],"status":"public","publication_status":"published","day":"22","publist_id":"3294","date_updated":"2023-02-23T12:23:56Z","year":"2011"},{"language":[{"iso":"eng"}],"conference":{"location":"Wrocław, Poland","name":"CADE 23: Automated Deduction ","start_date":"2011-07-31","end_date":"2011-08-05"},"date_published":"2011-07-19T00:00:00Z","intvolume":" 6803","month":"07","status":"public","department":[{"_id":"ToHe"}],"publication_status":"published","day":"19","date_updated":"2023-02-23T12:23:48Z","publist_id":"3312","year":"2011","alternative_title":["LNAI "],"citation":{"mla":"Wies, Thomas, et al. An Efficient Decision Procedure for Imperative Tree Data Structures. Vol. 6803, Springer, 2011, pp. 476–91, doi:10.1007/978-3-642-22438-6_36.","short":"T. Wies, M. Muñiz, V. Kuncak, in:, Springer, 2011, pp. 476–491.","ama":"Wies T, Muñiz M, Kuncak V. An efficient decision procedure for imperative tree data structures. In: Vol 6803. Springer; 2011:476-491. doi:10.1007/978-3-642-22438-6_36","ieee":"T. Wies, M. Muñiz, and V. Kuncak, “An efficient decision procedure for imperative tree data structures,” presented at the CADE 23: Automated Deduction , Wrocław, Poland, 2011, vol. 6803, pp. 476–491.","apa":"Wies, T., Muñiz, M., & Kuncak, V. (2011). An efficient decision procedure for imperative tree data structures (Vol. 6803, pp. 476–491). Presented at the CADE 23: Automated Deduction , Wrocław, Poland: Springer. https://doi.org/10.1007/978-3-642-22438-6_36","ista":"Wies T, Muñiz M, Kuncak V. 2011. An efficient decision procedure for imperative tree data structures. CADE 23: Automated Deduction , LNAI , vol. 6803, 476–491.","chicago":"Wies, Thomas, Marco Muñiz, and Viktor Kuncak. “An Efficient Decision Procedure for Imperative Tree Data Structures,” 6803:476–91. Springer, 2011. https://doi.org/10.1007/978-3-642-22438-6_36."},"date_created":"2018-12-11T12:02:40Z","title":"An efficient decision procedure for imperative tree data structures","quality_controlled":"1","_id":"3323","related_material":{"record":[{"status":"public","id":"5383","relation":"earlier_version"}]},"oa_version":"None","author":[{"first_name":"Thomas","last_name":"Wies","full_name":"Wies, Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Muñiz","full_name":"Muñiz, Marco","first_name":"Marco"},{"first_name":"Viktor","full_name":"Kuncak, Viktor","last_name":"Kuncak"}],"publisher":"Springer","page":"476 - 491","doi":"10.1007/978-3-642-22438-6_36","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"We present a new decidable logic called TREX for expressing constraints about imperative tree data structures. In particular, TREX supports a transitive closure operator that can express reachability constraints, which often appear in data structure invariants. We show that our logic is closed under weakest precondition computation, which enables its use for automated software verification. We further show that satisfiability of formulas in TREX is decidable in NP. The low complexity makes it an attractive alternative to more expensive logics such as monadic second-order logic (MSOL) over trees, which have been traditionally used for reasoning about tree data structures."}],"volume":6803,"type":"conference","scopus_import":1}]