bluuebunny/crossref_metadata_2025_split huggingface dataset:
Aspects of cubic nilpotent superfields
Authors: Aldabergenov Yermek , Antoniadis Ignatios , Chatrabhuti Auttakit , Isono Hiroshi 
Published: June 2023

AbstractWe study in more detail the cubic constraints for $${\mathcal N}=1$$

N
=
1

chiral superfields proposed in the earlier work Eur. Phys. J. C 81, 523 (2021), which describe low-energy goldstino-axion dynamics in global non-linearly realized supersymmetry. We generalize the constraint (i) by gauging the abelian symmetry that shifts the axion, and (ii) to supergravity. In the former case we show that after adding the abelian gauge multiplet, the construction can be formulated as a cubic nilpotent massive vector superfield. In the latter case we find explicit solution to the constraint including contributions from the supergravity multiplet. We also propose microscopic supergravity models (with linear supersymmetry), including a toy model for the string dilaton, which give rise to the cubic constraints at low energies.
Dielectric Properties of a Phenanthrene-Like Nanoisland B14A10: Monte Carlo Study
Authors: Fadil Z. , Raorane Chaitany Jayprakash , Fdil R.-El , Kim Seong Cheol 
Published: June 2023

The dielectric properties of a monolayer phenanthrene-like nanoisland of formula B[Formula: see text]A[Formula: see text] are examined in this research using Monte Carlo simulations. We evaluate the behaviors of the electric hysteresis loops and blocking temperature under the exchange coupling, crystalline field and temperature effects. The multi-loop hysteresis behavior examined in this research may have beneficial applications in nanotechnology and multi-state memory storage. Besides, the results found in the Phenanthrene-like nanoisland are in good agreement with several theoretical and experimental results.
WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly
Authors: Watt Conrad , Trela Maja , Lammich Peter , Märkl Florian 
Published: June 2023

We present WasmRef-Isabelle, a monadic interpreter for WebAssembly written in Isabelle/HOL and proven correct with respect to the WasmCert-Isabelle mechanisation of WebAssembly. WasmRef-Isabelle has been adopted and deployed as a fuzzing oracle in the continuous integration infrastructure of Wasmtime, a widely used WebAssembly implementation. Previous efforts to fuzz Wasmtime against WebAssembly's official OCaml reference interpreter were abandoned by Wasmtime's developers after the reference interpreter exhibited unacceptable performance characteristics, which its maintainers decided not to fix in order to preserve the interpreter's close definitional correspondence with the official specification. With WasmRef-Isabelle, we achieve the best of both worlds - an interpreter fast enough to be useable as a fuzzing oracle that also maintains a close correspondence with the specification through a mechanised proof of correctness.
We verify the correctness of WasmRef-Isabelle through a two-step refinement proof in Isabelle/HOL. We demonstrate that WasmRef-Isabelle significantly outperforms the official reference interpreter, has performance comparable to a Rust debug build of the industry WebAssembly interpreter Wasmi, and competes with unverified oracles on fuzzing throughput when deployed in Wasmtime's fuzzing infrastructure. We also present several new extensions to WasmCert-Isabelle which enhance WasmRef-Isabelle's utility as a fuzzing oracle: we add support for a number of upcoming WebAssembly features, and fully mechanise the numeric semantics of WebAssembly's integer operations.
Performal: Formal Verification of Latency Properties for Distributed Systems
Authors: Zhang Tony Nuda , Sharma Upamanyu , Kapritsos Manos 
Published: June 2023

Understanding and debugging the performance of distributed systems is a notoriously hard task, but a critical one. Traditional techniques like logging, tracing, and benchmarking represent a best-effort way to find performance bugs, but they either require a full deployment to be effective or can only find bugs after they manifest. Even with such techniques in place, real deployments often exhibit performance bugs that cause unwanted behavior.
In this paper, we present Performal, a novel methodology that leverages the recent advances in formal verification to provide rigorous latency guarantees for real, complex distributed systems. The task is not an easy one: it requires carefully decoupling the formal proofs from the execution environment, formally defining latency properties, and proving them on real, distributed implementations. We used Performal to prove rigorous upper bounds for the latency of three applications: a distributed lock, ZooKeeper and a MultiPaxos-based State Machine Replication system. Our experimental evaluation shows that these bounds are a good proxy for the behavior of the deployed system and can be used to identify performance bugs in real-world systems.
Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels
Authors: Bouajjani Ahmed , Enea Constantin , Román-Calvo Enrique 
Published: June 2023

