bluuebunny/crossref_metadata_2025 huggingface dataset:
Program Analysis for Adaptive Data Analysis
Authors: Liu Jiawen , Qu Weihao , Gaboardi Marco , Garg Deepak , Ullman Jonathan
Published: June 2024

Data analyses are usually designed to identify some property of the population from which the data are drawn, generalizing beyond the specific data sample. For this reason, data analyses are often designed in a way that guarantees that they produce a low generalization error. That is, they are designed so that the result of a data analysis run on a sample data does not differ too much from the result one would achieve by running the analysis over the entire population. An adaptive data analysis can be seen as a process composed by multiple queries interrogating some data, where the choice of which query to run next may rely on the results of previous queries. The generalization error of each individual query/analysis can be controlled by using an array of well-established statistical techniques. However, when queries are arbitrarily composed, the different errors can propagate through the chain of different queries and bring to a high generalization error. To address this issue, data analysts are designing several techniques that not only guarantee bounds on the generalization errors of single queries, but that also guarantee bounds on the generalization error of the composed analyses. The choice of which of these techniques to use, often depends on the chain of queries that an adaptive data analysis can generate. In this work, we consider adaptive data analyses implemented as while-like programs and we design a program analysis which can help with identifying which technique to use to control their generalization errors. More specifically, we formalize the intuitive notion of
adaptivity
as a quantitative property of programs. We do this because the adaptivity level of a data analysis is a key measure to choose the right technique. Based on this definition, we design a program analysis for soundly approximating this quantity. The program analysis generates a representation of the data analysis as a weighted dependency graph, where the weight is an upper bound on the number of times each variable can be reached, and uses a path search strategy to guarantee an upper bound on the adaptivity. We implement our program analysis and show that it can help to analyze the adaptivity of several concrete data analyses with different adaptivity structures.
Consolidating Smart Contracts with Behavioral Contracts
Authors: Wei Guannan , Xie Danning , Zhang Wuqi , Yuan Yongwei , Zhang Zhuo
Published: June 2024

Ensuring the reliability of smart contracts is of vital importance due to the wide adoption of smart contract

programs in decentralized financial applications. However, statically checking many rich properties of smart

contract programs can be challenging. On the other hand, dynamic validation approaches have shown promise

for widespread adoption in practice. Nevertheless, as part of the programming environment for smart contracts,

existing dynamic validation approaches have not provided programmers with a notion to clearly articulate

the interface between components, especially for addresses representing opaque contract instances. We argue

that the “design-by-contract” approach should complement the development of smart contract programs.

Unfortunately, there is only limited linguistic support for that in existing smart contract languages.

In this paper, we design a Solidity language extension ConSol that supports behavioral contracts. ConSol

provides programmers with a modular specification and monitoring system for both functional and latent

address behaviors. The key capability of ConSol is to attach specifications to first-class addresses and monitor

violations when invoking these addresses. We evaluate ConSol using 20 real-world cases, demonstrating

its effectiveness in expressing critical conditions and preventing attacks. Additionally, we assess ConSol’s

efficiency and compare gas consumption with manually inserted assertions, showing that our approach

introduces only marginal gas overhead. By separating specifications and implementations using behavioral

contracts, ConSol assists programmers in writing smart contract code that is more robust and readable.
Scaling Type-Based Points-to Analysis with Saturation
Authors: Wimmer Christian , Stancu Codrut , Kozak David , Würthinger Thomas
Published: June 2024

Designing a whole-program static analysis requires trade-offs between precision and scalability. While a context-insensitive points-to analysis is often considered a good compromise, it still has non-linear complexity that leads to scalability problems when analyzing large applications. On the other hand, rapid type analysis scales well but lacks precision. We use
saturation
in a context-insensitive type-based points-to analysis to make it as scalable as a rapid type analysis, while preserving most of the precision of the points-to analysis. With saturation, the points-to analysis only propagates small points-to sets for variables. If a variable can have more values than a certain threshold, the variable and all its usages are considered saturated and no longer analyzed. Our implementation in the points-to analysis of GraalVM Native Image, a closed-world approach to build standalone binaries for Java applications, shows that saturation allows GraalVM Native Image to analyze large Java applications with hundreds of thousands of methods in less than two ‍minutes.
Symbolic Execution for Quantum Error Correction Programs
Authors: Fang Wang , Ying Mingsheng
Published: June 2024

We define QSE, a symbolic execution framework for quantum programs by integrating symbolic variables into quantum states and the outcomes of quantum measurements.

The soundness of QSE is established through a theorem that ensures the correctness of symbolic execution within operational semantics.

We further introduce symbolic stabilizer states, which symbolize the phases of stabilizer generators, for the efficient analysis of quantum error correction (QEC) programs.

