bluuebunny/crossref_metadata_2025 huggingface dataset:
Architecture-Preserving Provable Repair of Deep Neural Networks
Authors: Tao Zhe , Nawas Stephanie , Mitchell Jacqueline , Thakur Aditya V.
Published: June 2023

Deep neural networks (DNNs) are becoming increasingly important components
of software, and are considered the state-of-the-art solution for a number
of problems, such as image recognition. However, DNNs are far from
infallible, and incorrect behavior of DNNs can have disastrous real-world
consequences. This paper addresses the problem of architecture-preserving
V-polytope provable repair of DNNs.
A V-polytope defines a convex bounded polytope using its vertex representation.
V-polytope provable repair guarantees that the repaired DNN
satisfies the given specification on the infinite set of points in the given V-polytope.
An architecture-preserving repair only modifies the parameters of the DNN, without
modifying its architecture. The repair has the flexibility to
modify multiple layers of the DNN, and runs in polynomial time.
It supports DNNs with activation functions that have some linear pieces,
as well as fully-connected, convolutional, pooling and residual layers.
To the best our knowledge, this is the first provable repair approach that
has all of these features.
We implement our approach in a tool called APRNN. Using
MNIST, ImageNet, and ACAS Xu DNNs, we show that
it has better efficiency, scalability, and generalization
compared to PRDNN and REASSURE, prior provable repair methods that are
not architecture preserving.
Defunctionalization with Dependent Types
Authors: Huang Yulong , Yallop Jeremy
Published: June 2023

The
defunctionalization
translation that eliminates higher-order functions from programs forms a key part of many compilers. However, defunctionalization for dependently-typed languages has not been formally studied.

We present the first formally-specified defunctionalization translation for a dependently-typed language and establish key metatheoretical properties such as soundness and type preservation. The translation is suitable for incorporation into type-preserving compilers for dependently-typed languages
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.
A Type System for Safe Intermittent Computing
Authors: Surbatovich Milijana , Spargo Naomi , Jia Limin , Lucia Brandon
Published: June 2023

Batteryless energy-harvesting devices enable computing in inaccessible environments, at a cost to programmability and correctness. These devices operate intermittently as energy is available, using a recovery system to save and restore state. Some program tasks must execute atomically w.r.t. power failures, re-executing if power fails before completion. Any re-execution should typically be
idempotent
—its behavior should match the behavior of a single execution. Thus, a key aspect of correct intermittent execution is identifying and recovering state causing undesired non-idempotence. Unfortunately, past intermittent systems take an ad-hoc approach, using unsound dataflow analyses or conservatively recovering all written state. Moreover, no prior work allows the programmer to directly specify idempotence requirements (including allowable non-idempotence).

We present curricle, the first
type system
approach to safe intermittence, for Rust. Type level reasoning allows programmers to express requirements and retains alias information crucial for sound analyses. Curricle uses information flow and type qualifiers to reject programs causing undesired non-idempotence. We implement Curricle’s type system on top of Rust’s compiler, evaluating the prototype on benchmarks from prior work. We find that Curricle benefits application programmers by allowing them to express idempotence requirements that are checked to be satisfied, and that targeting programs checked with Curricle allows intermittent system designers to write simpler recovery systems that perform better.
Optimal Reads-From Consistency Checking for C11-Style Memory Models
Authors: Tunç Hünkar Can , Abdulla Parosh Aziz , Chakraborty Soham , Krishna Shankaranarayanan , Mathur Umang , Pavlogiannis Andreas
Published: June 2023

Over the years, several memory models have been proposed to capture the subtle concurrency semantics of C/C++. One of the most fundamental problems associated with a memory model
M
is consistency checking: given an execution
X
, is
X
consistent with
M
? This problem lies at the heart of numerous applications, including specification testing and litmus tests, stateless model checking, and dynamic analyses. As such, it has been explored extensively and its complexity is well-understood for traditional models like SC and TSO. However, less is known for the numerous model variants of C/C++, for which the problem becomes challenging due to the intricacies of their concurrency primitives. In this work we study the problem of consistency checking for popular variants of the C11 memory model, in particular, the
RC
20 model, its release-acquire (
RA
) fragment, the strong and weak variants of
RA
(
SRA
and
WRA
), as well as the
Relaxed
fragment of
RC
20.

