[{"has_accepted_license":"1","oa_version":"Published Version","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"}],"month":"07","language":[{"iso":"eng"}],"conference":{"name":"CAV: Computer Aided Verification","start_date":"2018-07-14","end_date":"2018-07-17","location":"Oxford, United Kingdom"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"date_published":"2018-07-18T00:00:00Z","type":"conference","publication_identifier":{"issn":["03029743"]},"publist_id":"7783","oa":1,"file":[{"file_id":"5310","creator":"system","relation":"main_file","access_level":"open_access","date_updated":"2020-07-14T12:44:50Z","content_type":"application/pdf","file_name":"IST-2018-1010-v1+1_space-time_interpolants.pdf","date_created":"2018-12-12T10:17:53Z","checksum":"6dca832f575d6b3f0ea9dff56f579142","file_size":563710}],"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","related_material":{"record":[{"id":"6894","relation":"dissertation_contains","status":"public"}]},"_id":"140","scopus_import":"1","author":[{"first_name":"Goran","last_name":"Frehse","full_name":"Frehse, Goran"},{"first_name":"Mirco","last_name":"Giacobbe","orcid":"0000-0001-8180-0904","full_name":"Giacobbe, Mirco","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"publication_status":"published","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T11:44:50Z","article_processing_charge":"No","alternative_title":["LNCS"],"pubrep_id":"1010","title":"Space-time interpolants","intvolume":"     10981","page":"468 - 486","quality_controlled":"1","file_date_updated":"2020-07-14T12:44:50Z","publisher":"Springer","date_updated":"2023-09-19T09:30:43Z","citation":{"short":"G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2018, pp. 468–486.","mla":"Frehse, Goran, et al. <i>Space-Time Interpolants</i>. Vol. 10981, Springer, 2018, pp. 468–86, doi:<a href=\"https://doi.org/10.1007/978-3-319-96145-3_25\">10.1007/978-3-319-96145-3_25</a>.","ista":"Frehse G, Giacobbe M, Henzinger TA. 2018. Space-time interpolants. CAV: Computer Aided Verification, LNCS, vol. 10981, 468–486.","apa":"Frehse, G., Giacobbe, M., &#38; Henzinger, T. A. (2018). Space-time interpolants (Vol. 10981, pp. 468–486). Presented at the CAV: Computer Aided Verification, Oxford, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-319-96145-3_25\">https://doi.org/10.1007/978-3-319-96145-3_25</a>","ama":"Frehse G, Giacobbe M, Henzinger TA. Space-time interpolants. In: Vol 10981. Springer; 2018:468-486. doi:<a href=\"https://doi.org/10.1007/978-3-319-96145-3_25\">10.1007/978-3-319-96145-3_25</a>","ieee":"G. Frehse, M. Giacobbe, and T. A. Henzinger, “Space-time interpolants,” presented at the CAV: Computer Aided Verification, Oxford, United Kingdom, 2018, vol. 10981, pp. 468–486.","chicago":"Frehse, Goran, Mirco Giacobbe, and Thomas A Henzinger. “Space-Time Interpolants,” 10981:468–86. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-319-96145-3_25\">https://doi.org/10.1007/978-3-319-96145-3_25</a>."},"year":"2018","isi":1,"external_id":{"isi":["000491481600025"]},"doi":"10.1007/978-3-319-96145-3_25","day":"18","abstract":[{"text":"Reachability analysis is difficult for hybrid automata with affine differential equations, because the reach set needs to be approximated. Promising abstraction techniques usually employ interval methods or template polyhedra. Interval methods account for dense time and guarantee soundness, and there are interval-based tools that overapproximate affine flowpipes. But interval methods impose bounded and rigid shapes, which make refinement expensive and fixpoint detection difficult. Template polyhedra, on the other hand, can be adapted flexibly and can be unbounded, but sound template refinement for unbounded reachability analysis has been implemented only for systems with piecewise constant dynamics. We capitalize on the advantages of both techniques, combining interval arithmetic and template polyhedra, using the former to abstract time and the latter to abstract space. During a CEGAR loop, whenever a spurious error trajectory is found, we compute additional space constraints and split time intervals, and use these space-time interpolants to eliminate the counterexample. Space-time interpolation offers a lazy, flexible framework for increasing precision while guaranteeing soundness, both for error avoidance and fixpoint detection. To the best of out knowledge, this is the first abstraction refinement scheme for the reachability analysis over unbounded and dense time of affine hybrid systems, which is both sound and automatic. We demonstrate the effectiveness of our algorithm with several benchmark examples, which cannot be handled by other tools.","lang":"eng"}],"volume":10981,"ddc":["005"]},{"volume":10206,"ddc":["000"],"year":"2017","citation":{"ama":"Avni G, Goel S, Henzinger TA, Rodríguez Navas G. Computing scores of forwarding schemes in switched networks with probabilistic faults. In: Vol 10206. Springer; 2017:169-187. doi:<a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">10.1007/978-3-662-54580-5_10</a>","apa":"Avni, G., Goel, S., Henzinger, T. A., &#38; Rodríguez Navas, G. (2017). Computing scores of forwarding schemes in switched networks with probabilistic faults (Vol. 10206, pp. 169–187). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">https://doi.org/10.1007/978-3-662-54580-5_10</a>","chicago":"Avni, Guy, Shubham Goel, Thomas A Henzinger, and Guillermo Rodríguez Navas. “Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults,” 10206:169–87. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">https://doi.org/10.1007/978-3-662-54580-5_10</a>.","ieee":"G. Avni, S. Goel, T. A. Henzinger, and G. Rodríguez Navas, “Computing scores of forwarding schemes in switched networks with probabilistic faults,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden, 2017, vol. 10206, pp. 169–187.","short":"G. Avni, S. Goel, T.A. Henzinger, G. Rodríguez Navas, in:, Springer, 2017, pp. 169–187.","mla":"Avni, Guy, et al. <i>Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults</i>. Vol. 10206, Springer, 2017, pp. 169–87, doi:<a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">10.1007/978-3-662-54580-5_10</a>.","ista":"Avni G, Goel S, Henzinger TA, Rodríguez Navas G. 2017. Computing scores of forwarding schemes in switched networks with probabilistic faults. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10206, 169–187."},"date_updated":"2023-09-20T11:32:43Z","external_id":{"isi":["000440733400010"]},"isi":1,"day":"31","doi":"10.1007/978-3-662-54580-5_10","abstract":[{"lang":"eng","text":"Time-triggered switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. Due to the criticality of the applications running over them, developers need to ensure that end-to-end communication is dependable and predictable. Traditional approaches assume static networks that are not flexible to changes caused by reconfigurations or, more importantly, faults, which are dealt with in the application using redundancy. We adopt the concept of handling faults in the switches from non-real-time networks while maintaining the required predictability. \r\n\r\nWe study a class of forwarding schemes that can handle various types of failures. We consider probabilistic failures. We study a class of forwarding schemes that can handle various types of failures. We consider probabilistic failures. For a given network with a forwarding scheme and a constant ℓ, we compute the {\\em score} of the scheme, namely the probability (induced by faults) that at least ℓ messages arrive on time. We reduce the scoring problem to a reachability problem on a Markov chain with a &quot;product-like&quot; structure. Its special structure allows us to reason about it symbolically, and reduce the scoring problem to #SAT. Our solution is generic and can be adapted to different networks and other contexts. Also, we show the computational complexity of the scoring problem is #P-complete, and we study methods to estimate the score. We evaluate the effectiveness of our techniques with an implementation. "}],"quality_controlled":"1","page":"169 - 187","file_date_updated":"2018-12-12T10:08:37Z","publisher":"Springer","scopus_import":"1","_id":"1116","author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","first_name":"Guy","last_name":"Avni"},{"full_name":"Goel, Shubham","last_name":"Goel","first_name":"Shubham"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Guillermo","last_name":"Rodríguez Navas","full_name":"Rodríguez Navas, Guillermo"}],"date_created":"2018-12-11T11:50:14Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","publication_status":"published","intvolume":"     10206","title":"Computing scores of forwarding schemes in switched networks with probabilistic faults","alternative_title":["LNCS"],"pubrep_id":"758","file":[{"relation":"main_file","access_level":"open_access","file_id":"4698","creator":"system","date_created":"2018-12-12T10:08:37Z","file_size":321800,"date_updated":"2018-12-12T10:08:37Z","file_name":"IST-2017-758-v1+1_tacas-cr.pdf","content_type":"application/pdf"}],"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","type":"conference","date_published":"2017-03-31T00:00:00Z","publication_identifier":{"issn":["03029743"]},"oa":1,"publist_id":"6246","language":[{"iso":"eng"}],"conference":{"location":"Uppsala, Sweden","end_date":"2017-04-29","start_date":"2017-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"has_accepted_license":"1","project":[{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}],"oa_version":"Submitted Version","month":"03"},{"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","main_file_link":[{"url":"https://arxiv.org/abs/1705.02045","open_access":"1"}],"publist_id":"6815","oa":1,"publication_identifier":{"issn":["03029743"]},"date_published":"2017-07-28T00:00:00Z","type":"conference","conference":{"end_date":"2017-08-24","location":"Ystad, Sweden","start_date":"2017-08-22","name":"CAIP: Computer Analysis of Images and Patterns"},"language":[{"iso":"eng"}],"month":"07","oa_version":"Submitted Version","volume":10424,"abstract":[{"lang":"eng","text":"We present an efficient algorithm to compute Euler characteristic curves of gray scale images of arbitrary dimension. In various applications the Euler characteristic curve is used as a descriptor of an image. Our algorithm is the first streaming algorithm for Euler characteristic curves. The usage of streaming removes the necessity to store the entire image in RAM. Experiments show that our implementation handles terabyte scale images on commodity hardware. Due to lock-free parallelism, it scales well with the number of processor cores. Additionally, we put the concept of the Euler characteristic curve in the wider context of computational topology. In particular, we explain the connection with persistence diagrams."}],"doi":"10.1007/978-3-319-64689-3_32","day":"28","isi":1,"external_id":{"isi":["000432085900032"]},"date_updated":"2023-09-26T16:10:03Z","citation":{"ieee":"T. Heiss and H. Wagner, “Streaming algorithm for Euler characteristic curves of multidimensional images,” presented at the CAIP: Computer Analysis of Images and Patterns, Ystad, Sweden, 2017, vol. 10424, pp. 397–409.","chicago":"Heiss, Teresa, and Hubert Wagner. “Streaming Algorithm for Euler Characteristic Curves of Multidimensional Images.” edited by Michael Felsberg, Anders Heyden, and Norbert Krüger, 10424:397–409. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-64689-3_32\">https://doi.org/10.1007/978-3-319-64689-3_32</a>.","ama":"Heiss T, Wagner H. Streaming algorithm for Euler characteristic curves of multidimensional images. In: Felsberg M, Heyden A, Krüger N, eds. Vol 10424. Springer; 2017:397-409. doi:<a href=\"https://doi.org/10.1007/978-3-319-64689-3_32\">10.1007/978-3-319-64689-3_32</a>","apa":"Heiss, T., &#38; Wagner, H. (2017). Streaming algorithm for Euler characteristic curves of multidimensional images. In M. Felsberg, A. Heyden, &#38; N. Krüger (Eds.) (Vol. 10424, pp. 397–409). Presented at the CAIP: Computer Analysis of Images and Patterns, Ystad, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-319-64689-3_32\">https://doi.org/10.1007/978-3-319-64689-3_32</a>","ista":"Heiss T, Wagner H. 2017. Streaming algorithm for Euler characteristic curves of multidimensional images. CAIP: Computer Analysis of Images and Patterns, LNCS, vol. 10424, 397–409.","mla":"Heiss, Teresa, and Hubert Wagner. <i>Streaming Algorithm for Euler Characteristic Curves of Multidimensional Images</i>. Edited by Michael Felsberg et al., vol. 10424, Springer, 2017, pp. 397–409, doi:<a href=\"https://doi.org/10.1007/978-3-319-64689-3_32\">10.1007/978-3-319-64689-3_32</a>.","short":"T. Heiss, H. Wagner, in:, M. Felsberg, A. Heyden, N. Krüger (Eds.), Springer, 2017, pp. 397–409."},"year":"2017","publisher":"Springer","editor":[{"full_name":"Felsberg, Michael","last_name":"Felsberg","first_name":"Michael"},{"last_name":"Heyden","first_name":"Anders","full_name":"Heyden, Anders"},{"first_name":"Norbert","last_name":"Krüger","full_name":"Krüger, Norbert"}],"page":"397 - 409","quality_controlled":"1","title":"Streaming algorithm for Euler characteristic curves of multidimensional images","alternative_title":["LNCS"],"intvolume":"     10424","publication_status":"published","date_created":"2018-12-11T11:48:45Z","department":[{"_id":"HeEd"}],"article_processing_charge":"No","author":[{"full_name":"Heiss, Teresa","orcid":"0000-0002-1780-2689","last_name":"Heiss","first_name":"Teresa","id":"4879BB4E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Wagner, Hubert","first_name":"Hubert","last_name":"Wagner","id":"379CA8B8-F248-11E8-B48F-1D18A9856A87"}],"_id":"833","scopus_import":"1"},{"abstract":[{"text":"In this work we present a short and unified proof for the Strong and Weak Regularity Lemma, based on the cryptographic tech-nique called low-complexity approximations. In short, both problems reduce to a task of finding constructively an approximation for a certain target function under a class of distinguishers (test functions), where dis-tinguishers are combinations of simple rectangle-indicators. In our case these approximations can be learned by a simple iterative procedure, which yields a unified and simple proof, achieving for any graph with density d and any approximation parameter the partition size. The novelty in our proof is: (a) a simple approach which yields both strong and weaker variant, and (b) improvements when d = o(1). At an abstract level, our proof can be seen a refinement and simplification of the “analytic” proof given by Lovasz and Szegedy.","lang":"eng"}],"day":"01","doi":"10.1007/978-3-319-55911-7_42","citation":{"chicago":"Skórski, Maciej. “A Cryptographic View of Regularity Lemmas: Simpler Unified Proofs and Refined Bounds.” edited by Gerhard Jäger and Silvia Steila, 10185:586–99. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-55911-7_42\">https://doi.org/10.1007/978-3-319-55911-7_42</a>.","ieee":"M. Skórski, “A cryptographic view of regularity lemmas: Simpler unified proofs and refined bounds,” presented at the TAMC: Theory and Applications of Models of Computation, Bern, Switzerland, 2017, vol. 10185, pp. 586–599.","ama":"Skórski M. A cryptographic view of regularity lemmas: Simpler unified proofs and refined bounds. In: Jäger G, Steila S, eds. Vol 10185. Springer; 2017:586-599. doi:<a href=\"https://doi.org/10.1007/978-3-319-55911-7_42\">10.1007/978-3-319-55911-7_42</a>","apa":"Skórski, M. (2017). A cryptographic view of regularity lemmas: Simpler unified proofs and refined bounds. In G. Jäger &#38; S. Steila (Eds.) (Vol. 10185, pp. 586–599). Presented at the TAMC: Theory and Applications of Models of Computation, Bern, Switzerland: Springer. <a href=\"https://doi.org/10.1007/978-3-319-55911-7_42\">https://doi.org/10.1007/978-3-319-55911-7_42</a>","ista":"Skórski M. 2017. A cryptographic view of regularity lemmas: Simpler unified proofs and refined bounds. TAMC: Theory and Applications of Models of Computation, LNCS, vol. 10185, 586–599.","mla":"Skórski, Maciej. <i>A Cryptographic View of Regularity Lemmas: Simpler Unified Proofs and Refined Bounds</i>. Edited by Gerhard Jäger and Silvia Steila, vol. 10185, Springer, 2017, pp. 586–99, doi:<a href=\"https://doi.org/10.1007/978-3-319-55911-7_42\">10.1007/978-3-319-55911-7_42</a>.","short":"M. Skórski, in:, G. Jäger, S. Steila (Eds.), Springer, 2017, pp. 586–599."},"year":"2017","date_updated":"2021-01-12T08:07:46Z","volume":10185,"intvolume":"     10185","alternative_title":["LNCS"],"title":"A cryptographic view of regularity lemmas: Simpler unified proofs and refined bounds","date_created":"2018-12-11T11:47:42Z","department":[{"_id":"KrPi"}],"publication_status":"published","author":[{"full_name":"Skórski, Maciej","first_name":"Maciej","last_name":"Skórski","id":"EC09FA6A-02D0-11E9-8223-86B7C91467DD"}],"scopus_import":1,"_id":"650","editor":[{"first_name":"Gerhard","last_name":"Jäger","full_name":"Jäger, Gerhard"},{"first_name":"Silvia","last_name":"Steila","full_name":"Steila, Silvia"}],"publisher":"Springer","quality_controlled":"1","page":"586 - 599","publist_id":"7119","oa":1,"publication_identifier":{"issn":["03029743"]},"type":"conference","date_published":"2017-01-01T00:00:00Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","status":"public","main_file_link":[{"open_access":"1","url":"https://eprint.iacr.org/2016/965.pdf"}],"month":"01","oa_version":"Submitted Version","conference":{"end_date":"2017-04-22","location":"Bern, Switzerland","start_date":"2017-04-20","name":"TAMC: Theory and Applications of Models of Computation"},"language":[{"iso":"eng"}]},{"volume":10482,"ddc":["005"],"year":"2017","citation":{"ista":"Chatterjee K, Goharshady AK, Pavlogiannis A. 2017. JTDec: A tool for tree decompositions in soot. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 10482, 59–66.","mla":"Chatterjee, Krishnendu, et al. <i>JTDec: A Tool for Tree Decompositions in Soot</i>. Edited by Deepak D’Souza, vol. 10482, Springer, 2017, pp. 59–66, doi:<a href=\"https://doi.org/10.1007/978-3-319-68167-2_4\">10.1007/978-3-319-68167-2_4</a>.","short":"K. Chatterjee, A.K. Goharshady, A. Pavlogiannis, in:, D. D’Souza (Ed.), Springer, 2017, pp. 59–66.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. “JTDec: A Tool for Tree Decompositions in Soot.” edited by Deepak D’Souza, 10482:59–66. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-68167-2_4\">https://doi.org/10.1007/978-3-319-68167-2_4</a>.","ieee":"K. Chatterjee, A. K. Goharshady, and A. Pavlogiannis, “JTDec: A tool for tree decompositions in soot,” presented at the ATVA: Automated Technology for Verification and Analysis, Pune, India, 2017, vol. 10482, pp. 59–66.","apa":"Chatterjee, K., Goharshady, A. K., &#38; Pavlogiannis, A. (2017). JTDec: A tool for tree decompositions in soot. In D. D’Souza (Ed.) (Vol. 10482, pp. 59–66). Presented at the ATVA: Automated Technology for Verification and Analysis, Pune, India: Springer. <a href=\"https://doi.org/10.1007/978-3-319-68167-2_4\">https://doi.org/10.1007/978-3-319-68167-2_4</a>","ama":"Chatterjee K, Goharshady AK, Pavlogiannis A. JTDec: A tool for tree decompositions in soot. In: D’Souza D, ed. Vol 10482. Springer; 2017:59-66. doi:<a href=\"https://doi.org/10.1007/978-3-319-68167-2_4\">10.1007/978-3-319-68167-2_4</a>"},"date_updated":"2024-03-25T23:30:19Z","external_id":{"isi":["000723567800004"]},"isi":1,"day":"01","doi":"10.1007/978-3-319-68167-2_4","abstract":[{"lang":"eng","text":"The notion of treewidth of graphs has been exploited for faster algorithms for several problems arising in verification and program analysis. Moreover, various notions of balanced tree decompositions have been used for improved algorithms supporting dynamic updates and analysis of concurrent programs. In this work, we present a tool for constructing tree-decompositions of CFGs obtained from Java methods, which is implemented as an extension to the widely used Soot framework. The experimental results show that our implementation on real-world Java benchmarks is very efficient. Our tool also provides the first implementation for balancing tree-decompositions. In summary, we present the first tool support for exploiting treewidth in the static analysis problems on Java programs."}],"quality_controlled":"1","ec_funded":1,"page":"59 - 66","file_date_updated":"2020-07-14T12:48:16Z","editor":[{"full_name":"D'Souza, Deepak","last_name":"D'Souza","first_name":"Deepak"}],"publisher":"Springer","scopus_import":"1","_id":"949","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir","first_name":"Amir","last_name":"Goharshady"},{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:49:22Z","article_processing_charge":"No","publication_status":"published","intvolume":"     10482","pubrep_id":"845","alternative_title":["LNCS"],"title":"JTDec: A tool for tree decompositions in soot","file":[{"creator":"system","file_id":"4835","relation":"main_file","access_level":"open_access","file_name":"IST-2017-845-v1+1_2017_Chatterjee_JTDec.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:48:16Z","checksum":"a0d9f5f94dc594c4e71e78525c9942f1","file_size":948514,"date_created":"2018-12-12T10:10:45Z"}],"status":"public","related_material":{"record":[{"status":"public","id":"8934","relation":"dissertation_contains"}]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","type":"conference","date_published":"2017-01-01T00:00:00Z","publication_identifier":{"issn":["03029743"]},"oa":1,"publist_id":"6468","language":[{"iso":"eng"}],"conference":{"location":"Pune, India","end_date":"2017-10-06","name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2017-10-03"},"has_accepted_license":"1","project":[{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"oa_version":"Submitted Version","month":"01"},{"volume":10427,"doi":"10.1007/978-3-319-63390-9_21","day":"01","abstract":[{"lang":"eng","text":"We present a new algorithm for model counting of a class of string constraints. In addition to the classic operation of concatenation, our class includes some recursively defined operations such as Kleene closure, and replacement of substrings. Additionally, our class also includes length constraints on the string expressions, which means, by requiring reasoning about numbers, that we face a multi-sorted logic. In the end, our string constraints are motivated by their use in programming for web applications. Our algorithm comprises two novel features: the ability to use a technique of (1) partial derivatives for constraints that are already in a solved form, i.e. a form where its (string) satisfiability is clearly displayed, and (2) non-progression, where cyclic reasoning in the reduction process may be terminated (thus allowing for the algorithm to look elsewhere). Finally, we experimentally compare our model counter with two recent works on model counting of similar constraints, SMC [18] and ABC [5], to demonstrate its superior performance."}],"date_updated":"2023-09-22T09:58:02Z","citation":{"ista":"Trinh M, Chu DH, Jaffar J. 2017. Model counting for recursively-defined strings. CAV: Computer Aided Verification, LNCS, vol. 10427, 399–418.","mla":"Trinh, Minh, et al. <i>Model Counting for Recursively-Defined Strings</i>. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer, 2017, pp. 399–418, doi:<a href=\"https://doi.org/10.1007/978-3-319-63390-9_21\">10.1007/978-3-319-63390-9_21</a>.","short":"M. Trinh, D.H. Chu, J. Jaffar, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 399–418.","ieee":"M. Trinh, D. H. Chu, and J. Jaffar, “Model counting for recursively-defined strings,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10427, pp. 399–418.","chicago":"Trinh, Minh, Duc Hiep Chu, and Joxan Jaffar. “Model Counting for Recursively-Defined Strings.” edited by Rupak Majumdar and Viktor Kunčak, 10427:399–418. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63390-9_21\">https://doi.org/10.1007/978-3-319-63390-9_21</a>.","apa":"Trinh, M., Chu, D. H., &#38; Jaffar, J. (2017). Model counting for recursively-defined strings. In R. Majumdar &#38; V. Kunčak (Eds.) (Vol. 10427, pp. 399–418). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-63390-9_21\">https://doi.org/10.1007/978-3-319-63390-9_21</a>","ama":"Trinh M, Chu DH, Jaffar J. Model counting for recursively-defined strings. In: Majumdar R, Kunčak V, eds. Vol 10427. Springer; 2017:399-418. doi:<a href=\"https://doi.org/10.1007/978-3-319-63390-9_21\">10.1007/978-3-319-63390-9_21</a>"},"year":"2017","isi":1,"external_id":{"isi":["000431900900021"]},"publisher":"Springer","editor":[{"full_name":"Majumdar, Rupak","first_name":"Rupak","last_name":"Majumdar"},{"full_name":"Kunčak, Viktor","first_name":"Viktor","last_name":"Kunčak"}],"page":"399 - 418","quality_controlled":"1","publication_status":"published","department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2018-12-11T11:49:26Z","alternative_title":["LNCS"],"title":"Model counting for recursively-defined strings","intvolume":"     10427","_id":"962","scopus_import":"1","author":[{"full_name":"Trinh, Minh","first_name":"Minh","last_name":"Trinh"},{"id":"3598E630-F248-11E8-B48F-1D18A9856A87","first_name":"Duc Hiep","last_name":"Chu","full_name":"Chu, Duc Hiep"},{"first_name":"Joxan","last_name":"Jaffar","full_name":"Jaffar, Joxan"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","publication_identifier":{"issn":["03029743"]},"publist_id":"6443","date_published":"2017-01-01T00:00:00Z","type":"conference","conference":{"name":"CAV: Computer Aided Verification","start_date":"2017-07-24","end_date":"2017-07-28","location":"Heidelberg, Germany"},"language":[{"iso":"eng"}],"oa_version":"None","project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"month":"01"},{"volume":10201,"doi":"10.1007/978-3-662-54434-1_11","day":"19","abstract":[{"text":"Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly equivalent, are standard models for interprocedural analysis. Yet RSMs are more convenient as they (a) explicitly model function calls and returns, and (b) specify many natural parameters for algorithmic analysis, e.g., the number of entries and exits. We consider a general framework where RSM transitions are labeled from a semiring and path properties are algebraic with semiring operations, which can model, e.g., interprocedural reachability and dataflow analysis problems. Our main contributions are new algorithms for several fundamental problems. As compared to a direct translation of RSMs to PDSs and the best-known existing bounds of PDSs, our analysis algorithm improves the complexity for finite-height semirings (that subsumes reachability and standard dataflow properties). We further consider the problem of extracting distance values from the representation structures computed by our algorithm, and give efficient algorithms that distinguish the complexity of a one-time preprocessing from the complexity of each individual query. Another advantage of our algorithm is that our improvements carry over to the concurrent setting, where we improve the bestknown complexity for the context-bounded analysis of concurrent RSMs. Finally, we provide a prototype implementation that gives a significant speed-up on several benchmarks from the SLAM/SDV project.","lang":"eng"}],"date_updated":"2023-09-22T09:44:50Z","citation":{"ista":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. 2017. Faster algorithms for weighted recursive state machines. ESOP: European Symposium on Programming, LNCS, vol. 10201, 287–313.","mla":"Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Weighted Recursive State Machines</i>. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313, doi:<a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">10.1007/978-3-662-54434-1_11</a>.","short":"K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.), Springer, 2017, pp. 287–313.","chicago":"Chatterjee, Krishnendu, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis. “Faster Algorithms for Weighted Recursive State Machines.” edited by Hongseok Yang, 10201:287–313. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">https://doi.org/10.1007/978-3-662-54434-1_11</a>.","ieee":"K. Chatterjee, B. Kragl, S. Mishra, and A. Pavlogiannis, “Faster algorithms for weighted recursive state machines,” presented at the ESOP: European Symposium on Programming, Uppsala, Sweden, 2017, vol. 10201, pp. 287–313.","ama":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. Faster algorithms for weighted recursive state machines. In: Yang H, ed. Vol 10201. Springer; 2017:287-313. doi:<a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">10.1007/978-3-662-54434-1_11</a>","apa":"Chatterjee, K., Kragl, B., Mishra, S., &#38; Pavlogiannis, A. (2017). Faster algorithms for weighted recursive state machines. In H. Yang (Ed.) (Vol. 10201, pp. 287–313). Presented at the ESOP: European Symposium on Programming, Uppsala, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">https://doi.org/10.1007/978-3-662-54434-1_11</a>"},"year":"2017","isi":1,"external_id":{"isi":["000681702400011"]},"publisher":"Springer","editor":[{"full_name":"Yang, Hongseok","last_name":"Yang","first_name":"Hongseok"}],"page":"287 - 313","quality_controlled":"1","ec_funded":1,"publication_status":"published","date_created":"2018-12-11T11:49:41Z","article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"alternative_title":["LNCS"],"title":"Faster algorithms for weighted recursive state machines","intvolume":"     10201","_id":"1011","scopus_import":"1","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"320FC952-F248-11E8-B48F-1D18A9856A87","first_name":"Bernhard","last_name":"Kragl","orcid":"0000-0001-7745-9117","full_name":"Kragl, Bernhard"},{"full_name":"Mishra, Samarth","last_name":"Mishra","first_name":"Samarth"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas"}],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1701.04914"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","publication_identifier":{"issn":["03029743"]},"publist_id":"6384","oa":1,"date_published":"2017-03-19T00:00:00Z","type":"conference","conference":{"location":"Uppsala, Sweden","end_date":"2017-04-29","start_date":"2017-04-22","name":"ESOP: European Symposium on Programming"},"language":[{"iso":"eng"}],"oa_version":"Submitted Version","project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"month":"03"},{"publication_status":"published","date_created":"2018-12-11T11:49:34Z","department":[{"_id":"JaMa"}],"article_processing_charge":"No","title":"Transport based image morphing with intensity modulation","alternative_title":["LNCS"],"intvolume":"     10302","_id":"989","scopus_import":"1","author":[{"first_name":"Jan","last_name":"Maas","orcid":"0000-0002-0845-1338","full_name":"Maas, Jan","id":"4C5696CE-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Rumpf","first_name":"Martin","full_name":"Rumpf, Martin"},{"first_name":"Stefan","last_name":"Simon","full_name":"Simon, Stefan"}],"publisher":"Springer","editor":[{"first_name":"François","last_name":"Lauze","full_name":"Lauze, François"},{"full_name":"Dong, Yiqiu","last_name":"Dong","first_name":"Yiqiu"},{"full_name":"Bjorholm Dahl, Anders","first_name":"Anders","last_name":"Bjorholm Dahl"}],"page":"563 - 577","quality_controlled":"1","doi":"10.1007/978-3-319-58771-4_45","day":"18","abstract":[{"text":"We present a generalized optimal transport model in which the mass-preserving constraint for the L2-Wasserstein distance is relaxed by introducing a source term in the continuity equation. The source term is also incorporated in the path energy by means of its squared L2-norm in time of a functional with linear growth in space. This extension of the original transport model enables local density modulations, which is a desirable feature in applications such as image warping and blending. A key advantage of the use of a functional with linear growth in space is that it allows for singular sources and sinks, which can be supported on points or lines. On a technical level, the L2-norm in time ensures a disintegration of the source in time, which we use to obtain the well-posedness of the model and the existence of geodesic paths. The numerical discretization is based on the proximal splitting approach [18] and selected numerical test cases show the potential of the proposed approach. Furthermore, the approach is applied to the warping and blending of textures.","lang":"eng"}],"date_updated":"2023-09-22T09:55:50Z","citation":{"ista":"Maas J, Rumpf M, Simon S. 2017. Transport based image morphing with intensity modulation. SSVM:  Scale Space and Variational Methods in Computer Vision, LNCS, vol. 10302, 563–577.","short":"J. Maas, M. Rumpf, S. Simon, in:, F. Lauze, Y. Dong, A. Bjorholm Dahl (Eds.), Springer, 2017, pp. 563–577.","mla":"Maas, Jan, et al. <i>Transport Based Image Morphing with Intensity Modulation</i>. Edited by François Lauze et al., vol. 10302, Springer, 2017, pp. 563–77, doi:<a href=\"https://doi.org/10.1007/978-3-319-58771-4_45\">10.1007/978-3-319-58771-4_45</a>.","ieee":"J. Maas, M. Rumpf, and S. Simon, “Transport based image morphing with intensity modulation,” presented at the SSVM:  Scale Space and Variational Methods in Computer Vision, Kolding, Denmark, 2017, vol. 10302, pp. 563–577.","chicago":"Maas, Jan, Martin Rumpf, and Stefan Simon. “Transport Based Image Morphing with Intensity Modulation.” edited by François Lauze, Yiqiu Dong, and Anders Bjorholm Dahl, 10302:563–77. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-58771-4_45\">https://doi.org/10.1007/978-3-319-58771-4_45</a>.","ama":"Maas J, Rumpf M, Simon S. Transport based image morphing with intensity modulation. In: Lauze F, Dong Y, Bjorholm Dahl A, eds. Vol 10302. Springer; 2017:563-577. doi:<a href=\"https://doi.org/10.1007/978-3-319-58771-4_45\">10.1007/978-3-319-58771-4_45</a>","apa":"Maas, J., Rumpf, M., &#38; Simon, S. (2017). Transport based image morphing with intensity modulation. In F. Lauze, Y. Dong, &#38; A. Bjorholm Dahl (Eds.) (Vol. 10302, pp. 563–577). Presented at the SSVM:  Scale Space and Variational Methods in Computer Vision, Kolding, Denmark: Springer. <a href=\"https://doi.org/10.1007/978-3-319-58771-4_45\">https://doi.org/10.1007/978-3-319-58771-4_45</a>"},"year":"2017","isi":1,"external_id":{"isi":["000432210900045"]},"volume":10302,"oa_version":"None","month":"05","conference":{"start_date":"2017-06-04","name":"SSVM:  Scale Space and Variational Methods in Computer Vision","end_date":"2017-06-08","location":"Kolding, Denmark"},"language":[{"iso":"eng"}],"publication_identifier":{"issn":["03029743"]},"publist_id":"6410","date_published":"2017-05-18T00:00:00Z","type":"conference","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1"},{"date_published":"2011-08-01T00:00:00Z","type":"conference","oa":1,"publication_identifier":{"issn":["03029743"],"eissn":["16113349"],"isbn":["9783642236716"]},"status":"public","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","main_file_link":[{"open_access":"1","url":"http://hdl.handle.net/11441/30766"}],"publication":"Computer Analysis of Images and Patterns","month":"08","oa_version":"Published Version","language":[{"iso":"eng"}],"conference":{"start_date":"2011-08-29","name":"CAIP: International Conference on Computer Analysis of Images and Patterns","end_date":"2011-08-31","location":"Seville, Spain"},"date_updated":"2021-08-12T13:53:17Z","citation":{"mla":"Gonzalez-Diaz, Rocio, et al. “Incremental-Decremental Algorithm for Computing AT-Models and Persistent Homology.” <i>Computer Analysis of Images and Patterns</i>, vol. 6854, Springer Nature, 2011, pp. 286–93, doi:<a href=\"https://doi.org/10.1007/978-3-642-23672-3_35\">10.1007/978-3-642-23672-3_35</a>.","short":"R. Gonzalez-Diaz, A. Ion, M.J. Jimenez, R. Poyatos, in:, Computer Analysis of Images and Patterns, Springer Nature, 2011, pp. 286–293.","ista":"Gonzalez-Diaz R, Ion A, Jimenez MJ, Poyatos R. 2011. Incremental-decremental algorithm for computing AT-models and persistent homology. Computer Analysis of Images and Patterns. CAIP: International Conference on Computer Analysis of Images and Patterns, LNCS, vol. 6854, 286–293.","apa":"Gonzalez-Diaz, R., Ion, A., Jimenez, M. J., &#38; Poyatos, R. (2011). Incremental-decremental algorithm for computing AT-models and persistent homology. In <i>Computer Analysis of Images and Patterns</i> (Vol. 6854, pp. 286–293). Seville, Spain: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-642-23672-3_35\">https://doi.org/10.1007/978-3-642-23672-3_35</a>","ama":"Gonzalez-Diaz R, Ion A, Jimenez MJ, Poyatos R. Incremental-decremental algorithm for computing AT-models and persistent homology. In: <i>Computer Analysis of Images and Patterns</i>. Vol 6854. Springer Nature; 2011:286-293. doi:<a href=\"https://doi.org/10.1007/978-3-642-23672-3_35\">10.1007/978-3-642-23672-3_35</a>","chicago":"Gonzalez-Diaz, Rocio, Adrian Ion, Maria Jose Jimenez, and Regina Poyatos. “Incremental-Decremental Algorithm for Computing AT-Models and Persistent Homology.” In <i>Computer Analysis of Images and Patterns</i>, 6854:286–93. Springer Nature, 2011. <a href=\"https://doi.org/10.1007/978-3-642-23672-3_35\">https://doi.org/10.1007/978-3-642-23672-3_35</a>.","ieee":"R. Gonzalez-Diaz, A. Ion, M. J. Jimenez, and R. Poyatos, “Incremental-decremental algorithm for computing AT-models and persistent homology,” in <i>Computer Analysis of Images and Patterns</i>, Seville, Spain, 2011, vol. 6854, pp. 286–293."},"year":"2011","abstract":[{"lang":"eng","text":"In this paper, we establish a correspondence between the incremental algorithm for computing AT-models [8,9] and the one for computing persistent homology [6,14,15]. We also present a decremental algorithm for computing AT-models that allows to extend the persistence computation to a wider setting. Finally, we show how to combine incremental and decremental techniques for persistent homology computation."}],"doi":"10.1007/978-3-642-23672-3_35","day":"01","volume":6854,"author":[{"full_name":"Gonzalez-Diaz, Rocio","first_name":"Rocio","last_name":"Gonzalez-Diaz"},{"full_name":"Ion, Adrian","first_name":"Adrian","last_name":"Ion","id":"29F89302-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jimenez, Maria Jose","first_name":"Maria Jose","last_name":"Jimenez"},{"first_name":"Regina","last_name":"Poyatos","full_name":"Poyatos, Regina"}],"_id":"9648","scopus_import":"1","title":"Incremental-decremental algorithm for computing AT-models and persistent homology","alternative_title":["LNCS"],"intvolume":"      6854","publication_status":"published","article_processing_charge":"No","department":[{"_id":"HeEd"}],"date_created":"2021-07-11T22:01:19Z","page":"286-293","quality_controlled":"1","publisher":"Springer Nature"}]