bluuebunny/crossref_metadata_2025 huggingface dataset:
Compiling with Abstract Interpretation
Authors: Lesbre Dorian , Lemerre Matthieu
Published: June 2024

Rewriting and static analyses are mutually beneficial techniques: program transformations change the intensional aspects of the program, and can thus improve analysis precision, while some efficient transformations are enabled by specific knowledge of some program invariants. Despite the strong interaction between these techniques, they are usually considered distinct. In this paper, we demonstrate that we can turn abstract interpreters into compilers, using a simple free algebra over the standard signature of abstract domains. Functor domains correspond to compiler passes, for which soundness is translated to a proof of forward simulation, and completeness to backward simulation. We achieve translation to SSA using an abstract domain with a non-standard SSA signature. Incorporating such an SSA translation to an abstract interpreter improves its precision; in particular we show that an SSA-based non-relational domain is always more precise than a standard non-relational domain for similar time and memory complexity. Moreover, such a domain allows recovering from precision losses that occur when analyzing low-level machine code instead of source code. These results help implement analyses or compilation passes where symbolic and semantic methods simultaneously refine each other, and improves precision when compared to doing the passes in sequence.
Floating-Point TVPI Abstract Domain
Authors: Rivera Joao , Franchetti Franz , Püschel Markus
Published: June 2024

Floating-point arithmetic is natively supported in hardware and the preferred choice when implementing numerical software in scientific or engineering applications. However, such programs are notoriously hard to analyze due to round-off errors and the frequent use of elementary functions such as log, arctan, or sqrt.

In this work, we present the Two Variables per Inequality Floating-Point (TVPI-FP) domain, a numerical and constraint-based abstract domain designed for the analysis of floating-point programs. TVPI-FP supports all features of real-world floating-point programs including conditional branches, loops, and elementary functions and it is efficient asymptotically and in practice. Thus it overcomes limitations of prior tools that often are restricted to straight-line programs or require the use of expensive solvers. The key idea is the consistent use of interval arithmetic in inequalities and an associated redesign of all operators. Our extensive experiments show that TVPI-FP is often orders of magnitudes faster than more expressive tools at competitive, or better precision while also providing broader support for realistic programs with loops and conditionals.
NetBlocks: Staging Layouts for High-Performance Custom Host Network Stacks
Authors: Brahmakshatriya Ajay , Rinard Chris , Ghobadi Manya , Amarasinghe Saman
Published: June 2024

Modern network applications and environments, ranging from data centers and IoT devices to AR/VR headsets and underwater robotics, present diverse requirements that cannot be satisfied by the all or-nothing approach of TCP and UDP protocols. Network researchers and engineers need to create highly tailored protocols targeting individual problem domains. Existing library-based approaches either fall short on the flexibility in features or offer them at a significant performance overhead. To address this challenge, we present NetBlocks, a domain-specific language, and compiler for designing ad-hoc protocols and generating their highly optimized host network stack implementations. NetBlocks DSL input allows users to configure protocols by selecting and customizing features. Unlike other DSL compilers, NetBlocks also allows network researchers to extend the system and add more features easily without any prior compiler knowledge. Our design and implementation employ a high-performance Aspect-Oriented Programming framework written with the staging framework BuildIt. We also introduce a novel Layout Customization Layer that allows "staging packet layouts" alongside the implementation, which is critical for getting the best performance out of the protocol when possible, while allowing the practitioners to maintain compatibility with existing protocol layers where needed. Our evaluations on three applications ranging across deployments in data centers and underwater acoustic networks demonstrate a trade-off between performance (both latency and throughput) and selected features allowing the user to only pay-for what-they-use.
The Functional Essence of Imperative Binary Search Trees
Authors: Lorenzen Anton , Leijen Daan , Swierstra Wouter , Lindley Sam
Published: June 2024

Algorithms on restructuring binary search trees are typically

presented in imperative pseudocode. Understandably so, as their

performance relies on in-place execution, rather than the repeated

allocation of fresh nodes in memory. Unfortunately, these imperative

algorithms are notoriously difficult to verify as their loop

invariants must relate the unfinished tree fragments being

rebalanced. This paper presents several novel functional algorithms

for accessing and inserting elements in a restructuring binary search

tree that are as fast as their imperative counterparts; yet the

correctness of these functional algorithms is established using a

simple inductive argument. For each data structure, move-to-root,

splay, and zip trees, this paper describes both a bottom-up

algorithm using zippers and a top-down algorithm using a novel

first-class constructor context primitive.

The functional and imperative algorithms are equivalent:

we mechanise the proofs establishing this in the Coq

proof assistant using the Iris framework. This yields a first fully

verified implementation of well known algorithms on binary search trees with

performance on par with the fastest implementations in C.
Daedalus: Safer Document Parsing
Authors: Diatchki Iavor S. , Dodds Mike , Goldstein Harrison , Harris Bill , Holland David A. , Razet Benoit , Schlesinger Cole , Winwood Simon
Published: June 2024

Despite decades of contributions to the theoretical foundations of parsing and the many tools available to aid

in parser development, many security attacks in the wild still exploit parsers. The issues are myriad—flaws

