bluuebunny/crossref_metadata_2025 huggingface dataset:
A separation logic for heap space under garbage collection
Authors: Madiot Jean-Marie , Pottier François
Published: January 2022

We present SL♢, a Separation Logic that allows controlling the heap space consumption of a program in the presence of dynamic memory allocation and garbage collection. A user of the logic works with space credits, a resource that is consumed when an object is allocated and produced when a group of objects is logically deallocated, that is, when the user is able to prove that it has become unreachable and therefore can be collected. To prove such a fact, the user maintains pointed-by assertions that record the immediate predecessors of every object. Our calculus, SpaceLang, has mutable state, shared-memory concurrency, and code pointers. We prove that SL♢ is sound and present several simple examples of its use.
Property-directed reachability as abstract interpretation in the monotone theory
Authors: Feldman Yotam M. Y. , Sagiv Mooly , Shoham Sharon , Wilcox James R.
Published: January 2022

Inferring inductive invariants is one of the main challenges of formal verification. The theory of abstract interpretation provides a rich framework to devise invariant inference algorithms. One of the latest breakthroughs in invariant inference is property-directed reachability (PDR), but the research community views PDR and abstract interpretation as mostly unrelated techniques.

This paper shows that, surprisingly, propositional PDR can be formulated as an abstract interpretation algorithm in a logical domain. More precisely, we define a version of PDR, called Λ-PDR, in which all generalizations of counterexamples are used to strengthen a frame. In this way, there is no need to refine frames after their creation, because all the possible supporting facts are included in advance. We analyze this algorithm using notions from Bshouty’s monotone theory, originally developed in the context of exact learning. We show that there is an inherent overapproximation between the algorithm’s frames that is related to the monotone theory. We then define a new abstract domain in which the best abstract transformer performs this overapproximation, and show that it captures the invariant inference process, i.e., Λ-PDR corresponds to Kleene iterations with the best transformer in this abstract domain. We provide some sufficient conditions for when this process converges in a small number of iterations, with sometimes an exponential gap from the number of iterations required for naive exact forward reachability. These results provide a firm theoretical foundation for the benefits of how PDR tackles forward reachability.
Effectful program distancing
Authors: Dal Lago Ugo , Gavazzo Francesco
Published: January 2022

Semantics is traditionally concerned with program equivalence, in which all pairs of programs which are
not
equivalent are treated the same, and simply dubbed as incomparable. In recent years, various forms of program
metrics
have been introduced such that the distance between non-equivalent programs is measured as an element of an appropriate quantale. By letting the underlying quantale
vary
as the type of the compared programs become more complex, the recently introduced framework of differential logical relations allows for a new contextual form of reasoning. In this paper, we show that all this can be generalised to
effectful
higher-order programs, in which not only the
values
, but also the
effects
computations produce can be appropriately distanced in a principled way. We show that the resulting framework is flexible, allowing various forms of effects to be handled, and that it provides compact and informative judgments about program differences.
VIP: verifying real-world C idioms with integer-pointer casts
Authors: Lepigre Rodolphe , Sammler Michael , Memarian Kayvan , Krebbers Robbert , Dreyer Derek , Sewell Peter
Published: January 2022

Systems code often requires fine-grained control over memory layout and pointers, expressed using low-level (
e.g.
, bitwise) operations on pointer values. Since these operations go beyond what basic pointer arithmetic in C allows, they are performed with the help of
integer-pointer casts
. Prior work has explored increasingly realistic memory object models for C that account for the desired semantics of integer-pointer casts while also being sound w.r.t. compiler optimisations, culminating in PNVI, the preferred memory object model in ongoing discussions within the ISO WG14 C standards committee. However, its complexity makes it an unappealing target for verification, and no tools currently exist to verify C programs under PNVI.

In this paper, we introduce VIP, a new memory object model aimed at supporting C verification. VIP sidesteps the complexities of PNVI with a simple but effective idea: a new construct that lets programmers express the intended provenances of integer-pointer casts explicitly. At the same time, we prove VIP compatible with PNVI, thus enabling verification on top of VIP to benefit from PNVI’s validation with respect to practice. In particular, we build a verification tool, RefinedC-VIP, for verifying programs under VIP semantics. As the name suggests, RefinedC-VIP extends the recently developed RefinedC tool, which is automated yet also produces foundational proofs in Coq. We evaluate RefinedC-VIP on a range of systems-code idioms, and validate VIP’s expressiveness via an implementation in the Cerberus C semantics.
Bottom-up synthesis of recursive functional programs using angelic execution
Authors: Miltner Anders , Nuñez Adrian Trejo , Brendel Ana , Chaudhuri Swarat , Dillig Isil
Published: January 2022

