Search

We prove a factorizable version of the Feigin-Frenkel theorem on the center of the completed enveloping algebra of the affine Kac-Moody algebra attached to a simple Lie algebra at the critical level. On any smooth curve C we consider a sheaf of complete topological Lie algebras whose fiber at any point is the usual affine algebra at the critical level and consider its sheaf of completed enveloping algebras. We show that the center of this sheaf is a factorization algebra and establish that it is canonically isomorphic, in a factorizable manner, with the factorization algebra of functions on Opers on the pointed disk.

We extend the theory of fields/distributions developed the paper "A Feigin-Frenkel theorem with n singularities" to a general base scheme. In order to do so we introduce suitable notions of topological sheaves on schemes and study their basic properties. We then construct appropriate analogues of the spaces of fields, consider multiplication of fields between them and rebuild the basic theory of vertex algebras in the setting of global distributions in place of formal power series, which takes the form of chiral algebras introduced Beilinson and Drinfeld in "Chiral Algebras".

The excitation of bound states in the continuum (BICs) in two- or multi-qubit systems lies at the heart of entanglement generation and harnessing in waveguide quantum electrodynamics platforms. However, the generation of qubit pair BICs through single-photon scattering is hindered by the fact that these states are effectively decoupled from propagating photons. We prove that scattering of a parity-invariant single photon on a qubit pair, combined with a properly engineered time variation of the qubit detuning, is not only feasible, but also more effective than strategies based on the relaxation of the excited states of the qubits. The use of tensor network methods to simulate the proposed scheme enables to include photon delays in collision models, thus opening the possibility to follow the time evolution of the full quantum system, including qubits and field, and to efficiently implement and characterize the dynamics in non-ideal cases, which turn out to be optimal for the BIC generation strategy., Comment: 10 pages, 4 figures. For associated video, see http://drive.google.com/file/d/1DJSWkWYcf8sV5oVKmoLxkNXZ-26SuPhJ/view

Prostate cancer is a leading cause of cancer-related deaths among men. The recent development of high frequency, micro-ultrasound imaging offers improved resolution compared to conventional ultrasound and potentially a better ability to differentiate clinically significant cancer from normal tissue. However, the features of prostate cancer remain subtle, with ambiguous borders with normal tissue and large variations in appearance, making it challenging for both machine learning and humans to localize it on micro-ultrasound images. We propose a novel Mask Enhanced Deeply-supervised Micro-US network, termed MedMusNet, to automatically and more accurately segment prostate cancer to be used as potential targets for biopsy procedures. MedMusNet leverages predicted masks of prostate cancer to enforce the learned features layer-wisely within the network, reducing the influence of noise and improving overall consistency across frames. MedMusNet successfully detected 76% of clinically significant cancer with a Dice Similarity Coefficient of 0.365, significantly outperforming the baseline Swin-M2F in specificity and accuracy (Wilcoxon test, Bonferroni correction, p-value<0.05). While the lesion-level and patient-level analyses showed improved performance compared to human experts and different baseline, the improvements did not reach statistical significance, likely on account of the small cohort. We have presented a novel approach to automatically detect and segment clinically significant prostate cancer on B-mode micro-ultrasound images. Our MedMusNet model outperformed other models, surpassing even human experts. These preliminary results suggest the potential for aiding urologists in prostate cancer diagnosis via biopsy and treatment decision-making.

This study investigates the barriers to integrating Design for Assembly (DFA) principles within modular product architectures established using the Modular Function Deployment (MFD) method -- a critical stage for deploying mass customization production while reducing costs. Despite the potential benefits of DFA, its application in modular architectures development remains underutilized, due to a mix of challenges. Through content analysis of qualitative data gathered from a focus group and interviews with industry experts and practitioners, we identified four major categories of such challenges, or barriers to adoption of DFA: technological, economic, regulatory, and organizational (TERO). Key challenges include compliance with regulatory requirements for data usage, intellectual property concerns, and limited availability of quantitative data in the initial stages of MFD. The findings reveal that multidisciplinary collaboration is essential to addressing these barriers, as it enhances informed decision making and eases the practical integration of DFA. By analyzing insights from both academic literature and industrial practice, this research develops a conceptual model that describes the main issues of applying DFA in MFD, providing a valuable guide for companies aiming to improve their modular products assembly process. Ultimately, this study provides groundwork to support industry practitioners in overcoming existing barriers, promoting more cost effective, high quality modular design processes with the inclusion of efficient assembly considerations.