Modern applications, such as social networking systems and e-commerce platforms are centered around using large-scale databases for storing and retrieving data. Accesses to the database are typically enclosed in transactions that allow computations on shared data to be isolated from other concurrent computations and resilient to failures. Modern databases trade isolation for performance. The weaker the isolation level is, the more behaviors a database is allowed to exhibit and it is up to the developer to ensure that their application can tolerate those behaviors.In this work, we propose stateless model checking algorithms for studying correctness of such applications that rely on dynamic partial order reduction. These algorithms work for a number of widely-used weak isolation levels, including Read Committed, Causal Consistency, Snapshot Isolation and Serializability. We show that they are complete, sound and optimal, and run with polynomial memory consumption in all cases. We report on an implementation of these algorithms in the context of Java Pathfinder applied to a number of challenging applications drawn from the literature of distributed systems and databases.
Conflict-Driven Synthesis for Layout Engines
Authors: Liu Junrui , Chen Yanju , Atkinson Eric , Feng Yu , Bodik Rastislav 
Published: June 2023

Modern web browsers rely on layout engines to convert HTML documents to layout trees that specify color, size, and position. However, existing layout engines are notoriously difficult to maintain because of the complexity of web standards. This is especially true for incremental layout engines, which are designed to improve performance by updating only the parts of the layout tree that need to be changed.
In this paper, we propose Medea, a new framework for automatically generating incremental layout engines. Medea separates the specification of the layout engine from its incremental implementation, and guarantees correctness through layout engine synthesis. The synthesis is driven by a new iterative algorithm based on detecting conflicts that prevent optimality of the incremental algorithm.
We evaluated Medea on a fragment of HTML layout that includes challenging features such as margin collapse, floating layout, and absolute positioning. Medea successfully synthesized an incremental layout engine for this fragment. The synthesized layout engine is both correct and efficient. In particular, we demonstrated that it avoids real-world bugs that have been reported in the layout engines of Chrome, Firefox, and Safari. The incremental layout engine synthesized by Medea is up to 1.82× faster than a naive incremental baseline. We also demonstrated that our conflict-driven algorithm produces engines that are 2.74× faster than a baseline without conflict analysis.
Parallelism in a Region Inference Context
Authors: Elsman Martin , Henriksen Troels 
Published: June 2023

Region inference is a type-based program analysis that takes a non-annotated program as input and constructs a program that explicitly manages memory allocation and deallocation by dividing the heap into a stack of regions, each of which can grow and shrink independently from other regions, using constant-time operations.Whereas region-based memory management has shown useful in the contexts of explicit region-based memory management, and in particular, in combination with parallel execution of code, combining region inference with techniques for higher-order parallel programming has not been investigated.In this paper, we present an implementation of a fork-join parallel construct suitable for a compiler based on region inference. We present a minimal higher-order language incorporating the parallel construct, including typing rules and a dynamic semantics for the language, and demonstrate type soundness. We present a novel effect-based region-protection inference algorithm and discuss benefits and shortcomings of the approach. We also describe an efficient implementation embedded in the MLKit Standard ML compiler. Finally, we evaluate the approach and the implementation based on a number of parallel benchmarks, and thereby demonstrate that the technique effectively utilises multi-core architectures in a higher-order functional setting.
Don’t Look UB: Exposing Sanitizer-Eliding Compiler Optimizations
Authors: Isemann Raphael , Giuffrida Cristiano , Bos Herbert , van der Kouwe Erik , Gleissenthall Klaus von 
Published: June 2023

