bluuebunny/crossref_metadata_2025_split huggingface dataset:
The whole-genome molecular epidemiology of sequential isolates of
Acinetobacter baumannii
colonizing the rectum of patients in an adult intensive care unit of a tertiary hospital
Authors: Bulach Dieter , Carter Glen P. , Li Lucy , Al-Hashem Ghayda , Rotimi Vincent O. , Albert M. John 
Published: October 2023

ABSTRACT

Acinetobacter baumannii
is a nosocomial multidrug-resistant pathogen that specifically colonizes and infects patients in intensive care units (ICUs). Genome plasticity of
A. baumannii
may contribute to the rapid development of
A. baumannii
resistance during patient treatment. There is little clarity on the dynamics of colonization of
A. baumannii
in humans. We studied 269 serial isolates of
A. baumannii
colonizing the rectum of 32 adult patients in an ICU; 5 to 16 isolates were obtained from each patient over a period of weeks to months. The isolates were sequenced using the Illumina platform. Multi-locus sequence typing revealed genetic diversity with 13 sequence types (STs); the dominant ST2 accounted for 202 of the 269 isolates and was isolated from each patient. A core genome comparison of isolates was used to elucidate a detailed understanding of the relationship among isolates within an ST and the genomic relationship among STs. One to three STs were observed in the isolates from each patient. Instances of unchanged colonization, sequential lineage colonization, and colonization with multiple lineages of
A. baumannii
were seen. The number of resistance genes carried by the isolates varied from 2 to 17. The predominant genes corresponded to those encoding resistance to β-lactam and aminoglycoside antibiotics. Generally, there was a strong correlation between ST and a particular antimicrobial resistance gene profile. This study makes an important baseline contribution to information that will help us understand the role of
A. baumannii
colonization in the development of opportunistic infections in ICU patients.

IMPORTANCE

Acinetobacter baumannii
is a multidrug-resistant nosocomial pathogen that colonizes and infects debilitated patients in the ICU. There is very little information on the genomic characteristics of colonizing strains. This information is important to understand the evolution of lineages of
A. baumannii
that develop resistance while patients receive antibiotic treatment in the ICU. Our study demonstrated different patterns of colonization of the rectum of ICU patients with different STs of
A. baumannii
while one ST colonized all patients. Some STs carried more antibiotic resistance genes compared to others. However, there was a correlation between ST and a particular resistance gene profile. Our results further elucidate the dynamics of enteric colonization of this opportunistic pathogen.
Impact of a Water Microjet on a Microfiber
Authors: Bazilevsky A. V. , Rozhkov A. N. 
Published: October 2023

Abstract
The transverse impact of a pulsed water microjet on individual cylindrical fibers is studied. The stages of ejection, breakup, and collision of the microjet were recorded by high-speed photography. A significant deceleration of the microjet by the fiber and its splitting into two parts were revealed. The mechanisms of the observed phenomena and the influence of various factors are discussed.
Mineral and Raw-Material Potential of Strategic Critical Mineral Raw Material for Development of the High-Tech Industry of the Russian Federation
Authors: Petrov O. V. , Molchanov A. V. , Shatov V. V. , Zubova T. N. 
Published: October 2023

Abstract
The present paper briefly characterizes the state system of a regional geological study of subsoil implemented by Rosnedra and the Karpinsky All-Russian Research Geological Institute (VSEGEI) and provides an assessment of the mineral and raw material potential of the Russian Federation for strategic types of minerals. In 2022, the VSEGEI completed compiling of a set of 1 : 2 500 000 digital monometal maps of patterns of distribution and prediction of strategic and critical types of minerals of the Russian Federation in GIS-format. The reserves of these types of minerals were estimated according to the data of the state accounting system and expert reassessment of forecast resources was performed. As a result, regional prognostic criteria for localization of areas promising for searching deposits were developed. Recommendations on setting GDP-200/2 and/or GMK-200 on specific nomenclature sheets that are promising for realization of prospecting stage exploration for strategic types of mineral raw materials are given.
One-step embedding method for maintaining orientation of pathological tissue specimens using agar thin films
Authors: Uchiyama Atsushi , Kimura Fumikazu , Wakatsuki Yoshie , Yoshida Erika , Kato Ayako , Kato Kurumi , Yoshida Rio , Ito Yurie , Okimura Akira , Nakatsugawa Munehide 
Published: October 2023

