@phdthesis{14821,
  author       = {Chiossi, Heloisa},
  issn         = {2663 - 337X},
  pages        = {89},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Adaptive hierarchical representations in the hippocampus}},
  doi          = {10.15479/at:ista:14821},
  year         = {2024},
}

@phdthesis{15020,
  abstract     = {This thesis consists of four distinct pieces of work within theoretical biology, with two themes in common: the concept of optimization in biological systems, and the use of information-theoretic tools to quantify biological stochasticity and statistical uncertainty.
Chapter 2 develops a statistical framework for studying biological systems which we believe to be optimized for a particular utility function, such as retinal neurons conveying information about visual stimuli. We formalize such beliefs as maximum-entropy Bayesian priors, constrained by the expected utility. We explore how such priors aid inference of system parameters with limited data and enable optimality hypothesis testing: is the utility higher than by chance?
Chapter 3 examines the ultimate biological optimization process: evolution by natural selection. As some individuals survive and reproduce more successfully than others, populations evolve towards fitter genotypes and phenotypes. We formalize this as accumulation of genetic information, and use population genetics theory to study how much such information can be accumulated per generation and maintained in the face of random mutation and genetic drift. We identify the population size and fitness variance as the key quantities that control information accumulation and maintenance.
Chapter 4 reuses the concept of genetic information from Chapter 3, but from a different perspective: we ask how much genetic information organisms actually need, in particular in the context of gene regulation. For example, how much information is needed to bind transcription factors at correct locations within the genome? Population genetics provides us with a refined answer: with an increasing population size, populations achieve higher fitness by maintaining more genetic information. Moreover, regulatory parameters experience selection pressure to optimize the fitness-information trade-off, i.e. minimize the information needed for a given fitness. This provides an evolutionary derivation of the optimization priors introduced in Chapter 2.
Chapter 5 proves an upper bound on mutual information between a signal and a communication channel output (such as neural activity). Mutual information is an important utility measure for biological systems, but its practical use can be difficult due to the large dimensionality of many biological channels. Sometimes, a lower bound on mutual information is computed by replacing the high-dimensional channel outputs with decodes (signal estimates). Our result provides a corresponding upper bound, provided that the decodes are the maximum posterior estimates of the signal.},
  author       = {Hledik, Michal},
  issn         = {2663 - 337X},
  keywords     = {Theoretical biology, Optimality, Evolution, Information},
  pages        = {158},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Genetic information and biological optimization}},
  doi          = {10.15479/at:ista:15020},
  year         = {2024},
}

