bluuebunny/crossref_metadata_2025_split huggingface dataset:
Reclaiming independence in spatial‐clustering datasets: A series of data‐driven spatial weights matrices
Authors: Wang Wei , Xiao Xiong , Qian Jian , Chen Shiqi , Liao Fang , Yin Fei , Zhang Tao , Li Xiaosong , Ma Yue 
Published: March 2022

AbstractMost spatial models include a spatial weights matrix (W) derived from the first law of geography to adjust the spatial dependence to fulfill the independence assumption. In various fields such as epidemiological and environmental studies, the spatial dependence often shows clustering (or geographic discontinuity) due to natural or social factors. In such cases, adjustment using the first‐law‐of‐geography‐based W might be inappropriate and leads to inaccuracy estimations and loss of statistical power. In this work, we propose a series of data‐driven Ws (DDWs) built following the spatial pattern identified by the scan statistic, which can be easily carried out using existing tools such as SaTScan software. The DDWs take both the clustering (or discontinuous) and the intuitive first‐law‐of‐geographic‐based spatial dependence into consideration. Aiming at two common purposes in epidemiology studies (ie, estimating the effect value of explanatory variable X and estimating the risk of each spatial unit in disease mapping), the common spatial autoregressive models and the Leroux‐prior‐based conditional autoregressive (CAR) models were selected to evaluate performance of DDWs, respectively. Both simulation and case studies show that our DDWs achieve considerably better performance than the classic W in datasets with clustering (or discontinuous) spatial dependence. Furthermore, the latest published density‐based spatial clustering models, aiming at dealing with such clustering (or discontinuity) spatial dependence in disease mapping, were also compared as references. The DDWs, incorporated into the CAR models, still show considerable advantage, especially in the datasets for common diseases.
Regression modeling of restricted mean survival time for left‐truncated right‐censored data
Authors: Rong Rong , Ning Jing , Zhu Hong 
Published: March 2022

AbstractThe restricted mean survival time (RMST) is a clinically meaningful summary measure in studies with survival outcomes. Statistical methods have been developed for regression analysis of RMST to investigate impacts of covariates on RMST, which is a useful alternative to the Cox regression analysis. However, existing methods for regression modeling of RMST are not applicable to left‐truncated right‐censored data that arise frequently in prevalent cohort studies, for which the sampling bias due to left truncation and informative censoring induced by the prevalent sampling scheme must be properly addressed. The pseudo‐observation (PO) approach has been used in regression modeling of RMST for right‐censored data and competing‐risks data. For left‐truncated right‐censored data, we propose to directly model RMST as a function of baseline covariates based on POs under general censoring mechanisms. We adjust for the potential covariate‐dependent censoring or dependent censoring by the inverse probability of censoring weighting method. We establish large sample properties of the proposed estimators and assess their finite sample performances by simulation studies under various scenarios. We apply the proposed methods to a prevalent cohort of women diagnosed with stage IV breast cancer identified from surveillance, epidemiology, and end results‐medicare linked database.
Influence of steel fiber and polyvinyl alcohol fiber on properties of high performance concrete
Authors: Ju Yanzhong , Zhu Meitong , Zhang Xiaolei , Wang Dehong 
Published: March 2022

AbstractTo investigate influence of the single steel fibers, single polyvinyl alcohol fiber (PVA) and hybrid fibers on the properties of high performance concrete (HPC), the tests of the fresh properties, compressive strength, flexural strength and toughness of HPC reinforced with steel fiber and PVA fiber were conducted. The toughness of hybrid fiber HPC was evaluated through several flexural performance analysis methods and improved flexural toughness evaluation methods. In order to analyze the fiber toughening principle and the effect of different fiber content on flexural strength, the four‐point bending test was simulated by finite element modeling. And the calculation formula of hybrid steel‐PVA fiber HPC flexural strength was proposed. The results indicate that, steel fibers, PVA fibers and hybrid fibers can both improve HPC strength and toughness, while the content of PVA fiber had a critical value about 1%. If it is greater than this value, the enhancement of toughness will be reduced. Furthermore, the steel fiber and PVA fiber can play a bridging role in different scales to improve the toughness and strength of HPC.
The annual rate of independent events – A key interpretation for traditional extreme value distributions of wind velocity
Authors: Torrielli Alessio , Repetto Maria Pia , Solari Giovanni 
Published: March 2022