Large angular scale surveys in the absence of atmosphere are essential for measuring the primordial $B$-mode power spectrum of the Cosmic Microwave Background (CMB). Since this proposed measurement is about three to four orders of magnitude fainter than the temperature anisotropies of the CMB, in-flight calibration of the instruments and active suppression of systematic effects are crucial. We investigate the effect of changing the parameters of the scanning strategy on the in-flight calibration effectiveness, the suppression of the systematic effects themselves, and the ability to distinguish systematic effects by null-tests. Next-generation missions such as LiteBIRD, modulated by a Half-Wave Plate (HWP), will be able to observe polarisation using a single detector, eliminating the need to combine several detectors to measure polarisation, as done in many previous experiments and hence avoiding the consequent systematic effects. While the HWP is expected to suppress many systematic effects, some of them will remain. We use an analytical approach to comprehensively address the mitigation of these systematic effects and identify the characteristics of scanning strategies that are the most effective for implementing a variety of calibration strategies in the multi-dimensional space of common spacecraft scan parameters. We also present Falcons, a fast spacecraft scanning simulator that we developed to investigate this scanning parameter space.

We assess the capabilities of the LiteBIRD mission to map the hot gas distribution in the Universe through the thermal Sunyaev-Zeldovich (SZ) effect. Our analysis relies on comprehensive simulations incorporating various sources of Galactic and extragalactic foreground emission, while accounting for specific instrumental characteristics of LiteBIRD, such as detector sensitivities, frequency-dependent beam convolution, inhomogeneous sky scanning, and $1/f$ noise. We implement a tailored component-separation pipeline to map the thermal SZ Compton $y$-parameter over 98% of the sky. Despite lower angular resolution for galaxy cluster science, LiteBIRD provides full-sky coverage and, compared to the Planck satellite, enhanced sensitivity, as well as more frequency bands to enable the construction of an all-sky $y$-map, with reduced foreground contamination at large and intermediate angular scales. By combining LiteBIRD and Planck channels in the component-separation pipeline, we obtain an optimal $y$-map that leverages the advantages of both experiments, with the higher angular resolution of the Planck channels enabling the recovery of compact clusters beyond the LiteBIRD beam limitations, and the numerous sensitive LiteBIRD channels further mitigating foregrounds. The added value of LiteBIRD is highlighted through the examination of maps, power spectra, and one-point statistics of the various sky components. After component separation, the $1/f$ noise from LiteBIRD is effectively mitigated below the thermal SZ signal at all multipoles. Cosmological constraints on $S_8=\sigma_8\left(\Omega_{\rm m}/0.3\right)^{0.5}$ obtained from the LiteBIRD-Planck combined $y$-map power spectrum exhibits a 15% reduction in uncertainty compared to constraints from Planck alone. This improvement can be attributed to the increased portion of uncontaminated sky available in the LiteBIRD-Planck combined $y$-map., Comment: 38 pages, 13 figures, abstract shortened. Updated to match version accepted by JCAP