in memory management in contexts lacking memory safety, flaws in syntactic or semantic validation of

input, and misinterpretation of hundred-page-plus standards documents. It remains challenging to build and

maintain parsers for common, mature data formats.

In response to these challenges, we present Daedalus, a new domain-specific language (DSL) and toolchain

for writing safe parsers. Daedalus is built around functional-style parser combinators, which suit the rich data

dependencies often found in complex data formats. It adds domain-specific constructs for stream manipulation,

allowing the natural expression of parsing noncontiguous formats. Balancing between expressivity and

domain-specific constructs lends Daedalus specifications simplicity and leaves them amenable to analysis. As

a stand-alone DSL, Daedalus is able to generate safe parsers in multiple languages, currently C++ and Haskell.

We have implemented 20 data formats with Daedalus, including two large, complex formats—PDF and

NITF—and our evaluation shows that Daedalus parsers are concise and performant. Our experience with PDF

forms our largest case study. We worked with the PDF Association to build a reference implementation, which

was subject to a red-teaming exercise along with a number of other PDF parsers and was the only parser to be

found free of defects.
Descend: A Safe GPU Systems Programming Language
Authors: Köpcke Bastian , Gorlatch Sergei , Steuwer Michel
Published: June 2024

Graphics Processing Units (GPU) offer tremendous computational power by following a throughput oriented paradigm where many thousand computational units operate in parallel. Programming such massively parallel hardware is challenging. Programmers must correctly and efficiently coordinate thousands of threads and their accesses to various shared memory spaces. Existing mainstream GPU programming languages, such as CUDA and OpenCL, are based on C/C++ inheriting their fundamentally unsafe ways to access memory via raw pointers. This facilitates easy to make, but hard to detect bugs, such as
data races
and
deadlocks
.

In this paper, we present
Descend
: a safe GPU programming language. In contrast to prior safe high-level GPU programming approaches,
Descend
is an imperative GPU
systems programming language
in the spirit of Rust, enforcing safe CPU and GPU memory management in the type system by tracking
Ownership
and
Lifetimes
.
Descend
introduces a new
holistic GPU programming
model where computations are hierarchically scheduled over the GPU’s
execution resources
: grid, blocks, warps, and threads.
Descend
’s extended
Borrow
checking ensures that execution resources safely access memory regions without data races. For this, we introduced
views
describing safe parallel access patterns of memory regions, as well as
atomic
variables. For memory accesses that can’t be checked by our type system, users can annotate limited code sections as
unsafe
.

We discuss the memory safety guarantees offered by
Descend
and evaluate our implementation using multiple benchmarks, demonstrating that
Descend
is capable of expressing real-world GPU programs showing competitive performance compared to manually written CUDA programs lacking
Descend
’s safety guarantees.
Bit Blasting Probabilistic Programs
Authors: Garg Poorva , Holtzen Steven , Van den Broeck Guy , Millstein Todd
Published: June 2024

Probabilistic programming languages (PPLs) are an expressive means for creating and reasoning about probabilistic models. Unfortunately
hybrid
probabilistic programs that involve both continuous and discrete structures are not well supported by today’s PPLs. In this paper we develop a new approximate inference algorithm for hybrid probabilistic programs that first discretizes the continuous distributions and then performs discrete inference on the resulting program. The key novelty is a form of discretization that we call
bit blasting
, which uses a binary representation of numbers such that a domain of 2

b

discretized points can be succinctly represented as a discrete probabilistic program over
poly
(
b
) Boolean random variables. Surprisingly, we prove that many common continuous distributions can be bit blasted in a manner that incurs no loss of accuracy over an explicit discretization and supports efficient probabilistic inference. We have built a probabilistic programming system for hybrid programs called HyBit, which employs bit blasting followed by discrete probabilistic inference. We empirically demonstrate the benefits of our approach over existing sampling-based and symbolic inference approaches.
Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis
Authors: Ji Ruyi , Zhao Yuwei , Polikarpova Nadia , Xiong Yingfei , Hu Zhenjiang
Published: June 2024

Intermediate data structures are a common cause of inefficiency in functional programming.
Fusion
attempts to eliminate intermediate data structures by combining adjacent data traversals into one; existing fusion techniques, however, are based on predefined rewrite rules and hence are limited in expressiveness.

In this work we explore a different approach to eliminating intermediate data structures, based on inductive program synthesis. We dub this approach
superfusion
(by analogy with
superoptimization
, which uses inductive synthesis for program optimization). Starting from a reference program annotated with data structures to be eliminated, superfusion first generates a
sketch
where program fragments operating on those data structures are replaced with holes; it then fills the holes with constant-time expressions such that the resulting program is equivalent to the reference. The main technical challenge here is scalability because optimized programs are often complex, making the search space intractably large for naive enumeration. To address this challenge, our key insight is to first synthesize a
ghost function
that describes the relationship between the original intermediate data structure and its compressed version; this function, although not used in the final program, serves to decompose the joint sketch filling problem into independent simpler problems for each hole.