We present a novel bottom-up method for the synthesis of functional recursive programs. While bottom-up synthesis techniques can work better than top-down methods in certain settings, there is no prior technique for synthesizing recursive programs from logical specifications in a purely bottom-up fashion. The main challenge is that effective bottom-up methods need to execute sub-expressions of the code being synthesized, but it is impossible to execute a recursive subexpression of a program that has not been fully constructed yet. In this paper, we address this challenge using the concept of angelic semantics. Specifically, our method finds a program that satisfies the specification under angelic semantics (we refer to this as angelic synthesis), analyzes the assumptions made during its angelic execution, uses this analysis to strengthen the specification, and finally reattempts synthesis with the strengthened specification. Our proposed angelic synthesis algorithm is based on version space learning and therefore deals effectively with many incremental synthesis calls made during the overall algorithm. We have implemented this approach in a prototype called Burst and evaluate it on synthesis problems from prior work. Our experiments show that Burst is able to synthesize a solution to 94% of the benchmarks in our benchmark suite, outperforming prior work.
Semantics for variational Quantum programming
Authors: Jia Xiaodong , Kornell Andre , Lindenhovius Bert , Mislove Michael , Zamdzhiev Vladimir
Published: January 2022

We consider a programming language that can manipulate both classical and quantum information. Our language is type-safe and designed for variational quantum programming, which is a hybrid classical-quantum computational paradigm. The classical subsystem of the language is the Probabilistic FixPoint Calculus (PFPC), which is a lambda calculus with mixed-variance recursive types, term recursion and probabilistic choice. The quantum subsystem is a first-order linear type system that can manipulate quantum information. The two subsystems are related by mixed classical/quantum terms that specify how classical probabilistic effects are induced by quantum measurements, and conversely, how classical (probabilistic) programs can influence the quantum dynamics. We also describe a sound and computationally adequate denotational semantics for the language. Classical probabilistic effects are interpreted using a recently-described commutative probabilistic monad on DCPO. Quantum effects and resources are interpreted in a category of von Neumann algebras that we show is enriched over (continuous) domains. This strong sense of enrichment allows us to develop novel semantic methods that we use to interpret the relationship between the quantum and classical probabilistic effects. By doing so we provide a very detailed denotational analysis that relates domain-theoretic models of classical probabilistic programming to models of quantum programming.
Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI
Authors: Kolosick Matthew , Narayan Shravan , Johnson Evan , Watt Conrad , LeMay Michael , Garg Deepak , Jhala Ranjit , Stefan Deian
Published: January 2022

Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. Mozilla, for example, uses SFI to harden the Firefox browser by sandboxing third-party libraries, and companies like Fastly and Cloudflare use SFI to safely co-locate untrusted tenants on their edge clouds. While there have been significant efforts to optimize and verify SFI enforcement, context switching in SFI systems remains largely unexplored: almost all SFI systems use
heavyweight transitions
that are not only error-prone but incur significant performance overhead from saving, clearing, and restoring registers when context switching. We identify a set of
zero-cost conditions
that characterize when sandboxed code has sufficient structured to guarantee security via lightweight
zero-cost
transitions (simple function calls). We modify the Lucet Wasm compiler and its runtime to use zero-cost transitions, eliminating the undue performance tax on systems that rely on Lucet for sandboxing (e.g., we speed up image and font rendering in Firefox by up to 29.7% and 10% respectively). To remove the Lucet compiler and its correct implementation of the Wasm specification from the trusted computing base, we (1) develop a
static binary verifier
, VeriZero, which (in seconds) checks that binaries produced by Lucet satisfy our zero-cost conditions, and (2) prove the soundness of VeriZero by developing a logical relation that captures when a compiled Wasm function is semantically well-behaved with respect to our zero-cost conditions. Finally, we show that our model is useful beyond Wasm by describing a new, purpose-built SFI system, SegmentZero32, that uses x86 segmentation and LLVM with mostly off-the-shelf passes to enforce our zero-cost conditions; our prototype performs on-par with the state-of-the-art Native Client SFI system.
Twist: sound reasoning for purity and entanglement in Quantum programs
Authors: Yuan Charles , McNally Christopher , Carbin Michael
Published: January 2022

Quantum programming languages
enable developers to implement algorithms for quantum computers that promise computational breakthroughs in classically intractable tasks. Programming quantum computers requires awareness of
entanglement
, the phenomenon in which measurement outcomes of qubits are correlated. Entanglement can determine the correctness of algorithms and suitability of programming patterns.

In this work, we formalize
purity
as a central tool for automating reasoning about entanglement in quantum programs. A pure expression is one whose evaluation is unaffected by the measurement outcomes of qubits that it does not own, implying freedom from entanglement with any other expression in the computation.

We present Twist, the first language that features a type system for sound reasoning about purity. The type system enables the developer to identify pure expressions using type annotations. Twist also features purity assertion operators that state the absence of entanglement in the output of quantum gates. To soundly check these assertions, Twist uses a combination of static analysis and runtime verification.

We evaluate Twist’s type system and analyses on a benchmark suite of quantum programs in simulation, demonstrating that Twist can express quantum algorithms, catch programming errors in them, and support programs that existing languages disallow, while incurring runtime verification overhead of less than 3.5%.
Observational equality: now for good
Authors: Pujet Loïc , Tabareau Nicolas
Published: January 2022

