bluuebunny/crossref_metadata_2025_split huggingface dataset:
Protein–protein association properties of human βB2‐crystallins
Authors: Velasco‐Bolom José‐Luis , Domínguez Laura 
Published: July 2023

AbstractProtein–protein association events are involved in many physiological and pathological processes. Cataract disease is a pathology that manifests protein aggregation of crystallins. β‐Crystallins are present in a high proportion in the eye lens. Therefore, the structural study of the dimerization properties of crystallins can shed light on the first stages of protein aggregation. In the present work, we examine the protein–protein association profiles of the human βB2‐crystallin by employing extensive coarse‐grained molecular dynamics (CG‐MD) and the Markov state analysis. Interestingly, our results clearly show important changes in the protein dimerization kinetics between wt‐HβB2C and the deamidated systems. The two systems show dimeric conformations. However, the association and dissociation rates are very different. Our results show that the deamidated system can associate faster and dissociate slower than the wt‐ HβB2C. The deamidated system is in a slightly opened conformation with the Greek‐key motifs well folded, suggesting that a complete unfolding of the protein is not required for aggregation. Our results describe the first stages of crystallin aggregation due to post‐translational modifications.
Inclusion of binary proxy variables in logistic regression improves treatment effect estimation in observational studies in the presence of binary unmeasured confounding variables
Authors: Rosenbaum Cornelius , Yu Qingzhao , Buzhardt Sarah , Sutton Elizabeth , Chapple Andrew G. 
Published: July 2023

AbstractWe present a simulation study and application that shows inclusion of binary proxy variables related to binary unmeasured confounders improves the estimate of a related treatment effect in binary logistic regression. The simulation study included 60,000 randomly generated parameter scenarios of sample size 10,000 across six different simulation structures. We assessed bias by comparing the probability of finding the expected treatment effect relative to the modeled treatment effect with and without the proxy variable. Inclusion of a proxy variable in the logistic regression model significantly reduced the bias of the treatment or exposure effect when compared to logistic regression without the proxy variable. Including proxy variables in the logistic regression model improves the estimation of the treatment effect at weak, moderate, and strong association with unmeasured confounders and the outcome, treatment, or proxy variables. Comparative advantages held for weakly and strongly collapsible situations, as the number of unmeasured confounders increased, and as the number of proxy variables adjusted for increased.
How does global trade in environmental goods contribute to theSDGsin developing countries?
Authors: Wang Peiyu , Mao Xiyan , Huang Xianjin 
Published: July 2023

AbstractGlobal trade in environmental goods (EGs) has provided a new vision for international cooperation in response to sustainable development goals (SDGs). However, there are ongoing debates over whether developing countries can achieve sustainability during their trade participation. This study proposes a conceptual framework to observe countries' current trade status and potential for benefit from global EG trade. By tracing the changing status of 142 countries in the conceptual framework during 2001–2019, this study finds that global EG trade reduces inequality among developed countries while it increases inequality among developing countries. Some emerging market countries may enhance their status in the global trade network, but their upgrading within the global value chain remains slow. The current poor EG trade state and limited benefit potential of most developing countries will have a non‐significant impact in terms of achieving the SDGs. The study suggests that regional trade will give developing countries a better chance to integrate into trade markets and support them toward achieving the SDGs.
What plant breeding may (and may not) look like in 2050?
Authors: Bassi Filippo M. , Sanchez‐Garcia Miguel , Ortiz Rodomiro 
Published: July 2023

