@inproceedings{13292,
  abstract     = {The operator precedence languages (OPLs) represent the largest known subclass of the context-free languages which enjoys all desirable closure and decidability properties. This includes the decidability of language inclusion, which is the ultimate verification problem. Operator precedence grammars, automata, and logics have been investigated and used, for example, to verify programs with arithmetic expressions and exceptions (both of which are deterministic pushdown but lie outside the scope of the visibly pushdown languages). In this paper, we complete the picture and give, for the first time, an algebraic characterization of the class of OPLs in the form of a syntactic congruence that has finitely many equivalence classes exactly for the operator precedence languages. This is a generalization of the celebrated Myhill-Nerode theorem for the regular languages to OPLs. As one of the consequences, we show that universality and language inclusion for nondeterministic operator precedence automata can be solved by an antichain algorithm. Antichain algorithms avoid determinization and complementation through an explicit subset construction, by leveraging a quasi-order on words, which allows the pruning of the search space for counterexample words without sacrificing completeness. Antichain algorithms can be implemented symbolically, and these implementations are today the best-performing algorithms in practice for the inclusion of finite automata. We give a generic construction of the quasi-order needed for antichain algorithms from a finite syntactic congruence. This yields the first antichain algorithm for OPLs, an algorithm that solves the ExpTime-hard language inclusion problem for OPLs in exponential time.},
  author       = {Henzinger, Thomas A and Kebis, Pavol and Mazzocchi, Nicolas Adrien and Sarac, Naci E},
  booktitle    = {50th International Colloquium on Automata, Languages, and Programming},
  isbn         = {9783959772785},
  issn         = {1868-8969},
  location     = {Paderborn, Germany},
  pages        = {129:1----129:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Regular methods for operator precedence languages}},
  doi          = {10.4230/LIPIcs.ICALP.2023.129},
  volume       = {261},
  year         = {2023},
}

@inproceedings{13310,
  abstract     = {Machine-learned systems are in widespread use for making decisions about humans, and it is important that they are fair, i.e., not biased against individuals based on sensitive attributes. We present runtime verification of algorithmic fairness for systems whose models are unknown, but are assumed to have a Markov chain structure. We introduce a specification language that can model many common algorithmic fairness properties, such as demographic parity, equal opportunity, and social burden. We build monitors that observe a long sequence of events as generated by a given system, and output, after each observation, a quantitative estimate of how fair or biased the system was on that run until that point in time. The estimate is proven to be correct modulo a variable error bound and a given confidence level, where the error bound gets tighter as the observed sequence gets longer. Our monitors are of two types, and use, respectively, frequentist and Bayesian statistical inference techniques. While the frequentist monitors compute estimates that are objectively correct with respect to the ground truth, the Bayesian monitors compute estimates that are correct subject to a given prior belief about the system’s model. Using a prototype implementation, we show how we can monitor if a bank is fair in giving loans to applicants from different social backgrounds, and if a college is fair in admitting students while maintaining a reasonable financial burden on the society. Although they exhibit different theoretical complexities in certain cases, in our experiments, both frequentist and Bayesian monitors took less than a millisecond to update their verdicts after each observation.},
  author       = {Henzinger, Thomas A and Karimi, Mahyar and Kueffner, Konstantin and Mallik, Kaushik},
  booktitle    = {Computer Aided Verification},
  isbn         = {9783031377020},
  issn         = {1611-3349},
  location     = {Paris, France},
  pages        = {358–382},
  publisher    = {Springer Nature},
  title        = {{Monitoring algorithmic fairness}},
  doi          = {10.1007/978-3-031-37703-7_17},
  volume       = {13965},
  year         = {2023},
}