Building on the recent extension of dependent type theory with a universe of definitionally proof-irrelevant types, we introduce TTobs, a new type theory based on the setoidal interpretation of dependent type theory. TTobs equips every type with an identity relation that satisfies function extensionality, propositional extensionality, and definitional uniqueness of identity proofs (UIP). Compared to other existing proposals to enrich dependent type theory with these principles, our theory features a notion of reduction that is normalizing and provides an algorithmic canonicity result, which we formally prove in Agda using the logical relation framework of Abel et al. Our paper thoroughly develops the meta-theoretical properties of TTobs, such as the decidability of the conversion and of the type checking, as well as consistency. We also explain how to extend our theory with quotient types, and we introduce a setoidal version of Swan's Id types that turn it into a proper extension of MLTT with inductive equality.
Visibility reasoning for concurrent snapshot algorithms
Authors: Öhman Joakim , Nanevski Aleksandar
Published: January 2022

Visibility relations have been proposed by Henzinger et al. as an abstraction for proving linearizability of concurrent algorithms that obtains modular and reusable proofs. This is in contrast to the customary approach based on exhibiting the algorithm's linearization points. In this paper we apply visibility relations to develop modular proofs for three elegant concurrent snapshot algorithms of Jayanti. The proofs are divided by signatures into components of increasing level of abstraction; the components at higher abstraction levels are shared, i.e., they apply to all three algorithms simultaneously. Importantly, the interface properties mathematically capture Jayanti's original intuitions that have previously been given only informally.
Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itself
Authors: Jang Junyoung , Gélineau Samuel , Monnier Stefan , Pientka Brigitte
Published: January 2022

We describe the foundation of the metaprogramming language, Mœbius, which supports the generation of polymorphic code and, more importantly, the analysis of polymorphic code via pattern matching.

Mœbius has two main ingredients: 1) we exploit contextual modal types to describe open code together with the context in which it is meaningful. In Mœbius, open code can depend on type and term variables (level 0) whose values are supplied at a later stage, as well as code variables (level 1) that stand for code templates supplied at a later stage. This leads to a multi-level modal lambda-calculus that supports System-F style polymorphism and forms the basis for polymorphic code generation. 2) we extend the multi-level modal lambda-calculus to support pattern matching on code. As pattern matching on polymorphic code may refine polymorphic type variables, we extend our type-theoretic foundation to generate and track typing constraints that arise. We also give an operational semantics and prove type preservation.

Our multi-level modal foundation for Mœbius provides the appropriate abstractions for both generating and pattern matching on open code without committing to a concrete representation of variable binding and contexts. Hence, our work is a step towards building a general type-theoretic foundation for multi-staged metaprogramming that, on the one hand, enforces strong type guarantees and, on the other hand, makes it easy to generate and manipulate code. This will allow us to exploit the full potential of metaprogramming without sacrificing the reliability of and trust in the code we are producing and running.
Subcubic certificates for CFL reachability
Authors: Chistikov Dmitry , Majumdar Rupak , Schepper Philipp
Published: January 2022

Many problems in interprocedural program analysis can be modeled as the context-free language (CFL) reachability problem on graphs and can be solved in cubic time. Despite years of efforts, there are no known truly sub-cubic algorithms for this problem. We study the related
certification
task: given an instance of CFL reachability, are there small and efficiently checkable certificates for the existence and for the non-existence of a path? We show that, in both scenarios, there exist succinct certificates (
O
(
n
2
) in the size of the problem) and these certificates can be checked in subcubic (matrix multiplication) time. The certificates are based on grammar-based compression of paths (for reachability) and on invariants represented as matrix inequalities (for non-reachability). Thus, CFL reachability lies in nondeterministic and co-nondeterministic
subcubic
time.

A natural question is whether faster algorithms for CFL reachability will lead to faster algorithms for combinatorial problems such as Boolean satisfiability (SAT). As a consequence of our certification results, we show that there cannot be a fine-grained reduction from SAT to CFL reachability for a conditional lower bound stronger than
n
ω
, unless the nondeterministic strong exponential time hypothesis (NSETH) fails. In a nutshell, reductions from SAT are unlikely to explain the cubic bottleneck for CFL reachability.

Our results extend to related subcubic equivalent problems: pushdown reachability and 2NPDA recognition; as well as to all-pairs CFL reachability. For example, we describe succinct certificates for pushdown non-reachability (inductive invariants) and observe that they can be checked in matrix multiplication time. We also extract a new hardest 2NPDA language, capturing the “hard core” of all these problems.
Layered and object-based game semantics
Authors: Oliveira Vale Arthur , Melliès Paul-André , Shao Zhong , Koenig Jérémie , Stefanesco Léo
Published: January 2022

Large-scale software verification relies critically on the use of compositional languages, semantic models, specifications, and verification techniques. Recent work on certified abstraction layers synthesizes game semantics, the refinement calculus, and algebraic effects to enable the composition of heterogeneous components into larger certified systems. However, in existing models of certified abstraction layers, compositionality is restricted by the lack of encapsulation of state.