AbstractThe extreme value theory has been object of engineering studies for more than a century. The analysis of extreme winds plays a key role for complex civil structures and a driving role in different stages of wind turbines lifetime. Most of extremes probability models depend on the annual rate of independent events (ARIE) which has been traditionally considered a constant value. The authors have embraced a recent belief considering the ARIE as a function of the wind velocity. Even though a certain agreement has been achieved across the researches, some issues are still pending. In this regard, the paper shows that the annual, seasonal and daily fluctuations embedded in time series of the mean wind speeds, constrain its probability distribution and time correlation to be physically consistent. Besides, a new physical interpretation of the ARIE is presented, expressing how the independence across wind observations increases with the wind speed, up to the point that all yearly observations are independent if larger than a suitable speed value. Such a tendency is not revealed if the annual, seasonal and daily fluctuations are excluded by the analysis, leading to a deceitful shape of the ARIE. Finally, the paper shows how the velocity‐dependent ARIE model is consistent with the conventional asymptotic extreme value theory, if a sufficiently large left‐censorship applies to the dataset. The study of the ARIE presented in this paper is based on long‐term Monte Carlo simulation of the mean wind speed.
Adsorption performance and its mechanism of aqueous As(III) on polyporous calcined oyster shell‐supported Fe–Mn binary oxide
Authors: Shi Yao , Xing Yifei , Song Zhilian , Dang Xueming , Zhao Huimin 
Published: March 2022

AbstractFe–Mn binary oxide (FMBO) is a promising adsorbent for As(III) removal through combined adsorption and oxidation. The calcined oyster shell‐supported Fe–Mn binary oxide (FMBO/OS) adsorbent was synthesized by the co‐precipitation method. Results indicated that the calcined oyster shell, as a carrier, improved the stability of FMBO and its adsorption capacity for As(III). The maximum adsorption capacity of FMBO/OS on As(III) reached 140.5 mg·g−1. Under pH 5.0 and 25°C, the removal efficiency of FMBO/OS to As(III) solution (C0 = 10 mg·L−1) reached 87% within 12 h. Moreover, based on the characterization analyses, the removal mechanisms of As(III) were deduced to include the combined adsorption and oxidation process of FMBO and the synergistic effect of oyster shells. This work provides new insights into synthesizing efficient and green adsorbents to remove aqueous As(III). Meanwhile, it provides technical support for reusing waste biomass materials such as the oyster shell.Practitioner Points
FMBO/OS was prepared by a simple hydrothermal co‐precipitation method.
The carrier alleviates the agglomeration of Fe–Mn oxides.
The adsorbent shows a strong adsorption capacity of As(III) and good selectivity.
The good results benefit from the synergistic effect of calcium arsenate generation.
The prepared adsorbent can adsorb arsenic in real samples.
High‐temperature technology survey and comparison among incineration, pyrolysis, and gasification systems for water resource recovery facilities
Authors: Winchell Lloyd J. , Ross John J. , Brose Dominic A. , Pluth Thaís B. , Fonoll Xavier , Norton John W. , Bell Katherine Y. 
Published: March 2022