Motivated by applications in testing and model checking, we focus on reads-from consistency checking. The input is an execution
X
specifying a set of events, their program order and their reads-from relation, and the task is to decide the existence of a modification order on the writes of
X
that makes
X
consistent in a memory model. We draw a rich complexity landscape for this problem; our results include (i) nearly-linear-time algorithms for certain variants, which improve over prior results, (ii) fine-grained optimality results, as well as (iii) matching upper and lower bounds (NP-hardness) for other variants. To our knowledge, this is the first work to characterize the complexity of consistency checking for C11 memory models. We have implemented our algorithms inside the TruSt model checker and the C11Tester testing tool. Experiments on standard benchmarks show that our new algorithms improve consistency checking, often by a significant margin.
Fair Operational Semantics
Authors: Lee Dongjae , Cho Minki , Kim Jinwoo , Moon Soonwon , Song Youngju , Hur Chung-Kil
Published: June 2023

Fairness properties, which state that a sequence of bad events cannot happen infinitely before a good event takes place, are often crucial in program verification. However, general methods for expressing and reasoning about various kinds of fairness properties are relatively underdeveloped compared to those for safety properties.
This paper proposes FOS (Fair Operational Semantics), a theory capable of expressing arbitrary notions of fairness as an operational semantics and reasoning about these notions of fairness. In addition, FOS enables thread-local reasoning about fairness by providing thread-local simulation relations equipped with separation- logic-style resource algebras. We verify a ticket lock implementation and a client of the ticket lock under weak memory concurrency as an example, which requires reasoning about different notions of fairness including fairness of a scheduler, fairness of the ticket lock implementation, and even fairness of weak memory. The theory of FOS, as well as the examples in the paper, are fully formalized in Coq.
Synthesizing Quantum-Circuit Optimizers
Authors: Xu Amanda , Molavi Abtin , Pick Lauren , Tannu Swamit , Albarghouthi Aws
Published: June 2023

Near-term quantum computers are expected to work in an environment where each operation is noisy, with no error correction. Therefore, quantum-circuit optimizers are applied to minimize the number of noisy operations. Today, physicists are constantly experimenting with novel devices and architectures. For every new physical substrate and for every modification of a quantum computer, we need to modify or rewrite major pieces of the optimizer to run successful experiments. In this paper, we present QUESO, an efficient approach for automatically synthesizing a quantum-circuit optimizer for a given quantum device. For instance, in 1.2 minutes, QUESO can synthesize an optimizer with high-probability correctness guarantees for IBM computers that significantly outperforms leading compilers, such as IBM's Qiskit and TKET, on the majority (85%) of the circuits in a diverse benchmark suite.

A number of theoretical and algorithmic insights underlie QUESO: (1) An algebraic approach for representing rewrite rules and their semantics. This facilitates reasoning about complex
symbolic
rewrite rules that are beyond the scope of existing techniques. (2) A fast approach for probabilistically verifying equivalence of quantum circuits by reducing the problem to a special form of
polynomial identity testing
. (3) A novel probabilistic data structure, called a
polynomial identity filter
(PIF), for efficiently synthesizing rewrite rules. (4) A beam-search-based algorithm that efficiently applies the synthesized symbolic rewrite rules to optimize quantum circuits.
Trace-Guided Inductive Synthesis of Recursive Functional Programs
Authors: Yuan Yongwei , Radhakrishna Arjun , Samanta Roopsha
Published: June 2023

We propose a novel trace-guided approach to tackle the challenges of ambiguity and generalization in synthesis of recursive functional programs from input-output examples. Our approach augments the search space of programs with recursion traces consisting of recursive subcalls of the programs. Our method is based on a new version space algebra (VSA) for succinct representation and efficient manipulation of pairs of recursion traces and programs that are consistent with each other. We have implemented this approach in a tool called SyRup and evaluated it on benchmarks from prior work. Our evaluation demonstrates that SyRup not only requires fewer examples to achieve a certain success rate than existing synthesizers, but is also less sensitive to the quality of the examples.
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%.
Derivative Based Nonbacktracking Real-World Regex Matching with Backtracking Semantics
Authors: Moseley Dan , Nishio Mario , Perez Rodriguez Jose , Saarikivi Olli , Toub Stephen , Veanes Margus , Wan Tiki , Xu Eric
Published: June 2023