Axon diameter and myelin thickness are closely related microstructural tissue properties that affect the conduction velocity of action potentials in the nervous system. Imaging them non-invasively with MRI-based methods is thus valuable for studying brain microstructure and function. However, the relationship between MRI-based axon diameter and myelination measures has not been investigated across the brain, mainly due to methodological limitations in estimating axon diameters. In recent years, studies using ultra-high gradient strength diffusion MRI (dMRI) have demonstrated improved estimation of axon diameter across white-matter (WM) tracts in the human brain, making such investigations feasible. In this study, we aim to investigate relationships between tissue microstructure properties with MRI-based methods and compare the imaging findings to histological evidence from the literature. We collected dMRI with ultra-high gradient strength and multi-echo spin-echo MRI on ex vivo macaque and human brain samples on a preclinical scanner. From these data, we estimated axon diameter, intra-axonal signal fraction, myelin water fraction (MWF) and aggregate g-ratio and investigated their correlations. We found that the microstructural imaging parameters exhibited consistent patterns across WM tracts and species. Overall, the findings suggest that MRI-based axon geometry and myelination measures can provide complementary information about fiber morphology, and the relationships between these measures agree with prior histological evidence., Comment: 33 pages, 8 figures

LiteBIRD, the next-generation cosmic microwave background (CMB) experiment, aims for a launch in Japan's fiscal year 2032, marking a major advancement in the exploration of primordial cosmology and fundamental physics. Orbiting the Sun-Earth Lagrangian point L2, this JAXA-led strategic L-class mission will conduct a comprehensive mapping of the CMB polarization across the entire sky. During its 3-year mission, LiteBIRD will employ three telescopes within 15 unique frequency bands (ranging from 34 through 448 GHz), targeting a sensitivity of 2.2\,$\mu$K-arcmin and a resolution of 0.5$^\circ$ at 100\,GHz. Its primary goal is to measure the tensor-to-scalar ratio $r$ with an uncertainty $\delta r = 0.001$, including systematic errors and margin. If $r \geq 0.01$, LiteBIRD expects to achieve a $>5\sigma$ detection in the $\ell=$2-10 and $\ell=$11-200 ranges separately, providing crucial insight into the early Universe. We describe LiteBIRD's scientific objectives, the application of systems engineering to mission requirements, the anticipated scientific impact, and the operations and scanning strategies vital to minimizing systematic effects. We will also highlight LiteBIRD's synergies with concurrent CMB projects., Comment: 23 pages, 9 figures, 1 table, SPIE Astronomical Telescopes + Instrumentation 2024

The Primordial Inflation Explorer (PIXIE) is an Explorer-class mission concept to measure the energy spectrum and linear polarization of the cosmic microwave background (CMB). A single cryogenic Fourier transform spectrometer compares the sky to an external blackbody calibration target, measuring the Stokes I, Q, U parameters to levels ~200 Jy/sr in each 2.65 degree diameter beam over the full sky, in each of 300 frequency channels from 28 GHz to 6 THz. With sensitivity over 1000 times greater than COBE/FIRAS, PIXIE opens a broad discovery space for the origin, contents, and evolution of the universe. Measurements of small distortions from a CMB blackbody spectrum provide a robust determination of the mean electron pressure and temperature in the universe while constraining processes including dissipation of primordial density perturbations, black holes, and the decay or annihilation of dark matter. Full-sky maps of linear polarization measure the optical depth to reionization at nearly the cosmic variance limit and constrain models of primordial inflation. Spectra with sub-percent absolute calibration spanning microwave to far-IR wavelengths provide a legacy data set for analyses including line intensity mapping of extragalactic emission and the cosmic infrared background amplitude and anisotropy. We describe the PIXIE instrument sensitivity, foreground subtraction, and anticipated science return from both the baseline 2-year mission and a potential extended mission., Comment: 44 pages with 18 figures and 4 tables, including full sensitivity curves. Sensitivity curves are available for download at https://lambda.gsfc.nasa.gov/product/pixie/pixie_baseline_noise_get.html

We present the first automated verification technique for confidence-based 2-safety properties, such as global robustness and global fairness, in deep neural networks (DNNs). Our approach combines self-composition to leverage existing reachability analysis techniques and a novel abstraction of the softmax function, which is amenable to automated verification. We characterize and prove the soundness of our static analysis technique. Furthermore, we implement it on top of Marabou, a safety analysis tool for neural networks, conducting a performance evaluation on several publicly available benchmarks for DNN verification., Comment: Accepted at the 36th International Conference on Computer Aided Verification, 2024