@phdthesis{14711,
  abstract     = {In nature, different species find their niche in a range of environments, each with its unique characteristics. While some thrive in uniform (homogeneous) landscapes where environmental conditions stay relatively consistent across space, others traverse the complexities of spatially heterogeneous terrains. Comprehending how species are distributed and how they interact within these landscapes holds the key to gaining insights into their evolutionary dynamics while also informing conservation and management strategies.

For species inhabiting heterogeneous landscapes, when the rate of dispersal is low compared to spatial fluctuations in selection pressure, localized adaptations may emerge. Such adaptation in response to varying selection strengths plays an important role in the persistence of populations in our rapidly changing world. Hence, species in nature are continuously in a struggle to adapt to local environmental conditions, to ensure their continued survival. Natural populations can often adapt in time scales short enough for evolutionary changes to influence ecological dynamics and vice versa, thereby creating a feedback between evolution and demography. The analysis of this feedback and the relative contributions of gene flow, demography, drift, and natural selection to genetic variation and differentiation has remained a recurring theme in evolutionary biology. Nevertheless, the effective role of these forces in maintaining variation and shaping patterns of diversity is not fully understood. Even in homogeneous environments devoid of local adaptations, such understanding remains elusive. Understanding this feedback is crucial, for example in determining the conditions under which extinction risk can be mitigated in peripheral populations subject to deleterious mutation accumulation at the edges of species’ ranges
as well as in highly fragmented populations.

In this thesis we explore both uniform and spatially heterogeneous metapopulations, investigating and providing theoretical insights into the dynamics of local adaptation in the latter and examining the dynamics of load and extinction as well as the impact of joint ecological and evolutionary (eco-evolutionary) dynamics in the former. The thesis is divided into 5 chapters.

Chapter 1 provides a general introduction into the subject matter, clarifying concepts and ideas used throughout the thesis. In chapter 2, we explore how fast a species distributed across a heterogeneous landscape adapts to changing conditions marked by alterations in carrying capacity, selection pressure, and migration rate.

In chapter 3, we investigate how migration selection and drift influences adaptation and the maintenance of variation in a metapopulation with three habitats, an extension of previous models of adaptation in two habitats. We further develop analytical approximations for the critical threshold required for polymorphism to persist.

The focus of chapter 4 of the thesis is on understanding the interplay between ecology and evolution as coupled processes. We investigate how eco-evolutionary feedback between migration, selection, drift, and demography influences eco-evolutionary outcomes in marginal populations subject to deleterious mutation accumulation. Using simulations as well as theoretical approximations of the coupled dynamics of population size and allele frequency, we analyze how gene flow from a large mainland source influences genetic load and population size on an island (i.e., in a marginal population) under genetically realistic assumptions. Analyses of this sort are important because small isolated populations, are repeatedly affected by complex interactions between ecological and evolutionary processes, which can lead to their death. Understanding these interactions can therefore provide an insight into the conditions under which extinction risk can be mitigated in peripheral populations thus, contributing to conservation and restoration efforts.

Chapter 5 extends the analysis in chapter 4 to consider the dynamics of load (due to deleterious mutation accumulation) and extinction risk in a metapopulation. We explore the role of gene flow, selection, and dominance on load and extinction risk and further pinpoint critical thresholds required for metapopulation persistence.

Overall this research contributes to our understanding of ecological and evolutionary mechanisms that shape species’ persistence in fragmented landscapes, a crucial foundation for successful conservation efforts and biodiversity management.},
  author       = {Olusanya, Oluwafunmilola O},
  issn         = {2663 - 337X},
  pages        = {183},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Local adaptation, genetic load and extinction in metapopulations}},
  doi          = {10.15479/at:ista:14711},
  year         = {2024},
}

@article{12349,
  abstract     = {Statistics of natural scenes are not uniform - their structure varies dramatically from ground to sky. It remains unknown whether these non-uniformities are reflected in the large-scale organization of the early visual system and what benefits such adaptations would confer. Here, by relying on the efficient coding hypothesis, we predict that changes in the structure of receptive fields across visual space increase the efficiency of sensory coding. We show experimentally that, in agreement with our predictions, receptive fields of retinal ganglion cells change their shape along the dorsoventral retinal axis, with a marked surround asymmetry at the visual horizon. Our work demonstrates that, according to principles of efficient coding, the panoramic structure of natural scenes is exploited by the retina across space and cell-types.},
  author       = {Gupta, Divyansh and Mlynarski, Wiktor F and Sumser, Anton L and Symonova, Olga and Svaton, Jan and Jösch, Maximilian A},
  issn         = {1546-1726},
  journal      = {Nature Neuroscience},
  pages        = {606--614},
  publisher    = {Springer Nature},
  title        = {{Panoramic visual statistics shape retina-wide organization of receptive fields}},
  doi          = {10.1038/s41593-023-01280-0},
  volume       = {26},
  year         = {2023},
}

