[{"volume":"F130154","isi":1,"date_updated":"2023-09-26T15:38:36Z","project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"}],"page":"593 - 604","quality_controlled":"1","date_created":"2018-12-11T11:49:19Z","year":"2017","scopus_import":"1","publication_identifier":{"isbn":["978-145035105-8"]},"article_processing_charge":"No","type":"conference","language":[{"iso":"eng"}],"publisher":"ACM","doi":"10.1145/3106237.3106309","author":[{"full_name":"Le, Xuan","first_name":"Xuan","last_name":"Le"},{"first_name":"Duc Hiep","full_name":"Chu, Duc Hiep","last_name":"Chu","id":"3598E630-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Lo","full_name":"Lo, David","first_name":"David"},{"last_name":"Le Goues","first_name":"Claire","full_name":"Le Goues, Claire"},{"last_name":"Visser","first_name":"Willem","full_name":"Visser, Willem"}],"publist_id":"6477","date_published":"2017-09-01T00:00:00Z","external_id":{"isi":["000414279300055"]},"conference":{"name":"FSE: Foundations of Software Engineering","start_date":"2017-09-04","location":"Paderborn, Germany","end_date":"2017-09-08"},"oa_version":"None","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"}],"status":"public","citation":{"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:<a href=\"https://doi.org/10.1145/3106237.3106309\">10.1145/3106237.3106309</a>","apa":"Le, X., Chu, D. H., Lo, D., Le Goues, C., &#38; Visser, W. (2017). S3: Syntax- and semantic-guided repair synthesis via programming by examples (Vol. F130154, pp. 593–604). Presented at the FSE: Foundations of Software Engineering, Paderborn, Germany: ACM. <a href=\"https://doi.org/10.1145/3106237.3106309\">https://doi.org/10.1145/3106237.3106309</a>","ista":"Le X, Chu DH, Lo D, Le Goues C, Visser W. 2017. S3: Syntax- and semantic-guided repair synthesis via programming by examples. FSE: Foundations of Software Engineering vol. F130154, 593–604.","chicago":"Le, Xuan, Duc Hiep Chu, David Lo, Claire Le Goues, and Willem Visser. “S3: Syntax- and Semantic-Guided Repair Synthesis via Programming by Examples,” F130154:593–604. ACM, 2017. <a href=\"https://doi.org/10.1145/3106237.3106309\">https://doi.org/10.1145/3106237.3106309</a>.","mla":"Le, Xuan, et al. <i>S3: Syntax- and Semantic-Guided Repair Synthesis via Programming by Examples</i>. Vol. F130154, ACM, 2017, pp. 593–604, doi:<a href=\"https://doi.org/10.1145/3106237.3106309\">10.1145/3106237.3106309</a>.","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."},"day":"01","title":"S3: Syntax- and semantic-guided repair synthesis via programming by examples","publication_status":"published","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"942","month":"09","department":[{"_id":"ToHe"}]},{"related_material":{"record":[{"id":"6752","status":"public","relation":"later_version"}]},"title":"Infinite-duration bidding games","oa":1,"publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"950","month":"09","pubrep_id":"844","alternative_title":["LIPIcs"],"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"abstract":[{"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","lang":"eng"}],"article_number":"17","status":"public","citation":{"ista":"Avni G, Henzinger TA, Chonev VK. 2017. Infinite-duration bidding games. CONCUR: Concurrency Theory, LIPIcs, vol. 85, 17.","apa":"Avni, G., Henzinger, T. A., &#38; 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. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2017.21</a>","chicago":"Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration Bidding Games,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2017.21</a>.","mla":"Avni, Guy, et al. <i>Infinite-Duration Bidding Games</i>. Vol. 85, 17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.21\">10.4230/LIPIcs.CONCUR.2017.21</a>.","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.","short":"G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ama":"Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. In: Vol 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.21\">10.4230/LIPIcs.CONCUR.2017.21</a>"},"intvolume":"        85","has_accepted_license":"1","day":"01","file_date_updated":"2020-07-14T12:48:16Z","type":"conference","arxiv":1,"language":[{"iso":"eng"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","doi":"10.4230/LIPIcs.CONCUR.2017.21","ddc":["000"],"author":[{"orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","full_name":"Avni, Guy","first_name":"Guy"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Chonev, Ventsislav K","first_name":"Ventsislav K","last_name":"Chonev","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"6466","date_published":"2017-09-01T00:00:00Z","license":"https://creativecommons.org/licenses/by/4.0/","conference":{"start_date":"2017-09-05","name":"CONCUR: Concurrency Theory","end_date":"2017-09-07","location":"Berlin, Germany"},"external_id":{"arxiv":["1705.01433"]},"oa_version":"Published Version","volume":85,"file":[{"checksum":"6d5cccf755207b91ccbef95d8275b013","relation":"main_file","creator":"system","file_size":335170,"file_name":"IST-2017-844-v1+1_concur-cr.pdf","access_level":"open_access","date_updated":"2020-07-14T12:48:16Z","content_type":"application/pdf","date_created":"2018-12-12T10:18:00Z","file_id":"5318"}],"date_updated":"2023-08-29T07:02:13Z","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"quality_controlled":"1","date_created":"2018-12-11T11:49:22Z","year":"2017","scopus_import":1,"publication_identifier":{"issn":["1868-8969"]},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"}},{"department":[{"_id":"ToHe"}],"alternative_title":["LNCS"],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"962","month":"01","title":"Model counting for recursively-defined strings","publication_status":"published","day":"01","intvolume":"     10427","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.","mla":"Trinh, Minh, et al. <i>Model Counting for Recursively-Defined Strings</i>. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer, 2017, pp. 399–418, doi:<a href=\"https://doi.org/10.1007/978-3-319-63390-9_21\">10.1007/978-3-319-63390-9_21</a>.","apa":"Trinh, M., Chu, D. H., &#38; Jaffar, J. (2017). Model counting for recursively-defined strings. In R. Majumdar &#38; V. Kunčak (Eds.) (Vol. 10427, pp. 399–418). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-63390-9_21\">https://doi.org/10.1007/978-3-319-63390-9_21</a>","chicago":"Trinh, Minh, Duc Hiep Chu, and Joxan Jaffar. “Model Counting for Recursively-Defined Strings.” edited by Rupak Majumdar and Viktor Kunčak, 10427:399–418. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63390-9_21\">https://doi.org/10.1007/978-3-319-63390-9_21</a>.","ista":"Trinh M, Chu DH, Jaffar J. 2017. Model counting for recursively-defined strings. CAV: Computer Aided Verification, LNCS, vol. 10427, 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:<a href=\"https://doi.org/10.1007/978-3-319-63390-9_21\">10.1007/978-3-319-63390-9_21</a>","short":"M. Trinh, D.H. Chu, J. Jaffar, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 399–418."},"editor":[{"first_name":"Rupak","full_name":"Majumdar, Rupak","last_name":"Majumdar"},{"last_name":"Kunčak","first_name":"Viktor","full_name":"Kunčak, Viktor"}],"abstract":[{"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.","lang":"eng"}],"status":"public","date_published":"2017-01-01T00:00:00Z","conference":{"start_date":"2017-07-24","name":"CAV: Computer Aided Verification","end_date":"2017-07-28","location":"Heidelberg, Germany"},"external_id":{"isi":["000431900900021"]},"oa_version":"None","author":[{"last_name":"Trinh","full_name":"Trinh, Minh","first_name":"Minh"},{"first_name":"Duc Hiep","full_name":"Chu, Duc Hiep","last_name":"Chu","id":"3598E630-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Jaffar","first_name":"Joxan","full_name":"Jaffar, Joxan"}],"publist_id":"6443","publisher":"Springer","doi":"10.1007/978-3-319-63390-9_21","type":"conference","language":[{"iso":"eng"}],"article_processing_charge":"No","scopus_import":"1","publication_identifier":{"issn":["03029743"]},"date_updated":"2023-09-22T09:58:02Z","project":[{"call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF"}],"page":"399 - 418","quality_controlled":"1","year":"2017","date_created":"2018-12-11T11:49:26Z","volume":10427,"isi":1},{"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. "}],"status":"public","article_number":"37","citation":{"ama":"Avni G, Guha S, Kupferman O. Timed network games with clocks. In: Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.37\">10.4230/LIPIcs.MFCS.2017.37</a>","short":"G. Avni, S. Guha, O. Kupferman, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ieee":"G. Avni, S. Guha, and O. Kupferman, “Timed network games with clocks,” presented at the MFCS: Mathematical Foundations of Computer Science (SG), Aalborg, Denmark, 2017, vol. 83.","mla":"Avni, Guy, et al. <i>Timed Network Games with Clocks</i>. Vol. 83, 37, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.37\">10.4230/LIPIcs.MFCS.2017.37</a>.","ista":"Avni G, Guha S, Kupferman O. 2017. Timed network games with clocks. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 83, 37.","apa":"Avni, G., Guha, S., &#38; Kupferman, O. (2017). Timed network games with clocks (Vol. 83). Presented at the MFCS: Mathematical Foundations of Computer Science (SG), Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.37\">https://doi.org/10.4230/LIPIcs.MFCS.2017.37</a>","chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “Timed Network Games with Clocks,” Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.37\">https://doi.org/10.4230/LIPIcs.MFCS.2017.37</a>."},"intvolume":"        83","has_accepted_license":"1","day":"01","publication_status":"published","oa":1,"related_material":{"record":[{"relation":"later_version","status":"public","id":"6005"}]},"title":"Timed network games with clocks","month":"06","_id":"963","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","pubrep_id":"829","alternative_title":["LIPIcs"],"department":[{"_id":"ToHe"}],"file":[{"relation":"main_file","checksum":"f55eaf7f3c36ea07801112acfedd17d5","file_size":369730,"creator":"system","file_name":"IST-2017-829-v1+1_mfcs-cr.pdf","content_type":"application/pdf","date_created":"2018-12-12T10:14:10Z","file_id":"5059","date_updated":"2020-07-14T12:48:18Z","access_level":"open_access"}],"volume":83,"project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"}],"date_updated":"2023-02-23T12:35:50Z","date_created":"2018-12-11T11:49:26Z","year":"2017","quality_controlled":"1","scopus_import":1,"publication_identifier":{"issn":["18688969"]},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"type":"conference","file_date_updated":"2020-07-14T12:48:18Z","language":[{"iso":"eng"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","doi":"10.4230/LIPIcs.MFCS.2017.37","author":[{"orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy","full_name":"Avni, Guy"},{"first_name":"Shibashis","full_name":"Guha, Shibashis","last_name":"Guha"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"ddc":["004"],"publist_id":"6438","date_published":"2017-06-01T00:00:00Z","conference":{"start_date":"2017-08-21","name":"MFCS: Mathematical Foundations of Computer Science (SG)","end_date":"2017-08-25","location":"Aalborg, Denmark"},"oa_version":"Published Version"},{"publication_identifier":{"issn":["03029743"]},"scopus_import":"1","article_processing_charge":"No","isi":1,"file":[{"file_name":"IST-2017-758-v1+1_tacas-cr.pdf","access_level":"open_access","date_updated":"2018-12-12T10:08:37Z","date_created":"2018-12-12T10:08:37Z","content_type":"application/pdf","file_id":"4698","relation":"main_file","creator":"system","file_size":321800}],"volume":10206,"date_created":"2018-12-11T11:50:14Z","year":"2017","quality_controlled":"1","page":"169 - 187","project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"date_updated":"2023-09-20T11:32:43Z","publist_id":"6246","author":[{"orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","first_name":"Guy","full_name":"Avni, Guy"},{"last_name":"Goel","full_name":"Goel, Shubham","first_name":"Shubham"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Rodríguez Navas","first_name":"Guillermo","full_name":"Rodríguez Navas, Guillermo"}],"ddc":["000"],"oa_version":"Submitted Version","external_id":{"isi":["000440733400010"]},"conference":{"start_date":"2017-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2017-04-29","location":"Uppsala, Sweden"},"date_published":"2017-03-31T00:00:00Z","language":[{"iso":"eng"}],"type":"conference","file_date_updated":"2018-12-12T10:08:37Z","doi":"10.1007/978-3-662-54580-5_10","publisher":"Springer","citation":{"short":"G. Avni, S. Goel, T.A. Henzinger, G. Rodríguez Navas, in:, Springer, 2017, pp. 169–187.","ama":"Avni G, Goel S, Henzinger TA, Rodríguez Navas G. Computing scores of forwarding schemes in switched networks with probabilistic faults. In: Vol 10206. Springer; 2017:169-187. doi:<a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">10.1007/978-3-662-54580-5_10</a>","apa":"Avni, G., Goel, S., Henzinger, T. A., &#38; Rodríguez Navas, G. (2017). Computing scores of forwarding schemes in switched networks with probabilistic faults (Vol. 10206, pp. 169–187). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">https://doi.org/10.1007/978-3-662-54580-5_10</a>","chicago":"Avni, Guy, Shubham Goel, Thomas A Henzinger, and Guillermo Rodríguez Navas. “Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults,” 10206:169–87. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">https://doi.org/10.1007/978-3-662-54580-5_10</a>.","ista":"Avni G, Goel S, Henzinger TA, Rodríguez Navas G. 2017. Computing scores of forwarding schemes in switched networks with probabilistic faults. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 10206, 169–187.","mla":"Avni, Guy, et al. <i>Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults</i>. Vol. 10206, Springer, 2017, pp. 169–87, doi:<a href=\"https://doi.org/10.1007/978-3-662-54580-5_10\">10.1007/978-3-662-54580-5_10</a>.","ieee":"G. Avni, S. Goel, T. A. Henzinger, and G. Rodríguez Navas, “Computing scores of forwarding schemes in switched networks with probabilistic faults,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Uppsala, Sweden, 2017, vol. 10206, pp. 169–187."},"intvolume":"     10206","day":"31","has_accepted_license":"1","status":"public","abstract":[{"text":"Time-triggered switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. Due to the criticality of the applications running over them, developers need to ensure that end-to-end communication is dependable and predictable. Traditional approaches assume static networks that are not flexible to changes caused by reconfigurations or, more importantly, faults, which are dealt with in the application using redundancy. We adopt the concept of handling faults in the switches from non-real-time networks while maintaining the required predictability. \r\n\r\nWe study a class of forwarding schemes that can handle various types of failures. We consider probabilistic failures. We study a class of forwarding schemes that can handle various types of failures. We consider probabilistic failures. For a given network with a forwarding scheme and a constant ℓ, we compute the {\\em score} of the scheme, namely the probability (induced by faults) that at least ℓ messages arrive on time. We reduce the scoring problem to a reachability problem on a Markov chain with a &quot;product-like&quot; structure. Its special structure allows us to reason about it symbolically, and reduce the scoring problem to #SAT. Our solution is generic and can be adapted to different networks and other contexts. Also, we show the computational complexity of the scoring problem is #P-complete, and we study methods to estimate the score. We evaluate the effectiveness of our techniques with an implementation. ","lang":"eng"}],"alternative_title":["LNCS"],"pubrep_id":"758","department":[{"_id":"ToHe"}],"publication_status":"published","oa":1,"title":"Computing scores of forwarding schemes in switched networks with probabilistic faults","month":"03","_id":"1116","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1"},{"doi":"10.15479/AT:ISTA:TH_730","publisher":"Institute of Science and Technology Austria","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:44:34Z","type":"dissertation","oa_version":"Published Version","date_published":"2017-01-02T00:00:00Z","publist_id":"6203","ddc":["004","005"],"author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","last_name":"Daca","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw"}],"page":"163","date_created":"2018-12-11T11:50:27Z","year":"2017","date_updated":"2023-09-07T11:58:34Z","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"file":[{"file_name":"IST-2017-730-v1+1_Statistical_and_Logical_Methods_for_Property_Checking.pdf","date_updated":"2020-07-14T12:44:34Z","access_level":"open_access","file_id":"4880","content_type":"application/pdf","date_created":"2018-12-12T10:11:26Z","checksum":"1406a681cb737508234fde34766be2c2","relation":"main_file","creator":"system","file_size":1028586}],"article_processing_charge":"No","publication_identifier":{"issn":["2663-337X"]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","month":"01","_id":"1155","title":"Statistical and logical methods for property checking","related_material":{"record":[{"id":"1093","status":"public","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","status":"public","id":"1230"},{"status":"public","relation":"part_of_dissertation","id":"1234"},{"relation":"part_of_dissertation","status":"public","id":"1391"},{"relation":"part_of_dissertation","status":"public","id":"1501"},{"id":"1502","relation":"part_of_dissertation","status":"public"},{"id":"2063","relation":"part_of_dissertation","status":"public"},{"id":"2167","relation":"part_of_dissertation","status":"public"}]},"oa":1,"publication_status":"published","acknowledgement":" First of all, I want to thank my advisor, prof. Thomas A. Henzinger, for his guidance during my PhD program. I am grateful for the freedom I was given to pursue my research interests, and his continuous support. Working with prof. Henzinger was a truly inspiring experience and taught me what it means to be a scientist. I want to express my gratitude to my collaborators: Nikola Beneš, Krishnendu Chatterjee, Martin Chmelík, Ashutosh Gupta, Willibald Krenn, Jan Kˇretínský, Dejan Nickovic, Andrey Kupriyanov, and Tatjana Petrov. I have learned a great deal from my collaborators, and without their help this thesis would not be possible. In addition, I want to thank the members of my thesis committee: Dirk Beyer, Dejan Nickovic, and Georg Weissenbacher for their advice and reviewing this dissertation. I would especially like to acknowledge the late Helmut Veith, who was a member of my committee. I will remember Helmut for his kindness, enthusiasm, and wit, as well as for being an inspiring scientist. Finally, I would like to thank my colleagues for making my stay at IST such a pleasant experience: Guy Avni, Sergiy Bogomolov, Ventsislav Chonev, Rasmus Ibsen-Jensen, Mirco Giacobbe, Bernhard Kragl, Hui Kong, Petr Novotný, Jan Otop, Andreas Pavlogiannis, Tantjana Petrov, Arjun Radhakrishna, Jakob Ruess, Thorsten Tarrach, as well as other members of groups Henzinger and Chatterjee. ","department":[{"_id":"ToHe"}],"alternative_title":["ISTA Thesis"],"pubrep_id":"730","degree_awarded":"PhD","ec_funded":1,"status":"public","abstract":[{"text":"This dissertation concerns the automatic verification of probabilistic systems and programs with arrays by statistical and logical methods. Although statistical and logical methods are different in nature, we show that they can be successfully combined for system analysis. In the first part of the dissertation we present a new statistical algorithm for the verification of probabilistic systems with respect to unbounded properties, including linear temporal logic. Our algorithm often performs faster than the previous approaches, and at the same time requires less information about the system. In addition, our method can be generalized to unbounded quantitative properties such as mean-payoff bounds. In the second part, we introduce two techniques for comparing probabilistic systems. Probabilistic systems are typically compared using the notion of equivalence, which requires the systems to have the equal probability of all behaviors. However, this notion is often too strict, since probabilities are typically only empirically estimated, and any imprecision may break the relation between processes. On the one hand, we propose to replace the Boolean notion of equivalence by a quantitative distance of similarity. For this purpose, we introduce a statistical framework for estimating distances between Markov chains based on their simulation runs, and we investigate which distances can be approximated in our framework. On the other hand, we propose to compare systems with respect to a new qualitative logic, which expresses that behaviors occur with probability one or a positive probability. This qualitative analysis is robust with respect to modeling errors and applicable to many domains. In the last part, we present a new quantifier-free logic for integer arrays, which allows us to express counting. Counting properties are prevalent in array-manipulating programs, however they cannot be expressed in the quantified fragments of the theory of arrays. We present a decision procedure for our logic, and provide several complexity results.","lang":"eng"}],"day":"02","has_accepted_license":"1","supervisor":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"citation":{"ama":"Daca P. Statistical and logical methods for property checking. 2017. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">10.15479/AT:ISTA:TH_730</a>","short":"P. Daca, Statistical and Logical Methods for Property Checking, Institute of Science and Technology Austria, 2017.","mla":"Daca, Przemyslaw. <i>Statistical and Logical Methods for Property Checking</i>. Institute of Science and Technology Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">10.15479/AT:ISTA:TH_730</a>.","ieee":"P. Daca, “Statistical and logical methods for property checking,” Institute of Science and Technology Austria, 2017.","chicago":"Daca, Przemyslaw. “Statistical and Logical Methods for Property Checking.” Institute of Science and Technology Austria, 2017. <a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">https://doi.org/10.15479/AT:ISTA:TH_730</a>.","apa":"Daca, P. (2017). <i>Statistical and logical methods for property checking</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:TH_730\">https://doi.org/10.15479/AT:ISTA:TH_730</a>","ista":"Daca P. 2017. Statistical and logical methods for property checking. Institute of Science and Technology Austria."}},{"department":[{"_id":"ToHe"}],"acknowledgement":"This research was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund1 (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and by the National Science Centre (NCN), Poland under grant 2014/15/D/ST6/04543.\r\nA Technical Report of this article is available via: https://repository.ist.ac.at/171/","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"1196","month":"02","title":"Model measuring for discrete and hybrid systems","publication_status":"published","day":"01","citation":{"short":"T.A. Henzinger, J. Otop, Nonlinear Analysis: Hybrid Systems 23 (2017) 166–190.","ama":"Henzinger TA, Otop J. Model measuring for discrete and hybrid systems. <i>Nonlinear Analysis: Hybrid Systems</i>. 2017;23:166-190. doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">10.1016/j.nahs.2016.09.001</a>","ista":"Henzinger TA, Otop J. 2017. Model measuring for discrete and hybrid systems. Nonlinear Analysis: Hybrid Systems. 23, 166–190.","chicago":"Henzinger, Thomas A, and Jan Otop. “Model Measuring for Discrete and Hybrid Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">https://doi.org/10.1016/j.nahs.2016.09.001</a>.","apa":"Henzinger, T. A., &#38; Otop, J. (2017). Model measuring for discrete and hybrid systems. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">https://doi.org/10.1016/j.nahs.2016.09.001</a>","mla":"Henzinger, Thomas A., and Jan Otop. “Model Measuring for Discrete and Hybrid Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, Elsevier, 2017, pp. 166–90, doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.09.001\">10.1016/j.nahs.2016.09.001</a>.","ieee":"T. A. Henzinger and J. Otop, “Model measuring for discrete and hybrid systems,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23. Elsevier, pp. 166–190, 2017."},"intvolume":"        23","ec_funded":1,"status":"public","abstract":[{"lang":"eng","text":"We define the . model-measuring problem: given a model . M and specification . ϕ, what is the maximal distance . ρ such that all models . M' within distance . ρ from . M satisfy (or violate) . ϕ. The model-measuring problem presupposes a distance function on models. We concentrate on . automatic distance functions, which are defined by weighted automata. The model-measuring problem subsumes several generalizations of the classical model-checking problem, in particular, quantitative model-checking problems that measure the degree of satisfaction of a specification; robustness problems that measure how much a model can be perturbed without violating the specification; and parameter synthesis for hybrid systems. We show that for automatic distance functions, and (a) . ω-regular linear-time, (b) . ω-regular branching-time, and (c) hybrid specifications, the model-measuring problem can be solved.We use automata-theoretic model-checking methods for model measuring, replacing the emptiness question for word, tree, and hybrid automata by the . optimal-value question for the weighted versions of these automata. For automata over words and trees, we consider weighted automata that accumulate weights by maximizing, summing, discounting, and limit averaging. For hybrid automata, we consider monotonic (parametric) hybrid automata, a hybrid counterpart of (discrete) weighted automata.We give several examples of using the model-measuring problem to compute various notions of robustness and quantitative satisfaction for temporal specifications. Further, we propose the modeling framework for model measuring to ease the specification and reduce the likelihood of errors in modeling.Finally, we present a variant of the model-measuring problem, called the . model-repair problem. The model-repair problem applies to models that do not satisfy the specification; it can be used to derive restrictions, under which the model satisfies the specification, i.e., to repair the model."}],"external_id":{"isi":["000390637000011"]},"oa_version":"None","date_published":"2017-02-01T00:00:00Z","publication":"Nonlinear Analysis: Hybrid Systems","publist_id":"6154","author":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop"}],"doi":"10.1016/j.nahs.2016.09.001","publisher":"Elsevier","language":[{"iso":"eng"}],"type":"journal_article","article_processing_charge":"No","scopus_import":"1","quality_controlled":"1","page":"166 - 190","date_created":"2018-12-11T11:50:39Z","year":"2017","date_updated":"2023-09-20T11:18:50Z","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"volume":23,"isi":1},{"oa":1,"related_material":{"record":[{"id":"1610","relation":"earlier_version","status":"public"},{"id":"5438","relation":"earlier_version","status":"public"}]},"title":"Edit distance for pushdown automata","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"09","_id":"465","pubrep_id":"955","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"status":"public","abstract":[{"text":"The edit distance between two words w 1 , w 2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the edit distance from L 1 to L 2 is the minimal number k such that for every word from L 1 there exists a word in L 2 with edit distance at most k . We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for the following problems: (1) deciding whether, for a given threshold k , the edit distance from a pushdown automaton to a finite automaton is at most k , and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite. ","lang":"eng"}],"ec_funded":1,"intvolume":"        13","citation":{"apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2017). Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2017. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>.","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for pushdown automata. Logical Methods in Computer Science. 13(3).","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3. International Federation of Computational Logic, 2017.","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3, International Federation of Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017).","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. 2017;13(3). doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>"},"day":"13","has_accepted_license":"1","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:46:33Z","type":"journal_article","doi":"10.23638/LMCS-13(3:23)2017","publisher":"International Federation of Computational Logic","issue":"3","publist_id":"7356","publication":"Logical Methods in Computer Science","ddc":["004"],"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop"}],"license":"https://creativecommons.org/licenses/by-nd/4.0/","oa_version":"Published Version","date_published":"2017-09-13T00:00:00Z","volume":13,"file":[{"file_name":"IST-2015-321-v1+1_main.pdf","date_created":"2018-12-12T10:14:37Z","content_type":"application/pdf","file_id":"5090","date_updated":"2020-07-14T12:46:33Z","access_level":"open_access","relation":"main_file","checksum":"08041379ba408d40664f449eb5907a8f","file_size":279071,"creator":"system"},{"file_name":"IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf","date_updated":"2020-07-14T12:46:33Z","access_level":"open_access","file_id":"5091","content_type":"application/pdf","date_created":"2018-12-12T10:14:38Z","checksum":"08041379ba408d40664f449eb5907a8f","relation":"main_file","creator":"system","file_size":279071}],"quality_controlled":"1","year":"2017","date_created":"2018-12-11T11:46:37Z","date_updated":"2023-02-23T12:26:25Z","project":[{"call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-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","grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"}],"publication_identifier":{"issn":["18605974"]},"scopus_import":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)"}},{"volume":18,"project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"date_updated":"2023-02-23T12:26:19Z","year":"2017","date_created":"2018-12-11T11:46:38Z","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1606.03598"}],"scopus_import":1,"publication_identifier":{"issn":["15293785"]},"type":"journal_article","arxiv":1,"language":[{"iso":"eng"}],"publisher":"ACM","doi":"10.1145/3152769","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"issue":"4","publication":"ACM Transactions on Computational Logic (TOCL)","publist_id":"7354","date_published":"2017-12-01T00:00:00Z","oa_version":"Preprint","external_id":{"arxiv":["1606.03598"]},"abstract":[{"lang":"eng","text":"Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata or in any other known decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata, which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in runtime verification. We establish an almost-complete decidability picture for the basic decision problems about nested weighted automata and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties."}],"status":"public","article_number":"31","ec_funded":1,"intvolume":"        18","citation":{"ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2017;18(4). doi:<a href=\"https://doi.org/10.1145/3152769\">10.1145/3152769</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational Logic (TOCL) 18 (2017).","mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 4, 31, ACM, 2017, doi:<a href=\"https://doi.org/10.1145/3152769\">10.1145/3152769</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 4. ACM, 2017.","ista":"Chatterjee K, Henzinger TA, Otop J. 2017. Nested weighted automata. ACM Transactions on Computational Logic (TOCL). 18(4), 31.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2017). Nested weighted automata. <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>"},"day":"01","publication_status":"published","related_material":{"record":[{"id":"1656","status":"public","relation":"earlier_version"},{"id":"5415","status":"public","relation":"earlier_version"},{"status":"public","relation":"earlier_version","id":"5436"}]},"oa":1,"title":"Nested weighted automata","month":"12","_id":"467","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"},{"_id":"ToHe"}]},{"quality_controlled":"1","year":"2017","date_created":"2018-12-11T11:46:39Z","date_updated":"2023-02-21T16:48:11Z","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"}],"volume":18,"publication_identifier":{"issn":["15293785"]},"scopus_import":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.05739"}],"doi":"10.1145/3060139","publisher":"ACM","language":[{"iso":"eng"}],"type":"journal_article","oa_version":"Submitted Version","date_published":"2017-05-01T00:00:00Z","publist_id":"7349","publication":"ACM Transactions on Computational Logic (TOCL)","issue":"2","author":[{"full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","full_name":"Petrov, Tatjana","first_name":"Tatjana","last_name":"Petrov"}],"ec_funded":1,"article_number":"12","status":"public","abstract":[{"lang":"eng","text":"We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds. "}],"day":"01","intvolume":"        18","citation":{"ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical model checking for unbounded temporal properties,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 2. ACM, 2017.","mla":"Daca, Przemyslaw, et al. “Faster Statistical Model Checking for Unbounded Temporal Properties.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 2, 12, ACM, 2017, doi:<a href=\"https://doi.org/10.1145/3060139\">10.1145/3060139</a>.","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2017. Faster statistical model checking for unbounded temporal properties. ACM Transactions on Computational Logic (TOCL). 18(2), 12.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Faster Statistical Model Checking for Unbounded Temporal Properties.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3060139\">https://doi.org/10.1145/3060139</a>.","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2017). Faster statistical model checking for unbounded temporal properties. <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href=\"https://doi.org/10.1145/3060139\">https://doi.org/10.1145/3060139</a>","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking for unbounded temporal properties. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2017;18(2). doi:<a href=\"https://doi.org/10.1145/3060139\">10.1145/3060139</a>","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational Logic (TOCL) 18 (2017)."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"05","_id":"471","title":"Faster statistical model checking for unbounded temporal properties","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1234"}]},"oa":1,"publication_status":"published","department":[{"_id":"ToHe"}]},{"status":"public","abstract":[{"lang":"eng","text":"Many biological systems can be modeled as multiaffine hybrid systems. Due to the nonlinearity of multiaffine systems, it is difficult to verify their properties of interest directly. A common strategy to tackle this problem is to construct and analyze a discrete overapproximation of the original system. However, the conservativeness of a discrete abstraction significantly determines the level of confidence we can have in the properties of the original system. In this paper, in order to reduce the conservativeness of a discrete abstraction, we propose a new method based on a sufficient and necessary decision condition for computing discrete transitions between states in the abstract system. We assume the state space partition of a multiaffine system to be based on a set of multivariate polynomials. Hence, a rectangular partition defined in terms of polynomials of the form (xi − c) is just a simple case of multivariate polynomial partition, and the new decision condition applies naturally. We analyze and demonstrate the improvement of our method over the existing methods using some examples."}],"intvolume":"      9957","citation":{"ama":"Kong H, Bartocci E, Bogomolov S, et al. Discrete abstraction of multiaffine systems. In: Vol 9957. Springer; 2016:128-144. doi:<a href=\"https://doi.org/10.1007/978-3-319-47151-8_9\">10.1007/978-3-319-47151-8_9</a>","short":"H. Kong, E. Bartocci, S. Bogomolov, R. Grosu, T.A. Henzinger, Y. Jiang, C. Schilling, in:, Springer, 2016, pp. 128–144.","mla":"Kong, Hui, et al. <i>Discrete Abstraction of Multiaffine Systems</i>. Vol. 9957, Springer, 2016, pp. 128–44, doi:<a href=\"https://doi.org/10.1007/978-3-319-47151-8_9\">10.1007/978-3-319-47151-8_9</a>.","ieee":"H. Kong <i>et al.</i>, “Discrete abstraction of multiaffine systems,” presented at the HSB: Hybrid Systems Biology, Grenoble, France, 2016, vol. 9957, pp. 128–144.","apa":"Kong, H., Bartocci, E., Bogomolov, S., Grosu, R., Henzinger, T. A., Jiang, Y., &#38; Schilling, C. (2016). Discrete abstraction of multiaffine systems (Vol. 9957, pp. 128–144). Presented at the HSB: Hybrid Systems Biology, Grenoble, France: Springer. <a href=\"https://doi.org/10.1007/978-3-319-47151-8_9\">https://doi.org/10.1007/978-3-319-47151-8_9</a>","ista":"Kong H, Bartocci E, Bogomolov S, Grosu R, Henzinger TA, Jiang Y, Schilling C. 2016. Discrete abstraction of multiaffine systems. HSB: Hybrid Systems Biology, LNCS, vol. 9957, 128–144.","chicago":"Kong, Hui, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, Thomas A Henzinger, Yu Jiang, and Christian Schilling. “Discrete Abstraction of Multiaffine Systems,” 9957:128–44. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-47151-8_9\">https://doi.org/10.1007/978-3-319-47151-8_9</a>."},"day":"25","has_accepted_license":"1","publication_status":"published","title":"Discrete abstraction of multiaffine systems","oa":1,"_id":"1227","month":"09","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","pubrep_id":"781","alternative_title":["LNCS"],"department":[{"_id":"ToHe"}],"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).","file":[{"content_type":"application/pdf","file_id":"4840","date_created":"2018-12-12T10:10:49Z","date_updated":"2020-07-14T12:44:39Z","access_level":"open_access","file_name":"IST-2017-781-v1+1_main.pdf","file_size":683955,"creator":"system","relation":"main_file","checksum":"994e164b558c47bacf8dc066dd27c8fc"}],"volume":9957,"year":"2016","date_created":"2018-12-11T11:50:49Z","quality_controlled":"1","page":"128 - 144","project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"date_updated":"2021-01-12T06:49:13Z","scopus_import":1,"language":[{"iso":"eng"}],"type":"conference","file_date_updated":"2020-07-14T12:44:39Z","doi":"10.1007/978-3-319-47151-8_9","publisher":"Springer","publist_id":"6107","author":[{"orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","last_name":"Kong","first_name":"Hui","full_name":"Kong, Hui"},{"full_name":"Bartocci, Ezio","first_name":"Ezio","last_name":"Bartocci"},{"first_name":"Sergiy","full_name":"Bogomolov, Sergiy","last_name":"Bogomolov","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365"},{"full_name":"Grosu, Radu","first_name":"Radu","last_name":"Grosu"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Jiang","first_name":"Yu","full_name":"Jiang, Yu"},{"orcid":"0000-0003-3658-1065","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","last_name":"Schilling","full_name":"Schilling, Christian","first_name":"Christian"}],"ddc":["005"],"oa_version":"Submitted Version","conference":{"end_date":"2016-10-21","location":"Grenoble, France","start_date":"2016-10-20","name":"HSB: Hybrid Systems Biology"},"date_published":"2016-09-25T00:00:00Z"},{"scopus_import":1,"main_file_link":[{"url":"https://arxiv.org/abs/1511.02615","open_access":"1"}],"volume":9583,"date_updated":"2023-09-07T11:58:33Z","project":[{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"quality_controlled":"1","page":"328 - 347","year":"2016","date_created":"2018-12-11T11:50:50Z","author":[{"full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","last_name":"Daca","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh","first_name":"Ashutosh","last_name":"Gupta"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"}],"publist_id":"6104","date_published":"2016-01-01T00:00:00Z","conference":{"end_date":"2016-01-19","location":"St. Petersburg, FL, USA","start_date":"2016-01-17","name":"VMCAI: Verification, Model Checking and Abstract Interpretation"},"oa_version":"Preprint","type":"conference","language":[{"iso":"eng"}],"publisher":"Springer","doi":"10.1007/978-3-662-49122-5_16","intvolume":"      9583","citation":{"mla":"Daca, Przemyslaw, et al. <i>Abstraction-Driven Concolic Testing</i>. Vol. 9583, Springer, 2016, pp. 328–47, doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">10.1007/978-3-662-49122-5_16</a>.","ieee":"P. Daca, A. Gupta, and T. A. Henzinger, “Abstraction-driven concolic testing,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA, 2016, vol. 9583, pp. 328–347.","ista":"Daca P, Gupta A, Henzinger TA. 2016. Abstraction-driven concolic testing. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 9583, 328–347.","apa":"Daca, P., Gupta, A., &#38; Henzinger, T. A. (2016). Abstraction-driven concolic testing (Vol. 9583, pp. 328–347). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">https://doi.org/10.1007/978-3-662-49122-5_16</a>","chicago":"Daca, Przemyslaw, Ashutosh Gupta, and Thomas A Henzinger. “Abstraction-Driven Concolic Testing,” 9583:328–47. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">https://doi.org/10.1007/978-3-662-49122-5_16</a>.","ama":"Daca P, Gupta A, Henzinger TA. Abstraction-driven concolic testing. In: Vol 9583. Springer; 2016:328-347. doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_16\">10.1007/978-3-662-49122-5_16</a>","short":"P. Daca, A. Gupta, T.A. Henzinger, in:, Springer, 2016, pp. 328–347."},"day":"01","abstract":[{"lang":"eng","text":"Concolic testing is a promising method for generating test suites for large programs. However, it suffers from the path-explosion problem and often fails to find tests that cover difficult-to-reach parts of programs. In contrast, model checkers based on counterexample-guided abstraction refinement explore programs exhaustively, while failing to scale on large programs with precision. In this paper, we present a novel method that iteratively combines concolic testing and model checking to find a test suite for a given coverage criterion. If concolic testing fails to cover some test goals, then the model checker refines its program abstraction to prove more paths infeasible, which reduces the search space for concolic testing. We have implemented our method on top of the concolictesting tool Crest and the model checker CpaChecker. We evaluated our tool on a collection of programs and a category of SvComp benchmarks. In our experiments, we observed an improvement in branch coverage compared to Crest from 48% to 63% in the best case, and from 66% to 71% on average."}],"status":"public","ec_funded":1,"alternative_title":["LNCS"],"acknowledgement":"We thank Andrey Kupriyanov for feedback on the manuscript,\r\nand Michael Tautschnig for help with preparing the experiments. This research was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award).","department":[{"_id":"ToHe"}],"related_material":{"record":[{"id":"1155","relation":"dissertation_contains","status":"public"}]},"oa":1,"title":"Abstraction-driven concolic testing","publication_status":"published","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"01","_id":"1230"},{"date_updated":"2023-09-07T11:58:33Z","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"page":"112 - 129","quality_controlled":"1","date_created":"2018-12-11T11:50:51Z","year":"2016","volume":9636,"scopus_import":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1504.05739"}],"publisher":"Springer","doi":"10.1007/978-3-662-49674-9_7","type":"conference","language":[{"iso":"eng"}],"date_published":"2016-01-01T00:00:00Z","oa_version":"Preprint","conference":{"location":"Eindhoven, The Netherlands","end_date":"2016-04-08","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2016-04-02"},"author":[{"id":"49351290-F248-11E8-B48F-1D18A9856A87","last_name":"Daca","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Kretinsky, Jan","last_name":"Kretinsky"},{"id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9041-0905","last_name":"Petrov","full_name":"Petrov, Tatjana","first_name":"Tatjana"}],"publist_id":"6099","ec_funded":1,"abstract":[{"text":"We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds.","lang":"eng"}],"status":"public","day":"01","intvolume":"      9636","citation":{"ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical model checking for unbounded temporal properties,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands, 2016, vol. 9636, pp. 112–129.","mla":"Daca, Przemyslaw, et al. <i>Faster Statistical Model Checking for Unbounded Temporal Properties</i>. Vol. 9636, Springer, 2016, pp. 112–29, doi:<a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">10.1007/978-3-662-49674-9_7</a>.","ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Faster statistical model checking for unbounded temporal properties. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 9636, 112–129.","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2016). Faster statistical model checking for unbounded temporal properties (Vol. 9636, pp. 112–129). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, The Netherlands: Springer. <a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">https://doi.org/10.1007/978-3-662-49674-9_7</a>","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Faster Statistical Model Checking for Unbounded Temporal Properties,” 9636:112–29. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">https://doi.org/10.1007/978-3-662-49674-9_7</a>.","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking for unbounded temporal properties. In: Vol 9636. Springer; 2016:112-129. doi:<a href=\"https://doi.org/10.1007/978-3-662-49674-9_7\">10.1007/978-3-662-49674-9_7</a>","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Springer, 2016, pp. 112–129."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1234","month":"01","oa":1,"title":"Faster statistical model checking for unbounded temporal properties","related_material":{"record":[{"id":"471","relation":"later_version","status":"public"},{"status":"public","relation":"dissertation_contains","id":"1155"}]},"publication_status":"published","acknowledgement":"This research was funded in part by the European Research Council (ERC) under\r\ngrant  agreement  267989  (QUAREM),  the  Austrian  Science  Fund  (FWF)  under\r\ngrants project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), the Peo-\r\nple Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734, the SNSF Advanced Postdoc.\r\nMobility Fellowship – grant number P300P2\r\n161067, and the Czech Science Foun-\r\ndation under grant agreement P202/12/G061.","department":[{"_id":"ToHe"},{"_id":"CaGu"}],"alternative_title":["LNCS"]},{"citation":{"chicago":"Jiang, Yu, Yixiao Yang, Han Liu, Hui Kong, Ming Gu, Jiaguang Sun, and Lui Sha. “From Stateflow Simulation to Verified Implementation: A Verification Approach and a Real-Time Train Controller Design.” IEEE, 2016. <a href=\"https://doi.org/10.1109/RTAS.2016.7461337\">https://doi.org/10.1109/RTAS.2016.7461337</a>.","ista":"Jiang Y, Yang Y, Liu H, Kong H, Gu M, Sun J, Sha L. 2016. From stateflow simulation to verified implementation: A verification approach and a real-time train controller design. RTAS: Real-time and Embedded Technology and Applications Symposium, 7461337.","apa":"Jiang, Y., Yang, Y., Liu, H., Kong, H., Gu, M., Sun, J., &#38; Sha, L. (2016). From stateflow simulation to verified implementation: A verification approach and a real-time train controller design. Presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, Vienna, Austria: IEEE. <a href=\"https://doi.org/10.1109/RTAS.2016.7461337\">https://doi.org/10.1109/RTAS.2016.7461337</a>","mla":"Jiang, Yu, et al. <i>From Stateflow Simulation to Verified Implementation: A Verification Approach and a Real-Time Train Controller Design</i>. 7461337, IEEE, 2016, doi:<a href=\"https://doi.org/10.1109/RTAS.2016.7461337\">10.1109/RTAS.2016.7461337</a>.","ieee":"Y. Jiang <i>et al.</i>, “From stateflow simulation to verified implementation: A verification approach and a real-time train controller design,” presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, Vienna, Austria, 2016.","short":"Y. Jiang, Y. Yang, H. Liu, H. Kong, M. Gu, J. Sun, L. Sha, in:, IEEE, 2016.","ama":"Jiang Y, Yang Y, Liu H, et al. From stateflow simulation to verified implementation: A verification approach and a real-time train controller design. In: IEEE; 2016. doi:<a href=\"https://doi.org/10.1109/RTAS.2016.7461337\">10.1109/RTAS.2016.7461337</a>"},"day":"27","has_accepted_license":"1","status":"public","article_number":"7461337","abstract":[{"lang":"eng","text":"Simulink is widely used for model driven development (MDD) of industrial software systems. Typically, the Simulink based development is initiated from Stateflow modeling, followed by simulation, validation and code generation mapped to physical execution platforms. However, recent industrial trends have raised the demands of rigorous verification on safety-critical applications, which is unfortunately challenging for Simulink. In this paper, we present an approach to bridge the Stateflow based model driven development and a well- defined rigorous verification. First, we develop a self- contained toolkit to translate Stateflow model into timed automata, where major advanced modeling features in Stateflow are supported. Taking advantage of the strong verification capability of Uppaal, we can not only find bugs in Stateflow models which are missed by Simulink Design Verifier, but also check more important temporal properties. Next, we customize a runtime verifier for the generated nonintrusive VHDL and C code of Stateflow model for monitoring. The major strength of the customization is the flexibility to collect and analyze runtime properties with a pure software monitor, which opens more opportunities for engineers to achieve high reliability of the target system compared with the traditional act that only relies on Simulink Polyspace. We incorporate these two parts into original Stateflow based MDD seamlessly. In this way, safety-critical properties are both verified at the model level, and at the consistent system implementation level with physical execution environment in consideration. We apply our approach on a train controller design, and the verified implementation is tested and deployed on a real hardware platform."}],"pubrep_id":"780","department":[{"_id":"ToHe"}],"acknowledgement":"This work is supported in part by NSF CNS 13-30077, NSF CNS 13-29886, NSF CNS 15-45002, NSFC 61303014, NSFC 61202010, and NSFC 91218302.","publication_status":"published","oa":1,"title":"From stateflow simulation to verified implementation: A verification approach and a real-time train controller design","month":"04","_id":"1256","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"file":[{"relation":"main_file","checksum":"42f0462911cc9957f2356b12fb33b4b6","file_size":1293599,"creator":"system","file_name":"IST-2017-780-v1+1_RTAS-42-Camera-Ready.pdf","file_id":"4949","content_type":"application/pdf","date_created":"2018-12-12T10:12:31Z","date_updated":"2020-07-14T12:44:41Z","access_level":"open_access"}],"date_created":"2018-12-11T11:50:58Z","year":"2016","quality_controlled":"1","date_updated":"2021-01-12T06:49:26Z","publist_id":"6069","author":[{"last_name":"Jiang","first_name":"Yu","full_name":"Jiang, Yu"},{"last_name":"Yang","full_name":"Yang, Yixiao","first_name":"Yixiao"},{"first_name":"Han","full_name":"Liu, Han","last_name":"Liu"},{"id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941","full_name":"Kong, Hui","first_name":"Hui","last_name":"Kong"},{"full_name":"Gu, Ming","first_name":"Ming","last_name":"Gu"},{"full_name":"Sun, Jiaguang","first_name":"Jiaguang","last_name":"Sun"},{"first_name":"Lui","full_name":"Sha, Lui","last_name":"Sha"}],"ddc":["005"],"conference":{"start_date":"2016-04-11","name":"RTAS: Real-time and Embedded Technology and Applications Symposium","end_date":"2016-04-14","location":"Vienna, Austria"},"oa_version":"Submitted Version","date_published":"2016-04-27T00:00:00Z","language":[{"iso":"eng"}],"type":"conference","file_date_updated":"2020-07-14T12:44:41Z","doi":"10.1109/RTAS.2016.7461337","publisher":"IEEE"},{"publisher":"Springer","doi":"10.1007/978-3-662-53413-7_2","type":"conference","language":[{"iso":"eng"}],"date_published":"2016-08-31T00:00:00Z","oa_version":"Preprint","conference":{"start_date":"2016-09-08","name":"SAS: Static Analysis Symposium","end_date":"2016-09-10","location":"Edinburgh, United Kingdom"},"author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"}],"publist_id":"5932","date_updated":"2021-01-12T06:49:58Z","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","page":"23 - 38","date_created":"2018-12-11T11:51:26Z","year":"2016","volume":9837,"scopus_import":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.06764"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","month":"08","_id":"1335","title":"Quantitative monitor automata","oa":1,"publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"alternative_title":["LNCS"],"ec_funded":1,"abstract":[{"text":"In this paper we review various automata-theoretic formalisms for expressing quantitative properties. We start with finite-state Boolean automata that express the traditional regular properties. We then consider weighted ω-automata that can measure the average density of events, which finite-state Boolean automata cannot. However, even weighted ω-automata cannot express basic performance properties like average response time. We finally consider two formalisms of weighted ω-automata with monitors, where the monitors are either (a) counters or (b) weighted automata themselves. We present a translation result to establish that these two formalisms are equivalent. Weighted ω-automata with monitors generalize weighted ω-automata, and can express average response time property. They present a natural, robust, and expressive framework for quantitative specifications, with important decidable properties.","lang":"eng"}],"status":"public","day":"31","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Quantitative Monitor Automata</i>. Vol. 9837, Springer, 2016, pp. 23–38, doi:<a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">10.1007/978-3-662-53413-7_2</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative monitor automata,” presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom, 2016, vol. 9837, pp. 23–38.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2016). Quantitative monitor automata (Vol. 9837, pp. 23–38). Presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">https://doi.org/10.1007/978-3-662-53413-7_2</a>","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative monitor automata. SAS: Static Analysis Symposium, LNCS, vol. 9837, 23–38.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative Monitor Automata,” 9837:23–38. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">https://doi.org/10.1007/978-3-662-53413-7_2</a>.","ama":"Chatterjee K, Henzinger TA, Otop J. Quantitative monitor automata. In: Vol 9837. Springer; 2016:23-38. doi:<a href=\"https://doi.org/10.1007/978-3-662-53413-7_2\">10.1007/978-3-662-53413-7_2</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Springer, 2016, pp. 23–38."},"intvolume":"      9837"},{"scopus_import":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1501.00440"}],"quality_controlled":"1","page":"173 - 191","date_created":"2018-12-11T11:52:31Z","year":"2016","date_updated":"2021-01-12T06:51:22Z","project":[{"call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"volume":9271,"conference":{"start_date":"2015-09-04","name":"HSB: Hybrid Systems Biology","end_date":"2015-09-05","location":"Madrid, Spain"},"oa_version":"Preprint","date_published":"2016-01-10T00:00:00Z","publist_id":"5649","author":[{"full_name":"Beica, Andreea","first_name":"Andreea","last_name":"Beica"},{"id":"47F8433E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-6220-2052","first_name":"Calin C","full_name":"Guet, Calin C","last_name":"Guet"},{"orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","last_name":"Petrov","first_name":"Tatjana","full_name":"Petrov, Tatjana"}],"doi":"10.1007/978-3-319-26916-0_10","publisher":"Springer","language":[{"iso":"eng"}],"type":"conference","day":"10","intvolume":"      9271","citation":{"ieee":"A. Beica, C. C. Guet, and T. Petrov, “Efficient reduction of kappa models by static inspection of the rule-set,” presented at the HSB: Hybrid Systems Biology, Madrid, Spain, 2016, vol. 9271, pp. 173–191.","mla":"Beica, Andreea, et al. <i>Efficient Reduction of Kappa Models by Static Inspection of the Rule-Set</i>. Vol. 9271, Springer, 2016, pp. 173–91, doi:<a href=\"https://doi.org/10.1007/978-3-319-26916-0_10\">10.1007/978-3-319-26916-0_10</a>.","apa":"Beica, A., Guet, C. C., &#38; Petrov, T. (2016). Efficient reduction of kappa models by static inspection of the rule-set (Vol. 9271, pp. 173–191). Presented at the HSB: Hybrid Systems Biology, Madrid, Spain: Springer. <a href=\"https://doi.org/10.1007/978-3-319-26916-0_10\">https://doi.org/10.1007/978-3-319-26916-0_10</a>","chicago":"Beica, Andreea, Calin C Guet, and Tatjana Petrov. “Efficient Reduction of Kappa Models by Static Inspection of the Rule-Set,” 9271:173–91. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-26916-0_10\">https://doi.org/10.1007/978-3-319-26916-0_10</a>.","ista":"Beica A, Guet CC, Petrov T. 2016. Efficient reduction of kappa models by static inspection of the rule-set. HSB: Hybrid Systems Biology, LNCS, vol. 9271, 173–191.","ama":"Beica A, Guet CC, Petrov T. Efficient reduction of kappa models by static inspection of the rule-set. In: Vol 9271. Springer; 2016:173-191. doi:<a href=\"https://doi.org/10.1007/978-3-319-26916-0_10\">10.1007/978-3-319-26916-0_10</a>","short":"A. Beica, C.C. Guet, T. Petrov, in:, Springer, 2016, pp. 173–191."},"ec_funded":1,"status":"public","abstract":[{"lang":"eng","text":"When designing genetic circuits, the typical primitives used in major existing modelling formalisms are gene interaction graphs, where edges between genes denote either an activation or inhibition relation. However, when designing experiments, it is important to be precise about the low-level mechanistic details as to how each such relation is implemented. The rule-based modelling language Kappa allows to unambiguously specify mechanistic details such as DNA binding sites, dimerisation of transcription factors, or co-operative interactions. Such a detailed description comes with complexity and computationally costly executions. We propose a general method for automatically transforming a rule-based program, by eliminating intermediate species and adjusting the rate constants accordingly. To the best of our knowledge, we show the first automated reduction of rule-based models based on equilibrium approximations.\r\nOur algorithm is an adaptation of an existing algorithm, which was designed for reducing reaction-based programs; our version of the algorithm scans the rule-based Kappa model in search for those interaction patterns known to be amenable to equilibrium approximations (e.g. Michaelis-Menten scheme). Additional checks are then performed in order to verify if the reduction is meaningful in the context of the full model. The reduced model is efficiently obtained by static inspection over the rule-set. The tool is tested on a detailed rule-based model of a λ-phage switch, which lists 92 rules and 13 agents. The reduced model has 11 rules and 5 agents, and provides a dramatic reduction in simulation time of several orders of magnitude."}],"acknowledgement":"This research was supported by the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no. 291734, and the SNSF Early Postdoc.Mobility Fellowship, the grant number P2EZP2_148797.","department":[{"_id":"CaGu"},{"_id":"ToHe"}],"alternative_title":["LNCS"],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","month":"01","_id":"1524","title":"Efficient reduction of kappa models by static inspection of the rule-set","oa":1,"publication_status":"published"},{"ec_funded":1,"abstract":[{"text":"We present the first study of robustness of systems that are both timed as well as reactive (I/O). We study the behavior of such timed I/O systems in the presence of uncertain inputs and formalize their robustness using the analytic notion of Lipschitz continuity: a timed I/O system is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using similarity functions over timed words such as the timed version of the Manhattan distance and the Skorokhod distance. We consider two models of timed I/O systems — timed transducers and asynchronous sequential circuits. We show that K-robustness of timed transducers can be decided in polynomial space under certain conditions. For asynchronous sequential circuits, we reduce K-robustness w.r.t. timed Manhattan distances to K-robustness of discrete letter-to-letter transducers and show PSpace-completeness of the problem.","lang":"eng"}],"status":"public","day":"01","citation":{"short":"T.A. Henzinger, J. Otop, R. Samanta, in:, Springer, 2016, pp. 250–267.","ama":"Henzinger TA, Otop J, Samanta R. Lipschitz robustness of timed I/O systems. In: Vol 9583. Springer; 2016:250-267. doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">10.1007/978-3-662-49122-5_12</a>","apa":"Henzinger, T. A., Otop, J., &#38; Samanta, R. (2016). Lipschitz robustness of timed I/O systems (Vol. 9583, pp. 250–267). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">https://doi.org/10.1007/978-3-662-49122-5_12</a>","ista":"Henzinger TA, Otop J, Samanta R. 2016. Lipschitz robustness of timed I/O systems. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 9583, 250–267.","chicago":"Henzinger, Thomas A, Jan Otop, and Roopsha Samanta. “Lipschitz Robustness of Timed I/O Systems,” 9583:250–67. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">https://doi.org/10.1007/978-3-662-49122-5_12</a>.","mla":"Henzinger, Thomas A., et al. <i>Lipschitz Robustness of Timed I/O Systems</i>. Vol. 9583, Springer, 2016, pp. 250–67, doi:<a href=\"https://doi.org/10.1007/978-3-662-49122-5_12\">10.1007/978-3-662-49122-5_12</a>.","ieee":"T. A. Henzinger, J. Otop, and R. Samanta, “Lipschitz robustness of timed I/O systems,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, St. Petersburg, FL, USA, 2016, vol. 9583, pp. 250–267."},"intvolume":"      9583","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","month":"01","_id":"1526","title":"Lipschitz robustness of timed I/O systems","oa":1,"publication_status":"published","acknowledgement":"This research was supported in part by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and by the National Science Centre (NCN), Poland under grant 2014/15/D/ST6/04543.","department":[{"_id":"ToHe"}],"alternative_title":["LNCS"],"date_updated":"2021-01-12T06:51:23Z","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"quality_controlled":"1","page":"250 - 267","date_created":"2018-12-11T11:52:32Z","year":"2016","volume":9583,"scopus_import":1,"main_file_link":[{"url":"http://arxiv.org/abs/1506.01233","open_access":"1"}],"publisher":"Springer","doi":"10.1007/978-3-662-49122-5_12","type":"conference","language":[{"iso":"eng"}],"date_published":"2016-01-01T00:00:00Z","oa_version":"Preprint","conference":{"start_date":"2016-01-17","name":"VMCAI: Verification, Model Checking and Abstract Interpretation","end_date":"2016-01-19","location":"St. Petersburg, FL, USA"},"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"},{"id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","full_name":"Samanta, Roopsha","first_name":"Roopsha","last_name":"Samanta"}],"publist_id":"5647"},{"scopus_import":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"article_processing_charge":"Yes (via OA deal)","volume":18,"file":[{"content_type":"application/pdf","file_id":"5146","date_created":"2018-12-12T10:15:26Z","date_updated":"2020-07-14T12:45:13Z","access_level":"open_access","file_name":"IST-2016-457-v1+1_s10009-015-0393-y.pdf","file_size":2296522,"creator":"system","relation":"main_file","checksum":"31561d7705599a9bd4ea816accc0752e"}],"page":"449 - 467","quality_controlled":"1","year":"2016","date_created":"2018-12-11T11:53:34Z","date_updated":"2021-01-12T06:52:38Z","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"publist_id":"5431","publication":"International Journal on Software Tools for Technology Transfer","issue":"4","ddc":["000"],"author":[{"last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","first_name":"Sergiy","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Donzé","first_name":"Alexandre","full_name":"Donzé, Alexandre"},{"first_name":"Goran","full_name":"Frehse, Goran","last_name":"Frehse"},{"last_name":"Grosu","full_name":"Grosu, Radu","first_name":"Radu"},{"last_name":"Johnson","full_name":"Johnson, Taylor","first_name":"Taylor"},{"first_name":"Hamed","full_name":"Ladan, Hamed","last_name":"Ladan"},{"last_name":"Podelski","first_name":"Andreas","full_name":"Podelski, Andreas"},{"first_name":"Martin","full_name":"Wehrle, Martin","last_name":"Wehrle"}],"oa_version":"Published Version","date_published":"2016-08-01T00:00:00Z","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:45:13Z","type":"journal_article","doi":"10.1007/s10009-015-0393-y","publisher":"Springer","citation":{"ieee":"S. Bogomolov <i>et al.</i>, “Guided search for hybrid systems based on coarse-grained space abstractions,” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 18, no. 4. Springer, pp. 449–467, 2016.","mla":"Bogomolov, Sergiy, et al. “Guided Search for Hybrid Systems Based on Coarse-Grained Space Abstractions.” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 18, no. 4, Springer, 2016, pp. 449–67, doi:<a href=\"https://doi.org/10.1007/s10009-015-0393-y\">10.1007/s10009-015-0393-y</a>.","ista":"Bogomolov S, Donzé A, Frehse G, Grosu R, Johnson T, Ladan H, Podelski A, Wehrle M. 2016. Guided search for hybrid systems based on coarse-grained space abstractions. International Journal on Software Tools for Technology Transfer. 18(4), 449–467.","chicago":"Bogomolov, Sergiy, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor Johnson, Hamed Ladan, Andreas Podelski, and Martin Wehrle. “Guided Search for Hybrid Systems Based on Coarse-Grained Space Abstractions.” <i>International Journal on Software Tools for Technology Transfer</i>. Springer, 2016. <a href=\"https://doi.org/10.1007/s10009-015-0393-y\">https://doi.org/10.1007/s10009-015-0393-y</a>.","apa":"Bogomolov, S., Donzé, A., Frehse, G., Grosu, R., Johnson, T., Ladan, H., … Wehrle, M. (2016). Guided search for hybrid systems based on coarse-grained space abstractions. <i>International Journal on Software Tools for Technology Transfer</i>. Springer. <a href=\"https://doi.org/10.1007/s10009-015-0393-y\">https://doi.org/10.1007/s10009-015-0393-y</a>","ama":"Bogomolov S, Donzé A, Frehse G, et al. Guided search for hybrid systems based on coarse-grained space abstractions. <i>International Journal on Software Tools for Technology Transfer</i>. 2016;18(4):449-467. doi:<a href=\"https://doi.org/10.1007/s10009-015-0393-y\">10.1007/s10009-015-0393-y</a>","short":"S. Bogomolov, A. Donzé, G. Frehse, R. Grosu, T. Johnson, H. Ladan, A. Podelski, M. Wehrle, International Journal on Software Tools for Technology Transfer 18 (2016) 449–467."},"intvolume":"        18","day":"01","has_accepted_license":"1","status":"public","abstract":[{"text":"Hybrid systems represent an important and powerful formalism for modeling real-world applications such as embedded systems. A verification tool like SpaceEx is based on the exploration of a symbolic search space (the region space). As a verification tool, it is typically optimized towards proving the absence of errors. In some settings, e.g., when the verification tool is employed in a feedback-directed design cycle, one would like to have the option to call a version that is optimized towards finding an error trajectory in the region space. A recent approach in this direction is based on guided search. Guided search relies on a cost function that indicates which states are promising to be explored, and preferably explores more promising states first. In this paper, we propose an abstraction-based cost function based on coarse-grained space abstractions for guiding the reachability analysis. For this purpose, a suitable abstraction technique that exploits the flexible granularity of modern reachability analysis algorithms is introduced. The new cost function is an effective extension of pattern database approaches that have been successfully applied in other areas. The approach has been implemented in the SpaceEx model checker. The evaluation shows its practical potential.","lang":"eng"}],"ec_funded":1,"pubrep_id":"457","department":[{"_id":"ToHe"}],"oa":1,"title":"Guided search for hybrid systems based on coarse-grained space abstractions","publication_status":"published","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1705","month":"08"},{"file":[{"checksum":"0825eefd4e22774f6f62cb7d7389b05a","relation":"main_file","creator":"system","file_size":243458,"file_name":"IST-2016-645-v1+1_sagt-cr.pdf","access_level":"open_access","date_updated":"2020-07-14T12:44:45Z","file_id":"5073","content_type":"application/pdf","date_created":"2018-12-12T10:14:22Z"}],"volume":9928,"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"date_updated":"2023-08-17T13:52:49Z","date_created":"2018-12-11T11:51:28Z","year":"2016","page":"153 - 166","quality_controlled":"1","scopus_import":1,"type":"conference","file_date_updated":"2020-07-14T12:44:45Z","language":[{"iso":"eng"}],"publisher":"Springer","doi":"10.1007/978-3-662-53354-3_13","author":[{"last_name":"Avni","full_name":"Avni, Guy","first_name":"Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"ddc":["000"],"publist_id":"5926","date_published":"2016-09-01T00:00:00Z","oa_version":"Preprint","conference":{"location":"Liverpool, United Kingdom","end_date":"2016-09-21","name":"SAGT: Symposium on Algorithmic Game Theory","start_date":"2016-09-19"},"abstract":[{"lang":"eng","text":"In resource allocation games, selfish players share resources that are needed in order to fulfill their objectives. The cost of using a resource depends on the load on it. In the traditional setting, the players make their choices concurrently and in one-shot. That is, a strategy for a player is a subset of the resources. We introduce and study dynamic resource allocation games. In this setting, the game proceeds in phases. In each phase each player chooses one resource. A scheduler dictates the order in which the players proceed in a phase, possibly scheduling several players to proceed concurrently. The game ends when each player has collected a set of resources that fulfills his objective. The cost for each player then depends on this set as well as on the load on the resources in it – we consider both congestion and cost-sharing games. We argue that the dynamic setting is the suitable setting for many applications in practice. We study the stability of dynamic resource allocation games, where the appropriate notion of stability is that of subgame perfect equilibrium, study the inefficiency incurred due to selfish behavior, and also study problems that are particular to the dynamic setting, like constraints on the order in which resources can be chosen or the problem of finding a scheduler that achieves stability."}],"status":"public","ec_funded":1,"citation":{"ista":"Avni G, Henzinger TA, Kupferman O. 2016. Dynamic resource allocation games. SAGT: Symposium on Algorithmic Game Theory, LNCS, vol. 9928, 153–166.","apa":"Avni, G., Henzinger, T. A., &#38; Kupferman, O. (2016). Dynamic resource allocation games (Vol. 9928, pp. 153–166). Presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">https://doi.org/10.1007/978-3-662-53354-3_13</a>","chicago":"Avni, Guy, Thomas A Henzinger, and Orna Kupferman. “Dynamic Resource Allocation Games,” 9928:153–66. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">https://doi.org/10.1007/978-3-662-53354-3_13</a>.","mla":"Avni, Guy, et al. <i>Dynamic Resource Allocation Games</i>. Vol. 9928, Springer, 2016, pp. 153–66, doi:<a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">10.1007/978-3-662-53354-3_13</a>.","ieee":"G. Avni, T. A. Henzinger, and O. Kupferman, “Dynamic resource allocation games,” presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom, 2016, vol. 9928, pp. 153–166.","short":"G. Avni, T.A. Henzinger, O. Kupferman, in:, Springer, 2016, pp. 153–166.","ama":"Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. In: Vol 9928. Springer; 2016:153-166. doi:<a href=\"https://doi.org/10.1007/978-3-662-53354-3_13\">10.1007/978-3-662-53354-3_13</a>"},"intvolume":"      9928","has_accepted_license":"1","day":"01","publication_status":"published","title":"Dynamic resource allocation games","oa":1,"related_material":{"record":[{"id":"6761","status":"public","relation":"later_version"}]},"_id":"1341","month":"09","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","alternative_title":["LNCS"],"pubrep_id":"645","department":[{"_id":"ToHe"}],"acknowledgement":"This research was supported in part by the European Research Council (ERC) under grants 267989 (QUAREM) and 278410 (QUALITY), and by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award)."},{"doi":"10.1007/978-3-319-41540-6_21","_id":"1390","month":"07","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publisher":"Springer","language":[{"iso":"eng"}],"publication_status":"published","title":"QLOSE: Program repair with quantitative objectives","type":"conference","conference":{"end_date":"2016-07-23","location":"Toronto, Canada","start_date":"2016-07-17","name":"CAV: Computer Aided Verification"},"oa_version":"None","department":[{"_id":"ToHe"}],"date_published":"2016-07-13T00:00:00Z","alternative_title":["LNCS"],"publist_id":"5819","author":[{"last_name":"D'Antoni","first_name":"Loris","full_name":"D'Antoni, Loris"},{"last_name":"Samanta","full_name":"Samanta, Roopsha","first_name":"Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Rishabh","full_name":"Singh, Rishabh","last_name":"Singh"}],"year":"2016","date_created":"2018-12-11T11:51:45Z","page":"383 - 401","quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"date_updated":"2021-01-12T06:50:21Z","ec_funded":1,"status":"public","volume":9780,"abstract":[{"text":"The goal of automatic program repair is to identify a set of syntactic changes that can turn a program that is incorrect with respect\r\nto a given specification into a correct one. Existing program repair techniques typically aim to find any program that meets the given specification. Such “best-effort” strategies can end up generating a program that is quite different from the original one. Novel techniques have been proposed to compute syntactically minimal program fixes, but the smallest syntactic fix to a program can still significantly alter the original program’s behaviour. We propose a new approach to program repair based on program distances, which can quantify changes not only to the program syntax but also to the program semantics. We call this the quantitative program repair problem where the “optimal” repair is derived using multiple distances. We implement a solution to the quantitative repair\r\nproblem in a prototype tool called Qlose\r\n(Quantitatively close), using the program synthesizer Sketch. We evaluate the effectiveness of different distances in obtaining desirable repairs by evaluating\r\nQlose on programs taken from educational tools such as CodeHunt and edX.","lang":"eng"}],"day":"13","citation":{"ama":"D’Antoni L, Samanta R, Singh R. QLOSE: Program repair with quantitative objectives. In: Vol 9780. Springer; 2016:383-401. doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">10.1007/978-3-319-41540-6_21</a>","short":"L. D’Antoni, R. Samanta, R. Singh, in:, Springer, 2016, pp. 383–401.","ieee":"L. D’Antoni, R. Samanta, and R. Singh, “QLOSE: Program repair with quantitative objectives,” presented at the CAV: Computer Aided Verification, Toronto, Canada, 2016, vol. 9780, pp. 383–401.","mla":"D’Antoni, Loris, et al. <i>QLOSE: Program Repair with Quantitative Objectives</i>. Vol. 9780, Springer, 2016, pp. 383–401, doi:<a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">10.1007/978-3-319-41540-6_21</a>.","chicago":"D’Antoni, Loris, Roopsha Samanta, and Rishabh Singh. “QLOSE: Program Repair with Quantitative Objectives,” 9780:383–401. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">https://doi.org/10.1007/978-3-319-41540-6_21</a>.","ista":"D’Antoni L, Samanta R, Singh R. 2016. QLOSE: Program repair with quantitative objectives. CAV: Computer Aided Verification, LNCS, vol. 9780, 383–401.","apa":"D’Antoni, L., Samanta, R., &#38; Singh, R. (2016). QLOSE: Program repair with quantitative objectives (Vol. 9780, pp. 383–401). Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer. <a href=\"https://doi.org/10.1007/978-3-319-41540-6_21\">https://doi.org/10.1007/978-3-319-41540-6_21</a>"},"intvolume":"      9780","scopus_import":1}]