Sanitizers are widely used compiler features that detect undefined behavior and resulting vulnerabilities by injecting runtime checks into programs. For better performance, sanitizers are often used in conjunction with optimization passes. But doing so combines two compiler features with conflicting objectives. While sanitizers want to expose undefined behavior, optimizers often exploit these same properties for performance. In this paper, we show that this clash can have serious consequences: optimizations can remove sanitizer failures, thereby hiding the presence of bugs or even introducing new ones.
We present LookUB, a differential-testing based framework for finding optimizer transformations that elide sanitizer failures. We used our method to find 17 such sanitizer-eliding optimizations in Clang. Next, we used static analysis and fuzzing to search for bugs in open-source projects that were previously hidden due to sanitizer-eliding optimizations. This led us to discover 20 new bugs in Linux Containers, libmpeg2, NTFS-3G, and WINE. Finally, we present an effective mitigation strategy based on a customization of the Clang optimizer with an overhead increase of 4%.
flap: A Deterministic Parser with Fused Lexing
Authors: Yallop Jeremy , Xie Ningning , Krishnaswami Neel 
Published: June 2023

Lexers and parsers are typically defined separately and connected by a token stream. This separate definition is important for modularity and reduces the potential for parsing ambiguity. However, materializing tokens as data structures and case-switching on tokens comes with a cost.We show how tofuseseparately-defined lexers and parsers, drastically improving performance without compromising modularity or increasing ambiguity. We propose a deterministic variant of Greibach Normal Form that ensures deterministic parsing with a single token of lookahead and makes fusion strikingly simple, and prove that normalizing context free expressions into the deterministic normal form is semantics-preserving. Our staged parser combinator library, flap, provides a standard interface, but generates specialized token-free code that runs two to six times faster than ocamlyacc on a range of benchmarks.
An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits
Authors: Chen Yu-Fang , Chung Kai-Min , Lengál Ondřej , Lin Jyun-Ao , Tsai Wei-Lun , Yen Di-De 
Published: June 2023

We introduce a new paradigm for analysing and finding bugs in quantum circuits. In our approach, the problem is given by a ‍triple {
P
}
C
{
Q
} and the question is whether, given a set
P
of quantum states on the input of a circuit
C
, the set of quantum states on the output is equal to (or included in) a set
Q
. While this is not suitable to specify, e.g., functional correctness of a quantum circuit, it is sufficient to detect many bugs in quantum circuits. We propose a technique based on tree automata to compactly represent sets of quantum states and develop transformers to implement the semantics of quantum gates over this representation. Our technique computes with an algebraic representation of quantum states, avoiding the inaccuracy of working with floating-point numbers. We implemented the proposed approach in a prototype tool and evaluated its performance against various benchmarks from the literature. The evaluation shows that our approach is quite scalable, e.g., we managed to verify a large circuit with 40 qubits and 141,527 gates, or catch bugs injected into a circuit with 320 qubits and 1,758 gates, where all tools we compared with failed. In addition, our work establishes a connection between quantum program verification and automata, opening new possibilities to exploit the richness of automata theory and automata-based verification in the world of quantum computing.
Sound Dynamic Deadlock Prediction in Linear Time
Authors: Tunç Hünkar Can , Mathur Umang , Pavlogiannis Andreas , Viswanathan Mahesh 
Published: June 2023