@article{13314,
  abstract     = {The emergence of large-scale order in self-organized systems relies on local interactions between individual components. During bacterial cell division, FtsZ—a prokaryotic homologue of the eukaryotic protein tubulin—polymerizes into treadmilling filaments that further organize into a cytoskeletal ring. In vitro, FtsZ filaments can form dynamic chiral assemblies. However, how the active and passive properties of individual filaments relate to these large-scale self-organized structures remains poorly understood. Here we connect single-filament properties with the mesoscopic scale by combining minimal active matter simulations and biochemical reconstitution experiments. We show that the density and flexibility of active chiral filaments define their global order. At intermediate densities, curved, flexible filaments organize into chiral rings and polar bands. An effectively nematic organization dominates for high densities and for straight, mutant filaments with increased rigidity. Our predicted phase diagram quantitatively captures these features, demonstrating how the flexibility, density and chirality of the active filaments affect their collective behaviour. Our findings shed light on the fundamental properties of active chiral matter and explain how treadmilling FtsZ filaments organize during bacterial cell division.},
  author       = {Dunajova, Zuzana and Prats Mateu, Batirtze and Radler, Philipp and Lim, Keesiang and Brandis, Dörte and Velicky, Philipp and Danzl, Johann G and Wong, Richard W. and Elgeti, Jens and Hannezo, Edouard B and Loose, Martin},
  issn         = {1745-2481},
  journal      = {Nature Physics},
  pages        = {1916--1926},
  publisher    = {Springer Nature},
  title        = {{Chiral and nematic phases of flexible active filaments}},
  doi          = {10.1038/s41567-023-02218-w},
  volume       = {19},
  year         = {2023},
}

@phdthesis{13331,
  abstract     = {The extension of extremal combinatorics to the setting of exterior algebra is a work
in progress that gained attention recently. In this thesis, we study the combinatorial structure of exterior algebra by introducing a dictionary that translates the notions from the set systems into the framework of exterior algebra. We show both generalizations of celebrated Erdös--Ko--Rado theorem and Hilton--Milner theorem to the setting of exterior algebra in the simplest non-trivial case of two-forms.
},
  author       = {Köse, Seyda},
  issn         = {2791-4585},
  pages        = {26},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Exterior algebra and combinatorics}},
  doi          = {10.15479/at:ista:13331},
  year         = {2023},
}

@phdthesis{14058,
  abstract     = {Females and males across species are subject to divergent selective pressures arising
from di↵erent reproductive interests and ecological niches. This often translates into a
intricate array of sex-specific natural and sexual selection on traits that have a shared
genetic basis between both sexes, causing a genetic sexual conflict. The resolution of
this conflict mostly relies on the evolution of sex-specific expression of the shared genes,
leading to phenotypic sexual dimorphism. Such sex-specific gene expression is thought
to evolve via modifications of the genetic networks ultimately linked to sex-determining
transcription factors. Although much empirical and theoretical evidence supports this
standard picture of the molecular basis of sexual conflict resolution, there still are a
few open questions regarding the complex array of selective forces driving phenotypic
di↵erentiation between the sexes, as well as the molecular mechanisms underlying sexspecific adaptation. I address some of these open questions in my PhD thesis.
First, how do patterns of phenotypic sexual dimorphism vary within populations,
as a response to the temporal and spatial changes in sex-specific selective forces? To
tackle this question, I analyze the patterns of sex-specific phenotypic variation along
three life stages and across populations spanning the whole geographical range of Rumex
hastatulus, a wind-pollinated angiosperm, in the first Chapter of the thesis.
Second, how do gene expression patterns lead to phenotypic dimorphism, and what
are the molecular mechanisms underlying the observed transcriptomic variation? I
address this question by examining the sex- and tissue-specific expression variation in
newly-generated datasets of sex-specific expression in heads and gonads of Drosophila
melanogaster. I additionally used two complementary approaches for the study of the
genetic basis of sex di↵erences in gene expression in the second and third Chapters of
the thesis.
Third, how does intersex correlation, thought to be one of the main aspects constraining the ability for the two sexes to decouple, interact with the evolution of sexual
dimorphism? I develop models of sex-specific stabilizing selection, mutation and drift
to formalize common intuition regarding the patterns of covariation between intersex
correlation and sexual dimorphism in the fourth Chapter of the thesis.
Alltogether, the work described in this PhD thesis provides useful insights into the
links between genetic, transcriptomic and phenotypic layers of sex-specific variation,
and contributes to our general understanding of the dynamics of sexual dimorphism
evolution.},
  author       = {Puixeu Sala, Gemma},
  isbn         = {978-3-99078-035-0},
  issn         = {2663-337X},
  pages        = {230},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{The molecular basis of sexual dimorphism: Experimental and theoretical characterization of phenotypic, transcriptomic and genetic patterns of sex-specific adaptation}},
  doi          = {10.15479/at:ista:14058},
  year         = {2023},
}