Pathological histology examination involves handling a variety of specimens that are cut according to regulations and placed in cassettes. Tissue fragments in the cassettes are then diagnosed after processing, embedding, thin sectioning, staining and other procedures using a processing machine. Maintaining tissue fragment order and orientation during these processes is important for accurate diagnosis. In this study, we present a method of maintaining tissue fragment order and orientation using a thin film of ultra-high-strength agar and evaluate its usefulness during tissue sectioning.Cassettes were prepared, each containing three pieces of porcine liver, and compared embedding time with and without agar thin films (ATFs). Embedding was performed by three medical laboratory scientists with different levels of experience.To enable one-step tissue sample embedding, ATFs were integrated with samples in the cassettes. This resulted in an average reduction of 6.22 s of embedding time per cassette compared with traditional embedding methods.Through the use of ATFs, tissue fragment order and orientation is maintained, and embedding process time shortened. Additionally, ATFs are easily prepared and stored in 10% neutral buffered formalin over extended periods, allowing for immediate use during sectioning. This method is ideal to implement in busy pathology laboratories.
Surveillance is the first step to preventing injury among fast jet aircrew: results of a 2-year prospective cohort study
Authors: Wallace James Byron , Osmotherly Peter G , Gabbett Tim J , Spratford Wayne , Newman Phil Mark 
Published: October 2023

ObjectivesInjury surveillance is imperative for injury prevention but difficult in military populations. Our objective was to accurately describe the pattern of musculoskeletal complaints among Royal Australian Air Force (RAAF) fast jet aircrew (FJA) using the validated University of Canberra Fast Jet Aircrew Musculoskeletal Questionnaire (UC-FJAMQ) over a 2-year period, and determine injury burden on the workforce and operational capability.Methods306 RAAF FJA were monitored over a 2-year period (4×5 month reporting periods). Musculoskeletal complaint episodes (MCEs) were captured weekly using the UC-FJAMQ. Time loss episodes (TLEs) were captured from the UC-FJAMQ and injury registers completed by embedded physiotherapists. Cumulative severity and operational impact scores from the UC-FJAMQ, and time loss duration, were used to describe severity and calculate burden.ResultsMean weekly UC-FJAMQ response rate was 62%. 1012 MCEs were captured, with a mean weekly prevalence of 14.9% (95% CI 14.2–15.6), and incidence of 4.1 episodes per person-year (95% CI 3.9–4.4). A total of 145 TLEs were captured, with a mean 5-month prevalence of 12.4% (range 8.9–15.3%), and incidence of 0.37 episodes per person-year (95% CI 0.31–0.43). Spinal regions accounted for 81% of MCEs and contributed 76% and 85% of burden in relation to cumulative severity and operational impact, respectively. 57% of TLE burden came from spinal regions.ConclusionsDespite modest weekly UC-FJAMQ response rates, musculoskeletal complaints were shown to be widespread and negatively impact operational capability. Future injury prevention efforts among FJA should focus on spinal regions, particularly the neck.
Droplets and supersolids in ultra-cold atomic quantum gases
Authors: Mukherjee K. , Cardinale T. Arnone , Chergui L. , Stürmer P. , Reimann S. M. 
Published: October 2023