@misc{12370,
  abstract     = {Statistics of natural scenes are not uniform - their structure varies dramatically from ground to sky. It remains unknown whether these non-uniformities are reflected in the large-scale organization of the early visual system and what benefits such adaptations would confer. Here, by relying on the efficient coding hypothesis, we predict that changes in the structure of receptive fields across visual space increase the efficiency of sensory coding. We show experimentally that, in agreement with our predictions, receptive fields of retinal ganglion cells change their shape along the dorsoventral retinal axis, with a marked surround asymmetry at the visual horizon. Our work demonstrates that, according to principles of efficient coding, the panoramic structure of natural scenes is exploited by the retina across space and cell-types. },
  author       = {Gupta, Divyansh and Sumser, Anton L and Jösch, Maximilian A},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Research Data for: Panoramic visual statistics shape retina-wide organization of receptive fields}},
  doi          = {10.15479/AT:ISTA:12370},
  year         = {2023},
}

@phdthesis{12470,
  abstract     = {The brain is an exceptionally sophisticated organ consisting of billions of cells and trillions of 
connections that orchestrate our cognition and behavior. To decode its complex connectivity, it is 
pivotal to disentangle its intricate architecture spanning from cm-sized circuits down to tens of 
nm-small synapses.
To achieve this goal, I developed CATS – Comprehensive Analysis of nervous Tissue across 
Scales, a versatile toolbox for obtaining a holistic view of nervous tissue context with (superresolution) fluorescence microscopy. CATS combines comprehensive labeling of the extracellular
space, that is compatible with chemical fixation, with information on molecular markers, superresolved data acquisition and machine-learning based data analysis for segmentation and synapse 
identification.
I used CATS to analyze key features of nervous tissue connectivity, ranging from whole tissue 
architecture, neuronal in- and output-fields, down to synapse morphology.
Focusing on the hippocampal circuitry, I quantified synaptic transmission properties of mossy 
fiber boutons and analyzed the connectivity pattern of dentate gyrus granule cells with CA3 
pyramidal neurons. This shows that CATS is a viable tool to study hallmarks of neuronal 
connectivity with light microscopy.},
  author       = {Michalska, Julia M},
  isbn         = { 978-3-99078-026-8},
  issn         = {2663-337X},
  pages        = {201},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{A versatile toolbox for the comprehensive analysis of nervous tissue organization with light microscopy}},
  doi          = {10.15479/at:ista:12470},
  year         = {2023},
}

@phdthesis{12826,
  abstract     = {During navigation, animals can infer the structure of the environment by computing the optic flow cues elicited by their own movements, and subsequently use this information to instruct proper locomotor actions. These computations require a panoramic assessment of the visual environment in order to disambiguate similar sensory experiences that may require distinct behavioral responses. The estimation of the global motion patterns is therefore essential for successful navigation. Yet, our understanding of the algorithms and implementations that enable coherent panoramic visual perception remains scarce. Here I pursue this problem by dissecting the functional aspects of interneuronal communication in the lobula plate tangential cell network in Drosophila melanogaster. The results presented in the thesis demonstrate that the basis for effective interpretation of the optic flow in this circuit are stereotyped synaptic connections that mediate the formation of distinct subnetworks, each extracting a particular pattern of global motion. 
Firstly, I show that gap junctions are essential for a correct interpretation of binocular motion cues by horizontal motion-sensitive cells. HS cells form electrical synapses with contralateral H2 neurons that are involved in detecting yaw rotation and translation. I developed an FlpStop-mediated mutant of a gap junction protein ShakB that disrupts these electrical synapses. While the loss of electrical synapses does not affect the tuning of the direction selectivity in HS neurons, it severely alters their sensitivity to horizontal motion in the contralateral side. These physiological changes result in an inappropriate integration of binocular motion cues in walking animals. While wild-type flies form a binocular perception of visual motion by non-linear integration of monocular optic flow cues, the mutant flies sum the monocular inputs linearly. These results indicate that rather than averaging signals in neighboring neurons, gap-junctions operate in conjunction with chemical synapses to mediate complex non-linear optic flow computations.
Secondly, I show that stochastic manipulation of neuronal activity in the lobula plate tangential cell network is a powerful approach to study the neuronal implementation of optic flow-based navigation in flies. Tangential neurons form multiple subnetworks, each mediating course-stabilizing response to a particular global pattern of visual motion. Application of genetic mosaic techniques can provide sparse optogenetic activation of HS cells in numerous combinations. These distinct combinations of activated neurons drive an array of distinct behavioral responses, providing important insights into how visuomotor transformation is performed in the lobula plate tangential cell network. This approach can be complemented by stochastic silencing of tangential neurons, enabling direct assessment of the functional role of individual tangential neurons in the processing of specific visual motion patterns.
	Taken together, the findings presented in this thesis suggest that establishing specific activity patterns of tangential cells via stereotyped synaptic connectivity is a key to efficient optic flow-based navigation in Drosophila melanogaster.},
  author       = {Pokusaeva, Victoria},
  issn         = {2663 - 337X},
  pages        = {106},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Neural control of optic flow-based navigation in Drosophila melanogaster}},
  doi          = {10.15479/at:ista:12826},
  year         = {2023},
}