We develop a new derivative based theory and algorithm for nonbacktracking regex matching that supports anchors and counting, preserves backtracking semantics, and can be extended with lookarounds. The algorithm has been implemented as a new regex backend in .NET and was extensively tested as part of the formal release process of .NET7. We present a formal proof of the correctness of the algorithm, which we believe to be the first of its kind concerning industrial implementations of regex matchers. The paper describes the complete foundation, the matching algorithm, and key aspects of the implementation involving a regex rewrite system, as well as a comprehensive evaluation over industrial case studies and other regex engines.
Indexed Streams: A Formal Intermediate Representation for Fused Contraction Programs
Authors: Kovach Scott , Kolichala Praneeth , Gu Tiancheng , Kjolstad Fredrik
Published: June 2023

We introduce indexed streams, a formal operational model and intermediate representation that describes the fused execution of a contraction language that encompasses both sparse tensor algebra and relational algebra. We prove that the indexed stream model is correct with respect to a functional semantics. We also develop a compiler for contraction expressions that uses indexed streams as an intermediate representation. The compiler is only 540 lines of code, but we show that its performance can match both the TACO compiler for sparse tensor algebra and the SQLite and DuckDB query processing libraries for relational algebra.
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.
Search-Based Regular Expression Inference on a GPU
Authors: Valizadeh Mojtaba , Berger Martin
Published: June 2023

Regular expression inference (REI) is a supervised machine learning and program synthesis problem that takes a cost metric for regular expressions, and positive and negative examples of strings as input. It outputs a regular expression that is precise (i.e., accepts all positive and rejects all negative examples), and minimal w.r.t. to the cost metric. We present a novel algorithm for REI over arbitrary alphabets that is enumerative and trades off time for space. Our main algorithmic idea is to implement the search space of regular expressions succinctly as a contiguous matrix of bitvectors. Collectively, the bitvectors represent, as characteristic sequences, all sub-languages of the infix-closure of the union of positive and negative examples. Mathematically, this is a semiring of (a variant of) formal power series. Infix-closure enables bottom-up compositional construction of larger from smaller regular expressions using the operations of our semiring. This minimises data movement and data-dependent branching, hence maximises data-parallelism. In addition, the infix-closure remains unchanged during the search, hence search can be staged: first pre-compute various expensive operations, and then run the compute intensive search process. We provide two C++ implementations, one for general purpose CPUs and one for Nvidia GPUs (using CUDA). We benchmark both on Google Colab Pro: the GPU implementation is on average over 1000x faster than the CPU implementation on the hardest benchmarks.
Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic
Authors: Mulder Ike , Czajka Łukasz , Krebbers Robbert
Published: June 2023

Concurrent separation logic has been responsible for major advances in the formal verification of fine-grained concurrent algorithms and data structures such as locks, barriers, queues, and reference counters. The key ingredient of the verification of a fine-grained program is an invariant, which relates the physical data representation (on the heap) to a logical representation (in mathematics) and to the state of the threads (using a form of ghost state). An invariant is typically represented as a disjunction of logical states, but this disjunctive nature makes invariants a difficult target for automated verification. Current approaches roughly suffer from two problems. They use backtracking to introduce disjunctions in an uninformed manner, which can lead to unprovable goals if an appropriate case analysis has not been made before choosing the disjunct. Moreover, they eliminate disjunctions too eagerly, which can cause poor efficiency.

While disjunctions are no problem for automated provers based on classical (i.e., non-separating) logic, the challenges with disjunctions are prominent in the study of proof automation for intuitionistic logic. We take inspiration from that area—specifically, based on ideas from
connection calculus
, we design a simple multi-succedent calculus for separation logic with disjunctions featuring a novel concept of a
connection
. While our calculus is not complete, it has the advantage that it can be extended with features of the state-of-the-art concurrent separation logic Iris (such as modalities, higher-order quantification, ghost state, and invariants), and can be implemented effectively in the Coq proof assistant with little need for backtracking. We evaluate the practicality on 24 challenging benchmarks, 14 of which we can verify fully automatically.
Parameterized Algebraic Protocols
Authors: Mordido Andreia , Spaderna Janek , Thiemann Peter , Vasconcelos Vasco T.
Published: June 2023

