@article{17435, abstract = {The Mediterranean region is experiencing pronounced aridification and in certain areas higher occurrence of intense precipitation. In this work, we analyze the evolution of the precipitation probability distribution in terms of precipitating days (or “wet-days”) and all-days quantile trends, in Europe and the Mediterranean, using the ERA5 reanalysis. Looking at the form of wet-days quantile trends curves, we identify four regimes. Two are predominant: in most of northern Europe the precipitation quantiles all intensify, while in the Mediterranean the low-medium quantiles are mostly decreasing as extremes intensify or decrease. The wet-days distribution is then modeled by a Weibull law with two parameters, whose changes capture the four regimes. Assessing the significance of the parameters' changes over 1950–2020 shows that a signal on wet-days distribution has already emerged in northern Europe (where the distribution shifts to more intense precipitation), but not yet in the Mediterranean, where the natural variability is stronger. We extend the results by describing the all-days distribution change as the wet-days’ change plus a contribution from the dry-days frequency change, and study their relative contribution. In northern Europe, the wet-days distribution change is the dominant driver, and the contribution of dry-days frequency change can be neglected for wet-days percentiles above about 50%. In the Mediterranean, however, the change of precipitation distribution comes from the significant increase of dry-days frequency instead of an intensity change during wet-days. Therefore, in the Mediterranean the increase of dry-days frequency is crucial for all-days trends, even for heavy precipitation.}, author = {André, Julie and D'Andrea, Fabio and Drobinski, Philippe and Muller, Caroline J}, issn = {2169-8996}, journal = {Journal of Geophysical Research: Atmospheres}, number = {15}, publisher = {Wiley}, title = {{Regimes of precipitation change over Europe and the Mediterranean}}, doi = {10.1029/2023JD040413}, volume = {129}, year = {2024}, } @article{17436, abstract = {The auxin signaling molecule controls a variety of growth and developmental processes in land plants. Auxin regulates gene expression through a nuclear auxin signaling pathway (NAP) consisting of the ubiquitin ligase auxin receptor TIR1/AFB, its Aux/IAA degradation substrate, and DNA-binding ARF transcription factors. Although extensive qualitative understanding of the pathway and its interactions has been obtained, mostly by studying the flowering plant Arabidopsis thaliana, it remains unknown how these translate to quantitative system behavior in vivo, a problem that is confounded by the large NAP gene families in most species. Here, we used the minimal NAP of the liverwort Marchantia polymorpha to quantitatively map NAP protein accumulation and dynamics in vivo through the use of knockin fluorescent fusion proteins. Beyond revealing the dynamic native accumulation profile of the entire NAP protein network, we discovered that the two central ARFs, MpARF1 and MpARF2, are proteasomally degraded. This auxin-independent degradation tunes ARF protein stoichiometry to favor gene activation, thereby reprogramming auxin response during the developmental progression. Thus, quantitative analysis of the entire NAP has enabled us to identify ARF degradation and the stoichiometries of activator and repressor ARFs as a potential mechanism for controlling gemma germination.}, author = {Das, Shubhajit and De Roij, Martijn and Bellows, Simon and Alvarez, Melissa Dipp and Mutte, Sumanth and Kohlen, Wouter and Farcot, Etienne and Weijers, Dolf and Borst, Jan Willem}, issn = {2590-3462}, journal = {Plant Communications}, number = {11}, publisher = {Elsevier}, title = {{Quantitative imaging reveals the role of MpARF proteasomal degradation during gemma germination}}, doi = {10.1016/j.xplc.2024.101039}, volume = {5}, year = {2024}, } @article{17442, abstract = {Although eukaryotic Argonautes have a pivotal role in post-transcriptional gene regulation through nucleic acid cleavage, some short prokaryotic Argonaute variants (pAgos) rely on auxiliary nuclease factors for efficient foreign DNA degradation1. Here we reveal the activation pathway of the DNA defence module DdmDE system, which rapidly eliminates small, multicopy plasmids from the Vibrio cholerae seventh pandemic strain (7PET)2. Through a combination of cryo-electron microscopy, biochemistry and in vivo plasmid clearance assays, we demonstrate that DdmE is a catalytically inactive, DNA-guided, DNA-targeting pAgo with a distinctive insertion domain. We observe that the helicase-nuclease DdmD transitions from an autoinhibited, dimeric complex to a monomeric state upon loading of single-stranded DNA targets. Furthermore, the complete structure of the DdmDE–guide–target handover complex provides a comprehensive view into how DNA recognition triggers processive plasmid destruction. Our work establishes a mechanistic foundation for how pAgos utilize ancillary factors to achieve plasmid clearance, and provides insights into anti-plasmid immunity in bacteria. }, author = {Bravo, Jack Peter Kelly and Ramos, Delisa A. and Fregoso Ocampo, Rodrigo and Ingram, Caiden and Taylor, David W.}, issn = {1476-4687}, journal = {Nature}, number = {8018}, pages = {961--967}, publisher = {Springer Nature}, title = {{Plasmid targeting and destruction by the DdmDE bacterial defence system}}, doi = {10.1038/s41586-024-07515-9}, volume = {630}, year = {2024}, } @article{17449, abstract = {We prove that the $k$-th positive integer moment of partial sums of Steinhaus random multiplicative functions over the interval $(x, x+H]$ matches the corresponding Gaussian moment, as long as $H\ll x/(\log x)^{2k^2+2+o(1)}$ and $H$ tends to infinity with $x$. We show that properly normalized partial sums of typical multiplicative functions arising from realizations of random multiplicative functions have Gaussian limiting distribution in short moving intervals $(x, x+H]$ with $H\ll X/(\log X)^{W(X)}$ tending to infinity with $X$, where $x$ is uniformly chosen from $\{1,2,\dots, X\}$, and $W(X)$ tends to infinity with $X$ arbitrarily slowly. This makes some initial progress on a recent question of Harper.}, author = {Pandey, Mayank and Wang, Victor and Xu, Max Wenqiang}, issn = {1944-7833}, journal = {Algebra & Number Theory}, number = {2}, pages = {389--408}, publisher = {Mathematical Sciences Publishers}, title = {{Partial sums of typical multiplicative functions over short moving intervals}}, doi = {10.2140/ant.2024.18.389}, volume = {18}, year = {2024}, } @inproceedings{17456, abstract = {Data-parallel distributed training of deep neural networks (DNN) has gained very widespread adoption, but can still experience communication bottlenecks. To address this issue, entire families of compression mechanisms have been developed, including quantization, sparsification, and low-rank approximation, some of which are seeing significant practical adoption. Despite this progress, almost all known compression schemes apply compression uniformly across DNN layers, although layers are heterogeneous in terms of parameter count and their impact on model accuracy.In this work, we provide a general framework for adapting the degree of compression across the model's layers dynamically during training, improving the overall compression, while leading to substantial speedups, without sacrificing accuracy. Our framework, called L-GreCo, is based on an adaptive algorithm, which automatically picks the optimal compression parameters for model layers guaranteeing the best compression ratio while satisfying an error constraint. Extensive experiments over image classification and language modeling tasks shows that L-GreCo is effective across all existing families of compression methods, and achieves up to 2.5 × training speedup and up to 5 × compression improvement over efficient implementations of existing approaches, while recovering full accuracy. Moreover, L-GreCo is complementary to existing adaptive algorithms, improving their compression ratio by 50\% and practical throughput by 66\%. An anonymized implementation is available at https://github.com/LGrCo/L-GreCo.}, author = {Markov, Ilia and Alimohammadi, Kaveh and Frantar, Elias and Alistarh, Dan-Adrian}, booktitle = {Proceedings of Machine Learning and Systems }, editor = {Gibbons, P. and Pekhimenko, G. and De Sa, C.}, location = {Athens, Greece}, publisher = {Association for Computing Machinery}, title = {{L-GreCo: Layerwise-adaptive gradient compression for efficient data-parallel deep learning}}, volume = {6}, year = {2024}, } @article{17461, abstract = {Socially living animals can counteract disease through cooperative defences, leading to social immunity that collectively exceeds the sum of individual defences. In superorganismal colonies of social insects with permanent caste separation between reproductive queen(s) and nonreproducing workers, workers are obligate altruists and thus engage in unconditional social immunity, including highly specialised and self-sacrificial hygiene behaviours. Contrastingly, cooperation is facultative in cooperatively breeding families, where all members are reproductively totipotent but offspring transiently forgo reproduction to help their parents rear more siblings. Here, helpers should either express condition-dependent social immunity or disperse to pursue independent reproduction. We advocate inclusive fitness theory as a framework to predict when and how indirect fitness gains may outweigh direct fitness costs, thus favouring conditional social immunity.}, author = {Cremer, Sylvia and Pull, Christopher}, issn = {1471-5007}, journal = {Trends in Parasitology}, number = {9}, pages = {780--787}, publisher = {Elsevier}, title = {{Unconditional versus condition-dependent social immunity}}, doi = {10.1016/j.pt.2024.07.014}, volume = {40}, year = {2024}, } @article{17462, abstract = {We are interested in numerical algorithms for computing the electrical field generated by a charge distribution localized on scale l in an infinite heterogeneous correlated random medium, in a situation where the medium is only known in a box of diameter L >>l around the support of the charge. We show that the algorithm in [J. Lu, F. Otto, and L. Wang, Optimal Artificial Boundary Conditions Based on Second-Order Correctors for Three Dimensional Random Ellilptic Media, preprint, arXiv:2109.01616, 2021], suggesting optimal Dirichlet boundary conditions motivated by the multipole expansion [P. Bella, A. Giunti, and F. Otto, Comm. Partial Differential Equations, 45 (2020), pp. 561–640], still performs well in correlated media. With overwhelming probability, we obtain a convergence rate in terms of l, L, and the size of the correlations for which optimality is supported with numerical simulations. These estimates are provided for ensembles which satisfy a multiscale logarithmic Sobolev inequality, where our main tool is an extension of the semigroup estimates in [N. Clozeau, Stoch. Partial Differ. Equ. Anal. Comput., 11 (2023), pp. 1254–1378]. As part of our strategy, we construct sublinear second-order correctors in this correlated setting, which is of independent interest.}, author = {Clozeau, Nicolas and Wang, Lihan}, issn = {1540-3467}, journal = {Multiscale Modeling and Simulation}, number = {3}, pages = {973--1029}, publisher = {Society for Industrial and Applied Mathematics}, title = {{Artificial boundary conditions for random elliptic systems with correlated coefficient field}}, doi = {10.1137/23M1603819}, volume = {22}, year = {2024}, } @article{17463, abstract = {Allosteric modulation of protein function, wherein the binding of an effector to a protein triggers conformational changes at distant functional sites, plays a central part in the control of metabolism and cell signalling1,2,3. There has been considerable interest in designing allosteric systems, both to gain insight into the mechanisms underlying such ‘action at a distance’ modulation and to create synthetic proteins whose functions can be regulated by effectors4,5,6,7. However, emulating the subtle conformational changes distributed across many residues, characteristic of natural allosteric proteins, is a significant challenge8,9. Here, inspired by the classic Monod–Wyman–Changeux model of cooperativity10, we investigate the de novo design of allostery through rigid-body coupling of peptide-switchable hinge modules11 to protein interfaces12 that direct the formation of alternative oligomeric states. We find that this approach can be used to generate a wide variety of allosterically switchable systems, including cyclic rings that incorporate or eject subunits in response to peptide binding and dihedral cages that undergo effector-induced disassembly. Size-exclusion chromatography, mass photometry13 and electron microscopy reveal that these designed allosteric protein assemblies closely resemble the design models in both the presence and absence of peptide effectors and can have ligand-binding cooperativity comparable to classic natural systems such as haemoglobin14. Our results indicate that allostery can arise from global coupling of the energetics of protein substructures without optimized side-chain–side-chain allosteric communication pathways and provide a roadmap for generating allosterically triggerable delivery systems, protein nanomachines and cellular feedback control circuitry.}, author = {Pillai, Arvind and Idris, Abbas and Philomin, Annika and Weidle, Connor and Skotheim, Rebecca and Leung, Philip J.Y. and Broerman, Adam and Demakis, Cullen and Borst, Andrew J. and Praetorius, Florian M and Baker, David}, issn = {1476-4687}, journal = {Nature}, pages = {911–920 }, publisher = {Springer Nature}, title = {{De novo design of allosterically switchable protein assemblies}}, doi = {10.1038/s41586-024-07813-2}, volume = {632}, year = {2024}, } @misc{17471, abstract = {Mechanisms for suppressing thermalization in disorder-free many-body systems, such as Hilbert space fragmentation and quantum many-body scars, have recently attracted much interest in foundations of quantum statistical physics and potential quantum information processing applications. However, their sensitivity to realistic effects such as finite temperature remains largely unexplored. Here, we have utilized IBM's Kolkata quantum processor to demonstrate an unexpected robustness of quantum many-body scars at finite temperatures when the system is prepared in a thermal Gibbs ensemble. We identify such robustness in the PXP model, which describes quantum many-body scars in experimental systems of Rydberg atom arrays and ultracold atoms in tilted Bose--Hubbard optical lattices. By contrast, other theoretical models which host exact quantum many-body scars are found to lack such robustness, and their scarring properties quickly decay with temperature. Our study sheds light on the important differences between scarred models in terms of their algebraic structures, which impacts their resilience to finite temperature.}, author = {Desaules, Jean-Yves Marc}, keywords = {quantum many-body scars, non-equilibrium physics, non-Hermitian physics}, publisher = {Institute of Science and Technology Austria}, title = {{Data for "Enhanced many-body quantum scars from the non-Hermitian Fock skin effect"}}, doi = {10.15479/AT:ISTA:17471}, year = {2024}, } @article{17474, abstract = {Entropic risk (ERisk) is an established risk measure in finance, quantifying risk by an exponential re-weighting of rewards. We study ERisk for the first time in the context of turn-based stochastic games with the total reward objective. This gives rise to an objective function that demands the control of systems in a risk-averse manner. We show that the resulting games are determined and, in particular, admit optimal memoryless deterministic strategies. This contrasts risk measures that previously have been considered in the special case of Markov decision processes and that require randomization and/or memory. We provide several results on the decidability and the computational complexity of the threshold problem, i.e. whether the optimal value of ERisk exceeds a given threshold. Furthermore, an approximation algorithm for the optimal value of ERisk is provided.}, author = {Baier, Christel and Chatterjee, Krishnendu and Meggendorfer, Tobias and Piribauer, Jakob}, issn = {1090-2651}, journal = {Information and Computation}, publisher = {Elsevier}, title = {{Entropic risk for turn-based stochastic games}}, doi = {10.1016/j.ic.2024.105214}, volume = {301}, year = {2024}, } @article{17475, abstract = {As a discrete analogue of Kac’s celebrated question on ‘hearing the shape of a drum’ and towards a practical graph isomorphism test, it is of interest to understand which graphs are determined up to isomorphism by their spectrum (of their adjacency matrix). A striking conjecture in this area, due to van Dam and Haemers, is that ‘almost all graphs are determined by their spectrum’, meaning that the fraction of unlabelled n-vertex graphs which are determined by their spectrum converges to 1 as n → ∞. In this paper, we make a step towards this conjecture, showing that there are exponentially many n-vertex graphs which are determined by their spectrum. This improves on previous bounds (of shape e c √ n ). We also propose a number of further directions of research. }, author = {Koval, Illya and Kwan, Matthew Alan}, issn = {1464-3847}, journal = {Quarterly Journal of Mathematics}, number = {3}, pages = {869--899}, publisher = {Oxford University Press}, title = {{Exponentially many graphs are determined by their spectrum}}, doi = {10.1093/qmath/haae030}, volume = {75}, year = {2024}, } @article{17477, abstract = {Trapped-ion systems are a leading platform for quantum information processing, but they are currently limited to 1D and 2D arrays, which imposes restrictions on both their scalability and their range of applications. Here, we propose a path to overcome this limitation by demonstrating that Penning traps can be used to realize remarkably clean bilayer crystals, wherein hundreds of ions self-organize into two well-defined layers. These bilayer crystals are made possible by the inclusion of an anharmonic trapping potential, which is readily implementable with current technology. We study the normal modes of this system and discover salient differences compared to the modes of single-plane crystals. The bilayer geometry and the unique properties of the normal modes open new opportunities—in particular, in quantum sensing and quantum simulation—that are not straightforward in single-plane crystals. Furthermore, we illustrate that it may be possible to extend the ideas presented here to realize multilayer crystals with more than two layers. Our work increases the dimensionality of trapped-ion systems by efficiently utilizing all three spatial dimensions, and it lays the foundation for a new generation of quantum information processing experiments with multilayer 3D crystals of trapped ions.}, author = {Hawaldar, Samarth and Shahi, Prakriti and Carter, Allison L. and Rey, Ana Maria and Bollinger, John J. and Shankar, Athreya}, issn = {2160-3308}, journal = {Physical Review X}, number = {3}, publisher = {American Physical Society}, title = {{Bilayer crystals of trapped ions for quantum information processing}}, doi = {10.1103/PhysRevX.14.031030}, volume = {14}, year = {2024}, } @article{17479, abstract = {Phonon polaritons (PhPs), light coupled to lattice vibrations, in the highly anisotropic polar layered material molybdenum trioxide (α-MoO3) are currently the focus of intense research efforts due to their extreme subwavelength field confinement, directional propagation, and unprecedented low losses. Nevertheless, prior research has primarily concentrated on exploiting the squeezing and steering capabilities of α-MoO3 PhPs, without inquiring much into the dominant microscopic mechanism that determines their long lifetimes, which is key for their implementation in nanophotonic applications. This study delves into the fundamental processes that govern PhP damping in α-MoO3 by combining ab initio calculations with scattering-type scanning near-field optical microscopy (s-SNOM) and Fourier transform infrared (FTIR) spectroscopy measurements across a broad temperature range (8–300 K). The remarkable agreement between our theoretical predictions and experimental observations allows us to identify third-order anharmonic phonon–phonon scattering as the main damping mechanism of α-MoO3 PhPs. These findings shed light on the fundamental limits of low-loss PhPs, which is a crucial factor for assessing their implementation into nanophotonic devices.}, author = {Taboada-Gutiérrez, Javier and Zhou, Yixi and Tresguerres-Mata, Ana I.F. and Lanza, Christian and Martínez-Suárez, Abel and Álvarez-Pérez, Gonzalo and Duan, Jiahua and Martín, José Ignacio and Vélez, María and Prieto Gonzalez, Ivan and Bercher, Adrien and Teyssier, Jérémie and Errea, Ion and Nikitin, Alexey Y. and Martín-Sánchez, Javier and Kuzmenko, Alexey B. and Alonso-González, Pablo}, issn = {2330-4022}, journal = {ACS Photonics}, number = {9}, pages = {3570--3577}, publisher = {American Chemical Society}, title = {{Unveiling the mechanism of phonon-polariton damping in α‑MoO3}}, doi = {10.1021/acsphotonics.4c00485}, volume = {11}, year = {2024}, } @article{17480, abstract = {One of the most promising approaches towards large-scale quantum computation uses devices based on many Josephson junctions. Yet, even today, open questions regarding the single junction remain unsolved, such as the detailed understanding of the quantum phase transitions, the coupling of the Josephson junction to the environment or how to improve the coherence of a superconducting qubit. Here we design and build an engineered on-chip reservoir connected to a Josephson junction that acts as an efficient bolometer for detecting the Josephson radiation under non-equilibrium, that is, biased conditions. The bolometer converts the a.c. Josephson current at microwave frequencies up to about 100 GHz into a temperature rise measured by d.c. thermometry. A circuit model based on realistic parameter values captures both the current–voltage characteristics and the measured power quantitatively. The present experiment demonstrates an efficient, wide-band, thermal detection scheme of microwave photons and provides a sensitive detector of Josephson dynamics beyond the standard conductance measurements.}, author = {Karimi, Bayan and Steffensen, Gorm Ole and Higginbotham, Andrew P and Marcus, Charles M. and Levy Yeyati, Alfredo and Pekola, Jukka P.}, issn = {1748-3395}, journal = {Nature Nanotechnology}, pages = {1613--1618}, publisher = {Springer Nature}, title = {{Bolometric detection of Josephson radiation}}, doi = {10.1038/s41565-024-01770-7}, volume = {19}, year = {2024}, } @misc{17488, abstract = {Behavioural data for Pokusaeva, Satapathy et al. Relevant information can be found in the 'README.txt' file.}, author = {Satapathy, Roshan K and Jösch, Maximilian A and Symonova, Olga and Pokusaeva, Victoria}, keywords = {drosophila, behaviour, locomotion, gap junctions}, publisher = {Institute of Science and Technology Austria}, title = {{Bilateral interactions of optic-flow sensitive neurons coordinate course control in flies}}, doi = {10.15479/AT:ISTA:17488}, year = {2024}, } @phdthesis{17490, abstract = {Deep learning is essential in numerous applications nowadays, with many recent advancements made possible by training very large models. Despite their broad applicability, training neural networks is often time-intensive, and it is usually impractical to manage large models and datasets on a single machine. To address these issues, distributed deep learning training has become increasingly important. However, distributed training requires synchronization among nodes, and the mini-batch stochastic gradient descent algorithm places a significant load on network connections. A possible solution to tackle the synchronization bottleneck is to reduce a message size by lossy compression. In this thesis, we investigate systems and algorithmic approaches to communication compression during training. From the systems perspective, we demonstrate that a common approach of expensive hardware overprovisioning can be replaced through a thorough system design. We introduce a framework that introduces efficient software support for compressed communication in machine learning applications, applicable to both multi-GPU single-node training and larger-scale multi-node training. Our framework integrates with popular ML frameworks, providing up to 3x speedups for multi-GPU nodes based on commodity hardware and order-of-magnitude improvements in the multi-node setting, with negligible impact on accuracy. Also, we consider an application of our framework to different communication schemes, such as Fully Sharded Data Parallel. We provide strong convergence guarantees for the compression in such a setup. Empirical validation shows that our method preserves model accuracy for GPT-family models with up to 1.3 billion parameters, while completely removing the communication bottlenecks of non-compressed alternatives, providing up to 2.2x speedups end-to-end. From the algorithmic side, we propose a general framework that dynamically adjusts the degree of compression across a model's layers during training. This approach enhances overall compression and results in significant speedups without compromising accuracy. Our algorithm utilizes an adaptive algorithm that automatically selects the optimal compression parameters for model layers, ensuring the best compression ratio while adhering to an error constraint. Our method is effective across all existing families of compression methods. It achieves up to 2.5x faster training and up to a 5x improvement in compression compared to efficient implementations of current approaches. Additionally, LGreCo can complement existing adaptive algorithms. }, author = {Markov, Ilia}, issn = {2663-337X}, pages = {102}, publisher = {Institute of Science and Technology Austria}, title = {{Communication-efficient distributed training of deep neural networks : An algorithms and systems perspective}}, doi = {10.15479/at:ista:17490}, year = {2024}, } @article{17493, abstract = {Estimating global properties of many-body quantum systems such as entropy or bipartite entanglement is a notoriously difficult task, typically requiring a number of measurements or classical postprocessing resources growing exponentially in the system size. In this work, we address the problem of estimating global entropies and mixed-state entanglement via partial-transposed (PT) moments and show that efficient estimation strategies exist under the assumption that all the spatial correlation lengths are finite. Focusing on one-dimensional systems, we identify a set of approximate factorization conditions (AFCs) on the system density matrix, which allow us to reconstruct entropies and PT moments from information on local subsystems. This identification yields a simple and efficient strategy for entropy and entanglement estimation. Our method could be implemented in different ways, depending on how information on local subsystems is extracted. Focusing on randomized measurements providing a practical and common measurement scheme, we prove that our protocol requires only polynomially many measurements and postprocessing operations, assuming that the state to be measured satisfies the AFCs. We prove that the AFCs hold for finite-depth quantum-circuit states and translation-invariant matrix-product density operators and provide numerical evidence that they are satisfied in more general, physically interesting cases, including thermal states of local Hamiltonians. We argue that our method could be practically useful to detect bipartite mixed-state entanglement for large numbers of qubits available in today’s quantum platforms.}, author = {Vermersch, Benoît and Ljubotina, Marko and Cirac, J. Ignacio and Zoller, Peter and Serbyn, Maksym and Piroli, Lorenzo}, issn = {2160-3308}, journal = {Physical Review X}, number = {3}, publisher = {American Physical Society}, title = {{Many-body entropies and entanglement from polynomially many local measurements}}, doi = {10.1103/physrevx.14.031035}, volume = {14}, year = {2024}, } @article{17494, author = {Bravo, Jack Peter Kelly}, issn = {1746-0921}, journal = {Future Microbiology}, number = {15}, pages = {1269--1272}, publisher = {Taylor & Francis}, title = {{Anti-plasmid immunity: A key to pathogen success?}}, doi = {10.1080/17460913.2024.2389720}, volume = {19}, year = {2024}, } @article{17495, abstract = {Rust is a modern systems programming language whose ownership-based type system statically guarantees memory safety, making it particularly well-suited to the domain of safety-critical systems. In recent years, a wellspring of automated deductive verification tools have emerged for establishing functional correctness of Rust code. However, none of the previous tools produce foundational proofs (machine-checkable in a general-purpose proof assistant), and all of them are restricted to the safe fragment of Rust. This is a problem because the vast majority of Rust programs make use of unsafe code at critical points, such as in the implementation of widely-used APIs. We propose RefinedRust, a refinement type system—proven sound in the Coq proof assistant—with the goal of establishing foundational semi-automated functional correctness verification of both safe and unsafe Rust code. We have developed a prototype verification tool implementing RefinedRust. Our tool translates Rust code (with user annotations) into a model of Rust embedded in Coq, and then checks its adherence to the RefinedRust type system using separation logic automation in Coq. All proofs generated by RefinedRust are checked by the Coq proof assistant, so the automation and type system do not have to be trusted. We evaluate the effectiveness of RefinedRust by verifying a variant of Rust’s Vec implementation that involves intricate reasoning about unsafe pointer-manipulating code.}, author = {Gäher, Lennard and Sammler, Michael Joachim and Jung, Ralf and Krebbers, Robbert and Dreyer, Derek}, issn = {2475-1421}, journal = {Proceedings of the ACM on Programming Languages}, number = {PLDI}, pages = {1115--1139}, publisher = {Association for Computing Machinery}, title = {{RefinedRust: A type system for high-assurance verification of rust programs}}, doi = {10.1145/3656422}, volume = {8}, year = {2024}, } @article{17497, abstract = {Over the past two decades, there has been a great deal of progress on verification of full functional correctness of programs using separation logic, sometimes even producing “foundational” proofs in proof assistants like Coq. Unfortunately, even though existing approaches to this problem provide significant support for automated verification, they still incur a significant specification overhead: the user must supply the specification against which the program is verified, and the specification may be long, complex, or tedious to formulate. In this paper, we introduce Quiver, the first technique for inferring functional correctness specifications in separation logic while simultaneously verifying foundationally that they are correct. To guide Quiver towards the final specification, we take hints from the user in the form of a specification sketch, and then complete the sketch using inference. To do so, Quiver introduces a new abductive deductive verification technique, which integrates ideas from abductive inference (for specification inference) together with deductive separation logic automation (for foundational verification). The result is that users have to provide some guidance, but significantly less than with traditional deductive verification techniques based on separation logic. We have evaluated Quiver on a range of case studies, including code from popular open-source libraries.}, author = {Spies, Simon and Gäher, Lennard and Sammler, Michael Joachim and Dreyer, Derek}, issn = {2475-1421}, journal = {Proceedings of the ACM on Programming Languages}, number = {PLDI}, pages = {889--913}, publisher = {Association for Computing Machinery}, title = {{Quiver: Guided abductive inference of separation logic specifications in coq}}, doi = {10.1145/3656413}, volume = {8}, year = {2024}, }