We implement superfusion in a tool called SuFu and evaluate it on a dataset of 290 tasks collected from prior work on deductive fusion and program restructuring. The results show that SuFu solves 264 out of 290 tasks, exceeding the capabilities of rewriting-based fusion systems and achieving comparable performance with specialized approaches to program restructuring on their respective domains.
LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
Authors: Qiu Longfei , Kim Yoonseung , Shin Ji-Yong , Kim Jieung , Honoré Wolf , Shao Zhong
Published: June 2024

Byzantine fault-tolerant state machine replication (SMR) protocols, such as PBFT, HotStuff, and Jolteon, are essential for modern blockchain technologies. However, they are challenging to implement correctly because they have to deal with any unexpected message from byzantine peers and ensure safety and liveness at all times. Many formal frameworks have been developed to verify the safety of SMR implementations, but there is still a gap in the verification of their liveness. Existing liveness proofs are either limited to the network level or do not cover popular partially synchronous protocols.

We introduce LiDO, a consensus model that enables the verification of both safety and liveness of implementations through refinement. We observe that current consensus models cannot handle liveness because they do not include a pacemaker state. We show that by adding a pacemaker state to the LiDO model, we can express the liveness properties of SMR protocols as a few safety properties that can be easily verified by refinement proofs. Based on our LiDO model, we provide mechanized safety and liveness proofs for both unpipelined and pipelined Jolteon in Coq. This is the first mechanized liveness proof for a byzantine consensus protocol with non-trivial optimizations such as pipelining.
Compilation of Modular and General Sparse Workspaces
Authors: Zhang Genghan , Hsu Olivia , Kjolstad Fredrik
Published: June 2024

Recent years have seen considerable work on compiling sparse tensor algebra expressions. This paper addresses a shortcoming in that work, namely how to generate efficient code (in time and space) that scatters values into a sparse result tensor. We address this shortcoming through a compiler design that generates code that uses sparse intermediate tensors (sparse workspaces) as efficient adapters between compute code that scatters and result tensors that do not support random insertion. Our compiler automatically detects sparse scattering behavior in tensor expressions and inserts necessary intermediate workspace tensors. We present an algorithm template for workspace insertion that is the backbone of our code generation algorithm. Our algorithm template is modular by design, supporting sparse workspaces that span multiple user-defined implementations. Our evaluation shows that sparse workspaces can be up to 27.12× faster than the dense workspaces of prior work. On the other hand, dense workspaces can be up to 7.58× faster than the sparse workspaces generated by our compiler in other situations, which motivates our compiler design that supports both. Our compiler produces sequential code that is competitive with hand-optimized linear and tensor algebra libraries on the expressions they support, but that generalizes to any other expression. Sparse workspaces are also more memory efficient than dense workspaces as they compress away zeros. This compression can asymptotically decrease memory usage, enabling tensor computations on data that would otherwise run out of memory.
Linear Matching of JavaScript Regular Expressions
Authors: Barrière Aurèle , Pit-Claudel Clément
Published: June 2024

Modern regex languages have strayed far from well-understood
traditional regular expressions: they include features that
fundamentally transform the matching problem. In exchange for these
features, modern regex engines at times suffer from exponential
complexity blowups, a frequent source of denial-of-service
vulnerabilities in JavaScript applications. Worse, regex semantics
differ across languages, and the impact of these divergences on
algorithmic design and worst-case matching complexity has seldom been
investigated.

This paper provides a novel perspective on JavaScript's regex
semantics by identifying a larger-than-previously-understood subset of
the language that can be matched with linear time guarantees. In the
process, we discover several cases where state-of-the-art algorithms
were either wrong (semantically incorrect), inefficient (suffering
from superlinear complexity) or excessively restrictive (assuming
certain features could not be matched linearly). We introduce novel
algorithms to restore correctness and linear complexity. We further
advance the state-of-the-art in linear regex matching by presenting
the first nonbacktracking algorithms for matching lookarounds in
linear time: one supporting captureless lookbehinds in any regex
language, and another leveraging a JavaScript property to support
unrestricted lookaheads and lookbehinds. Finally, we describe new
time and space complexity tradeoffs for regex engines. All of our
algorithms are practical: we validated them in a prototype
implementation, and some have also been merged in the V8 JavaScript
implementation used in Chrome and Node.js.
Live Verification in an Interactive Proof Assistant
Authors: Gruetter Samuel , Fukala Viktor , Chlipala Adam
Published: June 2024

We present a prototype for a tool that enables programmers to verify their code as they write it in real-time.

After each line of code that the programmer writes, the tool tells the programmer whether it was able to prove absence of undefined behavior so far, and it displays a concise representation of the symbolic state of the program right after the added line.

The user can then either write the next line of code, or if needed or desired, write a specially marked comment that provides hints on how to solve side conditions or on how to represent the symbolic state more nicely.

Once the programmer has finished writing the program, it is already verified with a mathematical correctness proof.

Other tools providing real-time feedback already exist, but ours is the first one that only relies on a small trusted proof checker and that provides a concise summary of the symbolic state at the point in the program currently being edited, as opposed to only indicating whether user-stated assertions or postconditions hold.

Program verification requires loop invariants, which are hard to find and tedious to spell out.