We propose algebraic protocols that enable the definition of protocol templates and session types analogous to the definition of domain-specific types with algebraic datatypes. Parameterized algebraic protocols subsume all regular as well as most context-free and nested session types and, at the same time, replace the expensive superlinear algorithms for type checking by a nominal check that runs in linear time. Algebraic protocols in combination with polymorphism increase expressiveness and modularity by facilitating new ways of parameterizing and composing session types.
Scallop: A Language for Neurosymbolic Programming
Authors: Li Ziyang , Huang Jiani , Naik Mayur
Published: June 2023

We present Scallop, a language which combines the benefits of deep learning and logical reasoning. Scallop enables users to write a wide range of neurosymbolic applications and train them in a data- and compute-efficient manner. It achieves these goals through three key features: 1) a flexible symbolic representation that is based on the relational data model; 2) a declarative logic programming language that is based on Datalog and supports recursion, aggregation, and negation; and 3) a framework for automatic and efficient differentiable reasoning that is based on the theory of provenance semirings. We evaluate Scallop on a suite of eight neurosymbolic applications from the literature. Our evaluation demonstrates that Scallop is capable of expressing algorithmic reasoning in diverse and challenging AI tasks, provides a succinct interface for machine learning programmers to integrate logical domain knowledge, and yields solutions that are comparable or superior to state-of-the-art models in terms of accuracy. Furthermore, Scallop's solutions outperform these models in aspects such as runtime and data efficiency, interpretability, and generalizability.
Inductive Program Synthesis via Iterative Forward-Backward Abstract Interpretation
Authors: Yoon Yongho , Lee Woosuk , Yi Kwangkeun
Published: June 2023

A key challenge in example-based program synthesis is the gigantic search space of programs. To address this challenge, various work proposed to use abstract interpretation to prune the search space. However, most of existing approaches have focused only on forward abstract interpretation, and thus cannot fully exploit the power of abstract interpretation. In this paper, we propose a novel approach to inductive program synthesis via iterative forward-backward abstract interpretation. The forward abstract interpretation computes possible outputs of a program given inputs, while the backward abstract interpretation computes possible inputs of a program given outputs. By iteratively performing the two abstract interpretations in an alternating fashion, we can effectively determine if any completion of each partial program as a candidate can satisfy the input-output examples. We apply our approach to a standard formulation, syntax-guided synthesis (SyGuS), thereby supporting a wide range of inductive synthesis tasks. We have implemented our approach and evaluated it on a set of benchmarks from the prior work. The experimental results show that our approach significantly outperforms the state-of-the-art approaches thanks to the sophisticated abstract interpretation techniques.
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.
Synthesizing MILP Constraints for Efficient and Robust Optimization
Authors: Wang Jingbo , Gupta Aarti , Wang Chao
Published: June 2023

While mixed integer linear programming (MILP) solvers are routinely used to solve a wide range of important science and engineering problems, it remains a challenging task for end users to write correct and efficient MILP constraints, especially for problems specified using the inherently non-linear Boolean logic operations. To overcome this challenge, we propose a syntax guided synthesis (SyGuS) method capable of generating high-quality MILP constraints from the specifications expressed using arbitrary combinations of Boolean logic operations. At the center of our method is an extensible domain specification language (DSL) whose expressiveness may be improved by adding new integer variables as decision variables, together with an iterative procedure for synthesizing linear constraints from non-linear Boolean logic operations using these integer variables. To make the synthesis method efficient, we also propose an over-approximation technique for soundly proving the correctness of the synthesized linear constraints, and an under-approximation technique for safely pruning away the incorrect constraints. We have implemented and evaluated the method on a wide range of benchmark specifications from statistics, machine learning, and data science applications. The experimental results show that the method is efficient in handling these benchmarks, and the quality of the synthesized MILP constraints is close to, or higher than, that of manually-written constraints in terms of both compactness and solving time.
Incremental Verification of Neural Networks
Authors: Ugare Shubham , Banerjee Debangshu , Misailovic Sasa , Singh Gagandeep
Published: June 2023