@phdthesis{12885,
  abstract     = {High-performance semiconductors rely upon precise control of heat and charge transport. This can be achieved by precisely engineering defects in polycrystalline solids. There are multiple approaches to preparing such polycrystalline semiconductors, and the transformation of solution-processed colloidal nanoparticles is appealing because colloidal nanoparticles combine low cost with structural and compositional tunability along with rich surface chemistry. However, the multiple processes from nanoparticle synthesis to the final bulk nanocomposites are very complex. They involve nanoparticle purification, post-synthetic modifications, and finally consolidation (thermal treatments and densification). All these properties dictate the final material’s composition and microstructure, ultimately affecting its functional properties. This thesis explores the synthesis, surface chemistry and consolidation of colloidal semiconductor nanoparticles into dense solids. In particular, the transformations that take place during these processes, and their effect on the material’s transport properties are evaluated. },
  author       = {Calcabrini, Mariano},
  isbn         = {978-3-99078-028-2},
  issn         = {2663-337X},
  pages        = {82},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Nanoparticle-based semiconductor solids: From synthesis to consolidation}},
  doi          = {10.15479/at:ista:12885},
  year         = {2023},
}

@phdthesis{12964,
  abstract     = {Pattern formation is of great importance for its contribution across different biological behaviours. During developmental processes for example, patterns of chemical gradients are
established to determine cell fate and complex tissue patterns emerge to define structures such
as limbs and vascular networks. Patterns are also seen in collectively migrating groups, for
instance traveling waves of density emerging in moving animal flocks as well as collectively migrating cells and tissues. To what extent these biological patterns arise spontaneously through
the local interaction of individual constituents or are dictated by higher level instructions is
still an open question however there is evidence for the involvement of both types of process.
Where patterns arise spontaneously there is a long standing interest in how far the interplay
of mechanics, e.g. force generation and deformation, and chemistry, e.g. gene regulation
and signaling, contributes to the behaviour. This is because many systems are able to both
chemically regulate mechanical force production and chemically sense mechanical deformation,
forming mechano-chemical feedback loops which can potentially become unstable towards
spatio and/or temporal patterning.
We work with experimental collaborators to investigate the possibility that this type of
interaction drives pattern formation in biological systems at different scales. We focus first on
tissue-level ERK-density waves observed during the wound healing response across different
systems where many previous studies have proposed that patterns depend on polarized cell
migration and arise from a mechanical flocking-like mechanism. By combining theory with
mechanical and optogenetic perturbation experiments on in vitro monolayers we instead find
evidence for mechanochemical pattern formation involving only scalar bilateral feedbacks
between ERK signaling and cell contraction. We perform further modeling and experiment
to study how this instability couples with polar cell migration in order to produce a robust
and efficient wound healing response. In a following chapter we implement ERK-density
coupling and cell migration in a 2D active vertex model to investigate the interaction of
ERK-density patterning with different tissue rheologies and find that the spatio-temporal
dynamics are able to both locally and globally fluidize a tissue across the solid-fluid glass
transition. In a last chapter we move towards lower spatial scales in the context of subcellular
patterning of the cell cytoskeleton where we investigate the transition between phases of
spatially homogeneous temporal oscillations and chaotic spatio-temporal patterning in the
dynamics of myosin and ROCK activities (a motor component of the actomyosin cytoskeleton
and its activator). Experimental evidence supports an intrinsic chemical oscillator which we
encode in a reaction model and couple to a contractile active gel description of the cell cortex.
The model exhibits phases of chemical oscillations and contractile spatial patterning which
reproduce many features of the dynamics seen in Drosophila oocyte epithelia in vivo. However,
additional pharmacological perturbations to inhibit myosin contractility leaves the role of
contractile instability unclear. We discuss alternative hypotheses and investigate the possibility
of reaction-diffusion instability.},
  author       = {Boocock, Daniel R},
  isbn         = {978-3-99078-032-9},
  issn         = {2663-337X},
  pages        = {146},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Mechanochemical pattern formation across biological scales}},
  doi          = {10.15479/at:ista:12964},
  year         = {2023},
}

