[{"author":[{"id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","last_name":"Dragoi","first_name":"Cezara","full_name":"Dragoi, Cezara"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"full_name":"Zufferey, Damien","first_name":"Damien","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3197-8736"}],"oa":1,"_id":"1439","date_published":"2016-01-11T00:00:00Z","language":[{"iso":"eng"}],"doi":"10.1145/2837614.2837650","publisher":"ACM","year":"2016","type":"conference","month":"01","quality_controlled":"1","publist_id":"5759","volume":"20-22","date_created":"2018-12-11T11:52:01Z","department":[{"_id":"ToHe"}],"acknowledgement":"Damien Zufferey was supported by DARPA (Grants FA8650-11-C-7192 and FA8650-15-C-7564) and NSF (Grant CCF-1138967). ","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2016-01-20","end_date":"2016-01-22","name":"POPL: Principles of Programming Languages","location":"St. Petersburg, FL, USA"},"page":"400 - 415","oa_version":"Preprint","publication_status":"published","day":"11","ec_funded":1,"abstract":[{"text":"Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. We introduce PSYNC, a domain specific language based on the Heard-Of model, which views asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages. We define a runtime system for PSYNC that efficiently executes on asynchronous networks. We formalize the relation between the runtime system and PSYNC in terms of observational refinement. The high-level lockstep abstraction introduced by PSYNC simplifies the design and implementation of fault-tolerant distributed algorithms and enables automated formal verification. We have implemented an embedding of PSYNC in the SCALA programming language with a runtime system for asynchronous networks. We show the applicability of PSYNC by implementing several important fault-tolerant distributed algorithms and we compare the implementation of consensus algorithms in PSYNC against implementations in other languages in terms of code size, runtime efficiency, and verification.","lang":"eng"}],"date_updated":"2021-01-12T06:50:45Z","status":"public","main_file_link":[{"url":"https://hal.inria.fr/hal-01251199/","open_access":"1"}],"title":"PSYNC: A partially synchronous language for fault-tolerant distributed algorithms","project":[{"grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"}],"citation":{"ama":"Dragoi C, Henzinger TA, Zufferey D. PSYNC: A partially synchronous language for fault-tolerant distributed algorithms. In: Vol 20-22. ACM; 2016:400-415. doi:<a href=\"https://doi.org/10.1145/2837614.2837650\">10.1145/2837614.2837650</a>","mla":"Dragoi, Cezara, et al. <i>PSYNC: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms</i>. Vol. 20–22, ACM, 2016, pp. 400–15, doi:<a href=\"https://doi.org/10.1145/2837614.2837650\">10.1145/2837614.2837650</a>.","ista":"Dragoi C, Henzinger TA, Zufferey D. 2016. PSYNC: A partially synchronous language for fault-tolerant distributed algorithms. POPL: Principles of Programming Languages, ACM SIGPLAN Notices, vol. 20–22, 400–415.","apa":"Dragoi, C., Henzinger, T. A., &#38; Zufferey, D. (2016). PSYNC: A partially synchronous language for fault-tolerant distributed algorithms (Vol. 20–22, pp. 400–415). Presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA: ACM. <a href=\"https://doi.org/10.1145/2837614.2837650\">https://doi.org/10.1145/2837614.2837650</a>","short":"C. Dragoi, T.A. Henzinger, D. Zufferey, in:, ACM, 2016, pp. 400–415.","ieee":"C. Dragoi, T. A. Henzinger, and D. Zufferey, “PSYNC: A partially synchronous language for fault-tolerant distributed algorithms,” presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA, 2016, vol. 20–22, pp. 400–415.","chicago":"Dragoi, Cezara, Thomas A Henzinger, and Damien Zufferey. “PSYNC: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms,” 20–22:400–415. ACM, 2016. <a href=\"https://doi.org/10.1145/2837614.2837650\">https://doi.org/10.1145/2837614.2837650</a>."},"scopus_import":1,"alternative_title":["ACM SIGPLAN Notices"]},{"file":[{"file_size":489362,"file_name":"IST-2016-499-v1+1_9.pdf","date_updated":"2020-07-14T12:44:58Z","checksum":"cf5e94baa89a2dc4c5de01abc676eda8","date_created":"2018-12-12T10:14:02Z","file_id":"5050","creator":"system","relation":"main_file","content_type":"application/pdf","access_level":"open_access"}],"title":"The need for language support for fault-tolerant distributed systems","series_title":"Leibniz International Proceedings in Informatics","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989"},{"name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211"}],"citation":{"chicago":"Dragoi, Cezara, Thomas A Henzinger, and Damien Zufferey. “The Need for Language Support for Fault-Tolerant Distributed Systems.” Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. <a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">https://doi.org/10.4230/LIPIcs.SNAPL.2015.90</a>.","ieee":"C. Dragoi, T. A. Henzinger, and D. Zufferey, “The need for language support for fault-tolerant distributed systems,” vol. 32. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 90–102, 2015.","short":"C. Dragoi, T.A. Henzinger, D. Zufferey, 32 (2015) 90–102.","apa":"Dragoi, C., Henzinger, T. A., &#38; Zufferey, D. (2015). The need for language support for fault-tolerant distributed systems. Presented at the SNAPL: Summit oN Advances in Programming Languages, Asilomar, CA, United States: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">https://doi.org/10.4230/LIPIcs.SNAPL.2015.90</a>","mla":"Dragoi, Cezara, et al. <i>The Need for Language Support for Fault-Tolerant Distributed Systems</i>. Vol. 32, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 90–102, doi:<a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">10.4230/LIPIcs.SNAPL.2015.90</a>.","ista":"Dragoi C, Henzinger TA, Zufferey D. 2015. The need for language support for fault-tolerant distributed systems. 32, 90–102.","ama":"Dragoi C, Henzinger TA, Zufferey D. The need for language support for fault-tolerant distributed systems. 2015;32:90-102. doi:<a href=\"https://doi.org/10.4230/LIPIcs.SNAPL.2015.90\">10.4230/LIPIcs.SNAPL.2015.90</a>"},"pubrep_id":"499","alternative_title":["LIPIcs"],"has_accepted_license":"1","scopus_import":1,"ec_funded":1,"abstract":[{"lang":"eng","text":"Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. Nonetheless there is surprisingly little language and verification support to build distributed systems based on fault-tolerant algorithms. In this paper, we present some of the challenges that a designer has to overcome to implement a fault-tolerant distributed system. Then we review different models that have been proposed to reason about distributed algorithms and sketch how such a model can form the basis for a domain-specific programming language. Adopting a high-level programming model can simplify the programmer's life and make the code amenable to automated verification, while still compiling to efficiently executable code. We conclude by summarizing the current status of an ongoing language design and implementation project that is based on this idea."}],"oa_version":"Published Version","publication_status":"published","page":"90 - 102","day":"01","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"date_updated":"2020-08-11T10:09:14Z","status":"public","quality_controlled":"1","publication_identifier":{"isbn":["978-3-939897-80-4 "]},"publist_id":"5681","month":"01","volume":32,"department":[{"_id":"ToHe"}],"date_created":"2018-12-11T11:52:22Z","intvolume":"        32","ddc":["005"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2020-07-14T12:44:58Z","conference":{"name":"SNAPL: Summit oN Advances in Programming Languages","end_date":"2015-05-06","start_date":"2015-05-03","location":"Asilomar, CA, United States"},"oa":1,"_id":"1498","author":[{"id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","last_name":"Dragoi","first_name":"Cezara","full_name":"Dragoi, Cezara"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"first_name":"Damien","full_name":"Zufferey, Damien","orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","last_name":"Zufferey"}],"date_published":"2015-01-01T00:00:00Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","year":"2015","language":[{"iso":"eng"}],"doi":"10.4230/LIPIcs.SNAPL.2015.90","type":"conference"},{"acknowledgement":"Supported by the Vienna Science and Technology Fund (WWTF) through grant PROSEED.","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T11:51:45Z","intvolume":"      8318","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000","005"],"conference":{"location":"San Diego, USA","start_date":"2014-01-19","end_date":"2014-01-21","name":"VMCAI: Verification, Model Checking and Abstract Interpretation"},"file_date_updated":"2020-07-14T12:44:48Z","quality_controlled":"1","publist_id":"5817","month":"01","volume":8318,"publisher":"Springer","year":"2014","language":[{"iso":"eng"}],"doi":"10.1007/978-3-642-54013-4_10","type":"conference","oa":1,"_id":"1392","author":[{"full_name":"Dragoi, Cezara","first_name":"Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","last_name":"Dragoi"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"first_name":"Helmut","full_name":"Veith, Helmut","last_name":"Veith"},{"first_name":"Josef","full_name":"Widder, Josef","last_name":"Widder"},{"full_name":"Zufferey, Damien","first_name":"Damien","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3197-8736"}],"date_published":"2014-01-01T00:00:00Z","project":[{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"citation":{"chicago":"Dragoi, Cezara, Thomas A Henzinger, Helmut Veith, Josef Widder, and Damien Zufferey. “A Logic-Based Framework for Verifying Consensus Algorithms,” 8318:161–81. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-642-54013-4_10\">https://doi.org/10.1007/978-3-642-54013-4_10</a>.","ieee":"C. Dragoi, T. A. Henzinger, H. Veith, J. Widder, and D. Zufferey, “A logic-based framework for verifying consensus algorithms,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, San Diego, USA, 2014, vol. 8318, pp. 161–181.","apa":"Dragoi, C., Henzinger, T. A., Veith, H., Widder, J., &#38; Zufferey, D. (2014). A logic-based framework for verifying consensus algorithms (Vol. 8318, pp. 161–181). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, San Diego, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-642-54013-4_10\">https://doi.org/10.1007/978-3-642-54013-4_10</a>","ista":"Dragoi C, Henzinger TA, Veith H, Widder J, Zufferey D. 2014. A logic-based framework for verifying consensus algorithms. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 8318, 161–181.","short":"C. Dragoi, T.A. Henzinger, H. Veith, J. Widder, D. Zufferey, in:, Springer, 2014, pp. 161–181.","mla":"Dragoi, Cezara, et al. <i>A Logic-Based Framework for Verifying Consensus Algorithms</i>. Vol. 8318, Springer, 2014, pp. 161–81, doi:<a href=\"https://doi.org/10.1007/978-3-642-54013-4_10\">10.1007/978-3-642-54013-4_10</a>.","ama":"Dragoi C, Henzinger TA, Veith H, Widder J, Zufferey D. A logic-based framework for verifying consensus algorithms. In: Vol 8318. Springer; 2014:161-181. doi:<a href=\"https://doi.org/10.1007/978-3-642-54013-4_10\">10.1007/978-3-642-54013-4_10</a>"},"pubrep_id":"179","alternative_title":["LNCS"],"has_accepted_license":"1","scopus_import":1,"file":[{"creator":"system","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_name":"IST-2014-179-v1+1_vmcai14.pdf","file_size":444138,"checksum":"bffa33d39be77df0da39defe97eabf84","file_id":"4859","date_created":"2018-12-12T10:11:06Z","date_updated":"2020-07-14T12:44:48Z"}],"title":"A logic-based framework for verifying consensus algorithms","date_updated":"2021-01-12T06:50:22Z","status":"public","ec_funded":1,"abstract":[{"lang":"eng","text":"Fault-tolerant distributed algorithms play an important role in ensuring the reliability of many software applications. In this paper we consider distributed algorithms whose computations are organized in rounds. To verify the correctness of such algorithms, we reason about (i) properties (such as invariants) of the state, (ii) the transitions controlled by the algorithm, and (iii) the communication graph. We introduce a logic that addresses these points, and contains set comprehensions with cardinality constraints, function symbols to describe the local states of each process, and a limited form of quantifier alternation to express the verification conditions. We show its use in automating the verification of consensus algorithms. In particular, we give a semi-decision procedure for the unsatisfiability problem of the logic and identify a decidable fragment. We successfully applied our framework to verify the correctness of a variety of consensus algorithms tolerant to both benign faults (message loss, process crashes) and value faults (message corruption)."}],"oa_version":"Submitted Version","publication_status":"published","page":"161 - 181","day":"01"},{"department":[{"_id":"ToHe"}],"date_created":"2018-12-11T11:57:43Z","intvolume":"      8044","file_date_updated":"2020-07-14T12:45:41Z","conference":{"location":"St. Petersburg, Russia","start_date":"2013-07-13","end_date":"2013-07-19","name":"CAV: Computer Aided Verification"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"article_processing_charge":"No","publist_id":"4456","quality_controlled":"1","month":"07","volume":8044,"year":"2013","publisher":"Springer","doi":"10.1007/978-3-642-39799-8_54","language":[{"iso":"eng"}],"type":"conference","_id":"2447","oa":1,"author":[{"full_name":"Piskac, Ruzica","first_name":"Ruzica","last_name":"Piskac"},{"last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Wies, Thomas","first_name":"Thomas"},{"orcid":"0000-0002-3197-8736","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","first_name":"Damien","full_name":"Zufferey, Damien"}],"date_published":"2013-07-01T00:00:00Z","citation":{"ieee":"R. Piskac, T. Wies, and D. Zufferey, “Automating separation logic using SMT,” vol. 8044. Springer, pp. 773–789, 2013.","chicago":"Piskac, Ruzica, Thomas Wies, and Damien Zufferey. “Automating Separation Logic Using SMT.” Lecture Notes in Computer Science. Springer, 2013. <a href=\"https://doi.org/10.1007/978-3-642-39799-8_54\">https://doi.org/10.1007/978-3-642-39799-8_54</a>.","ama":"Piskac R, Wies T, Zufferey D. Automating separation logic using SMT. 2013;8044:773-789. doi:<a href=\"https://doi.org/10.1007/978-3-642-39799-8_54\">10.1007/978-3-642-39799-8_54</a>","apa":"Piskac, R., Wies, T., &#38; Zufferey, D. (2013). Automating separation logic using SMT. Presented at the CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. <a href=\"https://doi.org/10.1007/978-3-642-39799-8_54\">https://doi.org/10.1007/978-3-642-39799-8_54</a>","ista":"Piskac R, Wies T, Zufferey D. 2013. Automating separation logic using SMT. 8044, 773–789.","mla":"Piskac, Ruzica, et al. <i>Automating Separation Logic Using SMT</i>. Vol. 8044, Springer, 2013, pp. 773–89, doi:<a href=\"https://doi.org/10.1007/978-3-642-39799-8_54\">10.1007/978-3-642-39799-8_54</a>.","short":"R. Piskac, T. Wies, D. Zufferey, 8044 (2013) 773–789."},"has_accepted_license":"1","alternative_title":["LNCS"],"scopus_import":1,"title":"Automating separation logic using SMT","file":[{"access_level":"open_access","content_type":"application/pdf","relation":"main_file","creator":"dernst","checksum":"2e866932ab688f47ecd504acb4d5c7d4","file_id":"7859","date_created":"2020-05-15T11:13:01Z","date_updated":"2020-07-14T12:45:41Z","file_name":"2013_CAV_Piskac.pdf","file_size":309182}],"series_title":"Lecture Notes in Computer Science","date_updated":"2020-08-11T10:09:47Z","status":"public","abstract":[{"lang":"eng","text":"Separation logic (SL) has gained widespread popularity because of its ability to succinctly express complex invariants of a program’s heap configurations. Several specialized provers have been developed for decidable SL fragments. However, these provers cannot be easily extended or combined with solvers for other theories that are important in program verification, e.g., linear arithmetic. In this paper, we present a reduction of decidable SL fragments to a decidable first-order theory that fits well into the satisfiability modulo theories (SMT) framework. We show how to use this reduction to automate satisfiability, entailment, frame inference, and abduction problems for separation logic using SMT solvers. Our approach provides a simple method of integrating separation logic into existing verification tools that provide SMT backends, and an elegant way of combining SL fragments with other decidable first-order theories. We implemented this approach in a verification tool and applied it to heap-manipulating programs whose verification involves reasoning in theory combinations.\r\n"}],"day":"01","oa_version":"Submitted Version","publication_status":"published","page":"773 - 789"},{"month":"03","publist_id":"3947","quality_controlled":"1","volume":7795,"date_created":"2018-12-11T11:59:54Z","department":[{"_id":"ToHe"}],"conference":{"end_date":"2013-03-24","start_date":"2013-03-16","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Rome, Italy"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":"      7795","author":[{"last_name":"Bansal","full_name":"Bansal, Kshitij","first_name":"Kshitij"},{"last_name":"Koskinen","first_name":"Eric","full_name":"Koskinen, Eric"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","last_name":"Wies","full_name":"Wies, Thomas","first_name":"Thomas"},{"last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3197-8736","first_name":"Damien","full_name":"Zufferey, Damien"}],"_id":"2847","oa":1,"date_published":"2013-03-01T00:00:00Z","doi":"10.1007/978-3-642-36742-7_5","language":[{"iso":"eng"}],"year":"2013","publisher":"Springer","type":"conference","main_file_link":[{"open_access":"1","url":"http://arise.or.at/pubpdf/Structural_Counter_Abstraction.pdf"}],"series_title":"Lecture Notes in Computer Science","title":"Structural Counter Abstraction","related_material":{"record":[{"relation":"dissertation_contains","id":"1405","status":"public"}]},"citation":{"ista":"Bansal K, Koskinen E, Wies T, Zufferey D. 2013. Structural Counter Abstraction (eds. N. Piterman &#38; S. Smolka). 7795, 62–77.","apa":"Bansal, K., Koskinen, E., Wies, T., &#38; Zufferey, D. (2013). Structural Counter Abstraction. (N. Piterman &#38; S. Smolka, Eds.). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Rome, Italy: Springer. <a href=\"https://doi.org/10.1007/978-3-642-36742-7_5\">https://doi.org/10.1007/978-3-642-36742-7_5</a>","mla":"Bansal, Kshitij, et al. <i>Structural Counter Abstraction</i>. Edited by Nir Piterman and Scott Smolka, vol. 7795, Springer, 2013, pp. 62–77, doi:<a href=\"https://doi.org/10.1007/978-3-642-36742-7_5\">10.1007/978-3-642-36742-7_5</a>.","short":"K. Bansal, E. Koskinen, T. Wies, D. Zufferey, 7795 (2013) 62–77.","ama":"Bansal K, Koskinen E, Wies T, Zufferey D. Structural Counter Abstraction. Piterman N, Smolka S, eds. 2013;7795:62-77. doi:<a href=\"https://doi.org/10.1007/978-3-642-36742-7_5\">10.1007/978-3-642-36742-7_5</a>","chicago":"Bansal, Kshitij, Eric Koskinen, Thomas Wies, and Damien Zufferey. “Structural Counter Abstraction.” Edited by Nir Piterman and Scott Smolka. Lecture Notes in Computer Science. Springer, 2013. <a href=\"https://doi.org/10.1007/978-3-642-36742-7_5\">https://doi.org/10.1007/978-3-642-36742-7_5</a>.","ieee":"K. Bansal, E. Koskinen, T. Wies, and D. Zufferey, “Structural Counter Abstraction,” vol. 7795. Springer, pp. 62–77, 2013."},"project":[{"call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"}],"scopus_import":1,"editor":[{"last_name":"Piterman","full_name":"Piterman, Nir","first_name":"Nir"},{"last_name":"Smolka","first_name":"Scott","full_name":"Smolka, Scott"}],"alternative_title":["LNCS"],"day":"01","oa_version":"Submitted Version","page":"62 - 77","publication_status":"published","abstract":[{"lang":"eng","text":"Depth-Bounded Systems form an expressive class of well-structured transition systems. They can model a wide range of concurrent infinite-state systems including those with dynamic thread creation, dynamically changing communication topology, and complex shared heap structures. We present the first method to automatically prove fair termination of depth-bounded systems. Our method uses a numerical abstraction of the system, which we obtain by systematically augmenting an over-approximation of the system’s reachable states with a finite set of counters. This numerical abstraction can be analyzed with existing termination provers. What makes our approach unique is the way in which it exploits the well-structuredness of the analyzed system. We have implemented our work in a prototype tool and used it to automatically prove liveness properties of complex concurrent systems, including nonblocking algorithms such as Treiber’s stack and several distributed processes. Many of these examples are beyond the scope of termination analyses that are based on traditional counter abstractions."}],"ec_funded":1,"date_updated":"2023-09-07T11:36:36Z","status":"public"},{"publication":"Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation","title":"P: Safe asynchronous event-driven programming","month":"06","quality_controlled":"1","publist_id":"4626","main_file_link":[{"url":"http://research.microsoft.com/pubs/191069/pldi212_desai.pdf"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"end_date":"2013-06-19","start_date":"2013-06-16","name":"PLDI: Programming Languages Design and Implementation","location":"Seattle, WA, United States"},"scopus_import":1,"date_created":"2018-12-11T11:56:52Z","project":[{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989"}],"citation":{"chicago":"Desai, Ankush, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani, and Damien Zufferey. “P: Safe Asynchronous Event-Driven Programming.” In <i>Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>, 321–31. ACM, 2013. <a href=\"https://doi.org/10.1145/2491956.2462184\">https://doi.org/10.1145/2491956.2462184</a>.","ieee":"A. Desai, V. Gupta, E. Jackson, S. Qadeer, S. Rajamani, and D. Zufferey, “P: Safe asynchronous event-driven programming,” in <i>Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>, Seattle, WA, United States, 2013, pp. 321–331.","short":"A. Desai, V. Gupta, E. Jackson, S. Qadeer, S. Rajamani, D. Zufferey, in:, Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, 2013, pp. 321–331.","ista":"Desai A, Gupta V, Jackson E, Qadeer S, Rajamani S, Zufferey D. 2013. P: Safe asynchronous event-driven programming. Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI: Programming Languages Design and Implementation, 321–331.","mla":"Desai, Ankush, et al. “P: Safe Asynchronous Event-Driven Programming.” <i>Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>, ACM, 2013, pp. 321–31, doi:<a href=\"https://doi.org/10.1145/2491956.2462184\">10.1145/2491956.2462184</a>.","apa":"Desai, A., Gupta, V., Jackson, E., Qadeer, S., Rajamani, S., &#38; Zufferey, D. (2013). P: Safe asynchronous event-driven programming. In <i>Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation</i> (pp. 321–331). Seattle, WA, United States: ACM. <a href=\"https://doi.org/10.1145/2491956.2462184\">https://doi.org/10.1145/2491956.2462184</a>","ama":"Desai A, Gupta V, Jackson E, Qadeer S, Rajamani S, Zufferey D. P: Safe asynchronous event-driven programming. In: <i>Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>. ACM; 2013:321-331. doi:<a href=\"https://doi.org/10.1145/2491956.2462184\">10.1145/2491956.2462184</a>"},"department":[{"_id":"ToHe"}],"oa_version":"None","publication_status":"published","date_published":"2013-06-01T00:00:00Z","page":"321 - 331","day":"01","ec_funded":1,"abstract":[{"lang":"eng","text":"We describe the design and implementation of P, a domain-specific language to write asynchronous event driven code. P allows the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P unifies modeling and programming into one activity for the programmer. Not only can a P program be compiled into executable code, but it can also be tested using model checking techniques. P allows the programmer to specify the environment, used to &quot;close&quot; the system during testing, as nondeterministic ghost machines. Ghost machines are erased during compilation to executable code; a type system ensures that the erasure is semantics preserving. The P language is designed so that a P program can be checked for responsiveness-the ability to handle every event in a timely manner. By default, a machine needs to handle every event that arrives in every state. But handling every event in every state is impractical. The language provides a notion of deferred events where the programmer can annotate when she wants to delay processing an event. The default safety checker looks for presence of unhan-dled events. The language also provides default liveness checks that an event cannot be potentially deferred forever. P was used to implement and verify the core of the USB device driver stack that ships with Microsoft Windows 8. The resulting driver is more reliable and performs better than its prior incarnation (which did not use P); we have more confidence in the robustness of its design due to the language abstractions and verification provided by P."}],"author":[{"full_name":"Desai, Ankush","first_name":"Ankush","last_name":"Desai"},{"first_name":"Vivek","full_name":"Gupta, Vivek","last_name":"Gupta"},{"last_name":"Jackson","first_name":"Ethan","full_name":"Jackson, Ethan"},{"first_name":"Shaz","full_name":"Qadeer, Shaz","last_name":"Qadeer"},{"first_name":"Sriram","full_name":"Rajamani, Sriram","last_name":"Rajamani"},{"full_name":"Zufferey, Damien","first_name":"Damien","orcid":"0000-0002-3197-8736","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87"}],"_id":"2301","status":"public","type":"conference","language":[{"iso":"eng"}],"doi":"10.1145/2491956.2462184","publisher":"ACM","date_updated":"2021-01-12T06:56:38Z","year":"2013"},{"year":"2013","publisher":"Institute of Science and Technology Austria","doi":"10.15479/at:ista:1405","language":[{"iso":"eng"}],"type":"dissertation","_id":"1405","oa":1,"author":[{"first_name":"Damien","full_name":"Zufferey, Damien","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3197-8736"}],"date_published":"2013-09-05T00:00:00Z","acknowledgement":"This work was supported in part by the Austrian Science Fund NFN RiSE (Rigorous Systems Engineering) and by the ERC Advanced Grant QUAREM (Quantitative Reactve Modeling).\r\nChapter 2, 3, and 4 are joint work with Thomas A. Henzinger and Thomas Wies. Chapter 2 was published in FoSSaCS 2010 as “Forward Analysis of Depth-Bounded Processes” [112]. Chapter 3 was published in VMCAI 2012 as “Ideal Abstractions for Well-Structured Transition Systems” [114]. Chap- ter 5.1 is joint work with Kshitij Bansal, Eric Koskinen, and Thomas Wies. It was published in TACAS 2013 as “Structural Counter Abstraction” [13]. The author’s contribution in this part is mostly related to the implementation. The theory required to understand the method and its implementation is quickly recalled to make the thesis self-contained, but should not be considered as a contribution. For the details of the methods, we refer the reader to the orig- inal publication [13] and the corresponding technical report [14]. Chapter 5.2 is ongoing work with Shahram Esmaeilsabzali, Rupak Majumdar, and Thomas Wies. I also would like to thank the people who supported over the past 4 years. My advisor Thomas A. Henzinger who gave me a lot of freedom to work on projects I was interested in. My collaborators, especially Thomas Wies with whom I worked since the beginning. The members of my thesis committee, Viktor Kun- cak and Rupak Majumdar, who also agreed to advise me. Simon Aeschbacher, Pavol Cerny, Cezara Dragoi, Arjun Radhakrishna, my family, friends and col- leagues who created an enjoyable environment. ","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"date_created":"2018-12-11T11:51:50Z","file_date_updated":"2021-11-17T13:47:58Z","ddc":["000"],"article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publication_identifier":{"issn":["2663-337X"]},"publist_id":"5802","month":"09","supervisor":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"}],"date_updated":"2023-09-07T11:36:37Z","status":"public","degree_awarded":"PhD","abstract":[{"text":"Motivated by the analysis of highly dynamic message-passing systems, i.e. unbounded thread creation, mobility, etc. we present a framework for the analysis of depth-bounded systems. Depth-bounded systems are one of the most expressive known fragment of the π-calculus for which interesting verification problems are still decidable. Even though they are infinite state systems depth-bounded systems are well-structured, thus can be analyzed algorithmically. We give an interpretation of depth-bounded systems as graph-rewriting systems. This gives more flexibility and ease of use to apply depth-bounded systems to other type of systems like shared memory concurrency.\r\n\r\nFirst, we develop an adequate domain of limits for depth-bounded systems, a prerequisite for the effective representation of downward-closed sets. Downward-closed sets are needed by forward saturation-based algorithms to represent potentially infinite sets of states. Then, we present an abstract interpretation framework to compute the covering set of well-structured transition systems. Because, in general, the covering set is not computable, our abstraction over-approximates the actual covering set. Our abstraction captures the essence of acceleration based-algorithms while giving up enough precision to ensure convergence. We have implemented the analysis in the PICASSO tool and show that it is accurate in practice. Finally, we build some further analyses like termination using the covering set as starting point.","lang":"eng"}],"ec_funded":1,"day":"05","page":"134","oa_version":"Published Version","publication_status":"published","citation":{"ama":"Zufferey D. Analysis of dynamic message passing programs. 2013. doi:<a href=\"https://doi.org/10.15479/at:ista:1405\">10.15479/at:ista:1405</a>","mla":"Zufferey, Damien. <i>Analysis of Dynamic Message Passing Programs</i>. Institute of Science and Technology Austria, 2013, doi:<a href=\"https://doi.org/10.15479/at:ista:1405\">10.15479/at:ista:1405</a>.","apa":"Zufferey, D. (2013). <i>Analysis of dynamic message passing programs</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/at:ista:1405\">https://doi.org/10.15479/at:ista:1405</a>","ista":"Zufferey D. 2013. Analysis of dynamic message passing programs. Institute of Science and Technology Austria.","short":"D. Zufferey, Analysis of Dynamic Message Passing Programs, Institute of Science and Technology Austria, 2013.","ieee":"D. Zufferey, “Analysis of dynamic message passing programs,” Institute of Science and Technology Austria, 2013.","chicago":"Zufferey, Damien. “Analysis of Dynamic Message Passing Programs.” Institute of Science and Technology Austria, 2013. <a href=\"https://doi.org/10.15479/at:ista:1405\">https://doi.org/10.15479/at:ista:1405</a>."},"project":[{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7"}],"has_accepted_license":"1","alternative_title":["ISTA Thesis"],"main_file_link":[{"url":"http://dzufferey.github.io/files/2013_thesis.pdf"}],"title":"Analysis of dynamic message passing programs","file":[{"file_name":"2013_Zufferey_thesis_final.pdf","file_size":1514906,"date_created":"2021-02-22T11:28:36Z","checksum":"ed2d7b52933d134e8dc69d569baa284e","file_id":"9176","success":1,"date_updated":"2021-02-22T11:28:36Z","creator":"dernst","access_level":"open_access","content_type":"application/pdf","relation":"main_file"},{"content_type":"application/pdf","relation":"main_file","access_level":"closed","creator":"cchlebak","date_updated":"2021-11-17T13:47:58Z","date_created":"2021-11-16T14:42:52Z","file_id":"10298","checksum":"cecc4c4b14225bee973d32e3dba91a55","file_size":1378313,"file_name":"2013_Zufferey_thesis_final_pdfa.pdf"}],"related_material":{"record":[{"relation":"part_of_dissertation","id":"2847","status":"public"},{"relation":"part_of_dissertation","id":"3251","status":"public"},{"id":"4361","status":"public","relation":"part_of_dissertation"}]}},{"volume":301,"month":"05","publist_id":"3946","quality_controlled":"1","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","intvolume":"       301","date_created":"2018-12-11T11:59:55Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"pmid":1,"date_published":"2012-05-21T00:00:00Z","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Damien","full_name":"Zufferey, Damien","orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","last_name":"Zufferey"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"_id":"2848","oa":1,"type":"journal_article","doi":"10.1016/j.jtbi.2012.02.021","language":[{"iso":"eng"}],"year":"2012","publisher":"Elsevier","publication":"Journal of Theoretical Biology","title":"Evolutionary game dynamics in populations with different learners","external_id":{"pmid":["22394652"]},"main_file_link":[{"url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3322297/","open_access":"1"}],"scopus_import":1,"citation":{"chicago":"Chatterjee, Krishnendu, Damien Zufferey, and Martin Nowak. “Evolutionary Game Dynamics in Populations with Different Learners.” <i>Journal of Theoretical Biology</i>. Elsevier, 2012. <a href=\"https://doi.org/10.1016/j.jtbi.2012.02.021\">https://doi.org/10.1016/j.jtbi.2012.02.021</a>.","ieee":"K. Chatterjee, D. Zufferey, and M. Nowak, “Evolutionary game dynamics in populations with different learners,” <i>Journal of Theoretical Biology</i>, vol. 301. Elsevier, pp. 161–173, 2012.","ista":"Chatterjee K, Zufferey D, Nowak M. 2012. Evolutionary game dynamics in populations with different learners. Journal of Theoretical Biology. 301, 161–173.","apa":"Chatterjee, K., Zufferey, D., &#38; Nowak, M. (2012). Evolutionary game dynamics in populations with different learners. <i>Journal of Theoretical Biology</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jtbi.2012.02.021\">https://doi.org/10.1016/j.jtbi.2012.02.021</a>","short":"K. Chatterjee, D. Zufferey, M. Nowak, Journal of Theoretical Biology 301 (2012) 161–173.","mla":"Chatterjee, Krishnendu, et al. “Evolutionary Game Dynamics in Populations with Different Learners.” <i>Journal of Theoretical Biology</i>, vol. 301, Elsevier, 2012, pp. 161–73, doi:<a href=\"https://doi.org/10.1016/j.jtbi.2012.02.021\">10.1016/j.jtbi.2012.02.021</a>.","ama":"Chatterjee K, Zufferey D, Nowak M. Evolutionary game dynamics in populations with different learners. <i>Journal of Theoretical Biology</i>. 2012;301:161-173. doi:<a href=\"https://doi.org/10.1016/j.jtbi.2012.02.021\">10.1016/j.jtbi.2012.02.021</a>"},"project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"day":"21","oa_version":"Submitted Version","page":"161 - 173","publication_status":"published","abstract":[{"lang":"eng","text":"We study evolutionary game theory in a setting where individuals learn from each other. We extend the traditional approach by assuming that a population contains individuals with different learning abilities. In particular, we explore the situation where individuals have different search spaces, when attempting to learn the strategies of others. The search space of an individual specifies the set of strategies learnable by that individual. The search space is genetically given and does not change under social evolutionary dynamics. We introduce a general framework and study a specific example in the context of direct reciprocity. For this example, we obtain the counter intuitive result that cooperation can only evolve for intermediate benefit-to-cost ratios, while small and large benefit-to-cost ratios favor defection. Our paper is a step toward making a connection between computational learning theory and evolutionary game dynamics."}],"ec_funded":1,"status":"public","date_updated":"2021-01-12T07:00:12Z"},{"type":"conference","publisher":"Springer","year":"2012","language":[{"iso":"eng"}],"doi":"10.1007/978-3-642-27940-9_29","date_published":"2012-01-01T00:00:00Z","oa":1,"_id":"3251","author":[{"full_name":"Zufferey, Damien","first_name":"Damien","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-3197-8736"},{"first_name":"Thomas","full_name":"Wies, Thomas","last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"intvolume":"      7148","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","ddc":["000","005"],"file_date_updated":"2020-07-14T12:46:05Z","conference":{"location":"Philadelphia, PA, USA","start_date":"2012-01-22","end_date":"2012-01-24","name":"VMCAI: Verification, Model Checking and Abstract Interpretation"},"department":[{"_id":"ToHe"}],"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.","date_created":"2018-12-11T12:02:16Z","volume":7148,"quality_controlled":"1","publist_id":"3406","month":"01","status":"public","date_updated":"2023-09-07T11:36:36Z","ec_funded":1,"abstract":[{"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.","lang":"eng"}],"publication_status":"published","page":"445 - 460","oa_version":"Submitted Version","day":"01","alternative_title":["LNCS"],"has_accepted_license":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"}],"citation":{"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.","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.","short":"D. Zufferey, T. Wies, T.A. Henzinger, in:, Springer, 2012, pp. 445–460.","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>","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>"},"pubrep_id":"100","related_material":{"record":[{"relation":"dissertation_contains","id":"1405","status":"public"}]},"file":[{"date_updated":"2020-07-14T12:46:05Z","file_id":"4759","date_created":"2018-12-12T10:09:35Z","checksum":"f2f0d55efa32309ad1fe65a5fcaad90c","file_size":217104,"file_name":"IST-2012-100-v1+1_Ideal_abstractions_for_well-structured_transition_systems.pdf","relation":"main_file","content_type":"application/pdf","access_level":"open_access","creator":"system"}],"title":"Ideal abstractions for well structured transition systems"},{"citation":{"ama":"Henzinger TA, Singh A, Singh V, Wies T, Zufferey D. Static scheduling in clouds. In: USENIX; 2011:1-6.","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.","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.","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."},"department":[{"_id":"ToHe"}],"date_created":"2018-12-11T12:02:33Z","pubrep_id":"90","has_accepted_license":"1","file_date_updated":"2020-07-14T12:46:06Z","conference":{"end_date":"2011-06-15","start_date":"2011-06-14","name":"HotCloud: Workshop on Hot Topics in Cloud Computing"},"ddc":["000","005"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"3338","quality_controlled":"1","month":"06","title":"Static scheduling in clouds","file":[{"date_updated":"2020-07-14T12:46:06Z","file_id":"5333","checksum":"21a461ac004bb535c83320fe79b30375","date_created":"2018-12-12T10:18:14Z","file_size":232770,"file_name":"IST-2012-90-v1+1_Static_scheduling_in_clouds.pdf","relation":"main_file","content_type":"application/pdf","access_level":"open_access","creator":"system"}],"year":"2011","date_updated":"2021-01-12T07:42:31Z","publisher":"USENIX","language":[{"iso":"eng"}],"type":"conference","status":"public","_id":"3302","oa":1,"author":[{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"first_name":"Anmol","full_name":"Singh, Anmol","id":"72A86902-E99F-11E9-9F62-915534D1B916","last_name":"Singh"},{"full_name":"Singh, Vasu","first_name":"Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","last_name":"Singh"},{"last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87","full_name":"Wies, Thomas","first_name":"Thomas"},{"full_name":"Zufferey, Damien","first_name":"Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","last_name":"Zufferey","orcid":"0000-0002-3197-8736"}],"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","publication_status":"published","date_published":"2011-06-14T00:00:00Z","page":"1 - 6","oa_version":"Submitted Version"},{"title":"Scheduling large jobs by abstraction refinement","month":"04","publist_id":"3257","main_file_link":[{"url":"http://cs.nyu.edu/wies/publ/scheduling_large_jobs_by_abstraction_refinement.pdf","open_access":"1"}],"quality_controlled":"1","conference":{"location":"Salzburg, Austria","end_date":"2011-04-13","start_date":"2011-04-10","name":"EuroSys"},"scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","date_created":"2018-12-11T12:02:53Z","department":[{"_id":"ToHe"}],"citation":{"ieee":"T. A. Henzinger, V. Singh, T. Wies, and D. Zufferey, “Scheduling large jobs by abstraction refinement,” presented at the EuroSys, Salzburg, Austria, 2011, pp. 329–342.","chicago":"Henzinger, Thomas A, Vasu Singh, Thomas Wies, and Damien Zufferey. “Scheduling Large Jobs by Abstraction Refinement,” 329–42. ACM, 2011. <a href=\"https://doi.org/10.1145/1966445.1966476\">https://doi.org/10.1145/1966445.1966476</a>.","ama":"Henzinger TA, Singh V, Wies T, Zufferey D. Scheduling large jobs by abstraction refinement. In: ACM; 2011:329-342. doi:<a href=\"https://doi.org/10.1145/1966445.1966476\">10.1145/1966445.1966476</a>","ista":"Henzinger TA, Singh V, Wies T, Zufferey D. 2011. Scheduling large jobs by abstraction refinement. EuroSys, 329–342.","short":"T.A. Henzinger, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2011, pp. 329–342.","mla":"Henzinger, Thomas A., et al. <i>Scheduling Large Jobs by Abstraction Refinement</i>. ACM, 2011, pp. 329–42, doi:<a href=\"https://doi.org/10.1145/1966445.1966476\">10.1145/1966445.1966476</a>.","apa":"Henzinger, T. A., Singh, V., Wies, T., &#38; Zufferey, D. (2011). Scheduling large jobs by abstraction refinement (pp. 329–342). Presented at the EuroSys, Salzburg, Austria: ACM. <a href=\"https://doi.org/10.1145/1966445.1966476\">https://doi.org/10.1145/1966445.1966476</a>"},"day":"10","date_published":"2011-04-10T00:00:00Z","page":"329 - 342","publication_status":"published","oa_version":"Published Version","abstract":[{"lang":"eng","text":"The static scheduling problem often arises as a fundamental problem in real-time systems and grid computing. We consider the problem of statically scheduling a large job expressed as a task graph on a large number of computing nodes, such as a data center. This paper solves the large-scale static scheduling problem using abstraction refinement, a technique commonly used in formal verification to efficiently solve computationally hard problems. A scheduler based on abstraction refinement first attempts to solve the scheduling problem with abstract representations of the job and the computing resources. As abstract representations are generally small, the scheduling can be done reasonably fast. If the obtained schedule does not meet specified quality conditions (like data center utilization or schedule makespan) then the scheduler refines the job and data center abstractions and, again solves the scheduling problem. We develop different schedulers based on abstraction refinement. We implemented these schedulers and used them to schedule task graphs from various computing domains on simulated data centers with realistic topologies. We compared the speed of scheduling and the quality of the produced schedules with our abstraction refinement schedulers against a baseline scheduler that does not use any abstraction. We conclude that abstraction refinement techniques give a significant speed-up compared to traditional static scheduling heuristics, at a reasonable cost in the quality of the produced schedules. We further used our static schedulers in an actual system that we deployed on Amazon EC2 and compared it against the Hadoop dynamic scheduler for large MapReduce jobs. Our experiments indicate that there is great potential for static scheduling techniques."}],"author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Vasu","full_name":"Singh, Vasu","last_name":"Singh","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas","full_name":"Wies, Thomas","last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Damien","full_name":"Zufferey, Damien","orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","last_name":"Zufferey"}],"_id":"3358","oa":1,"status":"public","type":"conference","doi":"10.1145/1966445.1966476","language":[{"iso":"eng"}],"year":"2011","publisher":"ACM","date_updated":"2021-01-12T07:42:55Z"},{"title":"Model checking of linearizability of concurrent list implementations","file":[{"creator":"system","access_level":"open_access","content_type":"application/pdf","relation":"main_file","file_name":"IST-2010-0001_IST-2010-0001.pdf","file_size":372286,"date_created":"2018-12-12T11:53:44Z","checksum":"986645caad7dd85a6a091488f6c646dc","file_id":"5505","date_updated":"2020-07-14T12:46:43Z"}],"related_material":{"record":[{"id":"4390","status":"public","relation":"later_version"}]},"publication_identifier":{"issn":["2664-1690"]},"month":"04","has_accepted_license":"1","alternative_title":["IST Austria Technical Report"],"file_date_updated":"2020-07-14T12:46:43Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["004"],"citation":{"ieee":"P. Cerny, A. Radhakrishna, D. Zufferey, S. Chaudhuri, and R. Alur, <i>Model checking of linearizability of concurrent list implementations</i>. IST Austria, 2010.","chicago":"Cerny, Pavol, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, and Rajeev Alur. <i>Model Checking of Linearizability of Concurrent List Implementations</i>. IST Austria, 2010. <a href=\"https://doi.org/10.15479/AT:IST-2010-0001\">https://doi.org/10.15479/AT:IST-2010-0001</a>.","ama":"Cerny P, Radhakrishna A, Zufferey D, Chaudhuri S, Alur R. <i>Model Checking of Linearizability of Concurrent List Implementations</i>. IST Austria; 2010. doi:<a href=\"https://doi.org/10.15479/AT:IST-2010-0001\">10.15479/AT:IST-2010-0001</a>","apa":"Cerny, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., &#38; Alur, R. (2010). <i>Model checking of linearizability of concurrent list implementations</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2010-0001\">https://doi.org/10.15479/AT:IST-2010-0001</a>","short":"P. Cerny, A. Radhakrishna, D. Zufferey, S. Chaudhuri, R. Alur, Model Checking of Linearizability of Concurrent List Implementations, IST Austria, 2010.","ista":"Cerny P, Radhakrishna A, Zufferey D, Chaudhuri S, Alur R. 2010. Model checking of linearizability of concurrent list implementations, IST Austria, 27p.","mla":"Cerny, Pavol, et al. <i>Model Checking of Linearizability of Concurrent List Implementations</i>. IST Austria, 2010, doi:<a href=\"https://doi.org/10.15479/AT:IST-2010-0001\">10.15479/AT:IST-2010-0001</a>."},"department":[{"_id":"ToHe"}],"date_created":"2018-12-12T11:39:04Z","pubrep_id":"27","abstract":[{"lang":"eng","text":"Concurrent data structures with fine-grained synchronization are notoriously difficult to implement correctly. The difficulty of reasoning about these implementations does not stem from the number of variables or the program size, but rather from the large number of possible interleavings. These implementations are therefore prime candidates for model checking. We introduce an algorithm for verifying linearizability of singly-linked heap-based concurrent data structures. We consider a model consisting of an unbounded heap where each node consists an element from an unbounded data domain, with a restricted set of operations for testing and updating pointers and data elements. Our main result is that linearizability is decidable for programs that invoke a fixed number of methods, possibly in parallel. This decidable fragment covers many of the common implementation techniques — fine-grained locking, lazy synchronization, and lock-free synchronization. We also show how the technique can be used to verify optimistic implementations with the help of programmer annotations. We developed a verification tool CoLT and evaluated it on a representative sample of Java implementations of the concurrent set data structure. The tool verified linearizability of a number of implementations, found a known error in a lock-free imple- mentation and proved that the corrected version is linearizable."}],"day":"19","page":"27","publication_status":"published","date_published":"2010-04-19T00:00:00Z","oa_version":"Published Version","_id":"5391","oa":1,"author":[{"first_name":"Pavol","full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","last_name":"Cerny"},{"first_name":"Arjun","full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Zufferey, Damien","first_name":"Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","last_name":"Zufferey","orcid":"0000-0002-3197-8736"},{"full_name":"Chaudhuri, Swarat","first_name":"Swarat","last_name":"Chaudhuri"},{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"}],"type":"technical_report","status":"public","year":"2010","date_updated":"2023-02-23T12:09:09Z","publisher":"IST Austria","doi":"10.15479/AT:IST-2010-0001","language":[{"iso":"eng"}]},{"editor":[{"last_name":"Ong","first_name":"Luke","full_name":"Ong, Luke"}],"scopus_import":1,"alternative_title":["LNCS"],"has_accepted_license":"1","pubrep_id":"50","citation":{"ama":"Wies T, Zufferey D, Henzinger TA. Forward analysis of depth-bounded processes. In: Ong L, ed. Vol 6014. Springer; 2010:94-108. doi:<a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">10.1007/978-3-642-12032-9_8</a>","apa":"Wies, T., Zufferey, D., &#38; Henzinger, T. A. (2010). Forward analysis of depth-bounded processes. In L. Ong (Ed.) (Vol. 6014, pp. 94–108). Presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Paphos, Cyprus: Springer. <a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">https://doi.org/10.1007/978-3-642-12032-9_8</a>","ista":"Wies T, Zufferey D, Henzinger TA. 2010. Forward analysis of depth-bounded processes. FoSSaCS: Foundations of Software Science and Computation Structures, LNCS, vol. 6014, 94–108.","mla":"Wies, Thomas, et al. <i>Forward Analysis of Depth-Bounded Processes</i>. Edited by Luke Ong, vol. 6014, Springer, 2010, pp. 94–108, doi:<a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">10.1007/978-3-642-12032-9_8</a>.","short":"T. Wies, D. Zufferey, T.A. Henzinger, in:, L. Ong (Ed.), Springer, 2010, pp. 94–108.","ieee":"T. Wies, D. Zufferey, and T. A. Henzinger, “Forward analysis of depth-bounded processes,” presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Paphos, Cyprus, 2010, vol. 6014, pp. 94–108.","chicago":"Wies, Thomas, Damien Zufferey, and Thomas A Henzinger. “Forward Analysis of Depth-Bounded Processes.” edited by Luke Ong, 6014:94–108. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-12032-9_8\">https://doi.org/10.1007/978-3-642-12032-9_8</a>."},"related_material":{"record":[{"relation":"dissertation_contains","id":"1405","status":"public"}]},"title":"Forward analysis of depth-bounded processes","file":[{"file_size":240766,"file_name":"IST-2012-50-v1+1_Forward_analysis_of_depth-bounded_processes.pdf","date_updated":"2020-07-14T12:46:27Z","checksum":"3e610de84937d821316362658239134a","date_created":"2018-12-12T10:08:17Z","file_id":"4677","creator":"system","relation":"main_file","content_type":"application/pdf","access_level":"open_access"}],"status":"public","date_updated":"2023-09-07T11:36:36Z","oa_version":"Submitted Version","publication_status":"published","page":"94 - 108","day":"01","abstract":[{"lang":"eng","text":"Depth-bounded processes form the most expressive known fragment of the π-calculus for which interesting verification problems are still decidable. In this paper we develop an adequate domain of limits for the well-structured transition systems that are induced by depth-bounded processes. An immediate consequence of our result is that there exists a forward algorithm that decides the covering problem for this class. Unlike backward algorithms, the forward algorithm terminates even if the depth of the process is not known a priori. More importantly, our result suggests a whole spectrum of forward algorithms that enable the effective verification of a large class of mobile systems."}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","ddc":["004"],"file_date_updated":"2020-07-14T12:46:27Z","conference":{"location":"Paphos, Cyprus","start_date":"2010-03-20","end_date":"2010-03-28","name":"FoSSaCS: Foundations of Software Science and Computation Structures"},"intvolume":"      6014","date_created":"2018-12-11T12:08:27Z","department":[{"_id":"ToHe"}],"volume":6014,"month":"03","quality_controlled":"1","publist_id":"1099","type":"conference","language":[{"iso":"eng"}],"doi":"10.1007/978-3-642-12032-9_8","publisher":"Springer","year":"2010","date_published":"2010-03-01T00:00:00Z","author":[{"first_name":"Thomas","full_name":"Wies, Thomas","last_name":"Wies","id":"447BFB88-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Zufferey, Damien","first_name":"Damien","orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","last_name":"Zufferey"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"oa":1,"_id":"4361"},{"department":[{"_id":"ToHe"}],"date_created":"2018-12-11T12:08:33Z","ddc":["005"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file_date_updated":"2020-07-14T12:46:28Z","conference":{"start_date":"2010-10-24","end_date":"2010-10-29","name":"EMSOFT: Embedded Software ","location":"Arizona, USA"},"quality_controlled":"1","publist_id":"1078","month":"10","publisher":"ACM","year":"2010","language":[{"iso":"eng"}],"doi":"10.1145/1879021.1879022","type":"conference","oa":1,"_id":"4380","author":[{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"first_name":"Anmol","full_name":"Tomar, Anmol","last_name":"Tomar","id":"3D8D36B6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Singh, Vasu","first_name":"Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","last_name":"Singh"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","last_name":"Wies","first_name":"Thomas","full_name":"Wies, Thomas"},{"full_name":"Zufferey, Damien","first_name":"Damien","orcid":"0000-0002-3197-8736","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87"}],"date_published":"2010-10-24T00:00:00Z","citation":{"ama":"Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. A marketplace for cloud resources. In: ACM; 2010:1-8. doi:<a href=\"https://doi.org/10.1145/1879021.1879022\">10.1145/1879021.1879022</a>","short":"T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, ACM, 2010, pp. 1–8.","apa":"Henzinger, T. A., Tomar, A., Singh, V., Wies, T., &#38; Zufferey, D. (2010). A marketplace for cloud resources (pp. 1–8). Presented at the EMSOFT: Embedded Software , Arizona, USA: ACM. <a href=\"https://doi.org/10.1145/1879021.1879022\">https://doi.org/10.1145/1879021.1879022</a>","ista":"Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. A marketplace for cloud resources. EMSOFT: Embedded Software , 1–8.","mla":"Henzinger, Thomas A., et al. <i>A Marketplace for Cloud Resources</i>. ACM, 2010, pp. 1–8, doi:<a href=\"https://doi.org/10.1145/1879021.1879022\">10.1145/1879021.1879022</a>.","ieee":"T. A. Henzinger, A. Tomar, V. Singh, T. Wies, and D. Zufferey, “A marketplace for cloud resources,” presented at the EMSOFT: Embedded Software , Arizona, USA, 2010, pp. 1–8.","chicago":"Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien Zufferey. “A Marketplace for Cloud Resources,” 1–8. ACM, 2010. <a href=\"https://doi.org/10.1145/1879021.1879022\">https://doi.org/10.1145/1879021.1879022</a>."},"pubrep_id":"48","has_accepted_license":"1","scopus_import":1,"file":[{"date_updated":"2020-07-14T12:46:28Z","file_id":"4767","checksum":"7680dd24016810710f7c977bc94f85e9","date_created":"2018-12-12T10:09:42Z","file_size":222626,"file_name":"IST-2012-48-v1+1_A_marketplace_for_cloud_resources.pdf","content_type":"application/pdf","relation":"main_file","access_level":"open_access","creator":"system"}],"title":"A marketplace for cloud resources","date_updated":"2021-01-12T07:56:32Z","status":"public","abstract":[{"text":"Cloud computing is an emerging paradigm aimed to offer users pay-per-use computing resources, while leaving the burden of managing the computing infrastructure to the cloud provider. We present a new programming and pricing model that gives the cloud user the flexibility of trading execution speed and price on a per-job basis. We discuss the scheduling and resource management challenges for the cloud provider that arise in the implementation of this model. We argue that techniques from real-time and embedded software can be useful in this context.","lang":"eng"}],"publication_status":"published","oa_version":"Submitted Version","page":"1 - 8","day":"24"},{"date_updated":"2021-01-12T07:56:33Z","status":"public","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 claim that, in order to realize the full potential of cloud computing, the user must be presented with a pricing model that offers flexibility at the requirements level, such as a choice between different degrees of execution speed and the cloud provider must be presented with a programming model that offers flexibility at the execution level, such as a choice between different scheduling policies. In such a flexible framework, with each job, the user purchases a virtual computer with the desired speed and cost characteristics, and the cloud provider can optimize the utilization of resources across a stream of jobs from different users. We designed a flexible framework to test our hypothesis, which is called FlexPRICE (Flexible Provisioning of Resources in a Cloud Environment) and works as follows. A user presents a job to the cloud. The cloud finds different schedules to execute the job and presents a set of quotes to the user in terms of price and duration for the execution. The user then chooses a particular quote and the cloud is obliged to execute the job according to the chosen quote. FlexPRICE thus hides the complexity of the actual scheduling decisions from the user, but still provides enough flexibility to meet the users actual demands. We implemented FlexPRICE in a simulator called PRICES that allows us to experiment with our framework. We observe that FlexPRICE provides a wide range of execution options-from fast and expensive to slow and cheap-- for the whole spectrum of data-intensive and computation-intensive jobs. We also observe that the set of quotes computed by FlexPRICE do not vary as the number of simultaneous jobs increases."}],"day":"26","publication_status":"published","oa_version":"Submitted Version","page":"83 - 90","citation":{"mla":"Henzinger, Thomas A., et al. <i>FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment</i>. IEEE, 2010, pp. 83–90, doi:<a href=\"https://doi.org/10.1109/CLOUD.2010.71\">10.1109/CLOUD.2010.71</a>.","apa":"Henzinger, T. A., Tomar, A., Singh, V., Wies, T., &#38; Zufferey, D. (2010). FlexPRICE: Flexible provisioning of resources in a cloud environment (pp. 83–90). Presented at the CLOUD: Cloud Computing, Miami, USA: IEEE. <a href=\"https://doi.org/10.1109/CLOUD.2010.71\">https://doi.org/10.1109/CLOUD.2010.71</a>","ista":"Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. 2010. FlexPRICE: Flexible provisioning of resources in a cloud environment. CLOUD: Cloud Computing, 83–90.","short":"T.A. Henzinger, A. Tomar, V. Singh, T. Wies, D. Zufferey, in:, IEEE, 2010, pp. 83–90.","ama":"Henzinger TA, Tomar A, Singh V, Wies T, Zufferey D. FlexPRICE: Flexible provisioning of resources in a cloud environment. In: IEEE; 2010:83-90. doi:<a href=\"https://doi.org/10.1109/CLOUD.2010.71\">10.1109/CLOUD.2010.71</a>","chicago":"Henzinger, Thomas A, Anmol Tomar, Vasu Singh, Thomas Wies, and Damien Zufferey. “FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment,” 83–90. IEEE, 2010. <a href=\"https://doi.org/10.1109/CLOUD.2010.71\">https://doi.org/10.1109/CLOUD.2010.71</a>.","ieee":"T. A. Henzinger, A. Tomar, V. Singh, T. Wies, and D. Zufferey, “FlexPRICE: Flexible provisioning of resources in a cloud environment,” presented at the CLOUD: Cloud Computing, Miami, USA, 2010, pp. 83–90."},"pubrep_id":"47","has_accepted_license":"1","scopus_import":1,"title":"FlexPRICE: Flexible provisioning of resources in a cloud environment","file":[{"file_name":"IST-2012-47-v1+1_FlexPRICE-_Flexible_provisioning_of_resources_in_a_cloud_environment.pdf","file_size":467436,"file_id":"5188","checksum":"98e534675339a8e2beca08890d048145","date_created":"2018-12-12T10:16:03Z","date_updated":"2020-07-14T12:46:28Z","creator":"system","access_level":"open_access","relation":"main_file","content_type":"application/pdf"}],"year":"2010","publisher":"IEEE","doi":"10.1109/CLOUD.2010.71","language":[{"iso":"eng"}],"type":"conference","_id":"4381","oa":1,"author":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"last_name":"Tomar","id":"3D8D36B6-F248-11E8-B48F-1D18A9856A87","first_name":"Anmol","full_name":"Tomar, Anmol"},{"id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","last_name":"Singh","first_name":"Vasu","full_name":"Singh, Vasu"},{"id":"447BFB88-F248-11E8-B48F-1D18A9856A87","last_name":"Wies","full_name":"Wies, Thomas","first_name":"Thomas"},{"orcid":"0000-0002-3197-8736","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","full_name":"Zufferey, Damien","first_name":"Damien"}],"date_published":"2010-08-26T00:00:00Z","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T12:08:33Z","file_date_updated":"2020-07-14T12:46:28Z","conference":{"name":"CLOUD: Cloud Computing","start_date":"2010-07-05","end_date":"2010-07-10","location":"Miami, USA"},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","ddc":["004"],"article_processing_charge":"No","publist_id":"1077","quality_controlled":"1","month":"08"},{"date_updated":"2023-02-23T12:24:12Z","status":"public","abstract":[{"text":"Concurrent data structures with fine-grained synchronization are notoriously difficult to implement correctly. The difficulty of reasoning about these implementations does not stem from the number of variables or the program size, but rather from the large number of possible interleavings. These implementations are therefore prime candidates for model checking. We introduce an algorithm for verifying linearizability of singly-linked heap-based concurrent data structures. We consider a model consisting of an unbounded heap where each vertex stores an element from an unbounded data domain, with a restricted set of operations for testing and updating pointers and data elements. Our main result is that linearizability is decidable for programs that invoke a fixed number of methods, possibly in parallel. This decidable fragment covers many of the common implementation techniques — fine-grained locking, lazy synchronization, and lock-free synchronization. We also show how the technique can be used to verify optimistic implementations with the help of programmer annotations. We developed a verification tool CoLT and evaluated it on a representative sample of Java implementations of the concurrent set data structure. The tool verified linearizability of a number of implementations, found a known error in a lock-free implementation and proved that the corrected version is linearizable.","lang":"eng"}],"day":"01","publication_status":"published","oa_version":"Submitted Version","page":"465 - 479","citation":{"chicago":"Cerny, Pavol, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, and Rajeev Alur. “Model Checking of Linearizability of Concurrent List Implementations,” 6174:465–79. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-14295-6_41\">https://doi.org/10.1007/978-3-642-14295-6_41</a>.","ieee":"P. Cerny, A. Radhakrishna, D. Zufferey, S. Chaudhuri, and R. Alur, “Model checking of linearizability of concurrent list implementations,” presented at the CAV: Computer Aided Verification, Edinburgh, UK, 2010, vol. 6174, pp. 465–479.","ista":"Cerny P, Radhakrishna A, Zufferey D, Chaudhuri S, Alur R. 2010. Model checking of linearizability of concurrent list implementations. CAV: Computer Aided Verification, LNCS, vol. 6174, 465–479.","apa":"Cerny, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., &#38; Alur, R. (2010). Model checking of linearizability of concurrent list implementations (Vol. 6174, pp. 465–479). Presented at the CAV: Computer Aided Verification, Edinburgh, UK: Springer. <a href=\"https://doi.org/10.1007/978-3-642-14295-6_41\">https://doi.org/10.1007/978-3-642-14295-6_41</a>","mla":"Cerny, Pavol, et al. <i>Model Checking of Linearizability of Concurrent List Implementations</i>. Vol. 6174, Springer, 2010, pp. 465–79, doi:<a href=\"https://doi.org/10.1007/978-3-642-14295-6_41\">10.1007/978-3-642-14295-6_41</a>.","short":"P. Cerny, A. Radhakrishna, D. Zufferey, S. Chaudhuri, R. Alur, in:, Springer, 2010, pp. 465–479.","ama":"Cerny P, Radhakrishna A, Zufferey D, Chaudhuri S, Alur R. Model checking of linearizability of concurrent list implementations. In: Vol 6174. Springer; 2010:465-479. doi:<a href=\"https://doi.org/10.1007/978-3-642-14295-6_41\">10.1007/978-3-642-14295-6_41</a>"},"pubrep_id":"27","has_accepted_license":"1","alternative_title":["LNCS"],"file":[{"access_level":"open_access","content_type":"application/pdf","relation":"main_file","creator":"dernst","date_created":"2020-05-19T16:31:56Z","checksum":"2eb211ce40b3c4988bce3a3592980704","file_id":"7873","date_updated":"2020-07-14T12:46:28Z","file_name":"2010_CAV_Cerny.pdf","file_size":3633276}],"title":"Model checking of linearizability of concurrent list implementations","related_material":{"record":[{"id":"5391","status":"public","relation":"earlier_version"}]},"year":"2010","publisher":"Springer","doi":"10.1007/978-3-642-14295-6_41","language":[{"iso":"eng"}],"type":"conference","_id":"4390","oa":1,"author":[{"last_name":"Cerny","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","first_name":"Pavol","full_name":"Cerny, Pavol"},{"last_name":"Radhakrishna","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","full_name":"Radhakrishna, Arjun","first_name":"Arjun"},{"orcid":"0000-0002-3197-8736","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","first_name":"Damien","full_name":"Zufferey, Damien"},{"last_name":"Chaudhuri","first_name":"Swarat","full_name":"Chaudhuri, Swarat"},{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"}],"date_published":"2010-07-01T00:00:00Z","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T12:08:36Z","intvolume":"      6174","file_date_updated":"2020-07-14T12:46:28Z","conference":{"end_date":"2010-07-17","start_date":"2010-07-15","name":"CAV: Computer Aided Verification","location":"Edinburgh, UK"},"ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","publist_id":"1066","quality_controlled":"1","month":"07","volume":6174},{"file":[{"creator":"system","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_size":312147,"file_name":"IST-2012-41-v1+1_Shape_refinement_through_explicit_heap_analysis.pdf","date_updated":"2020-07-14T12:46:29Z","checksum":"7d26e59a9681487d7283eba337292b2c","file_id":"5332","date_created":"2018-12-12T10:18:13Z"}],"title":"Shape refinement through explicit heap analysis","alternative_title":["LNCS"],"has_accepted_license":"1","scopus_import":1,"editor":[{"last_name":"Rosenblum","full_name":"Rosenblum, David","first_name":"David"},{"last_name":"Taenzer","first_name":"Gabriele","full_name":"Taenzer, Gabriele"}],"project":[{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"citation":{"ama":"Beyer D, Henzinger TA, Théoduloz G, Zufferey D. Shape refinement through explicit heap analysis. In: Rosenblum D, Taenzer G, eds. Vol 6013. Springer; 2010:263-277. doi:<a href=\"https://doi.org/10.1007/978-3-642-12029-9_19\">10.1007/978-3-642-12029-9_19</a>","apa":"Beyer, D., Henzinger, T. A., Théoduloz, G., &#38; Zufferey, D. (2010). Shape refinement through explicit heap analysis. In D. Rosenblum &#38; G. Taenzer (Eds.) (Vol. 6013, pp. 263–277). Presented at the FASE: Fundamental Approaches To Software Engineering, Paphos, Cyprus: Springer. <a href=\"https://doi.org/10.1007/978-3-642-12029-9_19\">https://doi.org/10.1007/978-3-642-12029-9_19</a>","mla":"Beyer, Dirk, et al. <i>Shape Refinement through Explicit Heap Analysis</i>. Edited by David Rosenblum and Gabriele Taenzer, vol. 6013, Springer, 2010, pp. 263–77, doi:<a href=\"https://doi.org/10.1007/978-3-642-12029-9_19\">10.1007/978-3-642-12029-9_19</a>.","ista":"Beyer D, Henzinger TA, Théoduloz G, Zufferey D. 2010. Shape refinement through explicit heap analysis. FASE: Fundamental Approaches To Software Engineering, LNCS, vol. 6013, 263–277.","short":"D. Beyer, T.A. Henzinger, G. Théoduloz, D. Zufferey, in:, D. Rosenblum, G. Taenzer (Eds.), Springer, 2010, pp. 263–277.","ieee":"D. Beyer, T. A. Henzinger, G. Théoduloz, and D. Zufferey, “Shape refinement through explicit heap analysis,” presented at the FASE: Fundamental Approaches To Software Engineering, Paphos, Cyprus, 2010, vol. 6013, pp. 263–277.","chicago":"Beyer, Dirk, Thomas A Henzinger, Grégory Théoduloz, and Damien Zufferey. “Shape Refinement through Explicit Heap Analysis.” edited by David Rosenblum and Gabriele Taenzer, 6013:263–77. Springer, 2010. <a href=\"https://doi.org/10.1007/978-3-642-12029-9_19\">https://doi.org/10.1007/978-3-642-12029-9_19</a>."},"pubrep_id":"41","abstract":[{"text":"Shape analysis is a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structure. We present a stepwise approach to the selection of instrumentation predicates for a TVLA-based shape analysis, which takes us a step closer towards the fully automatic verification of data structures. The approach uses two techniques to guide the refinement of shape abstractions: (1) during program exploration, an explicit heap analysis collects sample instances of the heap structures, which are used to identify the data structures that are manipulated by the program; and (2) during abstraction refinement along an infeasible error path, we consider different possible heap abstractions and choose the coarsest one that eliminates the infeasible path. We have implemented this combined approach for automatic shape refinement as an extension of the software model checker BLAST. Example programs from a data-structure library that manipulate doubly-linked lists and trees were successfully verified by our tool.","lang":"eng"}],"page":"263 - 277","oa_version":"Submitted Version","publication_status":"published","day":"21","status":"public","date_updated":"2021-01-12T07:56:40Z","volume":6013,"quality_controlled":"1","publist_id":"1061","month":"04","intvolume":"      6013","ddc":["004"],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","conference":{"location":"Paphos, Cyprus","end_date":"2010-03-28","start_date":"2010-03-20","name":"FASE: Fundamental Approaches To Software Engineering"},"file_date_updated":"2020-07-14T12:46:29Z","department":[{"_id":"ToHe"}],"date_created":"2018-12-11T12:08:38Z","date_published":"2010-04-21T00:00:00Z","oa":1,"_id":"4396","author":[{"first_name":"Dirk","full_name":"Beyer, Dirk","last_name":"Beyer"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"full_name":"Théoduloz, Grégory","first_name":"Grégory","last_name":"Théoduloz"},{"id":"4397AC76-F248-11E8-B48F-1D18A9856A87","last_name":"Zufferey","orcid":"0000-0002-3197-8736","full_name":"Zufferey, Damien","first_name":"Damien"}],"type":"conference","publisher":"Springer","year":"2010","language":[{"iso":"eng"}],"doi":"10.1007/978-3-642-12029-9_19"},{"extern":1,"conference":{"name":"CAV: Computer Aided Verification"},"alternative_title":["LNCS 5123"],"date_created":"2018-12-11T12:08:38Z","citation":{"chicago":"Beyer, Dirk, Damien Zufferey, and Ritankar Majumdar. “CSIsat: Interpolation for LA+EUF,” 304–8. Springer, 2008.","ieee":"D. Beyer, D. Zufferey, and R. Majumdar, “CSIsat: Interpolation for LA+EUF,” presented at the CAV: Computer Aided Verification, 2008, pp. 304–308.","mla":"Beyer, Dirk, et al. <i>CSIsat: Interpolation for LA+EUF</i>. Springer, 2008, pp. 304–08.","short":"D. Beyer, D. Zufferey, R. Majumdar, in:, Springer, 2008, pp. 304–308.","ista":"Beyer D, Zufferey D, Majumdar R. 2008. CSIsat: Interpolation for LA+EUF. CAV: Computer Aided Verification, LNCS 5123, , 304–308.","apa":"Beyer, D., Zufferey, D., &#38; Majumdar, R. (2008). CSIsat: Interpolation for LA+EUF (pp. 304–308). Presented at the CAV: Computer Aided Verification, Springer.","ama":"Beyer D, Zufferey D, Majumdar R. CSIsat: Interpolation for LA+EUF. In: Springer; 2008:304-308."},"title":"CSIsat: Interpolation for LA+EUF","month":"01","quality_controlled":0,"publist_id":"1060","status":"public","type":"conference","publisher":"Springer","date_updated":"2021-01-12T07:56:40Z","year":"2008","page":"304 - 308","date_published":"2008-01-01T00:00:00Z","publication_status":"published","day":"01","author":[{"first_name":"Dirk","full_name":"Beyer, Dirk","last_name":"Beyer"},{"orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","last_name":"Zufferey","full_name":"Damien Zufferey","first_name":"Damien"},{"last_name":"Majumdar","full_name":"Majumdar, Ritankar S","first_name":"Ritankar"}],"_id":"4397"}]