@article{17068,
  abstract     = {In plants, the antagonism between growth and defense is hardwired by hormonal signaling. The perception of pathogen-associated molecular patterns (PAMPs) from invading microorganisms inhibits auxin signaling and plant growth. Conversely, pathogens manipulate auxin signaling to promote disease, but how this hormone inhibits immunity is not fully understood. Ustilago maydis is a maize pathogen that induces auxin signaling in its host. We characterized a U. maydis effector protein, Naked1 (Nkd1), that is translocated into the host nucleus. Through its native ethylene-responsive element binding factor-associated amphiphilic repression (EAR) motif, Nkd1 binds to the transcriptional co-repressors TOPLESS/TOPLESS-related (TPL/TPRs) and prevents the recruitment of a transcriptional repressor involved in hormonal signaling, leading to the de-repression of auxin and jasmonate signaling and thereby promoting susceptibility to (hemi)biotrophic pathogens. A moderate upregulation of auxin signaling inhibits the PAMP-triggered reactive oxygen species (ROS) burst, an early defense response. Thus, our findings establish a clear mechanism for auxin-induced pathogen susceptibility. Engineered Nkd1 variants with increased expression or increased EAR-mediated TPL/TPR binding trigger typical salicylic-acid-mediated defense reactions, leading to pathogen resistance. This implies that moderate binding of Nkd1 to TPL is a result of a balancing evolutionary selection process to enable TPL manipulation while avoiding host recognition.},
  author       = {Navarrete, Fernando and Gallei, Michelle C and Kornienko, Aleksandra E. and Saado, Indira and Khan, Mamoona and Chia, Khong-Sam and Darino, Martin A. and Bindics, Janos and Djamei, Armin},
  issn         = {2590-3462},
  journal      = {Plant Communications},
  number       = {2},
  publisher    = {Elsevier},
  title        = {{TOPLESS promotes plant immunity by repressing auxin signaling and is targeted by the fungal effector Naked1}},
  doi          = {10.1016/j.xplc.2021.100269},
  volume       = {3},
  year         = {2022},
}

@article{17069,
  abstract     = {Fertilization of an egg by multiple sperm (polyspermy) leads to lethal genome imbalance and chromosome segregation defects. In Arabidopsis thaliana, the block to polyspermy is facilitated by a mechanism that prevents polytubey (the arrival of multiple pollen tubes to one ovule). We show here that FERONIA, ANJEA, and HERCULES RECEPTOR KINASE 1 receptor-like kinases located at the septum interact with pollen tube–specific RALF6, 7, 16, 36, and 37 peptide ligands to establish this polytubey block. The same combination of RALF (rapid alkalinization factor) peptides and receptor complexes controls pollen tube reception and rupture inside the targeted ovule. Pollen tube rupture releases the polytubey block at the septum, which allows the emergence of secondary pollen tubes upon fertilization failure. Thus, orchestrated steps in the fertilization process in Arabidopsis are coordinated by the same signaling components to guarantee and optimize reproductive success.},
  author       = {Zhong, Sheng and Li, Ling and Wang, Zhijuan and Ge, Zengxiang and Li, Qiyun and Bleckmann, Andrea and Wang, Jizong and Song, Zihan and Shi, Yihao and Liu, Tianxu and Li, Luhan and Zhou, Huabin and Wang, Yanyan and Zhang, Li and Wu, Hen-Ming and Lai, Luhua and Gu, Hongya and Dong, Juan and Cheung, Alice Y. and Dresselhaus, Thomas and Qu, Li-Jia},
  issn         = {1095-9203},
  journal      = {Science},
  number       = {6578},
  pages        = {290--296},
  publisher    = {American Association for the Advancement of Science},
  title        = {{RALF peptide signaling controls the polytubey block in Arabidopsis}},
  doi          = {10.1126/science.abl4683},
  volume       = {375},
  year         = {2022},
}

@article{17070,
  abstract     = {We investigate the formation of magnetic Bose polaron, an impurity atom dressed by spin-wave excitations, in a one-dimensional spinor Bose gas. Within an effective potential model, the impurity is strongly confined by the host excitations which can even overcome the impurity-medium repulsion leading to a self-localized quasi-particle state. The phase diagram of the attractive and self-bound repulsive magnetic polaron, repulsive non-magnetic (Fröhlich-type) polaron and impurity-medium phase-separation regimes is explored with respect to the Rabi-coupling between the spin components, spin–spin interactions and impurity-medium coupling. The residue of such magnetic polarons decreases substantially in both strong attractive and repulsive branches with strong impurity-spin interactions, illustrating significant dressing of the impurity. The impurity can be used to probe and maneuver the spin polarization of the magnetic medium while suppressing ferromagnetic spin–spin correlations. It is shown that mean-field theory fails as the spinor gas approaches immiscibility since the generated spin-wave excitations are prominent. Our findings illustrate that impurities can be utilized to generate controllable spin–spin correlations and magnetic polaron states which can be realized with current cold atom setups.},
  author       = {Mistakidis, S I and Koutentakis, Georgios and Grusdt, F and Schmelcher, P and Sadeghpour, H R},
  issn         = {1367-2630},
  journal      = {New Journal of Physics},
  number       = {8},
  publisher    = {IOP Publishing},
  title        = {{Inducing spin-order with an impurity: phase diagram of the magnetic Bose polaron}},
  doi          = {10.1088/1367-2630/ac836c},
  volume       = {24},
  year         = {2022},
}

