---
_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'
...