We explore a middle ground in the design space between the two extremes of requiring users to spell out loop invariants manually and attempting to infer loop invariants automatically:

Since a loop invariant often looks quite similar to the symbolic state right before the loop, our tool asks the user to express the desired loop invariant as a diff from the symbolic state before the loop, which has the potential to lead to shorter, more maintainable proofs.

We prototyped our technique in the interactive proof assistant Coq, so our framework creates machine-checked proofs that the developed functions satisfy their specifications when executed according to the formal semantics of the source language.

Using a verified compiler proven against the same source-language semantics, we can ensure that the behavior of the compiled program matches the program's behavior as represented by the framework during the proof.

Additionally, since our polyglot source files can be viewed as Coq or C files at the same time, users willing to accept a larger trusted code base can compile them with GCC.
Falcon: A Scalable Analytical Cache Model
Authors: Pitchanathan Arjun , Grover Kunwar , Grosser Tobias
Published: June 2024

Compilers often use performance models to decide how to optimize code. This is often preferred over using hardware performance measurements, since hardware measurements can be expensive, limited by hardware availability, and makes the output of compilation non-deterministic. Analytical models, on the other hand, serve as efficient and noise-free performance indicators. Since many optimizations focus on improving memory performance, memory cache miss rate estimations can serve as an effective and noise-free performance indicator for superoptimizers, worst-case execution time analyses, manual program optimization, and many other performance-focused use cases. Existing methods to model the cache behavior of affine programs work on small programs such as those in the Polybench benchmark but do not scale to the larger programs we would like to optimize in production, which can be orders of magnitude bigger by lines of code. These analytical approaches hand of the whole program to a Presburger solver and perform expensive mathematical operations on the huge resulting formulas. We develop a scalable cache model for affine programs that splits the computation into smaller pieces that do not trigger the worst-case asymptotic behavior of these solvers. We evaluate our approach on 46 TorchVision neural networks, finding that our model has a geomean runtime of 44.9 seconds compared to over 32 minutes for the state-of-the-art prior cache model, and the latter is actually smaller than the true value because the prior model reached our four hour time limit on 54% of the networks, and this limit was never reached by our tool. Our model exploits parallelism effectively: running it on sixteen cores is 8.2x faster than running it single-threaded. While the state-of-the-art model takes over four hours to analyze a majority of the benchmark programs, Falcon produces results in at most 3 minutes and 3 seconds; moreover, after a local modification to the program being analyzed, our model efficiently updates the predictions in 513 ms on average (geomean). Thus, we provide the first scalable analytical cache model.
Numerical Fuzz: A Type System for Rounding Error Analysis
Authors: Kellison Ariel E. , Hsu Justin
Published: June 2024

Algorithms operating on real numbers are implemented as floating-point computations in practice, but floating-point operations introduce
roundoff errors
that can degrade the accuracy of the result. We propose Λ

num

, a functional programming language with a type system that can express quantitative bounds on roundoff error. Our type system combines a sensitivity analysis, enforced through a linear typing discipline, with a novel graded monad to track the accumulation of roundoff errors. We prove that our type system is sound by relating the denotational semantics of our language to the exact and floating-point operational semantics.

To demonstrate our system, we instantiate Λ

num

with error metrics proposed in the numerical analysis literature and we show how to incorporate rounding operations that faithfully model aspects of the IEEE 754 floating-point standard. To show that Λ

num

can be a useful tool for automated error analysis, we develop a prototype implementation for Λ

num

that infers error bounds that are competitive with existing tools, while often running significantly faster. Finally, we consider semantic extensions of our graded monad to bound error under more complex rounding behaviors, such as non-deterministic and randomized rounding.
Inductive Approach to Spacer
Authors: Tsukada Takeshi , Unno Hiroshi
Published: June 2024

The constrained Horn clause satisfiability problem is at the core of many automated verification methods, and Spacer is one of the most efficient solvers of this problem. The standard description of Spacer is based on an abstract transition system, dividing the whole procedure into small rules. This division makes individual rules easier to understand but, conversely, makes it difficult to discuss the procedure as a whole. As evidence of the difficulty in understanding the whole procedure, we point out that the claimed refutational completeness actually fails for several reasons, some of which were not present in the original version and subsequently added. It is also difficult to grasp the differences between Spacer and another procedure, such as GPDR.
This paper aims to provide a better understanding of Spacer by developing a Spacer-like procedure defined by structural induction. We first formulate the problem to be solved inductively, then give its naïve solver and transform it to obtain a Spacer-like procedure. Interestingly, our inductive approach almost unifies Spacer and GPDR, which differ in only one respect in our understanding. To demonstrate the usefulness of our inductive approach in understanding Spacer, we examine Spacer variants in the literature in terms of inductive procedures and discuss why they are not refutationally complete and how to fix them. We also implemented the proposed procedure and evaluated it experimentally.
V-Star: Learning Visibly Pushdown Grammars from Program Inputs
Authors: Jia Xiaodong , Tan Gang
Published: June 2024