In this paper, we present a novel game model for certified abstraction layers where the semantics of layer interfaces and implementations are defined solely based on their observable behaviors. Our key idea is to leverage Reddy's pioneer work on modeling the semantics of imperative languages not as functions on global states but as objects with their observable behaviors. We show that a layer interface can be modeled as an object type (i.e., a layer signature) plus an object strategy. A layer implementation is then essentially a regular map, in the sense of Reddy, from an object with the underlay signature to that with the overlay signature. A layer implementation is certified when its composition with the underlay object strategy implements the overlay object strategy. We also describe an extension that allows for non-determinism in layer interfaces.

After formulating layer implementations as regular maps between object spaces, we move to concurrency and design a notion of concurrent object space, where sequential traces may be identified modulo permutation of independent operations. We show how to express protected shared object concurrency, and a ticket lock implementation, in a simple model based on regular maps between concurrent object spaces.
Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation
Authors: Krawiec Faustyna , Peyton Jones Simon , Krishnaswami Neel , Ellis Tom , Eisenberg Richard A. , Fitzgibbon Andrew
Published: January 2022

In this paper, we give a simple and efficient implementation of reverse-mode automatic differentiation, which both extends easily to higher-order functions, and has run time and memory consumption linear in the run time of the original program. In addition to a formal description of the translation, we also describe an implementation of this algorithm, and prove its correctness by means of a logical relations argument.
Induction duality: primal-dual search for invariants
Authors: Padon Oded , Wilcox James R. , Koenig Jason R. , McMillan Kenneth L. , Aiken Alex
Published: January 2022

Many invariant inference techniques reason simultaneously about states and predicates, and it is well-known that these two kinds of reasoning are in some sense dual to each other. We present a new formal duality between states and predicates, and use it to derive a new primal-dual invariant inference algorithm. The new
induction duality
is based on a notion of provability by incremental induction that is formally dual to reachability, and the duality is surprisingly symmetric. The symmetry allows us to derive the dual of the well-known Houdini algorithm, and by combining Houdini with its dual image we obtain
primal-dual Houdini
, the first truly primal-dual invariant inference algorithm. An early prototype of primal-dual Houdini for the domain of distributed protocol verification can handle difficult benchmarks from the literature.
Oblivious algebraic data types
Authors: Ye Qianchuan , Delaware Benjamin
Published: January 2022

Secure computation allows multiple parties to compute joint functions over private data without leaking any sensitive data, typically using powerful cryptographic techniques. Writing secure applications using these techniques directly can be challenging, resulting in the development of several programming languages and compilers that aim to make secure computation accessible. Unfortunately, many of these languages either lack or have limited support for rich recursive data structures, like trees. In this paper, we propose a novel representation of structured data types, which we call oblivious algebraic data types, and a language for writing secure computations using them. This language combines dependent types with constructs for oblivious computation, and provides a security-type system which ensures that adversaries can learn nothing more than the result of a computation. Using this language, authors can write a single function over private data, and then easily build an equivalent secure computation according to a desired public view of their data.
The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency
Authors: Jeffrey Alan , Riely James , Batty Mark , Cooksey Simon , Kaysin Ilya , Podkopaev Anton
Published: January 2022

Program logics and semantics tell a pleasant story about sequential composition: when executing (S1;S2), we first execute S1 then S2. To improve performance, however, processors execute instructions out of order, and compilers reorder programs even more dramatically. By design, single-threaded systems cannot observe these reorderings; however, multiple-threaded systems can, making the story considerably less pleasant. A formal attempt to understand the resulting mess is known as a “relaxed memory model.” Prior models either fail to address sequential composition directly, or overly restrict processors and compilers, or permit nonsense thin-air behaviors which are unobservable in practice.

To support sequential composition while targeting modern hardware, we enrich the standard event-based approach with preconditions and families of predicate transformers. When calculating the meaning of (S1; S2), the predicate transformer applied to the precondition of an event e from S2 is chosen based on the set of events in S1 upon which e depends. We apply this approach to two existing memory models.
Partial (In)Completeness in abstract interpretation: limiting the imprecision in program analysis
Authors: Campion Marco , Dalla Preda Mila , Giacobazzi Roberto
Published: January 2022

Imprecision is inherent in any decidable (sound) approximation of undecidable program properties. In abstract interpretation this corresponds to the release of false alarms, e.g., when it is used for program analysis and program verification. As all alarming systems, a program analysis tool is credible when few false alarms are reported. As a consequence, we have to live together with false alarms, but also we need methods to control them. As for all approximation methods, also for abstract interpretation we need to estimate the accumulated imprecision during program analysis. In this paper we introduce a theory for estimating the error propagation in abstract interpretation, and hence in program analysis. We enrich abstract domains with a weakening of a metric distance. This enriched structure keeps coherence between the standard partial order relating approximated objects by their relative precision and the effective error made in this approximation. An abstract interpretation is precise when it is complete. We introduce the notion of partial completeness as a weakening of precision. In partial completeness the abstract interpreter may produce a bounded number of false alarms. We prove the key recursive properties of the class of programs for which an abstract interpreter is partially complete with a given bound of imprecision. Then, we introduce a proof system for estimating an upper bound of the error accumulated by the abstract interpreter during program analysis. Our framework is general enough to be instantiated to most known metrics for abstract domains.
Avoiding Overfitting: A Survey on Regularization Methods for Convolutional Neural Networks
Authors: Santos Claudio Filipi Gonçalves Dos , Papa João Paulo
Published: January 2022