Within the QSE framework, we can use symbolic expressions to characterize the possible discrete Pauli errors in QEC, providing a significant improvement over existing methods that rely on sampling with simulators.

We implement QSE with the support of symbolic stabilizer states in a prototype tool named QuantumSE.jl.

Our experiments on representative QEC codes, including quantum repetition codes, Kitaev's toric codes, and quantum Tanner codes, demonstrate the efficiency of QuantumSE.jl for debugging QEC programs with over 1000 qubits.

In addition, by substituting concrete values in symbolic expressions of measurement results, QuantumSE.jl is also equipped with a sampling feature for stabilizer circuits.

Despite a longer initialization time than the state-of-the-art stabilizer simulator, Google's Stim, QuantumSE.jl offers a quicker sampling rate in the experiments.
Reducing Static Analysis Unsoundness with Approximate Interpretation
Authors: Laursen Mathias Rud , Xu Wenyuan , Møller Anders
Published: June 2024

Static program analysis for JavaScript is more difficult than for many other programming languages. One of the main reasons is the presence of dynamic property accesses that read and write object properties via dynamically computed property names. To ensure scalability and precision, existing state-of-the-art analyses for JavaScript mostly ignore these operations although it results in missed call edges and aliasing relations.

We present a novel dynamic analysis technique named approximate interpretation that is designed to efficiently and fully automatically infer likely determinate facts about dynamic property accesses, in particular those that occur in complex library API initialization code, and how to use the produced information in static analysis to recover much of the abstract information that is otherwise missed.

Our implementation of the technique and experiments on 141 real-world Node.js-based JavaScript applications and libraries show that the approach leads to significant improvements in call graph construction. On average the use of approximate interpretation leads to 55.1% more call edges, 21.8% more reachable functions, 17.7% more resolved call sites, and only 1.5% fewer monomorphic call sites. For 36 JavaScript projects where dynamic call graphs are available, average analysis recall is improved from 75.9% to 88.1% with a negligible reduction in precision.
Maximum Consensus Floating Point Solutions for Infeasible Low-Dimensional Linear Programs with Convex Hull as the Intermediate Representation
Authors: Aanjaneya Mridul , Nagarakatte Santosh
Published: June 2024

This paper proposes a novel method to efficiently solve infeasible low-dimensional linear programs (LDLPs) with billions of constraints and a small number of unknown variables, where all the constraints cannot be satisfied simultaneously. We focus on infeasible linear programs generated in the RLibm project for creating correctly rounded math libraries. Specifically, we are interested in generating a floating point solution that satisfies the maximum number of constraints. None of the existing methods can solve such large linear programs while producing floating point solutions.

We observe that the convex hull can serve as an intermediate representation (IR) for solving infeasible LDLPs using the geometric duality between linear programs and convex hulls. Specifically, some of the constraints that correspond to points on the convex hull are precisely those constraints that make the linear program infeasible. Our key idea is to split the entire set of constraints into two subsets using the convex hull IR: (a) a set X of feasible constraints and (b) a superset V of infeasible constraints. Using the special structure of the RLibm constraints and the presence of a method to check whether a system is feasible or not, we identify a superset of infeasible constraints by computing the convex hull in 2-dimensions. Subsequently, we identify the key constraints (i.e., basis constraints) in the set of feasible constraints X and use them to create a new linear program whose solution identifies the maximum set of constraints satisfiable in V while satisfying all the constraints in X. This new solver enabled us to improve the performance of the resulting RLibm polynomials while solving the corresponding linear programs significantly faster.
Qubit Recycling Revisited
Authors: Jiang Hanru
Published: June 2024

Reducing the width of quantum circuits is crucial due to limited number of qubits in quantum devices. This paper revisit an optimization strategy known as
qubit recycling
(alternatively
wire-recycling
or
measurement-and-reset
), which leverages gate commutativity to reuse discarded qubits, thereby reducing circuit width. We introduce
qubit dependency graphs
(QDGs) as a key abstraction for this optimization. With QDG, we isolate the computationally demanding components, and observe that qubit recycling is essentially a matrix triangularization problem. Based on QDG and this observation, we study qubit recycling with a focus on complexity, algorithmic, and verification aspects. Firstly, we establish qubit recycling’s NP-hardness through reduction from Wilf’s question, another matrix triangularization problem. Secondly, we propose a QDG-guided solver featuring multiple heuristic options for effective qubit recycling. Benchmark tests conducted on RevLib illustrate our solver’s superior or comparable performance to existing alternatives. Notably, it achieves optimal solutions for the majority of circuits. Finally, we develop a certified qubit recycler that integrates verification and validation techniques, with its correctness proof mechanized in Coq.
An Algebraic Language for Specifying Quantum Networks
Authors: Buckley Anita , Chuprikov Pavel , Otoni Rodrigo , Soulé Robert , Rand Robert , Eugster Patrick
Published: June 2024