AbstractAt the turn of 2000 many authors envisioned future plant breeding. Twenty years after, which of those authors’ visions became reality or not, and which ones may become so in the years to come. After two decades of debates, climate change is a “certainty,” food systems shifted from maximizing farm production to reducing environmental impact, and hopes placed into GMOs are mitigated by their low appreciation by consumers. We revise herein how plant breeding may raise or reduce genetic gains based on the breeder's equation. “Accuracy of Selection” has significantly improved by many experimental‐scale field and laboratory implements, but also by vulgarizing statistical models, and integrating DNA markers into selection. Pre‐breeding has really promoted the increase of useful “Genetic Variance.” Shortening “Recycling Time” has seen great progression, to the point that achieving a denominator equal to “1” is becoming a possibility. Maintaining high “Selection Intensity” remains the biggest challenge, since adding any technology results in a higher cost per progeny, despite the steady reduction in cost per datapoint. Furthermore, the concepts of variety and seed enterprise might change with the advent of cheaper genomic tools to monitor their use and the promotion of participatory or citizen science. The technological and societal changes influence the new generation of plant breeders, moving them further away from field work, emphasizing instead the use of genomic‐based selection methods relying on big data. We envisage what skills plant breeders of tomorrow might need to address challenges, and whether their time in the field may dwindle.
Histological characteristics of a uterine hemangiosarcoma in a Brazilian Girolando cow
Authors: de Souza Giovanna Gati , Dinau Fernando Carmona , Ximenes Pedro Pol , de Moura Fernanda Barthelson Carvalho , Contel Isabeli Joaquim , Braga Iolanda Simões , Pelaquim Isadora Fernanda , Rocha Noeme Sousa 
Published: July 2023

AbstractA 7‐year‐old, pregnant dairy cow of the Girolando breed, weighing 450 kg, was referred to a veterinary hospital, presenting with lateral recumbency for 2 days. No health or reproductive alterations had ever been reported on the property of origin. A fetotomy was conducted at the hospital's reproductive care unit after purulent vaginal discharges, and no signals of fetal viability were observed, indicating an abortive process. The patient died within 24 hours following the reproductive intervention. A postmortem examination was performed, which revealed uterine alteration, comprising a bluish‐black, nondelimited, focally extensive mass in the region of the serous wall, involving the uterine corpus and horns and presenting diffuse haemorrhage without mucosal involvement. Histopathological examination confirmed the diagnosis of hemangiosarcoma. Uterine endothelial cells were Ki67‐positive, revealing proliferative activity of the neoplasm.
Megaoesophagus in a pet rabbit
Authors: Muffat‐es‐Jacques Patricia , Raymond Paul , Renard Jade , Combes Anais , Pignon Charly 
Published: July 2023

AbstractA 1‐year‐old, male, lop‐eared rabbit presented for anorexia and weakness. A dental trim and medical treatment for gastrointestinal stasis were implemented. Owners reclaimed the animal after 2 days. Two‐weeks later, its condition had worsened, and regurgitation was observed. Thoracic radiographs followed by barium contrast oesophagram revealed bronchopneumonia and megaoesophagus. A computed tomographic examination ruled out any structural compression (tumours, vascular ring anomalies). Treatment with assisted feeding, antibiotics and sildenafil was started. Increased regurgitations and worsening respiratory distress were observed. The rabbit died 16 days later. At postmortem examination, the oesophagus was dilated and filled with food, and the lungs showed patchy pneumonia and lobular consolidation. Generalised muscular atrophy and pericardial effusion were observed. Histopathological examination revealed severe broncho‐ and aspiration pneumonia, and moderate multifocal muscle degeneration affecting skeletal, lingual and oesophageal muscle and myocardium. The final diagnosis was acquired megaoesophagus. This is the first report of megaoesophagus in a rabbit.
Evaluation of replicate sampling using hierarchical spatial modeling of population surveys accounting for imperfect detectability
Authors: Camp Richard J. , Asing Chauncey K. , Banko Paul C. , Berry Lainie , Brinck Kevin W. , Farmer Chris , Genz Ayesha S. 
Published: July 2023