Complete verification of deep neural networks (DNNs) can exactly determine whether the DNN satisfies a desired trustworthy property (e.g., robustness, fairness) on an infinite set of inputs or not. Despite the tremendous progress to improve the scalability of complete verifiers over the years on individual DNNs, they are inherently inefficient when a deployed DNN is updated to improve its inference speed or accuracy. The inefficiency is because the expensive verifier needs to be run from scratch on the updated DNN. To improve efficiency, we propose a new, general framework for incremental and complete DNN verification based on the design of novel theory, data structure, and algorithms. Our contributions implemented in a tool named IVAN yield an overall geometric mean speedup of 2.4x for verifying challenging MNIST and CIFAR10 classifiers and a geometric mean speedup of 3.8x for the ACAS-XU classifiers over the state-of-the-art baselines.
Stochastic-skill-level-based Shared Control for Human Training in Urban Air Mobility Scenario
Authors: Byeon Sooyung , Choi Joonwon , Zhang Yutong , Hwang Inseok
Published: June 2023

This article proposes a novel stochastic-skill-level-based shared control framework to assist human novices to emulate human experts in complex dynamic control tasks. The proposed framework aims to infer stochastic-skill-levels (SSLs) of the human novices and provide personalized assistance based on the inferred SSLs. SSL can be assessed as a stochastic variable that denotes the probability that the novice will behave similarly to experts. We propose a data-driven method that can characterize novice demonstrations as a novice model and expert demonstrations as an expert model, respectively. Then, our SSL inference approach utilizes the novice and expert models to assess the SSL of the novices in complex dynamic control tasks. The shared control scheme is designed to dynamically adjust the level of assistance based on the inferred SSL to prevent frustration or tedium during human training due to poorly imposed assistance. The proposed framework is demonstrated by a human subject experiment in a human training scenario for a remotely piloted urban air mobility vehicle. The results show that the proposed framework can assess the SSL and tailor the assistance for an individual in real time. The proposed framework is compared to practice-only training (no assistance) and a baseline shared control approach to test the human learning rates in the designed training scenario with human subjects. A subjective survey is also examined to monitor the user experience of the proposed framework.
Efficient Computation of Optimal Thresholds in Cloud Auto-scaling Systems
Authors: Tournaire Thomas , Castel-Taleb Hind , Hyon Emmanuel
Published: June 2023

We consider a horizontal and dynamic auto-scaling technique in a cloud system where virtual machines hosted on a physical node are turned on and off to minimise energy consumption while meeting performance requirements. Finding cloud management policies that adapt the system to the load is not straightforward, and we consider here that virtual machines are turned on and off depending on queue load thresholds. We want to compute the optimal threshold values that minimize consumption costs and penalty costs (when performance requirements are not met). To solve this problem, we propose several optimisation methods, based on two different mathematical approaches. The first one is based on queueing theory and uses local search heuristics coupled with the stationary distributions of Markov chains. The second approach tackles the problem using Markov Decision Process (MDP) in which we assume that the policy is of a special multi-threshold type called hysteresis. We improve the heuristics of the former approach with the aggregation of Markov chains and queues approximation techniques. We assess the benefit of threshold-aware algorithms for solving MDPs. Then we carry out theoretical analyzes of the two approaches. We also compare them numerically and we show that all of the presented MDP algorithms strongly outperform the local search heuristics. Finally, we propose a cost model for a real scenario of a cloud system to apply our optimisation algorithms and to show their practical relevance. The major scientific contribution of the article is a set of fast (almost in real time) load-based threshold computation methods that can be used by a cloud provider to optimize its financial costs.
Enhanced H2S Gas Sensing Properties of the Hierarchical CuO Hollow Microspheres
Authors: Chao Yang , Zhang Huan , Li Jie , Wang Ai-Jing , Wang De-Cai , Jin Zhen
Published: June 2023