AbstractIn this mini-review, we briefly summarize some of the main concepts and ideas behind highly dilute self-bound quantum droplets of both binary and dipolar character. The latter type of systems has more recently led to the experimental discovery of a dipolar supersolid state that allows entirely new insights on this long-sought purely quantum state of matter, with exciting prospects for fundamental research as well as future applied quantum sensing technologies. The first half of the review provides a brief history of droplets and supersolidity in various settings and also discusses the self-binding in binary quantum gases, and the second half of the review summarizes our own recent work in the field, presented at the 2022 FQMT conference in Prague.
Leaf: Modularity for Temporary Sharing in Separation Logic
Authors: Hance Travis , Howell Jon , Padon Oded , Parno Bryan 
Published: October 2023

In concurrent verification, separation logic provides a strong story for handling both resources that are owned exclusively and resources that are shared persistently (i.e., forever). However, the situation is more complicated for temporarily shared state, where state might be shared and then later reclaimed as exclusive. We believe that a framework for temporarily-shared state should meet two key goals not adequately met by existing techniques. One, it should allow and encourage users to verify new sharing strategies. Two, it should provide an abstraction where users manipulate shared state in a way agnostic to the means with which it is shared.
We present Leaf, a library in the Iris separation logic which accomplishes both of these goals by introducing a novel operator, which we call guarding, that allows one proposition to represent a shared version of another. We demonstrate that Leaf meets these two goals through a modular case study: we verify a reader-writer lock that supports shared state, and a hash table built on top of it that uses shared state.
AtomiS: Data-Centric Synchronization Made Practical
Authors: Paulino Hervé , Almeida Matos Ana , Cederquist Jan , Giunti Marco , Matos João , Ravara António 
Published: October 2023

Data-Centric Synchronization (DCS) shifts the reasoning about concurrency restrictions from control structures to data declaration. It is a high-level declarative approach that abstracts away from the actual concurrency control mechanism(s) in use. Despite its advantages, the practical use of DCS is hindered by the fact that it may require many annotations and/or multiple implementations of the same method to cope with differently qualified parameters.
To overcome these limitations, in this paper we present AtomiS, a new DCS approach that requires only qualifying types of parameters and return values in interface definitions, and of fields in class definitions. The latter may also be abstracted away in type parameters, rendering class implementations virtually annotation-free. From this high level specification, a static analysis infers the atomicity constraints that are local to each method, considering valid only the method variants that are consistent with the specification, and performs code generation for all valid variants of each method. The generated code is then the target for automatic injection of concurrency control primitives that are responsible for ensuring the absence of data-races,
atomicity-violations and deadlocks.
We provide a Java implementation and showcase the applicability of AtomiS in real-life code. For the
benchmarks analysed, AtomiS requires fewer annotations than the original number of regions requiring locks, as well as fewer annotations than Atomic Sets (a reference DCS proposal).
A Cocktail Approach to Practical Call Graph Construction
Authors: Cai Yuandao , Zhang Charles 
Published: October 2023

After decades of research, constructing call graphs for modern C-based software remains either imprecise or inefficient when scaling up to the ever-growing complexity. The main culprit is the difficulty of resolving function pointers, as precise pointer analyses are cubic in nature and become exponential when considering calling contexts. This paper takes a practical stance by first conducting a comprehensive empirical study of function pointer manipulations in the wild. By investigating 5355 indirect calls in five popular open-source systems, we conclude that, instead of the past uniform treatments for function pointers, a cocktail approach can be more effective in “squeezing” the number of difficult pointers to a minimum using a potpourri of cheap methods. In particular, we decompose the costs of constructing highly precise call graphs of big code by tailoring several increasingly precise algorithms and synergizing them into a concerted workflow. As a result, many indirect calls can be precisely resolved in an efficient and principled fashion, thereby reducing the final, expensive refinements. This is, in spirit, similar to the well-known cocktail medical therapy.
The results are encouraging — our implemented prototype called Coral can achieve similar precision versus the previous field-, flow-, and context-sensitive Andersen-style call graph construction, yet scale up to millions of lines of code for the first time, to the best of our knowledge. Moreover, by evaluating the produced call graphs through the lens of downstream clients (i.e., use-after-free detection, thin slicing, and directed grey-box fuzzing), the results show that Coral can dramatically improve their effectiveness for better vulnerability hunting, understanding, and reproduction. More excitingly, we found twelve confirmed bugs (six impacted by indirect calls) in popular systems (e.g., MariaDB), spreading across multiple historical versions.
Building Dynamic System Call Sandbox with Partial Order Analysis
Authors: Zhang Quan , Zhou Chijin , Xu Yiwen , Yin Zijing , Wang Mingzhe , Su Zhuo , Sun Chengnian , Jiang Yu , Sun Jiaguang 
Published: October 2023