Quantum networks connect quantum capable nodes in order to achieve capabilities that are impossible only using classical information. Their fundamental unit of communication is the Bell pair, which consists of two entangled quantum bits. Unfortunately, Bell pairs are fragile and difficult to transmit directly, necessitating a network of repeaters, along with software and hardware that can ensure the desired results. Challenging intrinsic features of quantum networks, such as dealing with resource competition, motivate formal reasoning about quantum network protocols. To this end, we developed BellKAT, a novel specification language for quantum networks based upon Kleene algebra. To cater to the specific needs of quantum networks, we designed an algebraic structure, called BellSKA, which we use as the basis of BellKAT's denotational semantics. BellKAT's constructs describe entanglement distribution rules that allow for modular specification. We give BellKAT a sound and complete equational theory, allowing us to verify network protocols. We provide a prototype tool to showcase the expressiveness of BellKAT and how to optimize and verify networks in practice.
Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
Authors: Wang Peixin , Yang Tengshun , Fu Hongfei , Li Guanyan , Ong C.-H. Luke
Published: June 2024

In Bayesian probabilistic programming, a central problem is to estimate the normalised posterior distribution (NPD) of a probabilistic program with conditioning via score (a.k.a. observe) statements. Most previous approaches address this problem by Markov Chain Monte Carlo and variational inference, and therefore could not generate guaranteed outcomes within a finite time limit. Moreover, existing methods for exact inference either impose syntactic restrictions or cannot guarantee successful inference in general.

In this work, we propose a novel automated approach to derive guaranteed bounds for NPD via polynomial solving. We first establish a fixed-point theorem for the wide class of score-at-end Bayesian probabilistic programs that terminate almost-surely and have a single bounded score statement at program termination. Then, we propose a multiplicative variant of Optional Stopping Theorem (OST) to addressscore-recursiveBayesian programs where score statements with weights greater than one could appear inside a loop. Bayesian nonparametric models, enjoying a renaissance in statistics and machine learning, can be represented by score-recursive Bayesian programs and are difficult to handle due to an integrability issue. Finally, we use polynomial solving to implement our fixed-point theorem and OST variant. To improve the accuracy of the polynomial solving, we further propose a truncation operation and the synthesis of multiple bounds over various program inputs. Our approach can handle Bayesian probabilistic programs with unbounded while loops and continuous distributions with infinite supports. Experiments over a wide range of benchmarks show that compared with the most relevant approach (Beutner et al., PLDI 2022) for guaranteed NPD analysis via recursion unrolling, our approach is more time efficient and derives comparable or even tighter NPD bounds. Furthermore, our approach can handle score-recursive programs which previous approaches could not.
Stream Types
Authors: Cutler Joseph W. , Watson Christopher , Nkurumeh Emeka , Hilliard Phillip , Goldstein Harrison , Stanford Caleb , Pierce Benjamin C.
Published: June 2024

We propose a rich foundational theory of typed data streams and stream transformers, motivated by two high-level goals. First, the type of a stream should be able to express complex
sequential patterns
of events over time. And second, it should describe the internal
parallel structure
of the stream, to support deterministic stream processing on parallel and distributed systems. To these ends, we introduce
stream types
, with operators capturing sequential composition, parallel composition, and iteration, plus a core calculus λ

ST

of
transformers
over typed streams that naturally supports a number of common streaming idioms, including punctuation, windowing, and parallel partitioning, as first-class constructions. λ

ST

exploits a Curry-Howard-like correspondence with an ordered variant of the Logic of Bunched Implication to program with streams compositionally and uses Brzozowski-style derivatives to enable an incremental, prefix-based operational semantics. To illustrate the programming style supported by the rich types of λ

ST

, we present a number of examples written in Delta, a prototype high-level language design based on λ

ST

.
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties
Authors: Dardinier Thibault , Müller Peter
Published: June 2024