@article{17071,
  abstract     = {The eukaryotic nucleus pro­tects the genome and is enclosed by the two membranes of the nuclear envelope. Nuclear pore complexes (NPCs) perforate the nuclear envelope to facilitate nucleocytoplasmic transport. With a molecular weight of ∼120 MDa, the human NPC is one of the larg­est protein complexes. Its ~1000 proteins are taken in multiple copies from a set of about 30 distinct nucleoporins (NUPs). They can be roughly categorized into two classes. Scaf­fold NUPs contain folded domains and form a cylindrical scaffold architecture around a central channel. Intrinsically disordered NUPs line the scaffold and extend into the central channel, where they interact with cargo complexes. The NPC architecture is highly dynamic. It responds to changes in nuclear envelope tension with conforma­tional breathing that manifests in dilation and constriction movements. Elucidating the scaffold architecture, ultimately at atomic resolution, will be important for gaining a more precise understanding of NPC function and dynamics but imposes a substantial chal­lenge for structural biologists.
Considerable progress has been made toward this goal by a joint effort in the field. A synergistic combination of complementary approaches has turned out to be critical. In situ structural biology techniques were used to reveal the overall layout of the NPC scaffold that defines the spatial reference for molecular modeling. High-resolution structures of many NUPs were determined in vitro. Proteomic analysis and extensive biochemical work unraveled the interaction network of NUPs. Integra­tive modeling has been used to combine the different types of data, resulting in a rough outline of the NPC scaffold. Previous struc­tural models of the human NPC, however, were patchy and limited in accuracy owing to several challenges: (i) Many of the high-resolution structures of individual NUPs have been solved from distantly related species and, consequently, do not comprehensively cover their human counterparts. (ii) The scaf­fold is interconnected by a set of intrinsically disordered linker NUPs that are not straight­forwardly accessible to common structural biology techniques. (iii) The NPC scaffold intimately embraces the fused inner and outer nuclear membranes in a distinctive topol­ogy and cannot be studied in isolation. (iv) The conformational dynamics of scaffold NUPs limits the resolution achievable in structure determination.
In this study, we used artificial intelligence (AI)–based prediction to generate an exten­sive repertoire of structural models of human NUPs and their subcomplexes. The resulting models cover various domains and interfaces that so far remained structurally uncharac­terized. Benchmarking against previous and unpublished x-ray and cryo–electron micros­copy structures revealed unprecedented accu­racy. We obtained well-resolved cryo–electron tomographic maps of both the constricted and dilated conformational states of the hu­man NPC. Using integrative modeling, we fit­ted the structural models of individual NUPs into the cryo–electron microscopy maps. We explicitly included several linker NUPs and traced their trajectory through the NPC scaf­fold. We elucidated in great detail how mem­brane-associated and transmembrane NUPs are distributed across the fusion topology of both nuclear membranes. The resulting architectural model increases the structural coverage of the human NPC scaffold by about twofold. We extensively validated our model against both earlier and new experimental data. The completeness of our model has enabled microsecond-long coarse-grained molecular dynamics simulations of the NPC scaffold within an explicit membrane en­vironment and solvent. These simulations reveal that the NPC scaffold prevents the constriction of the otherwise stable double-membrane fusion pore to small diameters in the absence of membrane tension
Our 70-MDa atomically re­solved model covers >90% of the human NPC scaffold. It captures conforma­tional changes that occur during dilation and constriction. It also reveals the precise anchoring sites for intrinsically disordered NUPs, the identification of which is a prerequisite for a complete and dy­namic model of the NPC. Our study exempli­fies how AI-based structure prediction may accelerate the elucidation of subcellular ar­chitecture at atomic resolution.},
  author       = {Mosalaganti, Shyamal and Obarska-Kosinska, Agnieszka and Siggel, Marc and Taniguchi, Reiya and Turoňová, Beata and Zimmerli, Christian E. and Buczak, Katarzyna and Schmidt, Florian and Margiotta, Erica and Mackmull, Marie-Therese and Hagen, Wim J. H. and Hummer, Gerhard and Kosinski, Jan and Beck, Martin},
  issn         = {1095-9203},
  journal      = {Science},
  number       = {6598},
  publisher    = {American Association for the Advancement of Science},
  title        = {{AI-based structure prediction empowers integrative structural analysis of human nuclear pores}},
  doi          = {10.1126/science.abm9506},
  volume       = {376},
  year         = {2022},
}