Attack surface reduction is a security technique that secures the operating system by removing the unnecessary code or features of a program. By restricting the system calls that programs can use, the system call sandbox is able to reduce the exposed attack surface of the operating system and prevent attackers from damaging it through vulnerable programs. Ideally, programs should only retain access to system calls they require for normal execution. Many researchers focus on adopting static analysis to automatically restrict the system calls for each program. However, these methods do not adjust the restriction policy along with program execution. Thus, they need to permit all system calls required for program functionalities.
We observe that some system calls, especially security-sensitive ones, are used a few times in certain stages of a program’s execution and then never used again. This motivates us to minimize the set of required system calls dynamically. In this paper, we propose , which gradually disables access to unnecessary system calls throughout the program’s execution. To accomplish this, we utilize partial order analysis to transform the program into a partially ordered graph, which enables efficient identification of the necessary system calls at any given point during program execution. Once a system call is no longer required by the program, can restrict it immediately. To evaluate , we applied it to seven widely-used programs with an average of 615 KLOC, including web servers and databases. With partial order analysis, restricts an average of 23.50, 16.86, and 15.89 more system calls than the state-of-the-art Chestnut, Temporal Specialization, and the configuration-aware sandbox, C2C, respectively. For mitigating malicious exploitations, on average, defeats 83.42% of 1726 exploitation payloads with only a 5.07% overhead.
TASTyTruffle: Just-in-Time Specialization of Parametric Polymorphism
Authors: D'Souza Matt , You James , Lhoták Ondřej , Prokopec Aleksandar 
Published: October 2023

Parametric polymorphism enables programmers to express algorithms independently of the types of values that they operate on. The approach used to implement parametric polymorphism can have important performance implications. One popular approach, erasure, uses a uniform representation for generic data, which entails primitive boxing and other indirections that harm performance. Erasure destroys type information that could be used by language implementations to optimize generic code.
We present TASTyTruffle, an implementation for a subset of the Scala programming language. Instead of JVM bytecode, TASTyTruffle interprets Scala's TASTy intermediate representation, a typed representation wherein generic types are not erased. TASTy's precise type information empowers TASTyTruffle to implement generic code more effectively. In particular, it allows TASTyTruffle to reify types as run-time objects that can be passed around. Using reified types, TASTyTruffle supports heterogeneous box-free representations for generic values. TASTyTruffle also uses reified types to specialize generic code, producing monomorphic copies of generic code that can be easily and reliably optimized by its just-in-time (JIT) compiler.
Empirically, TASTyTruffle is competitive with standard JVM implementations on a small set of benchmark programs; when generic code is used with multiple types, TASTyTruffle consistently outperforms the JVM. The precise type information in TASTy enables TASTyTruffle to find additional optimization opportunities that could not be uncovered with erased JVM bytecode.
Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs
Authors: Renda Alex , Ding Yi , Carbin Michael 
Published: October 2023

