--- _id: '8195' abstract: - lang: eng 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. acknowledgement: "Bernhard Kragl and Thomas A. Henzinger were supported by\r\nthe Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award)." alternative_title: - LNCS article_processing_charge: No author: - first_name: Bernhard full_name: Kragl, Bernhard id: 320FC952-F248-11E8-B48F-1D18A9856A87 last_name: Kragl orcid: 0000-0001-7745-9117 - first_name: Shaz full_name: Qadeer, Shaz last_name: Qadeer - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 citation: 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 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. 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. 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. short: B. Kragl, S. Qadeer, T.A. Henzinger, in:, Computer Aided Verification, Springer Nature, 2020, pp. 275–298. date_created: 2020-08-03T11:45:35Z date_published: 2020-07-14T00:00:00Z date_updated: 2023-09-07T13:18:00Z day: '14' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-030-53288-8_14 external_id: isi: - '000695276000014' file: - access_level: open_access content_type: application/pdf creator: dernst date_created: 2020-08-06T08:14:54Z date_updated: 2020-08-06T08:14:54Z file_id: '8201' file_name: 2020_LNCS_Kragl.pdf file_size: 804237 relation: main_file success: 1 file_date_updated: 2020-08-06T08:14:54Z has_accepted_license: '1' intvolume: ' 12224' isi: 1 language: - iso: eng license: https://creativecommons.org/licenses/by/4.0/ month: '07' oa: 1 oa_version: Published Version page: 275-298 project: - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication: Computer Aided Verification publication_identifier: eisbn: - '9783030532888' eissn: - 1611-3349 isbn: - '9783030532871' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '8332' relation: dissertation_contains status: public scopus_import: '1' status: public title: Refinement for structured concurrent programs tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 12224 year: '2020' ... --- _id: '8012' abstract: - lang: eng 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. article_processing_charge: No author: - first_name: Bernhard full_name: Kragl, Bernhard id: 320FC952-F248-11E8-B48F-1D18A9856A87 last_name: Kragl orcid: 0000-0001-7745-9117 - first_name: Constantin full_name: Enea, Constantin last_name: Enea - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000-0002-2985-7724 - first_name: Suha Orhun full_name: Mutluergil, Suha Orhun last_name: Mutluergil - first_name: Shaz full_name: Qadeer, Shaz last_name: Qadeer citation: 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' 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' 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. 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. 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.' 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. conference: end_date: 2020-06-20 location: London, United Kingdom name: 'PLDI: Programming Language Design and Implementation' start_date: 2020-06-15 date_created: 2020-06-25T11:40:16Z date_published: 2020-06-01T00:00:00Z date_updated: 2023-09-07T13:18:00Z day: '01' department: - _id: ToHe doi: 10.1145/3385412.3385980 external_id: isi: - '000614622300016' isi: 1 language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.1145/3385412.3385980 month: '06' oa: 1 oa_version: Published Version page: 227-242 project: - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize publication: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation publication_identifier: isbn: - '9781450376136' publication_status: published publisher: Association for Computing Machinery quality_controlled: '1' related_material: record: - id: '8332' relation: dissertation_contains status: public scopus_import: '1' status: public title: Inductive sequentialization of asynchronous programs type: conference user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8 year: '2020' ... --- _id: '8358' abstract: - lang: eng text: "During bacterial cell division, the tubulin-homolog FtsZ forms a ring-like structure at the center of the cell. This so-called Z-ring acts as a scaffold recruiting several division-related proteins to mid-cell and plays a key role in distributing proteins at the division site, a feature driven by the treadmilling motion of FtsZ filaments around the septum. What regulates the architecture, dynamics and stability of the Z-ring is still poorly understood, but FtsZ-associated proteins (Zaps) are known to play an important role. \r\nAdvances in fluorescence microscopy and in vitro reconstitution experiments have helped to shed light into some of the dynamic properties of these complex systems, but methods that allow to collect and analyze large quantitative data sets of the underlying polymer dynamics are still missing.\r\nHere, using an in vitro reconstitution approach, we studied how different Zaps affect FtsZ filament dynamics and organization into large-scale patterns, giving special emphasis to the role of the well-conserved protein ZapA. For this purpose, we use high-resolution fluorescence microscopy combined with novel image analysis workfows to study pattern organization and polymerization dynamics of active filaments. We quantified the influence of Zaps on FtsZ on three diferent spatial scales: the large-scale organization of the membrane-bound filament network, the underlying\r\npolymerization dynamics and the behavior of single molecules.\r\nWe found that ZapA cooperatively increases the spatial order of the filament network, binds only transiently to FtsZ filaments and has no effect on filament length and treadmilling velocity. Our data provides a model for how FtsZ-associated proteins can increase the precision and stability of the bacterial cell division machinery in a\r\nswitch-like manner, without compromising filament dynamics. Furthermore, we believe that our automated quantitative methods can be used to analyze a large variety of dynamic cytoskeletal systems, using standard time-lapse\r\nmovies of homogeneously labeled proteins obtained from experiments in vitro or even inside the living cell.\r\n" acknowledged_ssus: - _id: Bio acknowledgement: I should also express my gratitude to the bioimaging facility at IST Austria, for their assistance with the TIRF setup over the years, and especially to Christoph Sommer, who gave me a lot of input when I was starting to dive into programming. alternative_title: - ISTA Thesis article_processing_charge: No author: - first_name: Paulo R full_name: Dos Santos Caldas, Paulo R id: 38FCDB4C-F248-11E8-B48F-1D18A9856A87 last_name: Dos Santos Caldas orcid: 0000-0001-6730-4461 citation: ama: Dos Santos Caldas PR. Organization and dynamics of treadmilling filaments in cytoskeletal networks of FtsZ and its crosslinkers. 2020. doi:10.15479/AT:ISTA:8358 apa: Dos Santos Caldas, P. R. (2020). Organization and dynamics of treadmilling filaments in cytoskeletal networks of FtsZ and its crosslinkers. Institute of Science and Technology Austria. https://doi.org/10.15479/AT:ISTA:8358 chicago: Dos Santos Caldas, Paulo R. “Organization and Dynamics of Treadmilling Filaments in Cytoskeletal Networks of FtsZ and Its Crosslinkers.” Institute of Science and Technology Austria, 2020. https://doi.org/10.15479/AT:ISTA:8358. ieee: P. R. Dos Santos Caldas, “Organization and dynamics of treadmilling filaments in cytoskeletal networks of FtsZ and its crosslinkers,” Institute of Science and Technology Austria, 2020. ista: Dos Santos Caldas PR. 2020. Organization and dynamics of treadmilling filaments in cytoskeletal networks of FtsZ and its crosslinkers. Institute of Science and Technology Austria. mla: Dos Santos Caldas, Paulo R. Organization and Dynamics of Treadmilling Filaments in Cytoskeletal Networks of FtsZ and Its Crosslinkers. Institute of Science and Technology Austria, 2020, doi:10.15479/AT:ISTA:8358. short: P.R. Dos Santos Caldas, Organization and Dynamics of Treadmilling Filaments in Cytoskeletal Networks of FtsZ and Its Crosslinkers, Institute of Science and Technology Austria, 2020. date_created: 2020-09-10T09:26:49Z date_published: 2020-09-10T00:00:00Z date_updated: 2023-09-07T13:18:51Z day: '10' ddc: - '572' degree_awarded: PhD department: - _id: MaLo doi: 10.15479/AT:ISTA:8358 file: - access_level: open_access checksum: 882f93fe9c351962120e2669b84bf088 content_type: application/pdf creator: pcaldas date_created: 2020-09-10T12:11:29Z date_updated: 2020-09-10T12:11:29Z file_id: '8364' file_name: phd_thesis_pcaldas.pdf file_size: 141602462 relation: main_file success: 1 - access_level: closed checksum: 70cc9e399c4e41e6e6ac445ae55e8558 content_type: application/x-zip-compressed creator: pcaldas date_created: 2020-09-10T12:18:17Z date_updated: 2020-09-11T07:48:10Z file_id: '8365' file_name: phd_thesis_latex_pcaldas.zip file_size: 450437458 relation: source_file file_date_updated: 2020-09-11T07:48:10Z has_accepted_license: '1' language: - iso: eng month: '09' oa: 1 oa_version: Published Version page: '135' publication_identifier: isbn: - 978-3-99078-009-1 issn: - 2663-337X publication_status: published publisher: Institute of Science and Technology Austria related_material: record: - id: '7572' relation: dissertation_contains status: public - id: '7197' relation: part_of_dissertation status: public status: public supervisor: - first_name: Martin full_name: Loose, Martin id: 462D4284-F248-11E8-B48F-1D18A9856A87 last_name: Loose orcid: 0000-0001-7309-9724 title: Organization and dynamics of treadmilling filaments in cytoskeletal networks of FtsZ and its crosslinkers tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: dissertation user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 year: '2020' ... --- _id: '8703' abstract: - lang: eng text: 'Even though Delaunay originally introduced his famous triangulations in the case of infinite point sets with translational periodicity, a software that computes such triangulations in the general case is not yet available, to the best of our knowledge. Combining and generalizing previous work, we present a practical algorithm for computing such triangulations. The algorithm has been implemented and experiments show that its performance is as good as the one of the CGAL package, which is restricted to cubic periodicity. ' alternative_title: - LIPIcs article_number: '75' article_processing_charge: No author: - first_name: Georg F full_name: Osang, Georg F id: 464B40D6-F248-11E8-B48F-1D18A9856A87 last_name: Osang orcid: 0000-0002-8882-5116 - first_name: Mael full_name: Rouxel-Labbé, Mael last_name: Rouxel-Labbé - first_name: Monique full_name: Teillaud, Monique last_name: Teillaud citation: ama: 'Osang GF, Rouxel-Labbé M, Teillaud M. Generalizing CGAL periodic Delaunay triangulations. In: 28th Annual European Symposium on Algorithms. Vol 173. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:10.4230/LIPIcs.ESA.2020.75' apa: 'Osang, G. F., Rouxel-Labbé, M., & Teillaud, M. (2020). Generalizing CGAL periodic Delaunay triangulations. In 28th Annual European Symposium on Algorithms (Vol. 173). Virtual, Online; Pisa, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ESA.2020.75' chicago: Osang, Georg F, Mael Rouxel-Labbé, and Monique Teillaud. “Generalizing CGAL Periodic Delaunay Triangulations.” In 28th Annual European Symposium on Algorithms, Vol. 173. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.ESA.2020.75. ieee: G. F. Osang, M. Rouxel-Labbé, and M. Teillaud, “Generalizing CGAL periodic Delaunay triangulations,” in 28th Annual European Symposium on Algorithms, Virtual, Online; Pisa, Italy, 2020, vol. 173. ista: 'Osang GF, Rouxel-Labbé M, Teillaud M. 2020. Generalizing CGAL periodic Delaunay triangulations. 28th Annual European Symposium on Algorithms. ESA: Annual European Symposium on Algorithms, LIPIcs, vol. 173, 75.' mla: Osang, Georg F., et al. “Generalizing CGAL Periodic Delaunay Triangulations.” 28th Annual European Symposium on Algorithms, vol. 173, 75, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:10.4230/LIPIcs.ESA.2020.75. short: G.F. Osang, M. Rouxel-Labbé, M. Teillaud, in:, 28th Annual European Symposium on Algorithms, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. conference: end_date: 2020-09-09 location: Virtual, Online; Pisa, Italy name: 'ESA: Annual European Symposium on Algorithms' start_date: 2020-09-07 date_created: 2020-10-25T23:01:18Z date_published: 2020-08-26T00:00:00Z date_updated: 2023-09-07T13:29:00Z day: '26' ddc: - '000' department: - _id: HeEd doi: 10.4230/LIPIcs.ESA.2020.75 ec_funded: 1 file: - access_level: open_access checksum: fe0f7c49a99ed870c671b911e10d5496 content_type: application/pdf creator: cziletti date_created: 2020-10-27T14:31:52Z date_updated: 2020-10-27T14:31:52Z file_id: '8712' file_name: 2020_LIPIcs_Osang.pdf file_size: 733291 relation: main_file success: 1 file_date_updated: 2020-10-27T14:31:52Z has_accepted_license: '1' intvolume: ' 173' language: - iso: eng license: https://creativecommons.org/licenses/by/3.0/ month: '08' oa: 1 oa_version: Published Version project: - _id: 266A2E9E-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '788183' name: Alpha Shape Theory Extended publication: 28th Annual European Symposium on Algorithms publication_identifier: isbn: - '9783959771627' issn: - '18688969' publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik quality_controlled: '1' related_material: record: - id: '9056' relation: dissertation_contains status: public scopus_import: '1' status: public title: Generalizing CGAL periodic Delaunay triangulations tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/3.0/legalcode name: Creative Commons Attribution 3.0 Unported (CC BY 3.0) short: CC BY (3.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 173 year: '2020' ... --- _id: '7481' abstract: - lang: eng text: 'We address the following question: How redundant is the parameterisation of ReLU networks? Specifically, we consider transformations of the weight space which leave the function implemented by the network intact. Two such transformations are known for feed-forward architectures: permutation of neurons within a layer, and positive scaling of all incoming weights of a neuron coupled with inverse scaling of its outgoing weights. In this work, we show for architectures with non-increasing widths that permutation and scaling are in fact the only function-preserving weight transformations. For any eligible architecture we give an explicit construction of a neural network such that any other network that implements the same function can be obtained from the original one by the application of permutations and rescaling. The proof relies on a geometric understanding of boundaries between linear regions of ReLU networks, and we hope the developed mathematical tools are of independent interest.' article_processing_charge: No author: - first_name: Phuong full_name: Bui Thi Mai, Phuong id: 3EC6EE64-F248-11E8-B48F-1D18A9856A87 last_name: Bui Thi Mai - first_name: Christoph full_name: Lampert, Christoph id: 40C20FD2-F248-11E8-B48F-1D18A9856A87 last_name: Lampert orcid: 0000-0001-8622-7887 citation: ama: 'Phuong M, Lampert C. Functional vs. parametric equivalence of ReLU networks. In: 8th International Conference on Learning Representations. ; 2020.' apa: Phuong, M., & Lampert, C. (2020). Functional vs. parametric equivalence of ReLU networks. In 8th International Conference on Learning Representations. Online. chicago: Phuong, Mary, and Christoph Lampert. “Functional vs. Parametric Equivalence of ReLU Networks.” In 8th International Conference on Learning Representations, 2020. ieee: M. Phuong and C. Lampert, “Functional vs. parametric equivalence of ReLU networks,” in 8th International Conference on Learning Representations, Online, 2020. ista: 'Phuong M, Lampert C. 2020. Functional vs. parametric equivalence of ReLU networks. 8th International Conference on Learning Representations. ICLR: International Conference on Learning Representations.' mla: Phuong, Mary, and Christoph Lampert. “Functional vs. Parametric Equivalence of ReLU Networks.” 8th International Conference on Learning Representations, 2020. short: M. Phuong, C. Lampert, in:, 8th International Conference on Learning Representations, 2020. conference: end_date: 2020-04-30 location: Online name: 'ICLR: International Conference on Learning Representations' start_date: 2020-04-27 date_created: 2020-02-11T09:07:37Z date_published: 2020-04-26T00:00:00Z date_updated: 2023-09-07T13:29:50Z day: '26' ddc: - '000' department: - _id: ChLa file: - access_level: open_access checksum: 8d372ea5defd8cb8fdc430111ed754a9 content_type: application/pdf creator: bphuong date_created: 2020-02-11T09:07:27Z date_updated: 2020-07-14T12:47:59Z file_id: '7482' file_name: main.pdf file_size: 405469 relation: main_file file_date_updated: 2020-07-14T12:47:59Z has_accepted_license: '1' language: - iso: eng month: '04' oa: 1 oa_version: Published Version publication: 8th International Conference on Learning Representations publication_status: published quality_controlled: '1' related_material: link: - relation: supplementary_material url: https://iclr.cc/virtual_2020/poster_Bylx-TNKvH.html record: - id: '9418' relation: dissertation_contains status: public status: public title: Functional vs. parametric equivalence of ReLU networks type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2020' ...