Hoare logics are proof systems that allow one to formally establish properties of computer programs. Traditional Hoare logics prove properties of individual program executions (such as functional correctness). Hoare logic has been generalized to prove also properties of multiple executions of a program (so-called hyperproperties, such as determinism or non-interference). These program logics prove the absence of (bad combinations of) executions. On the other hand, program logics similar to Hoare logic have been proposed to disprove program properties (e.g., Incorrectness Logic), by proving the existence of (bad combinations of) executions. All of these logics have in common that they specify program properties using assertions over a fixed number of states, for instance, a single pre- and post-state for functional properties or pairs of pre- and post-states for non-interference.
In this paper, we present Hyper Hoare Logic, a generalization of Hoare logic that lifts assertions to properties of arbitrary sets of states. The resulting logic is simple yet expressive: its judgments can express arbitrary program hyperproperties, a particular class of hyperproperties over the set of terminating executions of a program (including properties of individual program executions). By allowing assertions to reason about sets of states, Hyper Hoare Logic can reason about both the absence and the existence of (combinations of) executions, and, thereby, supports both proving and disproving program (hyper-)properties within the same logic, including (hyper-)properties that no existing Hoare logic can express. We prove that Hyper Hoare Logic is sound and complete, and demonstrate that it captures important proof principles naturally. All our technical results have been proved in Isabelle/HOL.
Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding
Authors: Yi Qiuping , Yu Yifan , Yang Guowei
Published: June 2024

Symbolic execution is a powerful technique for bug finding by generating test inputs to systematically explore all feasible paths within a given threshold. However, its practical usage is often limited by the
path explosion
problem. In this paper, we propose compatible branch coverage driven symbolic execution for efficient bug finding. Our new technique owns a novel path-pruning strategy obtained from program dependency analysis to effectively avoid unnecessary explorations. Specifically, based on a
Compatible Branch Set
, our technique directs symbolic execution to explore feasible branches while soundly pruning redundant paths that have no new contributions to branch coverage. We have implemented our approach atop KLEE and conducted experiments on a set of programs from Siemens Suite, GNU Coreutils, and other real-world programs. Experimental results show that, compared with the state-of-the-art symbolic execution techniques, our approach always uses significantly less time to reproduce bugs while achieving the same or better branch coverage. On average, our approach got over 45% path reduction and 3x speedup on the GNU Coreutils programs.
RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
Authors: Fitzgibbons Michael , Paraskevopoulou Zoe , Mushtak Noble , Thalakottur Michelle , Sulaiman Manzur Jose , Ahmed Amal
Published: June 2024

Safe, shared-memory interoperability between languages with different type systems and memory-safety guarantees is an intricate problem as crossing language boundaries may result in memory-safety violations. In this paper, we present RichWasm, a novel richly typed intermediate language designed to serve as a compilation target for typed high-level languages with different memory-safety guarantees. RichWasm is based on WebAssembly and enables safe shared-memory interoperability by incorporating a variety of type features that support fine-grained memory ownership and sharing. RichWasm is rich enough to serve as a typed compilation target for both typed garbage-collected languages and languages with an ownership-based type system and manually managed memory. We demonstrate this by providing compilers from core ML and L3, a type-safe language with strong updates, to RichWasm. RichWasm is compiled to regular Wasm, allowing for use in existing environments. We formalize RichWasm in Coq and prove type safety.
SpEQ: Translation of Sparse Codes using Equivalences
Authors: Laird Avery , Liu Bangtian , Bjørner Nikolaj , Dehnavi Maryam Mehri
Published: June 2024

We present SpEQ, a quick and correct strategy for detecting semantics in sparse codes and enabling automatic translation to high-performance library calls or domain-specific languages (DSLs). When sparse linear algebra codes contain implicit preconditions about how data is stored that hamper direct translation, SpEQ identifies the high-level computation along with storage details and related preconditions. A run-time check guards the translation and ensures that required preconditions are met. We implement SpEQ using the LLVM framework, the Z3 solver, and egglog library and correctly translate sparse linear algebra codes into two high-performance libraries, NVIDIA cuSPARSE and Intel MKL, and OpenMP (OMP). We evaluate SpEQ on ten diverse benchmarks against two state-of-the-art translation tools. SpEQ achieves geometric mean speedups of 3.25×, 5.09×, and 8.04× on OpenMP, MKL, and cuSPARSE backends, respectively. SpEQ is the only tool that can guarantee the correct translation of sparse computations.
Foundational Integration Verification of a Cryptographic Server
Authors: Erbsen Andres , Philipoom Jade , Jamner Dustin , Lin Ashley , Gruetter Samuel , Pit-Claudel Clément , Chlipala Adam
Published: June 2024

We present verification of a bare-metal server built using diverse implementation techniques and languages against a whole-system input-output specification in terms of machine code, network packets, and mathematical specifications of elliptic-curve cryptography. We used very different formal-reasoning techniques throughout the stack, ranging from computer algebra, symbolic execution, and verification-condition generation to interactive verification of functional programs including compilers for C-like and functional languages. All these component specifications and domain-specific reasoning techniques are defined and justified against common foundations in the Coq proof assistant. Connecting these components is a minimalistic specification style based on functional programs and assertions over simple objects, omnisemantics for program execution, and basic separation logic for memory layout. This design enables us to bring the components together in a top-level correctness theorem that can be audited without understanding or trusting the internal interfaces and tools. Our case study is a simple cryptographic server for flipping of a bit of state through public-key authenticated network messages, and its proof shows total functional correctness including static bounds on memory usage. This paper also describes our experiences with the specific verification tools we build upon, along with detailed analysis of reasons behind the widely varying levels of productivity we experienced between combinations of tools and tasks.
SPORE: Combining Symmetry and Partial Order Reduction
Authors: Kokologiannakis Michalis , Marmanis Iason , Vafeiadis Viktor
Published: June 2024