Programmers and researchers are increasingly developing surrogates of programs, models of a subset of the observable behavior of a given program, to solve a variety of software development challenges. Programmers train surrogates from measurements of the behavior of a program on a dataset of input examples. A key challenge of surrogate construction is determining what training data to use to train a surrogate of a given program.
We present a methodology for sampling datasets to train neural-network-based surrogates of programs. We first characterize the proportion of data to sample from each region of a program's input space (corresponding to different execution paths of the program) based on the complexity of learning a surrogate of the corresponding execution path. We next provide a program analysis to determine the complexity of different paths in a program. We evaluate these results on a range of real-world programs, demonstrating that complexity-guided sampling results in empirical improvements in accuracy.
Inference of Resource Management Specifications
Authors: Shadab Narges , Gharat Pritam , Tiwari Shrey , Ernst Michael D. , Kellogg Martin , Lahiri Shuvendu K. , Lal Akash , Sridharan Manu 
Published: October 2023

A resource leak occurs when a program fails to free some finite resource after it is no longer needed. Such leaks are a significant cause of real-world crashes and performance problems. Recent work proposed an approach to prevent resource leaks based on checking resource management specifications. A resource management specification expresses how the program allocates resources, passes them around, and releases them; it also tracks the ownership relationship between objects and resources, and aliasing relationships between objects. While this specify-and-verify approach has several advantages compared to prior techniques, the need to manually write annotations presents a significant barrier to its practical adoption.
This paper presents a novel technique to automatically infer a resource management specification for a program, broadening the applicability of specify-and-check verification for resource leaks. Inference in this domain is challenging because resource management specifications differ significantly in nature from the types that most inference techniques target. Further, for practical effectiveness, we desire a technique that can infer the resource management specification intended by the developer, even in cases when the code does not fully adhere to that specification. We address these challenges through a set of inference rules carefully designed to capture real-world coding patterns, yielding an effective fixed-point-based inference algorithm.
We have implemented our inference algorithm in two different systems, targeting programs written in Java and C#. In an experimental evaluation, our technique inferred 85.5% of the annotations that programmers had written manually for the benchmarks. Further, the verifier issued nearly the same rate of false alarms with the manually-written and automatically-inferred annotations.
Gradual Typing for Effect Handlers
Authors: New Max S. , Giovannini Eric , Licata Daniel R. 
Published: October 2023

We present a gradually typed language, GrEff, with effects and handlers that supports migration from unchecked to checked effect typing. This serves as a simple model of the integration of an effect typing discipline with an existing effectful typed language that does not track fine-grained effect information. Our language supports a simple module system to model the programming model of gradual migration from unchecked to checked effect typing in the style of Typed Racket.
The surface language GrEff is given semantics by elaboration to a core language Core GrEff. We equip Core GrEff with an inequational theory for reasoning about the semantic error ordering and desired program equivalences for programming with effects and handlers. We derive an operational semantics for the language from the equations provable in the theory. We then show that the theory is sound by constructing an operational logical relations model to prove the graduality theorem. This extends prior work on embedding-projection pair models of gradual typing to handle effect typing and subtyping.
A Deductive Verification Infrastructure for Probabilistic Programs
Authors: Schröer Philipp , Batz Kevin , Kaminski Benjamin Lucien , Katoen Joost-Pieter , Matheja Christoph 
Published: October 2023

This paper presents a quantitative program verification infrastructure for discrete
probabilistic programs.
Our infrastructure can be viewed as the probabilistic analogue of Boogie:
its central components are an intermediate verification language (IVL) together with a real-valued logic.
Our IVL provides a programming-language-style for expressing verification
conditions whose validity implies the correctness of a program under investigation.
As our
focus is on verifying quantitative properties such as bounds on
expected outcomes, expected run-times, or termination
probabilities, off-the-shelf IVLs based on Boolean first-order logic do not
suffice.
Instead, a paradigm shift from the standard Boolean to a real-valued domain is required.
Our IVL features quantitative generalizations of standard
verification constructs such as assume- and assert-statements. Verification conditions are generated by a
weakest-precondition-style semantics, based on our real-valued logic.
We show that
our verification infrastructure supports natural encodings of numerous verification
techniques from the literature. With our SMT-based implementation, we automatically verify a variety of benchmarks. To the best of our knowledge, this establishes the first deductive verification
infrastructure for expectation-based reasoning about probabilistic programs.