[{"quality_controlled":"1","file_date_updated":"2020-07-14T12:47:00Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","file":[{"access_level":"open_access","creator":"system","file_name":"IST-2018-925-v1+1_1710.03391v1.pdf","date_created":"2018-12-12T10:12:21Z","checksum":"6274f6c0da3376a7b079180d81568518","file_size":209294,"date_updated":"2020-07-14T12:47:00Z","file_id":"4939","content_type":"application/pdf","relation":"main_file"}],"doi":"10.4204/EPTCS.259.3","volume":259,"citation":{"mla":"Finkbeiner, Bernd, and Andrey Kupriyanov. “Causality-Based Model Checking.” Electronic Proceedings in Theoretical Computer Science, vol. 259, Open Publishing Association, 2017, pp. 31–38, doi:10.4204/EPTCS.259.3.","short":"B. Finkbeiner, A. Kupriyanov, in:, Electronic Proceedings in Theoretical Computer Science, Open Publishing Association, 2017, pp. 31–38.","apa":"Finkbeiner, B., & Kupriyanov, A. (2017). Causality-based model checking. In Electronic Proceedings in Theoretical Computer Science (Vol. 259, pp. 31–38). Uppsala, Sweden: Open Publishing Association. https://doi.org/10.4204/EPTCS.259.3","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: Electronic Proceedings in Theoretical Computer Science. Vol 259. Open Publishing Association; 2017:31-38. doi:10.4204/EPTCS.259.3","ieee":"B. Finkbeiner and A. Kupriyanov, “Causality-based model checking,” in Electronic Proceedings in Theoretical Computer Science, Uppsala, Sweden, 2017, vol. 259, pp. 31–38.","chicago":"Finkbeiner, Bernd, and Andrey Kupriyanov. “Causality-Based Model Checking.” In Electronic Proceedings in Theoretical Computer Science, 259:31–38. Open Publishing Association, 2017. https://doi.org/10.4204/EPTCS.259.3."},"publication_identifier":{"issn":["2075-2180"]},"_id":"549","day":"10","intvolume":" 259","publication_status":"published","ddc":["004"],"has_accepted_license":"1","scopus_import":"1","corr_author":"1","date_created":"2018-12-11T11:47:07Z","arxiv":1,"conference":{"end_date":"2017-04-29","location":"Uppsala, Sweden","name":"CREST: Causal Reasoning for Embedded and Safety-Critical Systems Technologies","start_date":"2017-04-29"},"alternative_title":["EPTCS"],"type":"conference","oa_version":"Submitted Version","publication":"Electronic Proceedings in Theoretical Computer Science","status":"public","isi":1,"language":[{"iso":"eng"}],"year":"2017","month":"10","page":"31 - 38","oa":1,"project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"}],"publisher":"Open Publishing Association","pubrep_id":"925","abstract":[{"lang":"eng","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."}],"external_id":{"arxiv":["1710.03391"],"isi":["000439358700004"]},"article_processing_charge":"No","department":[{"_id":"ToHe"}],"main_file_link":[{"url":"https://arxiv.org/abs/1710.03391","open_access":"1"}],"author":[{"last_name":"Finkbeiner","first_name":"Bernd","full_name":"Finkbeiner, Bernd"},{"id":"2C311BF8-F248-11E8-B48F-1D18A9856A87","first_name":"Andrey","last_name":"Kupriyanov","full_name":"Kupriyanov, Andrey"}],"date_published":"2017-10-10T00:00:00Z","publist_id":"7264","date_updated":"2025-09-18T09:38:35Z","title":"Causality-based model checking"},{"ec_funded":1,"author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"date_published":"2017-07-25T00:00:00Z","publist_id":"7170","series_title":"Theoretical Computer Science and General Issues","title":"The cost of exactness in quantitative reachability","date_updated":"2025-04-15T06:26:15Z","article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"Springer","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."}],"project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"oa":1,"language":[{"iso":"eng"}],"page":"367 - 381","month":"07","year":"2017","alternative_title":["LNCS"],"type":"book_chapter","publication":"Models, Algorithms, Logics and Tools","oa_version":"Submitted Version","status":"public","date_created":"2018-12-11T11:47:34Z","ddc":["000"],"editor":[{"first_name":"Luca","last_name":"Aceto","full_name":"Aceto, Luca"},{"full_name":"Bacci, Giorgio","first_name":"Giorgio","last_name":"Bacci"},{"full_name":"Ingólfsdóttir, Anna","last_name":"Ingólfsdóttir","first_name":"Anna"},{"first_name":"Axel","last_name":"Legay","full_name":"Legay, Axel"},{"last_name":"Mardare","first_name":"Radu","full_name":"Mardare, Radu"}],"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.","has_accepted_license":"1","scopus_import":"1","publication_identifier":{"issn":["0302-9743"],"isbn":["978-3-319-63120-2"]},"_id":"625","day":"25","intvolume":" 10460","publication_status":"published","volume":10460,"citation":{"mla":"Chatterjee, Krishnendu, et al. “The Cost of Exactness in Quantitative Reachability.” Models, Algorithms, Logics and Tools, edited by Luca Aceto et al., vol. 10460, Springer, 2017, pp. 367–81, doi:10.1007/978-3-319-63121-9_18.","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. Models, Algorithms, Logics and Tools. Vol 10460. Theoretical Computer Science and General Issues. Springer; 2017:367-381. doi:10.1007/978-3-319-63121-9_18","apa":"Chatterjee, K., Doyen, L., & Henzinger, T. A. (2017). The cost of exactness in quantitative reachability. In L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, & R. Mardare (Eds.), Models, Algorithms, Logics and Tools (Vol. 10460, pp. 367–381). Springer. https://doi.org/10.1007/978-3-319-63121-9_18","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.","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.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “The Cost of Exactness in Quantitative Reachability.” In Models, Algorithms, Logics and Tools, 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. https://doi.org/10.1007/978-3-319-63121-9_18.","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “The cost of exactness in quantitative reachability,” in Models, Algorithms, Logics and Tools, vol. 10460, L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, and R. Mardare, Eds. Springer, 2017, pp. 367–381."},"doi":"10.1007/978-3-319-63121-9_18","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"access_level":"open_access","creator":"dernst","file_name":"2017_ModelsAlgorithms_Chatterjee.pdf","date_created":"2019-11-19T08:06:50Z","checksum":"b2402766ec02c79801aac634bd8f9f6c","file_size":192826,"date_updated":"2020-07-14T12:47:25Z","file_id":"7048","content_type":"application/pdf","relation":"main_file"}],"quality_controlled":"1","file_date_updated":"2020-07-14T12:47:25Z"},{"file":[{"checksum":"f395d0d20102b89aeaad8b4ef4f18f4f","file_size":569863,"date_updated":"2020-07-14T12:47:27Z","file_id":"4897","content_type":"application/pdf","relation":"main_file","access_level":"open_access","creator":"system","file_name":"IST-2017-741-v1+1_main.pdf","date_created":"2018-12-12T10:11:41Z"},{"file_size":563276,"date_updated":"2020-07-14T12:47:27Z","checksum":"f416ee1ae4497b23ecdf28b1f18bb8df","content_type":"application/pdf","relation":"main_file","file_id":"4898","access_level":"open_access","date_created":"2018-12-12T10:11:42Z","creator":"system","file_name":"IST-2018-741-v2+2_main.pdf"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","file_date_updated":"2020-07-14T12:47:27Z","quality_controlled":"1","volume":10205,"citation":{"mla":"Bogomolov, Sergiy, et al. Counterexample Guided Refinement of Template Polyhedra. Vol. 10205, Springer, 2017, pp. 589–606, doi:10.1007/978-3-662-54577-5_34.","ama":"Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. Counterexample guided refinement of template polyhedra. In: Vol 10205. Springer; 2017:589-606. doi:10.1007/978-3-662-54577-5_34","apa":"Bogomolov, S., Frehse, G., Giacobbe, M., & 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. https://doi.org/10.1007/978-3-662-54577-5_34","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.","short":"S. Bogomolov, G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2017, 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. https://doi.org/10.1007/978-3-662-54577-5_34.","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."},"doi":"10.1007/978-3-662-54577-5_34","scopus_import":"1","has_accepted_license":"1","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).","ddc":["000"],"publication_status":"published","day":"31","intvolume":" 10205","_id":"631","publication_identifier":{"isbn":["978-366254576-8"]},"status":"public","oa_version":"Submitted Version","alternative_title":["LNCS"],"type":"conference","conference":{"location":"Uppsala, Sweden","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2017-04-22","end_date":"2017-04-29"},"date_created":"2018-12-11T11:47:36Z","corr_author":"1","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"6894"}]},"oa":1,"year":"2017","page":"589 - 606","month":"03","isi":1,"language":[{"iso":"eng"}],"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"}],"pubrep_id":"966","publisher":"Springer","project":[{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"date_updated":"2026-04-08T07:47:13Z","title":"Counterexample guided refinement of template polyhedra","date_published":"2017-03-31T00:00:00Z","publist_id":"7162","author":[{"last_name":"Bogomolov","orcid":"0000-0002-0686-0365","first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","full_name":"Bogomolov, Sergiy"},{"first_name":"Goran","last_name":"Frehse","full_name":"Frehse, Goran"},{"full_name":"Giacobbe, Mirco","first_name":"Mirco","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8180-0904","last_name":"Giacobbe"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"}],"department":[{"_id":"ToHe"}],"article_processing_charge":"No","external_id":{"isi":["000440734900034"]}},{"scopus_import":"1","editor":[{"full_name":"Abate, Alessandro","first_name":"Alessandro","last_name":"Abate"},{"full_name":"Bodo, Sylvie","last_name":"Bodo","first_name":"Sylvie"}],"intvolume":" 10381","day":"01","publication_status":"published","publication_identifier":{"isbn":["978-331963500-2"]},"_id":"633","oa_version":"None","status":"public","conference":{"end_date":"2017-07-23","location":"Heidelberg, Germany","start_date":"2017-07-22","name":"NSV: Numerical Software Verification"},"alternative_title":["LNCS"],"type":"conference","date_created":"2018-12-11T11:47:37Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1","citation":{"mla":"Bak, Stanley, et al. Challenges and Tool Implementation of Hybrid Rapidly Exploring Random Trees. Edited by Alessandro Abate and Sylvie Bodo, vol. 10381, Springer, 2017, pp. 83–89, doi:10.1007/978-3-319-63501-9_6.","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:10.1007/978-3-319-63501-9_6","short":"S. Bak, S. Bogomolov, T.A. Henzinger, A. Kumar, in:, A. Abate, S. Bodo (Eds.), Springer, 2017, pp. 83–89.","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.","apa":"Bak, S., Bogomolov, S., Henzinger, T. A., & Kumar, A. (2017). Challenges and tool implementation of hybrid rapidly exploring random trees. In A. Abate & S. Bodo (Eds.) (Vol. 10381, pp. 83–89). Presented at the NSV: Numerical Software Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63501-9_6","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. https://doi.org/10.1007/978-3-319-63501-9_6.","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."},"volume":10381,"doi":"10.1007/978-3-319-63501-9_6","title":"Challenges and tool implementation of hybrid rapidly exploring random trees","date_updated":"2025-09-11T07:25:57Z","author":[{"last_name":"Bak","first_name":"Stanley","full_name":"Bak, Stanley"},{"full_name":"Bogomolov, Sergiy","last_name":"Bogomolov","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Aviral","last_name":"Kumar","full_name":"Kumar, Aviral"}],"publist_id":"7159","date_published":"2017-01-01T00:00:00Z","department":[{"_id":"ToHe"}],"external_id":{"isi":["000440724800006"]},"article_processing_charge":"No","page":"83 - 89","year":"2017","month":"01","language":[{"iso":"eng"}],"isi":1,"abstract":[{"lang":"eng","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."}],"publisher":"Springer","project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}]},{"main_file_link":[{"url":"https://hal.archives-ouvertes.fr/hal-01552132","open_access":"1"}],"author":[{"full_name":"Bakhirkin, Alexey","last_name":"Bakhirkin","first_name":"Alexey"},{"last_name":"Ferrere","orcid":"0000-0001-5199-3143","first_name":"Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","full_name":"Ferrere, Thomas"},{"last_name":"Maler","first_name":"Oded","full_name":"Maler, Oded"},{"first_name":"Dogan","last_name":"Ulus","full_name":"Ulus, Dogan"}],"date_published":"2017-08-03T00:00:00Z","publist_id":"7152","date_updated":"2025-09-11T07:24:11Z","title":"On the quantitative semantics of regular expressions over real-valued signals","external_id":{"isi":["000611678300011"]},"article_processing_charge":"No","department":[{"_id":"ToHe"}],"publisher":"Springer","abstract":[{"lang":"eng","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."}],"project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"}],"oa":1,"isi":1,"language":[{"iso":"eng"}],"page":"189 - 206","year":"2017","month":"08","conference":{"end_date":"2017-09-07","location":"Berlin, Germany","name":"FORMATS: Formal Modelling and Analysis of Timed Systems","start_date":"2017-09-05"},"type":"conference","alternative_title":["LNCS"],"oa_version":"Submitted Version","status":"public","date_created":"2018-12-11T11:47:38Z","editor":[{"last_name":"Abate","first_name":"Alessandro","full_name":"Abate, Alessandro"},{"full_name":"Geeraerts, Gilles","last_name":"Geeraerts","first_name":"Gilles"}],"scopus_import":"1","publication_identifier":{"isbn":["978-331965764-6"]},"_id":"636","day":"03","intvolume":" 10419","publication_status":"published","volume":10419,"citation":{"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. https://doi.org/10.1007/978-3-319-65765-3_11.","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.","mla":"Bakhirkin, Alexey, et al. On the Quantitative Semantics of Regular Expressions over Real-Valued Signals. Edited by Alessandro Abate and Gilles Geeraerts, vol. 10419, Springer, 2017, pp. 189–206, doi:10.1007/978-3-319-65765-3_11.","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:10.1007/978-3-319-65765-3_11","short":"A. Bakhirkin, T. Ferrere, O. Maler, D. Ulus, in:, A. Abate, G. Geeraerts (Eds.), Springer, 2017, pp. 189–206.","apa":"Bakhirkin, A., Ferrere, T., Maler, O., & Ulus, D. (2017). On the quantitative semantics of regular expressions over real-valued signals. In A. Abate & G. Geeraerts (Eds.) (Vol. 10419, pp. 189–206). Presented at the FORMATS: Formal Modelling and Analysis of Timed Systems, Berlin, Germany: Springer. https://doi.org/10.1007/978-3-319-65765-3_11","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."},"doi":"10.1007/978-3-319-65765-3_11","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1"},{"title":"Numerical Software Verification","date_updated":"2026-03-31T12:28:01Z","publist_id":"7150","date_published":"2017-01-01T00:00:00Z","editor":[{"full_name":"Bogomolov, Sergiy","last_name":"Bogomolov","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy"},{"last_name":"Martel","first_name":"Matthieu","full_name":"Martel, Matthieu"},{"last_name":"Prabhakar","first_name":"Pavithra","full_name":"Prabhakar, Pavithra"}],"publication_status":"published","intvolume":" 10152","day":"01","department":[{"_id":"ToHe"}],"_id":"638","article_processing_charge":"No","publication_identifier":{"issn":["0302-9743"],"eisbn":["978-3-319-54292-8"]},"status":"public","oa_version":"None","alternative_title":["LNCS"],"type":"conference_editor","conference":{"end_date":"2016-07-18","start_date":"2016-07-17","name":"NSV: Numerical Software Verification","location":"Toronto, ON, Canada"},"date_created":"2018-12-11T11:47:38Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2017","month":"01","quality_controlled":"1","language":[{"iso":"eng"}],"volume":10152,"citation":{"mla":"Bogomolov, Sergiy, et al., editors. Numerical Software Verification. Vol. 10152, Springer, 2017, doi:10.1007/978-3-319-54292-8.","short":"S. Bogomolov, M. Martel, P. Prabhakar, eds., Numerical Software Verification, Springer, 2017.","ista":"Bogomolov S, Martel M, Prabhakar P eds. 2017. Numerical Software Verification, Springer,p.","apa":"Bogomolov, S., Martel, M., & Prabhakar, P. (Eds.). (2017). Numerical Software Verification (Vol. 10152). Presented at the NSV: Numerical Software Verification, Toronto, ON, Canada: Springer. https://doi.org/10.1007/978-3-319-54292-8","ama":"Bogomolov S, Martel M, Prabhakar P, eds. Numerical Software Verification. Vol 10152. Springer; 2017. doi:10.1007/978-3-319-54292-8","ieee":"S. Bogomolov, M. Martel, and P. Prabhakar, Eds., Numerical Software Verification, vol. 10152. Springer, 2017.","chicago":"Bogomolov, Sergiy, Matthieu Martel, and Pavithra Prabhakar, eds. Numerical Software Verification. Vol. 10152. Springer, 2017. https://doi.org/10.1007/978-3-319-54292-8."},"abstract":[{"text":"This book constitutes the refereed proceedings of the 9th InternationalWorkshop on Numerical Software Verification, NSV 2016, held in Toronto, ON, Canada in July 2011 - colocated with CAV 2016, the 28th International Conference on Computer Aided Verification.\r\nThe NSV workshop is dedicated to the development of logical and mathematical techniques for the reasoning about programmability and reliability.","lang":"eng"}],"publisher":"Springer","doi":"10.1007/978-3-319-54292-8"},{"publisher":"AAAI Press","pubrep_id":"818","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"}],"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":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"oa":1,"language":[{"iso":"eng"}],"isi":1,"year":"2017","page":"70 - 76","month":"05","author":[{"orcid":"0000-0001-5588-8287","last_name":"Avni","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","full_name":"Avni, Guy"},{"full_name":"Guha, Shibashis","first_name":"Shibashis","last_name":"Guha"},{"full_name":"Kupferman, Orna","last_name":"Kupferman","first_name":"Orna"}],"publist_id":"6395","date_published":"2017-05-30T00:00:00Z","title":"An abstraction-refinement methodology for reasoning about network games","date_updated":"2025-07-10T11:49:38Z","external_id":{"isi":["000764137500011"]},"article_processing_charge":"No","department":[{"_id":"ToHe"}],"citation":{"mla":"Avni, Guy, et al. An Abstraction-Refinement Methodology for Reasoning about Network Games. AAAI Press, 2017, pp. 70–76, doi:10.24963/ijcai.2017/11.","apa":"Avni, G., Guha, S., & 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. https://doi.org/10.24963/ijcai.2017/11","short":"G. Avni, S. Guha, O. Kupferman, in:, AAAI Press, 2017, pp. 70–76.","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.","ama":"Avni G, Guha S, Kupferman O. An abstraction-refinement methodology for reasoning about network games. In: AAAI Press; 2017:70-76. doi:10.24963/ijcai.2017/11","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. https://doi.org/10.24963/ijcai.2017/11."},"doi":"10.24963/ijcai.2017/11","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"file_size":365172,"date_updated":"2018-12-12T10:16:58Z","file_id":"5249","content_type":"application/pdf","relation":"main_file","access_level":"open_access","creator":"system","file_name":"IST-2017-818-v1+1_allIJCAI_CR.pdf","date_created":"2018-12-12T10:16:58Z"}],"quality_controlled":"1","file_date_updated":"2018-12-12T10:16:58Z","conference":{"end_date":"2017-08-25","location":"Melbourne, Australia","name":"IJCAI: International Joint Conference on Artificial Intelligence ","start_date":"2017-08-19"},"type":"conference","status":"public","oa_version":"Submitted Version","related_material":{"record":[{"status":"public","id":"6006","relation":"later_version"}]},"date_created":"2018-12-11T11:49:38Z","ddc":["004"],"has_accepted_license":"1","scopus_import":"1","publication_identifier":{"issn":["1045-0823"]},"_id":"1003","day":"30","publication_status":"published"},{"editor":[{"full_name":"Yang, Hongseok","first_name":"Hongseok","last_name":"Yang"}],"scopus_import":"1","publication_identifier":{"issn":["0302-9743"]},"_id":"1011","day":"19","intvolume":" 10201","publication_status":"published","conference":{"name":"ESOP: European Symposium on Programming","start_date":"2017-04-22","location":"Uppsala, Sweden","end_date":"2017-04-29"},"type":"conference","alternative_title":["LNCS"],"oa_version":"Submitted Version","status":"public","arxiv":1,"date_created":"2018-12-11T11:49:41Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","citation":{"ista":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. 2017. Faster algorithms for weighted recursive state machines. ESOP: European Symposium on Programming, LNCS, vol. 10201, 287–313.","apa":"Chatterjee, K., Kragl, B., Mishra, S., & 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. https://doi.org/10.1007/978-3-662-54434-1_11","short":"K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.), Springer, 2017, pp. 287–313.","ama":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. Faster algorithms for weighted recursive state machines. In: Yang H, ed. Vol 10201. Springer; 2017:287-313. doi:10.1007/978-3-662-54434-1_11","mla":"Chatterjee, Krishnendu, et al. Faster Algorithms for Weighted Recursive State Machines. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313, doi:10.1007/978-3-662-54434-1_11.","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. https://doi.org/10.1007/978-3-662-54434-1_11."},"volume":10201,"doi":"10.1007/978-3-662-54434-1_11","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"full_name":"Kragl, Bernhard","orcid":"0000-0001-7745-9117","last_name":"Kragl","id":"320FC952-F248-11E8-B48F-1D18A9856A87","first_name":"Bernhard"},{"full_name":"Mishra, Samarth","last_name":"Mishra","first_name":"Samarth"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"main_file_link":[{"url":"https://arxiv.org/abs/1701.04914","open_access":"1"}],"publist_id":"6384","date_published":"2017-03-19T00:00:00Z","date_updated":"2025-06-04T08:09:18Z","title":"Faster algorithms for weighted recursive state machines","external_id":{"arxiv":["1701.04914"],"isi":["000681702400011"]},"article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"ec_funded":1,"oa":1,"isi":1,"language":[{"iso":"eng"}],"page":"287 - 313","year":"2017","month":"03","publisher":"Springer","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."}],"project":[{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}]},{"abstract":[{"text":"We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates \"almost surely\". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice. Like others, we use variant functions (a.k.a. \"super-martingales\") that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains.","lang":"eng"}],"publisher":"Association for Computing Machinery","oa":1,"month":"12","year":"2017","language":[{"iso":"eng"}],"title":"A new proof rule for almost-sure termination","issue":"POPL","date_updated":"2026-06-18T08:40:04Z","date_published":"2017-12-07T00:00:00Z","main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/3158121","open_access":"1"}],"author":[{"first_name":"Annabelle","last_name":"Mciver","full_name":"Mciver, Annabelle"},{"last_name":"Morgan","first_name":"Carroll","full_name":"Morgan, Carroll"},{"first_name":"Benjamin Lucien","last_name":"Kaminski","full_name":"Kaminski, Benjamin Lucien"},{"orcid":"0000-0002-6143-1926","last_name":"Katoen","id":"4524F760-F248-11E8-B48F-1D18A9856A87","first_name":"Joost P","full_name":"Katoen, Joost P"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"article_processing_charge":"No","external_id":{"arxiv":["1711.03588"]},"citation":{"mla":"Mciver, Annabelle, et al. “A New Proof Rule for Almost-Sure Termination.” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, 33, Association for Computing Machinery, 2017, doi:10.1145/3158121.","ama":"Mciver A, Morgan C, Kaminski BL, Katoen JP. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2017;2(POPL). doi:10.1145/3158121","ista":"Mciver A, Morgan C, Kaminski BL, Katoen JP. 2017. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2(POPL), 33.","apa":"Mciver, A., Morgan, C., Kaminski, B. L., & Katoen, J. P. (2017). A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. Los Angeles, CA, United States: Association for Computing Machinery. https://doi.org/10.1145/3158121","short":"A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM on Programming Languages 2 (2017).","chicago":"Mciver, Annabelle, Carroll Morgan, Benjamin Lucien Kaminski, and Joost P Katoen. “A New Proof Rule for Almost-Sure Termination.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158121.","ieee":"A. Mciver, C. Morgan, B. L. Kaminski, and J. P. Katoen, “A new proof rule for almost-sure termination,” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL. Association for Computing Machinery, 2017."},"volume":2,"article_type":"original","article_number":"33","doi":"10.1145/3158121","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","status":"public","publication":"Proceedings of the ACM on Programming Languages","oa_version":"Published Version","type":"journal_article","conference":{"location":"Los Angeles, CA, United States","name":"POPL: Programming Languages","start_date":"2018-01-07","end_date":"2018-01-13"},"arxiv":1,"date_created":"2021-12-05T23:01:49Z","corr_author":"1","scopus_import":"1","acknowledgement":"McIver and Morgan are grateful to David Basin and the Information Security Group at ETH Zürich for hosting a six-month stay in Switzerland, during part of which this work began. And thanks particularly to Andreas Lochbihler, who shared with us the probabilistic termination problem that led to it. They acknowledge the support of ARC grant DP140101119. Part of this work was carried out during the Workshop on Probabilistic Programming Semantics\r\nat McGill University’s Bellairs Research Institute on Barbados organised by Alexandra Silva and\r\nPrakash Panangaden. Kaminski and Katoen are grateful to Sebastian Junges for spotting a flaw in §5.4.","ddc":["000"],"publication_status":"published","intvolume":" 2","day":"07","_id":"10418","publication_identifier":{"eissn":["2475-1421"]}},{"quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1016/j.ic.2016.10.006","citation":{"ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, “Quantitative fair simulation games,” Information and Computation, vol. 254, no. 2. Elsevier, pp. 143–166, 2017.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner. “Quantitative Fair Simulation Games.” Information and Computation. Elsevier, 2017. https://doi.org/10.1016/j.ic.2016.10.006.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Fair Simulation Games.” Information and Computation, vol. 254, no. 2, Elsevier, 2017, pp. 143–66, doi:10.1016/j.ic.2016.10.006.","ista":"Chatterjee K, Henzinger TA, Otop J, Velner Y. 2017. Quantitative fair simulation games. Information and Computation. 254(2), 143–166.","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., & Velner, Y. (2017). Quantitative fair simulation games. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2016.10.006","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Information and Computation 254 (2017) 143–166.","ama":"Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative fair simulation games. Information and Computation. 2017;254(2):143-166. doi:10.1016/j.ic.2016.10.006"},"volume":254,"article_type":"original","publication_status":"published","OA_place":"publisher","intvolume":" 254","day":"01","_id":"1066","scopus_import":"1","OA_type":"free access","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreements 267989 (QUAREM), 279307 (Graph Games), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE), S11407-N23 (RiSE), P23499-N23, and Microsoft faculty fellows award.","ddc":["000"],"date_created":"2018-12-11T11:49:58Z","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5428"}]},"corr_author":"1","publication":"Information and Computation","status":"public","oa_version":"Published Version","type":"journal_article","month":"06","page":"143 - 166","year":"2017","isi":1,"language":[{"iso":"eng"}],"oa":1,"project":[{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"abstract":[{"lang":"eng","text":"Simulation is an attractive alternative to language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. While fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable in general, whereas the (quantitative) simulation reduces to quantitative games, which admit pseudo-polynomial time algorithms.\r\n\r\nIn this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games, yet they still admit pseudo-polynomial time algorithms."}],"publisher":"Elsevier","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"article_processing_charge":"No","external_id":{"isi":["000402025600002"]},"issue":"2","title":"Quantitative fair simulation games","date_updated":"2026-06-18T08:47:01Z","date_published":"2017-06-01T00:00:00Z","publist_id":"6322","main_file_link":[{"url":"https://doi.org/10.1016/j.ic.2016.10.006","open_access":"1"}],"author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Otop","full_name":"Otop, Jan"},{"first_name":"Yaron","last_name":"Velner","full_name":"Velner, Yaron"}],"ec_funded":1},{"oa":1,"month":"07","page":"376 - 379 ","year":"2017","language":[{"iso":"eng"}],"isi":1,"abstract":[{"text":"Recently there has been a proliferation of automated program repair (APR) techniques, targeting various programming languages. Such techniques can be generally classified into two families: syntactic- and semantics-based. Semantics-based APR, on which we focus, typically uses symbolic execution to infer semantic constraints and then program synthesis to construct repairs conforming to them. While syntactic-based APR techniques have been shown successful on bugs in real-world programs written in both C and Java, semantics-based APR techniques mostly target C programs. This leaves empirical comparisons of the APR families not fully explored, and developers without a Java-based semantics APR technique. We present JFix, a semantics-based APR framework that targets Java, and an associated Eclipse plugin. JFix is implemented atop Symbolic PathFinder, a well-known symbolic execution engine for Java programs. It extends one particular APR technique (Angelix), and is designed to be sufficiently generic to support a variety of such techniques. We demonstrate that semantics-based APR can indeed efficiently and effectively repair a variety of classes of bugs in large real-world Java programs. This supports our claim that the framework can both support developers seeking semantics-based repair of bugs in Java programs, as well as enable larger scale empirical studies comparing syntactic- and semantics-based APR targeting Java. The demonstration of our tool is available via the project website at: https://xuanbachle.github.io/semanticsrepair/ ","lang":"eng"}],"publisher":"ACM","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"}],"date_updated":"2026-06-18T19:51:19Z","title":"JFIX: Semantics-based repair of Java programs via symbolic PathFinder","publist_id":"6478","date_published":"2017-07-10T00:00:00Z","author":[{"full_name":"Le, Xuan","last_name":"Le","first_name":"Xuan"},{"full_name":"Chu, Duc Hiep","last_name":"Chu","first_name":"Duc Hiep","id":"3598E630-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Lo, David","first_name":"David","last_name":"Lo"},{"full_name":"Le Goues, Claire","first_name":"Claire","last_name":"Le Goues"},{"full_name":"Visser, Willem","first_name":"Willem","last_name":"Visser"}],"main_file_link":[{"open_access":"1","url":"https://core.ac.uk/download/pdf/111759662.pdf"}],"department":[{"_id":"ToHe"}],"article_processing_charge":"No","external_id":{"isi":["000462903600038"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","citation":{"ieee":"X. Le, D. H. Chu, D. Lo, C. Le Goues, and W. Visser, “JFIX: Semantics-based repair of Java programs via symbolic PathFinder,” in Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, Santa Barbara, CA, United States, 2017, pp. 376–379.","chicago":"Le, Xuan, Duc Hiep Chu, David Lo, Claire Le Goues, and Willem Visser. “JFIX: Semantics-Based Repair of Java Programs via Symbolic PathFinder.” In Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, 376–79. ACM, 2017. https://doi.org/10.1145/3092703.3098225.","ista":"Le X, Chu DH, Lo D, Le Goues C, Visser W. 2017. JFIX: Semantics-based repair of Java programs via symbolic PathFinder. Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis. ISSTA: International Symposium on Software Testing and Analysis, 376–379.","apa":"Le, X., Chu, D. H., Lo, D., Le Goues, C., & Visser, W. (2017). JFIX: Semantics-based repair of Java programs via symbolic PathFinder. In Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (pp. 376–379). Santa Barbara, CA, United States: ACM. https://doi.org/10.1145/3092703.3098225","short":"X. Le, D.H. Chu, D. Lo, C. Le Goues, W. Visser, in:, Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, ACM, 2017, pp. 376–379.","ama":"Le X, Chu DH, Lo D, Le Goues C, Visser W. JFIX: Semantics-based repair of Java programs via symbolic PathFinder. In: Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis. ACM; 2017:376-379. doi:10.1145/3092703.3098225","mla":"Le, Xuan, et al. “JFIX: Semantics-Based Repair of Java Programs via Symbolic PathFinder.” Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, ACM, 2017, pp. 376–79, doi:10.1145/3092703.3098225."},"doi":"10.1145/3092703.3098225","scopus_import":"1","acknowledgement":"We thank Vu Le (Microsoft Research, Redmond), and anonymous reviewers for their comments. Duc-Hiep Chu was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).","ddc":["000"],"publication_status":"published","day":"10","_id":"941","status":"public","publication":"Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis","oa_version":"Published Version","type":"conference","conference":{"start_date":"2017-07-10","name":"ISSTA: International Symposium on Software Testing and Analysis","location":"Santa Barbara, CA, United States","end_date":"2017-07-14"},"date_created":"2018-12-11T11:49:19Z","corr_author":"1"},{"author":[{"last_name":"Le","first_name":"Xuan","full_name":"Le, Xuan"},{"full_name":"Chu, Duc Hiep","last_name":"Chu","first_name":"Duc Hiep","id":"3598E630-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Lo","first_name":"David","full_name":"Lo, David"},{"last_name":"Le Goues","first_name":"Claire","full_name":"Le Goues, Claire"},{"full_name":"Visser, Willem","first_name":"Willem","last_name":"Visser"}],"publist_id":"6477","date_published":"2017-09-01T00:00:00Z","date_updated":"2025-04-15T06:25:57Z","title":"S3: Syntax- and semantic-guided repair synthesis via programming by examples","external_id":{"isi":["000414279300055"]},"article_processing_charge":"No","department":[{"_id":"ToHe"}],"publisher":"ACM","abstract":[{"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. ","lang":"eng"}],"project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"language":[{"iso":"eng"}],"isi":1,"page":"593 - 604","month":"09","year":"2017","conference":{"end_date":"2017-09-08","start_date":"2017-09-04","name":"FSE: Foundations of Software Engineering","location":"Paderborn, Germany"},"type":"conference","oa_version":"None","status":"public","date_created":"2018-12-11T11:49:19Z","scopus_import":"1","publication_identifier":{"isbn":["978-145035105-8"]},"_id":"942","day":"01","publication_status":"published","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. https://doi.org/10.1145/3106237.3106309.","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.","apa":"Le, X., Chu, D. H., Lo, D., Le Goues, C., & 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. https://doi.org/10.1145/3106237.3106309","short":"X. Le, D.H. Chu, D. Lo, C. Le Goues, W. Visser, in:, ACM, 2017, pp. 593–604.","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:10.1145/3106237.3106309","mla":"Le, Xuan, et al. S3: Syntax- and Semantic-Guided Repair Synthesis via Programming by Examples. Vol. F130154, ACM, 2017, pp. 593–604, doi:10.1145/3106237.3106309."},"volume":"F130154","doi":"10.1145/3106237.3106309","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","quality_controlled":"1"},{"project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","pubrep_id":"844","abstract":[{"lang":"eng","text":"Two-player games on graphs are widely studied in formal methods as they model the interaction between a system and its environment. The game is played by moving a token throughout a graph to produce an infinite path. There are several common modes to determine how the players move the token through the graph; e.g., in turn-based games the players alternate turns in moving the token. We study the bidding mode of moving the token, which, to the best of our knowledge, has never been studied in infinite-duration games. Both players have separate budgets, which sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously, and a bid is legal if it does not exceed the available budget. The winner of the bidding pays his bid to the other player and moves the token. For reachability objectives, repeated bidding games have been studied and are called Richman games. There, a central question is the existence and computation of threshold budgets; namely, a value t\\in [0,1] such that if\\PO's budget exceeds $t$, he can win the game, and if\\PT's budget exceeds 1-t, he can win the game. We focus on parity games and mean-payoff games. We show the existence of threshold budgets in these games, and reduce the problem of finding them to Richman games. We also determine the strategy-complexity of an optimal strategy. Our most interesting result shows that memoryless strategies suffice for mean-payoff bidding games. \r\n"}],"language":[{"iso":"eng"}],"year":"2017","month":"09","oa":1,"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"external_id":{"arxiv":["1705.01433"]},"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publist_id":"6466","date_published":"2017-09-01T00:00:00Z","author":[{"full_name":"Avni, Guy","last_name":"Avni","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Guy"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chonev","first_name":"Ventsislav K","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87","full_name":"Chonev, Ventsislav K"}],"title":"Infinite-duration bidding games","date_updated":"2025-07-10T11:53:48Z","doi":"10.4230/LIPIcs.CONCUR.2017.21","article_number":"17","volume":85,"citation":{"ieee":"G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,” presented at the CONCUR: Concurrency Theory, Berlin, Germany, 2017, vol. 85.","chicago":"Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration Bidding Games,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.CONCUR.2017.21.","apa":"Avni, G., Henzinger, T. A., & Chonev, V. K. (2017). Infinite-duration bidding games (Vol. 85). Presented at the CONCUR: Concurrency Theory, Berlin, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2017.21","short":"G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ista":"Avni G, Henzinger TA, Chonev VK. 2017. Infinite-duration bidding games. CONCUR: Concurrency Theory, LIPIcs, vol. 85, 17.","ama":"Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. In: Vol 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.CONCUR.2017.21","mla":"Avni, Guy, et al. Infinite-Duration Bidding Games. Vol. 85, 17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.CONCUR.2017.21."},"quality_controlled":"1","file_date_updated":"2020-07-14T12:48:16Z","file":[{"access_level":"open_access","date_created":"2018-12-12T10:18:00Z","creator":"system","file_name":"IST-2017-844-v1+1_concur-cr.pdf","file_size":335170,"date_updated":"2020-07-14T12:48:16Z","checksum":"6d5cccf755207b91ccbef95d8275b013","content_type":"application/pdf","relation":"main_file","file_id":"5318"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","id":"6752","relation":"later_version"}]},"date_created":"2018-12-11T11:49:22Z","arxiv":1,"alternative_title":["LIPIcs"],"type":"conference","conference":{"location":"Berlin, Germany","name":"CONCUR: Concurrency Theory","start_date":"2017-09-05","end_date":"2017-09-07"},"status":"public","oa_version":"Published Version","_id":"950","publication_identifier":{"issn":["1868-8969"]},"publication_status":"published","day":"01","intvolume":" 85","has_accepted_license":"1","ddc":["000"],"scopus_import":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."}],"publisher":"Springer","project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"year":"2017","month":"01","page":"399 - 418","language":[{"iso":"eng"}],"isi":1,"date_updated":"2026-04-16T09:58:05Z","title":"Model counting for recursively-defined strings","author":[{"full_name":"Trinh, Minh","last_name":"Trinh","first_name":"Minh"},{"full_name":"Chu, Duc Hiep","id":"3598E630-F248-11E8-B48F-1D18A9856A87","first_name":"Duc Hiep","last_name":"Chu"},{"full_name":"Jaffar, Joxan","first_name":"Joxan","last_name":"Jaffar"}],"publist_id":"6443","date_published":"2017-01-01T00:00:00Z","department":[{"_id":"ToHe"}],"external_id":{"isi":["000431900900021"]},"article_processing_charge":"No","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. https://doi.org/10.1007/978-3-319-63390-9_21.","mla":"Trinh, Minh, et al. Model Counting for Recursively-Defined Strings. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer, 2017, pp. 399–418, doi:10.1007/978-3-319-63390-9_21.","ista":"Trinh M, Chu DH, Jaffar J. 2017. Model counting for recursively-defined strings. CAV: Computer Aided Verification, LNCS, vol. 10427, 399–418.","apa":"Trinh, M., Chu, D. H., & Jaffar, J. (2017). Model counting for recursively-defined strings. In R. Majumdar & V. Kunčak (Eds.) (Vol. 10427, pp. 399–418). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63390-9_21","short":"M. Trinh, D.H. Chu, J. Jaffar, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 399–418.","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:10.1007/978-3-319-63390-9_21"},"volume":10427,"doi":"10.1007/978-3-319-63390-9_21","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","quality_controlled":"1","oa_version":"None","status":"public","conference":{"end_date":"2017-07-28","name":"CAV: Computer Aided Verification","start_date":"2017-07-24","location":"Heidelberg, Germany"},"type":"conference","alternative_title":["LNCS"],"date_created":"2018-12-11T11:49:26Z","scopus_import":"1","editor":[{"first_name":"Rupak","last_name":"Majumdar","full_name":"Majumdar, Rupak"},{"full_name":"Kunčak, Viktor","last_name":"Kunčak","first_name":"Viktor"}],"day":"01","intvolume":" 10427","publication_status":"published","publication_identifier":{"issn":["0302-9743"]},"_id":"962"},{"file":[{"checksum":"f55eaf7f3c36ea07801112acfedd17d5","file_size":369730,"date_updated":"2020-07-14T12:48:18Z","file_id":"5059","content_type":"application/pdf","relation":"main_file","access_level":"open_access","creator":"system","file_name":"IST-2017-829-v1+1_mfcs-cr.pdf","date_created":"2018-12-12T10:14:10Z"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2020-07-14T12:48:18Z","quality_controlled":"1","volume":83,"citation":{"ieee":"G. Avni, S. Guha, and O. Kupferman, “Timed network games with clocks,” presented at the MFCS: Mathematical Foundations of Computer Science, 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. https://doi.org/10.4230/LIPIcs.MFCS.2017.37.","ista":"Avni G, Guha S, Kupferman O. 2017. Timed network games with clocks. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 83, 37.","apa":"Avni, G., Guha, S., & Kupferman, O. (2017). Timed network games with clocks (Vol. 83). Presented at the MFCS: Mathematical Foundations of Computer Science, Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2017.37","short":"G. Avni, S. Guha, O. Kupferman, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ama":"Avni G, Guha S, Kupferman O. Timed network games with clocks. In: Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.MFCS.2017.37","mla":"Avni, Guy, et al. Timed Network Games with Clocks. Vol. 83, 37, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.MFCS.2017.37."},"article_number":"37","doi":"10.4230/LIPIcs.MFCS.2017.37","scopus_import":"1","has_accepted_license":"1","ddc":["004"],"publication_status":"published","day":"01","intvolume":" 83","_id":"963","publication_identifier":{"issn":["1868-8969"]},"oa_version":"Published Version","status":"public","type":"conference","alternative_title":["LIPIcs"],"conference":{"end_date":"2017-08-25","start_date":"2017-08-21","name":"MFCS: Mathematical Foundations of Computer Science","location":"Aalborg, Denmark"},"date_created":"2018-12-11T11:49:26Z","related_material":{"record":[{"id":"6005","status":"public","relation":"later_version"}]},"oa":1,"year":"2017","month":"06","language":[{"iso":"eng"}],"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. "}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","pubrep_id":"829","project":[{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"date_updated":"2025-07-10T12:01:59Z","title":"Timed network games with clocks","date_published":"2017-06-01T00:00:00Z","publist_id":"6438","author":[{"full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Guy"},{"full_name":"Guha, Shibashis","first_name":"Shibashis","last_name":"Guha"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"department":[{"_id":"ToHe"}],"article_processing_charge":"No","tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"}},{"has_accepted_license":"1","date_published":"2017-08-04T00:00:00Z","author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"full_name":"Kragl, Bernhard","first_name":"Bernhard","id":"320FC952-F248-11E8-B48F-1D18A9856A87","last_name":"Kragl","orcid":"0000-0001-7745-9117"},{"first_name":"Shaz","last_name":"Qadeer","full_name":"Qadeer, Shaz"}],"ddc":["000"],"title":"Synchronizing the asynchronous","date_updated":"2025-04-15T08:11:53Z","_id":"6426","publication_identifier":{"issn":["2664-1690"]},"publication_status":"published","day":"04","department":[{"_id":"ToHe"}],"alternative_title":["IST Austria Technical Report"],"type":"technical_report","status":"public","oa_version":"Published Version","related_material":{"record":[{"relation":"later_version","status":"public","id":"133"}]},"date_created":"2019-05-13T08:15:55Z","file":[{"creator":"dernst","file_name":"main(1).pdf","date_created":"2019-05-13T08:14:44Z","access_level":"open_access","file_id":"6431","content_type":"application/pdf","relation":"main_file","checksum":"b48d42725182d7ca10107a118815f4cf","file_size":971347,"date_updated":"2020-07-14T12:47:30Z"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"language":[{"iso":"eng"}],"page":"28","file_date_updated":"2020-07-14T12:47:30Z","month":"08","year":"2017","publisher":"IST Austria","citation":{"ama":"Henzinger TA, Kragl B, Qadeer S. Synchronizing the Asynchronous. IST Austria; 2017. doi:10.15479/AT:IST-2018-853-v2-2","apa":"Henzinger, T. A., Kragl, B., & Qadeer, S. (2017). Synchronizing the asynchronous. IST Austria. https://doi.org/10.15479/AT:IST-2018-853-v2-2","short":"T.A. Henzinger, B. Kragl, S. Qadeer, Synchronizing the Asynchronous, IST Austria, 2017.","ista":"Henzinger TA, Kragl B, Qadeer S. 2017. Synchronizing the asynchronous, IST Austria, 28p.","mla":"Henzinger, Thomas A., et al. Synchronizing the Asynchronous. IST Austria, 2017, doi:10.15479/AT:IST-2018-853-v2-2.","chicago":"Henzinger, Thomas A, Bernhard Kragl, and Shaz Qadeer. Synchronizing the Asynchronous. IST Austria, 2017. https://doi.org/10.15479/AT:IST-2018-853-v2-2.","ieee":"T. A. Henzinger, B. Kragl, and S. Qadeer, Synchronizing the asynchronous. IST Austria, 2017."},"abstract":[{"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 asynchronous computation threads. We show that specifications and correctness proofs for asynchronous programs can be structured by introducing the fiction, for proof purposes, that intermediate, non-quiescent states of asynchronous operations can be ignored. Then, the task of specification becomes relatively simple and the task of verification can be naturally decomposed into smaller sub-tasks. The sub-tasks iteratively summarize, guided by the structure of an asynchronous program, the atomic effect of non-atomic operations and the synchronous effect of asynchronous operations. This structuring of specifications and proofs corresponds to the introduction of multiple layers of stepwise refinement for asynchronous programs. We present the first proof rule, called synchronization, to reduce asynchronous invocations on a lower layer to synchronous invocations on a higher layer. We implemented our proof method in CIVL and evaluated it on a collection of benchmark programs.","lang":"eng"}],"doi":"10.15479/AT:IST-2018-853-v2-2"},{"file_date_updated":"2020-07-14T12:47:31Z","quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","file":[{"relation":"main_file","content_type":"application/pdf","file_id":"4956","date_updated":"2020-07-14T12:47:31Z","file_size":3806864,"checksum":"faf546914ba29bcf9974ee36b6b16750","date_created":"2018-12-12T10:12:38Z","file_name":"IST-2017-831-v1+1_main.pdf","creator":"system","access_level":"open_access"}],"doi":"10.1007/978-3-319-65765-3_7","volume":"10419 ","citation":{"chicago":"Bogomolov, Sergiy, Mirco Giacobbe, Thomas A Henzinger, and Hui Kong. “Conic Abstractions for Hybrid Systems,” 10419:116–32. Springer, 2017. https://doi.org/10.1007/978-3-319-65765-3_7.","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.","mla":"Bogomolov, Sergiy, et al. Conic Abstractions for Hybrid Systems. Vol. 10419, Springer, 2017, pp. 116–32, doi:10.1007/978-3-319-65765-3_7.","ama":"Bogomolov S, Giacobbe M, Henzinger TA, Kong H. Conic abstractions for hybrid systems. In: Vol 10419. Springer; 2017:116-132. doi:10.1007/978-3-319-65765-3_7","apa":"Bogomolov, S., Giacobbe, M., Henzinger, T. A., & 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. https://doi.org/10.1007/978-3-319-65765-3_7","short":"S. Bogomolov, M. Giacobbe, T.A. Henzinger, H. Kong, in:, Springer, 2017, pp. 116–132.","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."},"day":"01","publication_status":"published","publication_identifier":{"isbn":["978-331965764-6"]},"_id":"647","scopus_import":"1","ddc":["005"],"has_accepted_license":"1","date_created":"2018-12-11T11:47:41Z","corr_author":"1","related_material":{"record":[{"status":"public","id":"6894","relation":"dissertation_contains"}]},"oa_version":"Submitted Version","status":"public","conference":{"location":"Berlin, Germany","start_date":"2017-09-05","name":"FORMATS: Formal Modelling and Analysis of Timed Systems","end_date":"2017-09-07"},"alternative_title":["LNCS"],"type":"conference","month":"09","year":"2017","page":"116 - 132","language":[{"iso":"eng"}],"isi":1,"oa":1,"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","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"}],"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."}],"pubrep_id":"831","publisher":"Springer","department":[{"_id":"ToHe"}],"external_id":{"isi":["000611678300007"]},"article_processing_charge":"No","title":"Conic abstractions for hybrid systems","date_updated":"2026-04-08T07:47:13Z","author":[{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy","orcid":"0000-0002-0686-0365","last_name":"Bogomolov","full_name":"Bogomolov, Sergiy"},{"id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","first_name":"Mirco","orcid":"0000-0001-8180-0904","last_name":"Giacobbe","full_name":"Giacobbe, Mirco"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","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"}],"date_published":"2017-09-01T00:00:00Z","publist_id":"7129"},{"doi":"10.1145/3049797.3049814","citation":{"ista":"Kong H, Bogomolov S, Schilling C, Jiang Y, Henzinger TA. 2017. Safety verification of nonlinear hybrid systems based on invariant clusters. Proceedings of the 20th International Conference on Hybrid Systems. HSCC: Hybrid Systems - Computation and Control , 163–172.","short":"H. Kong, S. Bogomolov, C. Schilling, Y. Jiang, T.A. Henzinger, in:, Proceedings of the 20th International Conference on Hybrid Systems, ACM, 2017, pp. 163–172.","apa":"Kong, H., Bogomolov, S., Schilling, C., Jiang, Y., & Henzinger, T. A. (2017). Safety verification of nonlinear hybrid systems based on invariant clusters. In Proceedings of the 20th International Conference on Hybrid Systems (pp. 163–172). Pittsburgh, PA, United States: ACM. https://doi.org/10.1145/3049797.3049814","ama":"Kong H, Bogomolov S, Schilling C, Jiang Y, Henzinger TA. Safety verification of nonlinear hybrid systems based on invariant clusters. In: Proceedings of the 20th International Conference on Hybrid Systems. ACM; 2017:163-172. doi:10.1145/3049797.3049814","mla":"Kong, Hui, et al. “Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters.” Proceedings of the 20th International Conference on Hybrid Systems, ACM, 2017, pp. 163–72, doi:10.1145/3049797.3049814.","ieee":"H. Kong, S. Bogomolov, C. Schilling, Y. Jiang, and T. A. Henzinger, “Safety verification of nonlinear hybrid systems based on invariant clusters,” in Proceedings of the 20th International Conference on Hybrid Systems, Pittsburgh, PA, United States, 2017, pp. 163–172.","chicago":"Kong, Hui, Sergiy Bogomolov, Christian Schilling, Yu Jiang, and Thomas A Henzinger. “Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters.” In Proceedings of the 20th International Conference on Hybrid Systems, 163–72. ACM, 2017. https://doi.org/10.1145/3049797.3049814."},"quality_controlled":"1","file_date_updated":"2020-07-14T12:47:34Z","file":[{"file_id":"4873","content_type":"application/pdf","relation":"main_file","checksum":"b7667434cbf5b5f0ade3bea1dbe5bf63","file_size":1650530,"date_updated":"2020-07-14T12:47:34Z","creator":"system","file_name":"IST-2017-817-v1+1_p163-kong.pdf","date_created":"2018-12-12T10:11:20Z","access_level":"open_access"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2018-12-11T11:47:47Z","type":"conference","conference":{"end_date":"2017-04-20","start_date":"2017-04-18","name":"HSCC: Hybrid Systems - Computation and Control ","location":"Pittsburgh, PA, United States"},"oa_version":"Submitted Version","status":"public","publication":"Proceedings of the 20th International Conference on Hybrid Systems","_id":"663","publication_identifier":{"isbn":["978-145034590-3"]},"publication_status":"published","day":"01","has_accepted_license":"1","ddc":["000"],"scopus_import":"1","publisher":"ACM","pubrep_id":"817","abstract":[{"text":"In this paper, we propose an approach to automatically compute invariant clusters for nonlinear semialgebraic hybrid systems. An invariant cluster for an ordinary differential equation (ODE) is a multivariate polynomial invariant g(u→, x→) = 0, parametric in u→, which can yield an infinite number of concrete invariants by assigning different values to u→ so that every trajectory of the system can be overapproximated precisely by the intersection of a group of concrete invariants. For semialgebraic systems, which involve ODEs with multivariate polynomial right-hand sides, given a template multivariate polynomial g(u→, x→), an invariant cluster can be obtained by first computing the remainder of the Lie derivative of g(u→, x→) divided by g(u→, x→) and then solving the system of polynomial equations obtained from the coefficients of the remainder. Based on invariant clusters and sum-of-squares (SOS) programming, we present a new method for the safety verification of hybrid systems. Experiments on nonlinear benchmark systems from biology and control theory show that our approach is efficient. ","lang":"eng"}],"language":[{"iso":"eng"}],"isi":1,"page":"163 - 172","month":"04","year":"2017","oa":1,"article_processing_charge":"No","external_id":{"isi":["000615962400019"]},"department":[{"_id":"ToHe"}],"date_published":"2017-04-01T00:00:00Z","publist_id":"7067","author":[{"first_name":"Hui","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941","last_name":"Kong","full_name":"Kong, Hui"},{"orcid":"0000-0002-0686-0365","last_name":"Bogomolov","first_name":"Sergiy","full_name":"Bogomolov, Sergiy"},{"full_name":"Schilling, Christian","last_name":"Schilling","first_name":"Christian"},{"first_name":"Yu","last_name":"Jiang","full_name":"Jiang, Yu"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"date_updated":"2025-09-11T07:06:15Z","title":"Safety verification of nonlinear hybrid systems based on invariant clusters"},{"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_published":"2017-08-01T00:00:00Z","publist_id":"6976","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan"}],"title":"Bidirectional nested weighted automata","date_updated":"2025-07-10T11:54:15Z","pubrep_id":"886","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","abstract":[{"lang":"eng","text":"Nested weighted automata (NWA) present a robust and convenient automata-theoretic formalism for quantitative specifications. Previous works have considered NWA that processed input words only in the forward direction. It is natural to allow the automata to process input words backwards as well, for example, to measure the maximal or average time between a response and the preceding request. We therefore introduce and study bidirectional NWA that can process input words in both directions. First, we show that bidirectional NWA can express interesting quantitative properties that are not expressible by forward-only NWA. Second, for the fundamental decision problems of emptiness and universality, we establish decidability and complexity results for the new framework which match the best-known results for the special case of forward-only NWA. Thus, for NWA, the increased expressiveness of bidirectionality is achieved at no additional computational complexity. This is in stark contrast to the unweighted case, where bidirectional finite automata are no more expressive but exponentially more succinct than their forward-only counterparts."}],"language":[{"iso":"eng"}],"month":"08","year":"2017","oa":1,"corr_author":"1","date_created":"2018-12-11T11:48:04Z","alternative_title":["LIPIcs"],"type":"conference","conference":{"start_date":"2017-09-05","name":"28th International Conference on Concurrency Theory, CONCUR","location":"Berlin, Germany","end_date":"2017-09-08"},"status":"public","oa_version":"Published Version","_id":"711","publication_identifier":{"issn":["1868-8969"]},"publication_status":"published","intvolume":" 85","day":"01","has_accepted_license":"1","ddc":["004","005"],"scopus_import":"1","doi":"10.4230/LIPIcs.CONCUR.2017.5","article_number":"5","volume":85,"citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Bidirectional Nested Weighted Automata,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.CONCUR.2017.5.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Bidirectional nested weighted automata,” presented at the 28th International Conference on Concurrency Theory, CONCUR, Berlin, Germany, 2017, vol. 85.","ama":"Chatterjee K, Henzinger TA, Otop J. Bidirectional nested weighted automata. In: Vol 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.CONCUR.2017.5","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2017). Bidirectional nested weighted automata (Vol. 85). Presented at the 28th International Conference on Concurrency Theory, CONCUR, Berlin, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2017.5","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ista":"Chatterjee K, Henzinger TA, Otop J. 2017. Bidirectional nested weighted automata. 28th International Conference on Concurrency Theory, CONCUR, LIPIcs, vol. 85, 5.","mla":"Chatterjee, Krishnendu, et al. Bidirectional Nested Weighted Automata. Vol. 85, 5, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.CONCUR.2017.5."},"quality_controlled":"1","file_date_updated":"2020-07-14T12:47:49Z","file":[{"relation":"main_file","content_type":"application/pdf","file_id":"4661","date_updated":"2020-07-14T12:47:49Z","file_size":570294,"checksum":"d2bda4783821a6358333fe27f11f4737","date_created":"2018-12-12T10:08:02Z","file_name":"IST-2017-886-v1+1_LIPIcs-CONCUR-2017-5.pdf","creator":"system","access_level":"open_access"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"abstract":[{"text":"This special issue of the Journal on Formal Methods in System Design is dedicated to Prof. Helmut Veith, who unexpectedly passed away in March 2016. Helmut Veith was a brilliant researcher, inspiring collaborator, passionate mentor, generous friend, and valued member of the formal methods community. Helmut was not only known for his numerous and influential contributions in the field of automated verification (most prominently his work on Counterexample-Guided Abstraction Refinement [1,2]), but also for his untiring and passionate efforts for the logic community: he co-organized the Vienna Summer of Logic (an event comprising twelve conferences and numerous workshops which attracted thousands of researchers from all over the world), he initiated the Vienna Center for Logic and Algorithms (which promotes international collaboration on logic and algorithms and organizes outreach events such as the LogicLounge), and he coordinated the Doctoral Program on Logical Methods in Computer Science at TU Wien (currently educating more than 40 doctoral students) and a National Research Network on Rigorous Systems Engineering (uniting fifteen researchers in Austria to address the challenge of building reliable and safe computer\r\nsystems). With his enthusiasm and commitment, Helmut completely reshaped the Austrian research landscape in the field of logic and verification in his few years as a full professor at TU Wien.","lang":"eng"}],"citation":{"chicago":"Gottlob, Georg, Thomas A Henzinger, and Georg Weißenbacher. “Preface of the Special Issue in Memoriam Helmut Veith.” Formal Methods in System Design. Springer, 2017. https://doi.org/10.1007/s10703-017-0307-6.","ieee":"G. Gottlob, T. A. Henzinger, and G. Weißenbacher, “Preface of the special issue in memoriam Helmut Veith,” Formal Methods in System Design, vol. 51, no. 2. Springer, pp. 267–269, 2017.","ama":"Gottlob G, Henzinger TA, Weißenbacher G. Preface of the special issue in memoriam Helmut Veith. Formal Methods in System Design. 2017;51(2):267-269. doi:10.1007/s10703-017-0307-6","ista":"Gottlob G, Henzinger TA, Weißenbacher G. 2017. Preface of the special issue in memoriam Helmut Veith. Formal Methods in System Design. 51(2), 267–269.","apa":"Gottlob, G., Henzinger, T. A., & Weißenbacher, G. (2017). Preface of the special issue in memoriam Helmut Veith. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-017-0307-6","short":"G. Gottlob, T.A. Henzinger, G. Weißenbacher, Formal Methods in System Design 51 (2017) 267–269.","mla":"Gottlob, Georg, et al. “Preface of the Special Issue in Memoriam Helmut Veith.” Formal Methods in System Design, vol. 51, no. 2, Springer, 2017, pp. 267–69, doi:10.1007/s10703-017-0307-6."},"volume":51,"publisher":"Springer","doi":"10.1007/s10703-017-0307-6","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","year":"2017","month":"11","page":"267 - 269","isi":1,"quality_controlled":"1","language":[{"iso":"eng"}],"oa_version":"None","status":"public","publication":"Formal Methods in System Design","type":"journal_article","date_created":"2018-12-11T11:48:16Z","title":"Preface of the special issue in memoriam Helmut Veith","date_updated":"2023-09-27T12:29:29Z","issue":"2","author":[{"first_name":"Georg","last_name":"Gottlob","full_name":"Gottlob, Georg"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Weißenbacher, Georg","last_name":"Weißenbacher","first_name":"Georg"}],"date_published":"2017-11-14T00:00:00Z","publist_id":"6924","intvolume":" 51","department":[{"_id":"ToHe"}],"day":"14","publication_status":"published","external_id":{"isi":["000415615600001"]},"article_processing_charge":"No","_id":"743"}]