[{"year":"2021","acknowledgement":"This research was performed while Bernhard Kragl was at IST Austria, supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","department":[{"_id":"ToHe"}],"publisher":"TU Wien Academic Press","editor":[{"full_name":"Ruzica, Piskac","last_name":"Ruzica","first_name":"Piskac"},{"first_name":"Michael W.","last_name":"Whalen","full_name":"Whalen, Michael W."}],"publication_status":"published","author":[{"id":"320FC952-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7745-9117","first_name":"Bernhard","last_name":"Kragl","full_name":"Kragl, Bernhard"},{"first_name":"Shaz","last_name":"Qadeer","full_name":"Qadeer, Shaz"}],"volume":2,"date_created":"2022-01-26T08:01:30Z","date_updated":"2022-01-26T08:20:41Z","file_date_updated":"2022-01-26T08:04:29Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"quality_controlled":"1","doi":"10.34727/2021/isbn.978-3-85448-046-4_23","conference":{"name":"FMCAD: Formal Methods in Computer-Aided Design","end_date":"2021-10-22","location":"Virtual","start_date":"2021-10-20"},"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-3-85448-046-4"]},"month":"10","_id":"10688","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","intvolume":" 2","title":"The Civl verifier","ddc":["000"],"status":"public","oa_version":"Published Version","file":[{"creator":"cchlebak","file_size":390555,"content_type":"application/pdf","file_name":"2021_FCAD2021_Kragl.pdf","access_level":"open_access","date_created":"2022-01-26T08:04:29Z","date_updated":"2022-01-26T08:04:29Z","success":1,"checksum":"35438ac9f9750340b7f8ae4ae3220d9f","file_id":"10689","relation":"main_file"}],"type":"conference","alternative_title":["Conference Series"],"abstract":[{"text":"Civl is a static verifier for concurrent programs designed around the conceptual framework of layered refinement,\r\nwhich views the task of verifying a program as a sequence of program simplification steps each justified by its own invariant. Civl verifies a layered concurrent program that compactly expresses all the programs in this sequence and the supporting invariants. This paper presents the design and implementation of the Civl verifier.","lang":"eng"}],"citation":{"apa":"Kragl, B., & Qadeer, S. (2021). The Civl verifier. In P. Ruzica & M. W. Whalen (Eds.), Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design (Vol. 2, pp. 143–152). Virtual: TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23","ieee":"B. Kragl and S. Qadeer, “The Civl verifier,” in Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design, Virtual, 2021, vol. 2, pp. 143–152.","ista":"Kragl B, Qadeer S. 2021. The Civl verifier. Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, Conference Series, vol. 2, 143–152.","ama":"Kragl B, Qadeer S. The Civl verifier. In: Ruzica P, Whalen MW, eds. Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design. Vol 2. TU Wien Academic Press; 2021:143–152. doi:10.34727/2021/isbn.978-3-85448-046-4_23","chicago":"Kragl, Bernhard, and Shaz Qadeer. “The Civl Verifier.” In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design, edited by Piskac Ruzica and Michael W. Whalen, 2:143–152. TU Wien Academic Press, 2021. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23.","short":"B. Kragl, S. Qadeer, in:, P. Ruzica, M.W. Whalen (Eds.), Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design, TU Wien Academic Press, 2021, pp. 143–152.","mla":"Kragl, Bernhard, and Shaz Qadeer. “The Civl Verifier.” Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design, edited by Piskac Ruzica and Michael W. Whalen, vol. 2, TU Wien Academic Press, 2021, pp. 143–152, doi:10.34727/2021/isbn.978-3-85448-046-4_23."},"publication":"Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design","page":"143–152","date_published":"2021-10-01T00:00:00Z","article_processing_charge":"No","has_accepted_license":"1","day":"01"},{"type":"conference","alternative_title":["LIPIcs"],"abstract":[{"text":"The monitoring of event frequencies can be used to recognize behavioral anomalies, to identify trends, and to deduce or discard hypotheses about the underlying system. For example, the performance of a web server may be monitored based on the ratio of the total count of requests from the least and most active clients. Exact frequency monitoring, however, can be prohibitively expensive; in the above example it would require as many counters as there are clients. In this paper, we propose the efficient probabilistic monitoring of common frequency properties, including the mode (i.e., the most common event) and the median of an event sequence. We define a logic to express composite frequency properties as a combination of atomic frequency properties. Our main contribution is an algorithm that, under suitable probabilistic assumptions, can be used to monitor these important frequency properties with four counters, independent of the number of different events. Our algorithm samples longer and longer subwords of an infinite event sequence. We prove the almost-sure convergence of our algorithm by generalizing ergodic theory from increasing-length prefixes to increasing-length subwords of an infinite sequence. A similar algorithm could be used to learn a connected Markov chain of a given structure from observing its outputs, to arbitrary precision, for a given confidence. ","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"7348","intvolume":" 152","title":"Monitoring event frequencies","ddc":["000"],"status":"public","file":[{"checksum":"b9a691d658d075c6369d3304d17fb818","date_updated":"2020-07-14T12:47:56Z","date_created":"2020-01-21T11:21:04Z","relation":"main_file","file_id":"7349","content_type":"application/pdf","file_size":617206,"creator":"bkragl","access_level":"open_access","file_name":"main.pdf"}],"oa_version":"Published Version","scopus_import":1,"has_accepted_license":"1","article_processing_charge":"No","day":"15","citation":{"ista":"Ferrere T, Henzinger TA, Kragl B. 2020. Monitoring event frequencies. 28th EACSL Annual Conference on Computer Science Logic. CSL: Computer Science Logic, LIPIcs, vol. 152, 20.","apa":"Ferrere, T., Henzinger, T. A., & Kragl, B. (2020). Monitoring event frequencies. In 28th EACSL Annual Conference on Computer Science Logic (Vol. 152). Barcelona, Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2020.20","ieee":"T. Ferrere, T. A. Henzinger, and B. Kragl, “Monitoring event frequencies,” in 28th EACSL Annual Conference on Computer Science Logic, Barcelona, Spain, 2020, vol. 152.","ama":"Ferrere T, Henzinger TA, Kragl B. Monitoring event frequencies. In: 28th EACSL Annual Conference on Computer Science Logic. Vol 152. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:10.4230/LIPIcs.CSL.2020.20","chicago":"Ferrere, Thomas, Thomas A Henzinger, and Bernhard Kragl. “Monitoring Event Frequencies.” In 28th EACSL Annual Conference on Computer Science Logic, Vol. 152. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.CSL.2020.20.","mla":"Ferrere, Thomas, et al. “Monitoring Event Frequencies.” 28th EACSL Annual Conference on Computer Science Logic, vol. 152, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:10.4230/LIPIcs.CSL.2020.20.","short":"T. Ferrere, T.A. Henzinger, B. Kragl, in:, 28th EACSL Annual Conference on Computer Science Logic, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020."},"publication":"28th EACSL Annual Conference on Computer Science Logic","date_published":"2020-01-15T00:00:00Z","article_number":"20","file_date_updated":"2020-07-14T12:47:56Z","year":"2020","department":[{"_id":"ToHe"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication_status":"published","author":[{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5199-3143","first_name":"Thomas","last_name":"Ferrere","full_name":"Ferrere, Thomas"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Kragl, Bernhard","last_name":"Kragl","first_name":"Bernhard","orcid":"0000-0001-7745-9117","id":"320FC952-F248-11E8-B48F-1D18A9856A87"}],"volume":152,"date_created":"2020-01-21T11:22:21Z","date_updated":"2021-01-12T08:13:12Z","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959771320"]},"month":"01","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"arxiv":["1910.06097"]},"oa":1,"project":[{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF"}],"quality_controlled":"1","doi":"10.4230/LIPIcs.CSL.2020.20","conference":{"name":"CSL: Computer Science Logic","start_date":"2020-01-13","location":"Barcelona, Spain","end_date":"2020-01-16"},"language":[{"iso":"eng"}]},{"author":[{"id":"320FC952-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7745-9117","first_name":"Bernhard","last_name":"Kragl","full_name":"Kragl, Bernhard"},{"first_name":"Shaz","last_name":"Qadeer","full_name":"Qadeer, Shaz"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"8332"}]},"date_created":"2020-08-03T11:45:35Z","date_updated":"2023-09-07T13:18:00Z","volume":12224,"year":"2020","acknowledgement":"Bernhard Kragl and Thomas A. Henzinger were supported by\r\nthe Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer Nature","file_date_updated":"2020-08-06T08:14:54Z","doi":"10.1007/978-3-030-53288-8_14","language":[{"iso":"eng"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"external_id":{"isi":["000695276000014"]},"isi":1,"quality_controlled":"1","project":[{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"month":"07","publication_identifier":{"eisbn":["9783030532888"],"issn":["0302-9743"],"isbn":["9783030532871"],"eissn":["1611-3349"]},"oa_version":"Published Version","file":[{"access_level":"open_access","file_name":"2020_LNCS_Kragl.pdf","creator":"dernst","file_size":804237,"content_type":"application/pdf","file_id":"8201","relation":"main_file","success":1,"date_updated":"2020-08-06T08:14:54Z","date_created":"2020-08-06T08:14:54Z"}],"_id":"8195","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","ddc":["000"],"status":"public","title":"Refinement for structured concurrent programs","intvolume":" 12224","abstract":[{"text":"This paper presents a foundation for refining concurrent programs with structured control flow. The verification problem is decomposed into subproblems that aid interactive program development, proof reuse, and automation. The formalization in this paper is the basis of a new design and implementation of the Civl verifier.","lang":"eng"}],"type":"conference","alternative_title":["LNCS"],"date_published":"2020-07-14T00:00:00Z","publication":"Computer Aided Verification","citation":{"short":"B. Kragl, S. Qadeer, T.A. Henzinger, in:, Computer Aided Verification, Springer Nature, 2020, pp. 275–298.","mla":"Kragl, Bernhard, et al. “Refinement for Structured Concurrent Programs.” Computer Aided Verification, vol. 12224, Springer Nature, 2020, pp. 275–98, doi:10.1007/978-3-030-53288-8_14.","chicago":"Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Refinement for Structured Concurrent Programs.” In Computer Aided Verification, 12224:275–98. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-53288-8_14.","ama":"Kragl B, Qadeer S, Henzinger TA. Refinement for structured concurrent programs. In: Computer Aided Verification. Vol 12224. Springer Nature; 2020:275-298. doi:10.1007/978-3-030-53288-8_14","apa":"Kragl, B., Qadeer, S., & Henzinger, T. A. (2020). Refinement for structured concurrent programs. In Computer Aided Verification (Vol. 12224, pp. 275–298). Springer Nature. https://doi.org/10.1007/978-3-030-53288-8_14","ieee":"B. Kragl, S. Qadeer, and T. A. Henzinger, “Refinement for structured concurrent programs,” in Computer Aided Verification, 2020, vol. 12224, pp. 275–298.","ista":"Kragl B, Qadeer S, Henzinger TA. 2020. Refinement for structured concurrent programs. Computer Aided Verification. , LNCS, vol. 12224, 275–298."},"page":"275-298","day":"14","article_processing_charge":"No","has_accepted_license":"1","scopus_import":"1"},{"date_updated":"2023-09-07T13:18:00Z","date_created":"2020-06-25T11:40:16Z","related_material":{"record":[{"id":"8332","status":"public","relation":"dissertation_contains"}]},"author":[{"last_name":"Kragl","first_name":"Bernhard","orcid":"0000-0001-7745-9117","id":"320FC952-F248-11E8-B48F-1D18A9856A87","full_name":"Kragl, Bernhard"},{"full_name":"Enea, Constantin","first_name":"Constantin","last_name":"Enea"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"},{"full_name":"Mutluergil, Suha Orhun","first_name":"Suha Orhun","last_name":"Mutluergil"},{"full_name":"Qadeer, Shaz","first_name":"Shaz","last_name":"Qadeer"}],"publisher":"Association for Computing Machinery","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2020","publication_identifier":{"isbn":["9781450376136"]},"month":"06","language":[{"iso":"eng"}],"doi":"10.1145/3385412.3385980","conference":{"name":"PLDI: Programming Language Design and Implementation","end_date":"2020-06-20","start_date":"2020-06-15","location":"London, United Kingdom"},"project":[{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"isi":1,"quality_controlled":"1","external_id":{"isi":["000614622300016"]},"oa":1,"main_file_link":[{"url":"https://doi.org/10.1145/3385412.3385980","open_access":"1"}],"abstract":[{"text":"Asynchronous programs are notoriously difficult to reason about because they spawn computation tasks which take effect asynchronously in a nondeterministic way. Devising inductive invariants for such programs requires understanding and stating complex relationships between an unbounded number of computation tasks in arbitrarily long executions. In this paper, we introduce inductive sequentialization, a new proof rule that sidesteps this complexity via a sequential reduction, a sequential program that captures every behavior of the original program up to reordering of coarse-grained commutative actions. A sequential reduction of a concurrent program is easy to reason about since it corresponds to a simple execution of the program in an idealized synchronous environment, where processes act in a fixed order and at the same speed. We have implemented and integrated our proof rule in the CIVL verifier, allowing us to provably derive fine-grained implementations of asynchronous programs. We have successfully applied our proof rule to a diverse set of message-passing protocols, including leader election protocols, two-phase commit, and Paxos.","lang":"eng"}],"type":"conference","oa_version":"Published Version","status":"public","title":"Inductive sequentialization of asynchronous programs","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","_id":"8012","article_processing_charge":"No","day":"01","scopus_import":"1","date_published":"2020-06-01T00:00:00Z","page":"227-242","citation":{"chicago":"Kragl, Bernhard, Constantin Enea, Thomas A Henzinger, Suha Orhun Mutluergil, and Shaz Qadeer. “Inductive Sequentialization of Asynchronous Programs.” In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, 227–42. Association for Computing Machinery, 2020. https://doi.org/10.1145/3385412.3385980.","mla":"Kragl, Bernhard, et al. “Inductive Sequentialization of Asynchronous Programs.” Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2020, pp. 227–42, doi:10.1145/3385412.3385980.","short":"B. Kragl, C. Enea, T.A. Henzinger, S.O. Mutluergil, S. Qadeer, in:, Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2020, pp. 227–242.","ista":"Kragl B, Enea C, Henzinger TA, Mutluergil SO, Qadeer S. 2020. Inductive sequentialization of asynchronous programs. Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 227–242.","apa":"Kragl, B., Enea, C., Henzinger, T. A., Mutluergil, S. O., & Qadeer, S. (2020). Inductive sequentialization of asynchronous programs. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 227–242). London, United Kingdom: Association for Computing Machinery. https://doi.org/10.1145/3385412.3385980","ieee":"B. Kragl, C. Enea, T. A. Henzinger, S. O. Mutluergil, and S. Qadeer, “Inductive sequentialization of asynchronous programs,” in Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, London, United Kingdom, 2020, pp. 227–242.","ama":"Kragl B, Enea C, Henzinger TA, Mutluergil SO, Qadeer S. Inductive sequentialization of asynchronous programs. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery; 2020:227-242. doi:10.1145/3385412.3385980"},"publication":"Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation"},{"publication_identifier":{"issn":["2663-337X"]},"month":"09","language":[{"iso":"eng"}],"supervisor":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"}],"degree_awarded":"PhD","doi":"10.15479/AT:ISTA:8332","oa":1,"file_date_updated":"2020-09-04T13:00:17Z","date_updated":"2023-09-13T08:45:08Z","date_created":"2020-09-04T12:24:12Z","related_material":{"record":[{"id":"133","relation":"part_of_dissertation","status":"public"},{"id":"8012","status":"public","relation":"part_of_dissertation"},{"id":"8195","relation":"part_of_dissertation","status":"public"},{"id":"160","status":"public","relation":"part_of_dissertation"}]},"author":[{"orcid":"0000-0001-7745-9117","id":"320FC952-F248-11E8-B48F-1D18A9856A87","last_name":"Kragl","first_name":"Bernhard","full_name":"Kragl, Bernhard"}],"publisher":"Institute of Science and Technology Austria","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2020","article_processing_charge":"No","has_accepted_license":"1","day":"03","date_published":"2020-09-03T00:00:00Z","page":"120","citation":{"short":"B. Kragl, Verifying Concurrent Programs: Refinement, Synchronization, Sequentialization, Institute of Science and Technology Austria, 2020.","mla":"Kragl, Bernhard. Verifying Concurrent Programs: Refinement, Synchronization, Sequentialization. Institute of Science and Technology Austria, 2020, doi:10.15479/AT:ISTA:8332.","chicago":"Kragl, Bernhard. “Verifying Concurrent Programs: Refinement, Synchronization, Sequentialization.” Institute of Science and Technology Austria, 2020. https://doi.org/10.15479/AT:ISTA:8332.","ama":"Kragl B. Verifying concurrent programs: Refinement, synchronization, sequentialization. 2020. doi:10.15479/AT:ISTA:8332","ieee":"B. Kragl, “Verifying concurrent programs: Refinement, synchronization, sequentialization,” Institute of Science and Technology Austria, 2020.","apa":"Kragl, B. (2020). Verifying concurrent programs: Refinement, synchronization, sequentialization. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:8332","ista":"Kragl B. 2020. Verifying concurrent programs: Refinement, synchronization, sequentialization. Institute of Science and Technology Austria."},"abstract":[{"lang":"eng","text":"Designing and verifying concurrent programs is a notoriously challenging, time consuming, and error prone task, even for experts. This is due to the sheer number of possible interleavings of a concurrent program, all of which have to be tracked and accounted for in a formal proof. Inventing an inductive invariant that captures all interleavings of a low-level implementation is theoretically possible, but practically intractable. We develop a refinement-based verification framework that provides mechanisms to simplify proof construction by decomposing the verification task into smaller subtasks.\r\n\r\nIn a first line of work, we present a foundation for refinement reasoning over structured concurrent programs. We introduce layered concurrent programs as a compact notation to represent multi-layer refinement proofs. A layered concurrent program specifies a sequence of connected concurrent programs, from most concrete to most abstract, such that common parts of different programs are written exactly once. Each program in this sequence is expressed as structured concurrent program, i.e., a program over (potentially recursive) procedures, imperative control flow, gated atomic actions, structured parallelism, and asynchronous concurrency. This is in contrast to existing refinement-based verifiers, which represent concurrent systems as flat transition relations. We present a powerful refinement proof rule that decomposes refinement checking over structured programs into modular verification conditions. Refinement checking is supported by a new form of modular, parameterized invariants, called yield invariants, and a linear permission system to enhance local reasoning.\r\n\r\nIn a second line of work, we present two new reduction-based program transformations that target asynchronous programs. These transformations reduce the number of interleavings that need to be considered, thus reducing the complexity of invariants. Synchronization simplifies the verification of asynchronous programs by introducing the fiction, for proof purposes, that asynchronous operations complete synchronously. Synchronization summarizes an asynchronous computation as immediate atomic effect. Inductive sequentialization establishes sequential reductions that captures every behavior of the original program up to reordering of coarse-grained commutative actions. A sequential reduction of a concurrent program is easy to reason about since it corresponds to a simple execution of the program in an idealized synchronous environment, where processes act in a fixed order and at the same speed.\r\n\r\nOur approach is implemented the CIVL verifier, which has been successfully used for the verification of several complex concurrent programs. In our methodology, the overall correctness of a program is established piecemeal by focusing on the invariant required for each refinement step separately. While the programmer does the creative work of specifying the chain of programs and the inductive invariant justifying each link in the chain, the tool automatically constructs the verification conditions underlying each refinement step."}],"alternative_title":["ISTA Thesis"],"type":"dissertation","oa_version":"Published Version","file":[{"checksum":"26fe261550f691280bda4c454bf015c7","date_updated":"2020-09-04T12:17:47Z","date_created":"2020-09-04T12:17:47Z","relation":"main_file","file_id":"8333","content_type":"application/pdf","file_size":1348815,"creator":"bkragl","access_level":"open_access","file_name":"kragl-thesis.pdf"},{"date_updated":"2020-09-04T13:00:17Z","date_created":"2020-09-04T13:00:17Z","checksum":"b9694ce092b7c55557122adba8337ebc","relation":"source_file","file_id":"8335","file_size":372312,"content_type":"application/zip","creator":"bkragl","file_name":"kragl-thesis.zip","access_level":"closed"}],"status":"public","ddc":["000"],"title":"Verifying concurrent programs: Refinement, synchronization, sequentialization","_id":"8332","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1"},{"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"}],"quality_controlled":"1","doi":"10.4230/LIPIcs.CONCUR.2018.21","conference":{"start_date":"2018-09-04","location":"Beijing, China","end_date":"2018-09-07","name":"CONCUR: International Conference on Concurrency Theory"},"language":[{"iso":"eng"}],"publication_identifier":{"issn":["18688969"]},"month":"08","year":"2018","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"ToHe"}],"publication_status":"published","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"6426"},{"status":"public","relation":"dissertation_contains","id":"8332"}]},"author":[{"orcid":"0000-0001-7745-9117","id":"320FC952-F248-11E8-B48F-1D18A9856A87","last_name":"Kragl","first_name":"Bernhard","full_name":"Kragl, Bernhard"},{"first_name":"Shaz","last_name":"Qadeer","full_name":"Qadeer, Shaz"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"volume":118,"date_created":"2018-12-11T11:44:48Z","date_updated":"2023-09-07T13:18:00Z","article_number":"21","publist_id":"7790","file_date_updated":"2020-07-14T12:44:44Z","citation":{"chicago":"Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Synchronizing the Asynchronous,” Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. https://doi.org/10.4230/LIPIcs.CONCUR.2018.21.","short":"B. Kragl, S. Qadeer, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","mla":"Kragl, Bernhard, et al. Synchronizing the Asynchronous. Vol. 118, 21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:10.4230/LIPIcs.CONCUR.2018.21.","ieee":"B. Kragl, S. Qadeer, and T. A. Henzinger, “Synchronizing the asynchronous,” presented at the CONCUR: International Conference on Concurrency Theory, Beijing, China, 2018, vol. 118.","apa":"Kragl, B., Qadeer, S., & Henzinger, T. A. (2018). Synchronizing the asynchronous (Vol. 118). Presented at the CONCUR: International Conference on Concurrency Theory, Beijing, China: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2018.21","ista":"Kragl B, Qadeer S, Henzinger TA. 2018. Synchronizing the asynchronous. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 118, 21.","ama":"Kragl B, Qadeer S, Henzinger TA. Synchronizing the asynchronous. In: Vol 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:10.4230/LIPIcs.CONCUR.2018.21"},"date_published":"2018-08-13T00:00:00Z","scopus_import":1,"has_accepted_license":"1","day":"13","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"133","intvolume":" 118","title":"Synchronizing the asynchronous","status":"public","ddc":["000"],"pubrep_id":"1039","file":[{"content_type":"application/pdf","file_size":745438,"creator":"system","file_name":"IST-2018-853-v2+2_concur2018.pdf","access_level":"open_access","date_updated":"2020-07-14T12:44:44Z","date_created":"2018-12-12T10:18:46Z","checksum":"c90895f4c5fafc18ddc54d1c8848077e","relation":"main_file","file_id":"5368"}],"oa_version":"Published Version","type":"conference","alternative_title":["LIPIcs"],"abstract":[{"lang":"eng","text":"Synchronous programs are easy to specify because the side effects of an operation are finished by the time the invocation of the operation returns to the caller. Asynchronous programs, on the other hand, are difficult to specify because there are side effects due to pending computation scheduled as a result of the invocation of an operation. They are also difficult to verify because of the large number of possible interleavings of concurrent computation threads. We present synchronization, a new proof rule that simplifies the verification of asynchronous programs by introducing the fiction, for proof purposes, that asynchronous operations complete synchronously. Synchronization summarizes an asynchronous computation as immediate atomic effect. Modular verification is enabled via pending asynchronous calls in atomic summaries, and a complementary proof rule that eliminates pending asynchronous calls when components and their specifications are composed. We evaluate synchronization in the context of a multi-layer refinement verification methodology on a collection of benchmark programs."}]},{"intvolume":" 10981","ddc":["000"],"title":"Layered Concurrent Programs","status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"160","oa_version":"Published Version","file":[{"file_id":"5705","relation":"main_file","date_updated":"2020-07-14T12:45:04Z","date_created":"2018-12-17T12:52:12Z","checksum":"c64fff560fe5a7532ec10626ad1c215e","file_name":"2018_LNCS_Kragl.pdf","access_level":"open_access","creator":"dernst","content_type":"application/pdf","file_size":1603844}],"alternative_title":["LNCS"],"type":"conference","abstract":[{"lang":"eng","text":"We present layered concurrent programs, a compact and expressive notation for specifying refinement proofs of concurrent programs. A layered concurrent program specifies a sequence of connected concurrent programs, from most concrete to most abstract, such that common parts of different programs are written exactly once. These programs are expressed in the ordinary syntax of imperative concurrent programs using gated atomic actions, sequencing, choice, and (recursive) procedure calls. Each concurrent program is automatically extracted from the layered program. We reduce refinement to the safety of a sequence of concurrent checker programs, one each to justify the connection between every two consecutive concurrent programs. These checker programs are also automatically extracted from the layered program. Layered concurrent programs have been implemented in the CIVL verifier which has been successfully used for the verification of several complex concurrent programs."}],"page":"79 - 102","citation":{"ista":"Kragl B, Qadeer S. 2018. Layered Concurrent Programs. CAV: Computer Aided Verification, LNCS, vol. 10981, 79–102.","apa":"Kragl, B., & Qadeer, S. (2018). Layered Concurrent Programs (Vol. 10981, pp. 79–102). Presented at the CAV: Computer Aided Verification, Oxford, UK: Springer. https://doi.org/10.1007/978-3-319-96145-3_5","ieee":"B. Kragl and S. Qadeer, “Layered Concurrent Programs,” presented at the CAV: Computer Aided Verification, Oxford, UK, 2018, vol. 10981, pp. 79–102.","ama":"Kragl B, Qadeer S. Layered Concurrent Programs. In: Vol 10981. Springer; 2018:79-102. doi:10.1007/978-3-319-96145-3_5","chicago":"Kragl, Bernhard, and Shaz Qadeer. “Layered Concurrent Programs,” 10981:79–102. Springer, 2018. https://doi.org/10.1007/978-3-319-96145-3_5.","mla":"Kragl, Bernhard, and Shaz Qadeer. Layered Concurrent Programs. Vol. 10981, Springer, 2018, pp. 79–102, doi:10.1007/978-3-319-96145-3_5.","short":"B. Kragl, S. Qadeer, in:, Springer, 2018, pp. 79–102."},"date_published":"2018-07-18T00:00:00Z","scopus_import":"1","has_accepted_license":"1","article_processing_charge":"No","day":"18","department":[{"_id":"ToHe"}],"publisher":"Springer","publication_status":"published","year":"2018","volume":10981,"date_updated":"2023-09-13T08:45:09Z","date_created":"2018-12-11T11:44:57Z","related_material":{"record":[{"id":"8332","relation":"dissertation_contains","status":"public"}]},"author":[{"full_name":"Kragl, Bernhard","first_name":"Bernhard","last_name":"Kragl","id":"320FC952-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7745-9117"},{"full_name":"Qadeer, Shaz","last_name":"Qadeer","first_name":"Shaz"}],"publist_id":"7761","file_date_updated":"2020-07-14T12:45:04Z","project":[{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"isi":1,"quality_controlled":"1","external_id":{"isi":["000491481600005"]},"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-96145-3_5","conference":{"end_date":"2018-07-17","start_date":"2018-07-14","location":"Oxford, UK","name":"CAV: Computer Aided Verification"},"month":"07"},{"oa":1,"citation":{"ama":"Henzinger TA, Kragl B, Qadeer S. Synchronizing the Asynchronous. IST Austria; 2017. doi:10.15479/AT:IST-2018-853-v2-2","apa":"Henzinger, T. A., Kragl, B., & Qadeer, S. (2017). Synchronizing the asynchronous. IST Austria. https://doi.org/10.15479/AT:IST-2018-853-v2-2","ieee":"T. A. Henzinger, B. Kragl, and S. Qadeer, Synchronizing the asynchronous. IST Austria, 2017.","ista":"Henzinger TA, Kragl B, Qadeer S. 2017. Synchronizing the asynchronous, IST Austria, 28p.","short":"T.A. Henzinger, B. Kragl, S. Qadeer, Synchronizing the Asynchronous, IST Austria, 2017.","mla":"Henzinger, Thomas A., et al. Synchronizing the Asynchronous. IST Austria, 2017, doi:10.15479/AT:IST-2018-853-v2-2.","chicago":"Henzinger, Thomas A, Bernhard Kragl, and Shaz Qadeer. Synchronizing the Asynchronous. IST Austria, 2017. https://doi.org/10.15479/AT:IST-2018-853-v2-2."},"page":"28","date_published":"2017-08-04T00:00:00Z","doi":"10.15479/AT:IST-2018-853-v2-2","language":[{"iso":"eng"}],"has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"day":"04","month":"08","_id":"6426","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2017","department":[{"_id":"ToHe"}],"publisher":"IST Austria","publication_status":"published","status":"public","title":"Synchronizing the asynchronous","ddc":["000"],"related_material":{"record":[{"id":"133","status":"public","relation":"later_version"}]},"author":[{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Kragl, Bernhard","first_name":"Bernhard","last_name":"Kragl","id":"320FC952-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7745-9117"},{"last_name":"Qadeer","first_name":"Shaz","full_name":"Qadeer, Shaz"}],"oa_version":"Published Version","file":[{"checksum":"b48d42725182d7ca10107a118815f4cf","date_created":"2019-05-13T08:14:44Z","date_updated":"2020-07-14T12:47:30Z","file_id":"6431","relation":"main_file","creator":"dernst","file_size":971347,"content_type":"application/pdf","access_level":"open_access","file_name":"main(1).pdf"}],"date_updated":"2023-02-21T16:59:21Z","date_created":"2019-05-13T08:15:55Z","type":"technical_report","alternative_title":["IST Austria Technical Report"],"abstract":[{"text":"Synchronous programs are easy to specify because the side effects of an operation are finished by the time the invocation of the operation returns to the caller. Asynchronous programs, on the other hand, are difficult to specify because there are side effects due to pending computation scheduled as a result of the invocation of an operation. They are also difficult to verify because of the large number of possible interleavings of concurrent asynchronous computation threads. We show that specifications and correctness proofs for asynchronous programs can be structured by introducing the fiction, for proof purposes, that intermediate, non-quiescent states of asynchronous operations can be ignored. Then, the task of specification becomes relatively simple and the task of verification can be naturally decomposed into smaller sub-tasks. The sub-tasks iteratively summarize, guided by the structure of an asynchronous program, the atomic effect of non-atomic operations and the synchronous effect of asynchronous operations. This structuring of specifications and proofs corresponds to the introduction of multiple layers of stepwise refinement for asynchronous programs. We present the first proof rule, called synchronization, to reduce asynchronous invocations on a lower layer to synchronous invocations on a higher layer. We implemented our proof method in CIVL and evaluated it on a collection of benchmark programs.","lang":"eng"}],"file_date_updated":"2020-07-14T12:47:30Z"},{"date_published":"2017-03-19T00:00:00Z","page":"287 - 313","citation":{"apa":"Chatterjee, K., Kragl, B., Mishra, S., & Pavlogiannis, A. (2017). Faster algorithms for weighted recursive state machines. In H. Yang (Ed.) (Vol. 10201, pp. 287–313). Presented at the ESOP: European Symposium on Programming, Uppsala, Sweden: Springer. https://doi.org/10.1007/978-3-662-54434-1_11","ieee":"K. Chatterjee, B. Kragl, S. Mishra, and A. Pavlogiannis, “Faster algorithms for weighted recursive state machines,” presented at the ESOP: European Symposium on Programming, Uppsala, Sweden, 2017, vol. 10201, pp. 287–313.","ista":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. 2017. Faster algorithms for weighted recursive state machines. ESOP: European Symposium on Programming, LNCS, vol. 10201, 287–313.","ama":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. Faster algorithms for weighted recursive state machines. In: Yang H, ed. Vol 10201. Springer; 2017:287-313. doi:10.1007/978-3-662-54434-1_11","chicago":"Chatterjee, Krishnendu, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis. “Faster Algorithms for Weighted Recursive State Machines.” edited by Hongseok Yang, 10201:287–313. Springer, 2017. https://doi.org/10.1007/978-3-662-54434-1_11.","short":"K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.), Springer, 2017, pp. 287–313.","mla":"Chatterjee, Krishnendu, et al. Faster Algorithms for Weighted Recursive State Machines. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313, doi:10.1007/978-3-662-54434-1_11."},"day":"19","article_processing_charge":"No","scopus_import":"1","oa_version":"Submitted Version","status":"public","title":"Faster algorithms for weighted recursive state machines","intvolume":" 10201","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","_id":"1011","abstract":[{"text":"Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly equivalent, are standard models for interprocedural analysis. Yet RSMs are more convenient as they (a) explicitly model function calls and returns, and (b) specify many natural parameters for algorithmic analysis, e.g., the number of entries and exits. We consider a general framework where RSM transitions are labeled from a semiring and path properties are algebraic with semiring operations, which can model, e.g., interprocedural reachability and dataflow analysis problems. Our main contributions are new algorithms for several fundamental problems. As compared to a direct translation of RSMs to PDSs and the best-known existing bounds of PDSs, our analysis algorithm improves the complexity for finite-height semirings (that subsumes reachability and standard dataflow properties). We further consider the problem of extracting distance values from the representation structures computed by our algorithm, and give efficient algorithms that distinguish the complexity of a one-time preprocessing from the complexity of each individual query. Another advantage of our algorithm is that our improvements carry over to the concurrent setting, where we improve the bestknown complexity for the context-bounded analysis of concurrent RSMs. Finally, we provide a prototype implementation that gives a significant speed-up on several benchmarks from the SLAM/SDV project.","lang":"eng"}],"alternative_title":["LNCS"],"type":"conference","language":[{"iso":"eng"}],"conference":{"name":"ESOP: European Symposium on Programming","end_date":"2017-04-29","location":"Uppsala, Sweden","start_date":"2017-04-22"},"doi":"10.1007/978-3-662-54434-1_11","quality_controlled":"1","isi":1,"project":[{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1701.04914"}],"external_id":{"isi":["000681702400011"]},"month":"03","publication_identifier":{"issn":["03029743"]},"date_updated":"2023-09-22T09:44:50Z","date_created":"2018-12-11T11:49:41Z","volume":10201,"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Kragl","first_name":"Bernhard","orcid":"0000-0001-7745-9117","id":"320FC952-F248-11E8-B48F-1D18A9856A87","full_name":"Kragl, Bernhard"},{"full_name":"Mishra, Samarth","first_name":"Samarth","last_name":"Mishra"},{"orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas"}],"publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"Springer","editor":[{"first_name":"Hongseok","last_name":"Yang","full_name":"Yang, Hongseok"}],"year":"2017","ec_funded":1,"publist_id":"6384"},{"author":[{"full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","last_name":"Gupta","first_name":"Ashutosh"},{"full_name":"Kovács, Laura","first_name":"Laura","last_name":"Kovács"},{"full_name":"Kragl, Bernhard","orcid":"0000-0001-7745-9117","id":"320FC952-F248-11E8-B48F-1D18A9856A87","last_name":"Kragl","first_name":"Bernhard"},{"last_name":"Voronkov","first_name":"Andrei","full_name":"Voronkov, Andrei"}],"date_updated":"2021-01-12T06:53:45Z","date_created":"2018-12-11T11:54:28Z","volume":8837,"year":"2014","acknowledgement":"This research was supported in part by the Austrian National Research Network RiSE (S11410-N23).","publication_status":"published","publisher":"Springer","department":[{"_id":"ToHe"}],"editor":[{"last_name":"Cassez","first_name":"Franck","full_name":"Cassez, Franck"},{"full_name":"Raskin, Jean-François","last_name":"Raskin","first_name":"Jean-François"}],"file_date_updated":"2020-07-14T12:45:19Z","ec_funded":1,"publist_id":"5226","conference":{"end_date":"2014-11-07","location":"Sydney, Australia","start_date":"2014-11-03","name":"ATVA: Automated Technology for Verification and Analysis"},"doi":"10.1007/978-3-319-11936-6_14","language":[{"iso":"eng"}],"oa":1,"quality_controlled":"1","project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"}],"month":"01","pubrep_id":"641","oa_version":"Submitted Version","file":[{"access_level":"open_access","file_name":"IST-2016-641-v1+1_atva2014.pdf","creator":"system","file_size":244294,"content_type":"application/pdf","file_id":"4801","relation":"main_file","checksum":"af4bd3fc1f4c93075e4dc5cbf625fe7b","date_created":"2018-12-12T10:10:15Z","date_updated":"2020-07-14T12:45:19Z"}],"_id":"1872","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","title":"Extensional crisis and proving identity","status":"public","ddc":["000"],"intvolume":" 8837","abstract":[{"lang":"eng","text":"Extensionality axioms are common when reasoning about data collections, such as arrays and functions in program analysis, or sets in mathematics. An extensionality axiom asserts that two collections are equal if they consist of the same elements at the same indices. Using extensionality is often required to show that two collections are equal. A typical example is the set theory theorem (∀x)(∀y)x∪y = y ∪x. Interestingly, while humans have no problem with proving such set identities using extensionality, they are very hard for superposition theorem provers because of the calculi they use. In this paper we show how addition of a new inference rule, called extensionality resolution, allows first-order theorem provers to easily solve problems no modern first-order theorem prover can solve. We illustrate this by running the VAMPIRE theorem prover with extensionality resolution on a number of set theory and array problems. Extensionality resolution helps VAMPIRE to solve problems from the TPTP library of first-order problems that were never solved before by any prover."}],"type":"conference","alternative_title":["LNCS"],"date_published":"2014-01-01T00:00:00Z","publication":"ATVA 2014","citation":{"ama":"Gupta A, Kovács L, Kragl B, Voronkov A. Extensional crisis and proving identity. In: Cassez F, Raskin J-F, eds. ATVA 2014. Vol 8837. Springer; 2014:185-200. doi:10.1007/978-3-319-11936-6_14","apa":"Gupta, A., Kovács, L., Kragl, B., & Voronkov, A. (2014). Extensional crisis and proving identity. In F. Cassez & J.-F. Raskin (Eds.), ATVA 2014 (Vol. 8837, pp. 185–200). Sydney, Australia: Springer. https://doi.org/10.1007/978-3-319-11936-6_14","ieee":"A. Gupta, L. Kovács, B. Kragl, and A. Voronkov, “Extensional crisis and proving identity,” in ATVA 2014, Sydney, Australia, 2014, vol. 8837, pp. 185–200.","ista":"Gupta A, Kovács L, Kragl B, Voronkov A. 2014. Extensional crisis and proving identity. ATVA 2014. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 8837, 185–200.","short":"A. Gupta, L. Kovács, B. Kragl, A. Voronkov, in:, F. Cassez, J.-F. Raskin (Eds.), ATVA 2014, Springer, 2014, pp. 185–200.","mla":"Gupta, Ashutosh, et al. “Extensional Crisis and Proving Identity.” ATVA 2014, edited by Franck Cassez and Jean-François Raskin, vol. 8837, Springer, 2014, pp. 185–200, doi:10.1007/978-3-319-11936-6_14.","chicago":"Gupta, Ashutosh, Laura Kovács, Bernhard Kragl, and Andrei Voronkov. “Extensional Crisis and Proving Identity.” In ATVA 2014, edited by Franck Cassez and Jean-François Raskin, 8837:185–200. Springer, 2014. https://doi.org/10.1007/978-3-319-11936-6_14."},"page":"185 - 200","day":"01","has_accepted_license":"1","scopus_import":1},{"type":"conference","alternative_title":["LNCS"],"abstract":[{"text":"We describe new extensions of the Vampire theorem prover for computing tree interpolants. These extensions generalize Craig interpolation in Vampire, and can also be used to derive sequence interpolants. We evaluated our implementation on a large number of examples over the theory of linear integer arithmetic and integer-indexed arrays, with and without quantifiers. When compared to other methods, our experiments show that some examples could only be solved by our implementation.","lang":"eng"}],"_id":"2237","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","title":"Tree interpolation in Vampire","ddc":["000"],"intvolume":" 8312","file":[{"checksum":"9cebaafca032e6769d273f393305c705","date_updated":"2020-07-14T12:45:34Z","date_created":"2020-05-15T11:10:40Z","relation":"main_file","file_id":"7858","content_type":"application/pdf","file_size":279206,"creator":"dernst","access_level":"open_access","file_name":"2013_LPAR_Blanc.pdf"}],"oa_version":"Submitted Version","scopus_import":1,"series_title":"Lecture Notes in Computer Science","day":"14","has_accepted_license":"1","article_processing_charge":"No","citation":{"chicago":"Blanc, Régis, Ashutosh Gupta, Laura Kovács, and Bernhard Kragl. “Tree Interpolation in Vampire.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-45221-5_13.","short":"R. Blanc, A. Gupta, L. Kovács, B. Kragl, 8312 (2013) 173–181.","mla":"Blanc, Régis, et al. Tree Interpolation in Vampire. Vol. 8312, Springer, 2013, pp. 173–81, doi:10.1007/978-3-642-45221-5_13.","apa":"Blanc, R., Gupta, A., Kovács, L., & Kragl, B. (2013). Tree interpolation in Vampire. Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Stellenbosch, South Africa: Springer. https://doi.org/10.1007/978-3-642-45221-5_13","ieee":"R. Blanc, A. Gupta, L. Kovács, and B. Kragl, “Tree interpolation in Vampire,” vol. 8312. Springer, pp. 173–181, 2013.","ista":"Blanc R, Gupta A, Kovács L, Kragl B. 2013. Tree interpolation in Vampire. 8312, 173–181.","ama":"Blanc R, Gupta A, Kovács L, Kragl B. Tree interpolation in Vampire. 2013;8312:173-181. doi:10.1007/978-3-642-45221-5_13"},"page":"173 - 181","date_published":"2013-01-14T00:00:00Z","file_date_updated":"2020-07-14T12:45:34Z","publist_id":"4724","year":"2013","publication_status":"published","publisher":"Springer","department":[{"_id":"ToHe"}],"author":[{"last_name":"Blanc","first_name":"Régis","full_name":"Blanc, Régis"},{"full_name":"Gupta, Ashutosh","last_name":"Gupta","first_name":"Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kovács, Laura","last_name":"Kovács","first_name":"Laura"},{"full_name":"Kragl, Bernhard","id":"320FC952-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7745-9117","first_name":"Bernhard","last_name":"Kragl"}],"date_updated":"2020-08-11T10:09:42Z","date_created":"2018-12-11T11:56:29Z","volume":8312,"month":"01","oa":1,"quality_controlled":"1","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"conference":{"end_date":"2013-12-19","start_date":"2013-12-14","location":"Stellenbosch, South Africa","name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning"},"doi":"10.1007/978-3-642-45221-5_13","language":[{"iso":"eng"}]}]