Several image processing tasks, such as image classification and object detection, have been significantly improved using Convolutional Neural Networks (CNN). Like ResNet and EfficientNet, many architectures have achieved outstanding results in at least one dataset by the time of their creation. A critical factor in training concerns the network’s regularization, which prevents the structure from overfitting. This work analyzes several regularization methods developed in the past few years, showing significant improvements for different CNN models. The works are classified into three main areas: the first one is called “data augmentation,” where all the techniques focus on performing changes in the input data. The second, named “internal changes,” aims to describe procedures to modify the feature maps generated by the neural network or the kernels. The last one, called “label,” concerns transforming the labels of a given input. This work presents two main differences comparing to other available surveys about regularization: (i) the first concerns the papers gathered in the manuscript, which are not older than five years, and (ii) the second distinction is about reproducibility, i.e., all works referred here have their code available in public repositories or they have been directly implemented in some framework, such as TensorFlow or Torch.
Machine Learning-based Orchestration of Containers: A Taxonomy and Future Directions
Authors: Zhong Zhiheng , Xu Minxian , Rodriguez Maria Alejandra , Xu Chengzhong , Buyya Rajkumar
Published: January 2022

Containerization is a lightweight application virtualization technology, providing high environmental consistency, operating system distribution portability, and resource isolation. Existing mainstream cloud service providers have prevalently adopted container technologies in their distributed system infrastructures for automated application management. To handle the automation of deployment, maintenance, autoscaling, and networking of containerized applications, container orchestration is proposed as an essential research problem. However, the highly dynamic and diverse feature of cloud workloads and environments considerably raises the complexity of orchestration mechanisms. Machine learning algorithms are accordingly employed by container orchestration systems for behavior modeling and prediction of multi-dimensional performance metrics. Such insights could further improve the quality of resource provisioning decisions in response to the changing workloads under complex environments. In this article, we present a comprehensive literature review of existing machine learning-based container orchestration approaches. Detailed taxonomies are proposed to classify the current researches by their common features. Moreover, the evolution of machine learning-based container orchestration technologies from the year 2016 to 2021 has been designed based on objectives and metrics. A comparative analysis of the reviewed techniques is conducted according to the proposed taxonomies, with emphasis on their key characteristics. Finally, various open research challenges and potential future directions are highlighted.
Approximate GCD by relaxed NewtonSLRA algorithm
Authors: Nagasaka Kosaku
Published: January 2022

We propose a better algorithm for approximate greatest common divisor (approximate GCD) of univariate polynomials in terms of robustness and distance, based on the NewtonSLRA algorithm that is a solver for the structured low rank approximation (SLRA) problem. Our algorithm mainly enlarges the tangent space in the NewtonSLRA algorithm and adapts it to a certain weighted Frobenius norm. Moreover, we propose some improvement in computing time.
Cellular reductions of the Pommaret-Seiler resolution for Quasi-stable ideals
Authors: Iglesias Rodrigo , de Cabezón Eduardo Sáenz
Published: January 2022

Involutive bases were introduced in [6] as a type of Gröbner bases with additional combinatorial properties. Pommaret bases are a particular kind of involutive bases with strong relations to commutative algebra and algebraic geometry[11, 12].
Abstracts of recent doctoral dissertations in computer algebra
Authors: editors CCA
Published: January 2022

Each quarter we are pleased to present abstracts of recent doctoral dissertations in Computer Algebra and Symbolic Computation. We encourage all recent Ph.D. graduates who have defended in the past two years (and their supervisors), to submit their abstracts for publication in CCA.
Social Connection as a Public Health Issue: The Evidence and a Systemic Framework for Prioritizing the “Social” in Social Determinants of Health
Authors: Holt-Lunstad Julianne
Published: January 2022

There is growing interest in and renewed support for prioritizing social factors in public health both in the USA and globally. While there are multiple widely recognized social determinants of health, indicators of social connectedness (e.g., social capital, social support, social isolation, loneliness) are often noticeably absent from the discourse. This article provides an organizing framework for conceptualizing social connection and summarizes the cumulative evidence supporting its relevance for health, including epidemiological associations, pathways, and biological mechanisms. This evidence points to several implications for prioritizing social connection within solutions across sectors, where public health work, initiatives, and research play a key role in addressing gaps. Therefore, this review proposes a systemic framework for cross-sector action to identify missed opportunities and guide future investigation, intervention, practice, and policy on promoting social connection and health for all.
Review—MoSe2 Nanostructures and Related Electrodes for Advanced Supercapacitor Developments
Authors: Sha Rinky , Maity Palash Chandra , Rajaji Umamaheswari , Liu Ting-Yu , Bhattacharyya Tarun Kanti
Published: January 2022