@article{14077,
  abstract     = {The regulatory architecture of gene expression is known to differ substantially between sexes in Drosophila, but most studies performed
so far used whole-body data and only single crosses, which may have limited their scope to detect patterns that are robust across tissues
and biological replicates. Here, we use allele-specific gene expression of parental and reciprocal hybrid crosses between 6 Drosophila
melanogaster inbred lines to quantify cis- and trans-regulatory variation in heads and gonads of both sexes separately across 3 replicate
crosses. Our results suggest that female and male heads, as well as ovaries, have a similar regulatory architecture. On the other hand,
testes display more and substantially different cis-regulatory effects, suggesting that sex differences in the regulatory architecture that
have been previously observed may largely derive from testis-specific effects. We also examine the difference in cis-regulatory variation
of genes across different levels of sex bias in gonads and heads. Consistent with the idea that intersex correlations constrain expression
and can lead to sexual antagonism, we find more cis variation in unbiased and moderately biased genes in heads. In ovaries, reduced cis
variation is observed for male-biased genes, suggesting that cis variants acting on these genes in males do not lead to changes in ovary
expression. Finally, we examine the dominance patterns of gene expression and find that sex- and tissue-specific patterns of inheritance
as well as trans-regulatory variation are highly variable across biological crosses, although these were performed in highly controlled
experimental conditions. This highlights the importance of using various genetic backgrounds to infer generalizable patterns.},
  author       = {Puixeu Sala, Gemma and Macon, Ariana and Vicoso, Beatriz},
  issn         = {2160-1836},
  journal      = {G3: Genes, Genomes, Genetics},
  keywords     = {Genetics (clinical), Genetics, Molecular Biology},
  number       = {8},
  publisher    = {Oxford University Press},
  title        = {{Sex-specific estimation of cis and trans regulation of gene expression in heads and gonads of Drosophila melanogaster}},
  doi          = {10.1093/g3journal/jkad121},
  volume       = {13},
  year         = {2023},
}

@article{14087,
  abstract     = {Polar active matter of self-propelled particles sustain spontaneous flows through the full-integer topological defects. We study theoretically the incompressible flow profiles around ±1 defects induced by polar and dipolar active forces. We show that dipolar forces induce vortical flows around the +1 defect, while the flow around the −1 defect has an 8-fold rotational symmetry. The vortical flow changes its chirality near the +1 defect core in the absence of the friction with a substrate. We show analytically that the flow induced by polar active forces is vortical near the +1 defect and is 4-fold symmetric near the −1 defect, while it becomes uniform in the far-field. For a pair of oppositely charged defects, this polar flow contributes to a mutual interaction force that depends only on the orientation of the defect pair relative to the background polarization, and that enhances defect pair annihilation. This is in contradiction with the effect of dipolar active forces which decay inversely proportional with the defect separation distance. As such, our analyses reveals a long-ranged mechanism for the pairwise interaction between topological defects in polar active matter.},
  author       = {Rønning, Jonas and Renaud, Julian B and Doostmohammadi, Amin and Angheluta, Luiza},
  issn         = {1744-6848},
  journal      = {Soft Matter},
  pages        = {7513--7527},
  publisher    = {Royal Society of Chemistry},
  title        = {{Spontaneous flows and dynamics of full-integer topological defects in polar active matter}},
  doi          = {10.1039/d3sm00316g},
  volume       = {39},
  year         = {2023},
}

@inproceedings{14260,
  abstract     = {This paper presents Lincheck, a new practical and user-friendly framework for testing concurrent algorithms on the Java Virtual Machine (JVM). Lincheck provides a simple and declarative way to write concurrent tests: instead of describing how to perform the test, users specify what to test by declaring all the operations to examine; the framework automatically handles the rest. As a result, tests written with Lincheck are concise and easy to understand. The framework automatically generates a set of concurrent scenarios, examines them using stress-testing or bounded model checking, and verifies that the results of each invocation are correct. Notably, if an error is detected via model checking, Lincheck provides an easy-to-follow trace to reproduce it, significantly simplifying the bug investigation.

To the best of our knowledge, Lincheck is the first production-ready tool on the JVM that offers such a simple way of writing concurrent tests, without requiring special skills or expertise. We successfully integrated Lincheck in the development process of several large projects, such as Kotlin Coroutines, and identified new bugs in popular concurrency libraries, such as a race in Java’s standard ConcurrentLinkedDeque and a liveliness bug in Java’s AbstractQueuedSynchronizer framework, which is used in most of the synchronization primitives. We believe that Lincheck can significantly improve the quality and productivity of concurrent algorithms research and development and become the state-of-the-art tool for checking their correctness.},
  author       = {Koval, Nikita and Fedorov, Alexander and Sokolova, Maria and Tsitelov, Dmitry and Alistarh, Dan-Adrian},
  booktitle    = {35th International Conference on Computer Aided Verification },
  isbn         = {9783031377051},
  issn         = {1611-3349},
  location     = {Paris, France},
  pages        = {156--169},
  publisher    = {Springer Nature},
  title        = {{Lincheck: A practical framework for testing concurrent data structures on JVM}},
  doi          = {10.1007/978-3-031-37706-8_8},
  volume       = {13964},
  year         = {2023},
}