AbstractEffective species management and conservation benefit from knowledge of species distribution and status. Surveys to obtain that information often involve replicate sampling, which increases survey effort and costs. We simultaneously modeled species distribution, abundance and spatial correlation, and compared the uncertainty in replicate abundance estimates of the endangered palila (Loxioides bailleui) using hierarchical generalized additive models with a soap film smoother that incorporated random effects for visit. Based on survey coverage and detections, we selected the 2017 point‐transect distance sampling survey on Mauna Kea, Hawai‘i Island, for our modeling. Our modeling approach allowed us to account for imperfect detections, control the effects of boundary features, and generate visit‐specific density surface maps. We found that visit‐specific smooths were nearly identical, indicating that little information was gained from a subsequent visit, and that most of the estimator uncertainty was derived from within‐visit variability. Scaling back the palila survey to a single visit would halve the survey effort and logistical costs and increase efficiencies in data management and processing. Changing the sampling protocol warrants careful consideration and our findings may help management and regulatory agencies by maximizing efficiency and minimizing costs of surveying protocols, while providing guidelines on how to best collect information critical to species' conservation.
Onboarding and Preliminary Functionality Training
Authors: Witczak Marcin , Seybold Lothar , Bulach Eric , Maucher Niko 
Published: July 2023

AbstractThe objective of this chapter is to introduce the reader into the KIS.ME IoT platform, which is divided into the hardware and cloud-based software layers. In particular, we start with the registration and onboarding of the IoT hardware. Subsequently, a hierarchical system overview is provided pertaining to users as well as assets and their digital twins. The chapter discusses also an intuitive concept of Datapoints, which constitute the main source of knowledge about the current status of an asset. The rest of the chapter is devoted to placing assets inside workspaces and associating them with a set of functional rules. After a comprehensive introduction to Rule engine, the reader is guided towards topics related to analysing the efficiency of the system associated with KIS.ME. The chapter is summarized with a set of exercises motivating the reader to obtain further skills pertaining to practical applications of the modern IoT.
Incremental Dead State Detection in Logarithmic Time
Authors: Stanford Caleb , Veanes Margus 
Published: July 2023

AbstractIdentifying live and dead states in an abstract transition system is a recurring problem in formal verification; for example, it arises in our recent work on efficiently deciding regex constraints in SMT. However, state-of-the-art graph algorithms for maintaining reachability informationincrementally(that is, as states are visited and before the entire state space is explored) assume that new edges can be added from any state at any time, whereas in many applications, outgoing edges are added from each state as it is explored. To formalize the latter situation, we proposeguided incremental digraphs(GIDs), incremental graphs which support labelingclosedstates (states which will not receive further outgoing edges). Our main result is that dead state detection in GIDs is solvable in$$O(\log m)$$amortized time per edge formedges, improving upon$$O(\sqrt{m})$$per edge due to Bender, Fineman, Gilbert, and Tarjan (BFGT) for general incremental directed graphs.We introduce two algorithms for GIDs: one establishing the logarithmic time bound, and a second algorithm to explore a lazy heuristics-based approach. To enable an apples-to-apples experimental comparison, we implemented both algorithms, two simpler baselines, and the state-of-the-art BFGT baseline using a common directed graph interface in Rust. Our evaluation shows 110-530x speedups over BFGT for the largest input graphs over a range of graph classes, random graphs, and graphs arising from regex benchmarks.
Certifying the Fairness of KNN in the Presence of Dataset Bias
Authors: Li Yannan , Wang Jingbo , Wang Chao 
Published: July 2023

AbstractWe propose a method for certifying the fairness of the classification result of a widely used supervised learning algorithm, thek-nearest neighbors (KNN), under the assumption that the training data may have historical bias caused by systematic mislabeling of samples from a protected minority group. To the best of our knowledge, this is the first certification method for KNN based on three variants of the fairness definition: individual fairness,$$\epsilon $$-fairness, and label-flipping fairness. We first define the fairness certification problem for KNN and then propose sound approximations of the complex arithmetic computations used in the state-of-the-art KNN algorithm. This is meant to lift the computation results from the concrete domain to an abstract domain, to reduce the computational cost. We show effectiveness of thisabstract interpretationbased technique through experimental evaluation on six datasets widely used in the fairness research literature. We also show that the method is accurate enough to obtain fairness certifications for a large number of test inputs, despite the presence of historical bias in the datasets.
NNV 2.0: The Neural Network Verification Tool
Authors: Lopez Diego Manzanas , Choi Sung Woo , Tran Hoang-Dung , Johnson Taylor T. 
Published: July 2023