@article{17072,
  abstract     = {The collapse of polypeptides is thought important to protein folding, aggregation, intrinsic disorder, and phase separation. However, whether polypeptide collapse is modulated in cells to control protein states is unclear. Here, using integrated protein manipulation and imaging, we show that the chaperonin GroEL-ES can accelerate the folding of proteins by strengthening their collapse. GroEL induces contractile forces in substrate chains, which draws them into the cavity and triggers a general compaction and discrete folding transitions, even for slow-folding proteins. This collapse enhancement is strongest in the nucleotide-bound states of GroEL and is aided by GroES binding to the cavity rim and by the amphiphilic C-terminal tails at the cavity bottom. Collapse modulation is distinct from other proposed GroEL-ES folding acceleration mechanisms, including steric confinement and misfold unfolding. Given the prevalence of collapse throughout the proteome, we conjecture that collapse modulation is more generally relevant within the protein quality control machinery.},
  author       = {Naqvi, Mohsin M. and Avellaneda Sarrió, Mario and Roth, Andrew and Koers, Eline J. and Roland, Antoine and Sunderlikova, Vanda and Kramer, Günter and Rye, Hays S. and Tans, Sander J.},
  issn         = {2375-2548},
  journal      = {Science Advances},
  number       = {9},
  publisher    = {American Association for the Advancement of Science},
  title        = {{Protein chain collapse modulation and folding stimulation by GroEL-ES}},
  doi          = {10.1126/sciadv.abl6293},
  volume       = {8},
  year         = {2022},
}