Symmetry reduction (SR) and partial order reduction (POR) aim to scale up model checking by exploiting the underlying program structure: SR avoids exploring executions equivalent up to some permutation of symmetric threads, while POR avoids exploring executions equivalent up to reordering of independent instructions. While both SR and POR have been well studied individually, their combination in the context of stateless model checking has remained an open problem. In this paper, we present SPORE, the first stateless model checker that combines SR and POR in a sound, complete and optimal manner. SPORE can leverage both symmetries in the client program itself, but also
internal symmetries
in the underlying implementation (i.e., idempotent operations), a novel symmetry notion we introduce in this paper. Our experiments confirm that SPORE explores drastically fewer executions than tools that solely employ SR/POR, thereby greatly advancing the state-of-the-art.
KATch: A Fast Symbolic Verifier for NetKAT
Authors: Moeller Mark , Jacobs Jules , Belanger Olivier Savary , Darais David , Schlesinger Cole , Smolka Steffen , Foster Nate , Silva Alexandra
Published: June 2024

We develop new data structures and algorithms for checking verification queries in NetKAT, a domain-specific language for specifying the behavior of network data planes. Our results extend the techniques obtained in prior work on symbolic automata and provide a framework for building efficient and scalable verification tools. We present KATch, an implementation of these ideas in Scala, featuring an extended set of NetKAT operators that are useful for expressing network-wide specifications, and a verification engine that constructs a bisimulation or generates a counter-example showing that none exists. We evaluate the performance of our implementation on real-world and synthetic benchmarks, verifying properties such as reachability and slice isolation, typically returning a result in well under a second, which is orders of magnitude faster than previous approaches. Our advancements underscore NetKAT's potential as a practical, declarative language for network specification and verification.
Hyperblock Scheduling for Verified High-Level Synthesis
Authors: Herklotz Yann , Wickerson John
Published: June 2024

High-level synthesis (HLS) is the automatic compilation of software programs into custom hardware designs. With programmable hardware devices (such as FPGAs) now widespread, HLS is increasingly relied upon, but existing HLS tools are too unreliable for safety- and security-critical applications. Herklotz et al. partially addressed this concern by building Vericert, a prototype HLS tool that is proven correct in Coq (à la CompCert), but it cannot compete performance-wise with unverified tools. This paper reports on our efforts to close this performance gap, thus obtaining the first practical verified HLS tool. We achieve this by implementing a flexible operation scheduler based on hyperblocks (basic blocks of predicated instructions) that supports operation chaining (packing dependent operations into a single clock cycle). Correctness is proven via translation validation: each schedule is checked using a Coq-verified validator that uses a SAT solver to reason about predicates. Avoiding exponential blow-up in this validation process is a key challenge, which we address by using final-state predicates and value summaries. Experiments on the PolyBench/C suite indicate that scheduling makes Vericert-generated hardware 2.1× faster, thus bringing Vericert into competition with a state-of-the-art open-source HLS tool when a similar set of optimisations is enabled.
Static Analysis for Checking the Disambiguation Robustness of Regular Expressions
Authors: Mamouras Konstantinos , Le Glaunec Alexis , Li Wu Angela , Chattopadhyay Agnishom
Published: June 2024

Regular expressions are commonly used for finding and extracting matches from sequence data. Due to the inherent ambiguity of regular expressions, a disambiguation policy must be considered for the match extraction problem, in order to uniquely determine the desired match out of the possibly many matches. The most common disambiguation policies are the POSIX policy and the greedy (PCRE) policy. The POSIX policy chooses the longest match out of the leftmost ones. The greedy policy chooses a leftmost match and further disambiguates using a greedy interpretation of Kleene iteration to match as many times as possible. The choice of disambiguation policy can affect the output of match extraction, which can be an issue for reusing regular expressions across regex engines. In this paper, we introduce and study the notion of disambiguation robustness for regular expressions. A regular expression is robust if its extraction semantics is indifferent to whether the POSIX or greedy disambiguation policy is chosen. This gives rise to a decision problem for regular expressions, which we prove to be PSPACE-complete. We propose a static analysis algorithm for checking the (non-)robustness of regular expressions and two performance optimizations. We have implemented the proposed algorithms and we have shown experimentally that they are practical for analyzing large datasets of regular expressions derived from various application domains.
Probabilistic Programming with Programmable Variational Inference
Authors: Becker McCoy R. , Lew Alexander K. , Wang Xiaoyan , Ghavami Matin , Huot Mathieu , Rinard Martin C. , Mansinghka Vikash K.
Published: June 2024