Molybdenum diselenide (MoSe2), an in-organic analog of graphene, is considered a rising star in the family of transition-metal dichalcogenides (TMDs) because of its stable covalent Mo–Se bond, good catalytic properties, huge specific surface area, higher electrical, multivalent oxidation states of transition metal ions, and its ability to be intercalated with suitably-sized metal atoms or organic molecules to modify their physical properties with a distinguishing layered structure. It is being projected as the next-generation 2D layered nano-material for many energy storage-conversion applications. This review covers the properties, functionalization of MoSe2, and their applications in supercapacitors, discussing the current developments of MoSe2 and its nano-composites-based supercapacitors, providing emphasis to the capacitive performances which comprise of specific capacitance/ capacity, cyclic lifespan, energy density, power density, rate capability, and their practicality in the real environments. Fundamental charge-storage mechanisms are also discussed to provide better insight into how MoSe2 is ascribed to each supercapacitor. Wherever applicable, limitations of the existing approaches and future outlook are also described.
Electromigration Separation of Lithium Isotopes: The Effect of Electrode Solutions
Authors: Wang Ciming , Zhang Pengrui , Huang Chaochi , Zhang Qian , Ju Huiqun , Xue Zixuan , Shao Fei , Li Bo , Mao Lianjing , Jing Yan , Jia Yongzhong , Sun Jinhe
Published: January 2022

Both lithium-6 and lithium-7 with high abundance are indispensable materials in nuclear industry. Here, an aqueous solution│organic solution│aqueous solution system was fabricated to separate lithium isotopes. The effects of species and concentration of electrolytes in the electrode solutions on the lithium ions migration and lithium isotope separation with different voltages and migration time was studied. It was found that lithium-7 was enriched in aqueous solutions on both sides at 0 V and 2 V, while lithium-7 was enriched in anode solution and lithium-6 was enriched in cathode solution at 16 V. The weakening stability of the chelate consisted of crown ether and lithium ion with increasing voltage was believed to the possible reason. Meanwhile, the variation of electrolyte in electrode solution led to notable changes in migration ratio of lithium ions and lithium isotope separation effect, which can be attributed to the different degree of both ionization and hydrolysis for various electrolytes in aqueous solutions and the different ability of H+ and NH4
+ to replace Li+ of chelate in organic solutions. This work is of great significance for the selection of electrode solutions in electromigration separation of lithium isotopes and even other electrochemical systems.
Coral-Like LaNixFe1−xO3 Perovskite Catalyst for High-Performance Oxygen Evolution Reaction
Authors: Wang Qing , Wang Haoye , Qi Songya , Su Zilong , Chen Kaixuan , Yu Xianglang , Xie Aijuan , Luo Shiping
Published: January 2022

With the rare earth element La was selected as the A site and transition metal ions (Ni, Fe) as the B site of perovskite-type oxides with general formula ABO3, a series of LaNixFe1−xO3 (x = 0, 0.3, 0.5, 0.7, 0.8, 1.0) perovskite catalysts were prepared by sol-gel method to investigate their catalytic performance for oxygen evolution reaction (OER). The catalyst activity was screened by linear scanning cyclic voltammetry (LSV), Tafel curves, and electrochemical impedance spectroscopy (EIS). A group of electrochemical tests for LaNixFe1−xO3 with various Ni/Fe ratios indicate that LaNi0.8Fe0.2O3 catalyst exhibits excellent electrochemical activity, with a resistance to charge-transfer reaction (R

ct
) of 5.942 Ω cm−2, overpotential of 391 mV, a Tafel slope of 102.8 mV dec−1, and electrochemical double-layer capacitance (C

dl
) of 12.31 mF cm−1. The stability test after 15000 s proves that the optimized LaNi0.8Fe0.2O3 has better stability compared to pristine LaFeO3 and LaNiO3. In addition, LaNi0.8Fe0.2O3 also exhibits the largest electrochemical active area (ECSA = 307.75 cm2) and exchange current density (j

o
= 1.08 mA cm−2). This work provides reference for perovskite in improving oxygen evolution performance.
Influence of Al2O3 Coatings on HF Induced Transition Metal Dissolution from Lithium-Ion Cathodes
Authors: Tesfamhret Yonas , Younesi Reza , Berg Erik J.
Published: January 2022