@article{14261,
  abstract     = {In this work, a generalized, adapted Numerov implementation capable of determining band structures of periodic quantum systems is outlined. Based on the input potential, the presented approach numerically solves the Schrödinger equation in position space at each momentum space point. Thus, in addition to the band structure, the method inherently provides information about the state functions and probability densities in position space at each momentum space point considered. The generalized, adapted Numerov framework provided reliable estimates for a variety of increasingly complex test suites in one, two, and three dimensions. The accuracy of the proposed methodology was benchmarked against results obtained for the analytically solvable Kronig-Penney model. Furthermore, the presented numerical solver was applied to a model potential representing a 2D optical lattice being a challenging application relevant, for example, in the field of quantum computing.},
  author       = {Gamper, Jakob and Kluibenschedl, Florian and Weiss, Alexander K.H. and Hofer, Thomas S.},
  issn         = {1948-7185},
  journal      = {Journal of Physical Chemistry Letters},
  number       = {33},
  pages        = {7395--7403},
  publisher    = {American Chemical Society},
  title        = {{Accessing position space wave functions in band structure calculations of periodic systems - a generalized, adapted numerov implementation for one-, two-, and three-dimensional quantum problems}},
  doi          = {10.1021/acs.jpclett.3c01707},
  volume       = {14},
  year         = {2023},
}

@article{14343,
  abstract     = {The total energy of an eigenstate in a composite quantum system tends to be distributed equally among its constituents. We identify the quantum fluctuation around this equipartition principle in the simplest disordered quantum system consisting of linear combinations of Wigner matrices. As our main ingredient, we prove the Eigenstate Thermalisation Hypothesis and Gaussian fluctuation for general quadratic forms of the bulk eigenvectors of Wigner matrices with an arbitrary deformation.},
  author       = {Cipolloni, Giorgio and Erdös, László and Henheik, Sven Joscha and Kolupaiev, Oleksii},
  issn         = {2050-5094},
  journal      = {Forum of Mathematics, Sigma},
  publisher    = {Cambridge University Press},
  title        = {{Gaussian fluctuations in the equipartition principle for Wigner matrices}},
  doi          = {10.1017/fms.2023.70},
  volume       = {11},
  year         = {2023},
}

@phdthesis{14374,
  abstract     = {Superconductivity has many important applications ranging from levitating trains over qubits to MRI scanners. The phenomenon is successfully modeled by Bardeen-Cooper-Schrieffer (BCS) theory. From a mathematical perspective, BCS theory has been studied extensively for systems without boundary. However, little is known in the presence of boundaries. With the help of numerical methods physicists observed that the critical temperature may increase in the presence of a boundary. The goal of this thesis is to understand the influence of boundaries on the critical temperature in BCS theory and to give a first rigorous justification of these observations. On the way, we also study two-body Schrödinger operators on domains with boundaries and prove additional results for superconductors without boundary.

BCS theory is based on a non-linear functional, where the minimizer indicates whether the system is superconducting or in the normal, non-superconducting state. By considering the Hessian of the BCS functional at the normal state, one can analyze whether the normal state is possibly a minimum of the BCS functional and estimate the critical temperature. The Hessian turns out to be a linear operator resembling a Schrödinger operator for two interacting particles, but with more complicated kinetic energy. As a first step, we study the two-body Schrödinger operator in the presence of boundaries.
For Neumann boundary conditions, we prove that the addition of a boundary can create new eigenvalues, which correspond to the two particles forming a bound state close to the boundary.

Second, we need to understand superconductivity in the translation invariant setting. While in three dimensions this has been extensively studied, there is no mathematical literature for the one and two dimensional cases. In dimensions one and two, we compute the weak coupling asymptotics of the critical temperature and the energy gap  in the translation invariant setting. We also prove that their ratio is independent of the microscopic details of the model in the weak coupling limit; this property is referred to as universality.

In the third part, we study the critical temperature of superconductors in the presence of boundaries. We start by considering the one-dimensional case of a half-line with contact interaction. Then, we generalize the results to generic interactions and half-spaces in one, two and three dimensions. Finally, we compare the critical temperature of a quarter space in two dimensions to the critical temperatures of a half-space and of the full space.},
  author       = {Roos, Barbara},
  issn         = {2663-337X},
  pages        = {206},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Boundary superconductivity in BCS theory}},
  doi          = {10.15479/at:ista:14374},
  year         = {2023},
}