AbstractSolids from wastewater treatment undergo processing to reduce mass, minimize pathogens, and condition the products for specific end uses. However, costs and contaminant concerns (e.g., per‐ and polyfluoroalkyl substances [PFAS]) challenge traditional landfill and land application practices. Incineration can overcome these issues but has become complicated due to evolving emissions regulations, and it suffers from poor public perception. These circumstances are driving the re‐emergence of pyrolysis and gasification technologies. A survey of suppliers was conducted to document differences with technologies. Both offer advantages over incineration with tailored production of a carbon‐rich solid, currently less stringent air emission requirements, and lower flue gas flows requiring treatment. However, incineration more simply combines drying and thermal processing into one reactor. Equipment costs provided favor pyrolysis and gasification at lower capacities but converge with incineration at higher capacities. Long‐term operational experience will confirm technology competitiveness and elucidate whether pyrolysis and gasification warrant widespread adoption.Practitioner Points

Pyrolysis and gasification systems are gaining traction in the wastewater industry with several full‐scale installations operating, in construction, or design
Several advantages, but some disadvantages, are considered in comparison with incineration
Organic contaminants, including PFAS, will undergo transformation and potentially complete mineralization through each process
Publication Bias in Precision Oncology and Cancer Biomarker Research; Challenges and Possible Implications
Authors: Lotsberg Maria Lie , D’mello Peters Stacey Ann 
Published: March 2022

AbstractPublication bias and lack of information sharing are major obstacles in scientific research. Indeed, a lot of time, money and effort might be misspent on research that has already been undertaken, but not published. Over time, this causes a bias in the scientific literature that has implications for researchers designing new research projects or interpreting results. It also affects society and decision-making processes as important scientific knowledge is not shared, used, and critically discussed. In the specific context of medical research, publication bias can have a great impact on patients’ lives, as they could potentially have received a more adequate treatment or avoided harmful side-effects. The issue of publication bias seems even more stringent for precision oncology and biomarker research, as aiming for perfection or ‘hyper precision’ will leave even less space for ‘negative’ results than in medical research in general. Indeed, although a lot of resources are spent on cancer biomarker research, still only a few biomarkers end up in the clinic, and even for those that “succeed” in this process, there are still challenges with defining cut-offs for biomarker positive and negative subgroups as well as deciding how to treat the biomarker defined subgroups in a most optimal way. The aim of this chapter is to explore the extent of publication bias in the context of precision oncology and cancer biomarker research: its implications on researchers, patients, and society, as well as to reflect on the deeper roots of the problem.
Filled with Desire, Perceive Molecules
Authors: Strand Roger , Engen Caroline 
Published: March 2022

AbstractCould there be a Taoist philosophy of Acute Myeloid Leukaemia (AML)? This chapter discusses why a molecular treatment of AML has been so hard to find but still so intensely researched, and exposes some of the ethical dilemmas involved when treating this aggressive blood cancer. It does so by applying the concepts and style of the ancient Chinese masterpiece Tao Te Ching, the essence of which is that the real world is richer than what can be expressed by language.
Precision Oncology in the News
Authors: Stenmarck Mille Sofie , Nilsen Irmelin W. 
Published: March 2022

AbstractCancer has been a highly prevalent topic in the news media for some time and continues to be so with the rise and alleged promise of precision medicine. In this chapter, we present two empirical studies that explore how the news media frames issues related to cancer treatment and research.Our two studies both find a striking lack of nuance and diversity in the framing. The media coverage has seemingly stagnated, with a framing of either tragic choices and patient stories, or the sensationalistic coverage of new cancer drugs and treatments. The news content is accepted as is without further challenging questions or objections. We consider why it is that these news framings remain unchallenged in this way.We argue that we need a more sober approach to cancer in the news media, thus challenging the dominant framings that have characterized the media coverage of the topic of cancer over the last decade. The news media is one of the contributing instances, shaping the public discourse on cancer. However the answer as to why we see this complete lack of nuance cannot solely be studied with a media centred approach.
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion
Authors: Koenig Jason R. , Padon Oded , Shoham Sharon , Aiken Alex 
Published: March 2022