@phdthesis{13074,
  abstract     = {Deep learning has become an integral part of a large number of important applications, and many of the recent breakthroughs have been enabled by the ability to train very large models, capable to capture complex patterns and relationships from the data. At the same time, the massive sizes of modern deep learning models have made their deployment to smaller devices more challenging; this is particularly important, as in many applications the users rely on accurate deep learning predictions, but they only have access to devices with limited memory and compute power. One solution to this problem is to prune neural networks, by setting as many of their parameters as possible to zero, to obtain accurate sparse models with lower memory footprint. Despite the great research progress in obtaining sparse models that preserve accuracy, while satisfying memory and computational constraints, there are still many challenges associated with efficiently training sparse models, as well as understanding their generalization properties.

The focus of this thesis is to investigate how the training process of sparse models can be made more efficient, and to understand the differences between sparse and dense models in terms of how well they can generalize to changes in the data distribution. We first study a method for co-training sparse and dense models, at a lower cost compared to regular training. With our method we can obtain very accurate sparse networks, and dense models that can recover the baseline accuracy. Furthermore, we are able to more easily analyze the differences, at prediction level, between the sparse-dense model pairs. Next, we investigate the generalization properties of sparse neural networks in more detail, by studying how well different sparse models trained on a larger task can adapt to smaller, more specialized tasks, in a transfer learning scenario. Our analysis across multiple pruning methods and sparsity levels reveals that sparse models provide features that can transfer similarly to or better than the dense baseline. However, the choice of the pruning method plays an important role, and can influence the results when the features are fixed (linear finetuning), or when they are allowed to adapt to the new task (full finetuning). Using sparse models with fixed masks for finetuning on new tasks has an important practical advantage, as it enables training neural networks on smaller devices. However, one drawback of current pruning methods is that the entire training cycle has to be repeated to obtain the initial sparse model, for every sparsity target; in consequence, the entire training process is costly and also multiple models need to be stored. In the last part of the thesis we propose a method that can train accurate dense models that are compressible in a single step, to multiple sparsity levels, without additional finetuning. Our method results in sparse models that can be competitive with existing pruning methods, and which can also successfully generalize to new tasks.},
  author       = {Peste, Elena-Alexandra},
  issn         = {2663-337X},
  pages        = {147},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Efficiency and generalization of sparse neural networks}},
  doi          = {10.15479/at:ista:13074},
  year         = {2023},
}