@article{14421,
  abstract     = {Only recently has it been possible to construct a self-adjoint Hamiltonian that involves the creation of Dirac particles at a point source in 3d space. Its definition makes use of an interior-boundary condition. Here, we develop for this Hamiltonian a corresponding theory of the Bohmian configuration. That is, we (non-rigorously) construct a Markov jump process $(Q_t)_{t\in\mathbb{R}}$ in the configuration space of a variable number of particles that is $|\psi_t|^2$-distributed at every time t and follows Bohmian trajectories between the jumps. The jumps correspond to particle creation or annihilation events and occur either to or from a configuration with a particle located at the source. The process is the natural analog of Bell's jump process, and a central piece in its construction is the determination of the rate of particle creation. The construction requires an analysis of the asymptotic behavior of the Bohmian trajectories near the source. We find that the particle reaches the source with radial speed 0, but orbits around the source infinitely many times in finite time before absorption (or after emission).},
  author       = {Henheik, Sven Joscha and Tumulka, Roderich},
  issn         = {1751-8121},
  journal      = {Journal of Physics A: Mathematical and Theoretical},
  number       = {44},
  publisher    = {IOP Publishing},
  title        = {{Creation rate of Dirac particles at a point source}},
  doi          = {10.1088/1751-8121/acfe62},
  volume       = {56},
  year         = {2023},
}

@article{14425,
  abstract     = {Water adsorption and dissociation processes on pristine low-index TiO2 interfaces are important but poorly understood outside the well-studied anatase (101) and rutile (110). To understand these, we construct three sets of machine learning potentials that are simultaneously applicable to various TiO2 surfaces, based on three density-functional-theory approximations. Here we show the water dissociation free energies on seven pristine TiO2 surfaces, and predict that anatase (100), anatase (110), rutile (001), and rutile (011) favor water dissociation, anatase (101) and rutile (100) have mostly molecular adsorption, while the simulations of rutile (110) sensitively depend on the slab thickness and molecular adsorption is preferred with thick slabs. Moreover, using an automated algorithm, we reveal that these surfaces follow different types of atomistic mechanisms for proton transfer and water dissociation: one-step, two-step, or both. These mechanisms can be rationalized based on the arrangements of water molecules on the different surfaces. Our finding thus demonstrates that the different pristine TiO2 surfaces react with water in distinct ways, and cannot be represented using just the low-energy anatase (101) and rutile (110) surfaces.},
  author       = {Zeng, Zezhu and Wodaczek, Felix and Liu, Keyang and Stein, Frederick and Hutter, Jürg and Chen, Ji and Cheng, Bingqing},
  issn         = {2041-1723},
  journal      = {Nature Communications},
  publisher    = {Springer Nature},
  title        = {{Mechanistic insight on water dissociation on pristine low-index TiO2 surfaces from machine learning molecular dynamics simulations}},
  doi          = {10.1038/s41467-023-41865-8},
  volume       = {14},
  year         = {2023},
}

@article{14466,
  abstract     = {The first long-lived turbulent structures observable in planar shear flows take the form of localized stripes, inclined with respect to the mean flow direction. The dynamics of these stripes is central to transition, and recent studies proposed an analogy to directed percolation where the stripes’ proliferation is ultimately responsible for the turbulence becoming sustained. In the present study we focus on the internal stripe dynamics as well as on the eventual stripe expansion, and we compare the underlying mechanisms in pressure- and shear-driven planar flows, respectively, plane-Poiseuille and plane-Couette flow. Despite the similarities of the overall laminar–turbulence patterns, the stripe proliferation processes in the two cases are fundamentally different. Starting from the growth and sustenance of individual stripes, we find that in plane-Couette flow new streaks are created stochastically throughout the stripe whereas in plane-Poiseuille flow streak creation is deterministic and occurs locally at the downstream tip. Because of the up/downstream symmetry, Couette stripes, in contrast to Poiseuille stripes, have two weak and two strong laminar turbulent interfaces. These differences in symmetry as well as in internal growth give rise to two fundamentally different stripe splitting mechanisms. In plane-Poiseuille flow splitting is connected to the elongational growth of the original stripe, and it results from a break-off/shedding of the stripe's tail. In plane-Couette flow splitting follows from a broadening of the original stripe and a division along the stripe into two slimmer stripes.},
  author       = {Marensi, Elena and Yalniz, Gökhan and Hof, Björn},
  issn         = {1469-7645},
  journal      = {Journal of Fluid Mechanics},
  keywords     = {turbulence, transition to turbulence, patterns},
  publisher    = {Cambridge University Press},
  title        = {{Dynamics and proliferation of turbulent stripes in plane-Poiseuille and plane-Couette flows}},
  doi          = {10.1017/jfm.2023.780},
  volume       = {974},
  year         = {2023},
}

@inproceedings{14485,
  abstract     = {Batching is a technique that stores multiple keys/values in each node of a data structure. In sequential search data structures, batching reduces latency by reducing the number of cache misses and shortening the chain of pointers to dereference. Applying batching to concurrent data structures is challenging, because it is difficult to maintain the search property and keep contention low in the presence of batching.
In this paper, we present a general methodology for leveraging batching in concurrent search data structures, called BatchBoost. BatchBoost builds a search data structure from distinct "data" and "index" layers. The data layer’s purpose is to store a batch of key/value pairs in each of its nodes. The index layer uses an unmodified concurrent search data structure to route operations to a position in the data layer that is "close" to where the corresponding key should exist. The requirements on the index and data layers are low: with minimal effort, we were able to compose three highly scalable concurrent search data structures based on three original data structures as the index layers with a batched version of the Lazy List as the data layer. The resulting BatchBoost data structures provide significant performance improvements over their original counterparts.},
  author       = {Aksenov, Vitaly and Anoprenko, Michael and Fedorov, Alexander and Spear, Michael},
  booktitle    = {37th International Symposium on Distributed Computing},
  isbn         = {9783959773010},
  issn         = {1868-8969},
  location     = {L'Aquila, Italy},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Brief announcement: BatchBoost: Universal batching for concurrent data structures}},
  doi          = {10.4230/LIPIcs.DISC.2023.35},
  volume       = {281},
  year         = {2023},
}

@phdthesis{14506,
  abstract     = {Payment channel networks are a promising approach to improve the scalability bottleneck
of cryptocurrencies. Two design principles behind payment channel networks are
efficiency and privacy. Payment channel networks improve efficiency by allowing users
to transact in a peer-to-peer fashion along multi-hop routes in the network, avoiding
the lengthy process of consensus on the blockchain. Transacting over payment channel
networks also improves privacy as these transactions are not broadcast to the blockchain.
Despite the influx of recent protocols built on top of payment channel networks and
their analysis, a common shortcoming of many of these protocols is that they typically
focus only on either improving efficiency or privacy, but not both. Another limitation
on the efficiency front is that the models used to model actions, costs and utilities of
users are limited or come with unrealistic assumptions.
This thesis aims to address some of the shortcomings of recent protocols and algorithms
on payment channel networks, particularly in their privacy and efficiency aspects. We
first present a payment route discovery protocol based on hub labelling and private
information retrieval that hides the route query and is also efficient. We then present
a rebalancing protocol that formulates the rebalancing problem as a linear program
and solves the linear program using multiparty computation so as to hide the channel
balances. The rebalancing solution as output by our protocol is also globally optimal.
We go on to develop more realistic models of the action space, costs, and utilities of
both existing and new users that want to join the network. In each of these settings,
we also develop algorithms to optimise the utility of these users with good guarantees
on the approximation and competitive ratios.},
  author       = {Yeo, Michelle X},
  issn         = {2663-337X},
  pages        = {162},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Advances in efficiency and privacy in payment channel network analysis}},
  doi          = {10.15479/14506},
  year         = {2023},
}

@phdthesis{14530,
  abstract     = {Most motions of many-body systems at any scale in nature with sufficient degrees of freedom tend to be chaotic; reaching from the orbital motion of planets, the air currents in our atmosphere, down to the water flowing through our pipelines or the movement of a population of bacteria. To the observer it is therefore intriguing when a moving collective exhibits order. Collective motion of flocks of birds, schools of fish or swarms of self-propelled particles or robots have been studied extensively over the past decades but the mechanisms involved in the transition from chaos to order remain unclear. Here, the interactions, that in most systems give rise to chaos, sustain order.  In this thesis we investigate mechanisms that preserve, destabilize or lead to the ordered state. We show that endothelial cells migrating in circular confinements transition to a collective rotating state and concomitantly synchronize the frequencies of nucleating actin waves within individual cells. Consequently, the frequency dependent cell migration speed uniformizes across the population. Complementary to the WAVE dependent nucleation of traveling actin waves, we show that in leukocytes the actin polymerization depending on WASp generates pushing forces locally at stationary patches. Next, in pipe flows, we study methods to disrupt the self--sustaining cycle of turbulence and therefore relaminarize the flow. While we find in pulsating flow conditions that turbulence emerges through a helical instability during the decelerating phase. Finally, we show quantitatively in brain slices of mice that wild-type control neurons can compensate the migratory deficits of a genetically modified neuronal sub--population in the developing cortex.  },
  author       = {Riedl, Michael},
  issn         = {2663-337X},
  keywords     = {Synchronization, Collective Movement, Active Matter, Cell Migration, Active Colloids},
  pages        = {260},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Synchronization in collectively moving active matter}},
  doi          = {10.15479/14530},
  year         = {2023},
}