Deadlocks are one of the most notorious concurrency bugs, and significant research has focused on detecting them efficiently. Dynamic predictive analyses work by observing concurrent executions, and reason about alternative interleavings that can witness concurrency bugs. Such techniques offer scalability and sound bug reports, and have emerged as an effective approach for concurrency bug detection, such as data races. Effective dynamic deadlock prediction, however, has proven a challenging task, as no deadlock predictor currently meets the requirements of soundness, high-precision, and efficiency.
In this paper, we first formally establish that this tradeoff is unavoidable, by showing that (a) sound and complete deadlock prediction is intractable, in general, and (b) even the seemingly simpler task of determining the presence of potential deadlocks, which often serve as unsound witnesses for actual predictable deadlocks, is intractable. The main contribution of this work is a new class of predictable deadlocks, called sync(hronization)-preserving deadlocks. Informally, these are deadlocks that can be predicted by reordering the observed execution while preserving the relative order of conflicting critical sections. We present two algorithms for sound deadlock prediction based on this notion. Our first algorithm SPDOffline detects all sync-preserving deadlocks, with running time that is linear per abstract deadlock pattern, a novel notion also introduced in this work. Our second algorithm SPDOnline predicts all sync-preserving deadlocks that involve two threads in a strictly online fashion, runs in overall linear time, and is better suited for a runtime monitoring setting.
We implemented both our algorithms and evaluated their ability to perform offline and online deadlock-prediction on a large dataset of standard benchmarks. Our results indicate that our new notion of sync-preserving deadlocks is highly effective, as (i) it can characterize the vast majority of deadlocks and (ii) it can be detected using an online, sound, complete and highly efficient algorithm.
Cutting the Cake: A Language for Fair Division
Authors: Bertram Noah , Levinson Alex , Hsu Justin 
Published: June 2023

The fair division literature in economics considers how to divide resources between multiple agents such that the allocation is envy-free: each agent receives their favorite piece. Researchers have developed a variety of fair division protocols for the most standard setting, where the agents want to split a single item, however, the protocols are highly intricate and the proofs of envy-freeness involve tedious case analysis.
We propose Slice, a domain specific language for fair-division. Programs in our language can be converted to logical formulas encoding envy-freeness and other target properties. Then, the constraints can be dispatched to automated solvers. We prove that our constraint generation procedure is sound and complete. We also report on a prototype implementation of Slice, which we have used to automatically check envy-freeness for several protocols from the fair division literature.
The Chaotic Property of BTA Deep-Hole Machining System under the Effect of Inner Cutting Fluid
Authors: Zhang Quanbin , Zhao Wu , Li Yamin , Jing Shuangxi 
Published: June 2023

To clarify the action mechanism of parameter change on system stability, the chaotic property of BTA deep-hole machining system under the effect of inner cutting fluid was analyzed. According to the kinematic characteristics of the internal cutting fluid and the equation of the moment of momentum of the system, the kinematic equation of the boring bar considering the effect of the internal fluid was established. The critical conditions of chaos were deduced according to the Hamiltonian function and Melnikov function of the plane near-Hamilton system. The mechanism of the liquid filling ratio, cutting fluid flow velocity, and frequency ratio parameters on the system’s critical instability surface is investigated. The correlation and sensitivity of influencing factors, such as filling ratio and frequency ratio, and cutting fluid flow velocity to the sensitivity of system chaos are explored. The results show that in precision machining, the change of liquid filling ratio is positively related to the stability of the system, the change of cutting fluid flow velocity is negatively correlated with the stability of the system, and the change of frequency ratio has no monotonicity effect on the stability of the system. The sensitivity of the chaotic characteristics of the system to each parameter is bounded by the filling liquid ratio h = 0.58. When 0 ≤ h ≤ 0.58, frequency ratio

ω
¯

> filling ratio h > cutting fluid flow velocity V0; when 0.58 < h ≤ 1, filling ratio h > frequency ratio

ω
¯

> cutting fluid flow velocity V0. These research conclusions can lay a certain theoretical foundation for the analysis, control, and optimization of the complex mechanical behavior of BTA deep-hole machining systems in engineering practice.
Adavosertib Enhances Antitumor Activity of Trastuzumab Deruxtecan in HER2-Expressing Cancers
Authors: DiPeri Timothy P. , Evans Kurt W. , Raso Maria Gabriela , Zhao Ming , Rizvi Yasmeen Q. , Zheng Xiaofeng , Wang Bailiang , Kirby Bryce P. , Kong Kathleen , Kahle Michael , Yap Timothy A. , Dumbrava Ecaterina E. , Ajani Jaffer A. , Fu Siqing , Keyomarsi Khandan , Meric-Bernstam Funda 
Published: June 2023

Abstract

