[{"date_published":"2019-10-10T00:00:00Z","type":"conference","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)"},"oa":1,"publication_identifier":{"eissn":["2475-1421"]},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","status":"public","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"10199"}]},"file":[{"creator":"cchlebak","file_id":"10278","success":1,"relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"2019_ACM_Chatterjee.pdf","date_updated":"2021-11-12T11:41:56Z","checksum":"2149979c46964c4d117af06ccb6c0834","file_size":570829,"date_created":"2021-11-12T11:41:56Z"}],"main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/3360550","open_access":"1"}],"publication":"Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications","has_accepted_license":"1","month":"10","article_number":"124","oa_version":"Published Version","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"}],"language":[{"iso":"eng"}],"keyword":["safety","risk","reliability and quality","software"],"conference":{"location":"Athens, Greece","end_date":"2019-10-25","name":"OOPSLA: Object-oriented Programming, Systems, Languages and Applications","start_date":"2019-10-23"},"external_id":{"arxiv":["1909.00989"]},"date_updated":"2025-07-14T09:10:15Z","citation":{"mla":"Chatterjee, Krishnendu, et al. “Value-Centric Dynamic Partial Order Reduction.” <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>, vol. 3, 124, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3360550\">10.1145/3360550</a>.","short":"K. Chatterjee, A. Pavlogiannis, V. Toman, in:, Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, ACM, 2019.","ista":"Chatterjee K, Pavlogiannis A, Toman V. 2019. Value-centric dynamic partial order reduction. Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA: Object-oriented Programming, Systems, Languages and Applications vol. 3, 124.","ama":"Chatterjee K, Pavlogiannis A, Toman V. Value-centric dynamic partial order reduction. In: <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>. Vol 3. ACM; 2019. doi:<a href=\"https://doi.org/10.1145/3360550\">10.1145/3360550</a>","apa":"Chatterjee, K., Pavlogiannis, A., &#38; Toman, V. (2019). Value-centric dynamic partial order reduction. In <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i> (Vol. 3). Athens, Greece: ACM. <a href=\"https://doi.org/10.1145/3360550\">https://doi.org/10.1145/3360550</a>","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Viktor Toman. “Value-Centric Dynamic Partial Order Reduction.” In <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>, Vol. 3. ACM, 2019. <a href=\"https://doi.org/10.1145/3360550\">https://doi.org/10.1145/3360550</a>.","ieee":"K. Chatterjee, A. Pavlogiannis, and V. Toman, “Value-centric dynamic partial order reduction,” in <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>, Athens, Greece, 2019, vol. 3."},"year":"2019","abstract":[{"lang":"eng","text":"The verification of concurrent programs remains an open challenge, as thread interaction has to be accounted for, which leads to state-space explosion. Stateless model checking battles this problem by exploring traces rather than states of the program. As there are exponentially many traces, dynamic partial-order reduction (DPOR) techniques are used to partition the trace space into equivalence classes, and explore a few representatives from each class. The standard equivalence that underlies most DPOR techniques is the happens-before equivalence, however recent works have spawned a vivid interest towards coarser equivalences. The efficiency of such approaches is a product of two parameters: (i) the size of the partitioning induced by the equivalence, and (ii) the time spent by the exploration algorithm in each class of the partitioning. In this work, we present a new equivalence, called value-happens-before and show that it has two appealing features. First, value-happens-before is always at least as coarse as the happens-before equivalence, and can be even exponentially coarser. Second, the value-happens-before partitioning is efficiently explorable when the number of threads is bounded. We present an algorithm called value-centric DPOR (VCDPOR), which explores the underlying partitioning using polynomial time per class. Finally, we perform an experimental evaluation of VCDPOR on various benchmarks, and compare it against other state-of-the-art approaches. Our results show that value-happens-before typically induces a significant reduction in the size of the underlying partitioning, which leads to a considerable reduction in the running time for exploring the whole partitioning."}],"arxiv":1,"doi":"10.1145/3360550","day":"10","ddc":["000"],"volume":3,"acknowledgement":"The authors would also like to thank anonymous referees for their valuable comments and helpful suggestions. This work is supported by the Austrian Science Fund (FWF) NFN grants S11407-N23 (RiSE/SHiNE) and S11402-N23 (RiSE/SHiNE), by the Vienna Science and Technology Fund (WWTF) Project ICT15-003, and by the Austrian Science Fund (FWF) Schrodinger grant J-4220.\r\n","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Toman, Viktor","orcid":"0000-0001-9036-063X","last_name":"Toman","first_name":"Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87"}],"_id":"10190","title":"Value-centric dynamic partial order reduction","intvolume":"         3","publication_status":"published","date_created":"2021-10-27T14:57:06Z","article_processing_charge":"No","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"file_date_updated":"2021-11-12T11:41:56Z","quality_controlled":"1","publisher":"ACM"},{"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","file":[{"creator":"dernst","file_id":"8638","access_level":"open_access","success":1,"relation":"main_file","file_name":"2018_LNCS_Elgyuett.pdf","content_type":"application/pdf","date_updated":"2020-10-09T06:24:21Z","file_size":537219,"checksum":"e5d81c9b50a6bd9d8a2c16953aad7e23","date_created":"2020-10-09T06:24:21Z"}],"date_published":"2018-08-26T00:00:00Z","type":"conference","publist_id":"7973","oa":1,"language":[{"iso":"eng"}],"conference":{"location":"Beijing, China","end_date":"2018-09-06","start_date":"2018-09-04","name":"FORMATS: Formal Modeling and Analysis of Timed Systems"},"has_accepted_license":"1","month":"08","oa_version":"Submitted Version","project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}],"ddc":["000"],"volume":11022,"isi":1,"external_id":{"isi":["000884993200004"]},"date_updated":"2023-09-13T08:58:34Z","citation":{"chicago":"Elgyütt, Adrian, Thomas Ferrere, and Thomas A Henzinger. “Monitoring Temporal Logic with Clock Variables,” 11022:53–70. Springer, 2018. <a href=\"https://doi.org/10.1007/978-3-030-00151-3_4\">https://doi.org/10.1007/978-3-030-00151-3_4</a>.","ieee":"A. Elgyütt, T. Ferrere, and T. A. Henzinger, “Monitoring temporal logic with clock variables,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Beijing, China, 2018, vol. 11022, pp. 53–70.","ama":"Elgyütt A, Ferrere T, Henzinger TA. Monitoring temporal logic with clock variables. In: Vol 11022. Springer; 2018:53-70. doi:<a href=\"https://doi.org/10.1007/978-3-030-00151-3_4\">10.1007/978-3-030-00151-3_4</a>","apa":"Elgyütt, A., Ferrere, T., &#38; Henzinger, T. A. (2018). Monitoring temporal logic with clock variables (Vol. 11022, pp. 53–70). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Beijing, China: Springer. <a href=\"https://doi.org/10.1007/978-3-030-00151-3_4\">https://doi.org/10.1007/978-3-030-00151-3_4</a>","ista":"Elgyütt A, Ferrere T, Henzinger TA. 2018. Monitoring temporal logic with clock variables. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 11022, 53–70.","short":"A. Elgyütt, T. Ferrere, T.A. Henzinger, in:, Springer, 2018, pp. 53–70.","mla":"Elgyütt, Adrian, et al. <i>Monitoring Temporal Logic with Clock Variables</i>. Vol. 11022, Springer, 2018, pp. 53–70, doi:<a href=\"https://doi.org/10.1007/978-3-030-00151-3_4\">10.1007/978-3-030-00151-3_4</a>."},"year":"2018","abstract":[{"lang":"eng","text":"We solve the offline monitoring problem for timed propositional temporal logic (TPTL), interpreted over dense-time Boolean signals. The variant of TPTL we consider extends linear temporal logic (LTL) with clock variables and reset quantifiers, providing a mechanism to specify real-time constraints. We first describe a general monitoring algorithm based on an exhaustive computation of the set of satisfying clock assignments as a finite union of zones. We then propose a specialized monitoring algorithm for the one-variable case using a partition of the time domain based on the notion of region equivalence, whose complexity is linear in the length of the signal, thereby generalizing a known result regarding the monitoring of metric temporal logic (MTL). The region and zone representations of time constraints are known from timed automata verification and can also be used in the discrete-time case. Our prototype implementation appears to outperform previous discrete-time implementations of TPTL monitoring,"}],"doi":"10.1007/978-3-030-00151-3_4","day":"26","file_date_updated":"2020-10-09T06:24:21Z","page":"53 - 70","quality_controlled":"1","publisher":"Springer","author":[{"id":"4A2E9DBA-F248-11E8-B48F-1D18A9856A87","first_name":"Adrian","last_name":"Elgyütt","full_name":"Elgyütt, Adrian"},{"last_name":"Ferrere","first_name":"Thomas","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"_id":"81","scopus_import":"1","title":"Monitoring temporal logic with clock variables","alternative_title":["LNCS"],"intvolume":"     11022","publication_status":"published","date_created":"2018-12-11T11:44:31Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No"},{"month":"08","article_number":"21","oa_version":"Published Version","project":[{"name":"Rigorous Systems Engineering","grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"}],"has_accepted_license":"1","conference":{"location":"Beijing, China","end_date":"2018-09-07","start_date":"2018-09-04","name":"CONCUR: International Conference on Concurrency Theory"},"language":[{"iso":"eng"}],"publist_id":"7790","oa":1,"publication_identifier":{"issn":["18688969"]},"date_published":"2018-08-13T00:00:00Z","type":"conference","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)"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"6426"},{"id":"8332","relation":"dissertation_contains","status":"public"}]},"status":"public","file":[{"date_created":"2018-12-12T10:18:46Z","checksum":"c90895f4c5fafc18ddc54d1c8848077e","file_size":745438,"date_updated":"2020-07-14T12:44:44Z","file_name":"IST-2018-853-v2+2_concur2018.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"5368","creator":"system"}],"pubrep_id":"1039","alternative_title":["LIPIcs"],"title":"Synchronizing the asynchronous","intvolume":"       118","publication_status":"published","date_created":"2018-12-11T11:44:48Z","department":[{"_id":"ToHe"}],"author":[{"id":"320FC952-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7745-9117","full_name":"Kragl, Bernhard","first_name":"Bernhard","last_name":"Kragl"},{"full_name":"Qadeer, Shaz","last_name":"Qadeer","first_name":"Shaz"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"_id":"133","scopus_import":1,"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file_date_updated":"2020-07-14T12:44:44Z","quality_controlled":"1","abstract":[{"lang":"eng","text":"Synchronous programs are easy to specify because the side effects of an operation are finished by the time the invocation of the operation returns to the caller. Asynchronous programs, on the other hand, are difficult to specify because there are side effects due to pending computation scheduled as a result of the invocation of an operation. They are also difficult to verify because of the large number of possible interleavings of concurrent computation threads. We present synchronization, a new proof rule that simplifies the verification of asynchronous programs by introducing the fiction, for proof purposes, that asynchronous operations complete synchronously. Synchronization summarizes an asynchronous computation as immediate atomic effect. Modular verification is enabled via pending asynchronous calls in atomic summaries, and a complementary proof rule that eliminates pending asynchronous calls when components and their specifications are composed. We evaluate synchronization in the context of a multi-layer refinement verification methodology on a collection of benchmark programs."}],"doi":"10.4230/LIPIcs.CONCUR.2018.21","day":"13","date_updated":"2023-09-07T13:18:00Z","year":"2018","citation":{"ista":"Kragl B, Qadeer S, Henzinger TA. 2018. Synchronizing the asynchronous. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 118, 21.","short":"B. Kragl, S. Qadeer, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","mla":"Kragl, Bernhard, et al. <i>Synchronizing the Asynchronous</i>. Vol. 118, 21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.21\">10.4230/LIPIcs.CONCUR.2018.21</a>.","chicago":"Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Synchronizing the Asynchronous,” Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2018.21</a>.","ieee":"B. Kragl, S. Qadeer, and T. A. Henzinger, “Synchronizing the asynchronous,” presented at the CONCUR: International Conference on Concurrency Theory, Beijing, China, 2018, vol. 118.","ama":"Kragl B, Qadeer S, Henzinger TA. Synchronizing the asynchronous. In: Vol 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.21\">10.4230/LIPIcs.CONCUR.2018.21</a>","apa":"Kragl, B., Qadeer, S., &#38; Henzinger, T. A. (2018). Synchronizing the asynchronous (Vol. 118). Presented at the CONCUR: International Conference on Concurrency Theory, Beijing, China: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2018.21</a>"},"ddc":["000"],"volume":118},{"project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","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"}],"oa_version":"Published Version","month":"07","has_accepted_license":"1","conference":{"name":"CAV: Computer Aided Verification","start_date":"2018-07-14","location":"Oxford, United Kingdom","end_date":"2018-07-17"},"language":[{"iso":"eng"}],"publication_identifier":{"issn":["03029743"]},"publist_id":"7783","oa":1,"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)"},"type":"conference","date_published":"2018-07-18T00:00:00Z","file":[{"date_created":"2018-12-12T10:17:53Z","file_size":563710,"checksum":"6dca832f575d6b3f0ea9dff56f579142","date_updated":"2020-07-14T12:44:50Z","content_type":"application/pdf","file_name":"IST-2018-1010-v1+1_space-time_interpolants.pdf","relation":"main_file","access_level":"open_access","file_id":"5310","creator":"system"}],"status":"public","related_material":{"record":[{"id":"6894","relation":"dissertation_contains","status":"public"}]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_created":"2018-12-11T11:44:50Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","publication_status":"published","intvolume":"     10981","alternative_title":["LNCS"],"pubrep_id":"1010","title":"Space-time interpolants","scopus_import":"1","_id":"140","author":[{"full_name":"Frehse, Goran","last_name":"Frehse","first_name":"Goran"},{"id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","full_name":"Giacobbe, Mirco","orcid":"0000-0001-8180-0904","last_name":"Giacobbe","first_name":"Mirco"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"publisher":"Springer","quality_controlled":"1","page":"468 - 486","file_date_updated":"2020-07-14T12:44:50Z","day":"18","doi":"10.1007/978-3-319-96145-3_25","abstract":[{"lang":"eng","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."}],"year":"2018","citation":{"ista":"Frehse G, Giacobbe M, Henzinger TA. 2018. Space-time interpolants. CAV: Computer Aided Verification, LNCS, vol. 10981, 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>.","short":"G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2018, 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>.","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.","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>"},"date_updated":"2023-09-19T09:30:43Z","external_id":{"isi":["000491481600025"]},"isi":1,"volume":10981,"ddc":["005"]},{"publication_identifier":{"issn":["03029743"]},"oa":1,"publist_id":"6246","type":"conference","date_published":"2017-03-31T00:00:00Z","file":[{"file_size":321800,"date_created":"2018-12-12T10:08:37Z","content_type":"application/pdf","file_name":"IST-2017-758-v1+1_tacas-cr.pdf","date_updated":"2018-12-12T10:08:37Z","access_level":"open_access","relation":"main_file","creator":"system","file_id":"4698"}],"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","project":[{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"oa_version":"Submitted Version","month":"03","has_accepted_license":"1","conference":{"start_date":"2017-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Uppsala, Sweden","end_date":"2017-04-29"},"language":[{"iso":"eng"}],"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. "}],"citation":{"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.","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."},"year":"2017","date_updated":"2023-09-20T11:32:43Z","external_id":{"isi":["000440733400010"]},"isi":1,"volume":10206,"ddc":["000"],"department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2018-12-11T11:50:14Z","publication_status":"published","intvolume":"     10206","alternative_title":["LNCS"],"pubrep_id":"758","title":"Computing scores of forwarding schemes in switched networks with probabilistic faults","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","first_name":"Shubham","last_name":"Goel"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Rodríguez Navas","first_name":"Guillermo","full_name":"Rodríguez Navas, Guillermo"}],"publisher":"Springer","quality_controlled":"1","page":"169 - 187","file_date_updated":"2018-12-12T10:08:37Z"},{"ddc":["004"],"volume":13,"abstract":[{"text":"The edit distance between two words w 1 , w 2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the edit distance from L 1 to L 2 is the minimal number k such that for every word from L 1 there exists a word in L 2 with edit distance at most k . We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for the following problems: (1) deciding whether, for a given threshold k , the edit distance from a pushdown automaton to a finite automaton is at most k , and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite. ","lang":"eng"}],"day":"13","doi":"10.23638/LMCS-13(3:23)2017","year":"2017","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2017. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>.","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3. International Federation of Computational Logic, 2017.","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2017). Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. 2017;13(3). doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for pushdown automata. Logical Methods in Computer Science. 13(3).","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017).","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3, International Federation of Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>."},"date_updated":"2023-02-23T12:26:25Z","publisher":"International Federation of Computational Logic","file_date_updated":"2020-07-14T12:46:33Z","quality_controlled":"1","ec_funded":1,"intvolume":"        13","pubrep_id":"955","title":"Edit distance for pushdown automata","date_created":"2018-12-11T11:46:37Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","issue":"3","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop"}],"scopus_import":1,"_id":"465","related_material":{"record":[{"id":"1610","relation":"earlier_version","status":"public"},{"relation":"earlier_version","id":"5438","status":"public"}]},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"file_name":"IST-2015-321-v1+1_main.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:46:33Z","file_size":279071,"checksum":"08041379ba408d40664f449eb5907a8f","date_created":"2018-12-12T10:14:37Z","creator":"system","file_id":"5090","access_level":"open_access","relation":"main_file"},{"checksum":"08041379ba408d40664f449eb5907a8f","file_size":279071,"date_created":"2018-12-12T10:14:38Z","file_name":"IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:46:33Z","relation":"main_file","access_level":"open_access","creator":"system","file_id":"5091"}],"oa":1,"publist_id":"7356","publication_identifier":{"issn":["18605974"]},"type":"journal_article","date_published":"2017-09-13T00:00:00Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)"},"language":[{"iso":"eng"}],"month":"09","project":[{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-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"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"oa_version":"Published Version","has_accepted_license":"1","publication":"Logical Methods in Computer Science"},{"_id":"471","scopus_import":1,"author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","last_name":"Daca","first_name":"Przemyslaw","full_name":"Daca, Przemyslaw"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905","full_name":"Petrov, Tatjana","first_name":"Tatjana","last_name":"Petrov"}],"issue":"2","publication_status":"published","date_created":"2018-12-11T11:46:39Z","department":[{"_id":"ToHe"}],"title":"Faster statistical model checking for unbounded temporal properties","intvolume":"        18","ec_funded":1,"quality_controlled":"1","publisher":"ACM","date_updated":"2023-02-21T16:48:11Z","citation":{"short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational Logic (TOCL) 18 (2017).","mla":"Daca, Przemyslaw, et al. “Faster Statistical Model Checking for Unbounded Temporal Properties.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 2, 12, ACM, 2017, doi:<a href=\"https://doi.org/10.1145/3060139\">10.1145/3060139</a>.","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2017. Faster statistical model checking for unbounded temporal properties. ACM Transactions on Computational Logic (TOCL). 18(2), 12.","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2017). Faster statistical model checking for unbounded temporal properties. <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href=\"https://doi.org/10.1145/3060139\">https://doi.org/10.1145/3060139</a>","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking for unbounded temporal properties. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2017;18(2). doi:<a href=\"https://doi.org/10.1145/3060139\">10.1145/3060139</a>","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Faster Statistical Model Checking for Unbounded Temporal Properties.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3060139\">https://doi.org/10.1145/3060139</a>.","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical model checking for unbounded temporal properties,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 2. ACM, 2017."},"year":"2017","doi":"10.1145/3060139","day":"01","abstract":[{"text":"We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds. ","lang":"eng"}],"volume":18,"publication":"ACM Transactions on Computational Logic (TOCL)","oa_version":"Submitted Version","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}],"month":"05","article_number":"12","language":[{"iso":"eng"}],"date_published":"2017-05-01T00:00:00Z","type":"journal_article","publication_identifier":{"issn":["15293785"]},"oa":1,"publist_id":"7349","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.05739"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1234"}]}},{"doi":"10.4204/EPTCS.259.3","day":"10","abstract":[{"text":"Model checking is usually based on a comprehensive traversal of the state space. Causality-based model checking is a radically different approach that instead analyzes the cause-effect relationships in a program. We give an overview on a new class of model checking algorithms that capture the causal relationships in a special data structure called concurrent traces. Concurrent traces identify key events in an execution history and link them through their cause-effect relationships. The model checker builds a tableau of concurrent traces, where the case splits represent different causal explanations of a hypothetical error. Causality-based model checking has been implemented in the ARCTOR tool, and applied to previously intractable multi-threaded benchmarks.","lang":"eng"}],"date_updated":"2023-10-17T12:02:46Z","citation":{"mla":"Finkbeiner, Bernd, and Andrey Kupriyanov. “Causality-Based Model Checking.” <i>Electronic Proceedings in Theoretical Computer Science</i>, vol. 259, Open Publishing Association, 2017, pp. 31–38, doi:<a href=\"https://doi.org/10.4204/EPTCS.259.3\">10.4204/EPTCS.259.3</a>.","short":"B. Finkbeiner, A. Kupriyanov, in:, Electronic Proceedings in Theoretical Computer Science, Open Publishing Association, 2017, pp. 31–38.","ista":"Finkbeiner B, Kupriyanov A. 2017. Causality-based model checking. Electronic Proceedings in Theoretical Computer Science. CREST: Causal Reasoning for Embedded and Safety-Critical Systems Technologies, EPTCS, vol. 259, 31–38.","ama":"Finkbeiner B, Kupriyanov A. Causality-based model checking. In: <i>Electronic Proceedings in Theoretical Computer Science</i>. Vol 259. Open Publishing Association; 2017:31-38. doi:<a href=\"https://doi.org/10.4204/EPTCS.259.3\">10.4204/EPTCS.259.3</a>","apa":"Finkbeiner, B., &#38; Kupriyanov, A. (2017). Causality-based model checking. In <i>Electronic Proceedings in Theoretical Computer Science</i> (Vol. 259, pp. 31–38). Uppsala, Sweden: Open Publishing Association. <a href=\"https://doi.org/10.4204/EPTCS.259.3\">https://doi.org/10.4204/EPTCS.259.3</a>","ieee":"B. Finkbeiner and A. Kupriyanov, “Causality-based model checking,” in <i>Electronic Proceedings in Theoretical Computer Science</i>, Uppsala, Sweden, 2017, vol. 259, pp. 31–38.","chicago":"Finkbeiner, Bernd, and Andrey Kupriyanov. “Causality-Based Model Checking.” In <i>Electronic Proceedings in Theoretical Computer Science</i>, 259:31–38. Open Publishing Association, 2017. <a href=\"https://doi.org/10.4204/EPTCS.259.3\">https://doi.org/10.4204/EPTCS.259.3</a>."},"year":"2017","volume":259,"ddc":["004"],"publication_status":"published","date_created":"2018-12-11T11:47:07Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","title":"Causality-based model checking","pubrep_id":"925","alternative_title":["EPTCS"],"intvolume":"       259","_id":"549","scopus_import":"1","author":[{"first_name":"Bernd","last_name":"Finkbeiner","full_name":"Finkbeiner, Bernd"},{"id":"2C311BF8-F248-11E8-B48F-1D18A9856A87","full_name":"Kupriyanov, Andrey","last_name":"Kupriyanov","first_name":"Andrey"}],"publisher":"Open Publishing Association","page":"31 - 38","quality_controlled":"1","file_date_updated":"2020-07-14T12:47:00Z","publication_identifier":{"issn":["2075-2180"]},"oa":1,"publist_id":"7264","date_published":"2017-10-10T00:00:00Z","type":"conference","main_file_link":[{"url":"https://arxiv.org/abs/1710.03391v1","open_access":"1"}],"file":[{"creator":"system","file_id":"4939","access_level":"open_access","relation":"main_file","file_name":"IST-2018-925-v1+1_1710.03391v1.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:47:00Z","file_size":209294,"checksum":"6274f6c0da3376a7b079180d81568518","date_created":"2018-12-12T10:12:21Z"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Submitted Version","project":[{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"month":"10","publication":"Electronic Proceedings in Theoretical Computer Science","has_accepted_license":"1","conference":{"end_date":"2017-04-29","location":"Uppsala, Sweden","start_date":"2017-04-29","name":"CREST: Causal Reasoning for Embedded and Safety-Critical Systems Technologies"},"language":[{"iso":"eng"}]},{"title":"The cost of exactness in quantitative reachability","alternative_title":["LNCS"],"intvolume":"     10460","publication_status":"published","date_created":"2018-12-11T11:47:34Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"article_processing_charge":"No","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"_id":"625","scopus_import":"1","publisher":"Springer","editor":[{"last_name":"Aceto","first_name":"Luca","full_name":"Aceto, Luca"},{"last_name":"Bacci","first_name":"Giorgio","full_name":"Bacci, Giorgio"},{"last_name":"Ingólfsdóttir","first_name":"Anna","full_name":"Ingólfsdóttir, Anna"},{"last_name":"Legay","first_name":"Axel","full_name":"Legay, Axel"},{"first_name":"Radu","last_name":"Mardare","full_name":"Mardare, Radu"}],"file_date_updated":"2020-07-14T12:47:25Z","page":"367 - 381","series_title":"Theoretical Computer Science and General Issues","ec_funded":1,"quality_controlled":"1","abstract":[{"lang":"eng","text":"In the analysis of reactive systems a quantitative objective assigns a real value to every trace of the system. The value decision problem for a quantitative objective requires a trace whose value is at least a given threshold, and the exact value decision problem requires a trace whose value is exactly the threshold. We compare the computational complexity of the value and exact value decision problems for classical quantitative objectives, such as sum, discounted sum, energy, and mean-payoff for two standard models of reactive systems, namely, graphs and graph games."}],"doi":"10.1007/978-3-319-63121-9_18","day":"25","date_updated":"2025-06-02T08:53:45Z","year":"2017","citation":{"ista":"Chatterjee K, Doyen L, Henzinger TA. 2017.The cost of exactness in quantitative reachability. In: Models, Algorithms, Logics and Tools. LNCS, vol. 10460, 367–381.","mla":"Chatterjee, Krishnendu, et al. “The Cost of Exactness in Quantitative Reachability.” <i>Models, Algorithms, Logics and Tools</i>, edited by Luca Aceto et al., vol. 10460, Springer, 2017, pp. 367–81, doi:<a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">10.1007/978-3-319-63121-9_18</a>.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, R. Mardare (Eds.), Models, Algorithms, Logics and Tools, Springer, 2017, pp. 367–381.","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “The cost of exactness in quantitative reachability,” in <i>Models, Algorithms, Logics and Tools</i>, vol. 10460, L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, and R. Mardare, Eds. Springer, 2017, pp. 367–381.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “The Cost of Exactness in Quantitative Reachability.” In <i>Models, Algorithms, Logics and Tools</i>, edited by Luca Aceto, Giorgio Bacci, Anna Ingólfsdóttir, Axel Legay, and Radu Mardare, 10460:367–81. Theoretical Computer Science and General Issues. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">https://doi.org/10.1007/978-3-319-63121-9_18</a>.","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2017). The cost of exactness in quantitative reachability. In L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, &#38; R. Mardare (Eds.), <i>Models, Algorithms, Logics and Tools</i> (Vol. 10460, pp. 367–381). Springer. <a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">https://doi.org/10.1007/978-3-319-63121-9_18</a>","ama":"Chatterjee K, Doyen L, Henzinger TA. The cost of exactness in quantitative reachability. In: Aceto L, Bacci G, Ingólfsdóttir A, Legay A, Mardare R, eds. <i>Models, Algorithms, Logics and Tools</i>. Vol 10460. Theoretical Computer Science and General Issues. Springer; 2017:367-381. doi:<a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">10.1007/978-3-319-63121-9_18</a>"},"ddc":["000"],"volume":10460,"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 and S11407-N23 (RiSE/SHiNE), and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund (WWTF) through project ICT15-003.","month":"07","oa_version":"Submitted Version","project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"publication":"Models, Algorithms, Logics and Tools","has_accepted_license":"1","language":[{"iso":"eng"}],"oa":1,"publist_id":"7170","publication_identifier":{"isbn":["978-3-319-63120-2"],"issn":["0302-9743"]},"date_published":"2017-07-25T00:00:00Z","type":"book_chapter","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"creator":"dernst","file_id":"7048","relation":"main_file","access_level":"open_access","file_name":"2017_ModelsAlgorithms_Chatterjee.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:47:25Z","checksum":"b2402766ec02c79801aac634bd8f9f6c","file_size":192826,"date_created":"2019-11-19T08:06:50Z"}]},{"language":[{"iso":"eng"}],"conference":{"end_date":"2017-04-29","location":"Uppsala, Sweden","start_date":"2017-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"has_accepted_license":"1","month":"03","project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}],"oa_version":"Submitted Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"6894"}]},"file":[{"creator":"system","file_id":"4897","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"IST-2017-741-v1+1_main.pdf","date_updated":"2020-07-14T12:47:27Z","file_size":569863,"checksum":"f395d0d20102b89aeaad8b4ef4f18f4f","date_created":"2018-12-12T10:11:41Z"},{"date_updated":"2020-07-14T12:47:27Z","content_type":"application/pdf","file_name":"IST-2018-741-v2+2_main.pdf","date_created":"2018-12-12T10:11:42Z","checksum":"f416ee1ae4497b23ecdf28b1f18bb8df","file_size":563276,"file_id":"4898","creator":"system","access_level":"open_access","relation":"main_file"}],"type":"conference","date_published":"2017-03-31T00:00:00Z","oa":1,"publist_id":"7162","publication_identifier":{"isbn":["978-366254576-8"]},"file_date_updated":"2020-07-14T12:47:27Z","quality_controlled":"1","page":"589 - 606","publisher":"Springer","author":[{"first_name":"Sergiy","last_name":"Bogomolov","orcid":"0000-0002-0686-0365","full_name":"Bogomolov, Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Frehse, Goran","first_name":"Goran","last_name":"Frehse"},{"last_name":"Giacobbe","first_name":"Mirco","full_name":"Giacobbe, Mirco","orcid":"0000-0001-8180-0904","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"}],"scopus_import":1,"_id":"631","intvolume":"     10205","pubrep_id":"966","alternative_title":["LNCS"],"title":"Counterexample guided refinement of template polyhedra","date_created":"2018-12-11T11:47:36Z","department":[{"_id":"ToHe"}],"publication_status":"published","ddc":["000"],"volume":10205,"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), by the European Commission under grant 643921 (UnCoVerCPS), and by the ARC project DP140104219 (Robust AI Planning for Hybrid Systems).","year":"2017","citation":{"apa":"Bogomolov, S., Frehse, G., Giacobbe, M., &#38; Henzinger, T. A. (2017). Counterexample guided refinement of template polyhedra (Vol. 10205, pp. 589–606). 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-54577-5_34\">https://doi.org/10.1007/978-3-662-54577-5_34</a>","ama":"Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. Counterexample guided refinement of template polyhedra. In: Vol 10205. Springer; 2017:589-606. doi:<a href=\"https://doi.org/10.1007/978-3-662-54577-5_34\">10.1007/978-3-662-54577-5_34</a>","ieee":"S. Bogomolov, G. Frehse, M. Giacobbe, and T. A. Henzinger, “Counterexample guided refinement of template polyhedra,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden, 2017, vol. 10205, pp. 589–606.","chicago":"Bogomolov, Sergiy, Goran Frehse, Mirco Giacobbe, and Thomas A Henzinger. “Counterexample Guided Refinement of Template Polyhedra,” 10205:589–606. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-662-54577-5_34\">https://doi.org/10.1007/978-3-662-54577-5_34</a>.","mla":"Bogomolov, Sergiy, et al. <i>Counterexample Guided Refinement of Template Polyhedra</i>. Vol. 10205, Springer, 2017, pp. 589–606, doi:<a href=\"https://doi.org/10.1007/978-3-662-54577-5_34\">10.1007/978-3-662-54577-5_34</a>.","short":"S. Bogomolov, G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2017, pp. 589–606.","ista":"Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. 2017. Counterexample guided refinement of template polyhedra. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10205, 589–606."},"date_updated":"2023-09-07T12:53:00Z","abstract":[{"text":"Template polyhedra generalize intervals and octagons to polyhedra whose facets are orthogonal to a given set of arbitrary directions. They have been employed in the abstract interpretation of programs and, with particular success, in the reachability analysis of hybrid automata. While previously, the choice of directions has been left to the user or a heuristic, we present a method for the automatic discovery of directions that generalize and eliminate spurious counterexamples. We show that for the class of convex hybrid automata, i.e., hybrid automata with (possibly nonlinear) convex constraints on derivatives, such directions always exist and can be found using convex optimization. We embed our method inside a CEGAR loop, thus enabling the time-unbounded reachability analysis of an important and richer class of hybrid automata than was previously possible. We evaluate our method on several benchmarks, demonstrating also its superior efficiency for the special case of linear hybrid automata.","lang":"eng"}],"day":"31","doi":"10.1007/978-3-662-54577-5_34"},{"conference":{"start_date":"2017-07-22","name":"NSV: Numerical Software Verification","location":"Heidelberg, Germany","end_date":"2017-07-23"},"language":[{"iso":"eng"}],"project":[{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}],"oa_version":"None","month":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","publication_identifier":{"isbn":["978-331963500-2"]},"publist_id":"7159","type":"conference","date_published":"2017-01-01T00:00:00Z","editor":[{"full_name":"Abate, Alessandro","first_name":"Alessandro","last_name":"Abate"},{"first_name":"Sylvie","last_name":"Bodo","full_name":"Bodo, Sylvie"}],"publisher":"Springer","quality_controlled":"1","page":"83 - 89","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T11:47:37Z","publication_status":"published","intvolume":"     10381","title":"Challenges and tool implementation of hybrid rapidly exploring random trees","alternative_title":["LNCS"],"scopus_import":1,"_id":"633","author":[{"last_name":"Bak","first_name":"Stanley","full_name":"Bak, Stanley"},{"first_name":"Sergiy","last_name":"Bogomolov","orcid":"0000-0002-0686-0365","full_name":"Bogomolov, Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kumar, Aviral","first_name":"Aviral","last_name":"Kumar"}],"volume":10381,"day":"01","doi":"10.1007/978-3-319-63501-9_6","abstract":[{"text":"A Rapidly-exploring Random Tree (RRT) is an algorithm which can search a non-convex region of space by incrementally building a space-filling tree. The tree is constructed from random points drawn from system’s state space and is biased to grow towards large unexplored areas in the system. RRT can provide better coverage of a system’s possible behaviors compared with random simulations, but is more lightweight than full reachability analysis. In this paper, we explore some of the design decisions encountered while implementing a hybrid extension of the RRT algorithm, which have not been elaborated on before. In particular, we focus on handling non-determinism, which arises due to discrete transitions. We introduce the notion of important points to account for this phenomena. We showcase our ideas using heater and navigation benchmarks.","lang":"eng"}],"year":"2017","citation":{"ista":"Bak S, Bogomolov S, Henzinger TA, Kumar A. 2017. Challenges and tool implementation of hybrid rapidly exploring random trees. NSV: Numerical Software Verification, LNCS, vol. 10381, 83–89.","mla":"Bak, Stanley, et al. <i>Challenges and Tool Implementation of Hybrid Rapidly Exploring Random Trees</i>. Edited by Alessandro Abate and Sylvie Bodo, vol. 10381, Springer, 2017, pp. 83–89, doi:<a href=\"https://doi.org/10.1007/978-3-319-63501-9_6\">10.1007/978-3-319-63501-9_6</a>.","short":"S. Bak, S. Bogomolov, T.A. Henzinger, A. Kumar, in:, A. Abate, S. Bodo (Eds.), Springer, 2017, pp. 83–89.","ieee":"S. Bak, S. Bogomolov, T. A. Henzinger, and A. Kumar, “Challenges and tool implementation of hybrid rapidly exploring random trees,” presented at the NSV: Numerical Software Verification, Heidelberg, Germany, 2017, vol. 10381, pp. 83–89.","chicago":"Bak, Stanley, Sergiy Bogomolov, Thomas A Henzinger, and Aviral Kumar. “Challenges and Tool Implementation of Hybrid Rapidly Exploring Random Trees.” edited by Alessandro Abate and Sylvie Bodo, 10381:83–89. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63501-9_6\">https://doi.org/10.1007/978-3-319-63501-9_6</a>.","ama":"Bak S, Bogomolov S, Henzinger TA, Kumar A. Challenges and tool implementation of hybrid rapidly exploring random trees. In: Abate A, Bodo S, eds. Vol 10381. Springer; 2017:83-89. doi:<a href=\"https://doi.org/10.1007/978-3-319-63501-9_6\">10.1007/978-3-319-63501-9_6</a>","apa":"Bak, S., Bogomolov, S., Henzinger, T. A., &#38; Kumar, A. (2017). Challenges and tool implementation of hybrid rapidly exploring random trees. In A. Abate &#38; S. Bodo (Eds.) (Vol. 10381, pp. 83–89). Presented at the NSV: Numerical Software Verification, Heidelberg, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-63501-9_6\">https://doi.org/10.1007/978-3-319-63501-9_6</a>"},"date_updated":"2021-01-12T08:07:06Z"},{"status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"url":"https://hal.archives-ouvertes.fr/hal-01552132","open_access":"1"}],"date_published":"2017-08-03T00:00:00Z","type":"conference","publist_id":"7152","oa":1,"publication_identifier":{"isbn":["978-331965764-6"]},"language":[{"iso":"eng"}],"conference":{"end_date":"2017-09-07","location":"Berlin, Germany","name":"FORMATS: Formal Modelling and Analysis of Timed Systems","start_date":"2017-09-05"},"month":"08","oa_version":"Submitted Version","project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"volume":10419,"date_updated":"2021-01-12T08:07:14Z","citation":{"ieee":"A. Bakhirkin, T. Ferrere, O. Maler, and D. Ulus, “On the quantitative semantics of regular expressions over real-valued signals,” presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany, 2017, vol. 10419, pp. 189–206.","chicago":"Bakhirkin, Alexey, Thomas Ferrere, Oded Maler, and Dogan Ulus. “On the Quantitative Semantics of Regular Expressions over Real-Valued Signals.” edited by Alessandro Abate and Gilles Geeraerts, 10419:189–206. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">https://doi.org/10.1007/978-3-319-65765-3_11</a>.","apa":"Bakhirkin, A., Ferrere, T., Maler, O., &#38; Ulus, D. (2017). On the quantitative semantics of regular expressions over real-valued signals. In A. Abate &#38; G. Geeraerts (Eds.) (Vol. 10419, pp. 189–206). Presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">https://doi.org/10.1007/978-3-319-65765-3_11</a>","ama":"Bakhirkin A, Ferrere T, Maler O, Ulus D. On the quantitative semantics of regular expressions over real-valued signals. In: Abate A, Geeraerts G, eds. Vol 10419. Springer; 2017:189-206. doi:<a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">10.1007/978-3-319-65765-3_11</a>","ista":"Bakhirkin A, Ferrere T, Maler O, Ulus D. 2017. On the quantitative semantics of regular expressions over real-valued signals. FORMATS: Formal Modelling and Analysis of Timed Systems, LNCS, vol. 10419, 189–206.","short":"A. Bakhirkin, T. Ferrere, O. Maler, D. Ulus, in:, A. Abate, G. Geeraerts (Eds.), Springer, 2017, pp. 189–206.","mla":"Bakhirkin, Alexey, et al. <i>On the Quantitative Semantics of Regular Expressions over Real-Valued Signals</i>. Edited by Alessandro Abate and Gilles Geeraerts, vol. 10419, Springer, 2017, pp. 189–206, doi:<a href=\"https://doi.org/10.1007/978-3-319-65765-3_11\">10.1007/978-3-319-65765-3_11</a>."},"year":"2017","abstract":[{"text":"Signal regular expressions can specify sequential properties of real-valued signals based on threshold conditions, regular operations, and duration constraints. In this paper we endow them with a quantitative semantics which indicates how robustly a signal matches or does not match a given expression. First, we show that this semantics is a safe approximation of a distance between the signal and the language defined by the expression. Then, we consider the robust matching problem, that is, computing the quantitative semantics of every segment of a given signal relative to an expression. We present an algorithm that solves this problem for piecewise-constant and piecewise-linear signals and show that for such signals the robustness map is a piecewise-linear function. The availability of an indicator describing how robustly a signal segment matches some regular pattern provides a general framework for quantitative monitoring of cyber-physical systems.","lang":"eng"}],"doi":"10.1007/978-3-319-65765-3_11","day":"03","page":"189 - 206","quality_controlled":"1","publisher":"Springer","editor":[{"first_name":"Alessandro","last_name":"Abate","full_name":"Abate, Alessandro"},{"last_name":"Geeraerts","first_name":"Gilles","full_name":"Geeraerts, Gilles"}],"author":[{"first_name":"Alexey","last_name":"Bakhirkin","full_name":"Bakhirkin, Alexey"},{"full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143","last_name":"Ferrere","first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Maler, Oded","last_name":"Maler","first_name":"Oded"},{"full_name":"Ulus, Dogan","last_name":"Ulus","first_name":"Dogan"}],"_id":"636","scopus_import":1,"alternative_title":["LNCS"],"title":"On the quantitative semantics of regular expressions over real-valued signals","intvolume":"     10419","publication_status":"published","date_created":"2018-12-11T11:47:38Z","department":[{"_id":"ToHe"}]},{"date_updated":"2023-09-07T12:53:00Z","citation":{"ama":"Bogomolov S, Giacobbe M, Henzinger TA, Kong H. Conic abstractions for hybrid systems. In: Vol 10419. Springer; 2017:116-132. doi:<a href=\"https://doi.org/10.1007/978-3-319-65765-3_7\">10.1007/978-3-319-65765-3_7</a>","apa":"Bogomolov, S., Giacobbe, M., Henzinger, T. A., &#38; Kong, H. (2017). Conic abstractions for hybrid systems (Vol. 10419, pp. 116–132). Presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-65765-3_7\">https://doi.org/10.1007/978-3-319-65765-3_7</a>","chicago":"Bogomolov, Sergiy, Mirco Giacobbe, Thomas A Henzinger, and Hui Kong. “Conic Abstractions for Hybrid Systems,” 10419:116–32. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-65765-3_7\">https://doi.org/10.1007/978-3-319-65765-3_7</a>.","ieee":"S. Bogomolov, M. Giacobbe, T. A. Henzinger, and H. Kong, “Conic abstractions for hybrid systems,” presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany, 2017, vol. 10419, pp. 116–132.","short":"S. Bogomolov, M. Giacobbe, T.A. Henzinger, H. Kong, in:, Springer, 2017, pp. 116–132.","mla":"Bogomolov, Sergiy, et al. <i>Conic Abstractions for Hybrid Systems</i>. Vol. 10419, Springer, 2017, pp. 116–32, doi:<a href=\"https://doi.org/10.1007/978-3-319-65765-3_7\">10.1007/978-3-319-65765-3_7</a>.","ista":"Bogomolov S, Giacobbe M, Henzinger TA, Kong H. 2017. Conic abstractions for hybrid systems. FORMATS: Formal Modelling and Analysis of Timed Systems, LNCS, vol. 10419, 116–132."},"year":"2017","abstract":[{"lang":"eng","text":"Despite researchers’ efforts in the last couple of decades, reachability analysis is still a challenging problem even for linear hybrid systems. Among the existing approaches, the most practical ones are mainly based on bounded-time reachable set over-approximations. For the purpose of unbounded-time analysis, one important strategy is to abstract the original system and find an invariant for the abstraction. In this paper, we propose an approach to constructing a new kind of abstraction called conic abstraction for affine hybrid systems, and to computing reachable sets based on this abstraction. The essential feature of a conic abstraction is that it partitions the state space of a system into a set of convex polyhedral cones which is derived from a uniform conic partition of the derivative space. Such a set of polyhedral cones is able to cut all trajectories of the system into almost straight segments so that every segment of a reach pipe in a polyhedral cone tends to be straight as well, and hence can be over-approximated tightly by polyhedra using similar techniques as HyTech or PHAVer. In particular, for diagonalizable affine systems, our approach can guarantee to find an invariant for unbounded reachable sets, which is beyond the capability of bounded-time reachability analysis tools. We implemented the approach in a tool and experiments on benchmarks show that our approach is more powerful than SpaceEx and PHAVer in dealing with diagonalizable systems."}],"doi":"10.1007/978-3-319-65765-3_7","day":"01","ddc":["005"],"volume":"10419 ","author":[{"first_name":"Sergiy","last_name":"Bogomolov","orcid":"0000-0002-0686-0365","full_name":"Bogomolov, Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","first_name":"Mirco","last_name":"Giacobbe","orcid":"0000-0001-8180-0904","full_name":"Giacobbe, Mirco"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Kong, Hui","orcid":"0000-0002-3066-6941","last_name":"Kong","first_name":"Hui","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87"}],"_id":"647","scopus_import":1,"title":"Conic abstractions for hybrid systems","alternative_title":["LNCS"],"pubrep_id":"831","publication_status":"published","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T11:47:41Z","file_date_updated":"2020-07-14T12:47:31Z","page":"116 - 132","quality_controlled":"1","publisher":"Springer","date_published":"2017-09-01T00:00:00Z","type":"conference","oa":1,"publist_id":"7129","publication_identifier":{"isbn":["978-331965764-6"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","related_material":{"record":[{"status":"public","id":"6894","relation":"dissertation_contains"}]},"file":[{"relation":"main_file","access_level":"open_access","creator":"system","file_id":"4956","checksum":"faf546914ba29bcf9974ee36b6b16750","file_size":3806864,"date_created":"2018-12-12T10:12:38Z","content_type":"application/pdf","file_name":"IST-2017-831-v1+1_main.pdf","date_updated":"2020-07-14T12:47:31Z"}],"has_accepted_license":"1","month":"09","oa_version":"Submitted Version","project":[{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"language":[{"iso":"eng"}],"conference":{"start_date":"2017-09-05","name":"FORMATS: Formal Modelling and Analysis of Timed Systems","location":"Berlin, Germany","end_date":"2017-09-07"}},{"conference":{"location":"Paderborn, Germany","end_date":"2017-09-08","start_date":"2017-09-04","name":"FSE: Foundations of Software Engineering"},"language":[{"iso":"eng"}],"month":"09","oa_version":"None","project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","publist_id":"6477","publication_identifier":{"isbn":["978-145035105-8"]},"date_published":"2017-09-01T00:00:00Z","type":"conference","publisher":"ACM","page":"593 - 604","quality_controlled":"1","title":"S3: Syntax- and semantic-guided repair synthesis via programming by examples","publication_status":"published","date_created":"2018-12-11T11:49:19Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","author":[{"first_name":"Xuan","last_name":"Le","full_name":"Le, Xuan"},{"full_name":"Chu, Duc Hiep","first_name":"Duc Hiep","last_name":"Chu","id":"3598E630-F248-11E8-B48F-1D18A9856A87"},{"first_name":"David","last_name":"Lo","full_name":"Lo, David"},{"full_name":"Le Goues, Claire","first_name":"Claire","last_name":"Le Goues"},{"last_name":"Visser","first_name":"Willem","full_name":"Visser, Willem"}],"_id":"942","scopus_import":"1","volume":"F130154","abstract":[{"lang":"eng","text":"A notable class of techniques for automatic program repair is known as semantics-based. Such techniques, e.g., Angelix, infer semantic specifications via symbolic execution, and then use program synthesis to construct new code that satisfies those inferred specifications. However, the obtained specifications are naturally incomplete, leaving the synthesis engine with a difficult task of synthesizing a general solution from a sparse space of many possible solutions that are consistent with the provided specifications but that do not necessarily generalize. We present S3, a new repair synthesis engine that leverages programming-by-examples methodology to synthesize high-quality bug repairs. The novelty in S3 that allows it to tackle the sparse search space to create more general repairs is three-fold: (1) A systematic way to customize and constrain the syntactic search space via a domain-specific language, (2) An efficient enumeration-based search strategy over the constrained search space, and (3) A number of ranking features based on measures of the syntactic and semantic distances between candidate solutions and the original buggy program. We compare S3’s repair effectiveness with state-of-the-art synthesis engines Angelix, Enumerative, and CVC4. S3 can successfully and correctly fix at least three times more bugs than the best baseline on datasets of 52 bugs in small programs, and 100 bugs in real-world large programs. "}],"doi":"10.1145/3106237.3106309","day":"01","isi":1,"external_id":{"isi":["000414279300055"]},"date_updated":"2023-09-26T15:38:36Z","citation":{"ieee":"X. Le, D. H. Chu, D. Lo, C. Le Goues, and W. Visser, “S3: Syntax- and semantic-guided repair synthesis via programming by examples,” presented at the FSE: Foundations of Software Engineering, Paderborn, Germany, 2017, vol. F130154, pp. 593–604.","chicago":"Le, Xuan, Duc Hiep Chu, David Lo, Claire Le Goues, and Willem Visser. “S3: Syntax- and Semantic-Guided Repair Synthesis via Programming by Examples,” F130154:593–604. ACM, 2017. <a href=\"https://doi.org/10.1145/3106237.3106309\">https://doi.org/10.1145/3106237.3106309</a>.","ama":"Le X, Chu DH, Lo D, Le Goues C, Visser W. S3: Syntax- and semantic-guided repair synthesis via programming by examples. In: Vol F130154. ACM; 2017:593-604. doi:<a href=\"https://doi.org/10.1145/3106237.3106309\">10.1145/3106237.3106309</a>","apa":"Le, X., Chu, D. H., Lo, D., Le Goues, C., &#38; Visser, W. (2017). S3: Syntax- and semantic-guided repair synthesis via programming by examples (Vol. F130154, pp. 593–604). Presented at the FSE: Foundations of Software Engineering, Paderborn, Germany: ACM. <a href=\"https://doi.org/10.1145/3106237.3106309\">https://doi.org/10.1145/3106237.3106309</a>","ista":"Le X, Chu DH, Lo D, Le Goues C, Visser W. 2017. S3: Syntax- and semantic-guided repair synthesis via programming by examples. FSE: Foundations of Software Engineering vol. F130154, 593–604.","mla":"Le, Xuan, et al. <i>S3: Syntax- and Semantic-Guided Repair Synthesis via Programming by Examples</i>. Vol. F130154, ACM, 2017, pp. 593–604, doi:<a href=\"https://doi.org/10.1145/3106237.3106309\">10.1145/3106237.3106309</a>.","short":"X. Le, D.H. Chu, D. Lo, C. Le Goues, W. Visser, in:, ACM, 2017, pp. 593–604."},"year":"2017"},{"alternative_title":["LNCS"],"title":"Model counting for recursively-defined strings","intvolume":"     10427","publication_status":"published","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T11:49:26Z","article_processing_charge":"No","author":[{"full_name":"Trinh, Minh","last_name":"Trinh","first_name":"Minh"},{"last_name":"Chu","first_name":"Duc Hiep","full_name":"Chu, Duc Hiep","id":"3598E630-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Joxan","last_name":"Jaffar","full_name":"Jaffar, Joxan"}],"_id":"962","scopus_import":"1","publisher":"Springer","editor":[{"full_name":"Majumdar, Rupak","first_name":"Rupak","last_name":"Majumdar"},{"last_name":"Kunčak","first_name":"Viktor","full_name":"Kunčak, Viktor"}],"page":"399 - 418","quality_controlled":"1","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."}],"doi":"10.1007/978-3-319-63390-9_21","day":"01","isi":1,"external_id":{"isi":["000431900900021"]},"date_updated":"2023-09-22T09:58:02Z","citation":{"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>","ista":"Trinh M, Chu DH, Jaffar J. 2017. Model counting for recursively-defined strings. CAV: Computer Aided Verification, LNCS, vol. 10427, 399–418.","short":"M. Trinh, D.H. Chu, J. Jaffar, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 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>."},"year":"2017","volume":10427,"month":"01","oa_version":"None","project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}],"conference":{"start_date":"2017-07-24","name":"CAV: Computer Aided Verification","end_date":"2017-07-28","location":"Heidelberg, Germany"},"language":[{"iso":"eng"}],"publist_id":"6443","publication_identifier":{"issn":["03029743"]},"date_published":"2017-01-01T00:00:00Z","type":"conference","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public"},{"ddc":["004"],"volume":83,"abstract":[{"lang":"eng","text":"Network games are widely used as a model for selfish resource-allocation problems. In the classical model, each player selects a path connecting her source and target vertex. The cost of traversing an edge depends on the number of players that traverse it. Thus, it abstracts the fact that different users may use a resource at different times and for different durations, which plays an important role in defining the costs of the users in reality. For example, when transmitting packets in a communication network, routing traffic in a road network, or processing a task in a production system, the traversal of the network involves an inherent delay, and so sharing and congestion of resources crucially depends on time. We study timed network games , which add a time component to network games. Each vertex v in the network is associated with a cost function, mapping the load on v to the price that a player pays for staying in v for one time unit with this load. In addition, each edge has a guard, describing time intervals in which the edge can be traversed, forcing the players to spend time on vertices. Unlike earlier work that add a time component to network games, the time in our model is continuous and cannot be discretized. In particular, players have uncountably many strategies, and a game may have uncountably many pure Nash equilibria. We study properties of timed network games with cost-sharing or congestion cost functions: their stability, equilibrium inefficiency, and complexity. In particular, we show that the answer to the question whether we can restrict attention to boundary strategies, namely ones in which edges are traversed only at the boundaries of guards, is mixed. "}],"doi":"10.4230/LIPIcs.MFCS.2017.37","day":"01","date_updated":"2023-02-23T12:35:50Z","year":"2017","citation":{"mla":"Avni, Guy, et al. <i>Timed Network Games with Clocks</i>. Vol. 83, 37, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.37\">10.4230/LIPIcs.MFCS.2017.37</a>.","short":"G. Avni, S. Guha, O. Kupferman, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ista":"Avni G, Guha S, Kupferman O. 2017. Timed network games with clocks. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 83, 37.","apa":"Avni, G., Guha, S., &#38; Kupferman, O. (2017). Timed network games with clocks (Vol. 83). Presented at the MFCS: Mathematical Foundations of Computer Science (SG), Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.37\">https://doi.org/10.4230/LIPIcs.MFCS.2017.37</a>","ama":"Avni G, Guha S, Kupferman O. Timed network games with clocks. In: Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.37\">10.4230/LIPIcs.MFCS.2017.37</a>","ieee":"G. Avni, S. Guha, and O. Kupferman, “Timed network games with clocks,” presented at the MFCS: Mathematical Foundations of Computer Science (SG), Aalborg, Denmark, 2017, vol. 83.","chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “Timed Network Games with Clocks,” Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.37\">https://doi.org/10.4230/LIPIcs.MFCS.2017.37</a>."},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file_date_updated":"2020-07-14T12:48:18Z","quality_controlled":"1","alternative_title":["LIPIcs"],"pubrep_id":"829","title":"Timed network games with clocks","intvolume":"        83","publication_status":"published","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T11:49:26Z","author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","first_name":"Guy","last_name":"Avni"},{"last_name":"Guha","first_name":"Shibashis","full_name":"Guha, Shibashis"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"}],"_id":"963","scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","related_material":{"record":[{"status":"public","id":"6005","relation":"later_version"}]},"file":[{"content_type":"application/pdf","file_name":"IST-2017-829-v1+1_mfcs-cr.pdf","date_updated":"2020-07-14T12:48:18Z","file_size":369730,"checksum":"f55eaf7f3c36ea07801112acfedd17d5","date_created":"2018-12-12T10:14:10Z","creator":"system","file_id":"5059","relation":"main_file","access_level":"open_access"}],"oa":1,"publist_id":"6438","publication_identifier":{"issn":["18688969"]},"date_published":"2017-06-01T00:00:00Z","type":"conference","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)"},"conference":{"start_date":"2017-08-21","name":"MFCS: Mathematical Foundations of Computer Science (SG)","end_date":"2017-08-25","location":"Aalborg, Denmark"},"language":[{"iso":"eng"}],"month":"06","article_number":"37","oa_version":"Published Version","project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"}],"has_accepted_license":"1"},{"publist_id":"6395","oa":1,"publication_identifier":{"issn":["10450823"]},"type":"conference","date_published":"2017-05-30T00:00:00Z","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","related_material":{"record":[{"relation":"later_version","id":"6006","status":"public"}]},"file":[{"date_created":"2018-12-12T10:16:58Z","file_size":365172,"date_updated":"2018-12-12T10:16:58Z","content_type":"application/pdf","file_name":"IST-2017-818-v1+1_allIJCAI_CR.pdf","relation":"main_file","access_level":"open_access","file_id":"5249","creator":"system"}],"month":"05","project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"}],"oa_version":"Submitted Version","has_accepted_license":"1","conference":{"location":"Melbourne, Australia","end_date":"2017-08-25","name":"IJCAI: International Joint Conference on Artificial Intelligence ","start_date":"2017-08-19"},"language":[{"iso":"eng"}],"abstract":[{"text":"Network games (NGs) are played on directed graphs and are extensively used in network design and analysis. Search problems for NGs include finding special strategy profiles such as a Nash equilibrium and a globally optimal solution. The networks modeled by NGs may be huge. In formal verification, abstraction has proven to be an extremely effective technique for reasoning about systems with big and even infinite state spaces. We describe an abstraction-refinement methodology for reasoning about NGs. Our methodology is based on an abstraction function that maps the state space of an NG to a much smaller state space. We search for a global optimum and a Nash equilibrium by reasoning on an under- and an overapproximation defined on top of this smaller state space. When the approximations are too coarse to find such profiles, we refine the abstraction function. Our experimental results demonstrate the efficiency of the methodology.","lang":"eng"}],"day":"30","doi":"10.24963/ijcai.2017/11","external_id":{"isi":["000764137500011"]},"isi":1,"citation":{"ista":"Avni G, Guha S, Kupferman O. 2017. An abstraction-refinement methodology for reasoning about network games. IJCAI: International Joint Conference on Artificial Intelligence , 70–76.","short":"G. Avni, S. Guha, O. Kupferman, in:, AAAI Press, 2017, pp. 70–76.","mla":"Avni, Guy, et al. <i>An Abstraction-Refinement Methodology for Reasoning about Network Games</i>. AAAI Press, 2017, pp. 70–76, doi:<a href=\"https://doi.org/10.24963/ijcai.2017/11\">10.24963/ijcai.2017/11</a>.","ieee":"G. Avni, S. Guha, and O. Kupferman, “An abstraction-refinement methodology for reasoning about network games,” presented at the IJCAI: International Joint Conference on Artificial Intelligence , Melbourne, Australia, 2017, pp. 70–76.","chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “An Abstraction-Refinement Methodology for Reasoning about Network Games,” 70–76. AAAI Press, 2017. <a href=\"https://doi.org/10.24963/ijcai.2017/11\">https://doi.org/10.24963/ijcai.2017/11</a>.","apa":"Avni, G., Guha, S., &#38; Kupferman, O. (2017). An abstraction-refinement methodology for reasoning about network games (pp. 70–76). Presented at the IJCAI: International Joint Conference on Artificial Intelligence , Melbourne, Australia: AAAI Press. <a href=\"https://doi.org/10.24963/ijcai.2017/11\">https://doi.org/10.24963/ijcai.2017/11</a>","ama":"Avni G, Guha S, Kupferman O. An abstraction-refinement methodology for reasoning about network games. In: AAAI Press; 2017:70-76. doi:<a href=\"https://doi.org/10.24963/ijcai.2017/11\">10.24963/ijcai.2017/11</a>"},"year":"2017","date_updated":"2023-09-22T09:49:00Z","ddc":["004"],"title":"An abstraction-refinement methodology for reasoning about network games","pubrep_id":"818","date_created":"2018-12-11T11:49:38Z","article_processing_charge":"No","department":[{"_id":"ToHe"}],"publication_status":"published","author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy","full_name":"Avni, Guy","orcid":"0000-0001-5588-8287"},{"full_name":"Guha, Shibashis","first_name":"Shibashis","last_name":"Guha"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"scopus_import":"1","_id":"1003","publisher":"AAAI Press","file_date_updated":"2018-12-12T10:16:58Z","quality_controlled":"1","page":"70 - 76"},{"project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"oa_version":"Submitted Version","month":"03","conference":{"name":"ESOP: European Symposium on Programming","start_date":"2017-04-22","location":"Uppsala, Sweden","end_date":"2017-04-29"},"language":[{"iso":"eng"}],"publication_identifier":{"issn":["03029743"]},"oa":1,"publist_id":"6384","type":"conference","date_published":"2017-03-19T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/1701.04914","open_access":"1"}],"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_created":"2018-12-11T11:49:41Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"article_processing_charge":"No","publication_status":"published","intvolume":"     10201","alternative_title":["LNCS"],"title":"Faster algorithms for weighted recursive state machines","scopus_import":"1","_id":"1011","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"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","first_name":"Samarth","last_name":"Mishra"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"}],"editor":[{"last_name":"Yang","first_name":"Hongseok","full_name":"Yang, Hongseok"}],"publisher":"Springer","ec_funded":1,"quality_controlled":"1","page":"287 - 313","day":"19","doi":"10.1007/978-3-662-54434-1_11","abstract":[{"lang":"eng","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."}],"year":"2017","citation":{"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.","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>.","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>","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.","short":"K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.), Springer, 2017, pp. 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>."},"date_updated":"2023-09-22T09:44:50Z","external_id":{"isi":["000681702400011"]},"isi":1,"volume":10201},{"volume":52,"isi":1,"external_id":{"isi":["000408311200013"]},"date_updated":"2025-07-14T09:09:58Z","year":"2017","citation":{"ieee":"K. Chatterjee, P. Novotný, and D. Zikelic, “Stochastic invariants for probabilistic termination,” presented at the POPL: Principles of Programming Languages, Paris, France, 2017, vol. 52, no. 1, pp. 145–160.","chicago":"Chatterjee, Krishnendu, Petr Novotný, and Djordje Zikelic. “Stochastic Invariants for Probabilistic Termination,” 52:145–60. ACM, 2017. <a href=\"https://doi.org/10.1145/3009837.3009873\">https://doi.org/10.1145/3009837.3009873</a>.","apa":"Chatterjee, K., Novotný, P., &#38; Zikelic, D. (2017). Stochastic invariants for probabilistic termination (Vol. 52, pp. 145–160). Presented at the POPL: Principles of Programming Languages, Paris, France: ACM. <a href=\"https://doi.org/10.1145/3009837.3009873\">https://doi.org/10.1145/3009837.3009873</a>","ama":"Chatterjee K, Novotný P, Zikelic D. Stochastic invariants for probabilistic termination. In: Vol 52. ACM; 2017:145-160. doi:<a href=\"https://doi.org/10.1145/3009837.3009873\">10.1145/3009837.3009873</a>","ista":"Chatterjee K, Novotný P, Zikelic D. 2017. Stochastic invariants for probabilistic termination. POPL: Principles of Programming Languages, ACM SIGPLAN Notices, vol. 52, 145–160.","short":"K. Chatterjee, P. Novotný, D. Zikelic, in:, ACM, 2017, pp. 145–160.","mla":"Chatterjee, Krishnendu, et al. <i>Stochastic Invariants for Probabilistic Termination</i>. Vol. 52, no. 1, ACM, 2017, pp. 145–60, doi:<a href=\"https://doi.org/10.1145/3009837.3009873\">10.1145/3009837.3009873</a>."},"abstract":[{"text":"Termination is one of the basic liveness properties, and we study the termination problem for probabilistic programs with real-valued variables. Previous works focused on the qualitative problem that asks whether an input program terminates with probability~1 (almost-sure termination). A powerful approach for this qualitative problem is the notion of ranking supermartingales with respect to a given set of invariants. The quantitative problem (probabilistic termination) asks for bounds on the termination probability. A fundamental and conceptual drawback of the existing approaches to address probabilistic termination is that even though the supermartingales consider the probabilistic behavior of the programs, the invariants are obtained completely ignoring the probabilistic aspect. In this work we address the probabilistic termination problem for linear-arithmetic probabilistic programs with nondeterminism. We define the notion of {\\em stochastic invariants}, which are constraints along with a probability bound that the constraints hold. We introduce a concept of {\\em repulsing supermartingales}. First, we show that repulsing supermartingales can be used to obtain bounds on the probability of the stochastic invariants. Second, we show the effectiveness of repulsing supermartingales in the following three ways: (1)~With a combination of ranking and repulsing supermartingales we can compute lower bounds on the probability of termination; (2)~repulsing supermartingales provide witnesses for refutation of almost-sure termination; and (3)~with a combination of ranking and repulsing supermartingales we can establish persistence properties of probabilistic programs. We also present results on related computational problems and an experimental evaluation of our approach on academic examples. ","lang":"eng"}],"doi":"10.1145/3009837.3009873","day":"01","page":"145 - 160","ec_funded":1,"quality_controlled":"1","publisher":"ACM","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Novotny","first_name":"Petr","full_name":"Novotny, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Djordje","last_name":"Zikelic","full_name":"Zikelic, Djordje"}],"issue":"1","_id":"1194","scopus_import":"1","alternative_title":["ACM SIGPLAN Notices"],"title":"Stochastic invariants for probabilistic termination","intvolume":"        52","publication_status":"published","date_created":"2018-12-11T11:50:39Z","department":[{"_id":"KrCh"}],"article_processing_charge":"No","related_material":{"record":[{"relation":"dissertation_contains","id":"14539","status":"public"}]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1611.01063"}],"date_published":"2017-01-01T00:00:00Z","type":"conference","publist_id":"6157","oa":1,"publication_identifier":{"issn":["07308566"]},"language":[{"iso":"eng"}],"conference":{"start_date":"2017-01-15","name":"POPL: Principles of Programming Languages","location":"Paris, France","end_date":"2017-01-21"},"month":"01","oa_version":"Submitted Version","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}]},{"conference":{"start_date":"2015-05-03","name":"SNAPL: Summit oN Advances in Programming Languages","location":"Asilomar, CA, United States","end_date":"2015-05-06"},"language":[{"iso":"eng"}],"month":"01","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"oa_version":"Published Version","has_accepted_license":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","file":[{"relation":"main_file","access_level":"open_access","file_id":"5050","creator":"system","date_created":"2018-12-12T10:14:02Z","checksum":"cf5e94baa89a2dc4c5de01abc676eda8","file_size":489362,"date_updated":"2020-07-14T12:44:58Z","content_type":"application/pdf","file_name":"IST-2016-499-v1+1_9.pdf"}],"oa":1,"publist_id":"5681","publication_identifier":{"isbn":["978-3-939897-80-4 "]},"type":"conference","date_published":"2015-01-01T00:00:00Z","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)"},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file_date_updated":"2020-07-14T12:44:58Z","quality_controlled":"1","ec_funded":1,"series_title":"Leibniz International Proceedings in Informatics","page":"90 - 102","intvolume":"        32","pubrep_id":"499","alternative_title":["LIPIcs"],"title":"The need for language support for fault-tolerant distributed systems","date_created":"2018-12-11T11:52:22Z","department":[{"_id":"ToHe"}],"publication_status":"published","author":[{"first_name":"Cezara","last_name":"Dragoi","full_name":"Dragoi, Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"4397AC76-F248-11E8-B48F-1D18A9856A87","last_name":"Zufferey","first_name":"Damien","full_name":"Zufferey, Damien","orcid":"0000-0002-3197-8736"}],"scopus_import":1,"_id":"1498","ddc":["005"],"volume":32,"abstract":[{"lang":"eng","text":"Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. Nonetheless there is surprisingly little language and verification support to build distributed systems based on fault-tolerant algorithms. In this paper, we present some of the challenges that a designer has to overcome to implement a fault-tolerant distributed system. Then we review different models that have been proposed to reason about distributed algorithms and sketch how such a model can form the basis for a domain-specific programming language. Adopting a high-level programming model can simplify the programmer's life and make the code amenable to automated verification, while still compiling to efficiently executable code. We conclude by summarizing the current status of an ongoing language design and implementation project that is based on this idea."}],"day":"01","doi":"10.4230/LIPIcs.SNAPL.2015.90","citation":{"apa":"Dragoi, C., Henzinger, T. A., &#38; Zufferey, D. (2015). The need for language support for fault-tolerant distributed systems. Presented at the SNAPL: Summit oN Advances in Programming Languages, Asilomar, CA, United States: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">https://doi.org/10.4230/LIPIcs.SNAPL.2015.90</a>","ama":"Dragoi C, Henzinger TA, Zufferey D. The need for language support for fault-tolerant distributed systems. 2015;32:90-102. doi:<a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">10.4230/LIPIcs.SNAPL.2015.90</a>","chicago":"Dragoi, Cezara, Thomas A Henzinger, and Damien Zufferey. “The Need for Language Support for Fault-Tolerant Distributed Systems.” Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. <a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">https://doi.org/10.4230/LIPIcs.SNAPL.2015.90</a>.","ieee":"C. Dragoi, T. A. Henzinger, and D. Zufferey, “The need for language support for fault-tolerant distributed systems,” vol. 32. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 90–102, 2015.","short":"C. Dragoi, T.A. Henzinger, D. Zufferey, 32 (2015) 90–102.","mla":"Dragoi, Cezara, et al. <i>The Need for Language Support for Fault-Tolerant Distributed Systems</i>. Vol. 32, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 90–102, doi:<a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">10.4230/LIPIcs.SNAPL.2015.90</a>.","ista":"Dragoi C, Henzinger TA, Zufferey D. 2015. The need for language support for fault-tolerant distributed systems. 32, 90–102."},"year":"2015","date_updated":"2020-08-11T10:09:14Z"}]