Compared to the wide array of advanced Monte Carlo methods supported by modern probabilistic programming languages (PPLs), PPL support for variational inference (VI) is less developed: users are typically limited to a predefined selection of variational objectives and gradient estimators, which are implemented monolithically (and without formal correctness arguments) in PPL backends. In this paper, we propose a more modular approach to supporting variational inference in PPLs, based on compositional program transformation. In our approach, variational objectives are expressed as programs, that may employ first-class constructs for computing densities of and expected values under user-defined models and variational families. We then transform these programs systematically into unbiased gradient estimators for optimizing the objectives they define. Our design makes it possible to prove unbiasedness by reasoning modularly about many interacting concerns in PPL implementations of variational inference, including automatic differentiation, density accumulation, tracing, and the application of unbiased gradient estimation strategies. Additionally, relative to existing support for VI in PPLs, our design increases expressiveness along three axes: (1) it supports an open-ended set of user-defined variational objectives, rather than a fixed menu of options; (2) it supports a combinatorial space of gradient estimation strategies, many not automated by today’s PPLs; and (3) it supports a broader class of models and variational families, because it supports constructs for approximate marginalization and normalization (previously introduced for Monte Carlo inference). We implement our approach in an extension to the Gen probabilistic programming system (genjax.vi, implemented in JAX), and evaluate our automation on several deep generative modeling tasks, showing minimal performance overhead vs. hand-coded implementations and performance competitive with well-established open-source PPLs.
PL4XGL: A Programming Language Approach to Explainable Graph Learning
Authors: Jeon Minseok , Park Jihyeok , Oh Hakjoo
Published: June 2024

In this article, we present a new, language-based approach to explainable graph learning. Though graph neural networks (GNNs) have shown impressive performance in various graph learning tasks, they have severe limitations in explainability, hindering their use in decision-critical applications. To address these limitations, several GNN explanation techniques have been proposed using a post-hoc explanation approach providing subgraphs as explanations for classification results. Unfortunately, however, they have two fundamental drawbacks in terms of additional explanation costs and 2) the correctness of the explanations. This paper aims to address these problems by developing a new graph-learning method based on programming language techniques. Our key idea is two-fold: 1) designing a graph description language (GDL) to explain the classification results and 2) developing a new GDL-based interpretable classification model instead of GNN-based models. Our graph-learning model, called PL4XGL, consists of a set of candidate GDL programs with labels and quality scores. For a given graph component, it searches the best GDL program describing the component and provides the corresponding label as the classification result and the program as the explanation. In our approach, learning from data is formulated as a program-synthesis problem, and we present top-down and bottom-up algorithms for synthesizing GDL programs from training data. Evaluation using widely-used datasets demonstrates that PL4XGL produces high-quality explanations that outperform those produced by the state-of-the-art GNN explanation technique, SubgraphX. We also show that PL4XGL achieves competitive classification accuracy comparable to popular GNN models.
A Family of Fast and Memory Efficient Lock- and Wait-Free Reclamation
Authors: Nikolaev Ruslan , Ravindran Binoy
Published: June 2024

Historically, memory management based on lock-free reference counting was very inefficient, especially for read-dominated workloads. Thus, approaches such as epoch-based reclamation (EBR), hazard pointers (HP), or a combination thereof have received significant attention. EBR exhibits excellent performance but is blocking due to potentially unbounded memory usage. In contrast, HP are non-blocking and achieve good memory efficiency but are much slower. Moreover, HP are only lock-free in the general case. Recently, several new memory reclamation approaches such as WFE and Hyaline have been proposed. WFE achieves wait-freedom, but is less memory efficient and performs suboptimally in oversubscribed scenarios; Hyaline achieves higher performance and memory efficiency, but lacks wait-freedom.

We present a family of non-blocking memory reclamation schemes, called Crystalline, that simultaneously addresses the challenges of high performance, high memory efficiency, and wait-freedom. Crystalline can guarantee complete wait-freedom even when threads are dynamically recycled, asynchronously reclaims memory in the sense that any thread can reclaim memory retired by any other thread, and ensures (an almost) balanced reclamation workload across all threads. The latter two properties result in Crystalline's high performance and memory efficiency. Simultaneously ensuring all three properties requires overcoming unique challenges. Crystalline supports ubiquitous x86-64 and ARM64 architectures, while achieving superior throughput than prior fast schemes such as EBR as the number of threads grows.