In present work, the hierarchical CuO hollow microspheres were synthesized through a facile hydrothermal method. The as-prepared samples were characterized by X-ray diffraction, scanning electron microscopy and transmission electron microscopy. The results show that the hierarchical CuO hollow microspheres with uniform size of 3 μm are self-assembled by hundreds of primary nanorods with diameters of about 20 nm. The wall thickness of the hollow microspheres is about 200 nm. The hierarchical CuO hollow microspheres exhibit good sensing performance in H2S detection. The optimal operating temperature is 180 °C. And, in a large range, the hierarchical CuO hollow microspheres display excellent linear sensing performance in ethanol detection. The detecting limit is lower to 1 ppm. Furthermore, the hierarchical CuO hollow microspheres demonstrate excellent selectivity in H2S detection. The sensing mechanism also has been discussed. It can be expected that the novel morphology of the hierarchical CuO hollow microspheres may bring amazing development for H2S detection.
Intrapulmonary arterial contraction assay reveals region-specific deregulation of vasoreactivity to lung injuries
Authors: Bai Yan , Li Guang , Yung Laiming , Yu Paul B. , Ai Xingbin
Published: June 2023

Utilizing mouse precision-cut lung slices with preserved intrapulmonary vessels, we demonstrated a location-dependent structural and contractile regulation of pulmonary arteries in health and on noxious stimulations. For instance, chronic ovalbumin and hypoxic exposure increased pulmonary arterial pressure (PAH) by remodeling intraacinar arterioles to reduce vascular wall compliance while enhancing vasoconstriction in proximal preacinar arteries. These findings suggest region-specific mechanisms and therapeutic targets for pulmonary vascular diseases such as PAH.
Prediction of Alzheimer’s Disease Using DHO‐Based Pretrained CNN Model
Authors: Venkatasubramanian S. , Dwivedi Jaiprakash Narain , Raja S. , Rajeswari N. , Logeshwaran J. , Praveen Kumar Avvaru
Published: June 2023

Detecting Alzheimer’s disease (AD) early on allows patients to take preventative measures before the onset of irreversible brain damage, which is a critical factor in the treatment of Alzheimer’s patients. Most machine detection methods are constrained by congenital observations, although computers have been utilized in several recent research studies to diagnose AD. In AD, the hippocampus is usually the first part of the brain to be affected. Structural magnetic resonance imaging (SMRI) can be used to assist in diagnosing AD by measuring the hippocampus’s form and volume (MRI). The information encoded by these attributes is restricted and may be affected by segmentation problems. These traits are also extracted independently of the classification, which could result in lower‐than‐desired classification accuracy. Researchers in this study used structural MRI data to develop a deep learning framework for combined automatic hippocampus segmentation and AD categorization. Multi‐task deep learning (MTDL) is used to learn hippocampus segmentation simultaneously. The hyperparameter optimization of the CNN model (capsule network) for illness classification is then carried out using the deer hunting optimization (DHO) technique. ADNI‐standardized MRI datasets have been used to test the suggested method, and it is accurate. Suggested MTDL achieved 97.1% accuracy and 93.5% of Dice coefficient, whereas the proposed MTDL model achieved an accuracy of 96% for binary classification and 93% for multi‐class classification.
Patient Involvement in Decisions regarding Emergency Department Discharge: A Multimethod Study
Authors: Thise Rasmussen Marie Louise , Lomborg Kirsten , Iversen Kasper Karmark , Konradsen Hanne
Published: June 2023

Background. Unmet care needs and more than one reasonable discharge solution have been identified among patients in the emergency department. Less than half of the patients attending emergency care have reported being involved in decisions to the degree they have wanted. Having a person-centered approach, such as involving patients in decisions regarding their discharge, has been reported as being associated with beneficial outcomes for the patient. Aim. The aim of the study was to explore the extent of patients’ involvement in discharge planning in acute care and how patient involvement in decisions regarding discharge planning is managed in clinical practice. Methods. A multimethod study, including both quantitative and qualitative data, was carried out. The quantitative part included a descriptive and comparative analysis of additional data from the patient’s medical records and patient’s responses to the CollaboRATE questionnaire. The qualitative part included a content analysis of notes from field studies of interactions between healthcare professionals and patients. Results. A total of 615 patients from an emergency department at a medium-sized hospital completed the questionnaire. Roughly, a third gave top-box scores (36%), indicating optimal involvement in decisions. Two factors, being discharged home and not readmitted, were significantly associated with the experience of being involved. In clinical practice, there was a focus on symptoms, and diagnostic tools and choice of treatment were decisive for the further care trajectory of the patients. Speed and low continuity left limited opportunities for dialogue to uncover patients’ preferences. At the same time, the patients did not expect to be involved. Conclusions. Two out of three patients did not experience being involved in decisions regarding emergency department discharge. The interactions reflected an organizational structure in which the conditions for patient involvement were limited. Uncovering opportunities and initiatives to increase the number of patients who experience being involved in decisions is important tasks for the future.
Investigating the Genetic Evolution of PCV2 and PCV3 across Six Swine Herds in China from 2020 to 2021
Authors: Cui Chenchen , Wang Menghang , Zhang Qianru , Wang Shujie , Zhang Hongliang , Tian Zhijun , An Tongqing , Cai Xuehui , Wang Gang
Published: June 2023