@misc{13126,
  abstract     = {Mapping the complex and dense arrangement of cells and their connectivity in brain tissue demands nanoscale spatial resolution imaging. Super-resolution optical microscopy excels at visualizing specific molecules and individual cells but fails to provide tissue context. Here, we developed Comprehensive Analysis of Tissues across Scales (CATS), a technology to densely map brain tissue architecture from millimeter regional to nanometer synaptic scales in diverse chemically fixed brain preparations, including rodent and human. CATS uses fixation-compatible extracellular labeling and optical imaging, including stimulated emission depletion or expansion microscopy, to comprehensively delineate cellular structures. It enables three-dimensional reconstruction of single synapses and mapping of synaptic connectivity by identification and analysis of putative synaptic cleft regions. Applying CATS to the mouse hippocampal mossy fiber circuitry, we reconstructed and quantified the synaptic input and output structure of identified neurons. We furthermore demonstrate applicability to clinically derived human tissue samples, including formalin-fixed paraffin-embedded routine diagnostic specimens, for visualizing the cellular architecture of brain tissue in health and disease.},
  author       = {Danzl, Johann G},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Research data for the publication "Imaging brain tissue architecture across millimeter to nanometer scales"}},
  doi          = {10.15479/AT:ISTA:13126},
  year         = {2023},
}

@inproceedings{13142,
  abstract     = {Reinforcement learning has received much attention for learning controllers of deterministic systems. We consider a learner-verifier framework for stochastic control systems and survey recent methods that formally guarantee a conjunction of reachability and safety properties. Given a property and a lower bound on the probability of the property being satisfied, our framework jointly learns a control policy and a formal certificate to ensure the satisfaction of the property with a desired probability threshold. Both the control policy and the formal certificate are continuous functions from states to reals, which are learned as parameterized neural networks. While in the deterministic case, the certificates are invariant and barrier functions for safety, or Lyapunov and ranking functions for liveness, in the stochastic case the certificates are supermartingales. For certificate verification, we use interval arithmetic abstract interpretation to bound the expected values of neural network functions.},
  author       = {Chatterjee, Krishnendu and Henzinger, Thomas A and Lechner, Mathias and Zikelic, Dorde},
  booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems },
  isbn         = {9783031308222},
  issn         = {1611-3349},
  location     = {Paris, France},
  pages        = {3--25},
  publisher    = {Springer Nature},
  title        = {{A learner-verifier framework for neural network controllers and certificates of stochastic systems}},
  doi          = {10.1007/978-3-031-30823-9_1},
  volume       = {13993},
  year         = {2023},
}

@article{13267,
  abstract     = {Three-dimensional (3D) reconstruction of living brain tissue down to an individual synapse level would create opportunities for decoding the dynamics and structure–function relationships of the brain’s complex and dense information processing network; however, this has been hindered by insufficient 3D resolution, inadequate signal-to-noise ratio and prohibitive light burden in optical imaging, whereas electron microscopy is inherently static. Here we solved these challenges by developing an integrated optical/machine-learning technology, LIONESS (live information-optimized nanoscopy enabling saturated segmentation). This leverages optical modifications to stimulated emission depletion microscopy in comprehensively, extracellularly labeled tissue and previous information on sample structure via machine learning to simultaneously achieve isotropic super-resolution, high signal-to-noise ratio and compatibility with living tissue. This allows dense deep-learning-based instance segmentation and 3D reconstruction at a synapse level, incorporating molecular, activity and morphodynamic information. LIONESS opens up avenues for studying the dynamic functional (nano-)architecture of living brain tissue.},
  author       = {Velicky, Philipp and Miguel Villalba, Eder and Michalska, Julia M and Lyudchik, Julia and Wei, Donglai and Lin, Zudi and Watson, Jake and Troidl, Jakob and Beyer, Johanna and Ben Simon, Yoav and Sommer, Christoph M and Jahr, Wiebke and Cenameri, Alban and Broichhagen, Johannes and Grant, Seth G.N. and Jonas, Peter M and Novarino, Gaia and Pfister, Hanspeter and Bickel, Bernd and Danzl, Johann G},
  issn         = {1548-7105},
  journal      = {Nature Methods},
  pages        = {1256--1265},
  publisher    = {Springer Nature},
  title        = {{Dense 4D nanoscale reconstruction of living brain tissue}},
  doi          = {10.1038/s41592-023-01936-6},
  volume       = {20},
  year         = {2023},
}