The cosmic microwave background (CMB), a remnant of the Big Bang, provides unparalleled insights into the primordial universe, its energy content, and the origin of cosmic structures. The success of forthcoming terrestrial and space experiments hinges on meticulously calibrated data. Specifically, the ability to achieve an absolute calibration of the polarization angles with a precision of < 0.1 deg is crucial to identify the signatures of primordial gravitational waves and cosmic birefringence within the CMB polarization. We introduce the COSMOCal project, designed to deploy a polarized source in space for calibrating microwave frequency observations. The project aims to integrate microwave polarization observations from small and large telescopes, ground-based and in space, into a unified scale, enhancing the effectiveness of each observatory and allowing robust combination of data. To demonstrate the feasibility and confirm the observational approach of our project, we developed a prototype instrument that operates in the atmospheric window centered at 260 GHz, specifically tailored for use with the NIKA2 camera at the IRAM 30 m telescope. We present the instrument components and their laboratory characterization. The results of tests performed with the fully assembled prototype using a KIDs-based instrument, similar concept of NIKA2, are also reported. This study paves the way for an observing campaign using the IRAM 30m telescope and contributes to the development of a space-based instrument., Comment: 13 pages, 13 figures. Published

A (target) quantum system is often measured through observations performed on a second (meter) system to which the target is coupled. In the presence of global conservation laws holding on the joint meter-target system, the Wigner-Araki-Yanase theorem and its generalizations predict a lower-bound on the measurement's error (Ozawa's bound). While practically negligible for macroscopic meters, it becomes relevant for microscopic ones. Here, we propose a simple interferometric setup, arguably within reach of present technology, in which a flying particle (a microscopic quantum meter) is used to measure a qubit by interacting with it in one arm of the interferometer. In this scenario, the globally conserved quantity is the total energy of particle and qubit. We show how the measurement error, $\varepsilon$, is linked to the non-stationary nature of the measured observable and the finite duration of the target-meter interaction while Ozawa's bound, $\varepsilon_{\mathrm B}$, only depends on the momentum uncertainty of the meter's wavepacket. When considering short wavepackets with respect to the evolution time of the qubit, we show that $\varepsilon/\varepsilon_{\mathrm B}$ is strictly tied to the position-momentum uncertainty of the meter's wavepacket and $\varepsilon/\varepsilon_{\mathrm B} \rightarrow 1$ only when employing Gaussian wavepackets. On the contrary, long wavepackets of any shape lead to $\varepsilon/\varepsilon_{\mathrm B} \rightarrow \sqrt{2}$. In addition to their fundamental relevance, our findings have important practical consequences for optimal resource management in quantum technologies., Comment: 5 pages plus appendices. 2 Figures

Optical Bloch Equations (OBEs) are coarse-grained equations modeling the dynamics of driven quantum emitters coupled to heat baths. At the fundamental level, they are derived from the evolution of isolated emitter-field systems ruled by autonomous collision models (ACMs), where the fields encompass both drives and baths. The OBEs have given rise to consistent thermodynamic analyses, where work (heat) flows from the drive (bath). These models do not explicitly capture the emitter-field correlations formed within each collision. Here we build a new kind of ACM which keeps track of these correlations, and exploit it to propose a new thermodynamic framework where correlations play a central role. Within each collision, each system is shown to be driven by an effective Hamiltonian, while a remnant term captures the effect of correlations. On the emitter side, this results in splitting the thermal dissipator in two terms: self-driving term proportional to the atom coherences in the energy basis, and a correlation term. On the field side, the two respectively impact the field amplitude and fluctuations, resulting in a physically observable splitting. Following this, we define work-like (heat-like) flows as the energy changes stemming from the effective Hamiltonian dynamics (correlating processes) which are accessible through -dyne or spectroscopic measurements. Our approach differs from former analyses by the emitter self-work, yielding a tighter expression of the second law. We relate this tightening to the extra-knowledge about the field state, as compared to open system frameworks. This new ACM can be extended to study the impact of correlations on various quantum open systems. It deepens the current understanding of quantum thermodynamics, energy management at quantum scales and can be probed in state-of-the-art quantum hardware, such as superconducting and photonic circuits., Comment: 16+18 pages, 3 figures. Comments are welcome!