To elucidate the prevalence, molecular evolution, and coinfection of PCV2 and PCV3 in China, we collected samples from six large-scale swine herds located in Heilongjiang, Henan, Hebei, and Hubei provinces and Xinjiang Uygur autonomous region from 2020 to 2021. Overall, 1,201 samples were analyzed and sequenced by PCR to identify the dominant genotypes of PCV2 and PCV3, and genetic variations in the capsid protein genes of PCV2 and PCV3 were evaluated. The major epidemic genotypes of PCV2 and PCV3 were different across different regions. The infection rate of PCV2 and PCV3 was 72.1% and 26.3%, respectively, and the coinfection rate was 18.6%. PCV2d was the dominant genotype across all herds. The PCV2d-positive rate in PCV2-positive samples was 93.5%–100% in five out of six herds, indicative of its predominance. PCV3 prevalence in China widely varied, and no dominant genotype was identified. Four, 21, 11, and 11 strains with PCV2a, PCV2d, PCV3a, and PCV3c genotypes were detected, respectively, with the capsid protein containing four, five, eight, and three aa sites with mutations, respectively. Overall, our findings revealed the dominant epidemic genotypes of PCV2 and PCV3 in six herds across five provinces in China, in addition to the main aa sites with mutations in the capsid protein. We believe that these results will facilitate the diagnosis, prevention, and control of PCV2 and PCV3 in China.
Statin Eligibility according to 2013 ACC/AHA and USPSTF Guidelines among Jordanian Patients with Acute Myocardial Infarction: The Impact of Gender
Authors: Ibdah Rashid , Alrawashdeh Ahmad , Rawashdeh Sukaina , Melhem Nebras Y. , Hammoudeh Ayman J. , Jarrah Mohamad I.
Published: June 2023

The objectives of this study were to evaluate statin eligibility among Middle Eastern patients admitted with acute myocardial infarction (AMI) who had no prior use of statin therapy, according to 2013 ACC/AHA and 2016 USPSTF guidelines, and to compare statin eligibility between men and women. This was a retrospective multicenter observational study of all adult patients admitted to five tertiary care centers in Jordan with a first-time AMI, no prior cardiovascular disease, and no prior statin use between April 2018 and June 2019. Ten-year atherosclerotic cardiovascular disease (ASCVD) risk score was estimated based on ACC/AHA risk score. A total of 774 patients met the inclusion criteria. The mean age was 55 years (

SD
±
11.3

), 120 (15.5%) were women, and 688 (88.9%) had at least one risk factor of cardiovascular disease. Compared to men, women were more likely to be older; had a history of diabetes, hypertension, and hypercholesterolemia; and had higher body mass index, systolic blood pressure, total cholesterol, and high-density lipoproteins. Compared to women, men were more likely to have a higher 10-year ASCVD risk score (14.0% vs. 17.8%,

p
=
0.005

), and more men had a 10-year ASCVD risk score of ≥7.5% and ≥10%. The proportion of patients eligible for statin therapy was 80.2% based on the 2013 ACC/AHA guidelines and 59.5% based on the USPSTF guidelines. A higher proportion of men were eligible for statin therapy compared to women, based on both the 2013 ACC/AHA (81.4% vs. 73.5%,

p
=
0.050

) and USPSTF guidelines (62.0% vs. 45.2%,

p
=
0.001

). Among Middle Easterners, over half of patients with AMI would have been eligible for statin therapy prior to admission based on the 2013 ACC/AHA and USPSTF guidelines, with the presence of gender gap. Adopting these guidelines in clinical practice might positively impact primary cardiovascular preventive strategies in this region.
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.