@inproceedings{14830,
  abstract     = {We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for providing formal reach-avoid guarantees, which combine and generalize stability and safety guarantees, with a tolerable probability threshold p in [0,1] over the infinite time horizon. Our method leverages advances in machine learning literature and it represents formal certificates as neural networks. In particular, we learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our RASMs provide reachability and avoidance guarantees by imposing constraints on what can be viewed as a stochastic extension of level sets of Lyapunov functions for deterministic systems. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification. We validate our approach on 3 stochastic non-linear reinforcement learning tasks.},
  author       = {Zikelic, Dorde and Lechner, Mathias and Henzinger, Thomas A and Chatterjee, Krishnendu},
  booktitle    = {Proceedings of the 37th AAAI Conference on Artificial Intelligence},
  issn         = {2374-3468},
  keywords     = {General Medicine},
  location     = {Washington, DC, United States},
  number       = {10},
  pages        = {11926--11935},
  publisher    = {Association for the Advancement of Artificial Intelligence},
  title        = {{Learning control policies for stochastic systems with reach-avoid guarantees}},
  doi          = {10.1609/aaai.v37i10.26407},
  volume       = {37},
  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},
}

@inproceedings{14242,
  abstract     = {We study the problem of training and certifying adversarially robust quantized neural networks (QNNs). Quantization is a technique for making neural networks more efficient by running them using low-bit integer arithmetic and is therefore commonly adopted in industry. Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization, and certification of the quantized representation is necessary to guarantee robustness. In this work, we present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs. Inspired by advances in robust learning of non-quantized networks, our training algorithm computes the gradient of an abstract representation of the actual network. Unlike existing approaches, our method can handle the discrete semantics of QNNs. Based on QA-IBP, we also develop a complete verification procedure for verifying the adversarial robustness of QNNs, which is guaranteed to terminate and produce a correct answer. Compared to existing approaches, the key advantage of our verification procedure is that it runs entirely on GPU or other accelerator devices. We demonstrate experimentally that our approach significantly outperforms existing methods and establish the new state-of-the-art for training and certifying the robustness of QNNs.},
  author       = {Lechner, Mathias and Zikelic, Dorde and Chatterjee, Krishnendu and Henzinger, Thomas A and Rus, Daniela},
  booktitle    = {Proceedings of the 37th AAAI Conference on Artificial Intelligence},
  isbn         = {9781577358800},
  location     = {Washington, DC, United States},
  number       = {12},
  pages        = {14964--14973},
  publisher    = {Association for the Advancement of Artificial Intelligence},
  title        = {{Quantization-aware interval bound propagation for training certifiably robust quantized neural networks}},
  doi          = {10.1609/aaai.v37i12.26747},
  volume       = {37},
  year         = {2023},
}