We also accentuate that many recent approaches, unlike HP, lack strict non-blocking guarantees when used with multiple data structures. By providing full wait-freedom, Crystalline addresses this problem as well.
ZPredict: ML-Based IPID Side-channel Measurements
Authors: Schulmann Haya , Zhao Shujie
Published: June 2024

Network reconnaissance and measurements play a central role in improving Internet security and are important for understanding the current deployments and trends. Such measurements often require coordination with the measured target. This limits the scalability and the coverage of the existing proposals. IP Identification (IPID) provides a side channel for remote measurements without requiring the targets to install agents or visit the measurement infrastructure. However, current IPID-based techniques have technical limitations due to their reliance on the idealistic assumption of stable IPID changes or prior knowledge, making them challenging to adopt for practical measurements.

In this work, we aim to tackle the limitations of existing techniques by introducing a novel approach: predictive analysis of IPID counter behavior. This involves utilizing a machine learning (ML) model to understand the historical patterns of IPID counter changes and predict future IPID values. To validate our approach, we implement six ML models and evaluate them on realistic IPID data collected from 4,698 Internet sources. Our evaluations demonstrate that among the six models, the Gaussian Process (GP) model has superior accuracy in tracking and predicting IPID values.

Using the GP-based predictive analysis, we implement a tool, called ZPredict, to infer various favorable information about target networks or servers. Our evaluation on a large dataset of public servers demonstrates its effectiveness in idle port scanning, measuring Russian censorship, and inferring Source Address Validation.

Our study methodology is ethical and was developed to mitigate any potential harm, taking into account the concerns associated with measurements.
Evaluating ChatGPT-4 Vision on Brazil's National Undergraduate Computer Science Exam
Authors: Mendonça Nabor C.
Published: June 2024

The recent integration of visual capabilities into Large Language Models (LLMs) has the potential to play a pivotal role in science and technology education, where visual elements such as diagrams, charts, and tables are commonly used to improve the learning experience. This study investigates the performance of ChatGPT-4 Vision, OpenAI’s most advanced visual model at the time the study was conducted, on the Bachelor in Computer Science section of Brazil’s 2021 National Undergraduate Exam (ENADE). By presenting the model with the exam’s open and multiple-choice questions in their original image format and allowing for reassessment in response to differing answer keys, we were able to evaluate the model’s reasoning and self-reflecting capabilities in a large-scale academic assessment involving textual and visual content. ChatGPT-4 Vision significantly outperformed the average exam participant, positioning itself within the top 10 best score percentile. While it excelled in questions that incorporated visual elements, it also encountered challenges with question interpretation, logical reasoning, and visual acuity. A positive correlation between the model’s performance in multiple-choice questions and the performance distribution of the human participants suggests multimodal LLMs can provide a useful tool for question testing and refinement. However, the involvement of an independent expert panel to review cases of disagreement between the model and the answer key revealed some poorly constructed questions containing vague or ambiguous statements, calling attention to the critical need for improved question design in future exams. Our findings suggest that while ChatGPT-4 Vision shows promise in multimodal academic evaluations, human oversight remains crucial for verifying the model’s accuracy and ensuring the fairness of high-stakes educational exams. The paper’s research materials are publicly available at
https://github.com/nabormendonca/gpt-4v-enade-cs-2021
.
Lanthanum Substituted Mg-Zn Ferrite Nanostructures: A Comprehensive Study of Cation Distribution, Structural, Morphological, Optical, Magnetic, Dielectric, and Electromagnetic Traits
Authors: Jasrotia Rohit , Sharma Anand , Ahmed Jahangeer , Verma Ritesh , Alshehri Saad M. , Lakshmaiya Natrayan , Sillanpää Mika , Kumar Rajinder , Khanna Virat
Published: June 2024

The sol-gel auto-combustion (SC) procedure was utilised to fabricate lanthanum-doped Mg-Zn nanostructures with the chemical composition, Mg0.6Zn0.4LaxFe2-xO4, (x = 0, 0.05, 0.10). X-ray diffraction showed nanocrystalline and single-phase of Mg-Zn nanostructures. The morphological traits showed formation of irregular and aggregated grains. Fourier transform infrared spectroscopy detected the formation of two characteristic band positions that fall within the range of 400 to 600 cm−1 and may occur because of stretching vibration within metal-oxygen (M-O) cations located at interstitial positions. From the M-H loops, the excellent values of magnetic factors, such as the saturation magnetization (Ms), rentivity (Mr), and coercivity (Hc) ranging from 35.30 to 44.79 emu g−1, 1.40 to 3.75 emu g−1, and 11.56 to 41.42 Oe were obtained. The loss tangent (tan δ) was observed to be miniscule for all of the samples due to which they can be useful for electronic applications. However, the initial values of the real permeability (

μ

′

) was high and it decreases until 4 GHz, after which it acquires a constant value for rest of frequency range. However, observed low values of the magnetic loss tangent (tan δ

μ
) were due to the large grain size and the high densification of the samples.
Supplementary Figure 8 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

