[{"author":[{"id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","first_name":"Pavol","last_name":"Cerny","full_name":"Cerny, Pavol"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","full_name":"Radhakrishna, Arjun","first_name":"Arjun","last_name":"Radhakrishna"}],"issue":"1","_id":"3249","scopus_import":1,"title":"Simulation distances","pubrep_id":"42","intvolume":"       413","publication_status":"published","date_created":"2018-12-11T12:02:15Z","department":[{"_id":"ToHe"}],"page":"21 - 35","ec_funded":1,"quality_controlled":"1","publisher":"Elsevier","date_updated":"2023-02-23T12:24:04Z","year":"2012","citation":{"ama":"Cerny P, Henzinger TA, Radhakrishna A. Simulation distances. <i>Theoretical Computer Science</i>. 2012;413(1):21-35. doi:<a href=\"https://doi.org/10.1016/j.tcs.2011.08.002\">10.1016/j.tcs.2011.08.002</a>","apa":"Cerny, P., Henzinger, T. A., &#38; Radhakrishna, A. (2012). Simulation distances. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2011.08.002\">https://doi.org/10.1016/j.tcs.2011.08.002</a>","chicago":"Cerny, Pavol, Thomas A Henzinger, and Arjun Radhakrishna. “Simulation Distances.” <i>Theoretical Computer Science</i>. Elsevier, 2012. <a href=\"https://doi.org/10.1016/j.tcs.2011.08.002\">https://doi.org/10.1016/j.tcs.2011.08.002</a>.","ieee":"P. Cerny, T. A. Henzinger, and A. Radhakrishna, “Simulation distances,” <i>Theoretical Computer Science</i>, vol. 413, no. 1. Elsevier, pp. 21–35, 2012.","mla":"Cerny, Pavol, et al. “Simulation Distances.” <i>Theoretical Computer Science</i>, vol. 413, no. 1, Elsevier, 2012, pp. 21–35, doi:<a href=\"https://doi.org/10.1016/j.tcs.2011.08.002\">10.1016/j.tcs.2011.08.002</a>.","short":"P. Cerny, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 413 (2012) 21–35.","ista":"Cerny P, Henzinger TA, Radhakrishna A. 2012. Simulation distances. Theoretical Computer Science. 413(1), 21–35."},"abstract":[{"text":"Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by real-valued distance functions between systems, where the distance between implementation and specification provides a measure of &quot;fit&quot; or &quot;desirability&quot;. We extend the simulation preorder to the quantitative setting by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specifications. The distances can be computed in polynomial time for safety specifications, and for liveness specifications given by weak fairness constraints. We show that the distance functions satisfy the triangle inequality, that the distance between two systems does not increase under parallel composition with a third system, and that the distance between two systems can be bounded from above and below by distances between abstractions of the two systems. These properties suggest that our simulation distances provide an appropriate basis for a quantitative theory of discrete systems. We also demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes.","lang":"eng"}],"doi":"10.1016/j.tcs.2011.08.002","day":"06","volume":413,"acknowledgement":"This work was partially supported by the ERC Advanced Grant QUAREM, the FWF NFN Grant S11402-N23 (RiSE), the European Union project COMBEST and the European Network of Excellence Artist Design.","publication":"Theoretical Computer Science","month":"01","oa_version":"None","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","_id":"25EFB36C-B435-11E9-9278-68D0E5697425","grant_number":"215543","name":"COMponent-Based Embedded Systems design Techniques"},{"_id":"25F1337C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Design for Embedded Systems","grant_number":"214373"}],"language":[{"iso":"eng"}],"date_published":"2012-01-06T00:00:00Z","type":"journal_article","publist_id":"3408","status":"public","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"4393"},{"relation":"earlier_version","id":"5389","status":"public"}]},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87"},{"conference":{"name":"VMCAI: Verification, Model Checking and Abstract Interpretation","start_date":"2012-01-22","end_date":"2012-01-24","location":"Philadelphia, PA, USA"},"language":[{"iso":"eng"}],"month":"01","oa_version":"Submitted Version","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"has_accepted_license":"1","status":"public","related_material":{"record":[{"relation":"dissertation_contains","id":"1405","status":"public"}]},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","file":[{"relation":"main_file","access_level":"open_access","file_id":"4759","creator":"system","date_created":"2018-12-12T10:09:35Z","checksum":"f2f0d55efa32309ad1fe65a5fcaad90c","file_size":217104,"date_updated":"2020-07-14T12:46:05Z","file_name":"IST-2012-100-v1+1_Ideal_abstractions_for_well-structured_transition_systems.pdf","content_type":"application/pdf"}],"oa":1,"publist_id":"3406","date_published":"2012-01-01T00:00:00Z","type":"conference","publisher":"Springer","file_date_updated":"2020-07-14T12:46:05Z","page":"445 - 460","quality_controlled":"1","ec_funded":1,"title":"Ideal abstractions for well structured transition systems","pubrep_id":"100","alternative_title":["LNCS"],"intvolume":"      7148","publication_status":"published","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T12:02:16Z","author":[{"orcid":"0000-0002-3197-8736","full_name":"Zufferey, Damien","first_name":"Damien","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","last_name":"Wies","first_name":"Thomas","full_name":"Wies, Thomas"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"_id":"3251","ddc":["000","005"],"acknowledgement":"This research was supported in part by the European Research Council (ERC) Advanced Investigator Grant QUAREM and by the Austrian Science Fund (FWF) project S11402-N23.","volume":7148,"abstract":[{"lang":"eng","text":"Many infinite state systems can be seen as well-structured transition systems (WSTS), i.e., systems equipped with a well-quasi-ordering on states that is also a simulation relation. WSTS are an attractive target for formal analysis because there exist generic algorithms that decide interesting verification problems for this class. Among the most popular algorithms are acceleration-based forward analyses for computing the covering set. Termination of these algorithms can only be guaranteed for flattable WSTS. Yet, many WSTS of practical interest are not flattable and the question whether any given WSTS is flattable is itself undecidable. We therefore propose an analysis that computes the covering set and captures the essence of acceleration-based algorithms, but sacrifices precision for guaranteed termination. Our analysis is an abstract interpretation whose abstract domain builds on the ideal completion of the well-quasi-ordered state space, and a widening operator that mimics acceleration and controls the loss of precision of the analysis. We present instances of our framework for various classes of WSTS. Our experience with a prototype implementation indicates that, despite the inherent precision loss, our analysis often computes the precise covering set of the analyzed system."}],"doi":"10.1007/978-3-642-27940-9_29","day":"01","date_updated":"2023-09-07T11:36:36Z","year":"2012","citation":{"short":"D. Zufferey, T. Wies, T.A. Henzinger, in:, Springer, 2012, pp. 445–460.","mla":"Zufferey, Damien, et al. <i>Ideal Abstractions for Well Structured Transition Systems</i>. Vol. 7148, Springer, 2012, pp. 445–60, doi:<a href=\"https://doi.org/10.1007/978-3-642-27940-9_29\">10.1007/978-3-642-27940-9_29</a>.","ista":"Zufferey D, Wies T, Henzinger TA. 2012. Ideal abstractions for well structured transition systems. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 7148, 445–460.","ama":"Zufferey D, Wies T, Henzinger TA. Ideal abstractions for well structured transition systems. In: Vol 7148. Springer; 2012:445-460. doi:<a href=\"https://doi.org/10.1007/978-3-642-27940-9_29\">10.1007/978-3-642-27940-9_29</a>","apa":"Zufferey, D., Wies, T., &#38; Henzinger, T. A. (2012). Ideal abstractions for well structured transition systems (Vol. 7148, pp. 445–460). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-642-27940-9_29\">https://doi.org/10.1007/978-3-642-27940-9_29</a>","chicago":"Zufferey, Damien, Thomas Wies, and Thomas A Henzinger. “Ideal Abstractions for Well Structured Transition Systems,” 7148:445–60. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-27940-9_29\">https://doi.org/10.1007/978-3-642-27940-9_29</a>.","ieee":"D. Zufferey, T. Wies, and T. A. Henzinger, “Ideal abstractions for well structured transition systems,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA, 2012, vol. 7148, pp. 445–460."}},{"volume":7148,"acknowledgement":"This work was partly supported by the French National Research Agency (ANR) project Veridyc (ANR-09-SEGI-016).","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","status":"public","day":"26","doi":"10.1007/978-3-642-27940-9_1","publist_id":"3404","abstract":[{"text":"We describe a framework for reasoning about programs with lists carrying integer numerical data. We use abstract domains to describe and manipulate complex constraints on configurations of these programs mixing constraints on the shape of the heap, sizes of the lists, on the multisets of data stored in these lists, and on the data at their different positions. Moreover, we provide powerful techniques for automatic validation of Hoare-triples and invariant checking, as well as for automatic synthesis of invariants and procedure summaries using modular inter-procedural analysis. The approach has been implemented in a tool called Celia and experimented successfully on a large benchmark of programs.","lang":"eng"}],"citation":{"ista":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Abstract domains for automated reasoning about list manipulating programs with infinite data. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 7148, 1–22.","mla":"Bouajjani, Ahmed, et al. <i>Abstract Domains for Automated Reasoning about List Manipulating Programs with Infinite Data</i>. Vol. 7148, Springer, 2012, pp. 1–22, doi:<a href=\"https://doi.org/10.1007/978-3-642-27940-9_1\">10.1007/978-3-642-27940-9_1</a>.","short":"A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Springer, 2012, pp. 1–22.","ieee":"A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Abstract domains for automated reasoning about list manipulating programs with infinite data,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA, 2012, vol. 7148, pp. 1–22.","chicago":"Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu. “Abstract Domains for Automated Reasoning about List Manipulating Programs with Infinite Data,” 7148:1–22. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-27940-9_1\">https://doi.org/10.1007/978-3-642-27940-9_1</a>.","ama":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. Abstract domains for automated reasoning about list manipulating programs with infinite data. In: Vol 7148. Springer; 2012:1-22. doi:<a href=\"https://doi.org/10.1007/978-3-642-27940-9_1\">10.1007/978-3-642-27940-9_1</a>","apa":"Bouajjani, A., Dragoi, C., Enea, C., &#38; Sighireanu, M. (2012). Abstract domains for automated reasoning about list manipulating programs with infinite data (Vol. 7148, pp. 1–22). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-642-27940-9_1\">https://doi.org/10.1007/978-3-642-27940-9_1</a>"},"year":"2012","date_updated":"2021-01-12T07:42:09Z","type":"conference","date_published":"2012-02-26T00:00:00Z","publisher":"Springer","conference":{"end_date":"2012-01-24","location":"Philadelphia, PA, USA","name":"VMCAI: Verification, Model Checking and Abstract Interpretation","start_date":"2012-01-22"},"quality_controlled":"1","page":"1 - 22","language":[{"iso":"eng"}],"date_created":"2018-12-11T12:02:17Z","department":[{"_id":"ToHe"}],"publication_status":"published","oa_version":"None","intvolume":"      7148","alternative_title":["LNCS"],"month":"02","title":"Abstract domains for automated reasoning about list manipulating programs with infinite data","_id":"3253","author":[{"first_name":"Ahmed","last_name":"Bouajjani","full_name":"Bouajjani, Ahmed"},{"last_name":"Dragoi","first_name":"Cezara","full_name":"Dragoi, Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Enea, Constantin","first_name":"Constantin","last_name":"Enea"},{"last_name":"Sighireanu","first_name":"Mihaela","full_name":"Sighireanu, Mihaela"}]},{"page":"167-182","series_title":"LNCS","quality_controlled":"1","publisher":"Springer","author":[{"last_name":"Bouajjani","first_name":"Ahmed","full_name":"Bouajjani, Ahmed"},{"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","first_name":"Mihaela","last_name":"Sighireanu"}],"_id":"10903","scopus_import":"1","title":"Accurate invariant checking for programs manipulating lists and arrays with infinite data","alternative_title":["LNCS"],"intvolume":"      7561","publication_status":"published","department":[{"_id":"ToHe"}],"date_created":"2022-03-21T07:58:39Z","article_processing_charge":"No","acknowledgement":"This work has been partially supported by the French ANR project Veridyc","volume":7561,"date_updated":"2023-09-05T14:07:24Z","citation":{"mla":"Bouajjani, Ahmed, et al. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” <i>Automated Technology for Verification and Analysis</i>, vol. 7561, Springer, 2012, pp. 167–82, doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">10.1007/978-3-642-33386-6_14</a>.","short":"A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Automated Technology for Verification and Analysis, Springer, Berlin, Heidelberg, 2012, pp. 167–182.","ista":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Accurate invariant checking for programs manipulating lists and arrays with infinite data. Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and AnalysisLNCS, LNCS, vol. 7561, 167–182.","ama":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. Accurate invariant checking for programs manipulating lists and arrays with infinite data. In: <i>Automated Technology for Verification and Analysis</i>. Vol 7561. LNCS. Berlin, Heidelberg: Springer; 2012:167-182. doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">10.1007/978-3-642-33386-6_14</a>","apa":"Bouajjani, A., Dragoi, C., Enea, C., &#38; Sighireanu, M. (2012). Accurate invariant checking for programs manipulating lists and arrays with infinite data. In <i>Automated Technology for Verification and Analysis</i> (Vol. 7561, pp. 167–182). Berlin, Heidelberg: Springer. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">https://doi.org/10.1007/978-3-642-33386-6_14</a>","ieee":"A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Accurate invariant checking for programs manipulating lists and arrays with infinite data,” in <i>Automated Technology for Verification and Analysis</i>, Thiruvananthapuram, India, 2012, vol. 7561, pp. 167–182.","chicago":"Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” In <i>Automated Technology for Verification and Analysis</i>, 7561:167–82. LNCS. Berlin, Heidelberg: Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_14\">https://doi.org/10.1007/978-3-642-33386-6_14</a>."},"year":"2012","abstract":[{"lang":"eng","text":"We propose a logic-based framework for automated reasoning about sequential programs manipulating singly-linked lists and arrays with unbounded data. We introduce the logic SLAD, which allows combining shape constraints, written in a fragment of Separation Logic, with data and size constraints. We address the problem of checking the entailment between SLAD formulas, which is crucial in performing pre-post condition reasoning. Although this problem is undecidable in general for SLAD, we propose a sound and powerful procedure that is able to solve this problem for a large class of formulas, beyond the capabilities of existing techniques and tools. We prove that this procedure is complete, i.e., it is actually a decision procedure for this problem, for an important fragment of SLAD including known decidable logics. We implemented this procedure and shown its preciseness and its efficiency on a significant benchmark of formulas."}],"doi":"10.1007/978-3-642-33386-6_14","day":"15","language":[{"iso":"eng"}],"conference":{"start_date":"2012-10-03","name":"ATVA: Automated Technology for Verification and Analysis","location":"Thiruvananthapuram, India","end_date":"2012-10-06"},"publication":"Automated Technology for Verification and Analysis","month":"10","oa_version":"None","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","place":"Berlin, Heidelberg","date_published":"2012-10-15T00:00:00Z","type":"conference","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783642333866"],"isbn":["9783642333859"]}},{"oa_version":"Published Version","month":"04","publication":"Tools and Algorithms for the Construction and Analysis of Systems","conference":{"start_date":"2012-03-24","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Tallinn, Estonia","end_date":"2012-04-01"},"language":[{"iso":"eng"}],"publication_identifier":{"eisbn":["9783642287565"],"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783642287558"]},"oa":1,"date_published":"2012-04-01T00:00:00Z","type":"conference","place":"Berlin, Heidelberg","main_file_link":[{"url":"https://doi.org/10.1007/978-3-642-28756-5_46","open_access":"1"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","publication_status":"published","article_processing_charge":"No","department":[{"_id":"ToHe"}],"date_created":"2022-03-21T08:03:30Z","title":"HSF(C): A software verifier based on Horn clauses","alternative_title":["LNCS"],"intvolume":"      7214","_id":"10906","scopus_import":"1","author":[{"first_name":"Sergey","last_name":"Grebenshchikov","full_name":"Grebenshchikov, Sergey"},{"id":"335E5684-F248-11E8-B48F-1D18A9856A87","full_name":"Gupta, Ashutosh","last_name":"Gupta","first_name":"Ashutosh"},{"last_name":"Lopes","first_name":"Nuno P.","full_name":"Lopes, Nuno P."},{"full_name":"Popeea, Corneliu","last_name":"Popeea","first_name":"Corneliu"},{"first_name":"Andrey","last_name":"Rybalchenko","full_name":"Rybalchenko, Andrey"}],"publisher":"Springer","editor":[{"full_name":"Flanagan, Cormac","first_name":"Cormac","last_name":"Flanagan"},{"first_name":"Barbara","last_name":"König","full_name":"König, Barbara"}],"page":"549-551","series_title":"LNCS","quality_controlled":"1","doi":"10.1007/978-3-642-28756-5_46","day":"01","abstract":[{"text":"HSF(C) is a tool that automates verification of safety and liveness properties for C programs. This paper describes the verification approach taken by HSF(C) and provides instructions on how to install and use the tool.","lang":"eng"}],"date_updated":"2023-09-05T14:09:54Z","year":"2012","citation":{"ista":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. 2012. HSF(C): A software verifier based on Horn clauses. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of SystemsLNCS, LNCS, vol. 7214, 549–551.","short":"S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko, in:, C. Flanagan, B. König (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Springer, Berlin, Heidelberg, 2012, pp. 549–551.","mla":"Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn Clauses.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51, doi:<a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">10.1007/978-3-642-28756-5_46</a>.","ieee":"S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko, “HSF(C): A software verifier based on Horn clauses,” in <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, Tallinn, Estonia, 2012, vol. 7214, pp. 549–551.","chicago":"Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, edited by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">https://doi.org/10.1007/978-3-642-28756-5_46</a>.","ama":"Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. HSF(C): A software verifier based on Horn clauses. In: Flanagan C, König B, eds. <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 7214. LNCS. Berlin, Heidelberg: Springer; 2012:549-551. doi:<a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">10.1007/978-3-642-28756-5_46</a>","apa":"Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., &#38; Rybalchenko, A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan &#38; B. König (Eds.), <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. <a href=\"https://doi.org/10.1007/978-3-642-28756-5_46\">https://doi.org/10.1007/978-3-642-28756-5_46</a>"},"volume":7214},{"volume":10,"external_id":{"pmid":["22778152"]},"date_updated":"2021-01-12T06:56:38Z","citation":{"ieee":"T. A. Henzinger and M. Mateescu, “The propagation approach for computing biochemical reaction networks,” <i>IEEE ACM Transactions on Computational Biology and Bioinformatics</i>, vol. 10, no. 2. IEEE, pp. 310–322, 2012.","chicago":"Henzinger, Thomas A, and Maria Mateescu. “The Propagation Approach for Computing Biochemical Reaction Networks.” <i>IEEE ACM Transactions on Computational Biology and Bioinformatics</i>. IEEE, 2012. <a href=\"https://doi.org/10.1109/TCBB.2012.91\">https://doi.org/10.1109/TCBB.2012.91</a>.","ama":"Henzinger TA, Mateescu M. The propagation approach for computing biochemical reaction networks. <i>IEEE ACM Transactions on Computational Biology and Bioinformatics</i>. 2012;10(2):310-322. doi:<a href=\"https://doi.org/10.1109/TCBB.2012.91\">10.1109/TCBB.2012.91</a>","apa":"Henzinger, T. A., &#38; Mateescu, M. (2012). The propagation approach for computing biochemical reaction networks. <i>IEEE ACM Transactions on Computational Biology and Bioinformatics</i>. IEEE. <a href=\"https://doi.org/10.1109/TCBB.2012.91\">https://doi.org/10.1109/TCBB.2012.91</a>","ista":"Henzinger TA, Mateescu M. 2012. The propagation approach for computing biochemical reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics. 10(2), 310–322.","mla":"Henzinger, Thomas A., and Maria Mateescu. “The Propagation Approach for Computing Biochemical Reaction Networks.” <i>IEEE ACM Transactions on Computational Biology and Bioinformatics</i>, vol. 10, no. 2, IEEE, 2012, pp. 310–22, doi:<a href=\"https://doi.org/10.1109/TCBB.2012.91\">10.1109/TCBB.2012.91</a>.","short":"T.A. Henzinger, M. Mateescu, IEEE ACM Transactions on Computational Biology and Bioinformatics 10 (2012) 310–322."},"year":"2012","abstract":[{"lang":"eng","text":"We introduce propagation models (PMs), a formalism able to express several kinds of equations that describe the behavior of biochemical reaction networks. Furthermore, we introduce the propagation abstract data type (PADT), which separates concerns regarding different numerical algorithms for the transient analysis of biochemical reaction networks from concerns regarding their implementation, thus allowing for portable and efficient solutions. The state of a propagation abstract data type is given by a vector that assigns mass values to a set of nodes, and its (next) operator propagates mass values through this set of nodes. We propose an approximate implementation of the (next) operator, based on threshold abstraction, which propagates only &quot;significant&quot; mass values and thus achieves a compromise between efficiency and accuracy. Finally, we give three use cases for propagation models: the chemical master equation (CME), the reaction rate equation (RRE), and a hybrid method that combines these two equations. These three applications use propagation models in order to propagate probabilities and/or expected values and variances of the model's variables."}],"doi":"10.1109/TCBB.2012.91","day":"03","page":"310 - 322","ec_funded":1,"quality_controlled":"1","publisher":"IEEE","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"first_name":"Maria","last_name":"Mateescu","full_name":"Mateescu, Maria","id":"3B43276C-F248-11E8-B48F-1D18A9856A87"}],"issue":"2","_id":"2302","pmid":1,"scopus_import":1,"title":"The propagation approach for computing biochemical reaction networks","intvolume":"        10","publication_status":"published","department":[{"_id":"ToHe"},{"_id":"CaGu"}],"date_created":"2018-12-11T11:56:52Z","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2012-07-03T00:00:00Z","type":"journal_article","publist_id":"4625","language":[{"iso":"eng"}],"publication":"IEEE ACM Transactions on Computational Biology and Bioinformatics","month":"07","oa_version":"None","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"}]},{"abstract":[{"text":"We solve the longstanding open problems of the blow-up involved in the translations, when possible, of a nondeterministic Büchi word automaton (NBW) to a nondeterministic co-Büchi word automaton (NCW) and to a deterministic co-Büchi word automaton (DCW). For the NBW to NCW translation, the currently known upper bound is 2o(nlog n) and the lower bound is 1.5n. We improve the upper bound to n2n and describe a matching lower bound of 2ω(n). For the NBW to DCW translation, the currently known upper bound is 2o(nlog n). We improve it to 2 o(n), which is asymptotically tight. Both of our upper-bound constructions are based on a simple subset construction, do not involve intermediate automata with richer acceptance conditions, and can be implemented symbolically. We continue and solve the open problems of translating nondeterministic Streett, Rabin, Muller, and parity word automata to NCW and to DCW. Going via an intermediate NBW is not optimal and we describe direct, simple, and asymptotically tight constructions, involving a 2o(n) blow-up. The constructions are variants of the subset construction, providing a unified approach for translating all common classes of automata to NCW and DCW. Beyond the theoretical importance of the results, we point to numerous applications of the new constructions. In particular, they imply a simple subset-construction based translation, when possible, of LTL to deterministic Büchi word automata.","lang":"eng"}],"publist_id":"7326","doi":"10.1145/2362355.2362357","day":"01","date_published":"2012-10-01T00:00:00Z","type":"journal_article","date_updated":"2021-01-12T08:01:03Z","year":"2012","citation":{"ama":"Boker U, Kupferman O. Translating to Co-Büchi made tight, unified, and useful. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2012;13(4). doi:<a href=\"https://doi.org/10.1145/2362355.2362357\">10.1145/2362355.2362357</a>","apa":"Boker, U., &#38; Kupferman, O. (2012). Translating to Co-Büchi made tight, unified, and useful. <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href=\"https://doi.org/10.1145/2362355.2362357\">https://doi.org/10.1145/2362355.2362357</a>","ieee":"U. Boker and O. Kupferman, “Translating to Co-Büchi made tight, unified, and useful,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 13, no. 4. ACM, 2012.","chicago":"Boker, Udi, and Orna Kupferman. “Translating to Co-Büchi Made Tight, Unified, and Useful.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2012. <a href=\"https://doi.org/10.1145/2362355.2362357\">https://doi.org/10.1145/2362355.2362357</a>.","mla":"Boker, Udi, and Orna Kupferman. “Translating to Co-Büchi Made Tight, Unified, and Useful.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 13, no. 4, 29, ACM, 2012, doi:<a href=\"https://doi.org/10.1145/2362355.2362357\">10.1145/2362355.2362357</a>.","short":"U. Boker, O. Kupferman, ACM Transactions on Computational Logic (TOCL) 13 (2012).","ista":"Boker U, Kupferman O. 2012. Translating to Co-Büchi made tight, unified, and useful. ACM Transactions on Computational Logic (TOCL). 13(4), 29."},"status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","volume":13,"title":"Translating to Co-Büchi made tight, unified, and useful","month":"10","article_number":"29","intvolume":"        13","oa_version":"None","publication_status":"published","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T11:46:47Z","author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","first_name":"Udi","last_name":"Boker","full_name":"Boker, Udi"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"}],"issue":"4","_id":"494","publication":"ACM Transactions on Computational Logic (TOCL)","scopus_import":1,"publisher":"ACM","language":[{"iso":"eng"}],"quality_controlled":"1"},{"year":"2012","citation":{"ieee":"A. Gupta, “Improved Single Pass Algorithms for Resolution Proof Reduction,” in <i>Automated Technology for Verification and Analysis</i>, vol. 7561, Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 107–121.","chicago":"Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” In <i>Automated Technology for Verification and Analysis</i>, 7561:107–21. LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">https://doi.org/10.1007/978-3-642-33386-6_10</a>.","apa":"Gupta, A. (2012). Improved Single Pass Algorithms for Resolution Proof Reduction. In <i>Automated Technology for Verification and Analysis</i> (Vol. 7561, pp. 107–121). Berlin, Heidelberg: Springer Berlin Heidelberg. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">https://doi.org/10.1007/978-3-642-33386-6_10</a>","ama":"Gupta A. Improved Single Pass Algorithms for Resolution Proof Reduction. In: <i>Automated Technology for Verification and Analysis</i>. Vol 7561. LNCS. Berlin, Heidelberg: Springer Berlin Heidelberg; 2012:107-121. doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">10.1007/978-3-642-33386-6_10</a>","ista":"Gupta A. 2012.Improved Single Pass Algorithms for Resolution Proof Reduction. In: Automated Technology for Verification and Analysis. vol. 7561, 107–121.","mla":"Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” <i>Automated Technology for Verification and Analysis</i>, vol. 7561, Springer Berlin Heidelberg, 2012, pp. 107–21, doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_10\">10.1007/978-3-642-33386-6_10</a>.","short":"A. Gupta, in:, Automated Technology for Verification and Analysis, Springer Berlin Heidelberg, Berlin, Heidelberg, 2012, pp. 107–121."},"date_updated":"2023-09-05T14:15:29Z","doi":"10.1007/978-3-642-33386-6_10","ddc":["005"],"volume":7561,"author":[{"first_name":"Ashutosh","last_name":"Gupta","full_name":"Gupta, Ashutosh"}],"_id":"5745","intvolume":"      7561","title":"Improved Single Pass Algorithms for Resolution Proof Reduction","pubrep_id":"180","article_processing_charge":"No","date_created":"2018-12-18T13:01:46Z","department":[{"_id":"ToHe"}],"publication_status":"published","file_date_updated":"2020-07-14T12:47:10Z","quality_controlled":"1","series_title":"LNCS","ec_funded":1,"page":"107-121","publisher":"Springer Berlin Heidelberg","type":"book_chapter","date_published":"2012-01-01T00:00:00Z","oa":1,"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783642333859","9783642333866"]},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","file":[{"content_type":"application/pdf","file_name":"2012_ATVA_Gupta.pdf","date_updated":"2020-07-14T12:47:10Z","checksum":"68415837a315de3cc4d120f6019d752c","file_size":465502,"date_created":"2018-12-18T13:07:35Z","creator":"dernst","file_id":"5746","relation":"main_file","access_level":"open_access"}],"place":"Berlin, Heidelberg","has_accepted_license":"1","publication":"Automated Technology for Verification and Analysis","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"oa_version":"None","language":[{"iso":"eng"}],"conference":{"end_date":"2012-10-06","location":"Thiruvananthapuram, Kerala, India","start_date":"2012-10-03","name":"ATVA 2012"}},{"title":"Conditional model checking: A technique to pass information between verifiers","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T11:51:42Z","publication_status":"published","author":[{"last_name":"Beyer","first_name":"Dirk","full_name":"Beyer, Dirk"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Mehmet","last_name":"Keremoglu","full_name":"Keremoglu, Mehmet"},{"full_name":"Wendler, Philipp","last_name":"Wendler","first_name":"Philipp"}],"scopus_import":1,"_id":"1384","publisher":"ACM","quality_controlled":"1","ec_funded":1,"abstract":[{"text":"Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition Ψ - usually a state predicate - such that the program satisfies the specification under the condition Ψ - that is, as long as the program does not leave the states in which Ψ is satisfied. In our experiments, we investigated as one major application of conditional model checking the sequential combination of model checkers with information passing. We give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve. Our experiments demonstrate that repeated application of conditional model checkers, passing information from one model checker to the next, can significantly improve the verification results and performance, i.e., we can now verify programs that we could not verify before.","lang":"eng"}],"day":"01","doi":"10.1145/2393596.2393664","year":"2012","citation":{"mla":"Beyer, Dirk, et al. “Conditional Model Checking: A Technique to Pass Information between Verifiers.” <i>Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering</i>, 57, ACM, 2012, doi:<a href=\"https://doi.org/10.1145/2393596.2393664\">10.1145/2393596.2393664</a>.","short":"D. Beyer, T.A. Henzinger, M. Keremoglu, P. Wendler, in:, Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, ACM, 2012.","ista":"Beyer D, Henzinger TA, Keremoglu M, Wendler P. 2012. Conditional model checking: A technique to pass information between verifiers. Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering. FSE: Foundations of Software Engineering, 57.","ama":"Beyer D, Henzinger TA, Keremoglu M, Wendler P. Conditional model checking: A technique to pass information between verifiers. In: <i>Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering</i>. ACM; 2012. doi:<a href=\"https://doi.org/10.1145/2393596.2393664\">10.1145/2393596.2393664</a>","apa":"Beyer, D., Henzinger, T. A., Keremoglu, M., &#38; Wendler, P. (2012). Conditional model checking: A technique to pass information between verifiers. In <i>Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering</i>. Cary, NC, USA: ACM. <a href=\"https://doi.org/10.1145/2393596.2393664\">https://doi.org/10.1145/2393596.2393664</a>","ieee":"D. Beyer, T. A. Henzinger, M. Keremoglu, and P. Wendler, “Conditional model checking: A technique to pass information between verifiers,” in <i>Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering</i>, Cary, NC, USA, 2012.","chicago":"Beyer, Dirk, Thomas A Henzinger, Mehmet Keremoglu, and Philipp Wendler. “Conditional Model Checking: A Technique to Pass Information between Verifiers.” In <i>Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering</i>. ACM, 2012. <a href=\"https://doi.org/10.1145/2393596.2393664\">https://doi.org/10.1145/2393596.2393664</a>."},"date_updated":"2021-01-12T06:50:18Z","acknowledgement":"This  research  was  supported  by  the  Canadian  NSERC grant   RGPIN   341819-07,    the   ERC   Advanced   Grant QUAREM, and the Austrian Science Fund NFN RiSE.","article_number":"57","month":"11","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"oa_version":"Preprint","publication":"Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering","conference":{"location":"Cary, NC, USA","end_date":"2012-11-16","start_date":"2012-11-11","name":"FSE: Foundations of Software Engineering"},"language":[{"iso":"eng"}],"publist_id":"5826","oa":1,"type":"conference","date_published":"2012-11-01T00:00:00Z","status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"url":"http://arxiv.org/abs/1109.6926","open_access":"1"}]},{"date_created":"2018-12-11T12:05:26Z","department":[{"_id":"ToHe"}],"publication_status":"published","oa_version":"None","intvolume":"        77","title":"Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code","month":"02","scopus_import":1,"publication":"Science of Computer Programming","_id":"3836","issue":"2","author":[{"first_name":"Arkadeb","last_name":"Ghosal","full_name":"Ghosal, Arkadeb"},{"full_name":"Iercan, Daniel","last_name":"Iercan","first_name":"Daniel"},{"full_name":"Kirsch, Christoph","first_name":"Christoph","last_name":"Kirsch"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Sangiovanni Vincentelli, Alberto","last_name":"Sangiovanni Vincentelli","first_name":"Alberto"}],"publisher":"Elsevier","quality_controlled":"1","page":"96 - 112","language":[{"iso":"eng"}],"day":"01","doi":"10.1016/j.scico.2010.06.004","publist_id":"2370","abstract":[{"lang":"eng","text":"Hierarchical Timing Language (HTL) is a coordination language for distributed, hard real-time applications. HTL is a hierarchical extension of Giotto and, like its predecessor, based on the logical execution time (LET) paradigm of real-time programming. Giotto is compiled into code for a virtual machine, called the EmbeddedMachine (or E machine). If HTL is targeted to the E machine, then the hierarchicalprogram structure needs to be flattened; the flattening makes separatecompilation difficult, and may result in E machinecode of exponential size. In this paper, we propose a generalization of the E machine, which supports a hierarchicalprogram structure at runtime through real-time trigger mechanisms that are arranged in a tree. We present the generalized E machine, and a modular compiler for HTL that generates code of linear size. The compiler may generate code for any part of a given HTL program separately in any order."}],"citation":{"ama":"Ghosal A, Iercan D, Kirsch C, Henzinger TA, Sangiovanni Vincentelli A. Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code. <i>Science of Computer Programming</i>. 2012;77(2):96-112. doi:<a href=\"https://doi.org/10.1016/j.scico.2010.06.004\">10.1016/j.scico.2010.06.004</a>","apa":"Ghosal, A., Iercan, D., Kirsch, C., Henzinger, T. A., &#38; Sangiovanni Vincentelli, A. (2012). Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code. <i>Science of Computer Programming</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.scico.2010.06.004\">https://doi.org/10.1016/j.scico.2010.06.004</a>","ieee":"A. Ghosal, D. Iercan, C. Kirsch, T. A. Henzinger, and A. Sangiovanni Vincentelli, “Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code,” <i>Science of Computer Programming</i>, vol. 77, no. 2. Elsevier, pp. 96–112, 2012.","chicago":"Ghosal, Arkadeb, Daniel Iercan, Christoph Kirsch, Thomas A Henzinger, and Alberto Sangiovanni Vincentelli. “Separate Compilation of Hierarchical Real-Time Programs into Linear-Bounded Embedded Machine Code.” <i>Science of Computer Programming</i>. Elsevier, 2012. <a href=\"https://doi.org/10.1016/j.scico.2010.06.004\">https://doi.org/10.1016/j.scico.2010.06.004</a>.","mla":"Ghosal, Arkadeb, et al. “Separate Compilation of Hierarchical Real-Time Programs into Linear-Bounded Embedded Machine Code.” <i>Science of Computer Programming</i>, vol. 77, no. 2, Elsevier, 2012, pp. 96–112, doi:<a href=\"https://doi.org/10.1016/j.scico.2010.06.004\">10.1016/j.scico.2010.06.004</a>.","short":"A. Ghosal, D. Iercan, C. Kirsch, T.A. Henzinger, A. Sangiovanni Vincentelli, Science of Computer Programming 77 (2012) 96–112.","ista":"Ghosal A, Iercan D, Kirsch C, Henzinger TA, Sangiovanni Vincentelli A. 2012. Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code. Science of Computer Programming. 77(2), 96–112."},"year":"2012","date_updated":"2021-01-12T07:52:32Z","type":"journal_article","date_published":"2012-02-01T00:00:00Z","volume":77,"status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87"},{"date_updated":"2022-05-24T08:00:54Z","year":"2012","citation":{"short":"K. Chatterjee, T.A. Henzinger, Journal of Computer and System Sciences 78 (2012) 394–413.","mla":"Chatterjee, Krishnendu, and Thomas A. Henzinger. “A Survey of Stochastic ω Regular Games.” <i>Journal of Computer and System Sciences</i>, vol. 78, no. 2, Elsevier, 2012, pp. 394–413, doi:<a href=\"https://doi.org/10.1016/j.jcss.2011.05.002\">10.1016/j.jcss.2011.05.002</a>.","ista":"Chatterjee K, Henzinger TA. 2012. A survey of stochastic ω regular games. Journal of Computer and System Sciences. 78(2), 394–413.","apa":"Chatterjee, K., &#38; Henzinger, T. A. (2012). A survey of stochastic ω regular games. <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jcss.2011.05.002\">https://doi.org/10.1016/j.jcss.2011.05.002</a>","ama":"Chatterjee K, Henzinger TA. A survey of stochastic ω regular games. <i>Journal of Computer and System Sciences</i>. 2012;78(2):394-413. doi:<a href=\"https://doi.org/10.1016/j.jcss.2011.05.002\">10.1016/j.jcss.2011.05.002</a>","ieee":"K. Chatterjee and T. A. Henzinger, “A survey of stochastic ω regular games,” <i>Journal of Computer and System Sciences</i>, vol. 78, no. 2. Elsevier, pp. 394–413, 2012.","chicago":"Chatterjee, Krishnendu, and Thomas A Henzinger. “A Survey of Stochastic ω Regular Games.” <i>Journal of Computer and System Sciences</i>. Elsevier, 2012. <a href=\"https://doi.org/10.1016/j.jcss.2011.05.002\">https://doi.org/10.1016/j.jcss.2011.05.002</a>."},"abstract":[{"lang":"eng","text":"We summarize classical and recent results about two-player games played on graphs with ω-regular objectives. These games have applications in the verification and synthesis of reactive systems. Important distinctions are whether a graph game is turn-based or concurrent; deterministic or stochastic; zero-sum or not. We cluster known results and open problems according to these classifications."}],"doi":"10.1016/j.jcss.2011.05.002","day":"02","ddc":["000"],"volume":78,"acknowledgement":"This research was supported in part by the ONR grant N00014-02-1-0671, by the AFOSR MURI grant F49620-00-1-0327, and by the NSF grants CCR-9988172, CCR-0085949, and CCR-0225610.","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"}],"issue":"2","_id":"3846","scopus_import":"1","title":"A survey of stochastic ω regular games","intvolume":"        78","publication_status":"published","article_processing_charge":"No","date_created":"2018-12-11T12:05:29Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:46:17Z","page":"394 - 413","quality_controlled":"1","article_type":"original","publisher":"Elsevier","date_published":"2012-03-02T00:00:00Z","type":"journal_article","oa":1,"publist_id":"2341","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","main_file_link":[{"url":"https://doi.org/10.1016/j.jcss.2011.05.002","open_access":"1"}],"file":[{"file_id":"5897","creator":"kschuh","access_level":"open_access","relation":"main_file","date_updated":"2020-07-14T12:46:17Z","file_name":"a_survey_of_stochastic_omega-regular_games.pdf","content_type":"application/pdf","date_created":"2019-01-29T10:54:28Z","file_size":336450,"checksum":"241b939deb4517cdd4426d49c67e3fa2"}],"publication":"Journal of Computer and System Sciences","has_accepted_license":"1","month":"03","oa_version":"Submitted Version","language":[{"iso":"eng"}]},{"conference":{"end_date":"2011-12-07","location":"Kenting, Taiwan","name":"APLAS: Asian Symposium on Programming Languages and Systems","start_date":"2011-12-05"},"editor":[{"first_name":"Hongseok","last_name":"Yang","full_name":"Yang, Hongseok"}],"publisher":"Springer","language":[{"iso":"eng"}],"ec_funded":1,"quality_controlled":"1","page":"188 - 203","intvolume":"      7078","alternative_title":["LNCS"],"title":"Solving recursion-free Horn clauses over LI+UIF","month":"12","date_created":"2018-12-11T12:02:20Z","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"}],"department":[{"_id":"ToHe"}],"publication_status":"published","oa_version":"None","author":[{"full_name":"Gupta, Ashutosh","first_name":"Ashutosh","last_name":"Gupta","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Popeea, Corneliu","first_name":"Corneliu","last_name":"Popeea"},{"full_name":"Rybalchenko, Andrey","first_name":"Andrey","last_name":"Rybalchenko"}],"_id":"3264","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","status":"public","volume":7078,"publist_id":"3383","abstract":[{"text":"Verification of programs with procedures, multi-threaded programs, and higher-order functional programs can be effectively au- tomated using abstraction and refinement schemes that rely on spurious counterexamples for abstraction discovery. The analysis of counterexam- ples can be automated by a series of interpolation queries, or, alterna- tively, as a constraint solving query expressed by a set of recursion free Horn clauses. (A set of interpolation queries can be formulated as a single constraint over Horn clauses with linear dependency structure between the unknown relations.) In this paper we present an algorithm for solving recursion free Horn clauses over a combined theory of linear real/rational arithmetic and uninterpreted functions. Our algorithm performs resolu- tion to deal with the clausal structure and relies on partial solutions to deal with (non-local) instances of functionality axioms.","lang":"eng"}],"day":"05","doi":"10.1007/978-3-642-25318-8_16","type":"conference","date_published":"2011-12-05T00:00:00Z","citation":{"chicago":"Gupta, Ashutosh, Corneliu Popeea, and Andrey Rybalchenko. “Solving Recursion-Free Horn Clauses over LI+UIF.” edited by Hongseok Yang, 7078:188–203. Springer, 2011. <a href=\"https://doi.org/10.1007/978-3-642-25318-8_16\">https://doi.org/10.1007/978-3-642-25318-8_16</a>.","ieee":"A. Gupta, C. Popeea, and A. Rybalchenko, “Solving recursion-free Horn clauses over LI+UIF,” presented at the APLAS: Asian Symposium on Programming Languages and Systems, Kenting, Taiwan, 2011, vol. 7078, pp. 188–203.","apa":"Gupta, A., Popeea, C., &#38; Rybalchenko, A. (2011). Solving recursion-free Horn clauses over LI+UIF. In H. Yang (Ed.) (Vol. 7078, pp. 188–203). Presented at the APLAS: Asian Symposium on Programming Languages and Systems, Kenting, Taiwan: Springer. <a href=\"https://doi.org/10.1007/978-3-642-25318-8_16\">https://doi.org/10.1007/978-3-642-25318-8_16</a>","ama":"Gupta A, Popeea C, Rybalchenko A. Solving recursion-free Horn clauses over LI+UIF. In: Yang H, ed. Vol 7078. Springer; 2011:188-203. doi:<a href=\"https://doi.org/10.1007/978-3-642-25318-8_16\">10.1007/978-3-642-25318-8_16</a>","ista":"Gupta A, Popeea C, Rybalchenko A. 2011. Solving recursion-free Horn clauses over LI+UIF. APLAS: Asian Symposium on Programming Languages and Systems, LNCS, vol. 7078, 188–203.","mla":"Gupta, Ashutosh, et al. <i>Solving Recursion-Free Horn Clauses over LI+UIF</i>. Edited by Hongseok Yang, vol. 7078, Springer, 2011, pp. 188–203, doi:<a href=\"https://doi.org/10.1007/978-3-642-25318-8_16\">10.1007/978-3-642-25318-8_16</a>.","short":"A. Gupta, C. Popeea, A. Rybalchenko, in:, H. Yang (Ed.), Springer, 2011, pp. 188–203."},"year":"2011","date_updated":"2021-01-12T07:42:15Z"},{"date_updated":"2021-01-12T07:42:29Z","citation":{"ama":"Henzinger TA, Mateescu M. Propagation models for computing biochemical reaction networks. In: Springer; 2011:1-3. doi:<a href=\"https://doi.org/10.1145/2037509.2037510\">10.1145/2037509.2037510</a>","apa":"Henzinger, T. A., &#38; Mateescu, M. (2011). Propagation models for computing biochemical reaction networks (pp. 1–3). Presented at the CMSB: Computational Methods in Systems Biology, Paris, France: Springer. <a href=\"https://doi.org/10.1145/2037509.2037510\">https://doi.org/10.1145/2037509.2037510</a>","chicago":"Henzinger, Thomas A, and Maria Mateescu. “Propagation Models for Computing Biochemical Reaction Networks,” 1–3. Springer, 2011. <a href=\"https://doi.org/10.1145/2037509.2037510\">https://doi.org/10.1145/2037509.2037510</a>.","ieee":"T. A. Henzinger and M. Mateescu, “Propagation models for computing biochemical reaction networks,” presented at the CMSB: Computational Methods in Systems Biology, Paris, France, 2011, pp. 1–3.","mla":"Henzinger, Thomas A., and Maria Mateescu. <i>Propagation Models for Computing Biochemical Reaction Networks</i>. Springer, 2011, pp. 1–3, doi:<a href=\"https://doi.org/10.1145/2037509.2037510\">10.1145/2037509.2037510</a>.","short":"T.A. Henzinger, M. Mateescu, in:, Springer, 2011, pp. 1–3.","ista":"Henzinger TA, Mateescu M. 2011. Propagation models for computing biochemical reaction networks. CMSB: Computational Methods in Systems Biology, 1–3."},"year":"2011","abstract":[{"text":"We introduce propagation models, a formalism designed to support general and efficient data structures for the transient analysis of biochemical reaction networks. We give two use cases for propagation abstract data types: the uniformization method and numerical integration. We also sketch an implementation of a propagation abstract data type, which uses abstraction to approximate states.","lang":"eng"}],"doi":"10.1145/2037509.2037510","day":"21","ddc":["000","004"],"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Mateescu, Maria","first_name":"Maria","last_name":"Mateescu"}],"_id":"3299","scopus_import":1,"title":"Propagation models for computing biochemical reaction networks","pubrep_id":"92","publication_status":"published","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T12:02:32Z","file_date_updated":"2020-07-14T12:46:06Z","page":"1 - 3","quality_controlled":"1","publisher":"Springer","date_published":"2011-09-21T00:00:00Z","type":"conference","oa":1,"publist_id":"3341","status":"public","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","file":[{"date_created":"2018-12-12T10:07:50Z","checksum":"7f5c65509db1a9fb049abedd9663ed06","file_size":255780,"date_updated":"2020-07-14T12:46:06Z","file_name":"IST-2012-92-v1+1_Propagation_models_for_computing_biochemical_reaction_networks.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"4649","creator":"system"}],"has_accepted_license":"1","month":"09","oa_version":"Submitted Version","language":[{"iso":"eng"}],"conference":{"name":"CMSB: Computational Methods in Systems Biology","start_date":"2011-09-21","end_date":"2011-09-23","location":"Paris, France"}},{"citation":{"ama":"Henzinger TA, Mateescu M. Tail approximation for the chemical master equation. In: Tampere International Center for Signal Processing; 2011.","apa":"Henzinger, T. A., &#38; Mateescu, M. (2011). Tail approximation for the chemical master equation. Presented at the WCSB: Workshop on Computational Systems Biology (TICSP), Tampere International Center for Signal Processing.","ieee":"T. A. Henzinger and M. Mateescu, “Tail approximation for the chemical master equation,” presented at the WCSB: Workshop on Computational Systems Biology (TICSP), 2011.","chicago":"Henzinger, Thomas A, and Maria Mateescu. “Tail Approximation for the Chemical Master Equation.” Tampere International Center for Signal Processing, 2011.","mla":"Henzinger, Thomas A., and Maria Mateescu. <i>Tail Approximation for the Chemical Master Equation</i>. Tampere International Center for Signal Processing, 2011.","short":"T.A. Henzinger, M. Mateescu, in:, Tampere International Center for Signal Processing, 2011.","ista":"Henzinger TA, Mateescu M. 2011. Tail approximation for the chemical master equation. WCSB: Workshop on Computational Systems Biology (TICSP)."},"year":"2011","date_updated":"2021-01-12T07:42:30Z","type":"conference","date_published":"2011-01-01T00:00:00Z","day":"01","oa":1,"publist_id":"3339","abstract":[{"text":"The chemical master equation is a differential equation describing the time evolution of the probability distribution over the possible “states” of a biochemical system. The solution of this equation is of interest within the systems biology field ever since the importance of the molec- ular noise has been acknowledged. Unfortunately, most of the systems do not have analytical solutions, and numerical solutions suffer from the course of dimensionality and therefore need to be approximated. Here, we introduce the concept of tail approximation, which retrieves an approximation of the probabilities in the tail of a distribution from the total probability of the tail and its conditional expectation. This approximation method can then be used to numerically compute the solution of the chemical master equation on a subset of the state space, thus fighting the explosion of the state space, for which this problem is renowned.","lang":"eng"}],"file":[{"date_created":"2018-12-12T10:18:12Z","file_size":240820,"checksum":"aa4d7a832a5419e6c0090650ebff2b9a","date_updated":"2020-07-14T12:46:06Z","content_type":"application/pdf","file_name":"IST-2012-91-v1+1_Tail_approximation_for_the_chemical_master_equation.pdf","relation":"main_file","access_level":"open_access","file_id":"5331","creator":"system"}],"ddc":["005","570"],"status":"public","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","has_accepted_license":"1","_id":"3301","author":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Mateescu, Maria","first_name":"Maria","last_name":"Mateescu"}],"date_created":"2018-12-11T12:02:33Z","department":[{"_id":"ToHe"}],"oa_version":"Submitted Version","publication_status":"published","title":"Tail approximation for the chemical master equation","pubrep_id":"91","month":"01","quality_controlled":"1","file_date_updated":"2020-07-14T12:46:06Z","language":[{"iso":"eng"}],"publisher":"Tampere International Center for Signal Processing","conference":{"name":"WCSB: Workshop on Computational Systems Biology (TICSP)"}},{"oa":1,"publist_id":"3338","abstract":[{"lang":"eng","text":"Cloud computing aims to give users virtually unlimited pay-per-use computing resources without the burden of managing the underlying infrastructure. We present a new job execution environment Flextic that exploits scal- able static scheduling techniques to provide the user with a flexible pricing model, such as a tradeoff between dif- ferent degrees of execution speed and execution price, and at the same time, reduce scheduling overhead for the cloud provider. We have evaluated a prototype of Flextic on Amazon EC2 and compared it against Hadoop. For various data parallel jobs from machine learning, im- age processing, and gene sequencing that we considered, Flextic has low scheduling overhead and reduces job du- ration by up to 15% compared to Hadoop, a dynamic cloud scheduler."}],"day":"14","type":"conference","date_published":"2011-06-14T00:00:00Z","citation":{"apa":"Henzinger, T. A., Singh, A., Singh, V., Wies, T., &#38; Zufferey, D. (2011). Static scheduling in clouds (pp. 1–6). Presented at the HotCloud: Workshop on Hot Topics in Cloud Computing, USENIX.","ama":"Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. Static scheduling in clouds. In: USENIX; 2011:1-6.","ieee":"T. A. Henzinger, A. Singh, V. Singh, T. Wies, and D. Zufferey, “Static scheduling in clouds,” presented at the HotCloud: Workshop on Hot Topics in Cloud Computing, 2011, pp. 1–6.","chicago":"Henzinger, Thomas A, Anmol Singh, Vasu Singh, Thomas Wies, and Damien Zufferey. “Static Scheduling in Clouds,” 1–6. USENIX, 2011.","short":"T.A. Henzinger, A. Singh, V. Singh, T. Wies, D. Zufferey, in:, USENIX, 2011, pp. 1–6.","mla":"Henzinger, Thomas A., et al. <i>Static Scheduling in Clouds</i>. USENIX, 2011, pp. 1–6.","ista":"Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. 2011. Static scheduling in clouds. HotCloud: Workshop on Hot Topics in Cloud Computing, 1–6."},"year":"2011","date_updated":"2021-01-12T07:42:31Z","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000","005"],"file":[{"checksum":"21a461ac004bb535c83320fe79b30375","file_size":232770,"date_created":"2018-12-12T10:18:14Z","file_name":"IST-2012-90-v1+1_Static_scheduling_in_clouds.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:46:06Z","access_level":"open_access","relation":"main_file","creator":"system","file_id":"5333"}],"pubrep_id":"90","title":"Static scheduling in clouds","month":"06","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T12:02:33Z","oa_version":"Submitted Version","publication_status":"published","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"},{"id":"72A86902-E99F-11E9-9F62-915534D1B916","full_name":"Singh, Anmol","first_name":"Anmol","last_name":"Singh"},{"first_name":"Vasu","last_name":"Singh","full_name":"Singh, Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Wies, Thomas","last_name":"Wies","first_name":"Thomas","id":"447BFB88-F248-11E8-B48F-1D18A9856A87"},{"id":"4397AC76-F248-11E8-B48F-1D18A9856A87","last_name":"Zufferey","first_name":"Damien","full_name":"Zufferey, Damien","orcid":"0000-0002-3197-8736"}],"has_accepted_license":"1","_id":"3302","conference":{"end_date":"2011-06-15","name":"HotCloud: Workshop on Hot Topics in Cloud Computing","start_date":"2011-06-14"},"publisher":"USENIX","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:46:06Z","quality_controlled":"1","page":"1 - 6"},{"pubrep_id":"506","title":"Timed parity games: Complexity and robustness","intvolume":"         7","publication_status":"published","date_created":"2018-12-11T12:02:37Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"last_name":"Prabhu","first_name":"Vinayak","full_name":"Prabhu, Vinayak"}],"issue":"4","_id":"3315","license":"https://creativecommons.org/licenses/by-nd/4.0/","scopus_import":1,"publisher":"International Federation of Computational Logic","file_date_updated":"2020-07-14T12:46:07Z","quality_controlled":"1","ec_funded":1,"abstract":[{"text":"We consider two-player games played in real time on game structures with clocks where the objectives of players are described using parity conditions. The games are concurrent in that at each turn, both players independently propose a time delay and an action, and the action with the shorter delay is chosen. To prevent a player from winning by blocking time, we restrict each player to play strategies that ensure that the player cannot be responsible for causing a zeno run. First, we present an efficient reduction of these games to turn-based (i.e., not concurrent) finite-state (i.e., untimed) parity games. Our reduction improves the best known complexity for solving timed parity games. Moreover, the rich class of algorithms for classical parity games can now be applied to timed parity games. The states of the resulting game are based on clock regions of the original game, and the state space of the finite game is linear in the size of the region graph. Second, we consider two restricted classes of strategies for the player that represents the controller in a real-time synthesis problem, namely, limit-robust and bounded-robust winning strategies. Using a limit-robust winning strategy, the controller cannot choose an exact real-valued time delay but must allow for some nonzero jitter in each of its actions. If there is a given lower bound on the jitter, then the strategy is bounded-robust winning. We show that exact strategies are more powerful than limit-robust strategies, which are more powerful than bounded-robust winning strategies for any bound. For both kinds of robust strategies, we present efficient reductions to standard timed automaton games. These reductions provide algorithms for the synthesis of robust real-time controllers.","lang":"eng"}],"doi":"10.2168/LMCS-7(4:8)2011","day":"14","date_updated":"2023-02-23T11:46:35Z","citation":{"ista":"Chatterjee K, Henzinger TA, Prabhu V. 2011. Timed parity games: Complexity and robustness. Logical Methods in Computer Science. 7(4).","mla":"Chatterjee, Krishnendu, et al. “Timed Parity Games: Complexity and Robustness.” <i>Logical Methods in Computer Science</i>, vol. 7, no. 4, International Federation of Computational Logic, 2011, doi:<a href=\"https://doi.org/10.2168/LMCS-7(4:8)2011\">10.2168/LMCS-7(4:8)2011</a>.","short":"K. Chatterjee, T.A. Henzinger, V. Prabhu, Logical Methods in Computer Science 7 (2011).","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Vinayak Prabhu. “Timed Parity Games: Complexity and Robustness.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2011. <a href=\"https://doi.org/10.2168/LMCS-7(4:8)2011\">https://doi.org/10.2168/LMCS-7(4:8)2011</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and V. Prabhu, “Timed parity games: Complexity and robustness,” <i>Logical Methods in Computer Science</i>, vol. 7, no. 4. International Federation of Computational Logic, 2011.","ama":"Chatterjee K, Henzinger TA, Prabhu V. Timed parity games: Complexity and robustness. <i>Logical Methods in Computer Science</i>. 2011;7(4). doi:<a href=\"https://doi.org/10.2168/LMCS-7(4:8)2011\">10.2168/LMCS-7(4:8)2011</a>","apa":"Chatterjee, K., Henzinger, T. A., &#38; Prabhu, V. (2011). Timed parity games: Complexity and robustness. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.2168/LMCS-7(4:8)2011\">https://doi.org/10.2168/LMCS-7(4:8)2011</a>"},"year":"2011","ddc":["000","005"],"volume":7,"month":"12","oa_version":"Published Version","project":[{"name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543","call_identifier":"FP7","_id":"25EFB36C-B435-11E9-9278-68D0E5697425"}],"publication":"Logical Methods in Computer Science","has_accepted_license":"1","language":[{"iso":"eng"}],"oa":1,"publist_id":"3324","date_published":"2011-12-14T00:00:00Z","type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)"},"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"3876"}]},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","status":"public","file":[{"checksum":"3480e1594bbef25ff7462fa93a8a814e","file_size":588863,"date_created":"2018-12-12T10:16:42Z","file_name":"IST-2016-86-v2+1_1011.0688_3_.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:46:07Z","relation":"main_file","access_level":"open_access","creator":"system","file_id":"5231"}]},{"ec_funded":1,"quality_controlled":"1","page":"176 - 185","publisher":"IEEE","author":[{"full_name":"Bloem, Roderick","last_name":"Bloem","first_name":"Roderick"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Greimel, Karin","first_name":"Karin","last_name":"Greimel"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jobstmann, Barbara","last_name":"Jobstmann","first_name":"Barbara"}],"scopus_import":1,"_id":"3316","title":"Specification-centered robustness","article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_created":"2018-12-11T12:02:38Z","publication_status":"published","year":"2011","citation":{"mla":"Bloem, Roderick, et al. “Specification-Centered Robustness.” <i>6th IEEE International Symposium on Industrial and Embedded Systems</i>, IEEE, 2011, pp. 176–85, doi:<a href=\"https://doi.org/10.1109/SIES.2011.5953660\">10.1109/SIES.2011.5953660</a>.","short":"R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, B. Jobstmann, in:, 6th IEEE International Symposium on Industrial and Embedded Systems, IEEE, 2011, pp. 176–185.","ista":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. 2011. Specification-centered robustness. 6th IEEE International Symposium on Industrial and Embedded Systems.  SIES: International Symposium on Industrial Embedded Systems, 176–185.","ama":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. Specification-centered robustness. In: <i>6th IEEE International Symposium on Industrial and Embedded Systems</i>. IEEE; 2011:176-185. doi:<a href=\"https://doi.org/10.1109/SIES.2011.5953660\">10.1109/SIES.2011.5953660</a>","apa":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., &#38; Jobstmann, B. (2011). Specification-centered robustness. In <i>6th IEEE International Symposium on Industrial and Embedded Systems</i> (pp. 176–185). Vasteras, Sweden: IEEE. <a href=\"https://doi.org/10.1109/SIES.2011.5953660\">https://doi.org/10.1109/SIES.2011.5953660</a>","chicago":"Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger, and Barbara Jobstmann. “Specification-Centered Robustness.” In <i>6th IEEE International Symposium on Industrial and Embedded Systems</i>, 176–85. IEEE, 2011. <a href=\"https://doi.org/10.1109/SIES.2011.5953660\">https://doi.org/10.1109/SIES.2011.5953660</a>.","ieee":"R. Bloem, K. Chatterjee, K. Greimel, T. A. Henzinger, and B. Jobstmann, “Specification-centered robustness,” in <i>6th IEEE International Symposium on Industrial and Embedded Systems</i>, Vasteras, Sweden, 2011, pp. 176–185."},"date_updated":"2021-01-12T07:42:36Z","abstract":[{"lang":"eng","text":"In addition to being correct, a system should be robust, that is, it should behave reasonably even after receiving unexpected inputs. In this paper, we summarize two formal notions of robustness that we have introduced previously for reactive systems. One of the notions is based on assigning costs for failures on a user-provided notion of incorrect transitions in a specification. Here, we define a system to be robust if a finite number of incorrect inputs does not lead to an infinite number of incorrect outputs. We also give a more refined notion of robustness that aims to minimize the ratio of output failures to input failures. The second notion is aimed at liveness. In contrast to the previous notion, it has no concept of recovery from an error. Instead, it compares the ratio of the number of liveness constraints that the system violates to the number of liveness constraints that the environment violates."}],"day":"14","doi":"10.1109/SIES.2011.5953660","language":[{"iso":"eng"}],"conference":{"end_date":"2011-06-17","location":"Vasteras, Sweden","start_date":"2011-06-15","name":" SIES: International Symposium on Industrial Embedded Systems"},"publication":"6th IEEE International Symposium on Industrial and Embedded Systems","month":"07","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S11402-N23"},{"name":"Design for Embedded Systems","grant_number":"214373","_id":"25F1337C-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","main_file_link":[{"url":"https://openlib.tugraz.at/download.php?id=5cb57c8a49344&location=browse","open_access":"1"}],"type":"conference","date_published":"2011-07-14T00:00:00Z","oa":1,"publist_id":"3323"},{"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","status":"public","related_material":{"record":[{"status":"public","id":"5383","relation":"earlier_version"}]},"volume":6803,"date_published":"2011-07-19T00:00:00Z","type":"conference","date_updated":"2023-02-23T12:23:48Z","year":"2011","citation":{"short":"T. Wies, M. Muñiz, V. Kuncak, in:, Springer, 2011, pp. 476–491.","mla":"Wies, Thomas, et al. <i>An Efficient Decision Procedure for Imperative Tree Data Structures</i>. Vol. 6803, Springer, 2011, pp. 476–91, doi:<a href=\"https://doi.org/10.1007/978-3-642-22438-6_36\">10.1007/978-3-642-22438-6_36</a>.","ista":"Wies T, Muñiz M, Kuncak V. 2011. An efficient decision procedure for imperative tree data structures. CADE 23: Automated Deduction , LNAI , vol. 6803, 476–491.","ama":"Wies T, Muñiz M, Kuncak V. An efficient decision procedure for imperative tree data structures. In: Vol 6803. Springer; 2011:476-491. doi:<a href=\"https://doi.org/10.1007/978-3-642-22438-6_36\">10.1007/978-3-642-22438-6_36</a>","apa":"Wies, T., Muñiz, M., &#38; Kuncak, V. (2011). An efficient decision procedure for imperative tree data structures (Vol. 6803, pp. 476–491). Presented at the CADE 23: Automated Deduction , Wrocław, Poland: Springer. <a href=\"https://doi.org/10.1007/978-3-642-22438-6_36\">https://doi.org/10.1007/978-3-642-22438-6_36</a>","ieee":"T. Wies, M. Muñiz, and V. Kuncak, “An efficient decision procedure for imperative tree data structures,” presented at the CADE 23: Automated Deduction , Wrocław, Poland, 2011, vol. 6803, pp. 476–491.","chicago":"Wies, Thomas, Marco Muñiz, and Viktor Kuncak. “An Efficient Decision Procedure for Imperative Tree Data Structures,” 6803:476–91. Springer, 2011. <a href=\"https://doi.org/10.1007/978-3-642-22438-6_36\">https://doi.org/10.1007/978-3-642-22438-6_36</a>."},"abstract":[{"text":"We present a new decidable logic called TREX for expressing constraints about imperative tree data structures. In particular, TREX supports a transitive closure operator that can express reachability constraints, which often appear in data structure invariants. We show that our logic is closed under weakest precondition computation, which enables its use for automated software verification. We further show that satisfiability of formulas in TREX is decidable in NP. The low complexity makes it an attractive alternative to more expensive logics such as monadic second-order logic (MSOL) over trees, which have been traditionally used for reasoning about tree data structures.","lang":"eng"}],"publist_id":"3312","doi":"10.1007/978-3-642-22438-6_36","day":"19","language":[{"iso":"eng"}],"page":"476 - 491","quality_controlled":"1","conference":{"start_date":"2011-07-31","name":"CADE 23: Automated Deduction ","end_date":"2011-08-05","location":"Wrocław, Poland"},"publisher":"Springer","author":[{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","last_name":"Wies","full_name":"Wies, Thomas"},{"last_name":"Muñiz","first_name":"Marco","full_name":"Muñiz, Marco"},{"full_name":"Kuncak, Viktor","first_name":"Viktor","last_name":"Kuncak"}],"_id":"3323","scopus_import":1,"title":"An efficient decision procedure for imperative tree data structures","month":"07","alternative_title":["LNAI "],"intvolume":"      6803","oa_version":"None","publication_status":"published","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T12:02:40Z"},{"author":[{"last_name":"Piskac","first_name":"Ruzica","full_name":"Piskac, Ruzica"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","last_name":"Wies","first_name":"Thomas","full_name":"Wies, Thomas"}],"scopus_import":1,"_id":"3324","intvolume":"      6538","alternative_title":["LNCS"],"title":"Decision procedures for automating termination proofs","date_created":"2018-12-11T12:02:40Z","department":[{"_id":"ToHe"}],"publication_status":"published","quality_controlled":"1","page":"371 - 386","editor":[{"full_name":"Jhala, Ranjit","last_name":"Jhala","first_name":"Ranjit"},{"full_name":"Schmidt, David","last_name":"Schmidt","first_name":"David"}],"publisher":"Springer","citation":{"mla":"Piskac, Ruzica, and Thomas Wies. <i>Decision Procedures for Automating Termination Proofs</i>. Edited by Ranjit Jhala and David Schmidt, vol. 6538, Springer, 2011, pp. 371–86, doi:<a href=\"https://doi.org/10.1007/978-3-642-18275-4_26\">10.1007/978-3-642-18275-4_26</a>.","short":"R. Piskac, T. Wies, in:, R. Jhala, D. Schmidt (Eds.), Springer, 2011, pp. 371–386.","ista":"Piskac R, Wies T. 2011. Decision procedures for automating termination proofs. VMCAI: Verification Model Checking and Abstract Interpretation, LNCS, vol. 6538, 371–386.","apa":"Piskac, R., &#38; Wies, T. (2011). Decision procedures for automating termination proofs. In R. Jhala &#38; D. Schmidt (Eds.) (Vol. 6538, pp. 371–386). Presented at the VMCAI: Verification Model Checking and Abstract Interpretation, Texas, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-642-18275-4_26\">https://doi.org/10.1007/978-3-642-18275-4_26</a>","ama":"Piskac R, Wies T. Decision procedures for automating termination proofs. In: Jhala R, Schmidt D, eds. Vol 6538. Springer; 2011:371-386. doi:<a href=\"https://doi.org/10.1007/978-3-642-18275-4_26\">10.1007/978-3-642-18275-4_26</a>","chicago":"Piskac, Ruzica, and Thomas Wies. “Decision Procedures for Automating Termination Proofs.” edited by Ranjit Jhala and David Schmidt, 6538:371–86. Springer, 2011. <a href=\"https://doi.org/10.1007/978-3-642-18275-4_26\">https://doi.org/10.1007/978-3-642-18275-4_26</a>.","ieee":"R. Piskac and T. Wies, “Decision procedures for automating termination proofs,” presented at the VMCAI: Verification Model Checking and Abstract Interpretation, Texas, USA, 2011, vol. 6538, pp. 371–386."},"year":"2011","date_updated":"2021-01-12T07:42:39Z","abstract":[{"text":"Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current tools has been on developing sophisticated techniques for constructing the abstractions while relying on known decidable logics (such as linear arithmetic) to express them. We believe we can significantly increase the class of programs that are amenable to automated termination proofs by identifying more expressive decidable logics for reasoning about well-founded relations. We therefore present a new decision procedure for reasoning about multiset orderings, which are among the most powerful orderings used to prove termination. We show that, using our decision procedure, one can automatically prove termination of natural abstractions of programs.","lang":"eng"}],"day":"01","doi":"10.1007/978-3-642-18275-4_26","volume":6538,"month":"01","oa_version":"Submitted Version","language":[{"iso":"eng"}],"conference":{"name":"VMCAI: Verification Model Checking and Abstract Interpretation","start_date":"2011-01-23","location":"Texas, USA","end_date":"2011-01-25"},"type":"conference","date_published":"2011-01-01T00:00:00Z","oa":1,"publist_id":"3311","status":"public","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"url":"https://infoscience.epfl.ch/record/170697/","open_access":"1"}]},{"volume":46,"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"short":"R. Alur, P. Cerny, in:, ACM, 2011, pp. 599–610.","mla":"Alur, Rajeev, and Pavol Cerny. <i>Streaming Transducers for Algorithmic Verification of Single Pass List Processing Programs</i>. Vol. 46, no. 1, ACM, 2011, pp. 599–610, doi:<a href=\"https://doi.org/10.1145/1926385.1926454\">10.1145/1926385.1926454</a>.","ista":"Alur R, Cerny P. 2011. Streaming transducers for algorithmic verification of single pass list processing programs. POPL: Principles of Programming Languages vol. 46, 599–610.","ama":"Alur R, Cerny P. Streaming transducers for algorithmic verification of single pass list processing programs. In: Vol 46. ACM; 2011:599-610. doi:<a href=\"https://doi.org/10.1145/1926385.1926454\">10.1145/1926385.1926454</a>","apa":"Alur, R., &#38; Cerny, P. (2011). Streaming transducers for algorithmic verification of single pass list processing programs (Vol. 46, pp. 599–610). Presented at the POPL: Principles of Programming Languages, Texas, USA: ACM. <a href=\"https://doi.org/10.1145/1926385.1926454\">https://doi.org/10.1145/1926385.1926454</a>","ieee":"R. Alur and P. Cerny, “Streaming transducers for algorithmic verification of single pass list processing programs,” presented at the POPL: Principles of Programming Languages, Texas, USA, 2011, vol. 46, no. 1, pp. 599–610.","chicago":"Alur, Rajeev, and Pavol Cerny. “Streaming Transducers for Algorithmic Verification of Single Pass List Processing Programs,” 46:599–610. ACM, 2011. <a href=\"https://doi.org/10.1145/1926385.1926454\">https://doi.org/10.1145/1926385.1926454</a>."},"year":"2011","date_updated":"2022-03-21T08:12:51Z","type":"conference","date_published":"2011-01-26T00:00:00Z","day":"26","doi":"10.1145/1926385.1926454","publist_id":"3310","abstract":[{"lang":"eng","text":"We introduce streaming data string transducers that map input data strings to output data strings in a single left-to-right pass in linear time. Data strings are (unbounded) sequences of data values, tagged with symbols from a finite set, over a potentially infinite data do- main that supports only the operations of equality and ordering. The transducer uses a finite set of states, a finite set of variables ranging over the data domain, and a finite set of variables ranging over data strings. At every step, it can make decisions based on the next in- put symbol, updating its state, remembering the input data value in its data variables, and updating data-string variables by concatenat- ing data-string variables and new symbols formed from data vari- ables, while avoiding duplication. We establish that the problems of checking functional equivalence of two streaming transducers, and of checking whether a streaming transducer satisfies pre/post verification conditions specified by streaming acceptors over in- put/output data-strings, are in PSPACE. We identify a class of imperative and a class of functional pro- grams, manipulating lists of data items, which can be effectively translated to streaming data-string transducers. The imperative pro- grams dynamically modify a singly-linked heap by changing next- pointers of heap-nodes and by adding new nodes. The main re- striction specifies how the next-pointers can be used for traversal. We also identify an expressively equivalent fragment of functional programs that traverse a list using syntactically restricted recursive calls. Our results lead to algorithms for assertion checking and for checking functional equivalence of two programs, written possibly in different programming styles, for commonly used routines such as insert, delete, and reverse."}],"quality_controlled":"1","page":"599 - 610","language":[{"iso":"eng"}],"publisher":"ACM","conference":{"start_date":"2011-01-26","name":"POPL: Principles of Programming Languages","end_date":"2011-01-28","location":"Texas, USA"},"scopus_import":"1","_id":"3325","issue":"1","author":[{"first_name":"Rajeev","last_name":"Alur","full_name":"Alur, Rajeev"},{"id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","last_name":"Cerny","first_name":"Pavol","full_name":"Cerny, Pavol"}],"department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2018-12-11T12:02:41Z","publication_status":"published","oa_version":"None","intvolume":"        46","title":"Streaming transducers for algorithmic verification of single pass list processing programs","month":"01"}]