@phdthesis{14539,
  abstract     = {Stochastic systems provide a formal framework for modelling and quantifying uncertainty in systems and have been widely adopted in many application domains. Formal
verification and control of finite state stochastic systems, a subfield of formal methods
also known as probabilistic model checking, is well studied. In contrast, formal verification and control of infinite state stochastic systems have received comparatively
less attention. However, infinite state stochastic systems commonly arise in practice.
For instance, probabilistic models that contain continuous probability distributions such
as normal or uniform, or stochastic dynamical systems which are a classical model for
control under uncertainty, both give rise to infinite state systems.
The goal of this thesis is to contribute to laying theoretical and algorithmic foundations
of fully automated formal verification and control of infinite state stochastic systems,
with a particular focus on systems that may be executed over a long or infinite time.
We consider formal verification of infinite state stochastic systems in the setting of
static analysis of probabilistic programs and formal control in the setting of controller
synthesis in stochastic dynamical systems. For both problems, we present some of the
first fully automated methods for probabilistic (a.k.a. quantitative) reachability and
safety analysis applicable to infinite time horizon systems. We also advance the state
of the art of probability 1 (a.k.a. qualitative) reachability analysis for both problems.
Finally, for formal controller synthesis in stochastic dynamical systems, we present a
novel framework for learning neural network control policies in stochastic dynamical
systems with formal guarantees on correctness with respect to quantitative reachability,
safety or reach-avoid specifications.
},
  author       = {Zikelic, Dorde},
  isbn         = {978-3-99078-036-7},
  issn         = {2663-337X},
  pages        = {256},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Automated verification and control of infinite state stochastic systems}},
  doi          = {10.15479/14539},
  year         = {2023},
}

