[{"date_created":"2018-12-11T11:52:01Z","doi":"10.1145/2837614.2837650","date_published":"2016-01-11T00:00:00Z","page":"400 - 415","day":"11","year":"2016","oa":1,"publisher":"ACM","quality_controlled":"1","acknowledgement":"Damien Zufferey was supported by DARPA (Grants FA8650-11-C-7192 and FA8650-15-C-7564) and NSF (Grant CCF-1138967). ","title":"PSYNC: A partially synchronous language for fault-tolerant distributed algorithms","author":[{"full_name":"Dragoi, Cezara","last_name":"Dragoi","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","first_name":"Cezara"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Zufferey, Damien","orcid":"0000-0002-3197-8736","last_name":"Zufferey","first_name":"Damien","id":"4397AC76-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"5759","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Dragoi, Cezara, et al. PSYNC: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms. Vol. 20–22, ACM, 2016, pp. 400–15, doi:10.1145/2837614.2837650.","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:10.1145/2837614.2837650","apa":"Dragoi, C., Henzinger, T. A., & 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. https://doi.org/10.1145/2837614.2837650","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.","short":"C. Dragoi, T.A. Henzinger, D. Zufferey, in:, ACM, 2016, 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. https://doi.org/10.1145/2837614.2837650.","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."},"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"ec_funded":1,"volume":"20-22","language":[{"iso":"eng"}],"publication_status":"published","month":"01","main_file_link":[{"url":"https://hal.inria.fr/hal-01251199/","open_access":"1"}],"alternative_title":["ACM SIGPLAN Notices"],"scopus_import":1,"oa_version":"Preprint","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. 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."}],"department":[{"_id":"ToHe"}],"date_updated":"2021-01-12T06:50:45Z","status":"public","conference":{"location":"St. Petersburg, FL, USA","end_date":"2016-01-22","start_date":"2016-01-20","name":"POPL: Principles of Programming Languages"},"type":"conference","_id":"1439"},{"oa_version":"Published Version","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. 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.","lang":"eng"}],"intvolume":" 32","month":"01","alternative_title":["LIPIcs"],"scopus_import":1,"language":[{"iso":"eng"}],"file":[{"relation":"main_file","access_level":"open_access","content_type":"application/pdf","checksum":"cf5e94baa89a2dc4c5de01abc676eda8","file_id":"5050","creator":"system","file_size":489362,"date_updated":"2020-07-14T12:44:58Z","file_name":"IST-2016-499-v1+1_9.pdf","date_created":"2018-12-12T10:14:02Z"}],"publication_status":"published","publication_identifier":{"isbn":["978-3-939897-80-4 "]},"ec_funded":1,"volume":32,"series_title":"Leibniz International Proceedings in Informatics","_id":"1498","pubrep_id":"499","status":"public","conference":{"name":"SNAPL: Summit oN Advances in Programming Languages","location":"Asilomar, CA, United States","end_date":"2015-05-06","start_date":"2015-05-03"},"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)"},"type":"conference","ddc":["005"],"date_updated":"2020-08-11T10:09:14Z","file_date_updated":"2020-07-14T12:44:58Z","department":[{"_id":"ToHe"}],"oa":1,"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","day":"01","year":"2015","has_accepted_license":"1","date_created":"2018-12-11T11:52:22Z","date_published":"2015-01-01T00:00:00Z","doi":"10.4230/LIPIcs.SNAPL.2015.90","page":"90 - 102","project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Dragoi, Cezara, et al. The Need for Language Support for Fault-Tolerant Distributed Systems. Vol. 32, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 90–102, doi:10.4230/LIPIcs.SNAPL.2015.90.","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., & 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. https://doi.org/10.4230/LIPIcs.SNAPL.2015.90","ama":"Dragoi C, Henzinger TA, Zufferey D. The need for language support for fault-tolerant distributed systems. 2015;32:90-102. doi:10.4230/LIPIcs.SNAPL.2015.90","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. https://doi.org/10.4230/LIPIcs.SNAPL.2015.90.","ista":"Dragoi C, Henzinger TA, Zufferey D. 2015. The need for language support for fault-tolerant distributed systems. 32, 90–102."},"title":"The need for language support for fault-tolerant distributed systems","publist_id":"5681","author":[{"first_name":"Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","full_name":"Dragoi, Cezara","last_name":"Dragoi"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"orcid":"0000-0002-3197-8736","full_name":"Zufferey, Damien","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","first_name":"Damien"}]},{"abstract":[{"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).","lang":"eng"}],"oa_version":"Submitted Version","alternative_title":["LNCS"],"scopus_import":1,"intvolume":" 8318","month":"01","publication_status":"published","language":[{"iso":"eng"}],"file":[{"file_id":"4859","checksum":"bffa33d39be77df0da39defe97eabf84","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_name":"IST-2014-179-v1+1_vmcai14.pdf","date_created":"2018-12-12T10:11:06Z","file_size":444138,"date_updated":"2020-07-14T12:44:48Z","creator":"system"}],"ec_funded":1,"volume":8318,"_id":"1392","conference":{"start_date":"2014-01-19","end_date":"2014-01-21","location":"San Diego, USA","name":"VMCAI: Verification, Model Checking and Abstract Interpretation"},"type":"conference","pubrep_id":"179","status":"public","date_updated":"2021-01-12T06:50:22Z","ddc":["000","005"],"file_date_updated":"2020-07-14T12:44:48Z","department":[{"_id":"ToHe"}],"acknowledgement":"Supported by the Vienna Science and Technology Fund (WWTF) through grant PROSEED.","oa":1,"quality_controlled":"1","publisher":"Springer","year":"2014","has_accepted_license":"1","day":"01","page":"161 - 181","date_created":"2018-12-11T11:51:45Z","date_published":"2014-01-01T00:00:00Z","doi":"10.1007/978-3-642-54013-4_10","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"}],"citation":{"apa":"Dragoi, C., Henzinger, T. A., Veith, H., Widder, J., & 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. https://doi.org/10.1007/978-3-642-54013-4_10","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:10.1007/978-3-642-54013-4_10","short":"C. Dragoi, T.A. Henzinger, H. Veith, J. Widder, D. Zufferey, in:, Springer, 2014, pp. 161–181.","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.","mla":"Dragoi, Cezara, et al. A Logic-Based Framework for Verifying Consensus Algorithms. Vol. 8318, Springer, 2014, pp. 161–81, doi:10.1007/978-3-642-54013-4_10.","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.","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. https://doi.org/10.1007/978-3-642-54013-4_10."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Dragoi, Cezara","last_name":"Dragoi","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","first_name":"Cezara"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"first_name":"Helmut","last_name":"Veith","full_name":"Veith, Helmut"},{"last_name":"Widder","full_name":"Widder, Josef","first_name":"Josef"},{"full_name":"Zufferey, Damien","orcid":"0000-0002-3197-8736","last_name":"Zufferey","id":"4397AC76-F248-11E8-B48F-1D18A9856A87","first_name":"Damien"}],"publist_id":"5817","title":"A logic-based framework for verifying consensus algorithms"},{"publist_id":"4630","author":[{"id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","first_name":"Cezara","last_name":"Dragoi","full_name":"Dragoi, Cezara"},{"full_name":"Enea, Constantin","last_name":"Enea","first_name":"Constantin"},{"first_name":"Mihaela","last_name":"Sighireanu","full_name":"Sighireanu, Mihaela"}],"title":"Local shape analysis for overlaid data structures","citation":{"apa":"Dragoi, C., Enea, C., & Sighireanu, M. (2013). Local shape analysis for overlaid data structures (Vol. 7935, pp. 150–171). Presented at the SAS: Static Analysis Symposium, Seattle, WA, United States: Springer. https://doi.org/10.1007/978-3-642-38856-9_10","ama":"Dragoi C, Enea C, Sighireanu M. Local shape analysis for overlaid data structures. In: Vol 7935. Springer; 2013:150-171. doi:10.1007/978-3-642-38856-9_10","ieee":"C. Dragoi, C. Enea, and M. Sighireanu, “Local shape analysis for overlaid data structures,” presented at the SAS: Static Analysis Symposium, Seattle, WA, United States, 2013, vol. 7935, pp. 150–171.","short":"C. Dragoi, C. Enea, M. Sighireanu, in:, Springer, 2013, pp. 150–171.","mla":"Dragoi, Cezara, et al. Local Shape Analysis for Overlaid Data Structures. Vol. 7935, Springer, 2013, pp. 150–71, doi:10.1007/978-3-642-38856-9_10.","ista":"Dragoi C, Enea C, Sighireanu M. 2013. Local shape analysis for overlaid data structures. SAS: Static Analysis Symposium, LNCS, vol. 7935, 150–171.","chicago":"Dragoi, Cezara, Constantin Enea, and Mihaela Sighireanu. “Local Shape Analysis for Overlaid Data Structures,” 7935:150–71. Springer, 2013. https://doi.org/10.1007/978-3-642-38856-9_10."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"}],"page":"150 - 171","doi":"10.1007/978-3-642-38856-9_10","date_published":"2013-01-01T00:00:00Z","date_created":"2018-12-11T11:56:50Z","has_accepted_license":"1","year":"2013","day":"01","quality_controlled":"1","publisher":"Springer","oa":1,"file_date_updated":"2020-07-14T12:45:37Z","department":[{"_id":"ToHe"}],"date_updated":"2021-01-12T06:56:36Z","ddc":["000","004"],"type":"conference","conference":{"name":"SAS: Static Analysis Symposium","location":"Seattle, WA, United States","end_date":"2013-06-22","start_date":"2013-06-20"},"status":"public","pubrep_id":"196","_id":"2298","volume":7935,"ec_funded":1,"publication_status":"published","file":[{"creator":"system","date_updated":"2020-07-14T12:45:37Z","file_size":299004,"date_created":"2018-12-12T10:10:36Z","file_name":"IST-2014-196-v1+1_sas13.pdf","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_id":"4824","checksum":"907edd33a5892e3af093365f1fd57ed7"}],"language":[{"iso":"eng"}],"alternative_title":["LNCS"],"scopus_import":1,"month":"01","intvolume":" 7935","abstract":[{"lang":"eng","text":"We present a shape analysis for programs that manipulate overlaid data structures which share sets of objects. The abstract domain contains Separation Logic formulas that (1) combine a per-object separating conjunction with a per-field separating conjunction and (2) constrain a set of variables interpreted as sets of objects. The definition of the abstract domain operators is based on a notion of homomorphism between formulas, viewed as graphs, used recently to define optimal decision procedures for fragments of the Separation Logic. Based on a Frame Rule that supports the two versions of the separating conjunction, the analysis is able to reason in a modular manner about non-overlaid data structures and then, compose information only at a few program points, e.g., procedure returns. We have implemented this analysis in a prototype tool and applied it on several interesting case studies that manipulate overlaid and nested linked lists.\r\n"}],"oa_version":"Submitted Version"},{"oa":1,"publisher":"Springer Berlin Heidelberg","quality_controlled":"1","page":"174-190","date_created":"2018-12-18T13:10:21Z","date_published":"2013-01-01T00:00:00Z","doi":"10.1007/978-3-642-39799-8_11","year":"2013","has_accepted_license":"1","publication":"Computer Aided Verification","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"article_processing_charge":"No","author":[{"first_name":"Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","full_name":"Dragoi, Cezara","last_name":"Dragoi"},{"last_name":"Gupta","full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"title":"Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates","citation":{"ista":"Dragoi C, Gupta A, Henzinger TA. 2013.Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In: Computer Aided Verification. vol. 8044, 174–190.","chicago":"Dragoi, Cezara, Ashutosh Gupta, and Thomas A Henzinger. “Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates.” In Computer Aided Verification, 8044:174–90. CAV. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013. https://doi.org/10.1007/978-3-642-39799-8_11.","ama":"Dragoi C, Gupta A, Henzinger TA. Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In: Computer Aided Verification. Vol 8044. CAV. Berlin, Heidelberg: Springer Berlin Heidelberg; 2013:174-190. doi:10.1007/978-3-642-39799-8_11","apa":"Dragoi, C., Gupta, A., & Henzinger, T. A. (2013). Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In Computer Aided Verification (Vol. 8044, pp. 174–190). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_11","short":"C. Dragoi, A. Gupta, T.A. Henzinger, in:, Computer Aided Verification, Springer Berlin Heidelberg, Berlin, Heidelberg, 2013, pp. 174–190.","ieee":"C. Dragoi, A. Gupta, and T. A. Henzinger, “Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates,” in Computer Aided Verification, vol. 8044, Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 174–190.","mla":"Dragoi, Cezara, et al. “Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates.” Computer Aided Verification, vol. 8044, Springer Berlin Heidelberg, 2013, pp. 174–90, doi:10.1007/978-3-642-39799-8_11."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","scopus_import":"1","intvolume":" 8044","place":"Berlin, Heidelberg","oa_version":"None","ec_funded":1,"volume":8044,"publication_status":"published","publication_identifier":{"issn":["0302-9743"],"isbn":["9783642397981","9783642397998"],"eissn":["1611-3349"]},"language":[{"iso":"eng"}],"file":[{"date_updated":"2020-07-14T12:47:10Z","file_size":236480,"creator":"dernst","date_created":"2018-12-18T13:13:33Z","file_name":"2013_CAV_Dragoi.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"5748","checksum":"a901cc6b71db08b61c0d4c0cbacc6287"}],"conference":{"start_date":"2013-07-13","end_date":"2013-07-19","location":"Saint Petersburg, Russia","name":"CAV 2013"},"type":"book_chapter","pubrep_id":"195","status":"public","_id":"5747","series_title":"CAV","file_date_updated":"2020-07-14T12:47:10Z","department":[{"_id":"ToHe"}],"date_updated":"2023-09-05T14:16:07Z","ddc":["005"]},{"_id":"3253","status":"public","type":"conference","conference":{"name":"VMCAI: Verification, Model Checking and Abstract Interpretation","start_date":"2012-01-22","location":"Philadelphia, PA, USA","end_date":"2012-01-24"},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"apa":"Bouajjani, A., Dragoi, C., Enea, C., & 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. https://doi.org/10.1007/978-3-642-27940-9_1","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:10.1007/978-3-642-27940-9_1","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.","mla":"Bouajjani, Ahmed, et al. Abstract Domains for Automated Reasoning about List Manipulating Programs with Infinite Data. Vol. 7148, Springer, 2012, pp. 1–22, doi:10.1007/978-3-642-27940-9_1.","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.","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. https://doi.org/10.1007/978-3-642-27940-9_1."},"date_updated":"2021-01-12T07:42:09Z","title":"Abstract domains for automated reasoning about list manipulating programs with infinite data","department":[{"_id":"ToHe"}],"publist_id":"3404","author":[{"full_name":"Bouajjani, Ahmed","last_name":"Bouajjani","first_name":"Ahmed"},{"full_name":"Dragoi, Cezara","last_name":"Dragoi","first_name":"Cezara","id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Constantin","full_name":"Enea, Constantin","last_name":"Enea"},{"full_name":"Sighireanu, Mihaela","last_name":"Sighireanu","first_name":"Mihaela"}],"oa_version":"None","acknowledgement":"This work was partly supported by the French National Research Agency (ANR) project Veridyc (ANR-09-SEGI-016).","abstract":[{"lang":"eng","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."}],"month":"02","intvolume":" 7148","alternative_title":["LNCS"],"quality_controlled":"1","publisher":"Springer","day":"26","language":[{"iso":"eng"}],"year":"2012","publication_status":"published","doi":"10.1007/978-3-642-27940-9_1","date_published":"2012-02-26T00:00:00Z","volume":7148,"date_created":"2018-12-11T12:02:17Z","page":"1 - 22"},{"year":"2012","publication":"Automated Technology for Verification and Analysis","day":"15","page":"167-182","date_created":"2022-03-21T07:58:39Z","doi":"10.1007/978-3-642-33386-6_14","date_published":"2012-10-15T00:00:00Z","acknowledgement":"This work has been partially supported by the French ANR project Veridyc","quality_controlled":"1","publisher":"Springer","citation":{"chicago":"Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” In Automated Technology for Verification and Analysis, 7561:167–82. LNCS. Berlin, Heidelberg: Springer, 2012. https://doi.org/10.1007/978-3-642-33386-6_14.","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.","mla":"Bouajjani, Ahmed, et al. “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.” Automated Technology for Verification and Analysis, vol. 7561, Springer, 2012, pp. 167–82, doi:10.1007/978-3-642-33386-6_14.","ama":"Bouajjani A, Dragoi C, Enea C, Sighireanu M. Accurate invariant checking for programs manipulating lists and arrays with infinite data. In: Automated Technology for Verification and Analysis. Vol 7561. LNCS. Berlin, Heidelberg: Springer; 2012:167-182. doi:10.1007/978-3-642-33386-6_14","apa":"Bouajjani, A., Dragoi, C., Enea, C., & Sighireanu, M. (2012). Accurate invariant checking for programs manipulating lists and arrays with infinite data. In Automated Technology for Verification and Analysis (Vol. 7561, pp. 167–182). Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-33386-6_14","short":"A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Automated Technology for Verification and Analysis, Springer, Berlin, Heidelberg, 2012, pp. 167–182.","ieee":"A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Accurate invariant checking for programs manipulating lists and arrays with infinite data,” in Automated Technology for Verification and Analysis, Thiruvananthapuram, India, 2012, vol. 7561, pp. 167–182."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","article_processing_charge":"No","author":[{"full_name":"Bouajjani, Ahmed","last_name":"Bouajjani","first_name":"Ahmed"},{"id":"2B2B5ED0-F248-11E8-B48F-1D18A9856A87","first_name":"Cezara","last_name":"Dragoi","full_name":"Dragoi, Cezara"},{"first_name":"Constantin","last_name":"Enea","full_name":"Enea, Constantin"},{"first_name":"Mihaela","full_name":"Sighireanu, Mihaela","last_name":"Sighireanu"}],"title":"Accurate invariant checking for programs manipulating lists and arrays with infinite data","publication_status":"published","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783642333859"],"issn":["0302-9743"],"eisbn":["9783642333866"]},"language":[{"iso":"eng"}],"volume":7561,"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."}],"oa_version":"None","alternative_title":["LNCS"],"scopus_import":"1","intvolume":" 7561","place":"Berlin, Heidelberg","month":"10","date_updated":"2023-09-05T14:07:24Z","department":[{"_id":"ToHe"}],"series_title":"LNCS","_id":"10903","conference":{"name":"ATVA: Automated Technology for Verification and Analysis","location":"Thiruvananthapuram, India","end_date":"2012-10-06","start_date":"2012-10-03"},"type":"conference","status":"public"}]