[{"scopus_import":1,"pubrep_id":"313","month":"09","doi":"10.1007/978-3-319-10936-7_17","file_date_updated":"2020-07-14T12:45:19Z","has_accepted_license":"1","volume":8723,"date_published":"2014-09-01T00:00:00Z","language":[{"iso":"eng"}],"type":"conference","date_updated":"2021-01-12T06:53:46Z","year":"2014","title":"Cost-aware automatic program repair","editor":[{"last_name":"Müller-Olm","first_name":"Markus","full_name":"Müller-Olm, Markus"},{"first_name":"Helmut","last_name":"Seidl","full_name":"Seidl, Helmut"}],"author":[{"full_name":"Samanta, Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","first_name":"Roopsha","last_name":"Samanta"},{"full_name":"Olivo, Oswaldo","last_name":"Olivo","first_name":"Oswaldo"},{"first_name":"Emerson","last_name":"Allen","full_name":"Allen, Emerson"}],"oa_version":"Submitted Version","conference":{"start_date":"2014-09-11","location":"Munich, Germany","end_date":"2014-09-14","name":"SAS: Static Analysis Symposium"},"citation":{"ama":"Samanta R, Olivo O, Allen E. Cost-aware automatic program repair. In: Müller-Olm M, Seidl H, eds. Vol 8723. Springer; 2014:268-284. doi:<a href=\"https://doi.org/10.1007/978-3-319-10936-7_17\">10.1007/978-3-319-10936-7_17</a>","apa":"Samanta, R., Olivo, O., &#38; Allen, E. (2014). Cost-aware automatic program repair. In M. Müller-Olm &#38; H. Seidl (Eds.) (Vol. 8723, pp. 268–284). Presented at the SAS: Static Analysis Symposium, Munich, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-10936-7_17\">https://doi.org/10.1007/978-3-319-10936-7_17</a>","short":"R. Samanta, O. Olivo, E. Allen, in:, M. Müller-Olm, H. Seidl (Eds.), Springer, 2014, pp. 268–284.","chicago":"Samanta, Roopsha, Oswaldo Olivo, and Emerson Allen. “Cost-Aware Automatic Program Repair.” edited by Markus Müller-Olm and Helmut Seidl, 8723:268–84. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-319-10936-7_17\">https://doi.org/10.1007/978-3-319-10936-7_17</a>.","ista":"Samanta R, Olivo O, Allen E. 2014. Cost-aware automatic program repair. SAS: Static Analysis Symposium, LNCS, vol. 8723, 268–284.","ieee":"R. Samanta, O. Olivo, and E. Allen, “Cost-aware automatic program repair,” presented at the SAS: Static Analysis Symposium, Munich, Germany, 2014, vol. 8723, pp. 268–284.","mla":"Samanta, Roopsha, et al. <i>Cost-Aware Automatic Program Repair</i>. Edited by Markus Müller-Olm and Helmut Seidl, vol. 8723, Springer, 2014, pp. 268–84, doi:<a href=\"https://doi.org/10.1007/978-3-319-10936-7_17\">10.1007/978-3-319-10936-7_17</a>."},"abstract":[{"text":"We present a formal framework for repairing infinite-state, imperative, sequential programs, with (possibly recursive) procedures and multiple assertions; the framework can generate repaired programs by modifying the original erroneous program in multiple program locations, and can ensure the readability of the repaired program using user-defined expression templates; the framework also generates a set of inductive assertions that serve as a proof of correctness of the repaired program. As a step toward integrating programmer intent and intuition in automated program repair, we present a cost-aware formulation - given a cost function associated with permissible statement modifications, the goal is to ensure that the total program modification cost does not exceed a given repair budget. As part of our predicate abstractionbased solution framework, we present a sound and complete algorithm for repair of Boolean programs. We have developed a prototype tool based on SMT solving and used it successfully to repair diverse errors in benchmark C programs.","lang":"eng"}],"quality_controlled":"1","ddc":["000","005"],"_id":"1875","department":[{"_id":"ToHe"}],"page":"268 - 284","publisher":"Springer","file":[{"file_id":"4650","relation":"main_file","creator":"system","date_updated":"2020-07-14T12:45:19Z","content_type":"application/pdf","access_level":"open_access","checksum":"78ec4ea1bdecc676cd3e8cad35c6182c","file_size":409485,"date_created":"2018-12-12T10:07:51Z","file_name":"IST-2014-313-v1+1_SOE.SAS14.pdf"}],"oa":1,"alternative_title":["LNCS"],"status":"public","publist_id":"5221","publication_status":"published","intvolume":"      8723","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","date_created":"2018-12-11T11:54:29Z","day":"01"},{"ddc":["000"],"_id":"5411","month":"01","doi":"10.15479/AT:IST-2014-148-v2-1","pubrep_id":"152","date_published":"2014-01-28T00:00:00Z","file":[{"date_updated":"2020-07-14T12:46:46Z","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"5543","creator":"system","checksum":"0e03aba625cc334141a3148432aa5760","date_created":"2018-12-12T11:54:21Z","file_size":534732,"file_name":"IST-2014-148-v2+1_main_tr.pdf"}],"oa":1,"publisher":"IST Austria","has_accepted_license":"1","file_date_updated":"2020-07-14T12:46:46Z","page":"20","department":[{"_id":"ToHe"}],"alternative_title":["IST Austria Technical Report"],"language":[{"iso":"eng"}],"status":"public","date_updated":"2025-09-29T11:40:47Z","publication_identifier":{"issn":["2664-1690"]},"type":"technical_report","related_material":{"record":[{"id":"2167","status":"public","relation":"later_version"}]},"title":"Compositional specifications for IOCO testing","publication_status":"published","year":"2014","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","author":[{"last_name":"Daca","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724"},{"last_name":"Krenn","first_name":"Willibald","full_name":"Krenn, Willibald"},{"first_name":"Dejan","last_name":"Nickovic","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"}],"date_created":"2018-12-12T11:39:11Z","day":"28","abstract":[{"text":"Model-based testing is a promising technology for black-box software and hardware testing, in which test cases are generated automatically from high-level specifications. Nowadays, systems typically consist of multiple interacting components and, due to their complexity, testing presents a considerable portion of the effort and cost in the design process. Exploiting the compositional structure of system specifications can considerably reduce the effort in model-based testing. Moreover, inferring properties about the system from testing its individual components allows the designer to reduce the amount of integration testing.\r\nIn this paper, we study compositional properties of the IOCO-testing theory. We propose a new approach to composition and hiding operations, inspired by contract-based design and interface theories. These operations preserve behaviors that are compatible under composition and hiding, and prune away incompatible ones. The resulting specification characterizes the input sequences for which the unit testing of components is sufficient to infer the correctness of component integration without the need for further tests. We provide a methodology that uses these results to minimize integration testing effort, but also to detect potential weaknesses in specifications. While we focus on asynchronous models and the IOCO conformance relation, the resulting methodology can be applied to a broader class of systems.","lang":"eng"}],"citation":{"apa":"Daca, P., Henzinger, T. A., Krenn, W., &#38; Nickovic, D. (2014). <i>Compositional specifications for IOCO testing</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-148-v2-1\">https://doi.org/10.15479/AT:IST-2014-148-v2-1</a>","ama":"Daca P, Henzinger TA, Krenn W, Nickovic D. <i>Compositional Specifications for IOCO Testing</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-148-v2-1\">10.15479/AT:IST-2014-148-v2-1</a>","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Willibald Krenn, and Dejan Nickovic. <i>Compositional Specifications for IOCO Testing</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-148-v2-1\">https://doi.org/10.15479/AT:IST-2014-148-v2-1</a>.","ista":"Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications for IOCO testing, IST Austria, 20p.","ieee":"P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, <i>Compositional specifications for IOCO testing</i>. IST Austria, 2014.","mla":"Daca, Przemyslaw, et al. <i>Compositional Specifications for IOCO Testing</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-148-v2-1\">10.15479/AT:IST-2014-148-v2-1</a>.","short":"P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, Compositional Specifications for IOCO Testing, IST Austria, 2014."}},{"pubrep_id":"171","_id":"5416","month":"02","doi":"10.15479/AT:IST-2014-171-v1-1","ddc":["005"],"alternative_title":["IST Austria Technical Report"],"language":[{"iso":"eng"}],"status":"public","oa":1,"file":[{"relation":"main_file","file_id":"5492","creator":"system","date_updated":"2020-07-14T12:46:49Z","content_type":"application/pdf","access_level":"open_access","checksum":"445456d22371e4e49aad2b9a0c13bf80","file_size":712077,"date_created":"2018-12-12T11:53:32Z","file_name":"IST-2014-171-v1+1_report.pdf"}],"date_published":"2014-02-19T00:00:00Z","page":"22","department":[{"_id":"ToHe"}],"has_accepted_license":"1","publisher":"IST Austria","file_date_updated":"2020-07-14T12:46:49Z","title":"Model measuring for hybrid systems","related_material":{"record":[{"id":"2217","status":"public","relation":"later_version"}]},"year":"2014","publication_status":"published","date_updated":"2025-06-26T08:32:32Z","type":"technical_report","publication_identifier":{"issn":["2664-1690"]},"day":"19","date_created":"2018-12-12T11:39:12Z","citation":{"short":"T.A. Henzinger, J. Otop, Model Measuring for Hybrid Systems, IST Austria, 2014.","ieee":"T. A. Henzinger and J. Otop, <i>Model measuring for hybrid systems</i>. IST Austria, 2014.","mla":"Henzinger, Thomas A., and Jan Otop. <i>Model Measuring for Hybrid Systems</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-171-v1-1\">10.15479/AT:IST-2014-171-v1-1</a>.","ista":"Henzinger TA, Otop J. 2014. Model measuring for hybrid systems, IST Austria, 22p.","chicago":"Henzinger, Thomas A, and Jan Otop. <i>Model Measuring for Hybrid Systems</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-171-v1-1\">https://doi.org/10.15479/AT:IST-2014-171-v1-1</a>.","ama":"Henzinger TA, Otop J. <i>Model Measuring for Hybrid Systems</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-171-v1-1\">10.15479/AT:IST-2014-171-v1-1</a>","apa":"Henzinger, T. A., &#38; Otop, J. (2014). <i>Model measuring for hybrid systems</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-171-v1-1\">https://doi.org/10.15479/AT:IST-2014-171-v1-1</a>"},"abstract":[{"text":"As hybrid systems involve continuous behaviors, they should be evaluated by quantitative methods, rather than qualitative methods. In this paper we adapt a quantitative framework, called model measuring, to the hybrid systems domain. The model-measuring problem asks, given a model M and a specification, what is the maximal distance such that all models within that distance from M satisfy (or violate) the specification. A distance function on models is given as part of the input of the problem. Distances, especially related to continuous behaviors are more natural in the hybrid case than the discrete case. We are interested in distances represented by monotonic hybrid automata, a hybrid counterpart of (discrete) weighted automata, whose recognized timed languages are monotone (w.r.t. inclusion) in the values of parameters.The contributions of this paper are twofold. First, we give sufficient conditions under which the model-measuring problem can be solved. Second, we discuss the modeling of distances and applications of the model-measuring problem.","lang":"eng"}],"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan"}]},{"publisher":"IST Austria","file_date_updated":"2020-07-14T12:46:49Z","has_accepted_license":"1","department":[{"_id":"ToHe"}],"page":"14","date_published":"2014-02-19T00:00:00Z","file":[{"file_name":"IST-2014-172-v1+1_report.pdf","checksum":"fcc3eab903cfcd3778b338d2d0d44d18","file_size":383052,"date_created":"2018-12-12T11:53:20Z","file_id":"5481","relation":"main_file","creator":"system","access_level":"open_access","content_type":"application/pdf","date_updated":"2020-07-14T12:46:49Z"}],"oa":1,"status":"public","language":[{"iso":"eng"}],"alternative_title":["IST Austria Technical Report"],"ddc":["000"],"_id":"5417","month":"02","pubrep_id":"175","doi":"10.15479/AT:IST-2014-172-v1-1","author":[{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Otop","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"We define the model-measuring problem: given a model M and specification φ, what is the maximal distance ρ such that all models M'within distance ρ from M satisfy (or violate)φ. The model measuring problem presupposes a distance function on models. We concentrate on automatic distance functions, which are defined by weighted automata.\r\nThe 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, and robustness problems that measure how much a model can be perturbed without violating the specification.\r\nWe show that for automatic distance functions, and ω-regular linear-time and branching-time specifications, the model-measuring problem can be solved.\r\nWe use automata-theoretic model-checking methods for model measuring, replacing the emptiness question for standard word and tree automata by the optimal-weight question for the weighted versions of these automata. We consider weighted automata that accumulate weights by maximizing, summing, discounting, and limit averaging. \r\nWe give several examples of using the model-measuring problem to compute various notions of robustness and quantitative satisfaction for temporal specifications."}],"citation":{"mla":"Henzinger, Thomas A., and Jan Otop. <i>From Model Checking to Model Measuring</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-172-v1-1\">10.15479/AT:IST-2014-172-v1-1</a>.","ieee":"T. A. Henzinger and J. Otop, <i>From model checking to model measuring</i>. IST Austria, 2014.","chicago":"Henzinger, Thomas A, and Jan Otop. <i>From Model Checking to Model Measuring</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-172-v1-1\">https://doi.org/10.15479/AT:IST-2014-172-v1-1</a>.","ista":"Henzinger TA, Otop J. 2014. From model checking to model measuring, IST Austria, 14p.","short":"T.A. Henzinger, J. Otop, From Model Checking to Model Measuring, IST Austria, 2014.","apa":"Henzinger, T. A., &#38; Otop, J. (2014). <i>From model checking to model measuring</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-172-v1-1\">https://doi.org/10.15479/AT:IST-2014-172-v1-1</a>","ama":"Henzinger TA, Otop J. <i>From Model Checking to Model Measuring</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-172-v1-1\">10.15479/AT:IST-2014-172-v1-1</a>"},"date_created":"2018-12-12T11:39:13Z","day":"19","publication_identifier":{"issn":["2664-1690"]},"type":"technical_report","date_updated":"2024-10-21T06:02:58Z","publication_status":"published","year":"2014","related_material":{"record":[{"relation":"later_version","status":"public","id":"2327"}]},"title":"From model checking to model measuring"},{"day":"05","date_created":"2018-12-12T11:39:16Z","abstract":[{"lang":"eng","text":"Simulation is an attractive alternative for language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. For non-deterministic automata, while language inclusion is PSPACE-complete, simulation can be computed in polynomial time. 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. Again, 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 for mean-payoff automata and the decidability is open for discounted-sum automata, whereas the (quantitative) simulation reduce to mean-payoff games and discounted-sum 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. For example, whereas for mean-payoff and discounted-sum games, the players do not need memory to play optimally; we show in contrast that for simulation games with Büchi acceptance conditions, (i) for mean-payoff objectives, optimal strategies for both players require infinite memory in general, and (ii) for discounted-sum objectives, optimal strategies need not exist for both players. While the simulation games with Büchi acceptance conditions are more complicated (e.g., due to infinite-memory requirements for mean-payoff objectives) as compared to their counterpart without Büchi acceptance conditions, we still present pseudo-polynomial time algorithms to solve simulation games with Büchi acceptance conditions for both weighted mean-payoff and weighted discounted-sum automata."}],"citation":{"ama":"Chatterjee K, Henzinger TA, Otop J, Velner Y. <i>Quantitative Fair Simulation Games</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-315-v1-1\">10.15479/AT:IST-2014-315-v1-1</a>","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., &#38; Velner, Y. (2014). <i>Quantitative fair simulation games</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-315-v1-1\">https://doi.org/10.15479/AT:IST-2014-315-v1-1</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Quantitative Fair Simulation Games, IST Austria, 2014.","ista":"Chatterjee K, Henzinger TA, Otop J, Velner Y. 2014. Quantitative fair simulation games, IST Austria, 26p.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner. <i>Quantitative Fair Simulation Games</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-315-v1-1\">https://doi.org/10.15479/AT:IST-2014-315-v1-1</a>.","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, <i>Quantitative fair simulation games</i>. IST Austria, 2014.","mla":"Chatterjee, Krishnendu, et al. <i>Quantitative Fair Simulation Games</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-315-v1-1\">10.15479/AT:IST-2014-315-v1-1</a>."},"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Jan","last_name":"Otop","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Velner","first_name":"Yaron","full_name":"Velner, Yaron"}],"related_material":{"record":[{"relation":"later_version","status":"public","id":"1066"}]},"title":"Quantitative fair simulation games","publication_status":"published","year":"2014","date_updated":"2026-06-18T08:47:00Z","publication_identifier":{"issn":["2664-1690"]},"type":"technical_report","alternative_title":["IST Austria Technical Report"],"status":"public","language":[{"iso":"eng"}],"date_published":"2014-12-05T00:00:00Z","file":[{"date_updated":"2020-07-14T12:46:52Z","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"5521","creator":"system","checksum":"b1d573bc04365625ff9974880c0aa807","file_size":531046,"date_created":"2018-12-12T11:53:59Z","file_name":"IST-2014-315-v1+1_report.pdf"}],"oa":1,"has_accepted_license":"1","file_date_updated":"2020-07-14T12:46:52Z","publisher":"IST Austria","page":"26","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"doi":"10.15479/AT:IST-2014-315-v1-1","_id":"5428","month":"12","pubrep_id":"315","ddc":["004"]},{"intvolume":"      8837","publication_status":"published","publist_id":"5045","day":"01","date_created":"2018-12-11T11:55:17Z","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","acknowledgement":"Sponsor: P202/12/G061; GACR; Czech Science Foundation\r\n\r\n","_id":"2026","quality_controlled":"1","status":"public","alternative_title":["LNCS"],"publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","page":"235 - 241","department":[{"_id":"ToHe"}],"publisher":"Springer","title":"Rabinizer 3: Safraless translation of ltl to small deterministic automata","year":"2014","date_updated":"2024-10-21T06:02:50Z","type":"conference","citation":{"short":"Z. Komárková, J. Kretinsky, in:, F. Cassez, J.-F. Raskin (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer, 2014, pp. 235–241.","chicago":"Komárková, Zuzana, and Jan Kretinsky. “Rabinizer 3: Safraless Translation of Ltl to Small Deterministic Automata.” In <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, edited by Franck Cassez and Jean-François Raskin, 8837:235–41. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-319-11936-6_17\">https://doi.org/10.1007/978-3-319-11936-6_17</a>.","ista":"Komárková Z, Kretinsky J. 2014. Rabinizer 3: Safraless translation of ltl to small deterministic automata. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 8837, 235–241.","mla":"Komárková, Zuzana, and Jan Kretinsky. “Rabinizer 3: Safraless Translation of Ltl to Small Deterministic Automata.” <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, edited by Franck Cassez and Jean-François Raskin, vol. 8837, Springer, 2014, pp. 235–41, doi:<a href=\"https://doi.org/10.1007/978-3-319-11936-6_17\">10.1007/978-3-319-11936-6_17</a>.","ieee":"Z. Komárková and J. Kretinsky, “Rabinizer 3: Safraless translation of ltl to small deterministic automata,” in <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Sydney, Australia, 2014, vol. 8837, pp. 235–241.","ama":"Komárková Z, Kretinsky J. Rabinizer 3: Safraless translation of ltl to small deterministic automata. In: Cassez F, Raskin J-F, eds. <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol 8837. Springer; 2014:235-241. doi:<a href=\"https://doi.org/10.1007/978-3-319-11936-6_17\">10.1007/978-3-319-11936-6_17</a>","apa":"Komárková, Z., &#38; Kretinsky, J. (2014). Rabinizer 3: Safraless translation of ltl to small deterministic automata. In F. Cassez &#38; J.-F. Raskin (Eds.), <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol. 8837, pp. 235–241). Sydney, Australia: Springer. <a href=\"https://doi.org/10.1007/978-3-319-11936-6_17\">https://doi.org/10.1007/978-3-319-11936-6_17</a>"},"abstract":[{"lang":"eng","text":"We present a tool for translating LTL formulae into deterministic ω-automata. It is the first tool that covers the whole LTL that does not use Safra’s determinization or any of its variants. This leads to smaller automata. There are several outputs of the tool: firstly, deterministic Rabin automata, which are the standard input for probabilistic model checking, e.g. for the probabilistic model-checker PRISM; secondly, deterministic generalized Rabin automata, which can also be used for probabilistic model checking and are sometimes by orders of magnitude smaller. We also link our tool to PRISM and show that this leads to a significant speed-up of probabilistic LTL model checking, especially with the generalized Rabin automata."}],"conference":{"name":"ATVA: Automated Technology for Verification and Analysis","end_date":"2014-11-07","start_date":"2014-11-03","location":"Sydney, Australia"},"oa_version":"None","editor":[{"full_name":"Cassez, Franck","first_name":"Franck","last_name":"Cassez"},{"full_name":"Raskin, Jean-François","first_name":"Jean-François","last_name":"Raskin"}],"author":[{"full_name":"Komárková, Zuzana","first_name":"Zuzana","last_name":"Komárková"},{"last_name":"Kretinsky","first_name":"Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan"}],"doi":"10.1007/978-3-319-11936-6_17","month":"01","scopus_import":"1","language":[{"iso":"eng"}],"ec_funded":1,"date_published":"2014-01-01T00:00:00Z","volume":8837,"project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"}]},{"year":"2014","title":"Probabilistic bisimulation: Naturally on distributions","arxiv":1,"type":"conference","date_updated":"2025-06-11T07:57:15Z","abstract":[{"text":"In contrast to the usual understanding of probabilistic systems as stochastic processes, recently these systems have also been regarded as transformers of probabilities. In this paper, we give a natural definition of strong bisimulation for probabilistic systems corresponding to this view that treats probability distributions as first-class citizens. Our definition applies in the same way to discrete systems as well as to systems with uncountable state and action spaces. Several examples demonstrate that our definition refines the understanding of behavioural equivalences of probabilistic systems. In particular, it solves a longstanding open problem concerning the representation of memoryless continuous time by memoryfull continuous time. Finally, we give algorithms for computing this bisimulation not only for finite but also for classes of uncountably infinite systems.","lang":"eng"}],"citation":{"apa":"Hermanns, H., Krčál, J., &#38; Kretinsky, J. (2014). Probabilistic bisimulation: Naturally on distributions. In P. Baldan &#38; D. Gorla (Eds.), <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol. 8704, pp. 249–265). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/978-3-662-44584-6_18\">https://doi.org/10.1007/978-3-662-44584-6_18</a>","ama":"Hermanns H, Krčál J, Kretinsky J. Probabilistic bisimulation: Naturally on distributions. In: Baldan P, Gorla D, eds. <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:249-265. doi:<a href=\"https://doi.org/10.1007/978-3-662-44584-6_18\">10.1007/978-3-662-44584-6_18</a>","chicago":"Hermanns, Holger, Jan Krčál, and Jan Kretinsky. “Probabilistic Bisimulation: Naturally on Distributions.” In <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, edited by Paolo Baldan and Daniele Gorla, 8704:249–65. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. <a href=\"https://doi.org/10.1007/978-3-662-44584-6_18\">https://doi.org/10.1007/978-3-662-44584-6_18</a>.","ista":"Hermanns H, Krčál J, Kretinsky J. 2014. Probabilistic bisimulation: Naturally on distributions. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory, LNCS, vol. 8704, 249–265.","ieee":"H. Hermanns, J. Krčál, and J. Kretinsky, “Probabilistic bisimulation: Naturally on distributions,” in <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Rome, Italy, 2014, vol. 8704, pp. 249–265.","mla":"Hermanns, Holger, et al. “Probabilistic Bisimulation: Naturally on Distributions.” <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, edited by Paolo Baldan and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 249–65, doi:<a href=\"https://doi.org/10.1007/978-3-662-44584-6_18\">10.1007/978-3-662-44584-6_18</a>.","short":"H. Hermanns, J. Krčál, J. Kretinsky, in:, P. Baldan, D. Gorla (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 249–265."},"author":[{"full_name":"Hermanns, Holger","first_name":"Holger","last_name":"Hermanns"},{"last_name":"Krčál","first_name":"Jan","full_name":"Krčál, Jan"},{"full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","first_name":"Jan","last_name":"Kretinsky"}],"editor":[{"last_name":"Baldan","first_name":"Paolo","full_name":"Baldan, Paolo"},{"full_name":"Gorla, Daniele","first_name":"Daniele","last_name":"Gorla"}],"conference":{"end_date":"2014-09-05","start_date":"2014-09-02","location":"Rome, Italy","name":"CONCUR: Concurrency Theory"},"oa_version":"Submitted Version","month":"09","doi":"10.1007/978-3-662-44584-6_18","scopus_import":"1","language":[{"iso":"eng"}],"project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"}],"date_published":"2014-09-01T00:00:00Z","volume":8704,"ec_funded":1,"publication_status":"published","intvolume":"      8704","publist_id":"4993","day":"01","date_created":"2018-12-11T11:55:27Z","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1404.5084"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","_id":"2053","acknowledgement":"This work is supported by the EU 7th Framework Programme under grant agreements 295261 (MEALS) and 318490 (SENSATION), Czech Science Foundation under grant agreement P202/12/G061, the DFG Transregional Collaborative Research Centre SFB/TR 14 AVACS, and by the CAS/SAFEA International Partnership Program for Creative Research Teams.","external_id":{"arxiv":["1404.5084"]},"publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","alternative_title":["LNCS"],"status":"public","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"page":"249 - 265","oa":1},{"scopus_import":"1","month":"11","doi":"10.1007/s00285-013-0738-7","volume":69,"date_published":"2014-11-20T00:00:00Z","language":[{"iso":"eng"}],"type":"journal_article","arxiv":1,"date_updated":"2025-09-29T11:50:22Z","year":"2014","title":"Markov chain aggregation and its applications to combinatorial reaction networks","author":[{"full_name":"Ganguly, Arnab","last_name":"Ganguly","first_name":"Arnab"},{"id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","full_name":"Petrov, Tatjana","last_name":"Petrov","first_name":"Tatjana","orcid":"0000-0002-9041-0905"},{"full_name":"Koeppl, Heinz","first_name":"Heinz","last_name":"Koeppl"}],"oa_version":"Submitted Version","citation":{"ama":"Ganguly A, Petrov T, Koeppl H. Markov chain aggregation and its applications to combinatorial reaction networks. <i>Journal of Mathematical Biology</i>. 2014;69(3):767-797. doi:<a href=\"https://doi.org/10.1007/s00285-013-0738-7\">10.1007/s00285-013-0738-7</a>","apa":"Ganguly, A., Petrov, T., &#38; Koeppl, H. (2014). Markov chain aggregation and its applications to combinatorial reaction networks. <i>Journal of Mathematical Biology</i>. Springer. <a href=\"https://doi.org/10.1007/s00285-013-0738-7\">https://doi.org/10.1007/s00285-013-0738-7</a>","short":"A. Ganguly, T. Petrov, H. Koeppl, Journal of Mathematical Biology 69 (2014) 767–797.","mla":"Ganguly, Arnab, et al. “Markov Chain Aggregation and Its Applications to Combinatorial Reaction Networks.” <i>Journal of Mathematical Biology</i>, vol. 69, no. 3, Springer, 2014, pp. 767–97, doi:<a href=\"https://doi.org/10.1007/s00285-013-0738-7\">10.1007/s00285-013-0738-7</a>.","ieee":"A. Ganguly, T. Petrov, and H. Koeppl, “Markov chain aggregation and its applications to combinatorial reaction networks,” <i>Journal of Mathematical Biology</i>, vol. 69, no. 3. Springer, pp. 767–797, 2014.","ista":"Ganguly A, Petrov T, Koeppl H. 2014. Markov chain aggregation and its applications to combinatorial reaction networks. Journal of Mathematical Biology. 69(3), 767–797.","chicago":"Ganguly, Arnab, Tatjana Petrov, and Heinz Koeppl. “Markov Chain Aggregation and Its Applications to Combinatorial Reaction Networks.” <i>Journal of Mathematical Biology</i>. Springer, 2014. <a href=\"https://doi.org/10.1007/s00285-013-0738-7\">https://doi.org/10.1007/s00285-013-0738-7</a>."},"abstract":[{"text":"We consider a continuous-time Markov chain (CTMC) whose state space is partitioned into aggregates, and each aggregate is assigned a probability measure. A sufficient condition for defining a CTMC over the aggregates is presented as a variant of weak lumpability, which also characterizes that the measure over the original process can be recovered from that of the aggregated one. We show how the applicability of de-aggregation depends on the initial distribution. The application section is devoted to illustrate how the developed theory aids in reducing CTMC models of biochemical systems particularly in connection to protein-protein interactions. We assume that the model is written by a biologist in form of site-graph-rewrite rules. Site-graph-rewrite rules compactly express that, often, only a local context of a protein (instead of a full molecular species) needs to be in a certain configuration in order to trigger a reaction event. This observation leads to suitable aggregate Markov chains with smaller state spaces, thereby providing sufficient reduction in computational complexity. This is further exemplified in two case studies: simple unbounded polymerization and early EGFR/insulin crosstalk.","lang":"eng"}],"external_id":{"arxiv":["1303.4532"],"isi":["000340588700008"]},"quality_controlled":"1","isi":1,"article_processing_charge":"No","_id":"2056","acknowledgement":"T. Petrov is supported by SystemsX.ch—the Swiss Inititative for Systems Biology.","page":"767 - 797","department":[{"_id":"CaGu"},{"_id":"ToHe"}],"publisher":"Springer","oa":1,"status":"public","publication":"Journal of Mathematical Biology","publist_id":"4990","publication_status":"published","intvolume":"        69","main_file_link":[{"url":"http://arxiv.org/abs/1303.4532","open_access":"1"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","issue":"3","date_created":"2018-12-11T11:55:28Z","day":"20"},{"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"}],"corr_author":"1","date_published":"2014-07-01T00:00:00Z","volume":8559,"ec_funded":1,"language":[{"iso":"eng"}],"scopus_import":"1","doi":"10.1007/978-3-319-08867-9_31","month":"07","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Martin","last_name":"Chmelik","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw","last_name":"Daca","first_name":"Przemyslaw"}],"conference":{"end_date":"2014-07-22","start_date":"2014-07-18","location":"Vienna, Austria","name":"CAV: Computer Aided Verification"},"oa_version":"None","abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems.We focus on qualitative properties forMDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation ofMDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.We present an automated technique for assume-guarantee style reasoning for compositional analysis ofMDPs with qualitative properties by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements."}],"citation":{"short":"K. Chatterjee, M. Chmelik, P. Daca, in:, Springer, 2014, pp. 473–490.","mla":"Chatterjee, Krishnendu, et al. <i>CEGAR for Qualitative Analysis of Probabilistic Systems</i>. Vol. 8559, Springer, 2014, pp. 473–90, doi:<a href=\"https://doi.org/10.1007/978-3-319-08867-9_31\">10.1007/978-3-319-08867-9_31</a>.","ieee":"K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for qualitative analysis of probabilistic systems,” presented at the CAV: Computer Aided Verification, Vienna, Austria, 2014, vol. 8559, pp. 473–490.","ista":"Chatterjee K, Chmelik M, Daca P. 2014. CEGAR for qualitative analysis of probabilistic systems. CAV: Computer Aided Verification, LNCS, vol. 8559, 473–490.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Qualitative Analysis of Probabilistic Systems,” 8559:473–90. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-319-08867-9_31\">https://doi.org/10.1007/978-3-319-08867-9_31</a>.","ama":"Chatterjee K, Chmelik M, Daca P. CEGAR for qualitative analysis of probabilistic systems. In: Vol 8559. Springer; 2014:473-490. doi:<a href=\"https://doi.org/10.1007/978-3-319-08867-9_31\">10.1007/978-3-319-08867-9_31</a>","apa":"Chatterjee, K., Chmelik, M., &#38; Daca, P. (2014). CEGAR for qualitative analysis of probabilistic systems (Vol. 8559, pp. 473–490). Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer. <a href=\"https://doi.org/10.1007/978-3-319-08867-9_31\">https://doi.org/10.1007/978-3-319-08867-9_31</a>"},"type":"conference","date_updated":"2026-04-15T10:02:12Z","year":"2014","related_material":{"record":[{"id":"5412","relation":"earlier_version","status":"public"},{"status":"public","relation":"earlier_version","id":"5413"},{"id":"5414","relation":"earlier_version","status":"public"},{"id":"1155","status":"public","relation":"dissertation_contains"}]},"title":"CEGAR for qualitative analysis of probabilistic systems","publisher":"Springer","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"473 - 490","status":"public","alternative_title":["LNCS"],"quality_controlled":"1","_id":"2063","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","date_created":"2018-12-11T11:55:30Z","publist_id":"4978","publication_status":"published","intvolume":"      8559"},{"page":"348 - 363","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"Elsevier","oa":1,"status":"public","publication":"Theoretical Computer Science","external_id":{"arxiv":["1210.2450"],"isi":["000347601300009"]},"quality_controlled":"1","isi":1,"_id":"1733","article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1210.2450"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","issue":"3","day":"04","date_created":"2018-12-11T11:53:43Z","publist_id":"5392","publication_status":"published","intvolume":"       560","corr_author":"1","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"ec_funded":1,"date_published":"2014-12-04T00:00:00Z","volume":560,"language":[{"iso":"eng"}],"scopus_import":"1","doi":"10.1016/j.tcs.2014.08.019","month":"12","author":[{"first_name":"Pavol","last_name":"Cerny","full_name":"Cerny, Pavol"},{"last_name":"Chmelik","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Arjun","last_name":"Radhakrishna","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"Submitted Version","citation":{"short":"P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 560 (2014) 348–363.","ista":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. 2014. Interface simulation distances. Theoretical Computer Science. 560(3), 348–363.","chicago":"Cerny, Pavol, Martin Chmelik, Thomas A Henzinger, and Arjun Radhakrishna. “Interface Simulation Distances.” <i>Theoretical Computer Science</i>. Elsevier, 2014. <a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">https://doi.org/10.1016/j.tcs.2014.08.019</a>.","ieee":"P. Cerny, M. Chmelik, T. A. Henzinger, and A. Radhakrishna, “Interface simulation distances,” <i>Theoretical Computer Science</i>, vol. 560, no. 3. Elsevier, pp. 348–363, 2014.","mla":"Cerny, Pavol, et al. “Interface Simulation Distances.” <i>Theoretical Computer Science</i>, vol. 560, no. 3, Elsevier, 2014, pp. 348–63, doi:<a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">10.1016/j.tcs.2014.08.019</a>.","ama":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. Interface simulation distances. <i>Theoretical Computer Science</i>. 2014;560(3):348-363. doi:<a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">10.1016/j.tcs.2014.08.019</a>","apa":"Cerny, P., Chmelik, M., Henzinger, T. A., &#38; Radhakrishna, A. (2014). Interface simulation distances. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">https://doi.org/10.1016/j.tcs.2014.08.019</a>"},"abstract":[{"text":"The classical (boolean) notion of refinement for behavioral interfaces of system components is the alternating refinement preorder. In this paper, we define a distance for interfaces, called interface simulation distance. It makes the alternating refinement preorder quantitative by, intuitively, tolerating errors (while counting them) in the alternating simulation game. We show that the interface simulation distance satisfies the triangle inequality, that the distance between two interfaces does not increase under parallel composition with a third interface, that the distance between two interfaces can be bounded from above and below by distances between abstractions of the two interfaces, and how to synthesize an interface from incompatible requirements. We illustrate the framework, and the properties of the distances under composition of interfaces, with two case studies.","lang":"eng"}],"type":"journal_article","arxiv":1,"date_updated":"2025-09-29T13:14:25Z","year":"2014","title":"Interface simulation distances","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"2916"}]}},{"language":[{"iso":"eng"}],"project":[{"call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"}],"has_accepted_license":"1","file_date_updated":"2020-07-14T12:45:34Z","volume":10,"date_published":"2014-02-13T00:00:00Z","ec_funded":1,"doi":"10.2168/LMCS-10(1:10)2014","month":"02","pubrep_id":"389","scopus_import":"1","abstract":[{"text":" A discounted-sum automaton (NDA) is a nondeterministic finite automaton with edge weights, valuing a run by the discounted sum of visited edge weights. More precisely, the weight in the i-th position of the run is divided by λi, where the discount factor λ is a fixed rational number greater than 1. The value of a word is the minimal value of the automaton runs on it. Discounted summation is a common and useful measuring scheme, especially for infinite sequences, reflecting the assumption that earlier weights are more important than later weights. Unfortunately, determinization of NDAs, which is often essential in formal verification, is, in general, not possible. We provide positive news, showing that every NDA with an integral discount factor is determinizable. We complete the picture by proving that the integers characterize exactly the discount factors that guarantee determinizability: for every nonintegral rational discount factor λ, there is a nondeterminizable λ-NDA. We also prove that the class of NDAs with integral discount factors enjoys closure under the algebraic operations min, max, addition, and subtraction, which is not the case for general NDAs nor for deterministic NDAs. For general NDAs, we look into approximate determinization, which is always possible as the influence of a word's suffix decays. We show that the naive approach, of unfolding the automaton computations up to a sufficient level, is doubly exponential in the discount factor. We provide an alternative construction for approximate determinization, which is singly exponential in the discount factor, in the precision, and in the number of states. We also prove matching lower bounds, showing that the exponential dependency on each of these three parameters cannot be avoided. All our results hold equally for automata over finite words and for automata over infinite words. ","lang":"eng"}],"citation":{"ama":"Boker U, Henzinger TA. Exact and approximate determinization of discounted-sum automata. <i>Logical Methods in Computer Science</i>. 2014;10(1). doi:<a href=\"https://doi.org/10.2168/LMCS-10(1:10)2014\">10.2168/LMCS-10(1:10)2014</a>","apa":"Boker, U., &#38; Henzinger, T. A. (2014). Exact and approximate determinization of discounted-sum automata. <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic. <a href=\"https://doi.org/10.2168/LMCS-10(1:10)2014\">https://doi.org/10.2168/LMCS-10(1:10)2014</a>","short":"U. Boker, T.A. Henzinger, Logical Methods in Computer Science 10 (2014).","mla":"Boker, Udi, and Thomas A. Henzinger. “Exact and Approximate Determinization of Discounted-Sum Automata.” <i>Logical Methods in Computer Science</i>, vol. 10, no. 1, International Federation for Computational Logic, 2014, doi:<a href=\"https://doi.org/10.2168/LMCS-10(1:10)2014\">10.2168/LMCS-10(1:10)2014</a>.","ieee":"U. Boker and T. A. Henzinger, “Exact and approximate determinization of discounted-sum automata,” <i>Logical Methods in Computer Science</i>, vol. 10, no. 1. International Federation for Computational Logic, 2014.","chicago":"Boker, Udi, and Thomas A Henzinger. “Exact and Approximate Determinization of Discounted-Sum Automata.” <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic, 2014. <a href=\"https://doi.org/10.2168/LMCS-10(1:10)2014\">https://doi.org/10.2168/LMCS-10(1:10)2014</a>.","ista":"Boker U, Henzinger TA. 2014. Exact and approximate determinization of discounted-sum automata. Logical Methods in Computer Science. 10(1)."},"author":[{"full_name":"Boker, Udi","first_name":"Udi","last_name":"Boker"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"}],"oa_version":"Published Version","year":"2014","title":"Exact and approximate determinization of discounted-sum automata","publication_identifier":{"issn":["1860-5974"]},"type":"journal_article","date_updated":"2026-07-06T13:22:33Z","publication":"Logical Methods in Computer Science","status":"public","publisher":"International Federation for Computational Logic","department":[{"_id":"ToHe"}],"file":[{"access_level":"open_access","date_updated":"2020-07-14T12:45:34Z","content_type":"application/pdf","relation":"main_file","file_id":"4643","creator":"system","file_name":"IST-2015-389-v1+1_1401.3957.pdf","checksum":"9f6ea2e2d8d4a32ff0becc29d835bbf8","date_created":"2018-12-12T10:07:45Z","file_size":550936}],"oa":1,"_id":"2233","article_processing_charge":"No","isi":1,"das_tickbox":"1","ddc":["000"],"external_id":{"isi":["000333744700015"]},"quality_controlled":"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"},"issue":"1","date_created":"2018-12-11T11:56:28Z","day":"13","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","intvolume":"        10","publist_id":"4728"},{"publication_status":"published","intvolume":"      8837","publist_id":"5046","day":"01","date_created":"2018-12-11T11:55:17Z","main_file_link":[{"url":"http://arxiv.org/abs/1402.2967","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"2027","article_processing_charge":"No","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 246967 (VERIWARE), by the EU FP7 project HIERATIC, by the Czech Science Foundation grant No P202/12/P612, by EPSRC project EP/K038575/1.","das_tickbox":"1","external_id":{"arxiv":["1402.2967"]},"quality_controlled":"1","alternative_title":["LNCS"],"status":"public","publication":"12th International Symposium on Automated Technology for Verification and Analysis","page":"98 - 114","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"Springer","oa":1,"year":"2014","title":"Verification of Markov decision processes using learning algorithms","type":"conference","arxiv":1,"date_updated":"2026-07-07T13:15:34Z","citation":{"mla":"Brázdil, Tomáš, et al. “Verification of Markov Decision Processes Using Learning Algorithms.” <i>12th International Symposium on Automated Technology for Verification and Analysis</i>, vol. 8837, Springer, 2014, pp. 98–114, doi:<a href=\"https://doi.org/10.1007/978-3-319-11936-6_8\">10.1007/978-3-319-11936-6_8</a>.","ieee":"T. Brázdil <i>et al.</i>, “Verification of Markov decision processes using learning algorithms,” in <i>12th International Symposium on Automated Technology for Verification and Analysis</i>, Sydney, Australia, 2014, vol. 8837, pp. 98–114.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt, Jan Kretinsky, Marta Kwiatkowska, David Parker, and Mateusz Ujma. “Verification of Markov Decision Processes Using Learning Algorithms.” In <i>12th International Symposium on Automated Technology for Verification and Analysis</i>, 8837:98–114. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-319-11936-6_8\">https://doi.org/10.1007/978-3-319-11936-6_8</a>.","ista":"Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M, Parker D, Ujma M. 2014. Verification of Markov decision processes using learning algorithms. 12th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 8837, 98–114.","short":"T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska, D. Parker, M. Ujma, in:, 12th International Symposium on Automated Technology for Verification and Analysis, Springer, 2014, pp. 98–114.","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska, M., … Ujma, M. (2014). Verification of Markov decision processes using learning algorithms. In <i>12th International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 8837, pp. 98–114). Sydney, Australia: Springer. <a href=\"https://doi.org/10.1007/978-3-319-11936-6_8\">https://doi.org/10.1007/978-3-319-11936-6_8</a>","ama":"Brázdil T, Chatterjee K, Chmelik M, et al. Verification of Markov decision processes using learning algorithms. In: <i>12th International Symposium on Automated Technology for Verification and Analysis</i>. Vol 8837. Springer; 2014:98-114. doi:<a href=\"https://doi.org/10.1007/978-3-319-11936-6_8\">10.1007/978-3-319-11936-6_8</a>"},"abstract":[{"lang":"eng","text":"We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model checking for unbounded properties inMDPs. In contrast with other related techniques, our approach is not restricted to time-bounded (finite-horizon) or discounted properties, nor does it assume any particular properties of the MDP. We also show how our methods extend to LTL objectives. We present experimental results showing the performance of our framework on several examples."}],"author":[{"last_name":"Brázdil","first_name":"Tomáš","full_name":"Brázdil, Tomáš"},{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin","last_name":"Chmelik","first_name":"Martin"},{"first_name":"Vojtěch","last_name":"Forejt","full_name":"Forejt, Vojtěch"},{"last_name":"Kretinsky","orcid":"0000-0002-8122-2881","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan"},{"full_name":"Kwiatkowska, Marta","first_name":"Marta","last_name":"Kwiatkowska"},{"full_name":"Parker, David","first_name":"David","last_name":"Parker"},{"last_name":"Ujma","first_name":"Mateusz","full_name":"Ujma, Mateusz"}],"conference":{"name":"ATVA: Automated Technology for Verification and Analysis","location":"Sydney, Australia","start_date":"2014-11-03","end_date":"2014-11-07"},"oa_version":"Submitted Version","month":"11","doi":"10.1007/978-3-319-11936-6_8","scopus_import":"1","language":[{"iso":"eng"}],"project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"_id":"26241A12-B435-11E9-9278-68D0E5697425","grant_number":"24696","name":"Light-regulated ligand traps for spatio-temporal inhibition of cell signaling"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"ec_funded":1,"volume":8837,"date_published":"2014-11-01T00:00:00Z"},{"publication_identifier":{"issn":["2664-1690"]},"type":"technical_report","date_updated":"2026-07-07T14:01:10Z","publication_status":"published","year":"2014","related_material":{"record":[{"relation":"later_version","status":"public","id":"5436"},{"status":"public","relation":"later_version","id":"1656"},{"relation":"later_version","status":"public","id":"467"}]},"title":"Nested weighted automata","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"last_name":"Otop","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"}],"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"Recently there has been a significant effort to add quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, several basic system properties such as average response time cannot be expressed with weighted automata. In this work, we introduce nested weighted automata as a new formalism for expressing important quantitative properties such as average response time. We establish an almost complete decidability picture for the basic decision problems for nested weighted automata, and illustrate its applicability in several domains.  "}],"citation":{"apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2014). <i>Nested weighted automata</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-170-v1-1\">https://doi.org/10.15479/AT:IST-2014-170-v1-1</a>","ama":"Chatterjee K, Henzinger TA, Otop J. <i>Nested Weighted Automata</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-170-v1-1\">10.15479/AT:IST-2014-170-v1-1</a>","ista":"Chatterjee K, Henzinger TA, Otop J. 2014. Nested weighted automata, IST Austria, 27p.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. <i>Nested Weighted Automata</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-170-v1-1\">https://doi.org/10.15479/AT:IST-2014-170-v1-1</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, <i>Nested weighted automata</i>. IST Austria, 2014.","mla":"Chatterjee, Krishnendu, et al. <i>Nested Weighted Automata</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-170-v1-1\">10.15479/AT:IST-2014-170-v1-1</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2014."},"date_created":"2018-12-12T11:39:12Z","day":"19","ddc":["004"],"_id":"5415","month":"02","doi":"10.15479/AT:IST-2014-170-v1-1","pubrep_id":"170","has_accepted_license":"1","publisher":"IST Austria","file_date_updated":"2020-07-14T12:46:48Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"27","date_published":"2014-02-19T00:00:00Z","oa":1,"file":[{"access_level":"open_access","content_type":"application/pdf","date_updated":"2020-07-14T12:46:48Z","creator":"system","relation":"main_file","file_id":"5497","file_name":"IST-2014-170-v1+1_main.pdf","file_size":573457,"date_created":"2018-12-12T11:53:36Z","checksum":"31f90dcf2cf899c3f8c6427cfcc2b3c7"}],"alternative_title":["IST Austria Technical Report"],"language":[{"iso":"eng"}],"status":"public"},{"publist_id":"5013","publication_status":"published","intvolume":"        15","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","issue":"4","date_created":"2018-12-11T11:55:21Z","day":"16","das_tickbox":"1","ddc":["000","004"],"external_id":{"isi":["000345570700002"]},"quality_controlled":"1","article_processing_charge":"No","_id":"2038","isi":1,"acknowledgement":"The research was supported in part by ERC Starting grant 278410 (QUALITY).","publisher":"ACM","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"oa":1,"file":[{"checksum":"354c41d37500b56320afce94cf9a99c2","file_size":346184,"date_created":"2018-12-12T10:10:59Z","file_name":"IST-2014-192-v1+1_AccumulativeValues.pdf","date_updated":"2020-07-14T12:45:26Z","content_type":"application/pdf","access_level":"open_access","file_id":"4851","relation":"main_file","creator":"system"}],"publication":"ACM Transactions on Computational Logic","status":"public","type":"journal_article","date_updated":"2026-07-07T14:01:43Z","year":"2014","related_material":{"record":[{"id":"5385","status":"public","relation":"earlier_version"},{"id":"3356","relation":"earlier_version","status":"public"}]},"title":"Temporal specifications with accumulative values","author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","full_name":"Boker, Udi","last_name":"Boker","first_name":"Udi"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"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":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"oa_version":"Submitted Version","abstract":[{"lang":"eng","text":"Recently, there has been an effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions. At the heart of quantitative objectives lies the accumulation of values along a computation. It is often the accumulated sum, as with energy objectives, or the accumulated average, as with mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric (or Boolean) variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point in time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire infinite computation. We study the border of decidability for such quantitative extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities with both prefix-accumulation assertions, or extending LTL with both path-accumulation assertions, results in temporal logics whose model-checking problem is decidable. Moreover, the prefix-accumulation assertions may be generalized with &quot;controlled accumulation,&quot; allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that this branching-time logic is, in a sense, the maximal logic with one or both of the prefix-accumulation assertions that permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, such as CTL or LTL, makes the problem undecidable."}],"article_number":"27","citation":{"ama":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. Temporal specifications with accumulative values. <i>ACM Transactions on Computational Logic</i>. 2014;15(4). doi:<a href=\"https://doi.org/10.1145/2629686\">10.1145/2629686</a>","apa":"Boker, U., Chatterjee, K., Henzinger, T. A., &#38; Kupferman, O. (2014). Temporal specifications with accumulative values. <i>ACM Transactions on Computational Logic</i>. ACM. <a href=\"https://doi.org/10.1145/2629686\">https://doi.org/10.1145/2629686</a>","short":"U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, ACM Transactions on Computational Logic 15 (2014).","chicago":"Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman. “Temporal Specifications with Accumulative Values.” <i>ACM Transactions on Computational Logic</i>. ACM, 2014. <a href=\"https://doi.org/10.1145/2629686\">https://doi.org/10.1145/2629686</a>.","ista":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2014. Temporal specifications with accumulative values. ACM Transactions on Computational Logic. 15(4), 27.","mla":"Boker, Udi, et al. “Temporal Specifications with Accumulative Values.” <i>ACM Transactions on Computational Logic</i>, vol. 15, no. 4, 27, ACM, 2014, doi:<a href=\"https://doi.org/10.1145/2629686\">10.1145/2629686</a>.","ieee":"U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, “Temporal specifications with accumulative values,” <i>ACM Transactions on Computational Logic</i>, vol. 15, no. 4. ACM, 2014."},"scopus_import":"1","doi":"10.1145/2629686","month":"09","pubrep_id":"192","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"file_date_updated":"2020-07-14T12:45:26Z","has_accepted_license":"1","volume":15,"date_published":"2014-09-16T00:00:00Z","ec_funded":1,"article_type":"original","language":[{"iso":"eng"}]},{"_id":"1872","article_processing_charge":"No","acknowledgement":"This research was supported in part by the Austrian National Research Network RiSE (S11410-N23).","das_tickbox":"1","quality_controlled":"1","ddc":["000"],"alternative_title":["LNCS"],"status":"public","publication":"12th International Symposium on Automated Technology for Verification and Analysis","department":[{"_id":"ToHe"}],"page":"185 - 200","publisher":"Springer","file":[{"checksum":"af4bd3fc1f4c93075e4dc5cbf625fe7b","file_size":244294,"date_created":"2018-12-12T10:10:15Z","file_name":"IST-2016-641-v1+1_atva2014.pdf","date_updated":"2020-07-14T12:45:19Z","content_type":"application/pdf","access_level":"open_access","file_id":"4801","relation":"main_file","creator":"system"}],"oa":1,"publication_status":"published","intvolume":"      8837","publist_id":"5226","date_created":"2018-12-11T11:54:28Z","day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","pubrep_id":"641","doi":"10.1007/978-3-319-11936-6_14","month":"01","scopus_import":"1","language":[{"iso":"eng"}],"has_accepted_license":"1","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"}],"file_date_updated":"2020-07-14T12:45:19Z","ec_funded":1,"volume":8837,"date_published":"2014-01-01T00:00:00Z","year":"2014","title":"Extensional crisis and proving identity","type":"conference","date_updated":"2026-07-08T06:49:33Z","citation":{"ama":"Gupta A, Kovács L, Kragl B, Voronkov A. Extensional crisis and proving identity. In: <i>12th International Symposium on Automated Technology for Verification and Analysis</i>. Vol 8837. Springer; 2014:185-200. doi:<a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">10.1007/978-3-319-11936-6_14</a>","apa":"Gupta, A., Kovács, L., Kragl, B., &#38; Voronkov, A. (2014). Extensional crisis and proving identity. In <i>12th International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 8837, pp. 185–200). Sydney, Australia: Springer. <a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">https://doi.org/10.1007/978-3-319-11936-6_14</a>","short":"A. Gupta, L. Kovács, B. Kragl, A. Voronkov, in:, 12th International Symposium on Automated Technology for Verification and Analysis, Springer, 2014, pp. 185–200.","chicago":"Gupta, Ashutosh, Laura Kovács, Bernhard Kragl, and Andrei Voronkov. “Extensional Crisis and Proving Identity.” In <i>12th International Symposium on Automated Technology for Verification and Analysis</i>, 8837:185–200. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">https://doi.org/10.1007/978-3-319-11936-6_14</a>.","ista":"Gupta A, Kovács L, Kragl B, Voronkov A. 2014. Extensional crisis and proving identity. 12th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 8837, 185–200.","ieee":"A. Gupta, L. Kovács, B. Kragl, and A. Voronkov, “Extensional crisis and proving identity,” in <i>12th International Symposium on Automated Technology for Verification and Analysis</i>, Sydney, Australia, 2014, vol. 8837, pp. 185–200.","mla":"Gupta, Ashutosh, et al. “Extensional Crisis and Proving Identity.” <i>12th International Symposium on Automated Technology for Verification and Analysis</i>, vol. 8837, Springer, 2014, pp. 185–200, doi:<a href=\"https://doi.org/10.1007/978-3-319-11936-6_14\">10.1007/978-3-319-11936-6_14</a>."},"abstract":[{"text":"Extensionality axioms are common when reasoning about data collections, such as arrays and functions in program analysis, or sets in mathematics. An extensionality axiom asserts that two collections are equal if they consist of the same elements at the same indices. Using extensionality is often required to show that two collections are equal. A typical example is the set theory theorem (∀x)(∀y)x∪y = y ∪x. Interestingly, while humans have no problem with proving such set identities using extensionality, they are very hard for superposition theorem provers because of the calculi they use. In this paper we show how addition of a new inference rule, called extensionality resolution, allows first-order theorem provers to easily solve problems no modern first-order theorem prover can solve. We illustrate this by running the VAMPIRE theorem prover with extensionality resolution on a number of set theory and array problems. Extensionality resolution helps VAMPIRE to solve problems from the TPTP library of first-order problems that were never solved before by any prover.","lang":"eng"}],"author":[{"full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh","last_name":"Gupta"},{"full_name":"Kovács, Laura","first_name":"Laura","last_name":"Kovács"},{"full_name":"Kragl, Bernhard","id":"320FC952-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7745-9117","first_name":"Bernhard","last_name":"Kragl"},{"last_name":"Voronkov","first_name":"Andrei","full_name":"Voronkov, Andrei"}],"oa_version":"Submitted Version","conference":{"end_date":"2014-11-07","location":"Sydney, Australia","start_date":"2014-11-03","name":"ATVA: Automated Technology for Verification and Analysis"}},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"14","date_created":"2022-03-21T07:33:22Z","issue":"5","publication_status":"published","publisher":"ACM","department":[{"_id":"ToHe"}],"publication":"Proceedings of the ACM International Conference on Computing Frontiers - CF '13","status":"public","quality_controlled":"1","acknowledgement":"This work has been supported by the European Research Council advanced grant on Quantitative Reactive Modeling (QUAREM) and the National Research Network RiSE on Rigorous Systems Engineering (Austrian Science Fund S11402-N23 and S11404-N23).","_id":"10898","article_processing_charge":"No","conference":{"start_date":"2013-05-14","location":"Ischia, Italy","end_date":"2013-05-16","name":"CF: Conference on Computing Frontiers"},"oa_version":"None","author":[{"full_name":"Haas, Andreas","first_name":"Andreas","last_name":"Haas"},{"first_name":"Michael","last_name":"Lippautz","full_name":"Lippautz, Michael"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger"},{"full_name":"Payer, Hannes","first_name":"Hannes","last_name":"Payer"},{"first_name":"Ana","last_name":"Sokolova","full_name":"Sokolova, Ana"},{"last_name":"Kirsch","first_name":"Christoph M.","full_name":"Kirsch, Christoph M."},{"last_name":"Sezgin","first_name":"Ali","id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","full_name":"Sezgin, Ali"}],"abstract":[{"text":"A prominent remedy to multicore scalability issues in concurrent data structure implementations is to relax the sequential specification of the data structure. We present distributed queues (DQ), a new family of relaxed concurrent queue implementations. DQs implement relaxed queues with linearizable emptiness check and either configurable or bounded out-of-order behavior or pool behavior. Our experiments show that DQs outperform and outscale in micro- and macrobenchmarks all strict and relaxed queue as well as pool implementations that we considered.","lang":"eng"}],"article_number":"17","citation":{"apa":"Haas, A., Lippautz, M., Henzinger, T. A., Payer, H., Sokolova, A., Kirsch, C. M., &#38; Sezgin, A. (2013). Distributed queues in shared memory: Multicore performance and scalability through quantitative relaxation. In <i>Proceedings of the ACM International Conference on Computing Frontiers - CF ’13</i>. Ischia, Italy: ACM. <a href=\"https://doi.org/10.1145/2482767.2482789\">https://doi.org/10.1145/2482767.2482789</a>","ama":"Haas A, Lippautz M, Henzinger TA, et al. Distributed queues in shared memory: Multicore performance and scalability through quantitative relaxation. In: <i>Proceedings of the ACM International Conference on Computing Frontiers - CF ’13</i>. ACM; 2013. doi:<a href=\"https://doi.org/10.1145/2482767.2482789\">10.1145/2482767.2482789</a>","chicago":"Haas, Andreas, Michael Lippautz, Thomas A Henzinger, Hannes Payer, Ana Sokolova, Christoph M. Kirsch, and Ali Sezgin. “Distributed Queues in Shared Memory: Multicore Performance and Scalability through Quantitative Relaxation.” In <i>Proceedings of the ACM International Conference on Computing Frontiers - CF ’13</i>. ACM, 2013. <a href=\"https://doi.org/10.1145/2482767.2482789\">https://doi.org/10.1145/2482767.2482789</a>.","ista":"Haas A, Lippautz M, Henzinger TA, Payer H, Sokolova A, Kirsch CM, Sezgin A. 2013. Distributed queues in shared memory: Multicore performance and scalability through quantitative relaxation. Proceedings of the ACM International Conference on Computing Frontiers - CF ’13. CF: Conference on Computing Frontiers, 17.","mla":"Haas, Andreas, et al. “Distributed Queues in Shared Memory: Multicore Performance and Scalability through Quantitative Relaxation.” <i>Proceedings of the ACM International Conference on Computing Frontiers - CF ’13</i>, no. 5, 17, ACM, 2013, doi:<a href=\"https://doi.org/10.1145/2482767.2482789\">10.1145/2482767.2482789</a>.","ieee":"A. Haas <i>et al.</i>, “Distributed queues in shared memory: Multicore performance and scalability through quantitative relaxation,” in <i>Proceedings of the ACM International Conference on Computing Frontiers - CF ’13</i>, Ischia, Italy, 2013, no. 5.","short":"A. Haas, M. Lippautz, T.A. Henzinger, H. Payer, A. Sokolova, C.M. Kirsch, A. Sezgin, in:, Proceedings of the ACM International Conference on Computing Frontiers - CF ’13, ACM, 2013."},"date_updated":"2025-05-14T11:23:58Z","publication_identifier":{"isbn":["978-145032053-5"]},"type":"conference","title":"Distributed queues in shared memory: Multicore performance and scalability through quantitative relaxation","year":"2013","date_published":"2013-05-14T00:00:00Z","ec_funded":1,"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"}],"language":[{"iso":"eng"}],"scopus_import":"1","month":"05","doi":"10.1145/2482767.2482789"},{"month":"09","doi":"10.4230/LIPIcs.CSL.2013.563","pubrep_id":"136","scopus_import":1,"language":[{"iso":"eng"}],"ec_funded":1,"date_published":"2013-09-01T00:00:00Z","volume":23,"project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7"}],"file_date_updated":"2020-07-14T12:45:34Z","has_accepted_license":"1","title":"Elementary modal logics over transitive structures","year":"2013","date_updated":"2020-08-11T10:09:42Z","type":"conference","citation":{"ama":"Michaliszyn J, Otop J. Elementary modal logics over transitive structures. 2013;23:563-577. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CSL.2013.563\">10.4230/LIPIcs.CSL.2013.563</a>","apa":"Michaliszyn, J., &#38; Otop, J. (2013). Elementary modal logics over transitive structures. Presented at the CSL: Computer Science Logic, Torino, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CSL.2013.563\">https://doi.org/10.4230/LIPIcs.CSL.2013.563</a>","short":"J. Michaliszyn, J. Otop, 23 (2013) 563–577.","ieee":"J. Michaliszyn and J. Otop, “Elementary modal logics over transitive structures,” vol. 23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 563–577, 2013.","mla":"Michaliszyn, Jakub, and Jan Otop. <i>Elementary Modal Logics over Transitive Structures</i>. Vol. 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 563–77, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CSL.2013.563\">10.4230/LIPIcs.CSL.2013.563</a>.","chicago":"Michaliszyn, Jakub, and Jan Otop. “Elementary Modal Logics over Transitive Structures.” Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. <a href=\"https://doi.org/10.4230/LIPIcs.CSL.2013.563\">https://doi.org/10.4230/LIPIcs.CSL.2013.563</a>.","ista":"Michaliszyn J, Otop J. 2013. Elementary modal logics over transitive structures. 23, 563–577."},"abstract":[{"lang":"eng","text":"We show that modal logic over universally first-order definable classes of transitive frames is decidable. More precisely, let K be an arbitrary class of transitive Kripke frames definable by a universal first-order sentence. We show that the global and finite global satisfiability problems of modal logic over K are decidable in NP, regardless of choice of K. We also show that the local satisfiability and the finite local satisfiability problems of modal logic over K are decidable in NEXPTIME."}],"conference":{"name":"CSL: Computer Science Logic","location":"Torino, Italy","start_date":"2013-09-02","end_date":"2013-09-05"},"oa_version":"Published Version","author":[{"first_name":"Jakub","last_name":"Michaliszyn","full_name":"Michaliszyn, Jakub"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan"}],"_id":"2243","quality_controlled":"1","ddc":["000","004"],"status":"public","alternative_title":["LIPIcs"],"file":[{"checksum":"e0732e73a8b1e39483df7717d53e3e35","file_size":454915,"date_created":"2018-12-12T10:12:11Z","file_name":"IST-2016-136-v1+2_39.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:45:34Z","access_level":"open_access","relation":"main_file","file_id":"4929","creator":"system"}],"oa":1,"department":[{"_id":"ToHe"}],"page":"563 - 577","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","series_title":"Leibniz International Proceedings in Informatics","intvolume":"        23","publication_status":"published","publist_id":"4708","day":"01","date_created":"2018-12-11T11:56:32Z","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"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"_id":"2288","doi":"10.1007/978-3-642-40708-6","month":"07","quality_controlled":"1","language":[{"iso":"eng"}],"status":"public","alternative_title":["LNCS"],"volume":8130,"date_published":"2013-07-01T00:00:00Z","corr_author":"1","department":[{"_id":"ToHe"}],"publisher":"Springer","title":"Computational Methods in Systems Biology","intvolume":"      8130","year":"2013","publication_status":"published","publist_id":"4643","date_updated":"2024-10-09T20:55:17Z","type":"conference_editor","publication_identifier":{"isbn":["978-3-642-40707-9"]},"day":"01","date_created":"2018-12-11T11:56:47Z","citation":{"apa":"Gupta, A., &#38; Henzinger, T. A. (Eds.). (2013). <i>Computational Methods in Systems Biology</i> (Vol. 8130). Presented at the CMSB: Computational Methods in Systems Biology, Klosterneuburg, Austria: Springer. <a href=\"https://doi.org/10.1007/978-3-642-40708-6\">https://doi.org/10.1007/978-3-642-40708-6</a>","ama":"Gupta A, Henzinger TA, eds. <i>Computational Methods in Systems Biology</i>. Vol 8130. Springer; 2013. doi:<a href=\"https://doi.org/10.1007/978-3-642-40708-6\">10.1007/978-3-642-40708-6</a>","ista":"Gupta A, Henzinger TA eds. 2013. Computational Methods in Systems Biology, Springer,p.","chicago":"Gupta, Ashutosh, and Thomas A Henzinger, eds. <i>Computational Methods in Systems Biology</i>. Vol. 8130. Springer, 2013. <a href=\"https://doi.org/10.1007/978-3-642-40708-6\">https://doi.org/10.1007/978-3-642-40708-6</a>.","mla":"Gupta, Ashutosh, and Thomas A. Henzinger, editors. <i>Computational Methods in Systems Biology</i>. Vol. 8130, Springer, 2013, doi:<a href=\"https://doi.org/10.1007/978-3-642-40708-6\">10.1007/978-3-642-40708-6</a>.","ieee":"A. Gupta and T. A. Henzinger, Eds., <i>Computational Methods in Systems Biology</i>, vol. 8130. Springer, 2013.","short":"A. Gupta, T.A. Henzinger, eds., Computational Methods in Systems Biology, Springer, 2013."},"abstract":[{"text":"This book constitutes the proceedings of the 11th International Conference on Computational Methods in Systems Biology, CMSB 2013, held in Klosterneuburg, Austria, in September 2013. The 15 regular papers included in this volume were carefully reviewed and selected from 27 submissions. They deal with computational models for all levels, from molecular and cellular, to organs and entire organisms.","lang":"eng"}],"oa_version":"None","conference":{"start_date":"2013-09-22","location":"Klosterneuburg, Austria","end_date":"2013-09-24","name":"CMSB: Computational Methods in Systems Biology"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","editor":[{"first_name":"Ashutosh","last_name":"Gupta","full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"}]},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","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"},"issue":"4","day":"05","date_created":"2018-12-11T11:56:47Z","publist_id":"4642","publication_status":"published","intvolume":"        28","publisher":"Springer","department":[{"_id":"ToHe"}],"page":"331 - 344","file":[{"file_name":"IST-2016-626-v1+1_s00450-013-0251-7.pdf","date_created":"2018-12-12T10:17:51Z","file_size":570361,"checksum":"f117a00f9f046165bfa95595681e08a0","access_level":"open_access","date_updated":"2020-07-14T12:45:37Z","content_type":"application/pdf","creator":"system","file_id":"5308","relation":"main_file"}],"oa":1,"publication":"Computer Science Research and Development","status":"public","ddc":["000"],"quality_controlled":"1","_id":"2289","author":[{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"oa_version":"Published Version","abstract":[{"text":"Formal verification aims to improve the quality of software by detecting errors before they do harm. At the basis of formal verification is the logical notion of correctness, which purports to capture whether or not a program behaves as desired. We suggest that the boolean partition of software into correct and incorrect programs falls short of the practical need to assess the behavior of software in a more nuanced fashion against multiple criteria. We therefore propose to introduce quantitative fitness measures for programs, specifically for measuring the function, performance, and robustness of reactive programs such as concurrent processes. This article describes the goals of the ERC Advanced Investigator Project QUAREM. The project aims to build and evaluate a theory of quantitative fitness measures for reactive models. Such a theory must strive to obtain quantitative generalizations of the paradigms that have been success stories in qualitative reactive modeling, such as compositionality, property-preserving abstraction and abstraction refinement, model checking, and synthesis. The theory will be evaluated not only in the context of software and hardware engineering, but also in the context of systems biology. In particular, we will use the quantitative reactive models and fitness measures developed in this project for testing hypotheses about the mechanisms behind data from biological experiments.","lang":"eng"}],"citation":{"chicago":"Henzinger, Thomas A. “Quantitative Reactive Modeling and Verification.” <i>Computer Science Research and Development</i>. Springer, 2013. <a href=\"https://doi.org/10.1007/s00450-013-0251-7\">https://doi.org/10.1007/s00450-013-0251-7</a>.","ista":"Henzinger TA. 2013. Quantitative reactive modeling and verification. Computer Science Research and Development. 28(4), 331–344.","ieee":"T. A. Henzinger, “Quantitative reactive modeling and verification,” <i>Computer Science Research and Development</i>, vol. 28, no. 4. Springer, pp. 331–344, 2013.","mla":"Henzinger, Thomas A. “Quantitative Reactive Modeling and Verification.” <i>Computer Science Research and Development</i>, vol. 28, no. 4, Springer, 2013, pp. 331–44, doi:<a href=\"https://doi.org/10.1007/s00450-013-0251-7\">10.1007/s00450-013-0251-7</a>.","short":"T.A. Henzinger, Computer Science Research and Development 28 (2013) 331–344.","apa":"Henzinger, T. A. (2013). Quantitative reactive modeling and verification. <i>Computer Science Research and Development</i>. Springer. <a href=\"https://doi.org/10.1007/s00450-013-0251-7\">https://doi.org/10.1007/s00450-013-0251-7</a>","ama":"Henzinger TA. Quantitative reactive modeling and verification. <i>Computer Science Research and Development</i>. 2013;28(4):331-344. doi:<a href=\"https://doi.org/10.1007/s00450-013-0251-7\">10.1007/s00450-013-0251-7</a>"},"type":"journal_article","date_updated":"2024-10-09T20:55:17Z","year":"2013","title":"Quantitative reactive modeling and verification","file_date_updated":"2020-07-14T12:45:37Z","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"}],"has_accepted_license":"1","corr_author":"1","date_published":"2013-10-05T00:00:00Z","volume":28,"ec_funded":1,"language":[{"iso":"eng"}],"scopus_import":1,"month":"10","pubrep_id":"626","doi":"10.1007/s00450-013-0251-7"},{"abstract":[{"lang":"eng","text":"We present a shape analysis for programs that manipulate overlaid data structures which share sets of objects. The abstract domain contains Separation Logic formulas that (1) combine a per-object separating conjunction with a per-field separating conjunction and (2) constrain a set of variables interpreted as sets of objects. The definition of the abstract domain operators is based on a notion of homomorphism between formulas, viewed as graphs, used recently to define optimal decision procedures for fragments of the Separation Logic. Based on a Frame Rule that supports the two versions of the separating conjunction, the analysis is able to reason in a modular manner about non-overlaid data structures and then, compose information only at a few program points, e.g., procedure returns. We have implemented this analysis in a prototype tool and applied it on several interesting case studies that manipulate overlaid and nested linked lists.\r\n"}],"citation":{"short":"C. Dragoi, C. Enea, M. Sighireanu, in:, Springer, 2013, pp. 150–171.","ista":"Dragoi C, Enea C, Sighireanu M. 2013. Local shape analysis for overlaid data structures. SAS: Static Analysis Symposium, LNCS, vol. 7935, 150–171.","chicago":"Dragoi, Cezara, Constantin Enea, and Mihaela Sighireanu. “Local Shape Analysis for Overlaid Data Structures,” 7935:150–71. Springer, 2013. <a href=\"https://doi.org/10.1007/978-3-642-38856-9_10\">https://doi.org/10.1007/978-3-642-38856-9_10</a>.","mla":"Dragoi, Cezara, et al. <i>Local Shape Analysis for Overlaid Data Structures</i>. Vol. 7935, Springer, 2013, pp. 150–71, doi:<a href=\"https://doi.org/10.1007/978-3-642-38856-9_10\">10.1007/978-3-642-38856-9_10</a>.","ieee":"C. Dragoi, C. Enea, and M. Sighireanu, “Local shape analysis for overlaid data structures,” presented at the SAS: Static Analysis Symposium, Seattle, WA, United States, 2013, vol. 7935, pp. 150–171.","ama":"Dragoi C, Enea C, Sighireanu M. Local shape analysis for overlaid data structures. In: Vol 7935. Springer; 2013:150-171. doi:<a href=\"https://doi.org/10.1007/978-3-642-38856-9_10\">10.1007/978-3-642-38856-9_10</a>","apa":"Dragoi, C., Enea, C., &#38; Sighireanu, M. (2013). Local shape analysis for overlaid data structures (Vol. 7935, pp. 150–171). Presented at the SAS: Static Analysis Symposium, Seattle, WA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-642-38856-9_10\">https://doi.org/10.1007/978-3-642-38856-9_10</a>"},"author":[{"first_name":"Cezara","last_name":"Dragoi","full_name":"Dragoi, Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Constantin","last_name":"Enea","full_name":"Enea, Constantin"},{"full_name":"Sighireanu, Mihaela","last_name":"Sighireanu","first_name":"Mihaela"}],"oa_version":"Submitted Version","conference":{"name":"SAS: Static Analysis Symposium","end_date":"2013-06-22","start_date":"2013-06-20","location":"Seattle, WA, United States"},"year":"2013","title":"Local shape analysis for overlaid data structures","type":"conference","date_updated":"2021-01-12T06:56:36Z","language":[{"iso":"eng"}],"has_accepted_license":"1","file_date_updated":"2020-07-14T12:45:37Z","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"}],"volume":7935,"date_published":"2013-01-01T00:00:00Z","ec_funded":1,"doi":"10.1007/978-3-642-38856-9_10","month":"01","pubrep_id":"196","scopus_import":1,"day":"01","date_created":"2018-12-11T11:56:50Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","intvolume":"      7935","publist_id":"4630","alternative_title":["LNCS"],"status":"public","publisher":"Springer","page":"150 - 171","department":[{"_id":"ToHe"}],"oa":1,"file":[{"creator":"system","relation":"main_file","file_id":"4824","access_level":"open_access","date_updated":"2020-07-14T12:45:37Z","content_type":"application/pdf","file_name":"IST-2014-196-v1+1_sas13.pdf","date_created":"2018-12-12T10:10:36Z","file_size":299004,"checksum":"907edd33a5892e3af093365f1fd57ed7"}],"_id":"2298","ddc":["000","004"],"quality_controlled":"1"}]