[{"date_published":"2017-12-01T00:00:00Z","page":"765 - 787","citation":{"chicago":"Giacobbe, Mirco, Calin C Guet, Ashutosh Gupta, Thomas A Henzinger, Tiago Paixao, and Tatjana Petrov. “Model Checking the Evolution of Gene Regulatory Networks.” Acta Informatica. Springer, 2017. https://doi.org/10.1007/s00236-016-0278-x.","short":"M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, Acta Informatica 54 (2017) 765–787.","mla":"Giacobbe, Mirco, et al. “Model Checking the Evolution of Gene Regulatory Networks.” Acta Informatica, vol. 54, no. 8, Springer, 2017, pp. 765–87, doi:10.1007/s00236-016-0278-x.","ieee":"M. Giacobbe, C. C. Guet, A. Gupta, T. A. Henzinger, T. Paixao, and T. Petrov, “Model checking the evolution of gene regulatory networks,” Acta Informatica, vol. 54, no. 8. Springer, pp. 765–787, 2017.","apa":"Giacobbe, M., Guet, C. C., Gupta, A., Henzinger, T. A., Paixao, T., & Petrov, T. (2017). Model checking the evolution of gene regulatory networks. Acta Informatica. Springer. https://doi.org/10.1007/s00236-016-0278-x","ista":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. 2017. Model checking the evolution of gene regulatory networks. Acta Informatica. 54(8), 765–787.","ama":"Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking the evolution of gene regulatory networks. Acta Informatica. 2017;54(8):765-787. doi:10.1007/s00236-016-0278-x"},"publication":"Acta Informatica","article_processing_charge":"No","has_accepted_license":"1","day":"01","scopus_import":"1","oa_version":"Published Version","file":[{"checksum":"4e661d9135d7f8c342e8e258dee76f3e","date_created":"2019-01-17T15:57:29Z","date_updated":"2020-07-14T12:44:46Z","relation":"main_file","file_id":"5841","file_size":755241,"content_type":"application/pdf","creator":"dernst","access_level":"open_access","file_name":"2017_ActaInformatica_Giacobbe.pdf"}],"pubrep_id":"649","intvolume":" 54","status":"public","title":"Model checking the evolution of gene regulatory networks","ddc":["006","576"],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"1351","issue":"8","abstract":[{"lang":"eng","text":"The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs—an important problem of interest in evolutionary biology—more efficiently than the classical simulation method. We specify the property in linear temporal logic. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights."}],"type":"journal_article","language":[{"iso":"eng"}],"doi":"10.1007/s00236-016-0278-x","project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"name":"Speed of Adaptation in Population Genetics and Evolutionary Computation","call_identifier":"FP7","grant_number":"618091","_id":"25B1EC9E-B435-11E9-9278-68D0E5697425"},{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"},{"_id":"25B07788-B435-11E9-9278-68D0E5697425","grant_number":"250152","call_identifier":"FP7","name":"Limits to selection in biology and in evolutionary computation"}],"quality_controlled":"1","isi":1,"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"isi":["000414343200003"]},"publication_identifier":{"issn":["00015903"]},"month":"12","volume":54,"date_updated":"2023-09-20T11:06:03Z","date_created":"2018-12-11T11:51:32Z","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"1835"}]},"author":[{"full_name":"Giacobbe, Mirco","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8180-0904","first_name":"Mirco","last_name":"Giacobbe"},{"full_name":"Guet, Calin C","orcid":"0000-0001-6220-2052","id":"47F8433E-F248-11E8-B48F-1D18A9856A87","last_name":"Guet","first_name":"Calin C"},{"full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","first_name":"Ashutosh"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"first_name":"Tiago","last_name":"Paixao","id":"2C5658E6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-2361-3953","full_name":"Paixao, Tiago"},{"orcid":"0000-0002-9041-0905","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","last_name":"Petrov","first_name":"Tatjana","full_name":"Petrov, Tatjana"}],"publisher":"Springer","department":[{"_id":"ToHe"},{"_id":"CaGu"},{"_id":"NiBa"}],"publication_status":"published","year":"2017","license":"https://creativecommons.org/licenses/by/4.0/","publist_id":"5898","ec_funded":1,"file_date_updated":"2020-07-14T12:44:46Z"},{"publisher":"Elsevier","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2017","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/","volume":23,"date_updated":"2023-09-20T11:18:50Z","date_created":"2018-12-11T11:50:39Z","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"ec_funded":1,"publist_id":"6154","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"}],"quality_controlled":"1","isi":1,"external_id":{"isi":["000390637000011"]},"language":[{"iso":"eng"}],"doi":"10.1016/j.nahs.2016.09.001","month":"02","intvolume":" 23","title":"Model measuring for discrete and hybrid systems","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"1196","oa_version":"None","type":"journal_article","abstract":[{"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.","lang":"eng"}],"page":"166 - 190","citation":{"ama":"Henzinger TA, Otop J. Model measuring for discrete and hybrid systems. Nonlinear Analysis: Hybrid Systems. 2017;23:166-190. doi:10.1016/j.nahs.2016.09.001","ista":"Henzinger TA, Otop J. 2017. Model measuring for discrete and hybrid systems. Nonlinear Analysis: Hybrid Systems. 23, 166–190.","ieee":"T. A. Henzinger and J. Otop, “Model measuring for discrete and hybrid systems,” Nonlinear Analysis: Hybrid Systems, vol. 23. Elsevier, pp. 166–190, 2017.","apa":"Henzinger, T. A., & Otop, J. (2017). Model measuring for discrete and hybrid systems. Nonlinear Analysis: Hybrid Systems. Elsevier. https://doi.org/10.1016/j.nahs.2016.09.001","mla":"Henzinger, Thomas A., and Jan Otop. “Model Measuring for Discrete and Hybrid Systems.” Nonlinear Analysis: Hybrid Systems, vol. 23, Elsevier, 2017, pp. 166–90, doi:10.1016/j.nahs.2016.09.001.","short":"T.A. Henzinger, J. Otop, Nonlinear Analysis: Hybrid Systems 23 (2017) 166–190.","chicago":"Henzinger, Thomas A, and Jan Otop. “Model Measuring for Discrete and Hybrid Systems.” Nonlinear Analysis: Hybrid Systems. Elsevier, 2017. https://doi.org/10.1016/j.nahs.2016.09.001."},"publication":"Nonlinear Analysis: Hybrid Systems","date_published":"2017-02-01T00:00:00Z","scopus_import":"1","article_processing_charge":"No","day":"01"},{"citation":{"short":"G. Avni, S. Goel, T.A. Henzinger, G. Rodríguez Navas, in:, Springer, 2017, pp. 169–187.","mla":"Avni, Guy, et al. Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults. Vol. 10206, Springer, 2017, pp. 169–87, doi:10.1007/978-3-662-54580-5_10.","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. https://doi.org/10.1007/978-3-662-54580-5_10.","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:10.1007/978-3-662-54580-5_10","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.","apa":"Avni, G., Goel, S., Henzinger, T. A., & 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. https://doi.org/10.1007/978-3-662-54580-5_10","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."},"page":"169 - 187","date_published":"2017-03-31T00:00:00Z","scopus_import":"1","day":"31","has_accepted_license":"1","article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"1116","ddc":["000"],"title":"Computing scores of forwarding schemes in switched networks with probabilistic faults","status":"public","intvolume":" 10206","pubrep_id":"758","oa_version":"Submitted Version","file":[{"relation":"main_file","file_id":"4698","date_created":"2018-12-12T10:08:37Z","date_updated":"2018-12-12T10:08:37Z","access_level":"open_access","file_name":"IST-2017-758-v1+1_tacas-cr.pdf","file_size":321800,"content_type":"application/pdf","creator":"system"}],"type":"conference","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"Time-triggered switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. Due to the criticality of the applications running over them, developers need to ensure that end-to-end communication is dependable and predictable. Traditional approaches assume static networks that are not flexible to changes caused by reconfigurations or, more importantly, faults, which are dealt with in the application using redundancy. We adopt the concept of handling faults in the switches from non-real-time networks while maintaining the required predictability. \r\n\r\nWe study a class of forwarding schemes that can handle various types of failures. We consider probabilistic failures. We study a class of forwarding schemes that can handle various types of failures. We consider probabilistic failures. For a given network with a forwarding scheme and a constant ℓ, we compute the {\\em score} of the scheme, namely the probability (induced by faults) that at least ℓ messages arrive on time. We reduce the scoring problem to a reachability problem on a Markov chain with a "product-like" 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. "}],"external_id":{"isi":["000440733400010"]},"oa":1,"isi":1,"quality_controlled":"1","project":[{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"conference":{"end_date":"2017-04-29","location":"Uppsala, Sweden","start_date":"2017-04-22","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"doi":"10.1007/978-3-662-54580-5_10","language":[{"iso":"eng"}],"month":"03","publication_identifier":{"issn":["03029743"]},"year":"2017","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer","author":[{"first_name":"Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy"},{"full_name":"Goel, Shubham","first_name":"Shubham","last_name":"Goel"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"last_name":"Rodríguez Navas","first_name":"Guillermo","full_name":"Rodríguez Navas, Guillermo"}],"date_updated":"2023-09-20T11:32:43Z","date_created":"2018-12-11T11:50:14Z","volume":10206,"file_date_updated":"2018-12-12T10:08:37Z","publist_id":"6246"},{"day":"01","article_processing_charge":"No","scopus_import":"1","date_published":"2017-06-01T00:00:00Z","page":"143 - 166","publication":"Information and Computation","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner. “Quantitative Fair Simulation Games.” Information and Computation. Elsevier, 2017. https://doi.org/10.1016/j.ic.2016.10.006.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Fair Simulation Games.” Information and Computation, vol. 254, no. 2, Elsevier, 2017, pp. 143–66, doi:10.1016/j.ic.2016.10.006.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Information and Computation 254 (2017) 143–166.","ista":"Chatterjee K, Henzinger TA, Otop J, Velner Y. 2017. Quantitative fair simulation games. Information and Computation. 254(2), 143–166.","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, “Quantitative fair simulation games,” Information and Computation, vol. 254, no. 2. Elsevier, pp. 143–166, 2017.","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., & Velner, Y. (2017). Quantitative fair simulation games. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2016.10.006","ama":"Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative fair simulation games. Information and Computation. 2017;254(2):143-166. doi:10.1016/j.ic.2016.10.006"},"abstract":[{"text":"Simulation is an attractive alternative to language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. While fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable in general, whereas the (quantitative) simulation reduces to quantitative games, which admit pseudo-polynomial time algorithms.\r\n\r\nIn this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games, yet they still admit pseudo-polynomial time algorithms.","lang":"eng"}],"issue":"2","type":"journal_article","oa_version":"None","title":"Quantitative fair simulation games","status":"public","intvolume":" 254","_id":"1066","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","month":"06","language":[{"iso":"eng"}],"doi":"10.1016/j.ic.2016.10.006","quality_controlled":"1","isi":1,"project":[{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"external_id":{"isi":["000402025600002"]},"publist_id":"6322","ec_funded":1,"date_updated":"2023-09-20T12:07:48Z","date_created":"2018-12-11T11:49:58Z","volume":254,"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Otop"},{"full_name":"Velner, Yaron","last_name":"Velner","first_name":"Yaron"}],"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5428"}]},"publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"Elsevier","year":"2017"},{"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"orcid":"0000-0001-7745-9117","id":"320FC952-F248-11E8-B48F-1D18A9856A87","last_name":"Kragl","first_name":"Bernhard","full_name":"Kragl, Bernhard"},{"first_name":"Samarth","last_name":"Mishra","full_name":"Mishra, Samarth"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas"}],"volume":10201,"date_updated":"2023-09-22T09:44:50Z","date_created":"2018-12-11T11:49:41Z","year":"2017","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"editor":[{"last_name":"Yang","first_name":"Hongseok","full_name":"Yang, Hongseok"}],"publisher":"Springer","publication_status":"published","publist_id":"6384","ec_funded":1,"doi":"10.1007/978-3-662-54434-1_11","conference":{"name":"ESOP: European Symposium on Programming","location":"Uppsala, Sweden","start_date":"2017-04-22","end_date":"2017-04-29"},"language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1701.04914"}],"oa":1,"external_id":{"isi":["000681702400011"]},"project":[{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"quality_controlled":"1","isi":1,"publication_identifier":{"issn":["03029743"]},"month":"03","oa_version":"Submitted Version","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"1011","intvolume":" 10201","status":"public","title":"Faster algorithms for weighted recursive state machines","abstract":[{"lang":"eng","text":"Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly equivalent, are standard models for interprocedural analysis. Yet RSMs are more convenient as they (a) explicitly model function calls and returns, and (b) specify many natural parameters for algorithmic analysis, e.g., the number of entries and exits. We consider a general framework where RSM transitions are labeled from a semiring and path properties are algebraic with semiring operations, which can model, e.g., interprocedural reachability and dataflow analysis problems. Our main contributions are new algorithms for several fundamental problems. As compared to a direct translation of RSMs to PDSs and the best-known existing bounds of PDSs, our analysis algorithm improves the complexity for finite-height semirings (that subsumes reachability and standard dataflow properties). We further consider the problem of extracting distance values from the representation structures computed by our algorithm, and give efficient algorithms that distinguish the complexity of a one-time preprocessing from the complexity of each individual query. Another advantage of our algorithm is that our improvements carry over to the concurrent setting, where we improve the bestknown complexity for the context-bounded analysis of concurrent RSMs. Finally, we provide a prototype implementation that gives a significant speed-up on several benchmarks from the SLAM/SDV project."}],"type":"conference","alternative_title":["LNCS"],"date_published":"2017-03-19T00:00:00Z","citation":{"chicago":"Chatterjee, Krishnendu, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis. “Faster Algorithms for Weighted Recursive State Machines.” edited by Hongseok Yang, 10201:287–313. Springer, 2017. https://doi.org/10.1007/978-3-662-54434-1_11.","mla":"Chatterjee, Krishnendu, et al. Faster Algorithms for Weighted Recursive State Machines. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313, doi:10.1007/978-3-662-54434-1_11.","short":"K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.), Springer, 2017, pp. 287–313.","ista":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. 2017. Faster algorithms for weighted recursive state machines. ESOP: European Symposium on Programming, LNCS, vol. 10201, 287–313.","ieee":"K. Chatterjee, B. Kragl, S. Mishra, and A. Pavlogiannis, “Faster algorithms for weighted recursive state machines,” presented at the ESOP: European Symposium on Programming, Uppsala, Sweden, 2017, vol. 10201, pp. 287–313.","apa":"Chatterjee, K., Kragl, B., Mishra, S., & Pavlogiannis, A. (2017). Faster algorithms for weighted recursive state machines. In H. Yang (Ed.) (Vol. 10201, pp. 287–313). Presented at the ESOP: European Symposium on Programming, Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54434-1_11","ama":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. Faster algorithms for weighted recursive state machines. In: Yang H, ed. Vol 10201. Springer; 2017:287-313. doi:10.1007/978-3-662-54434-1_11"},"page":"287 - 313","article_processing_charge":"No","day":"19","scopus_import":"1"},{"conference":{"start_date":"2017-08-19","location":"Melbourne, Australia","end_date":"2017-08-25","name":"IJCAI: International Joint Conference on Artificial Intelligence "},"doi":"10.24963/ijcai.2017/11","language":[{"iso":"eng"}],"oa":1,"external_id":{"isi":["000764137500011"]},"quality_controlled":"1","isi":1,"project":[{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"month":"05","publication_identifier":{"issn":["10450823"]},"author":[{"full_name":"Avni, Guy","last_name":"Avni","first_name":"Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Guha","first_name":"Shibashis","full_name":"Guha, Shibashis"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"}],"related_material":{"record":[{"id":"6006","relation":"later_version","status":"public"}]},"date_updated":"2023-09-22T09:49:00Z","date_created":"2018-12-11T11:49:38Z","year":"2017","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"AAAI Press","file_date_updated":"2018-12-12T10:16:58Z","publist_id":"6395","date_published":"2017-05-30T00:00:00Z","citation":{"ama":"Avni G, Guha S, Kupferman O. An abstraction-refinement methodology for reasoning about network games. In: AAAI Press; 2017:70-76. doi:10.24963/ijcai.2017/11","ista":"Avni G, Guha S, Kupferman O. 2017. An abstraction-refinement methodology for reasoning about network games. IJCAI: International Joint Conference on Artificial Intelligence , 70–76.","apa":"Avni, G., Guha, S., & Kupferman, O. (2017). An abstraction-refinement methodology for reasoning about network games (pp. 70–76). Presented at the IJCAI: International Joint Conference on Artificial Intelligence , Melbourne, Australia: AAAI Press. https://doi.org/10.24963/ijcai.2017/11","ieee":"G. Avni, S. Guha, and O. Kupferman, “An abstraction-refinement methodology for reasoning about network games,” presented at the IJCAI: International Joint Conference on Artificial Intelligence , Melbourne, Australia, 2017, pp. 70–76.","mla":"Avni, Guy, et al. An Abstraction-Refinement Methodology for Reasoning about Network Games. AAAI Press, 2017, pp. 70–76, doi:10.24963/ijcai.2017/11.","short":"G. Avni, S. Guha, O. Kupferman, in:, AAAI Press, 2017, pp. 70–76.","chicago":"Avni, Guy, Shibashis Guha, and Orna Kupferman. “An Abstraction-Refinement Methodology for Reasoning about Network Games,” 70–76. AAAI Press, 2017. https://doi.org/10.24963/ijcai.2017/11."},"page":"70 - 76","day":"30","article_processing_charge":"No","has_accepted_license":"1","scopus_import":"1","pubrep_id":"818","file":[{"relation":"main_file","file_id":"5249","date_updated":"2018-12-12T10:16:58Z","date_created":"2018-12-12T10:16:58Z","file_name":"IST-2017-818-v1+1_allIJCAI_CR.pdf","access_level":"open_access","file_size":365172,"content_type":"application/pdf","creator":"system"}],"oa_version":"Submitted Version","_id":"1003","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","ddc":["004"],"status":"public","title":"An abstraction-refinement methodology for reasoning about network games","abstract":[{"lang":"eng","text":"Network games (NGs) are played on directed graphs and are extensively used in network design and analysis. Search problems for NGs include finding special strategy profiles such as a Nash equilibrium and a globally optimal solution. The networks modeled by NGs may be huge. In formal verification, abstraction has proven to be an extremely effective technique for reasoning about systems with big and even infinite state spaces. We describe an abstraction-refinement methodology for reasoning about NGs. Our methodology is based on an abstraction function that maps the state space of an NG to a much smaller state space. We search for a global optimum and a Nash equilibrium by reasoning on an under- and an overapproximation defined on top of this smaller state space. When the approximations are too coarse to find such profiles, we refine the abstraction function. Our experimental results demonstrate the efficiency of the methodology."}],"type":"conference"},{"oa_version":"None","intvolume":" 10427","status":"public","title":"Model counting for recursively-defined strings","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"962","abstract":[{"lang":"eng","text":"We present a new algorithm for model counting of a class of string constraints. In addition to the classic operation of concatenation, our class includes some recursively defined operations such as Kleene closure, and replacement of substrings. Additionally, our class also includes length constraints on the string expressions, which means, by requiring reasoning about numbers, that we face a multi-sorted logic. In the end, our string constraints are motivated by their use in programming for web applications. Our algorithm comprises two novel features: the ability to use a technique of (1) partial derivatives for constraints that are already in a solved form, i.e. a form where its (string) satisfiability is clearly displayed, and (2) non-progression, where cyclic reasoning in the reduction process may be terminated (thus allowing for the algorithm to look elsewhere). Finally, we experimentally compare our model counter with two recent works on model counting of similar constraints, SMC [18] and ABC [5], to demonstrate its superior performance."}],"alternative_title":["LNCS"],"type":"conference","date_published":"2017-01-01T00:00:00Z","page":"399 - 418","citation":{"chicago":"Trinh, Minh, Duc Hiep Chu, and Joxan Jaffar. “Model Counting for Recursively-Defined Strings.” edited by Rupak Majumdar and Viktor Kunčak, 10427:399–418. Springer, 2017. https://doi.org/10.1007/978-3-319-63390-9_21.","mla":"Trinh, Minh, et al. Model Counting for Recursively-Defined Strings. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer, 2017, pp. 399–418, doi:10.1007/978-3-319-63390-9_21.","short":"M. Trinh, D.H. Chu, J. Jaffar, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 399–418.","ista":"Trinh M, Chu DH, Jaffar J. 2017. Model counting for recursively-defined strings. CAV: Computer Aided Verification, LNCS, vol. 10427, 399–418.","ieee":"M. Trinh, D. H. Chu, and J. Jaffar, “Model counting for recursively-defined strings,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10427, pp. 399–418.","apa":"Trinh, M., Chu, D. H., & Jaffar, J. (2017). Model counting for recursively-defined strings. In R. Majumdar & V. Kunčak (Eds.) (Vol. 10427, pp. 399–418). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63390-9_21","ama":"Trinh M, Chu DH, Jaffar J. Model counting for recursively-defined strings. In: Majumdar R, Kunčak V, eds. Vol 10427. Springer; 2017:399-418. doi:10.1007/978-3-319-63390-9_21"},"article_processing_charge":"No","day":"01","scopus_import":"1","volume":10427,"date_updated":"2023-09-22T09:58:02Z","date_created":"2018-12-11T11:49:26Z","author":[{"full_name":"Trinh, Minh","first_name":"Minh","last_name":"Trinh"},{"id":"3598E630-F248-11E8-B48F-1D18A9856A87","last_name":"Chu","first_name":"Duc Hiep","full_name":"Chu, Duc Hiep"},{"last_name":"Jaffar","first_name":"Joxan","full_name":"Jaffar, Joxan"}],"editor":[{"last_name":"Majumdar","first_name":"Rupak","full_name":"Majumdar, Rupak"},{"full_name":"Kunčak, Viktor","last_name":"Kunčak","first_name":"Viktor"}],"department":[{"_id":"ToHe"}],"publisher":"Springer","publication_status":"published","year":"2017","publist_id":"6443","language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-63390-9_21","conference":{"end_date":"2017-07-28","location":"Heidelberg, Germany","start_date":"2017-07-24","name":"CAV: Computer Aided Verification"},"project":[{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"isi":1,"quality_controlled":"1","external_id":{"isi":["000431900900021"]},"publication_identifier":{"issn":["03029743"]},"month":"01"},{"month":"09","publication_identifier":{"isbn":["978-145035105-8"]},"conference":{"name":"FSE: Foundations of Software Engineering","location":"Paderborn, Germany","start_date":"2017-09-04","end_date":"2017-09-08"},"doi":"10.1145/3106237.3106309","language":[{"iso":"eng"}],"external_id":{"isi":["000414279300055"]},"isi":1,"quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"publist_id":"6477","author":[{"first_name":"Xuan","last_name":"Le","full_name":"Le, Xuan"},{"full_name":"Chu, Duc Hiep","first_name":"Duc Hiep","last_name":"Chu","id":"3598E630-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Lo, David","first_name":"David","last_name":"Lo"},{"last_name":"Le Goues","first_name":"Claire","full_name":"Le Goues, Claire"},{"full_name":"Visser, Willem","last_name":"Visser","first_name":"Willem"}],"date_created":"2018-12-11T11:49:19Z","date_updated":"2023-09-26T15:38:36Z","volume":"F130154","year":"2017","publication_status":"published","publisher":"ACM","department":[{"_id":"ToHe"}],"day":"01","article_processing_charge":"No","scopus_import":"1","date_published":"2017-09-01T00:00:00Z","citation":{"chicago":"Le, Xuan, Duc Hiep Chu, David Lo, Claire Le Goues, and Willem Visser. “S3: Syntax- and Semantic-Guided Repair Synthesis via Programming by Examples,” F130154:593–604. ACM, 2017. https://doi.org/10.1145/3106237.3106309.","mla":"Le, Xuan, et al. S3: Syntax- and Semantic-Guided Repair Synthesis via Programming by Examples. Vol. F130154, ACM, 2017, pp. 593–604, doi:10.1145/3106237.3106309.","short":"X. Le, D.H. Chu, D. Lo, C. Le Goues, W. Visser, in:, ACM, 2017, pp. 593–604.","ista":"Le X, Chu DH, Lo D, Le Goues C, Visser W. 2017. S3: Syntax- and semantic-guided repair synthesis via programming by examples. FSE: Foundations of Software Engineering vol. F130154, 593–604.","apa":"Le, X., Chu, D. H., Lo, D., Le Goues, C., & Visser, W. (2017). S3: Syntax- and semantic-guided repair synthesis via programming by examples (Vol. F130154, pp. 593–604). Presented at the FSE: Foundations of Software Engineering, Paderborn, Germany: ACM. https://doi.org/10.1145/3106237.3106309","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.","ama":"Le X, Chu DH, Lo D, Le Goues C, Visser W. S3: Syntax- and semantic-guided repair synthesis via programming by examples. In: Vol F130154. ACM; 2017:593-604. doi:10.1145/3106237.3106309"},"page":"593 - 604","abstract":[{"lang":"eng","text":"A notable class of techniques for automatic program repair is known as semantics-based. Such techniques, e.g., Angelix, infer semantic specifications via symbolic execution, and then use program synthesis to construct new code that satisfies those inferred specifications. However, the obtained specifications are naturally incomplete, leaving the synthesis engine with a difficult task of synthesizing a general solution from a sparse space of many possible solutions that are consistent with the provided specifications but that do not necessarily generalize. We present S3, a new repair synthesis engine that leverages programming-by-examples methodology to synthesize high-quality bug repairs. The novelty in S3 that allows it to tackle the sparse search space to create more general repairs is three-fold: (1) A systematic way to customize and constrain the syntactic search space via a domain-specific language, (2) An efficient enumeration-based search strategy over the constrained search space, and (3) A number of ranking features based on measures of the syntactic and semantic distances between candidate solutions and the original buggy program. We compare S3’s repair effectiveness with state-of-the-art synthesis engines Angelix, Enumerative, and CVC4. S3 can successfully and correctly fix at least three times more bugs than the best baseline on datasets of 52 bugs in small programs, and 100 bugs in real-world large programs. "}],"type":"conference","oa_version":"None","_id":"942","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","title":"S3: Syntax- and semantic-guided repair synthesis via programming by examples","status":"public"},{"page":"267 - 269","isi":1,"quality_controlled":"1","citation":{"chicago":"Gottlob, Georg, Thomas A Henzinger, and Georg Weißenbacher. “Preface of the Special Issue in Memoriam Helmut Veith.” Formal Methods in System Design. Springer, 2017. https://doi.org/10.1007/s10703-017-0307-6.","short":"G. Gottlob, T.A. Henzinger, G. Weißenbacher, Formal Methods in System Design 51 (2017) 267–269.","mla":"Gottlob, Georg, et al. “Preface of the Special Issue in Memoriam Helmut Veith.” Formal Methods in System Design, vol. 51, no. 2, Springer, 2017, pp. 267–69, doi:10.1007/s10703-017-0307-6.","ieee":"G. Gottlob, T. A. Henzinger, and G. Weißenbacher, “Preface of the special issue in memoriam Helmut Veith,” Formal Methods in System Design, vol. 51, no. 2. Springer, pp. 267–269, 2017.","apa":"Gottlob, G., Henzinger, T. A., & Weißenbacher, G. (2017). Preface of the special issue in memoriam Helmut Veith. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-017-0307-6","ista":"Gottlob G, Henzinger TA, Weißenbacher G. 2017. Preface of the special issue in memoriam Helmut Veith. Formal Methods in System Design. 51(2), 267–269.","ama":"Gottlob G, Henzinger TA, Weißenbacher G. Preface of the special issue in memoriam Helmut Veith. Formal Methods in System Design. 2017;51(2):267-269. doi:10.1007/s10703-017-0307-6"},"external_id":{"isi":["000415615600001"]},"publication":"Formal Methods in System Design","language":[{"iso":"eng"}],"doi":"10.1007/s10703-017-0307-6","date_published":"2017-11-14T00:00:00Z","article_processing_charge":"No","month":"11","day":"14","publisher":"Springer","department":[{"_id":"ToHe"}],"intvolume":" 51","title":"Preface of the special issue in memoriam Helmut Veith","status":"public","publication_status":"published","_id":"743","year":"2017","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","volume":51,"oa_version":"None","date_updated":"2023-09-27T12:29:29Z","date_created":"2018-12-11T11:48:16Z","author":[{"last_name":"Gottlob","first_name":"Georg","full_name":"Gottlob, Georg"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Weißenbacher, Georg","last_name":"Weißenbacher","first_name":"Georg"}],"type":"journal_article","issue":"2","publist_id":"6924","abstract":[{"text":"This special issue of the Journal on Formal Methods in System Design is dedicated to Prof. Helmut Veith, who unexpectedly passed away in March 2016. Helmut Veith was a brilliant researcher, inspiring collaborator, passionate mentor, generous friend, and valued member of the formal methods community. Helmut was not only known for his numerous and influential contributions in the field of automated verification (most prominently his work on Counterexample-Guided Abstraction Refinement [1,2]), but also for his untiring and passionate efforts for the logic community: he co-organized the Vienna Summer of Logic (an event comprising twelve conferences and numerous workshops which attracted thousands of researchers from all over the world), he initiated the Vienna Center for Logic and Algorithms (which promotes international collaboration on logic and algorithms and organizes outreach events such as the LogicLounge), and he coordinated the Doctoral Program on Logical Methods in Computer Science at TU Wien (currently educating more than 40 doctoral students) and a National Research Network on Rigorous Systems Engineering (uniting fifteen researchers in Austria to address the challenge of building reliable and safe computer\r\nsystems). With his enthusiasm and commitment, Helmut completely reshaped the Austrian research landscape in the field of logic and verification in his few years as a full professor at TU Wien.","lang":"eng"}]},{"file_date_updated":"2020-07-14T12:47:00Z","publist_id":"7264","date_created":"2018-12-11T11:47:07Z","date_updated":"2023-10-17T12:02:46Z","volume":259,"author":[{"first_name":"Bernd","last_name":"Finkbeiner","full_name":"Finkbeiner, Bernd"},{"last_name":"Kupriyanov","first_name":"Andrey","id":"2C311BF8-F248-11E8-B48F-1D18A9856A87","full_name":"Kupriyanov, Andrey"}],"publication_status":"published","publisher":"Open Publishing Association","department":[{"_id":"ToHe"}],"year":"2017","month":"10","publication_identifier":{"issn":["2075-2180"]},"language":[{"iso":"eng"}],"conference":{"start_date":"2017-04-29","location":"Uppsala, Sweden","end_date":"2017-04-29","name":"CREST: Causal Reasoning for Embedded and Safety-Critical Systems Technologies"},"doi":"10.4204/EPTCS.259.3","quality_controlled":"1","project":[{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"main_file_link":[{"url":"https://arxiv.org/abs/1710.03391v1","open_access":"1"}],"oa":1,"abstract":[{"lang":"eng","text":"Model checking is usually based on a comprehensive traversal of the state space. Causality-based model checking is a radically different approach that instead analyzes the cause-effect relationships in a program. We give an overview on a new class of model checking algorithms that capture the causal relationships in a special data structure called concurrent traces. Concurrent traces identify key events in an execution history and link them through their cause-effect relationships. The model checker builds a tableau of concurrent traces, where the case splits represent different causal explanations of a hypothetical error. Causality-based model checking has been implemented in the ARCTOR tool, and applied to previously intractable multi-threaded benchmarks."}],"alternative_title":["EPTCS"],"type":"conference","oa_version":"Submitted Version","file":[{"file_name":"IST-2018-925-v1+1_1710.03391v1.pdf","access_level":"open_access","creator":"system","file_size":209294,"content_type":"application/pdf","file_id":"4939","relation":"main_file","date_created":"2018-12-12T10:12:21Z","date_updated":"2020-07-14T12:47:00Z","checksum":"6274f6c0da3376a7b079180d81568518"}],"pubrep_id":"925","ddc":["004"],"title":"Causality-based model checking","status":"public","intvolume":" 259","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"549","day":"10","has_accepted_license":"1","article_processing_charge":"No","scopus_import":"1","date_published":"2017-10-10T00:00:00Z","page":"31 - 38","publication":"Electronic Proceedings in Theoretical Computer Science","citation":{"ista":"Finkbeiner B, Kupriyanov A. 2017. Causality-based model checking. Electronic Proceedings in Theoretical Computer Science. CREST: Causal Reasoning for Embedded and Safety-Critical Systems Technologies, EPTCS, vol. 259, 31–38.","ieee":"B. Finkbeiner and A. Kupriyanov, “Causality-based model checking,” in Electronic Proceedings in Theoretical Computer Science, Uppsala, Sweden, 2017, vol. 259, pp. 31–38.","apa":"Finkbeiner, B., & Kupriyanov, A. (2017). Causality-based model checking. In Electronic Proceedings in Theoretical Computer Science (Vol. 259, pp. 31–38). Uppsala, Sweden: Open Publishing Association. https://doi.org/10.4204/EPTCS.259.3","ama":"Finkbeiner B, Kupriyanov A. Causality-based model checking. In: Electronic Proceedings in Theoretical Computer Science. Vol 259. Open Publishing Association; 2017:31-38. doi:10.4204/EPTCS.259.3","chicago":"Finkbeiner, Bernd, and Andrey Kupriyanov. “Causality-Based Model Checking.” In Electronic Proceedings in Theoretical Computer Science, 259:31–38. Open Publishing Association, 2017. https://doi.org/10.4204/EPTCS.259.3.","mla":"Finkbeiner, Bernd, and Andrey Kupriyanov. “Causality-Based Model Checking.” Electronic Proceedings in Theoretical Computer Science, vol. 259, Open Publishing Association, 2017, pp. 31–38, doi:10.4204/EPTCS.259.3.","short":"B. Finkbeiner, A. Kupriyanov, in:, Electronic Proceedings in Theoretical Computer Science, Open Publishing Association, 2017, pp. 31–38."}},{"quality_controlled":"1","project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"language":[{"iso":"eng"}],"conference":{"name":"MFCS: Mathematical Foundations of Computer Science (SG)","location":"Krakow; Poland","start_date":"2016-08-22","end_date":"2016-08-26"},"doi":"10.4230/LIPIcs.MFCS.2016.24","month":"08","publication_status":"published","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23\r\n(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna\r\nScience and Technology Fund (WWTF) through project ICT15-003 and by the National Science Centre\r\n(NCN), Poland under grant 2014/15/D/ST6/04543.","year":"2016","date_created":"2018-12-11T11:50:05Z","date_updated":"2021-01-12T06:48:12Z","volume":58,"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"article_number":"24","file_date_updated":"2018-12-12T10:17:31Z","ec_funded":1,"publist_id":"6286","citation":{"ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted limit-average automata of bounded width,” presented at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow; Poland, 2016, vol. 58.","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Nested weighted limit-average automata of bounded width (Vol. 58). Presented at the MFCS: Mathematical Foundations of Computer Science (SG), Krakow; Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.MFCS.2016.24","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Nested weighted limit-average automata of bounded width. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 58, 24.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted limit-average automata of bounded width. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.MFCS.2016.24","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Limit-Average Automata of Bounded Width,” Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. https://doi.org/10.4230/LIPIcs.MFCS.2016.24.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","mla":"Chatterjee, Krishnendu, et al. Nested Weighted Limit-Average Automata of Bounded Width. Vol. 58, 24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.MFCS.2016.24."},"date_published":"2016-08-01T00:00:00Z","scopus_import":1,"day":"01","has_accepted_license":"1","title":"Nested weighted limit-average automata of bounded width","ddc":["004"],"status":"public","intvolume":" 58","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1090","oa_version":"Published Version","file":[{"access_level":"open_access","file_name":"IST-2017-795-v1+1_LIPIcs-MFCS-2016-24.pdf","content_type":"application/pdf","file_size":564560,"creator":"system","relation":"main_file","file_id":"5286","date_created":"2018-12-12T10:17:31Z","date_updated":"2018-12-12T10:17:31Z"}],"pubrep_id":"795","alternative_title":["LIPIcs"],"type":"conference","abstract":[{"lang":"eng","text":" While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e.g., average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e.g., for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e.g., average response time with no overlapping requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i.e., emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness."}]},{"article_number":"6","file_date_updated":"2018-12-12T10:10:10Z","ec_funded":1,"publist_id":"6280","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","year":"2016","acknowledgement":"This work has been supported by the National Research Network RiSE on Rigorous Systems Engineering\r\n(Austrian Science Fund (FWF): S11402-N23, S11403-N23, S11404-N23, S11411-N23), a Google\r\nPhD Fellowship, an Erwin Schrödinger Fellowship (Austrian Science Fund (FWF): J3696-N26), EPSRC\r\ngrants EP/H005633/1 and EP/K008528/1, the Vienna Science and Technology Fund (WWTF) trough\r\ngrant PROSEED, the European Research Council (ERC) under grant 267989 (QUAREM) and by the\r\nAustrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","date_updated":"2021-01-12T06:48:14Z","date_created":"2018-12-11T11:50:07Z","volume":59,"author":[{"first_name":"Andreas","last_name":"Haas","full_name":"Haas, Andreas"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Holzer, Andreas","first_name":"Andreas","last_name":"Holzer"},{"full_name":"Kirsch, Christoph","first_name":"Christoph","last_name":"Kirsch"},{"last_name":"Lippautz","first_name":"Michael","full_name":"Lippautz, Michael"},{"last_name":"Payer","first_name":"Hannes","full_name":"Payer, Hannes"},{"full_name":"Sezgin, Ali","id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","first_name":"Ali","last_name":"Sezgin"},{"full_name":"Sokolova, Ana","first_name":"Ana","last_name":"Sokolova"},{"first_name":"Helmut","last_name":"Veith","full_name":"Veith, Helmut"}],"month":"08","quality_controlled":"1","project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"language":[{"iso":"eng"}],"conference":{"name":"CONCUR: Concurrency Theory","end_date":"2016-08-26","start_date":"2016-08-23","location":"Quebec City; Canada"},"doi":"10.4230/LIPIcs.CONCUR.2016.6","alternative_title":["LIPIcs"],"type":"conference","abstract":[{"lang":"eng","text":" The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Nevertheless, for applications that do not require all guarantees offered by linearizability, recent research has focused on improving performance and scalability of concurrent data structures by relaxing their semantics. In this paper, we present local linearizability, a relaxed consistency condition that is applicable to container-type concurrent data structures like pools, queues, and stacks. While linearizability requires that the effect of each operation is observed by all threads at the same time, local linearizability only requires that for each thread T, the effects of its local insertion operations and the effects of those removal operations that remove values inserted by T are observed by all threads at the same time. We investigate theoretical and practical properties of local linearizability and its relationship to many existing consistency conditions. We present a generic implementation method for locally linearizable data structures that uses existing linearizable data structures as building blocks. Our implementations show performance and scalability improvements over the original building blocks and outperform the fastest existing container-type implementations. "}],"title":"Local linearizability for concurrent container-type data structures","ddc":["004"],"status":"public","intvolume":" 59","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1095","oa_version":"Published Version","file":[{"date_created":"2018-12-12T10:10:10Z","date_updated":"2018-12-12T10:10:10Z","file_id":"4795","relation":"main_file","creator":"system","file_size":589747,"content_type":"application/pdf","file_name":"IST-2017-793-v1+1_LIPIcs-CONCUR-2016-6.pdf","access_level":"open_access"}],"pubrep_id":"793","scopus_import":1,"day":"01","has_accepted_license":"1","publication":"Leibniz International Proceedings in Informatics","citation":{"chicago":"Haas, Andreas, Thomas A Henzinger, Andreas Holzer, Christoph Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. “Local Linearizability for Concurrent Container-Type Data Structures.” In Leibniz International Proceedings in Informatics, Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.6.","mla":"Haas, Andreas, et al. “Local Linearizability for Concurrent Container-Type Data Structures.” Leibniz International Proceedings in Informatics, vol. 59, 6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.6.","short":"A. Haas, T.A. Henzinger, A. Holzer, C. Kirsch, M. Lippautz, H. Payer, A. Sezgin, A. Sokolova, H. Veith, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","ista":"Haas A, Henzinger TA, Holzer A, Kirsch C, Lippautz M, Payer H, Sezgin A, Sokolova A, Veith H. 2016. Local linearizability for concurrent container-type data structures. Leibniz International Proceedings in Informatics. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 6.","apa":"Haas, A., Henzinger, T. A., Holzer, A., Kirsch, C., Lippautz, M., Payer, H., … Veith, H. (2016). Local linearizability for concurrent container-type data structures. In Leibniz International Proceedings in Informatics (Vol. 59). Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2016.6","ieee":"A. Haas et al., “Local linearizability for concurrent container-type data structures,” in Leibniz International Proceedings in Informatics, Quebec City; Canada, 2016, vol. 59.","ama":"Haas A, Henzinger TA, Holzer A, et al. Local linearizability for concurrent container-type data structures. In: Leibniz International Proceedings in Informatics. Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.6"},"date_published":"2016-08-01T00:00:00Z"},{"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1103","year":"2016","acknowledgement":"This work was supported in part by DST-SERB, GoI under Project No. YSS/2014/000623 and by the European Research Council (ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).","status":"public","publication_status":"published","title":"Parallel reachability analysis for hybrid systems","department":[{"_id":"ToHe"}],"publisher":"IEEE","author":[{"first_name":"Amit","last_name":"Gurung","full_name":"Gurung, Amit"},{"first_name":"Arup","last_name":"Deka","full_name":"Deka, Arup"},{"full_name":"Bartocci, Ezio","last_name":"Bartocci","first_name":"Ezio"},{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365","first_name":"Sergiy","last_name":"Bogomolov","full_name":"Bogomolov, Sergiy"},{"last_name":"Grosu","first_name":"Radu","full_name":"Grosu, Radu"},{"full_name":"Ray, Rajarshi","last_name":"Ray","first_name":"Rajarshi"}],"date_created":"2018-12-11T11:50:09Z","date_updated":"2021-01-12T06:48:18Z","oa_version":"Preprint","article_number":"7797741","type":"conference","abstract":[{"lang":"eng","text":"We propose two parallel state-space-exploration algorithms for hybrid automaton (HA), with the goal of enhancing performance on multi-core shared-memory systems. The first uses the parallel, breadth-first-search algorithm (PBFS) of the SPIN model checker, when traversing the discrete modes of the HA, and enhances it with a parallel exploration of the continuous states within each mode. We show that this simple-minded extension of PBFS does not provide the desired load balancing in many HA benchmarks. The second algorithm is a task-parallel BFS algorithm (TP-BFS), which uses a cheap precomputation of the cost associated with the post operations (both continuous and discrete) in order to improve load balancing. We illustrate the TP-BFS and the cost precomputation of the post operators on a support-function-based algorithm for state-space exploration. The performance comparison of the two algorithms shows that, in general, TP-BFS provides a better utilization/load-balancing of the CPU. Both algorithms are implemented in the model checker XSpeed. Our experiments show a maximum speed-up of more than 2000 χ on a navigation benchmark, with respect to SpaceEx LGG scenario. In order to make the comparison fair, we employed an equal number of post operations in both tools. To the best of our knowledge, this paper represents the first attempt to provide parallel, reachability-analysis algorithms for HA."}],"ec_funded":1,"publist_id":"6272","citation":{"ama":"Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. Parallel reachability analysis for hybrid systems. In: IEEE; 2016. doi:10.1109/MEMCOD.2016.7797741","ista":"Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. 2016. Parallel reachability analysis for hybrid systems. MEMOCODE: International Conference on Formal Methods and Models for System Design, 7797741.","apa":"Gurung, A., Deka, A., Bartocci, E., Bogomolov, S., Grosu, R., & Ray, R. (2016). Parallel reachability analysis for hybrid systems. Presented at the MEMOCODE: International Conference on Formal Methods and Models for System Design, Kanpur, India : IEEE. https://doi.org/10.1109/MEMCOD.2016.7797741","ieee":"A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, and R. Ray, “Parallel reachability analysis for hybrid systems,” presented at the MEMOCODE: International Conference on Formal Methods and Models for System Design, Kanpur, India , 2016.","mla":"Gurung, Amit, et al. Parallel Reachability Analysis for Hybrid Systems. 7797741, IEEE, 2016, doi:10.1109/MEMCOD.2016.7797741.","short":"A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, R. Ray, in:, IEEE, 2016.","chicago":"Gurung, Amit, Arup Deka, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, and Rajarshi Ray. “Parallel Reachability Analysis for Hybrid Systems.” IEEE, 2016. https://doi.org/10.1109/MEMCOD.2016.7797741."},"oa":1,"main_file_link":[{"url":"https://arxiv.org/abs/1606.05473","open_access":"1"}],"quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"conference":{"end_date":"2016-11-20","location":"Kanpur, India ","start_date":"2016-11-18","name":"MEMOCODE: International Conference on Formal Methods and Models for System Design"},"doi":"10.1109/MEMCOD.2016.7797741","date_published":"2016-12-27T00:00:00Z","language":[{"iso":"eng"}],"scopus_import":1,"month":"12","day":"27"},{"publisher":"ACM","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2016","date_created":"2018-12-11T11:50:20Z","date_updated":"2021-01-12T06:48:33Z","author":[{"last_name":"Avni","first_name":"Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","full_name":"Avni, Guy"},{"full_name":"Guha, Shibashis","last_name":"Guha","first_name":"Shibashis"},{"full_name":"Rodríguez Navas, Guillermo","last_name":"Rodríguez Navas","first_name":"Guillermo"}],"article_number":"26","ec_funded":1,"publist_id":"6223","file_date_updated":"2018-12-12T10:09:31Z","project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"quality_controlled":"1","oa":1,"language":[{"iso":"eng"}],"doi":"10.1145/2968478.2968499","conference":{"name":"EMSOFT: Embedded Software ","start_date":"2016-10-01","location":"Pittsburgh, PA, USA","end_date":"2016-10-07"},"month":"10","status":"public","ddc":["000"],"title":"Synthesizing time triggered schedules for switched networks with faulty links","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1135","oa_version":"Submitted Version","file":[{"access_level":"open_access","file_name":"IST-2016-644-v1+1_emsoft-no-format.pdf","creator":"system","file_size":279240,"content_type":"application/pdf","file_id":"4755","relation":"main_file","date_updated":"2018-12-12T10:09:31Z","date_created":"2018-12-12T10:09:31Z"}],"pubrep_id":"644","type":"conference","abstract":[{"lang":"eng","text":"Time-triggered (TT) switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. These networks rely on the notion of globally discretized time (i.e. time slots) and a static TT schedule that prescribes which message is sent through which link at every time slot, such that all messages reach their destination before a global timeout. These schedules are generated offline, assuming a static network with fault-free links, and entrusting all error-handling functions to the end user. Assuming the network is static is an over-optimistic view, and indeed links tend to fail in practice. We study synthesis of TT schedules on a network in which links fail over time and we assume the switches run a very simple error-recovery protocol once they detect a crashed link. We address the problem of finding a pk; qresistant schedule; namely, one that, assuming the switches run a fixed error-recovery protocol, guarantees that the number of messages that arrive at their destination by the timeout is at least no matter what sequence of at most k links fail. Thus, we maintain the simplicity of the switches while giving a guarantee on the number of messages that meet the timeout. We show how a pk; q-resistant schedule can be obtained using a CEGAR-like approach: find a schedule, decide whether it is pk; q-resistant, and if it is not, use the witnessing fault sequence to generate a constraint that is added to the program. The newly added constraint disallows the schedule to be regenerated in a future iteration while also eliminating several other schedules that are not pk; q-resistant. We illustrate the applicability of our approach using an SMT-based implementation. © 2016 ACM."}],"citation":{"chicago":"Avni, Guy, Shibashis Guha, and Guillermo Rodríguez Navas. “Synthesizing Time Triggered Schedules for Switched Networks with Faulty Links.” In Proceedings of the 13th International Conference on Embedded Software . ACM, 2016. https://doi.org/10.1145/2968478.2968499.","mla":"Avni, Guy, et al. “Synthesizing Time Triggered Schedules for Switched Networks with Faulty Links.” Proceedings of the 13th International Conference on Embedded Software , 26, ACM, 2016, doi:10.1145/2968478.2968499.","short":"G. Avni, S. Guha, G. Rodríguez Navas, in:, Proceedings of the 13th International Conference on Embedded Software , ACM, 2016.","ista":"Avni G, Guha S, Rodríguez Navas G. 2016. Synthesizing time triggered schedules for switched networks with faulty links. Proceedings of the 13th International Conference on Embedded Software . EMSOFT: Embedded Software , 26.","apa":"Avni, G., Guha, S., & Rodríguez Navas, G. (2016). Synthesizing time triggered schedules for switched networks with faulty links. In Proceedings of the 13th International Conference on Embedded Software . Pittsburgh, PA, USA: ACM. https://doi.org/10.1145/2968478.2968499","ieee":"G. Avni, S. Guha, and G. Rodríguez Navas, “Synthesizing time triggered schedules for switched networks with faulty links,” in Proceedings of the 13th International Conference on Embedded Software , Pittsburgh, PA, USA, 2016.","ama":"Avni G, Guha S, Rodríguez Navas G. Synthesizing time triggered schedules for switched networks with faulty links. In: Proceedings of the 13th International Conference on Embedded Software . ACM; 2016. doi:10.1145/2968478.2968499"},"publication":"Proceedings of the 13th International Conference on Embedded Software ","date_published":"2016-10-01T00:00:00Z","scopus_import":1,"has_accepted_license":"1","day":"01"},{"scopus_import":1,"day":"10","month":"10","quality_controlled":"1","citation":{"ama":"Duggirala P, Fan C, Potok M, et al. Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. In: 2016 IEEE Conference on Control Applications. IEEE; 2016. doi:10.1109/CCA.2016.7587948","apa":"Duggirala, P., Fan, C., Potok, M., Qi, B., Mitra, S., Viswanathan, M., … Xiang, W. (2016). Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. In 2016 IEEE Conference on Control Applications. Buenos Aires, Argentina : IEEE. https://doi.org/10.1109/CCA.2016.7587948","ieee":"P. Duggirala et al., “Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP,” in 2016 IEEE Conference on Control Applications, Buenos Aires, Argentina , 2016.","ista":"Duggirala P, Fan C, Potok M, Qi B, Mitra S, Viswanathan M, Bak S, Bogomolov S, Johnson T, Nguyen L, Schilling C, Sogokon A, Tran H, Xiang W. 2016. Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. 2016 IEEE Conference on Control Applications. CCA: Control Applications , 7587948.","short":"P. Duggirala, C. Fan, M. Potok, B. Qi, S. Mitra, M. Viswanathan, S. Bak, S. Bogomolov, T. Johnson, L. Nguyen, C. Schilling, A. Sogokon, H. Tran, W. Xiang, in:, 2016 IEEE Conference on Control Applications, IEEE, 2016.","mla":"Duggirala, Parasara, et al. “Tutorial: Software Tools for Hybrid Systems Verification Transformation and Synthesis C2E2 HyST and TuLiP.” 2016 IEEE Conference on Control Applications, 7587948, IEEE, 2016, doi:10.1109/CCA.2016.7587948.","chicago":"Duggirala, Parasara, Chuchu Fan, Matthew Potok, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, Stanley Bak, et al. “Tutorial: Software Tools for Hybrid Systems Verification Transformation and Synthesis C2E2 HyST and TuLiP.” In 2016 IEEE Conference on Control Applications. IEEE, 2016. https://doi.org/10.1109/CCA.2016.7587948."},"publication":"2016 IEEE Conference on Control Applications","language":[{"iso":"eng"}],"doi":"10.1109/CCA.2016.7587948","date_published":"2016-10-10T00:00:00Z","conference":{"name":"CCA: Control Applications ","end_date":"2016-09-22","start_date":"2016-09-19","location":"Buenos Aires, Argentina "},"type":"conference","article_number":"7587948","publist_id":"6224","abstract":[{"text":"Hybrid systems have both continuous and discrete dynamics and are useful for modeling a variety of control systems, from air traffic control protocols to robotic maneuvers and beyond. Recently, numerous powerful and scalable tools for analyzing hybrid systems have emerged. Several of these tools implement automated formal methods for mathematically proving a system meets a specification. This tutorial session will present three recent hybrid systems tools: C2E2, HyST, and TuLiP. C2E2 is a simulated-based verification tool for hybrid systems, and uses validated numerical solvers and bloating of simulation traces to verify systems meet specifications. HyST is a hybrid systems model transformation and translation tool, and uses a canonical intermediate representation to support most of the recent verification tools, as well as automated sound abstractions that simplify verification of a given hybrid system. TuLiP is a controller synthesis tool for hybrid systems, where given a temporal logic specification to be satisfied for a system (plant) model, TuLiP will find a controller that meets a given specification. © 2016 IEEE.","lang":"eng"}],"publisher":"IEEE","department":[{"_id":"ToHe"}],"publication_status":"published","title":"Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP","status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1134","year":"2016","oa_version":"None","date_updated":"2021-01-12T06:48:32Z","date_created":"2018-12-11T11:50:20Z","author":[{"last_name":"Duggirala","first_name":"Parasara","full_name":"Duggirala, Parasara"},{"first_name":"Chuchu","last_name":"Fan","full_name":"Fan, Chuchu"},{"last_name":"Potok","first_name":"Matthew","full_name":"Potok, Matthew"},{"full_name":"Qi, Bolun","last_name":"Qi","first_name":"Bolun"},{"full_name":"Mitra, Sayan","first_name":"Sayan","last_name":"Mitra"},{"last_name":"Viswanathan","first_name":"Mahesh","full_name":"Viswanathan, Mahesh"},{"full_name":"Bak, Stanley","last_name":"Bak","first_name":"Stanley"},{"full_name":"Bogomolov, Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0686-0365","first_name":"Sergiy","last_name":"Bogomolov"},{"last_name":"Johnson","first_name":"Taylor","full_name":"Johnson, Taylor"},{"last_name":"Nguyen","first_name":"Luan","full_name":"Nguyen, Luan"},{"full_name":"Schilling, Christian","first_name":"Christian","last_name":"Schilling","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065"},{"full_name":"Sogokon, Andrew","last_name":"Sogokon","first_name":"Andrew"},{"last_name":"Tran","first_name":"Hoang","full_name":"Tran, Hoang"},{"full_name":"Xiang, Weiming","first_name":"Weiming","last_name":"Xiang"}]},{"month":"07","language":[{"iso":"eng"}],"conference":{"end_date":"2016-07-08","location":"New York, NY, USA","start_date":"2016-07-05","name":"LICS: Logic in Computer Science"},"doi":"10.1145/2933575.2933588","quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"external_id":{"arxiv":["1604.06764"]},"oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.06764"}],"publist_id":"6220","ec_funded":1,"date_created":"2018-12-11T11:50:21Z","date_updated":"2021-01-12T06:48:34Z","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan"}],"publication_status":"published","publisher":"IEEE","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), FWF Grant No P23499- N23, FWF NFN Grant No S114","year":"2016","day":"05","scopus_import":1,"date_published":"2016-07-05T00:00:00Z","page":"76 - 85","publication":"Proceedings of the 31st Annual ACM/IEEE Symposium","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative Automata under Probabilistic Semantics.” In Proceedings of the 31st Annual ACM/IEEE Symposium, 76–85. IEEE, 2016. https://doi.org/10.1145/2933575.2933588.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Automata under Probabilistic Semantics.” Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85, doi:10.1145/2933575.2933588.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative automata under probabilistic semantics. Proceedings of the 31st Annual ACM/IEEE Symposium. LICS: Logic in Computer Science, 76–85.","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Quantitative automata under probabilistic semantics. In Proceedings of the 31st Annual ACM/IEEE Symposium (pp. 76–85). New York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2933588","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative automata under probabilistic semantics,” in Proceedings of the 31st Annual ACM/IEEE Symposium, New York, NY, USA, 2016, pp. 76–85.","ama":"Chatterjee K, Henzinger TA, Otop J. Quantitative automata under probabilistic semantics. In: Proceedings of the 31st Annual ACM/IEEE Symposium. IEEE; 2016:76-85. doi:10.1145/2933575.2933588"},"abstract":[{"text":"Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative automata under probabilistic semantics. We show that several problems that are undecidable for the classical questions of emptiness and universality become decidable under the probabilistic semantics. We present a complete picture of decidability for such automata, and even an almost-complete picture of computational complexity, for the probabilistic questions we consider. © 2016 ACM.","lang":"eng"}],"type":"conference","oa_version":"Preprint","title":"Quantitative automata under probabilistic semantics","status":"public","_id":"1138","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"has_accepted_license":"1","day":"25","scopus_import":1,"date_published":"2016-09-25T00:00:00Z","page":"128 - 144","citation":{"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.","ieee":"H. Kong et al., “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., & Schilling, C. (2016). Discrete abstraction of multiaffine systems (Vol. 9957, pp. 128–144). Presented at the HSB: Hybrid Systems Biology, Grenoble, France: Springer. https://doi.org/10.1007/978-3-319-47151-8_9","ama":"Kong H, Bartocci E, Bogomolov S, et al. Discrete abstraction of multiaffine systems. In: Vol 9957. Springer; 2016:128-144. doi:10.1007/978-3-319-47151-8_9","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. https://doi.org/10.1007/978-3-319-47151-8_9.","mla":"Kong, Hui, et al. Discrete Abstraction of Multiaffine Systems. Vol. 9957, Springer, 2016, pp. 128–44, doi:10.1007/978-3-319-47151-8_9.","short":"H. Kong, E. Bartocci, S. Bogomolov, R. Grosu, T.A. Henzinger, Y. Jiang, C. Schilling, in:, Springer, 2016, pp. 128–144."},"abstract":[{"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.","lang":"eng"}],"alternative_title":["LNCS"],"type":"conference","file":[{"date_created":"2018-12-12T10:10:49Z","date_updated":"2020-07-14T12:44:39Z","checksum":"994e164b558c47bacf8dc066dd27c8fc","relation":"main_file","file_id":"4840","content_type":"application/pdf","file_size":683955,"creator":"system","file_name":"IST-2017-781-v1+1_main.pdf","access_level":"open_access"}],"oa_version":"Submitted Version","pubrep_id":"781","intvolume":" 9957","ddc":["005"],"title":"Discrete abstraction of multiaffine systems","status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1227","month":"09","language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-47151-8_9","conference":{"name":"HSB: Hybrid Systems Biology","start_date":"2016-10-20","location":"Grenoble, France","end_date":"2016-10-21"},"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"}],"quality_controlled":"1","oa":1,"publist_id":"6107","file_date_updated":"2020-07-14T12:44:39Z","volume":9957,"date_created":"2018-12-11T11:50:49Z","date_updated":"2021-01-12T06:49:13Z","author":[{"full_name":"Kong, Hui","first_name":"Hui","last_name":"Kong","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3066-6941"},{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"full_name":"Bogomolov, Sergiy","last_name":"Bogomolov","first_name":"Sergiy","orcid":"0000-0002-0686-0365","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Grosu","first_name":"Radu","full_name":"Grosu, Radu"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jiang, Yu","last_name":"Jiang","first_name":"Yu"},{"full_name":"Schilling, Christian","first_name":"Christian","last_name":"Schilling","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065"}],"department":[{"_id":"ToHe"}],"publisher":"Springer","publication_status":"published","year":"2016","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)."},{"month":"04","doi":"10.1109/RTAS.2016.7461337","conference":{"name":"RTAS: Real-time and Embedded Technology and Applications Symposium","end_date":"2016-04-14","start_date":"2016-04-11","location":"Vienna, Austria"},"language":[{"iso":"eng"}],"oa":1,"quality_controlled":"1","publist_id":"6069","file_date_updated":"2020-07-14T12:44:41Z","article_number":"7461337","author":[{"first_name":"Yu","last_name":"Jiang","full_name":"Jiang, Yu"},{"first_name":"Yixiao","last_name":"Yang","full_name":"Yang, Yixiao"},{"last_name":"Liu","first_name":"Han","full_name":"Liu, Han"},{"last_name":"Kong","first_name":"Hui","orcid":"0000-0002-3066-6941","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","full_name":"Kong, Hui"},{"first_name":"Ming","last_name":"Gu","full_name":"Gu, Ming"},{"full_name":"Sun, Jiaguang","first_name":"Jiaguang","last_name":"Sun"},{"full_name":"Sha, Lui","last_name":"Sha","first_name":"Lui"}],"date_updated":"2021-01-12T06:49:26Z","date_created":"2018-12-11T11:50:58Z","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.","year":"2016","publisher":"IEEE","department":[{"_id":"ToHe"}],"publication_status":"published","has_accepted_license":"1","day":"27","scopus_import":1,"date_published":"2016-04-27T00:00:00Z","citation":{"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.","ieee":"Y. Jiang et al., “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.","apa":"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. Presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, Vienna, Austria: IEEE. https://doi.org/10.1109/RTAS.2016.7461337","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:10.1109/RTAS.2016.7461337","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. https://doi.org/10.1109/RTAS.2016.7461337.","mla":"Jiang, Yu, et al. From Stateflow Simulation to Verified Implementation: A Verification Approach and a Real-Time Train Controller Design. 7461337, IEEE, 2016, doi:10.1109/RTAS.2016.7461337.","short":"Y. Jiang, Y. Yang, H. Liu, H. Kong, M. Gu, J. Sun, L. Sha, in:, IEEE, 2016."},"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."}],"type":"conference","pubrep_id":"780","file":[{"date_updated":"2020-07-14T12:44:41Z","date_created":"2018-12-12T10:12:31Z","checksum":"42f0462911cc9957f2356b12fb33b4b6","file_id":"4949","relation":"main_file","creator":"system","file_size":1293599,"content_type":"application/pdf","file_name":"IST-2017-780-v1+1_RTAS-42-Camera-Ready.pdf","access_level":"open_access"}],"oa_version":"Submitted Version","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"1256","ddc":["005"],"status":"public","title":"From stateflow simulation to verified implementation: A verification approach and a real-time train controller design"},{"publisher":"Springer","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","year":"2016","volume":9837,"date_updated":"2021-01-12T06:49:58Z","date_created":"2018-12-11T11:51:26Z","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"publist_id":"5932","ec_funded":1,"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"}],"quality_controlled":"1","oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.06764"}],"language":[{"iso":"eng"}],"doi":"10.1007/978-3-662-53413-7_2","conference":{"end_date":"2016-09-10","location":"Edinburgh, United Kingdom","start_date":"2016-09-08","name":"SAS: Static Analysis Symposium"},"month":"08","intvolume":" 9837","status":"public","title":"Quantitative monitor automata","_id":"1335","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","alternative_title":["LNCS"],"type":"conference","abstract":[{"lang":"eng","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."}],"page":"23 - 38","citation":{"ama":"Chatterjee K, Henzinger TA, Otop J. Quantitative monitor automata. In: Vol 9837. Springer; 2016:23-38. doi:10.1007/978-3-662-53413-7_2","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Quantitative monitor automata (Vol. 9837, pp. 23–38). Presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53413-7_2","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.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative monitor automata. SAS: Static Analysis Symposium, LNCS, vol. 9837, 23–38.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Springer, 2016, pp. 23–38.","mla":"Chatterjee, Krishnendu, et al. Quantitative Monitor Automata. Vol. 9837, Springer, 2016, pp. 23–38, doi:10.1007/978-3-662-53413-7_2.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative Monitor Automata,” 9837:23–38. Springer, 2016. https://doi.org/10.1007/978-3-662-53413-7_2."},"date_published":"2016-08-31T00:00:00Z","scopus_import":1,"day":"31"},{"department":[{"_id":"ToHe"}],"intvolume":" 9780","publisher":"Springer","title":"QLOSE: Program repair with quantitative objectives","publication_status":"published","status":"public","year":"2016","_id":"1390","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","volume":9780,"oa_version":"None","date_created":"2018-12-11T11:51:45Z","date_updated":"2021-01-12T06:50:21Z","author":[{"first_name":"Loris","last_name":"D'Antoni","full_name":"D'Antoni, Loris"},{"full_name":"Samanta, Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","first_name":"Roopsha","last_name":"Samanta"},{"first_name":"Rishabh","last_name":"Singh","full_name":"Singh, Rishabh"}],"alternative_title":["LNCS"],"type":"conference","publist_id":"5819","ec_funded":1,"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"}],"page":"383 - 401","project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","citation":{"ama":"D’Antoni L, Samanta R, Singh R. QLOSE: Program repair with quantitative objectives. In: Vol 9780. Springer; 2016:383-401. doi:10.1007/978-3-319-41540-6_21","apa":"D’Antoni, L., Samanta, R., & Singh, R. (2016). QLOSE: Program repair with quantitative objectives (Vol. 9780, pp. 383–401). Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer. https://doi.org/10.1007/978-3-319-41540-6_21","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.","ista":"D’Antoni L, Samanta R, Singh R. 2016. QLOSE: Program repair with quantitative objectives. CAV: Computer Aided Verification, LNCS, vol. 9780, 383–401.","short":"L. D’Antoni, R. Samanta, R. Singh, in:, Springer, 2016, pp. 383–401.","mla":"D’Antoni, Loris, et al. QLOSE: Program Repair with Quantitative Objectives. Vol. 9780, Springer, 2016, pp. 383–401, doi:10.1007/978-3-319-41540-6_21.","chicago":"D’Antoni, Loris, Roopsha Samanta, and Rishabh Singh. “QLOSE: Program Repair with Quantitative Objectives,” 9780:383–401. Springer, 2016. https://doi.org/10.1007/978-3-319-41540-6_21."},"language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-41540-6_21","date_published":"2016-07-13T00:00:00Z","conference":{"start_date":"2016-07-17","location":"Toronto, Canada","end_date":"2016-07-23","name":"CAV: Computer Aided Verification"},"scopus_import":1,"month":"07","day":"13"}]