Hydrogen radical attacks and subsequent hydrogen migrations are considered to play an important role in the atomic-scale mechanisms of diamond chemical vapour deposition growth. We perform a comprehensive analysis of the reactions involving H-radical and vacancies on H-passivated diamond surfaces exposed to hydrogen radical-rich atmosphere. By means of first principles calculations -- density functional theory and climbing image nudged elastic band method -- transition states related to these mechanisms are identified and characterised. In addition, accurate reaction rates are computed using variational transition state theory. Together, these methods provide -- for a broad range of temperatures and hydrogen radical concentrations -- a picture of the relative likelihood of the migration or radical attack processes, along with a statistical description of the hydrogen coverage fraction of the (100) H-passivated surface, refining earlier results via a more thorough analysis of the processes at stake. Additionally, the migration of H-vacancy is shown to be anisotropic, and occurring preferentially across the dimer rows of the reconstructed surface. The approach used in this work can be generalised to other crystallographic orientations of diamond surfaces or other semiconductors.

Waveguide quantum electrodynamics represents a powerful platform to generate entanglement and tailor photonic states. We consider a pair of identical qubits coupled to a parity invariant waveguide in the microwave domain. By working in the one- and two-excitation sectors, we provide a unified view of decay processes and we show the common origin of directional single photon emission and two photon directional bunching. Unveiling the quantum trajectories, we demonstrate that both phenomena are rooted in the selective coupling of orthogonal qubits Bell states with different photon propagation directions. We comment on how to use this mechanism to implement optimized post-selection of Bell states, heralded by the detection of photons on one qubits side.

We estimate the efficiency of mitigating the lensing $B$-mode polarization, the so-called delensing, for the $LiteBIRD$ experiment with multiple external data sets of lensing-mass tracers. The current best bound on the tensor-to-scalar ratio, $r$, is limited by lensing rather than Galactic foregrounds. Delensing will be a critical step to improve sensitivity to $r$ as measurements of $r$ become more and more limited by lensing. In this paper, we extend the analysis of the recent $LiteBIRD$ forecast paper to include multiple mass tracers, i.e., the CMB lensing maps from $LiteBIRD$ and CMB-S4-like experiment, cosmic infrared background, and galaxy number density from $Euclid$- and LSST-like survey. We find that multi-tracer delensing will further improve the constraint on $r$ by about $20\%$. In $LiteBIRD$, the residual Galactic foregrounds also significantly contribute to uncertainties of the $B$-modes, and delensing becomes more important if the residual foregrounds are further reduced by an improved component separation method., Comment: 21 pages, 7 figures

We explore the capability of measuring lensing signals in $LiteBIRD$ full-sky polarization maps. With a $30$ arcmin beam width and an impressively low polarization noise of $2.16\,\mu$K-arcmin, $LiteBIRD$ will be able to measure the full-sky polarization of the cosmic microwave background (CMB) very precisely. This unique sensitivity also enables the reconstruction of a nearly full-sky lensing map using only polarization data, even considering its limited capability to capture small-scale CMB anisotropies. In this paper, we investigate the ability to construct a full-sky lensing measurement in the presence of Galactic foregrounds, finding that several possible biases from Galactic foregrounds should be negligible after component separation by harmonic-space internal linear combination. We find that the signal-to-noise ratio of the lensing is approximately $40$ using only polarization data measured over $90\%$ of the sky. This achievement is comparable to $Planck$'s recent lensing measurement with both temperature and polarization and represents a four-fold improvement over $Planck$'s polarization-only lensing measurement. The $LiteBIRD$ lensing map will complement the $Planck$ lensing map and provide several opportunities for cross-correlation science, especially in the northern hemisphere.