AbstractThis manuscript presents the updated version of the Neural Network Verification (NNV) tool. NNV is a formal verification software tool for deep learning models and cyber-physical systems with neural network components. NNV was first introduced as a verification framework for feedforward and convolutional neural networks, as well as for neural network control systems. Since then, numerous works have made significant improvements in the verification of new deep learning models, as well as tackling some of the scalability issues that may arise when verifying complex models. In this new version of NNV, we introduce verification support for multiple deep learning models, including neural ordinary differential equations, semantic segmentation networks and recurrent neural networks, as well as a collection of reachability methods that aim to reduce the computation cost of reachability analysis of complex neural networks. We have also added direct support for standard input verification formats in the community such as VNNLIB (verification properties), and ONNX (neural networks) formats. We present a collection of experiments in which NNV verifies safety and robustness properties of feedforward, convolutional, semantic segmentation and recurrent neural networks, as well as neural ordinary differential equations and neural network control systems. Furthermore, we demonstrate the capabilities of NNV against a commercially available product in a collection of benchmarks from control systems, semantic segmentation, image classification, and time-series data.
Rounding Meets Approximate Model Counting
Authors: Yang Jiong , Meel Kuldeep S. 
Published: July 2023

AbstractThe problem of model counting, also known as $$\#\textsf{SAT}$$, is to compute the number of models or satisfying assignments of a given Boolean formula F. Model counting is a fundamental problem in computer science with a wide range of applications. In recent years, there has been a growing interest in using hashing-based techniques for approximate model counting that provide $$(\varepsilon , \delta )$$-guarantees: i.e., the count returned is within a $$(1+\varepsilon )$$-factor of the exact count with confidence at least $$1-\delta $$. While hashing-based techniques attain reasonable scalability for large enough values of $$\delta $$, their scalability is severely impacted for smaller values of $$\delta $$, thereby preventing their adoption in application domains that require estimates with high confidence.The primary contribution of this paper is to address the Achilles heel of hashing-based techniques: we propose a novel approach based on rounding that allows us to achieve a significant reduction in runtime for smaller values of $$\delta $$. The resulting counter, called $$\textsf{ApproxMC6}$$ (The resulting tool $$\textsf{ApproxMC6}$$ is available open-source at https://github.com/meelgroup/approxmc), achieves a substantial runtime performance improvement over the current state-of-the-art counter, $$\textsf{ApproxMC}$$. In particular, our extensive evaluation over a benchmark suite consisting of 1890 instances shows $$\textsf{ApproxMC6}$$ solves 204 more instances than $$\textsf{ApproxMC}$$, and achieves a $$4\times $$ speedup over $$\textsf{ApproxMC}$$.
Rely-Guarantee Reasoning for Causally Consistent Shared Memory
Authors: Lahav Ori , Dongol Brijesh , Wehrheim Heike 
Published: July 2023

AbstractRely-guarantee (RG) is a highly influential compositional proof technique for concurrent programs, which was originally developed assuming a sequentially consistent shared memory. In this paper, we first generalize RG to make it parametric with respect to the underlying memory model by introducing an RG framework that is applicable to any model axiomatically characterized by Hoare triples. Second, we instantiate this framework for reasoning about concurrent programs under causally consistent memory, which is formulated using a recently proposed potential-based operational semantics, thereby providing the first reasoning technique for such semantics. The proposed program logic, which we call $${\textsf{Piccolo}}$$
Piccolo
, employs a novel assertion language allowing one to specify ordered sequences of states that each thread may reach. We employ $${\textsf{Piccolo}}$$
Piccolo
for multiple litmus tests, as well as for an adaptation of Peterson’s algorithm for mutual exclusion to causally consistent memory.
Closed-Loop Analysis of Vision-Based Autonomous Systems: A Case Study
Authors: Păsăreanu Corina S. , Mangal Ravi , Gopinath Divya , Getir Yaman Sinem , Imrie Calum , Calinescu Radu , Yu Huafeng 
Published: July 2023

