IST Austria: PubRep (Institute of Science and Technology)
Not a member yet
6140 research outputs found
Sort by
RefinedProsa: Connecting response-time analysis with C verification for interrupt-free schedulers
No full textThere has been a recent upsurge of interest in formal, machine-checked verification of timing guarantees for C implementations of real-time system schedulers. However, prior work has only considered tick-based schedulers, which enjoy a clearly defined notion of time: the time "quantum". In this work, we present a new approach to real-time systems verification for interrupt-free schedulers, which are commonly used in deeply embedded and resource-constrained systems but which do not enjoy a natural notion of periodic time. Our approach builds on and connects two recently developed Rocq-based systems—RefinedC (for foundational C verification) and Prosa (for verified response-time analysis)—adapting the former to reason about timed traces and the latter to reason about overheads. We apply the resulting system, which we call RefinedProsa, to verify Rössl, a simple yet representative, fixed-priority, non-preemptive, interrupt-free scheduler implemented in C
Layer-specific control of inhibition by NDNF interneurons
No full textNeuronal processing of external sensory input is shaped by internally generated top–down information. In the neocortex, top–down projections primarily target layer 1, which contains NDNF (neuron-derived neurotrophic factor)-expressing interneurons and the dendrites of pyramidal cells. Here, we investigate the hypothesis that NDNF interneurons shape cortical computations in an unconventional, layer-specific way, by exerting presynaptic inhibition on synapses in layer 1 while leaving synapses in deeper layers unaffected. We first confirm experimentally that in the auditory cortex, synapses from somatostatin-expressing (SOM) onto NDNF neurons are indeed modulated by ambient Gamma-aminobutyric acid (GABA). Shifting to a computational model, we then show that this mechanism introduces a distinct mutual inhibition motif between NDNF interneurons and the synaptic outputs of SOM interneurons. This motif can control inhibition in a layer-specific way and introduces competition between NDNF and SOM interneurons for dendritic inhibition onto pyramidal cells on different timescales. NDNF interneurons can thereby control cortical information flow by redistributing dendritic inhibition from fast to slow timescales and by gating different sources of dendritic inhibition
Moist convective scaling: Insights from an idealised model
No full textThe response of clouds and moist-convective processes to heat loss to space by long-wave radiative cooling is an important feedback in the Earth's atmosphere. It is known that moist convection increases roughly in equilibrium with radiative cooling, an assumption often made in simplified models of the tropical atmosphere. In this study, we use an idealised two-dimensional model of the atmosphere introduced by Vallis et. al. and incorporate a bulk-cooling term, which is an idealisation of radiative cooling in the atmosphere. We comment briefly on the static stability of the system to dry and moist convection and characteris its moist convective response to changes in the bulk cooling. We find that, while the clear-sky regions of the model respond directly to the change in the cooling term, the regions dominated by moist convective plumes are insensitive to changes in cooling. Similar to previous findings from cloud-resolving models, we too find in our idealised setting that the majority of the increase in convection occurs via an increase in the areal coverage of convection, rather than its intensity. We argue that these small-scale convective processes are an upper bound on how quickly convective intensity can change to stay in equilibrium with radiative cooling
Cataclysmic variables and AM CVn binaries in SRG/eROSITA + Gaia: Volume limited samples, X-ray luminosity functions, and space densities
No full textWe present volume-limited samples of cataclysmic variables (CVs) and AM CVn binaries jointly selected from SRG/eROSITA eRASS1 and Gaia DR3 using an X-ray + optical color–color diagram (the "X-ray Main Sequence"). This tool identifies all CV subtypes, including magnetic and low-accretion rate systems, in contrast to most previous surveys. We find 23 CVs, 3 of which are AM CVns, out to 150 pc in the Western Galactic Hemisphere. Our 150 pc sample is spectroscopically verified and complete down to LX = 1.3 × 1029 erg s−1 in the 0.2–2.3 keV band, and we also present CV candidates out to 300 pc and 1000 pc. We discovered two previously unknown systems in our 150 pc sample: the third nearest AM CVn and a magnetic period bouncer. We find the mean LX of CVs to be 〈LX〉 ≈ 4.6 × 1030 erg s−1, in contrast to previous surveys which yielded 〈LX〉 ∼ 1031−1032 erg s−1. We construct X-ray luminosity functions that, for the first time, flatten out at LX ∼ 1030 erg s−1. We infer average number, mass, and luminosity densities of ρN,CV = (3.7 ± 0.7) × 10−6pc−3, (math formular), and (math formular), respectively, in the solar neighborhood. Our uniform selection method also allows us to place meaningful estimates on the space density of AM CVns, ρN,AM CVn = (5.5 ± 3.7) × 10−7 pc−3. Magnetic CVs and period bouncers make up 35% and 25% of our sample, respectively. This work, through a novel discovery technique, shows that the observed number densities of CVs and AM CVns, as well as the fraction of period bouncers, are still in tension with population synthesis estimates
Human hippocampal CA3 uses specific functional connectivity rules for efficient associative memory
No full textOur brain has remarkable computational power, generating sophisticated behaviors, storing memories over an individual’s lifetime, and producing higher cognitive functions. However, little of our neuroscience knowledge covers the human brain. Is this organ truly unique, or is it a scaled version of the extensively studied rodent brain? Combining multicellular patch-clamp recording with expansion-based superresolution microscopy and full-scale modeling, we determined the cellular and microcircuit properties of the human hippocampal CA3 region, a fundamental circuit for memory storage. In contrast to neocortical networks, human hippocampal CA3 displayed sparse connectivity, providing a circuit architecture that maximizes associational power. Human synapses showed unique reliability, high precision, and long integration times, exhibiting both species- and circuit-specific properties. Together with expanded neuronal numbers, these circuit characteristics greatly enhanced the memory storage capacity of CA3. Our results reveal distinct microcircuit properties of the human hippocampus and begin to unravel the inner workings of our most complex organ
Loschmidt echo for deformed Wigner matrices
No full textWe consider two Hamiltonians that are close to each other, H1≈H2, and analyze the time-decay of the corresponding Loschmidt echo M(t):=|⟨ψ0,eitH2e−itH1ψ0⟩|2 that expresses the effect of an imperfect time reversal on the initial state ψ0. Our model Hamiltonians are deformed Wigner matrices that do not share a common eigenbasis. The main tools for our results are two-resolvent laws for such H1 and H2
PMLR
No full textFiltering-based probabilistic numerical solvers for ordinary differential equations (ODEs), also known as ODE filters, have been established as efficient methods for quantifying numerical uncertainty in the solution of ODEs. In practical applications, however, the underlying dynamical system often contains uncertain parameters, requiring the propagation of this model uncertainty to the ODE solution. In this paper, we demonstrate that ODE filters, despite their probabilistic nature, do not automatically solve this uncertainty propagation problem. To address this limitation, we present a novel approach that combines ODE filters with numerical quadrature to properly marginalize over uncertain parameters, while accounting for both parameter uncertainty and numerical solver uncertainty. Experiments across multiple dynamical systems demonstrate that the resulting uncertainty estimates closely match reference solutions. Notably, we show
how the numerical uncertainty from the ODE solver can help prevent overconfidence in the propagated uncertainty estimates, especially when using larger step sizes. Our results illustrate that probabilistic numerical methods can effectively quantify both numerical and parametric uncertainty in dynamical systems
ISTA Thesis
No full textThe space of codimension-2 shapes, such as curves in 3D and surfaces in 4D, is an infinite-dimensional manifold. This thesis explores geometric structures and dynamics on this space, with emphasis on their implications for physics, particularly hydrodynamics.
Our investigation ranges from theoretical studies of infinite-dimensional symplectic and prequantum geometry to numerical computation of the time evolution of shapes. The thesis presents four main contributions.
In the first part, we introduce implicit representations of codimension-2 shapes using a class of complex-valued functions, and prove that the space of these implicit representations forms a prequantum bundle over the codimension-2 shape space. This reveals a new geometric interpretation of the canonical symplectic structure on the codimension-2 shape space.
In the second part, we use implicit representations to develop a simulation method for the dynamics of space curves. To handle chaotic systems such as vortex filaments in hydrodynamics, we exploit the infinite degrees of freedom, hidden in both the configuration and dynamics of implicit representations.
In the third part, we introduce new symplectic structures on the space of space curves, which generalize the only previously known symplectic structure on this space, allowing for new Hamiltonian dynamics of space curves.
In the fourth part, we apply a symplectic viewpoint to a differential geometric problem with practical applications. We derive a new area formula for spherical polygons via prequantization
LNCS
No full textPolynomial quantified entailments with existentially and universally quantified variables arise in many problems of verification and program analysis. We present PolyQEnt which is a tool for solving polynomial quantified entailments in which variables on both sides of the implication are real valued or unbounded integers. Our tool provides a unified framework for polynomial quantified entailment problems that arise in several papers in the literature. Our experimental evaluation over a wide range of benchmarks shows the applicability of the tool as well as its benefits as opposed to simply using existing SMT solvers to solve such constraints