Transition metal (TM) dissolution from oxide cathode materials is a major challenge limiting the performance of modern Li-ion batteries. Coating the cathode materials with thin protective layers has proved to be a successful strategy to prolong their lifetime. Yet, there is a lack of fundamental understanding of the working mechanisms of the coating. Herein, the effect of the most commonly employed coating material, Al2O3, on suppressing hydrofluoric acid(HF)-induced TM dissolution from two state-of-the-art cathode materials, LiMn2O4 and LiNi0.8Mn0.1Co0.1O2, is investigated. Karl Fischer titration, fluoride selective probe and inductively coupled plasma optical emission spectrometry are coupled to determine the evolution of H2O, HF and TM concentrations, respectively, when the active materials come in contact with the aged electrolyte. The coating reduces the extent of TM dissolution, in part due to the ability of Al2O3 to scavenge HF and reduce the acidity of the electrolyte. Delithiation of the cathode materials, however, increases the extent of TM dissolution, likely because of the higher vulnerability of surface TMs in +IV oxidation state towards HF attack. In conclusion, the current study evidences the important role of acid-base reactions in governing TM dissolution in Li-ion batteries and shows that coatings enhance the chemical integrity of the cathode towards an acidic electrolyte.
Vascular responses to simulated breath-hold diving involving multiple reflexes
Authors: Fico Brandon G. , Alhalimi Taha A. , Tanaka Hirofumi
Published: January 2022

Breath-hold diving evokes a complex cardiovascular response. The degrees of hypertension induced by the diving reflex are substantial and accentuated by the underwater swimming. This condition provides a circulatory challenge to properly buffer and cushion cardiac pulsations. We determined hemodynamic changes during the diving maneuver and hypothesized that central artery compliance would be augmented during simulated breath-hold diving. A total of 20 healthy young adults were studied. Hemodynamics were measured during exercise on a cycle ergometer, apnea, face immersion in cold water (trigeminal stimulation), and simulated breath-hold diving. Arterial compliance was measured by recording the carotid artery diameter from images derived from an ultrasound machine at the cephalic portion of the common carotid artery 1–2 cm proximal to the carotid bulb, whereas arterial pressure waveforms were obtained using an arterial tonometry placed on the contralateral carotid artery and recorded on a data acquisition software. The change in diameter was divided by the change in blood pressure to calculate arterial compliance. Arterial compliance increased with simulated diving compared with rest ( P = 0.007) and was elevated compared with exercise and apnea alone ( P < 0.01). A significant increase in heart rate was observed with exercise, apnea, and facial immersion when compared with rest ( P < 0.001). However, simulated diving brought the heart rate down to resting levels. Cardiac output increased with all conditions ( P < 0.001), with an attenuated response during simulated diving compared with exercise and facial immersion ( P < 0.05). Mean blood pressure was elevated during all conditions ( P < 0.001), with a further elevation observed during simulated diving compared with exercise ( P < 0.001), apnea ( P = 0.016), and facial immersion ( P < 0.001). Total peripheral resistance was decreased during exercise and facial immersion compared with rest ( P < 0.001) but was increased during simulated diving compared with exercise ( P < 0.001), apnea ( P = 0.008), and facial immersion ( P = 0.003). We concluded that central artery compliance is augmented during simulated breath-hold diving to help buffer cardiac pulsations.
Some Midpoint Inequalities for
η
-Convex Function via Weighted Fractional Integrals
Authors: Chen Lei , Nazeer Waqas , Ali Farman , Botmart Thongchai , Mehfooz Sarah
Published: January 2022

In this research, by using a weighted fractional integral, we establish a midpoint version of Hermite-Hadamrad Fejér type inequality for

η

-convex function on a specific interval. To confirm the validity, we considered some special cases of our results and relate them with already existing results. It can be observed that several existing results are special cases of our presented results.
Exploration of Intelligent Manufacturing Methods for Complex Products Driven by Multisource Data
Authors: Zhang Lei
Published: January 2022

In order to improve the multisource data-driven fusion effect in the intelligent manufacturing process of complex products, based on the proposed adaptive fog computing architecture, this paper takes into account the efficient processing of complex product intelligent manufacturing services within the framework and the rational utilization of fog computing layer resources to establish a fog computing resource scheduling model. Moreover, this paper proposes a fog computing architecture for intelligent manufacturing services for complex products. The architecture adopts a three-layer fog computing framework, which can reasonably provide three types of services in the field of intelligent manufacturing. In addition, this study combines experimental research to verify the intelligent model of this article and counts the experimental results. From the analysis of experimental data, it can be seen that the complex product intelligent manufacturing system based on multisource data driven proposed in this paper meets the data fusion requirements of complex product intelligent manufacturing.
A Novel Mathematical Model for Radio Mean Square Labeling Problem
Authors: Badr Elsayed , Nada Shokry , Ali Al-Shamiri Mohammed M. , Abdel-Hay Atef , ELrokh Ashraf
Published: January 2022