AbstractDeep neural networks (DNNs) are increasingly used in safety-critical autonomous systems as perception components processing high-dimensional image data. Formal analysis of these systems is particularly challenging due to the complexity of the perception DNNs, the sensors (cameras), and the environment conditions. We present a case study applying formal probabilistic analysis techniques to an experimental autonomous system that guides airplanes on taxiways using a perception DNN. We address the above challenges by replacing the camera and the network with a compact abstraction whose transition probabilities are computed from the confusion matrices measuring the performance of the DNN on a representative image data set. As the probabilities are estimated based on empirical data, and thus are subject to error, we also compute confidence intervals in addition to point estimates for these probabilities and thereby strengthen the soundness of the analysis. We also show how to leverage local, DNN-specific analyses as run-time guards to filter out mis-behaving inputs and increase the safety of the overall system. Our findings are applicable to other autonomous systems that use complex DNNs for perception.
Verse: A Python Library for Reasoning About Multi-agent Hybrid System Scenarios
Authors: Li Yangge , Zhu Haoqing , Braught Katherine , Shen Keyi , Mitra Sayan 
Published: July 2023

Abstract
We present the Verse library with the aim of making hybrid system verification more usable for multi-agent scenarios. In Verse, decision making agents move in a map and interact with each other through sensors. The decision logic for each agent is written in a subset of Python and the continuous dynamics is given by a black-box simulator. Multiple agents can be instantiated, and they can be ported to different maps for creating scenarios. Verse provides functions for simulating and verifying such scenarios using existing reachability analysis algorithms. We illustrate capabilities and use cases of the library with heterogeneous agents, incremental verification, different sensor models, and plug-n-play subroutines for post computations.
Automated Analyses of IOT Event Monitoring Systems
Authors: Apicelli Andrew , Bayless Sam , Das Ankush , Gacek Andrew , Jaganathan Dhiva , Padhi Saswat , Sharma Vaibhav , Whalen Michael W. , Yadav Raveesh 
Published: July 2023

AbstractAWS IoT Events is an AWS service that makes it easy to respond to events from IoT sensors and applications.Detector modelsin AWS IoT Events enable customers to monitor their equipment or device fleets for failures or changes in operation and trigger actions when such events occur. If these models are incorrect, they may become out-of-sync with the actual state of the equipment causing customers to be unable to respond to events occurring on it.Working backwards from common mistakes made when creating detector models, we have created a set of automated analyzers that allow customers to prove their models are free from six common mistakes. Our analyzers have been running in the AWS IoT Events production service since December 2021. Our analyzers check six correctness properties in the production service in real time. 93% of customers of AWS IoT Events have run our analyzers without needing to have any knowledge of them. Our analyzers have reported property violations in 22% of submitted detector models in the production service.
Synthesizing Permissive Winning Strategy Templates for Parity Games
Authors: Anand Ashwani , Nayak Satya Prakash , Schmuck Anne-Kathrin 
Published: July 2023

AbstractWe present a novel method to compute permissive winning strategies in two-player games over finite graphs with $$ \omega $$
ω
-regular winning conditions. Given a game graph G and a parity winning condition $$\varPhi $$
Φ
, we compute a winning strategy template$$\varPsi $$
Ψ
that collects an infinite number of winning strategies for objective $$\varPhi $$
Φ
in a concise data structure. We use this new representation of sets of winning strategies to tackle two problems arising from applications of two-player games in the context of cyber-physical system design – (i) incremental synthesis, i.e., adapting strategies to newly arriving, additional$$\omega $$
ω
-regular objectives $$\varPhi '$$

Φ
′

, and (ii) fault-tolerant control, i.e., adapting strategies to the occasional or persistent unavailability of actuators. The main features of our strategy templates – which we utilize for solving these challenges – are their easy computability, adaptability, and compositionality. For incremental synthesis, we empirically show on a large set of benchmarks that our technique vastly outperforms existing approaches if the number of added specifications increases. While our method is not complete, our prototype implementation returns the full winning region in all 1400 benchmark instances, i.e. handling a large problem class efficiently in practice.