@phdthesis{14547,
  abstract     = {Superconductor-semiconductor heterostructures currently capture a significant amount of research interest and they serve as the physical platform in many proposals towards topological quantum computation.
Despite being under extensive investigations, historically using transport techniques, the basic properties of the interface between the superconductor and the semiconductor remain to be understood.

In this thesis, two separate studies on the Al-InAs heterostructures are reported with the first focusing on the physics of the material motivated by the emergence of a new phase, the Bogoliubov-Fermi surface. 
The second focuses on a technological application, a gate-tunable Josephson parametric amplifier.

In the first study, we investigate the hypothesized unconventional nature of the induced superconductivity at the interface between the Al thin film and the InAs quantum well.
We embed a two-dimensional Al-InAs hybrid system in a resonant microwave circuit allowing measurements of change in inductance.
The behaviour of the resonance in a range of temperature and in-plane magnetic field has been studied and compared with the theory of conventional s-wave superconductor and a two-component theory that includes both contribution of the $s$-wave pairing in Al and the intraband $p \pm ip$ pairing in InAs.
Measuring the temperature dependence of resonant frequency, no discrepancy is found between data and the conventional theory.
We observe the breakdown of superconductivity due to an applied magnetic field which contradicts the conventional theory.
In contrast, the data can be captured quantitatively by fitting to a two-component model.
We find the evidence of the intraband $p \pm ip$ pairing in the InAs and the emergence of the Bogoliubov-Fermi surfaces due to magnetic field with the characteristic value $B^* = 0.33~\mathrm{T}$.
From the fits, the sheet resistance of Al, the carrier density and mobility in InAs are determined.
By systematically studying the anisotropy of the circuit response, we find weak anisotropy for $B < B^*$ and increasingly strong anisotropy for $B > B^*$ resulting in a pronounced two-lobe structure in polar plot of frequency versus field angle.
Strong resemblance between the field dependence of dissipation and superfluid density hints at a hidden signature of the Bogoliubov-Fermi surface that is burried in the dissipation data.

In the second study, we realize a parametric amplifier with a Josephson field effect transistor as the active element.
The device's modest construction consists of a gated SNS weak link embedded at the center of a coplanar waveguide resonator.
By applying a gate voltage, the resonant frequency is field-effect tunable over a range of 2 GHz.
Modelling the JoFET minimally as a parallel RL circuit, the dissipation introduced by the JoFET can be quantitatively related to the gate voltage.
We observed gate-tunable Kerr nonlinearity qualitatively in line with expectation.
The JoFET amplifier has 20 dB of gain, 4 MHz of instantaneous bandwidth, and a 1dB compression point of -125.5 dBm when operated at a fixed resonant frequency.
In general, the signal-to-noise ratio is improved by 5-7 dB when the JoFET amplifier is activated compared.
The noise of the measurement chain and insertion loss of relevant circuit elements are calibrated to determine the expected and the real noise performance of the JoFET amplifier.
As a quantification of the noise performance, the measured total input-referred noise of the JoFET amplifier is in good agreement with the estimated expectation which takes device loss into account.
We found that the noise performance of the device reported in this document approaches one photon of total input-referred added noise which is the quantum limit imposed in nondegenerate parametric amplifier.},
  author       = {Phan, Duc T},
  issn         = {2663-337X},
  keywords     = {superconductor-semiconductor, superconductivity, Al, InAs, p-wave, superconductivity, JPA, microwave},
  pages        = {80},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Resonant microwave spectroscopy of Al-InAs}},
  doi          = {10.15479/14547},
  year         = {2023},
}