@inbook{17075,
  abstract     = {Disorders associated with the malfunction of amino acid transporters mainly affect the function of the intestine, kidney, brain, and liver. Mutations of brain amino acid transporters, for example, alter neuronal excitability (e.g., episodic ataxia due to SLC1A3 (EAAT1) defect and hyperekplexia due to SLC6A5 (GLYT2) deficiency) or brain development (SLC1A1 (EAAT3), SLC3A2/SLC7A5 (CD98hc/LAT1), and SLC1A4 (ASCT1) deficiencies). Mutations of renal and intestinal amino acid transporters SLC3A1/SLC7A9 (rBAT/b0,+AT) and SLC1A1 (EAAT3) cause renal problems (cystinuria and dicarboxylic aminoaciduria, respectively) and malabsorption that can affect whole-body homoeostasis (Hartnup disorder SLC6A19 (B0AT1), lysinuric protein intolerance SLC3A2/SLC7A7 (CD98hc/y+LAT1), and hyperdibasic aminoaciduria type 1). Mutations in the neuronal system A amino acid transporter SLC38A8 (SNAT8) cause eye developmental and visual defects. Inborn errors associated with mitochondrial SLC25 family members such as SLC25A12 (neuronal- and muscle-specific mitochondrial aspartate/glutamate transporter 1; AGC1) (global cerebral hypomyelination), SLC25A13 (aspartate/glutamate transporter 2) (citrin deficiency), SLC25A15 (ornithine-citrulline carrier 2) (homocitrullinuria, hyperornithinemia, and hyperammonemia syndrome), and SLC25A22 (mitochondrial glutamate/H+ symporter 1, GC1) (neonatal myoclonic epilepsy) will be dealt within Chap. 43 (defects of mitochondrial carriers).},
  author       = {Palacín, Manuel and Bröer, Stefan and Novarino, Gaia},
  booktitle    = {Physician's Guide to the Diagnosis, Treatment, and Follow-Up of Inherited Metabolic Diseases},
  editor       = {Blau, Nenad and Vici, Carlo Dionisi and Ferreira, Carlos R.  and Vianey-Saban, Christine and van Karnebeek, Clara D.M.},
  isbn         = {9783030677268},
  pages        = {291--312},
  publisher    = {Springer Nature},
  title        = {{Amino Acid Transport Defects}},
  doi          = {10.1007/978-3-030-67727-5_18},
  year         = {2022},
}

@article{17076,
  abstract     = {Introduction: The levels of many blood proteins are associated with Alzheimer's disease (AD) or its pathological hallmarks. Elucidating the molecular factors that control circulating levels of these proteins may help to identify proteins associated with disease risk mechanisms.

Methods: Genome-wide and epigenome-wide studies (nindividuals ≤1064) were performed on plasma levels of 282 AD-associated proteins, identified by a structured literature review. Bayesian penalized regression estimated contributions of genetic and epigenetic variation toward inter-individual differences in plasma protein levels. Mendelian randomization (MR) and co-localization tested associations between proteins and disease-related phenotypes.

Results: Sixty-four independent genetic and 26 epigenetic loci were associated with 45 proteins. Novel findings included an association between plasma triggering receptor expressed on myeloid cells 2 (TREM2) levels and a polymorphism and cytosine-phosphate-guanine (CpG) site within the MS4A4A locus. Higher plasma tubulin-specific chaperone A (TBCA) and TREM2 levels were significantly associated with lower AD risk.

Discussion: Our data inform the regulation of biomarker levels and their relationships with AD.},
  author       = {Hillary, Robert F. and Gadd, Danni A. and McCartney, Daniel L. and Shi, Liu and Campbell, Archie and Walker, Rosie M. and Ritchie, Craig W. and Deary, Ian J. and Evans, Kathryn L. and Nevado‐Holgado, Alejo J. and Hayward, Caroline and Porteous, David J. and McIntosh, Andrew M. and Lovestone, Simon and Robinson, Matthew Richard and Marioni, Riccardo E.},
  issn         = {2352-8729},
  journal      = {Alzheimer's & Dementia: Diagnosis, Assessment & Disease Monitoring},
  number       = {1},
  publisher    = {Wiley},
  title        = {{Genome‐ and epigenome‐wide studies of plasma protein biomarkers for Alzheimer's disease implicate TBCA and TREM2 in disease risk}},
  doi          = {10.1002/dad2.12280},
  volume       = {14},
  year         = {2022},
}

@article{17077,
  abstract     = {Resolving a conjecture of Füredi from 1988, we prove that with high probability, the random graph 𝔾(𝑛, 1/2) admits a friendly bisection of its vertex set, i.e., a
partition of its vertex set into two parts whose sizes differ by at most one in which
𝑛 − 𝑜(𝑛) vertices have more neighbours in their own part as across. Our proof is constructive, and in the process, we develop a new method to study stochastic processes
driven by degree information in random graphs; this involves combining enumeration
techniques with an abstract second moment argument.},
  author       = {Ferber, Asaf and Kwan, Matthew Alan and Narayanan, Bhargav and Sah, Ashwin and Sawhney, Mehtaab},
  issn         = {2692-3688},
  journal      = {Communications of the American Mathematical Society},
  number       = {10},
  pages        = {380--416},
  publisher    = {American Mathematical Society},
  title        = {{Friendly bisections of random graphs}},
  doi          = {10.1090/cams/13},
  volume       = {2},
  year         = {2022},
}

@inproceedings{17084,
  abstract     = {Given a graph where every vertex has exactly one labeled token, how can we most quickly execute a given permutation on the tokens? In (sequential) token swapping, the goal is to use the shortest possible sequence of swaps, each of which exchanges the tokens at the two endpoints of an edge of the graph. In parallel token swapping, the goal is to use the fewest rounds, each of which consists of one or more swaps on the edges of a matching. We prove that both of these problems remain NP-hard when the graph is restricted to be a tree. These token swapping problems have been studied by disparate groups of researchers in discrete mathematics, theoretical computer science, robot motion planning, game theory, and engineering. Previous work establishes NP-completeness on general graphs (for both problems), constant-factor approximation algorithms, and some poly-time exact algorithms for simple graph classes such as cliques, stars, paths, and cycles. Sequential and parallel token swapping on trees were first studied over thirty years ago (as "sorting with a transposition tree") and over twenty-five years ago (as "routing permutations via matchings"), yet their complexities were previously unknown. We also show limitations on approximation of sequential token swapping on trees: we identify a broad class of algorithms that encompass all three known polynomial-time algorithms that achieve the best known approximation factor (which is 2) and show that no such algorithm can achieve an approximation factor less than 2.},
  author       = {Aichholzer, Oswin and Demaine, Erik D. and Korman, Matias and Lubiw, Anna and Lynch, Jayson and Masárová, Zuzana and Rudoy, Mikhail and Vassilevska Williams, Virginia and Wein, Nicole},
  booktitle    = {30th Annual European Symposium on Algorithms},
  location     = {Berlin/Potsdam, Germany},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Hardness of token swapping on trees}},
  doi          = {10.4230/LIPIcs.ESA.2022.3},
  volume       = {244},
  year         = {2022},
}

@inbook{17085,
  abstract     = {Mosses are a cosmopolitan group of land plants, sister to vascular plants, with a high potential for molecular and cell biological research. The species Physcomitrium patens has helped gaining better understanding of the biological processes of the plant cell, and it has become a central system to understand water-to-land plant transition through 2D-to-3D growth transition, regulation of asymmetric cell division, shoot apical cell establishment and maintenance, phyllotaxis and regeneration. P. patens was the first fully sequenced moss in 2008, with the latest annotated release in 2018. It has been shown that many gene functions and networks are conserved in mosses when compared to angiosperms. Importantly, this model organism has a simplified and accessible body structure that facilitates close tracking in time and space with the support of live cell imaging set-ups and multiple reporter lines. This has become possible thanks to its fully established molecular toolkit, with highly efficient PEG-assisted, CRISPR/Cas9 and RNAi transformation and silencing protocols, among others. Here we provide examples on how mosses exhibit advantages over vascular plants to study several processes and their future potential to answer some other outstanding questions in plant cell biology.},
  author       = {Floriach-Clark, Jordi and Tang, Han and Willemsen, Viola},
  booktitle    = {Model Organisms in Plant Genetics},
  editor       = {Abdurakhmonov, Ibrokhim Y.},
  isbn         = {9781839697500},
  publisher    = {IntechOpen},
  title        = {{Mosses: Accessible Systems for Plant Development Studies}},
  doi          = {10.5772/intechopen.100535},
  year         = {2022},
}

@inproceedings{17086,
  abstract     = {We consider a high-dimensional mean estimation problem over a binary hidden Markov model, which illuminates the interplay between memory in data, sample size, dimension, and signal strength in statistical inference. In this model, an estimator observes n samples of a d-dimensional parameter vector θ∗∈Rd, multiplied by a random sign Si (1≤i≤n), and corrupted by isotropic standard Gaussian noise. The sequence of signs {Si}i∈[n]∈{−1,1}n is drawn from a stationary homogeneous Markov chain with flip probability δ∈[0,1/2]. As δ varies, this model smoothly interpolates two well-studied models: the Gaussian Location Model for which δ=0 and the Gaussian Mixture Model for which δ=1/2. Assuming that the estimator knows δ, we establish a nearly minimax optimal (up to logarithmic factors) estimation error rate, as a function of ∥θ∗∥,δ,d,n. We then provide an upper bound to the case of estimating δ, assuming a (possibly inaccurate) knowledge of θ∗. The bound is proved to be tight when θ∗ is an accurately known constant. These results are then combined to an algorithm which estimates θ∗ with δ unknown a priori, and theoretical guarantees on its error are stated.},
  author       = {Zhang, Yihan and Weinberger, Nir},
  booktitle    = {36th Conference on Neural Information Processing Systems},
  isbn         = {9781713871088},
  location     = {New Orleans, LA, United States},
  publisher    = {ML Research Press},
  title        = {{Mean estimation in high-dimensional binary Markov Gaussian mixture models}},
  volume       = {35},
  year         = {2022},
}

@inproceedings{17088,
  abstract     = {In this paper, we consider the problem of sparsifying BERT models, which are a key building block for natural language processing, in order to reduce their storage and computational cost. We introduce the Optimal BERT Surgeon (oBERT), an efficient and accurate pruning method based on approximate second-order information, which we show to yield state-of-the-art results in both stages of language tasks: pre-training and fine-tuning. Specifically, oBERT extends existing work on second-order pruning by allowing for pruning weight blocks, and is the first such method that is applicable at BERT scale. Second, we investigate compounding compression approaches to obtain highly compressed but accurate models for deployment on edge devices. These models significantly push boundaries of the current state-of-the-art sparse BERT models with respect to all metrics: model size, inference speed and task accuracy. For example, relative to the dense BERT-base, we obtain 10x model size compression with < 1% accuracy drop, 10x CPU-inference speedup with < 2% accuracy drop, and 29x CPU-inference speedup with < 7.5% accuracy drop. Our code, fully integrated with Transformers and SparseML, is available at https://github.com/neuralmagic/sparseml/tree/main/research/optimal_BERT_surgeon_oBERT.},
  author       = {Kurtic, Eldar and Campos, Daniel and Nguyen, Tuan and Frantar, Elias and Kurtz, Mark and Fineran, Benjamin and Goin, Michael and Alistarh, Dan-Adrian},
  booktitle    = {Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing},
  location     = {Abu Dhabi, United Arab Emirates},
  pages        = {4163--4181},
  publisher    = {Association for Computational Linguistics},
  title        = {{The optimal BERT surgeon: Scalable and accurate second-order pruning for large language models}},
  doi          = {10.18653/v1/2022.emnlp-main.279},
  year         = {2022},
}

@unpublished{17115,
  abstract     = {Cascades are RNA-guided multi-subunit CRISPR-Cas surveillances complexes that target foreign nucleic acids for destruction. Here, we present a 2.9-Å resolution cryo-electron (cryo-EM) structure of the <jats:italic>D. vulgaris</jats:italic> type I-C Cascade bound to a double-stranded (ds)DNA target. Our data shows how the 5’-TTC-3’ protospacer adjacent motif (PAM) sequence is recognized, and provides a unique mechanism through which the displaced, single-stranded non-target strand (NTS) is stabilized via stacking interactions with protein subunits in order to favor R-loop formation and prevent dsDNA re-annealing. Additionally, we provide structural insights into how diverse anti-CRISPR (Acr) proteins utilize distinct strategies to achieve a shared mechanism of type I-C Cascade inhibition by blocking initial DNA binding. These observations provide a structural basis for directional R-loop formation and reveal how divergent Acr proteins have converged upon common molecular mechanisms to efficiently shut down CRISPR immunity.},
  author       = {O’Brien, Roisin E. and Bravo, Jack Peter Kelly and Ramos, Delisa and Hibshman, Grace N. and Wright, Jacquelyn T. and Taylor, David W.},
  booktitle    = {bioRxiv},
  publisher    = {Cold Spring Harbor Laboratory},
  title        = {{Modes of inhibition used by phage anti-CRISPRs to evade type I-C Cascade}},
  doi          = {10.1101/2022.06.15.496202},
  year         = {2022},
}

@unpublished{17116,
  abstract     = {CRISPR (Clustered regularly interspaced short palindromic repeats)-Cas (CRISPR-associated) systems are a type of adaptive immune response in bacteria and archaea that utilize crRNA (CRISPR RNA)-guided effector complexes to target complementary RNA or DNA for destruction. The prototypical type III-A and III-B CRISPR-Cas systems utilize multi-subunit effector complexes composed of individual proteins to cleave ssRNA targets at 6-nt intervals, as well as non-specifically degrading ssDNA and activating cyclic oligoadenylate (cOA) synthesis. Recent studies have shown that type III systems can contain subunit fusions yet maintain canonical type III RNA-targeting capabilities. To understand how a multi-subunit fusion effector functions, we determine structures of a variant type III-D effector and biochemically characterize how it cleaves RNA targets. These findings provide insights into how multi-subunit fusion proteins are tethered together and assemble into an active and programmable RNA endonuclease, how the effector utilizes a novel mechanism for target RNA seeding, and the structural basis for the evolution of type III effector complexes. Furthermore, our results provide a blueprint for fusing subunits in class 1 effectors for design of user-defined effector complexes with disparate activities.</jats:p><jats:sec><jats:title>Important note</jats:title><jats:p>While this manuscript was in preparation, a manuscript describing the structure of the type III-E effector was published<jats:sup>1</jats:sup>. We reference these important findings; however, a careful comparison of the structures will follow once the coordinates have been released by the PDB.},
  author       = {Schwartz, Evan A. and Bravo, Jack Peter Kelly and Macias, Luis A. and McCafferty, Caitlyn L. and Dangerfield, Tyler L. and Walker, Jada N. and Brodbelt, Jennifer S. and Fineran, Peter C. and Fagerlund, Robert D. and Taylor, David W.},
  booktitle    = {bioRxiv},
  publisher    = {Cold Spring Harbor Laboratory},
  title        = {{Assembly of multi-subunit fusion proteins into the RNA-targeting type III-D CRISPR-Cas effector complex}},
  doi          = {10.1101/2022.06.13.496011},
  year         = {2022},
}

@unpublished{17117,
  abstract     = {Cas12a2 is a CRISPR-associated nuclease that performs RNA-guided degradation of non-specific single-stranded (ss)RNA, ssDNA and double-stranded (ds)DNA upon recognition of a complementary RNA target, culminating in abortive infection (Dmytrenko 2022). Here, we report structures of Cas12a2 in binary, ternary, and quaternary complexes to reveal a complete activation pathway. Our structures reveal that Cas12a2 is autoinhibited until binding a cognate RNA target, which exposes the RuvC active site within a large, positively charged cleft. Double-stranded DNA substrates are captured through duplex distortion and local melting, stabilized by pairs of ‘aromatic clamp’ residues that are crucial for dsDNA degradation and in <jats:italic>vivo</jats:italic> immune system function. Our work provides a structural basis for this unprecedented mechanism of abortive infection to achieve population-level immunity, which can be leveraged to create rational mutants that degrade a spectrum of collateral substrates.},
  author       = {Bravo, Jack Peter Kelly and Hallmark, Thom and Naegle, Bronson and Beisel, Chase L. and Jackson, Ryan N. and Taylor, David W.},
  booktitle    = {bioRxiv},
  publisher    = {Cold Spring Harbor Laboratory},
  title        = {{Large-scale structural rearrangements unleash indiscriminate nuclease activity of CRISPR-Cas12a2}},
  doi          = {10.1101/2022.06.13.495754},
  year         = {2022},
}

@article{17383,
  abstract     = {We present a computational inverse design framework for a new class of volumetric deployable structures that have compact rest states and deploy into bending-active 3D target surfaces. Umbrella meshes consist of elastic beams, rigid plates, and hinge joints that can be directly printed or assembled in a zero-energy fabrication state. During deployment, as the elastic beams of varying heights rotate from vertical to horizontal configurations, the entire structure transforms from a compact block into a target curved surface. Umbrella Meshes encode both intrinsic and extrinsic curvature of the target surface and in principle are free from the area expansion ratio bounds of past auxetic material systems.
We build a reduced physics-based simulation framework to accurately and efficiently model the complex interaction between the elastically deforming components. To determine the mesh topology and optimal shape parameters for approximating a given target surface, we propose an inverse design optimization algorithm initialized with conformal flattening. Our algorithm minimizes the structure's strain energy in its deployed state and optimizes actuation forces so that the final deployed structure is in stable equilibrium close to the desired surface with few or no external constraints. We validate our approach by fabricating a series of physical models at various scales using different manufacturing techniques.},
  author       = {Ren, Yingying and Kusupati, Uday and Panetta, Julian and Isvoranu, Florin and Pellis, Davide and Chen, Tian and Pauly, Mark},
  issn         = {1557-7368},
  journal      = {ACM Transactions on Graphics},
  number       = {4},
  pages        = {1--15},
  publisher    = {Association for Computing Machinery},
  title        = {{Umbrella meshes: Elastic mechanisms for freeform shape deployment}},
  doi          = {10.1145/3528223.3530089},
  volume       = {41},
  year         = {2022},
}

@article{17501,
  abstract     = {Low-level systems code often needs to interact with data, such as page table entries or network packet headers, in which multiple pieces of information are packaged together as bitfield components of a single machine integer and accessed via bitfield manipulations (e.g., shifts and masking). Most existing approaches to verifying such code employ SMT solvers, instantiated with theories for bit vector reasoning: these provide a powerful hammer, but also significantly increase the trusted computing base of the verification toolchain.
In this work, we propose an alternative approach to the verification of bitfield-manipulating systems code, which we call BFF. Building on the RefinedC framework, BFF is not only highly automated (as SMT-based approaches are) but also foundational---i.e., it produces a machine-checked proof of program correctness against a formal semantics for C programs, fully mechanized in Coq. Unlike SMT-based approaches, we do not try to solve the general problem of arbitrary bit vector reasoning, but rather observe that real systems code typically accesses bitfields using simple, well-understood programming patterns: the layout of a bit vector is known up front, and its bitfields are accessed in predictable ways through a handful of bitwise operations involving bit masks. Correspondingly, we center our approach around the concept of a structured bit vector---i.e., a bit vector with a known bitfield layout---which we use to drive simple and predictable automation. We validate the BFF approach by verifying a range of bitfield-manipulating C functions drawn from real systems code, including page table manipulation code from the Linux kernel and the pKVM hypervisor.},
  author       = {Zhu, Fengmin and Sammler, Michael Joachim and Lepigre, Rodolphe and Dreyer, Derek and Garg, Deepak},
  issn         = {2475-1421},
  journal      = {Proceedings of the ACM on Programming Languages},
  number       = {OOPSLA2},
  pages        = {1613--1638},
  publisher    = {Association for Computing Machinery},
  title        = {{BFF: Foundational and automated verification of bitfield-manipulating programs}},
  doi          = {10.1145/3563345},
  volume       = {6},
  year         = {2022},
}

@inproceedings{17502,
  abstract     = {Recent years have seen great advances towards verifying large-scale systems code. However, these verifications are usually based on hand-written assembly or machine-code semantics for the underlying architecture that only cover a small part of the instruction set architecture (ISA). In contrast, other recent work has used Sail to establish formal models for large real-world architectures, including Armv8-A and RISC-V, that are comprehensive (complete enough to boot an operating system or hypervisor) and authoritative (automatically derived from the Arm internal model and validated against the Arm validation suite, and adopted as the official formal specification by RISC-V International, respectively). But the scale and complexity of these models makes them challenging to use as a basis for verification.
In this paper, we propose Islaris, the first system to support verification of machine code above these complete and authoritative real-world ISA specifications. Islaris uses a novel combination of SMT-solver-based symbolic execution (the Isla symbolic executor) and automated reasoning in a foundational program logic (a new separation logic we derive using Iris in Coq). We show that this approach can handle Armv8-A and RISC-V machine code exercising a wide range of systems features, including installing and calling exception vectors, code parametric on a relocation address offset (from the production pKVM hypervisor); unaligned access faults; memory-mapped IO; and compiled C code using inline assembly and function pointers.},
  author       = {Sammler, Michael Joachim and Hammond, Angus and Lepigre, Rodolphe and Campbell, Brian and Pichon-Pharabod, Jean and Dreyer, Derek and Garg, Deepak and Sewell, Peter},
  booktitle    = {Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
  location     = {San Diego, CA, United States},
  pages        = {825--840},
  publisher    = {Association for Computing Machinery},
  title        = {{Islaris: Verification of machine code against authoritative ISA semantics}},
  doi          = {10.1145/3519939.3523434},
  year         = {2022},
}

@article{17503,
  abstract     = {Systems code often requires fine-grained control over memory layout and pointers, expressed using low-level (e.g., bitwise) operations on pointer values. Since these operations go beyond what basic pointer arithmetic in C allows, they are performed with the help of integer-pointer casts. Prior work has explored increasingly realistic memory object models for C that account for the desired semantics of integer-pointer casts while also being sound w.r.t. compiler optimisations, culminating in PNVI, the preferred memory object model in ongoing discussions within the ISO WG14 C standards committee. However, its complexity makes it an unappealing target for verification, and no tools currently exist to verify C programs under PNVI.
In this paper, we introduce VIP, a new memory object model aimed at supporting C verification. VIP sidesteps the complexities of PNVI with a simple but effective idea: a new construct that lets programmers express the intended provenances of integer-pointer casts explicitly. At the same time, we prove VIP compatible with PNVI, thus enabling verification on top of VIP to benefit from PNVI’s validation with respect to practice. In particular, we build a verification tool, RefinedC-VIP, for verifying programs under VIP semantics. As the name suggests, RefinedC-VIP extends the recently developed RefinedC tool, which is automated yet also produces foundational proofs in Coq. We evaluate RefinedC-VIP on a range of systems-code idioms, and validate VIP’s expressiveness via an implementation in the Cerberus C semantics.},
  author       = {Lepigre, Rodolphe and Sammler, Michael Joachim and Memarian, Kayvan and Krebbers, Robbert and Dreyer, Derek and Sewell, Peter},
  issn         = {2475-1421},
  journal      = {Proceedings of the ACM on Programming Languages},
  number       = {POPL},
  pages        = {1--32},
  publisher    = {Association for Computing Machinery},
  title        = {{VIP: Verifying real-world C idioms with integer-pointer casts}},
  doi          = {10.1145/3498681},
  volume       = {6},
  year         = {2022},
}

@article{17504,
  abstract     = {Today’s compilers employ a variety of non-trivial optimizations to achieve good performance. One key trick compilers use to justify transformations of concurrent programs is to assume that the source program has no data races: if it does, they cause the program to have undefined behavior (UB) and give the compiler free rein. However, verifying correctness of optimizations that exploit this assumption is a non-trivial problem. In particular, prior work either has not proven that such optimizations preserve program termination (particularly non-obvious when considering optimizations that move instructions out of loop bodies), or has treated all synchronization operations as external functions (losing the ability to reorder instructions around them).
In this work we present Simuliris, the first simulation technique to establish termination preservation (under a fair scheduler) for a range of concurrent program transformations that exploit UB in the source language. Simuliris is based on the idea of using ownership to reason modularly about the assumptions the compiler makes about programs with well-defined behavior. This brings the benefits of concurrent separation logics to the space of verifying program transformations: we can combine powerful reasoning techniques such as framing and coinduction to perform thread-local proofs of non-trivial concurrent program optimizations. Simuliris is built on a (non-step-indexed) variant of the Coq-based Iris framework, and is thus not tied to a particular language. In addition to demonstrating the effectiveness of Simuliris on standard compiler optimizations involving data race UB, we also instantiate it with Jung et al.’s Stacked Borrows semantics for Rust and generalize their proofs of interesting type-based aliasing optimizations to account for concurrency.},
  author       = {Gäher, Lennard and Sammler, Michael Joachim and Spies, Simon and Jung, Ralf and Dang, Hoang-Hai and Krebbers, Robbert and Kang, Jeehoon and Dreyer, Derek},
  issn         = {2475-1421},
  journal      = {Proceedings of the ACM on Programming Languages},
  number       = {POPL},
  pages        = {1--31},
  publisher    = {Association for Computing Machinery},
  title        = {{Simuliris: A separation logic framework for verifying concurrent program optimizations}},
  doi          = {10.1145/3498689},
  volume       = {6},
  year         = {2022},
}