AbstractWe present a PDR/IC3 algorithm for finding inductive invariants with quantifier alternations. We tackle scalability issues that arise due to the large search space of quantified invariants by combining a breadth-first search strategy and a new syntactic form for quantifier-free bodies. The breadth-first strategy prevents inductive generalization from getting stuck in regions of the search space that are expensive to search and focuses instead on lemmas that are easy to discover. The new syntactic form is well-suited to lemmas with quantifier alternations by allowing both limited conjunction and disjunction in the quantifier-free body, while carefully controlling the size of the search space. Combining the breadth-first strategy with the new syntactic form results in useful inductive bias by prioritizing lemmas according to: (i) well-defined syntactic metrics for simple quantifier structures and quantifier-free bodies, and (ii) the empirically useful heuristic of preferring lemmas that are fast to discover. On a benchmark suite of primarily distributed protocols and complex Paxos variants, we demonstrate that our algorithm can solve more of the most complicated examples than state-of-the-art techniques.
LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions
Authors: Paulsen Brandon , Wang Chao 
Published: March 2022

AbstractThe most scalable approaches to certifying neural network robustness depend on computing sound linear lower and upper bounds for the network’s activation functions. Current approaches are limited in that the linear bounds must be handcrafted by an expert, and can be sub-optimal, especially when the network’s architecture composes operations using, for example, multiplication such as in LSTMs and the recently popularSwishactivation. The dependence on an expert prevents the application of robustness certification to developments in the state-of-the-art of activation functions, and furthermore the lack of tightness guarantees may give a false sense of insecurity about a particular model. To the best of our knowledge, we are the first to consider the problem ofautomaticallysynthesizingtightlinear bounds for arbitrary n-dimensional activation functions. We propose the first fully automated method that achieves tight linear bounds while only leveraging the mathematical definition of the activation function itself. Our method leverages an efficient heuristic technique to synthesize bounds that are tight andusually sound, and then verifies the soundness (and adjusts the bounds if necessary) using the highly optimized branch-and-bound SMT solver,dReal. Even though our method depends on an SMT solver, we show that the runtime is reasonable in practice, and, compared with state of the art, our method often achieves 2-5X tighter final output bounds and more than quadruple certified robustness.
Clausal Proofs for Pseudo-Boolean Reasoning
Authors: Bryant Randal E. , Biere Armin , Heule Marijn J. H. 
Published: March 2022

AbstractWhen augmented with a Pseudo-Boolean (PB) solver, a Boolean satisfiability (SAT) solver can apply apply powerful reasoning methods to determine when a set of parity or cardinality constraints, extracted from the clauses of the input formula, has no solution. By converting the intermediate constraints generated by the PB solver into ordered binary decision diagrams (BDDs), a proof-generating, BDD-based SAT solver can then produce a clausal proof that the input formula is unsatisfiable. Working together, the two solvers can generate proofs of unsatisfiability for problems that are intractable for other proof-generating SAT solvers. The PB solver can, at times, detect that the proof can exploit modular arithmetic to give smaller BDD representations and therefore shorter proofs.
Moving Definition Variables in Quantified Boolean Formulas
Authors: Reeves Joseph E. , Heule Marijn J. H. , Bryant Randal E. 
Published: March 2022

AbstractAugmenting problem variables in a quantified Boolean formula with definition variables enables a compact representation in clausal form. Generally these definition variables are placed in the innermost quantifier level. To restore some structural information, we introduce a preprocessing technique that moves definition variables to the quantifier level closest to the variables that define them. We express the movement in the QRAT proof system to allow verification by independent proof checkers. We evaluated definition variable movement on the QBFEVAL’20 competition benchmarks. Movement significantly improved performance for the competition’s top solvers. Combining variable movement with the preprocessorBloqqerimproves solver performance compared to usingBloqqeralone.
Property Directed Reachability for Generalized Petri Nets
Authors: Amat Nicolas , Zilio Silvano Dal , Hujsa Thomas 
Published: March 2022