Accurate description of program inputs remains a critical challenge in the field of programming languages. Active learning, as a well-established field, achieves exact learning for regular languages. We offer an innovative grammar inference tool, V-Star, based on the active learning of visibly pushdown automata. V-Star deduces nesting structures of program input languages from sample inputs, employing a novel inference mechanism based on nested patterns. This mechanism identifies token boundaries and converts languages such as XML documents into VPLs. We then adapted Angluin's L-Star, an exact learning algorithm, for VPA learning, which improves the precision of our tool. Our evaluation demonstrates that V-Star effectively and efficiently learns a variety of practical grammars, including S-Expressions, JSON, and XML, and outperforms other state-of-the-art tools.
Equivalence and Similarity Refutation for Probabilistic Programs
Authors: Chatterjee Krishnendu , Goharshady Ehsan Kafshdar , Novotný Petr , Žikelić Đorđe
Published: June 2024

We consider the problems of statically refuting equivalence and similarity of output distributions defined by a pair of probabilistic programs. Equivalence and similarity are two fundamental relational properties of probabilistic programs that are essential for their correctness both in implementation and in compilation. In this work, we present a new method for static equivalence and similarity refutation. Our method refutes equivalence and similarity by computing a function over program outputs whose expected value with respect to the output distributions of two programs is different. The function is computed simultaneously with an upper expectation supermartingale and a lower expectation submartingale for the two programs, which we show to together provide a formal certificate for refuting equivalence and similarity. To the best of our knowledge, our method is the first approach to relational program analysis to offer the combination of the following desirable features: (1) it is fully automated, (2) it is applicable to infinite-state probabilistic programs, and (3) it provides formal guarantees on the correctness of its results. We implement a prototype of our method and our experiments demonstrate the effectiveness of our method to refute equivalence and similarity for a number of examples collected from the literature.
Dead Man’s PLC: Towards Viable Cyber Extortion for Operational Technology
Authors: Derbyshire Richard , Green Benjamin , van der Walt Charl , Hutchison David
Published: June 2024

For decades, operational technology (OT) has enjoyed the luxury of being suitably inaccessible, and thus has experienced directly targeted cyber attacks from only the most advanced and well-resourced adversaries. However, security via obscurity cannot last forever, and indeed a shift is happening whereby less advanced adversaries are showing an appetite for targeting OT. With this shift in adversary demographics, there will likely also be a shift in attack goals, from clandestine process degradation and espionage to overt cyber extortion (Cy-X). Even if encryption-based Cy-X techniques were launched against OT assets, typical recovery practices designed for engineering processes would provide adequate resilience. In response, this article introduces Dead Man’s PLC (DM-PLC), a pragmatic step towards viable OT Cy-X that acknowledges and weaponises the resilience processes typically encountered in any OT environment. Using only existing functionality, DM-PLC considers an entire environment as the entity under ransom, whereby all assets constantly send one another heartbeats to ensure the attack remains untampered with, treating any deviations as a detonation trigger akin to a DM switch. A proof of concept of DM-PLC is implemented and evaluated on a peer reviewed and industry validated OT testbed to demonstrate its malicious potential.
Categorical and Continuous Features in Counterfactual Explanations of AI Systems
Authors: Warren Greta , Byrne Ruth M. J. , Keane Mark T.
Published: June 2024

Recently, eXplainable AI (XAI) research has focused on the use of counterfactual explanations to address interpretability, algorithmic recourse, and bias in AI system decision-making. The developers of these algorithms claim they meet user requirements in generating counterfactual explanations with “plausible,” “actionable” or “causally important” features. However, few of these claims have been tested in controlled psychological studies. Hence, we know very little about which aspects of counterfactual explanations really help users understand the decisions of AI systems. Nor do we know whether counterfactual explanations are an advance on more traditional causal explanations that have a longer history in AI (e.g., in expert systems). Accordingly, we carried out three user studies to (1) test a fundamental distinction in feature-types, between categorical and continuous features, and (2) compare the relative effectiveness of counterfactual and causal explanations. The studies used a simulated, automated decision-making app that determined safe driving limits after drinking alcohol, based on predicted blood alcohol content, where users’ responses were measured objectively (using predictive accuracy) and subjectively (using satisfaction and trust judgments). Study 1 (
N

\({=}\)

127) showed that users understand explanations referring to categorical features more readily than those referring to continuous features. It also discovered a dissociation between objective and subjective measures: counterfactual explanations elicited higher accuracy than no-explanation controls but elicited no more accuracy than causal explanations, yet counterfactual explanations elicited greater satisfaction and trust than causal explanations. In Study 2 (
N

\({=}\)

136) we transformed the continuous features of presented items to be categorical (i.e., binary) and found that these converted features led to highly accurate responding. Study 3 (
N

\({=}\)

211) explicitly compared matched items involving either mixed features (i.e., a mix of categorical and continuous features) or categorical features (i.e., categorical and categorically-transformed continuous features), and found that users were more accurate when categorically-transformed features were used instead of continuous ones. It also replicated the dissociation between objective and subjective effects of explanations. The findings delineate important boundary conditions for current and future counterfactual explanation methods in XAI.
LiVeR: Lightweight Vehicle Detection and Classification in Real-Time
Authors: Shekhar Chandra , Debadarshini Jagnyashini , Saha Sudipta
Published: June 2024