Purpose:
Cyclin E (CCNE1) has been proposed as a biomarker of sensitivity to adavosertib, a Wee1 kinase inhibitor, and a mechanism of resistance to HER2-targeted therapy.

Experimental Design:
Copy number and genomic sequencing data from The Cancer Genome Atlas and MD Anderson Cancer Center databases were analyzed to assess ERBB2 and CCNE1 expression. Molecular characteristics of tumors and patient-derived xenografts (PDX) were assessed by next-generation sequencing, whole-exome sequencing, fluorescent in situ hybridization, and IHC. In vitro, CCNE1 was overexpressed or knocked down in HER2+ cell lines to evaluate drug combination efficacy. In vivo, NSG mice bearing PDXs were subjected to combinatorial therapy with various treatment regimens, followed by tumor growth assessment. Pharmacodynamic markers in PDXs were characterized by IHC and reverse-phase protein array.

Results:
Among several ERBB2-amplified cancers, CCNE1 co-amplification was identified (gastric 37%, endometroid 43%, and ovarian serous adenocarcinoma 41%). We hypothesized that adavosertib may enhance activity of HER2 antibody–drug conjugate trastuzumab deruxtecan (T-DXd). In vitro, sensitivity to T-DXd was decreased by cyclin E overexpression and increased by knockdown, and adavosertib was synergistic with topoisomerase I inhibitor DXd. In vivo, the T-DXd + adavosertib combination significantly increased γH2AX and antitumor activity in HER2 low, cyclin E amplified gastroesophageal cancer PDX models and prolonged event-free survival (EFS) in a HER2-overexpressing gastroesophageal cancer model. T-DXd + adavosertib treatment also increased EFS in other HER2-expressing tumor types, including a T-DXd–treated colon cancer model.

Conclusions:
We provide rationale for combining T-DXd with adavosertib in HER2-expressing cancers, especially with co-occuring CCNE1 amplifications.
See related commentary by Rolfo et al., p. 4317
Early Changes in Circulating Cell-Free KRAS G12C Predict Response to Adagrasib in KRAS Mutant Non–Small Cell Lung Cancer Patients
Authors: Paweletz Cloud P. , Heavey Grace A. , Kuang Yanan , Durlacher Emily , Kheoh Thian , Chao Richard C. , Spira Alexander I. , Leventakos Konstantinos , Johnson Melissa L. , Ou Sai-Hong Ignatius , Riely Gregory J. , Anderes Kenna , Yang Wenjing , Christensen James G. , Jänne Pasi A. 
Published: June 2023

Abstract

Purpose:
Non-invasive monitoring of circulating tumor DNA (ctDNA) has the potential to be a readily available measure for early prediction of clinical response. Here, we report on early ctDNA changes of KRAS G12C in a Phase 2 trial of adagrasib in patients with advanced, KRAS G12C-mutant lung cancer.

Experimental Design:
We performed serial droplet digital PCR (ddPCR) and plasma NGS on 60 KRAS G12C-mutant patients with lung cancer that participated in cohort A of the KRYSTAL-1 clinical trial. We analyzed the change in ctDNA at 2 specific intervals: Between cycles 1 and 2 and at cycle 4. Changes in ctDNA were compared with clinical and radiographic response.

Results:
We found that, in general, a maximal response in KRAS G12C ctDNA levels could be observed during the initial approximately 3-week treatment period, well before the first scan at approximately 6 weeks. 35 patients (89.7%) exhibited a decrease in KRAS G12C cfDNA &gt;90% and 33 patients (84.6%) achieved complete clearance by cycle 2. Patients with complete ctDNA clearance at cycle 2 showed an improved objective response rate (ORR) compared with patients with incomplete ctDNA clearance (60.6% vs. 33.3%). Furthermore, complete ctDNA clearance at cycle 4 was associated with an improved overall survival (14.7 vs. 5.4 months) and progression-free survival (HR, 0.3).

Conclusions:
These results support using early plasma response of KRAS G12C assessed at approximately 3 weeks to anticipate the likelihood of a favorable objective clinical response.