Circulating ORF1p (first generation Simoa assay) versus prostate-specific antigen (PSA).
Supplementary Figure 20 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

Additional second-generation ORF1p Simoa assay measurements in healthy and cancer patients.
Supplementary Figure 11 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

Engineered Nanobody constructs.
CD28 Costimulation Augments CAR Signaling in NK Cells via the LCK/CD3ζ/ZAP70 Signaling Axis
Authors: Acharya Sunil , Basar Rafet , Daher May , Rafei Hind , Li Ping , Uprety Nadima , Ensley Emily , Shanley Mayra , Kumar Bijender , Banerjee Pinaki P. , Melo Garcia Luciana , Lin Paul , Mohanty Vakul , Kim Kun H. , Jiang Xianli , Pan Yuchen , Li Ye , Liu Bin , Nunez Cortes Ana K. , Zhang Chenyu , Fathi Mohsen , Rezvan Ali , Montalvo Melisa J. , Cha Sophia L. , Reyes-Silva Francia , Shrestha Rejeena , Guo Xingliang , Kundu Kiran , Biederstädt Alexander , Muniz-Feliciano Luis , Deyter Gary M. , Kaplan Mecit , Jiang Xin R. , Liu Enli , Jain Antrix , Roszik Janos , Fowlkes Natalie W. , Solis Soto Luisa M. , Raso Maria G. , Khoury Joseph D. , Lin Pei , Vega Francisco , Varadarajan Navin , Chen Ken , Marin David , Shpall Elizabeth J. , Rezvani Katayoun
Published: June 2024

Multiple factors in the design of a chimeric antigen receptor (CAR) influence CAR T-cell activity, with costimulatory signals being a key component. Yet, the impact of costimulatory domains on the downstream signaling and subsequent functionality of CAR-engineered natural killer (NK) cells remains largely unexplored. Here, we evaluated the impact of various costimulatory domains on CAR-NK cell activity, using a CD70-targeting CAR. We found that CD28, a costimulatory molecule not inherently present in mature NK cells, significantly enhanced the antitumor efficacy and long-term cytotoxicity of CAR-NK cells both in vitro and in multiple xenograft models of hematologic and solid tumors. Mechanistically, we showed that CD28 linked to CD3ζ creates a platform that recruits critical kinases, such as lymphocyte-specific protein tyrosine kinase (LCK) and zeta-chain-associated protein kinase 70 (ZAP70), initiating a signaling cascade that enhances CAR-NK cell function. Our study provides insights into how CD28 costimulation enhances CAR-NK cell function and supports its incorporation in NK-based CARs for cancer immunotherapy.

Significance: We demonstrated that incorporation of the T-cell–centric costimulatory molecule CD28, which is normally absent in mature natural killer (NK) cells, into the chimeric antigen receptor (CAR) construct recruits key kinases including lymphocyte-specific protein tyrosine kinase and zeta-chain-associated protein kinase 70 and results in enhanced CAR-NK cell persistence and sustained antitumor cytotoxicity.
Supplementary Figure S8 from The TERT Promoter is Polycomb-Repressed in Neuroblastoma Cells with Long Telomeres
Authors: Graham Mindy K. , Xu Beisi , Davis Christine , Meeker Alan K. , Heaphy Christopher M. , Yegnasubramanian Srinivasan , Dyer Michael A. , Zeineldin Maged
Published: June 2024

Supplementary Figure S8
FIGURE 3 from The TERT Promoter is Polycomb-Repressed in Neuroblastoma Cells with Long Telomeres
Authors: Graham Mindy K. , Xu Beisi , Davis Christine , Meeker Alan K. , Heaphy Christopher M. , Yegnasubramanian Srinivasan , Dyer Michael A. , Zeineldin Maged
Published: June 2024

Active chromatin marks in MYCN-amplified neuroblastoma and repressive chromatin marks in neuroblastoma cells with long telomeres. ChromHMM states, all ChIP-Seq tracks and WGBS for MYCN-amplified O-PDX (SJNBL013763, A) and cell line (SKNBE2, B) showing active marks in the TERT locus. ChromHMM states, all ChIP-seq tracks and WGBS for ATRX-mutant, ALT-positive O-PDX (SJNBL030014, C) and cell line (SKNMM, D) showing repressive marks in the TERT locus. The color codes for different ChromHMM states are shown in E.