Search for: All records

In eukaryotes, many DNA/RNA-binding proteins possess intrinsically disordered regions (IDRs) with large negative charge, some of which involve a consecutive sequence of aspartate (D) or glutamate (E) residues. We refer to them as D/E repeats. The functional role of D/E repeats is not well understood, though some of them are known to cause autoinhibition through intramolecular electrostatic interaction with functional domains. In this work, we investigated the impacts of D/E repeats on the target DNA search kinetics for the high-mobility group box 1 (HMGB1) protein and the artificial protein constructs of the Antp homeodomain fused with D/E repeats of varied lengths. Our experimental data showed that D/E repeats of particular lengths can accelerate the target association in the overwhelming presence of non-functional high-affinity ligands (‘decoys’). Our coarse-grained molecular dynamics (CGMD) simulations showed that the autoinhibited proteins can bind to DNA and transition into the uninhibited complex with DNA through an electrostatically driven induced-fit process. In conjunction with the CGMD simulations, our kinetic model can explain how D/E repeats can accelerate the target association process in the presence of decoys. This study illuminates an unprecedented role of the negatively charged IDRs in the target search process.

High-precision potassium (K) isotope measurements in marine carbonates allow using this novel geochemical proxy to constrain seawater chemistry through geologic time. However, these measurements are still scarce due to the challenges of low-K contents in carbonates during K ion chromatography, such as insufficient sample purification, non-quantitative yield, and high accumulative blank. Here we optimize a dual-column K purification method that addresses these challenges, achieving a satisfactory K separation using 100–150 mg carbonates for routine high-precision K isotope analysis on the Sapphire™ MC-ICP-MS. We then report K isotope compositions in multiple certified reference materials, including limestone, dolostone, coral, and basalt for future inter-laboratory comparisons. The optimized K purification method provides great potential for future K isotope studies of marine carbonates.

Multi-band photometric observations of 11 totally eclipsing contact binaries were carried out. Applying the Wilson–Devinney program, photometric solutions were obtained. There are two W-subtype systems, which are CRTS J133031.1+161202 and CRTS J154254.0+324652, and the rest of the systems are A-subtype systems. CRTS J154254.0 + 324652 has the highest fill-out factor with 94.3 per cent, and the lowest object is CRTS J155009.2 + 493639 with only 18.9 per cent. The mass ratios of the 11 systems are all less than 0.1, which means that they are extremely low-mass ratio binary systems. We performed period variation investigation and found that the orbital periods of three systems decrease slowly, which may be caused by the angular momentum loss, and those of six systems increase slowly, which indicates that the materials may transfer from the secondary component to the primary component. LAMOST low-resolution spectra of four objects were analysed, and using the spectral subtraction technique, Hα emission line was detected, which means that the four objects exhibit chromospheric activity. In order to understand their evolutionary status, the mass–luminosity and mass–radius diagrams were plotted. The two diagrams indicate that the primary component is in the main sequence evolution stage, and the secondary component is above TAMS, indicating thatmore »they are over-luminous. To determine whether the 11 systems are in a stable state, the ratio of spin angular momentum to orbital angular momentum (Js/Jo) and the instability parameters were calculated, and we argued that CRTS J234634.7 + 222824 is on the verge of a merger.

« less

Reusable symbolic evaluators are a key building block of solver-aided verification and synthesis tools. A reusable evaluator reduces the semantics of all paths in a program to logical constraints, and a client tool uses these constraints to formulate a satisfiability query that is discharged with SAT or SMT solvers. The correctness of the evaluator is critical to the soundness of the tool and the domain properties it aims to guarantee. Yet so far, the trust in these evaluators has been based on an ad-hoc foundation of testing and manual reasoning. This paper presents the first formal framework for reasoning about the behavior of reusable symbolic evaluators. We develop a new symbolic semantics for these evaluators that incorporates state merging. Symbolic evaluators use state merging to avoid path explosion and generate compact encodings. To accommodate a wide range of implementations, our semantics is parameterized by a symbolic factory, which abstracts away the details of merging and creation of symbolic values. The semantics targets a rich language that extends Core Scheme with assumptions and assertions, and thus supports branching, loops, and (first-class) procedures. The semantics is designed to support reusability, by guaranteeing two key properties: legality of the generated symbolic states, andmore »the reducibility of symbolic evaluation to concrete evaluation. Legality makes it simpler for client tools to formulate queries, and reducibility enables testing of client tools on concrete inputs. We use the Lean theorem prover to mechanize our symbolic semantics, prove that it is sound and complete with respect to the concrete semantics, and prove that it guarantees legality and reducibility. To demonstrate the generality of our semantics, we develop Leanette, a reference evaluator written in Lean, and Rosette 4, an optimized evaluator written in Racket. We prove Leanette correct with respect to the semantics, and validate Rosette 4 against Leanette via solver-aided differential testing. To demonstrate the practicality of our approach, we port 16 published verification and synthesis tools from Rosette 3 to Rosette 4. Rosette 3 is an existing reusable evaluator that implements the classic merging semantics, adopted from bounded model checking. Rosette 4 replaces the semantic core of Rosette 3 but keeps its optimized symbolic factory. Our results show that Rosette 4 matches the performance of Rosette 3 across a wide range of benchmarks, while providing a cleaner interface that simplifies the implementation of client tools.« less

Video analytics has many applications in traffic control, security monitoring, action/event analysis, etc. With the adoption of deep neural networks, the accuracy of video analytics in video streams has been greatly improved. However, deep neural networks for performing video analytics are compute-intensive. In order to reduce processing time, many systems switch to the lower frame rate or resolution. State-of-the-art switching approaches adjust configurations by profiling video clips on a large configuration space. Multiple configurations are tested periodically and the cheapest one with a desired accuracy is adopted. In this paper, we propose a method that adapts the configuration by analyzing past video analytics results instead of profiling candidate configurations. Our method adopts a lower/higher resolution or frame rate when objects move slow/fast. We train a model that automatically selects the best configuration. We evaluate our method with two real-world video analytics applications: traffic tracking and pose estimation. Compared to the periodic profiling method, our method achieves 3%-12% higher accuracy with the same resource cost and 8-17x faster with comparable accuracy.