@phdthesis{14587,
  abstract     = {This thesis concerns the application of variational methods to the study of evolution problems arising in fluid mechanics and in material sciences. The main focus is on weak-strong stability properties of some curvature driven interface evolution problems, such as the two-phase Navier–Stokes flow with surface tension and multiphase mean curvature flow, and on the phase-field approximation of the latter. Furthermore, we discuss a variational approach to the study of a class of doubly nonlinear wave equations.
First, we consider the two-phase Navier–Stokes flow with surface tension within a bounded domain. The two fluids are immiscible and separated by a sharp interface, which intersects the boundary of the domain at a constant contact angle of ninety degree. We devise a suitable concept of varifolds solutions for the associated interface evolution problem and we establish a weak-strong uniqueness principle in case of a two dimensional ambient space. In order to focus on the boundary effects and on the singular geometry of the evolving domains, we work for simplicity in the regime of same viscosities for the two fluids.
The core of the thesis consists in the rigorous proof of the convergence of the vectorial Allen-Cahn equation towards multiphase mean curvature flow for a suitable class of multi- well potentials and for well-prepared initial data. We even establish a rate of convergence. Our relative energy approach relies on the concept of gradient-flow calibration for branching singularities in multiphase mean curvature flow and thus enables us to overcome the limitations of other approaches. To the best of the author’s knowledge, our result is the first quantitative and unconditional one available in the literature for the vectorial/multiphase setting.
This thesis also contains a first study of weak-strong stability for planar multiphase mean curvature flow beyond the singularity resulting from a topology change. Previous weak-strong results are indeed limited to time horizons before the first topology change of the strong solution. We consider circular topology changes and we prove weak-strong stability for BV solutions to planar multiphase mean curvature flow beyond the associated singular times by dynamically adapting the strong solutions to the weak one by means of a space-time shift.
In the context of interface evolution problems, our proofs for the main results of this thesis are based on the relative energy technique, relying on novel suitable notions of relative energy functionals, which in particular measure the interface error. Our statements follow from the resulting stability estimates for the relative energy associated to the problem.
At last, we introduce a variational approach to the study of nonlinear evolution problems. This approach hinges on the minimization of a parameter dependent family of convex functionals over entire trajectories, known as Weighted Inertia-Dissipation-Energy (WIDE) functionals. We consider a class of doubly nonlinear wave equations and establish the convergence, up to subsequences, of the associated WIDE minimizers to a solution of the target problem as the parameter goes to zero.},
  author       = {Marveggio, Alice},
  issn         = {2663-337X},
  pages        = {228},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Weak-strong stability and phase-field approximation of interface evolution problems in fluid mechanics and in material sciences}},
  doi          = {10.15479/at:ista:14587},
  year         = {2023},
}