When a measurement observable does not commute with a quantum system's Hamiltonian, the energy of the measured system is typically not conserved during the measurement. Instead, energy can be transferred between the measured system and the meter. In this work, we experimentally investigate the energetics of non-commuting measurements in a circuit quantum electrodynamics system containing a transmon qubit embedded in a 3D microwave cavity. We show through spectral analysis of the cavity photons that a frequency shift is imparted on the probe, in balance with the associated energy changes of the qubit. Our experiment provides new insights into foundations of quantum measurement, as well as a better understanding of the key mechanisms at play in quantum energetics., Comment: 9 pages, 4 figures

Measuring an observable which does not commute with the Hamiltonian of a quantum system usually modifies the mean energy of this system. In an autonomous measurement scheme, coupling the system to a quantum meter, the system's energy change must be compensated by the meter's energy change. Here, we theoretically study such an autonomous meter-system dynamics: a qubit interacting dispersively with a light pulse propagating in a one-dimensional waveguide. The phase of the light pulse is shifted, conditioned to the qubit's state along the $z$-direction, while the orientation of the qubit Hamiltonian is arbitrary. As the interaction is dispersive, photon number is conserved so that energy balance has to be attained by spectral deformations of the light pulse. Building on analytical and numerical solutions, we reveal the mechanism underlying this spectral deformation and display how it compensates for the qubit's energy change. We explain the formation of a three-peak structure of the output spectrum and we provide the conditions under which this is observable., Comment: 9 pages plus appendices, 9 figures

The Cosmic Microwave Background (CMB) radiation offers a unique window into the early Universe, facilitating precise examinations of fundamental cosmological theories. However, the quest for detecting B-modes in the CMB, predicted by theoretical models of inflation, faces substantial challenges in terms of calibration and foreground modeling. The COSMOCal (COsmic Survey of Millimeter wavelengths Objects for CMB experiments Calibration) project aims at enhancing the accuracy of the absolute calibration of the polarization angle $\psi$ of current and future CMB experiments. The concept includes the build of a very well known artificial source emitting in the frequency range [20-350] GHz that would act as an absolute calibrator for several polarization facilities on Earth. A feasibility study to place the artificial source in geostationary orbit, in the far field for all the telescopes on Earth, is ongoing. In the meanwhile ongoing hardware work is dedicated to build a prototype to test the technology, the precision and the stability of the polarization recovering in the 1 mm band (220-300 GHz). High-resolution experiments as the NIKA2 camera at the IRAM 30m telescope will be deployed for such use. Once carefully calibrated ($\Delta\psi$ < 0.1 degrees) it will be used to observe astrophysical sources such as the Crab nebula, which is the best candidate in the sky for the absolute calibration of CMB experiments., Comment: to appear in Proc. of the mm Universe 2023 conference, Grenoble (France), June 2023, published by F. Mayet et al. (Eds), EPJ Web of conferences, EDP Sciences

The Q&U Bolometric Interferometer for Cosmology (QUBIC) is the first bolometric interferometer designed to measure the primordial B-mode polarization of the Cosmic Microwave Background (CMB). Bolometric interferometry is a novel technique that combines the sensitivity of bolometric detectors with the control of systematic effects that is typical of interferometry, both key features in the quest for the faint signal of the primordial B-modes. A unique feature is the so-called "spectral imaging", i.e., the ability to recover the sky signal in several sub-bands within the physical band during data analysis. This feature provides an in-band spectral resolution of \Delta{\nu}/{\nu} \sim 0.04 that is unattainable by a traditional imager. This is a key tool for controlling the Galactic foregrounds contamination. In this paper, we describe the principles of bolometric interferometry, the current status of the QUBIC experiment and future prospects., Comment: To appear in Proc. of the mm Universe 2023 conference, Grenoble (France), June 2023, published by F. Mayet et al. (Eds), EPJ Web of conferences, EDP Sciences