A radio mean square labeling of a connected graph is motivated by the channel assignment problem for radio transmitters to avoid interference of signals sent by transmitters. It is an injective map h from the set of vertices of the graph G to the set of positive integers , such that for any two distinct vertices x, y, the inequality d(x, y) + ⌈ (h(x))2 + (h(y))2/2 ⌉ ≥ dim(G) + 1 holds. For a particular radio mean square labeling h, the maximum number of h(v) taken over all vertices of G is called its spam, denoted by rmsn(h), and the minimum value of rmsn(h) taking over all radio mean square labeling h of G is called the radio mean square number of G, denoted by rmsn(G). In this study, we investigate the radio mean square numbers rmsn(Pn) and rmsn(Cn) for path and cycle, respectively. Then, we present an approximate algorithm to determine rmsn(G) for graph G. Finally, a new mathematical model to find the upper bound of rmsn(G) for graph G is introduced. A comparison between the proposed approximate algorithm and the proposed mathematical model is given. We also show that the computational results and their analysis prove that the proposed approximate algorithm overcomes the integer linear programming model (ILPM) according to the radio mean square number. On the other hand, the proposed ILPM outperforms the proposed approximate algorithm according to the running time.
On the Network Strength of Meta-Aramid Fiber Suspension and Its Relationship to Formation
Authors: Sha Jiulong , Gao Jiawen , Wang Peiyao , Zhang Qiannan , Zhang Xinyi , Song Shunxi , Lu Peng
Published: January 2022

Because of poor surface hydrophilicity, meta-aramid fibers readily form flocs by intertwining or interlacing, and this severely affects the uniformity of meta-aramid paper. To investigate the flocculation mechanism of meta-aramid fiber suspensions, the critical flocculant concentration, shear, and compressive network strength of meta-aramid fiber suspensions were examined. A hand sheet former was used to study the influence of the yielding properties of suspensions on the uniformity of meta-aramid paper, and the relationship between the formation index and rheological properties was determined. The results showed that the critical gel concentration ranged from 0.37 to 0.68 g/L, which was much lower than that of plant fiber suspensions. In addition, the compressive yield stress (

P
y

) and shear yield stress (

τ
y

) of the meta-aramid fiber suspensions were found to increase linearly and exponentially, respectively, with an increasing concentration, and the uniformity index of the paper sheets was found to depend on a power of

τ
y
⋅
P
y

. This provides an effective method for predicting paper sheet uniformity.
Optimal Asset Allocation for CRRA and CARA Insurers under the Vasicek Interest Rate Model
Authors: Hu Hanlei , Lai Shaoyong , Chen Hongjing
Published: January 2022

This paper considers the reinsurance‐investment problem with interest rate risks under constant relative risk aversion and constant absolute risk aversion preferences, respectively. Stochastic control theory and dynamic programming principle are applied to investigate the optimal proportional reinsurance‐investment strategy for an insurer under the Vasicek stochastic interest rate model. Solving the corresponding Hamilton‐Jacobi‐Bellman equation via the Legendre transform approach, the optimal premium allocation strategies maximizing the expected utilities of terminal wealth are derived. In addition, several sensitivity analyses and numerical illustrations are given to analyze the impacts of different risk preferences and interest rate fluctuation on the optimal strategies. We find that the asset allocation and reinsurance ratio of the insurer are correlated with risk preference coefficient and interest rate fluctuation, and the insurance company may adjust the reinsurance‐investment strategy to deal with interest rate risk.
Imaging Review of Subscapularis Tendon and Rotator Interval Pathology
Authors: Ahmad Zohaib Y. , Diaz Luis E. , Roemer Frank W. , Goud Ajay , Guermazi Ali
Published: January 2022

As the largest rotator cuff muscle, the subscapularis plays a major role in stabilizing the glenohumeral joint, in conjunction with surrounding rotator cuff structures. Injury to the subscapularis tendon can be isolated, but more commonly is seen in conjunction with supraspinatus tendon pathology. Injury can be associated with biceps pulley instability, superior labral anterior-posterior (SLAP) tears, humeral head subluxation, and anterosuperior and coracoid impingements. The involvement of the rotator interval can lead to what is called “the hidden lesion,” due to its difficulty to diagnose during arthroscopy. Understanding the anatomical relations of the subscapularis tendon with the rest of the rotator cuff and rotator interval, as well as common patterns of injury that involve the subscapularis tendon, can aid in proper diagnosis of these injuries leading to prompt surgical repair. This review describes the anatomy of the subscapularis muscle and tendon, and the magnetic resonance imaging (MRI) patterns of subscapularis tendon injury.
Quality Evaluation Model for Smart City Social Sports Information Cloud Service
Authors: Zhang Lan
Published: January 2022

With the continuous development of social economy, social sport is more and more valued and favored by the people as a universal and nationwide sport, but it should be noted that social sport involves a wide range of aspects, but due to its particularity, it is also constrained by economic development. In view of these needs and limitations, three technical methods of entropy method, RSR (rank-sum ratio), and TOPSIS are introduced, to sort out the development of social sports, national physical development, social sports guidance, and the number of people to be measured in various places based on the relevant technologies of smart cities in this paper, realize the application analysis of social sports in the public service level. This paper aims to provide a scientific evaluation and evaluation method for social sports information cloud services. The results of simulation experiments show that the evaluation of social sports information cloud service quality based on smart cities is effective, and the comprehensive application of methods can be implemented perfectly, and the further promotion and popularization of social sports services can be realized.