AbstractWe propose a semi-decision procedure for checking generalized reachability properties, on generalized Petri nets, that is based on the Property Directed Reachability (PDR) method. We actually define three different versions, that vary depending on the method used for abstracting possible witnesses, and that are able to handle problems of increasing difficulty. We have implemented our methods in a model-checker called SMPT and give empirical evidences that our approach can handle problems that are difficult or impossible to check with current state of the art tools.
Searching for Ribbon-Shaped Paths in Fair Transition Systems
Authors: Bozzano Marco , Cimatti Alessandro , Tonetta Stefano , Vozarova Viktoria 
Published: March 2022

AbstractDiagnosability is a fundamental problem of partial observable systems in safety-critical design. Diagnosability verification checks if the observable part of system is sufficient to detect some faults. A counterexample to diagnosability may consist of infinitely many indistinguishable traces that differ in the occurrence of the fault. When the system under analysis is modeled as a Büchi automaton or finite-state Fair Transition System, this problem reduces to look for ribbon-shaped paths, i.e., fair paths with a loop in the middle.In this paper, we propose to solve the problem by extending the liveness-to-safety approach to look for lasso-shaped paths. The algorithm can be applied to various diagnosability conditions in a uniform way by changing the conditions on the loops. We implemented and evaluated the approach on various diagnosability benchmarks.
CoVeriTeam: On-Demand Composition of Cooperative Verification Systems
Authors: Beyer Dirk , Kanav Sudeep 
Published: March 2022

AbstractThere is no silver bullet for software verification: Different techniques have different strengths. Thus, it is imperative to combine the strengths of verification tools via combinations and cooperation. CoVeriTeam is a language and tool for on-demand composition of cooperative approaches. It provides a systematic and modular way to combine existing tools (without changing them) in order to leverage their full potential. The idea of cooperative verification is that different tools help each other to achieve the goal of correctly solving verification tasks.The language is based on verification artifacts (programs, specifications, witnesses) as basic objects and verification actors (verifiers, validators, testers) as basic operations. We define composition operators that make it possible to easily describe new compositions. Verification artifacts are the interface between the different verification actors. CoVeriTeam consists of a language for composition of verification actors, and its interpreter.As a result of viewing tools as components, we can now create powerful verification engines that are beyond the possibilities of single tools, avoiding to develop certain components repeatedly. We illustrate the abilities of CoVeriTeam on a few case studies. We expect that CoVeriTeam will help verification researchers and practitioners to easily experiment with new tools, and assist them in rapid prototyping of tool combinations.
Efficient Neural Network Analysis with Sum-of-Infeasibilities
Authors: Wu Haoze , Zeljić Aleksandar , Katz Guy , Barrett Clark 
Published: March 2022

AbstractInspired by sum-of-infeasibilities methods in convex optimization, we propose a novel procedure for analyzing verification queries on neural networks with piecewise-linear activation functions. Given a convex relaxation which over-approximates the non-convex activation functions, we encode the violations of activation functions as a cost function and optimize it with respect to the convex relaxation. The cost function, referred to as the Sum-of-Infeasibilities (SoI), is designed so that its minimum is zero and achieved only if all the activation functions are satisfied. We propose a stochastic procedure, , to efficiently minimize the SoI. An extension to a canonical case-analysis-based complete search procedure can be achieved by replacing the convex procedure executed at each search state with . Extending the complete search with achieves multiple simultaneous goals: 1) it guides the search towards a counter-example; 2) it enables more informed branching decisions; and 3) it creates additional opportunities for bound derivation. An extensive evaluation across different benchmarks and solvers demonstrates the benefit of the proposed techniques. In particular, we demonstrate that SoI significantly improves the performance of an existing complete search procedure. Moreover, the SoI-based implementation outperforms other state-of-the-art complete verifiers. We also show that our technique can efficiently improve upon the perturbation bound derived by a recent adversarial attack algorithm.