Detection of vehicles and their classification is a significant component of wide-area monitoring and surveillance, as well as
intelligent- transportation
. Existing solutions tend to employ heavy-weight infrastructure and costly equipment, as well as largely depend on constant support from the cloud through round-the-clock internet connectivity and uninterrupted power supply. Moreover, existing works mainly concentrate on localized measurement and do not discuss their efficient integration to address the problem over a wide area. For practical use in an outdoor environment, apart from being technically sound and accurate, a solution also needs to be
cost-effective
,
lightweight
,
easy to install
,
flexible
,
low overhead
, and
easily maintainable
, as well as
self-sufficient
as much as possible. However, fulfilling all these goals together is a challenging task. In this work, we propose an IoT-assisted strategy,
LiVeR
, to accomplish it. For self-sufficient on-the-fly classification in resource-constrained low-power IoT devices, LiVeR minimizes not only the computational requirements but also the energy consumption, which enables sustained operation in a hostile outdoor environment for a considerably long time solely based on battery power. Through extensive studies based on outdoor measurement and trace-based simulation on empirical data, we demonstrate that LiVeR classifies vehicles of small, medium, and large size with an accuracy of 91.3% up to 98.8%, 92.3% up to 98.5%, and 93.8% up to 98.8%, respectively, for single-lane traffic. We also demonstrate that LiVeR spends only about one-third of the number of RF packets to achieve vehicle detection and classification compared to the state-of-the-art RF-based solution, considerably extending the lifetime of the system.
Osteoporosis Failure of Aluminum Current Collector Induced Crosstalk Degradation at the Imide-Type Lithium Salt Comprised Practical-Level Lithium-Ion Batteries
Authors: Byun Jooeun , Kim Wontak , Lee Min A , Yu Ji-Sang , Choi Jiyoung , Yun Jong-Cheol , Cho Woosuk , Mun Junyoung , Kim Hyun-Seung
Published: June 2024

The atypical failure mechanism caused by the inclusion of lithium bis(fluorosulfonyl)imide (LiFSI) salt in lithium-ion batteries (LIB) is elucidated. When subjected to elevated temperature cycling, the LiFSI salt triggers the degradation of the aluminum current collector, leading to the dissolution of Al ions into the electrolyte. These dissolved Al ions then migrate toward the negative electrode surface where they spontaneously reduce and form Al deposits due to the low electrode potential. This Al deposition further catalyzes the cathodic decomposition of the electrolyte, impacting the interphasial resistance of the negative electrode and consuming both Li ions and electrolyte components. Upon extended cycling with LiFSI-containing electrolytes, a notable decline in the reversible capacity of LIB becomes evident due to cross-talk failure resulting from Al current collector corrosion. Consequently, to enhance the cycling performance of LIBs using LiFSI-based electrolytes, it is necessary to simultaneously prevent Al corrosion and subsequent deposition on the surface of the negative electrode.
Electrodeposition of Beta-Tantalum in Alkali Metal Halides and Oxohalide Melts
Authors: Kuznetsov S. A.
Published: June 2024

Data on the electrolytic preparation of β-Ta in halide and oxohalide melts were reported. It was shown that during electrolysis in halide melts containing K2TaF7, the amount β-Ta in the cathodic products can be markedly increased by using a copper cathode with a definite texture. It was found that in chloride-oxofluoride melts the β-Ta content increases monotonically on passing from NaCl to KCl and RbCl melt. The dependencies of the β-Ta content in cathodic products on the ratio of oxygen to tantalum concentrations were studied in chloride-oxofluoride and fluoride-oxofluoride melts. The maxima of these dependences were identified and explained. It was shown that β-Ta could be obtained by electrolysis in molten salts only at temperatures below 850 °C.
Ulk1 phosphorylation at S555 is not required for endurance training-induced improvements in exercise and metabolic capacity in mice
Authors: Guan Yuntian , Spaulding Hannah , Yu Qing , Zhang Mei , Willoughby Orion , Drake Joshua C. , Yan Zhen
Published: June 2024

We have used CRISPR/Cas9-mediated gene editing to generate Ulk1-S555A knock-in mice to show that loss of phosphorylation of Ulk1 at S555 blunted exercise-induced mitophagy and mildly impairs energy metabolism during exercise in healthy mice. However, the knock-in mice retained exercise training-mediated improvements of endurance capacity and energy metabolism during exercise. These findings suggest that exercise-induced mitophagy through Ulk1 activation is not required for the metabolic adaptation and improved exercise capacity in young, healthy mice.
Atorvastatin Attenuates Endothelial Cell Injury in Atherosclerosis Through Inhibiting ACSL4‐Mediated Ferroptosis
Authors: Tan Huilian , Liu Ling , Qi Yanchao , Zhang Dahong , Zhi Yanchun , Li Yu , Zhang Huimin , Liu Jun
Published: June 2024