Quasi-static Rayleigh-B\'enard convection with an imposed horizontal magnetic field is investigated numerically for Chandrasekhar numbers up to $Q=10^6$ with stress free boundary conditions. Both $Q$ and the Rayleigh number ($Ra$) are varied to identify the various dynamical regimes that are present in this system. We find three primary regimes: (I) a two-dimensional (2D) regime in which the axes of the convection rolls are oriented parallel to the imposed magnetic field; (II) an anisotropic three-dimensional (3D) regime; and (III) a mean flow regime characterized by a large scale horizontal flow directed transverse to the imposed magnetic field. The transition to 3D dynamics is preceded by a series of 2D transitions in which the number of convective rolls decreases as $Ra$ is increased. For sufficiently large $Q$, there is an eventual transition to two rolls just prior to the 2D/3D transition. The 2D/3D transition occurs when inertial forces become comparable to the Lorentz force, i.e. when $\sqrt{Q}/Re = O(1)$; 2D, magnetically constrained states persist when $\sqrt{Q}/Re \gtrsim O(1)$. Within the 2D regime we find heat and momentum transport scalings that are consistent with the hydrodynamic asymptotic predictions of Chini and Cox [Phys. Fluids \textbf{21}, 083603 (2009)]: the Nusselt number ($Nu$) and Reynolds number ($Re$) scale as $Nu \sim Ra^{1/3}$ and $Re \sim Ra^{2/3}$, respectively. For $Q=10^6$, we find that the scaling behavior of $Nu$ and $Re$ breaks down at large values of $Ra$ due to a sequence of bifurcations and the eventual manifestation of mean flows., Comment: 31 pages, 9 figures

Cryptographic protocols are hard to design and prove correct, as witnessed by the ever-growing list of attacks even on protocol standards. Symbolic models of cryptography enable automated formal security proofs of such protocols against an idealized model, which abstracts away from the algebraic properties of cryptographic schemes and thus misses attacks. Computational models yield rigorous guarantees but support at present only interactive proofs and/or restricted classes of protocols. A promising approach is given by the computationally complete symbolic attacker (CCSA), formalized in the BC Logic, which aims at bridging and getting the best of the two worlds, obtaining cryptographic guarantees by symbolic analysis. The BC Logic is supported by a recently developed interactive theorem prover, Squirrel, which enables machine-checked interactive security proofs, as opposed to automated ones, thus requiring expert knowledge. We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. The key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations. We overcome the burden of interactive proving in higher-order (HO) logic and automatically establish soundness of cryptographic protocols using only FO reasoning. On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness. On the practical side, CryptoVampire integrates dedicated proof techniques using FO saturation algorithms and heuristics, which enable leveraging the state-of-the-art Vampire FO theorem prover as the underlying proving engine. Our experimental results show CryptoVampire's effectiveness of as a standalone verifier and in terms of automation support for Squirrel.

The human thalamus is a highly connected subcortical grey-matter structure within the brain. It comprises dozens of nuclei with different function and connectivity, which are affected differently by disease. For this reason, there is growing interest in studying the thalamic nuclei in vivo with MRI. Tools are available to segment the thalamus from 1 mm T1 scans, but the contrast of the lateral and internal boundaries is too faint to produce reliable segmentations. Some tools have attempted to incorporate information from diffusion MRI in the segmentation to refine these boundaries, but do not generalise well across diffusion MRI acquisitions. Here we present the first CNN that can segment thalamic nuclei from T1 and diffusion data of any resolution without retraining or fine tuning. Our method builds on a public histological atlas of the thalamic nuclei and silver standard segmentations on high-quality diffusion data obtained with a recent Bayesian adaptive segmentation tool. We combine these with an approximate degradation model for fast domain randomisation during training. Our CNN produces a segmentation at 0.7 mm isotropic resolution, irrespective of the resolution of the input. Moreover, it uses a parsimonious model of the diffusion signal at each voxel (fractional anisotropy and principal eigenvector) that is compatible with virtually any set of directions and b-values, including huge amounts of legacy data. We show results of our proposed method on three heterogeneous datasets acquired on dozens of different scanners. An implementation of the method is publicly available at https://freesurfer.net/fswiki/ThalamicNucleiDTI., Comment: Under review