@inproceedings{14243,
  abstract     = {Two-player zero-sum "graph games" are central in logic, verification, and multi-agent systems. The game proceeds by placing a token on a vertex of a graph, and allowing the players to move it to produce an infinite path, which determines the winner or payoff of the game. Traditionally, the players alternate turns in moving the token. In "bidding games", however, the players have budgets and in each turn, an auction (bidding) determines which player moves the token. So far, bidding games have only been studied as full-information games. In this work we initiate the study of partial-information bidding games: we study bidding games in which a player's initial budget is drawn from a known probability distribution. We show that while for some bidding mechanisms and objectives, it is straightforward to adapt the results from the full-information setting to the partial-information setting, for others, the analysis is significantly more challenging, requires new techniques, and gives rise to interesting results. Specifically, we study games with "mean-payoff" objectives in combination with "poorman" bidding. We construct optimal strategies for a partially-informed player who plays against a fully-informed adversary. We show that, somewhat surprisingly, the "value" under pure strategies does not necessarily exist in such games.},
  author       = {Avni, Guy and Jecker, Ismael R and Zikelic, Dorde},
  booktitle    = {Proceedings of the 37th AAAI Conference on Artificial Intelligence},
  isbn         = {9781577358800},
  location     = {Washington, DC, United States},
  number       = {5},
  pages        = {5464--5471},
  title        = {{Bidding graph games with partially-observable budgets}},
  doi          = {10.1609/aaai.v37i5.25679},
  volume       = {37},
  year         = {2023},
}

@article{14257,
  abstract     = {Mapping the complex and dense arrangement of cells and their connectivity in brain tissue demands nanoscale spatial resolution imaging. Super-resolution optical microscopy excels at visualizing specific molecules and individual cells but fails to provide tissue context. Here we developed Comprehensive Analysis of Tissues across Scales (CATS), a technology to densely map brain tissue architecture from millimeter regional to nanometer synaptic scales in diverse chemically fixed brain preparations, including rodent and human. CATS uses fixation-compatible extracellular labeling and optical imaging, including stimulated emission depletion or expansion microscopy, to comprehensively delineate cellular structures. It enables three-dimensional reconstruction of single synapses and mapping of synaptic connectivity by identification and analysis of putative synaptic cleft regions. Applying CATS to the mouse hippocampal mossy fiber circuitry, we reconstructed and quantified the synaptic input and output structure of identified neurons. We furthermore demonstrate applicability to clinically derived human tissue samples, including formalin-fixed paraffin-embedded routine diagnostic specimens, for visualizing the cellular architecture of brain tissue in health and disease.},
  author       = {Michalska, Julia M and Lyudchik, Julia and Velicky, Philipp and Korinkova, Hana and Watson, Jake and Cenameri, Alban and Sommer, Christoph M and Amberg, Nicole and Venturino, Alessandro and Roessler, Karl and Czech, Thomas and Höftberger, Romana and Siegert, Sandra and Novarino, Gaia and Jonas, Peter M and Danzl, Johann G},
  issn         = {1546-1696},
  journal      = {Nature Biotechnology},
  publisher    = {Springer Nature},
  title        = {{Imaging brain tissue architecture across millimeter to nanometer scales}},
  doi          = {10.1038/s41587-023-01911-8},
  year         = {2023},
}

@inproceedings{14317,
  abstract     = {Markov decision processes can be viewed as transformers of probability distributions. While this view is useful from a practical standpoint to reason about trajectories of distributions, basic reachability and safety problems are known to be computationally intractable (i.e., Skolem-hard) to solve in such models. Further, we show that even for simple examples of MDPs, strategies for safety objectives over distributions can require infinite memory and randomization.
In light of this, we present a novel overapproximation approach to synthesize strategies in an MDP, such that a safety objective over the distributions is met. More precisely, we develop a new framework for template-based synthesis of certificates as affine distributional and inductive invariants for safety objectives in MDPs. We provide two algorithms within this framework. One can only synthesize memoryless strategies, but has relative completeness guarantees, while the other can synthesize general strategies. The runtime complexity of both algorithms is in PSPACE. We implement these algorithms and show that they can solve several non-trivial examples.},
  author       = {Akshay, S. and Chatterjee, Krishnendu and Meggendorfer, Tobias and Zikelic, Dorde},
  booktitle    = {International Conference on Computer Aided Verification},
  isbn         = {9783031377082},
  issn         = {1611-3349},
  location     = {Paris, France},
  pages        = {86--112},
  publisher    = {Springer Nature},
  title        = {{MDPs as distribution transformers: Affine invariant synthesis for safety objectives}},
  doi          = {10.1007/978-3-031-37709-9_5},
  volume       = {13966},
  year         = {2023},
}