Objective: This study is aimed at investigating the effects of atorvastatin (ATV) on endothelial cell injury in atherosclerosis (AS) through inhibiting acyl‐CoA synthetase long‐chain family member 4 (ACSL4)‐mediated ferroptosis.

Methods: Human umbilical vein endothelial cells (HUVECs) were treated with oxidized low‐density lipoprotein (ox‐LDL) to establish an in vitro model of AS. The cell viability, lactate dehydrogenase (LDH) release, apoptosis, and expression levels of apoptotic proteins were assessed. The levels of inflammatory factors and adhesion molecules were determined by ELISA and Western blot, respectively. Cellular iron content, lipid peroxidation, glutathione (GSH) levels, and lipid reactive oxygen species (ROS) were measured. ACSL4 overexpression was performed to investigate its role in ATV‐mediated protection against ferroptosis.

Results: ATV alleviated ox‐LDL‐induced HUVEC damage by restoring cell viability, reducing LDH levels, and inhibiting apoptosis. It also attenuated inflammation and adhesion by decreasing the levels of inflammatory factors TNF‐α, IL‐6, and IL‐8, as well as adhesion molecules ICAM‐1 and VCAM‐1. ATV inhibited ferroptosis by regulating iron content, malondialdehyde (MDA) levels, ROS levels, and ACSL4 protein expression. Overexpression of ACSL4 (oe‐ACSL4) hindered the protective effects of ATV on cell viability, antiapoptotic protein expression, LDH levels, apoptosis, and inflammatory factors.

Conclusion: Our findings suggest that ATV attenuates endothelial cell injury in AS by inhibiting ACSL4‐mediated ferroptosis. These results provide insights into the potential therapeutic strategies for the treatment of AS.
Interaction of Glycemic Control and Statin Use on Diabetes‐Tuberculosis Treatment Outcome: A Nested Case‐Control Study
Authors: Meng Xiangrui , Zheng Huiqiu , Du Jian , Wang Xuemei , Wang Yanling , Hu Jing , Zhao Jing , Du Qianqian , Gao Yulong
Published: June 2024

This study aims to explore the interaction of glycemic control and statin use on the treatment outcomes of pulmonary tuberculosis‐diabetes comorbidity (PTB‐DM) patients. A nested case‐control study was conducted in a tuberculosis patients’ cohort. We defined cases as patients who experienced unfavorable outcomes. Glycemic control was estimated at the baseline. Statin use was obtained from medical records. The multivariate logistic regression models were developed, and the interaction table invented by Andersson was adopted to analyze the interaction of glycemic control and statin use on treatment outcomes. A total of 2,047 patients were included in this study. There was a significant interaction between glycemic control and statin use on the treatment outcomes. Patients with good glycemic control and no statin use (OR = 0.464, 95% CI: 0.360–0.623) had a lower risk of unfavorable outcomes than those with poor glycemic control and statin use (OR = 0.604, 95% CI: 0.401–0.734). Patients with good glycemic control and statin use had the lowest risk of unfavorable outcomes (OR = 0.394, 95% CI: 0.264–0.521). Glycemic control in diabetes‐tuberculosis treatment should be paid considerable attention. Patients can benefit from statin use even if they have poor glycemic control. Patients with good glycemic control and statin use can have the best outcomes.
Ibrutinib in Combination with R-GemOx in Patients with Relapsed or Refractory Diffuse Large B-cell Lymphoma of Nongerminal Center B-cell–like Type: Phase II Clinical Trial of the Spanish GELTAMO Group
Authors: Rey-Búa Beatriz , Grande Carlos , Sánchez Blanco José J. , Abrisqueta Pau , Gutiérrez Antonio , Ramírez Páyer Ángel , Giné Eva , Zeberio Etxetxipia Izaskun , Terol Maria J. , de la Cruz Vicente Fátima , Andreu Rafel , Ramirez Maria J. , de la Fuente Adolfo , Viguria Maria C. , Peñarrubia María J. , Jiménez-Ubieto Ana , Montes-Moreno Santiago , López-Guillermo Armando , Caballero María D. , Martín García-Sancho Alejandro
Published: June 2024

Purpose:

This phase II clinical trial evaluated the combination of ibrutinib with rituximab, gemcitabine, and oxaliplatin (R-GemOx) in patients with nongerminal center B-cell–like (non-GCB) diffuse large B-cell lymphoma (DLBCL).

Patients and Methods:

The IBDCL trial (NCT02692248) included patients with histologic diagnosis of non-GCB DLBCL with relapsed or refractory disease and non-candidates for stem-cell transplantation. Patients received an induction treatment consisting of six or eight cycles of R-GemOx at standard doses every 2 weeks, in combination with ibrutinib (560 mg daily), followed by a maintenance treatment with ibrutinib for a maximum of 2 years. The primary objective was to evaluate the overall response rate after four cycles.

Results:

Sixty-four patients were included, 72% of them refractory to the last regimen. The overall response rate and complete remission rate after the fourth cycle were 53% [95% confidence interval (CI), 41–65] and 34% (95% CI, 24–46), respectively. Twenty-four (37%) patients started maintenance, and 7 (11%) completed the planned 2 years. After a median follow-up of 29.7 months (range: 0.4–48.6), the estimated 2-year progression-free survival and overall survival were 18% (95% CI, 8–28) and 26% (95% CI, 14–37), respectively. The most common grade ≥3 treatment-related adverse events were thrombocytopenia (44%), neutropenia (30%), and anemia (14%). Grade ≥3 infectious and cardiovascular treatment-related adverse events were reported in 6 (9%) and 1 (2%) patient, respectively.

Conclusions:

Ibrutinib in combination with R-GemOx, followed by ibrutinib maintenance, demonstrated encouraging antitumor activity with durable responses and a manageable toxicity in patients with non-GCB DLBCL.
Supplementary Figure 16 from Ultrasensitive Detection of Circulating LINE-1 ORF1p as a Specific Multicancer Biomarker
Authors: Taylor Martin S. , Wu Connie , Fridy Peter C. , Zhang Stephanie J. , Senussi Yasmeen , Wolters Justina C. , Cajuso Tatiana , Cheng Wen-Chih , Heaps John D. , Miller Bryant D. , Mori Kei , Cohen Limor , Jiang Hua , Molloy Kelly R. , Chait Brian T. , Goggins Michael G. , Bhan Irun , Franses Joseph W. , Yang Xiaoyu , Taplin Mary-Ellen , Wang Xinan , Christiani David C. , Johnson Bruce E. , Meyerson Matthew , Uppaluri Ravindra , Egloff Ann Marie , Denault Elyssa N. , Spring Laura M. , Wang Tian-Li , Shih Ie-Ming , Fairman Jennifer E. , Jung Euihye , Arora Kshitij S. , Yilmaz Osman H. , Cohen Sonia , Sharova Tatyana , Chi Gary , Norden Bryanna L. , Song Yuhui , Nieman Linda T. , Pappas Leontios , Parikh Aparna R. , Strickland Matthew R. , Corcoran Ryan B. , Mustelin Tomas , Eng George , Yilmaz Ömer H. , Matulonis Ursula A. , Chan Andrew T. , Skates Steven J. , Rueda Bo R. , Drapkin Ronny , Klempner Samuel J. , Deshpande Vikram , Ting David T. , Rout Michael P. , LaCava John , Walt David R. , Burns Kathleen H.
Published: June 2024

Screening of multimeric nanobodies for ORF1p detection with Simoa.
KARAKTERISTIK PASIEN DAN LUARAN FEMTO LASIK DI PMN RS MATA CICENDO
Authors: Budiman  , Knoch Andrew Maximilian Herman , Siagian Helena Margareth Angelica
Published: June 2024

Background: Refractive error ranks first among all other types of eye. However, there is currently no new research in Indonesia on the epidemiology of the most recent myopia patients or the results of Femto LASIK, which is one of the well-known refractive error remedies that the public is choosing these days. This study aimed to describe the characteristics and outcomes of patients who underwent Femto LASIK at the Cicendo National Eye Hospital throughout 2022. 
Methods: A retrospective descriptive study was conducted using medical records of patients who underwent Femto LASIK surgery in 2022. Gender, age, level of education, place of residence, eye lateralization, motives for surgery, presenting visual acuity, best corrected visual acuity, degree of myopia, and refractive error correction were reviewed. 
Results: A total of 209 patients were selected. The majority of the subjects were male (67,5%) with age ranging from 18 to 48 years. Most patients were high school graduates (84,2%) and resided in Java Island (48,8%). The surgery was predominantly performed on both eyes (88%) due to career requirements (60,3%) and for the correction of mild myopia (44,8%). Most patients presenting visual acuity were severe visual impairment (40,4%). After LASIK, there were residual refractive errors for all degrees of myopia. The efficacy and safety index were highest among cases of mild myopia. 
Conclusion: The study's conclusions showed that male residents of Java were the patients' most prevalent characteristics. Femto LASIK has proven to be highly effective and safe, particularly in cases of low myopia.
A idade da terra em Paraty - Uma proposta de periodização histórica
Authors: Gusmão Neusa Maria Mendes de
Published: June 2024

The aim of this paper is to call attention of historians and other scholars to Paraty, a now highly disturbed region of the State of Rio de Janeiro. The economic and social course of the area shows that its past and present are a result of the expansion of Brazilian capitalism in different moments. At first, as a commercial entrepôt, Paraty had its roads intensively used, a sign of the process of irradiation of the mercantile capital and its interests. The decline of the export economies (Minas and Vale do Paraíba) resulted in the suspension of these fluxes, resulting in the economic and social disarticulation of the region. During the fifties of the XXth century, local society and economy revived due to the development of new interests, again alien to the region, which activated the old roads, as well as the building of a new one, the Rio-Santos highway. To each moment of the described process corresponds a specific form of land and local labor appropriation and use, through mechanisms of valorization and devaluation of these fundamental goods, i.e., land and labor.
O dote na sociedade paulista do século XIX: legislação e evidências
Authors: Samara Eni de Mesquita
Published: June 2024

The purpose of this article is to study the role, function, and variations of the dowry system in the paulista society during the nineteenth century, according to the legislation and historical evidences found in the documents and related with the problem.