bluuebunny/crossref_metadata_2025 huggingface dataset:
Effect of flow rate on the end‐expiratory lung volume in infants with bronchiolitis using high‐flow nasal cannula evaluated through electrical impedance tomography
Authors: Nascimento Milena S. , do Prado Cristiane , Costa Eduardo L. V. , Alcala Glasiele C. , Corrêa Letícia C. , Rossi Felipe S. , Amato Marcelo B. P. , Rebello Celso M.
Published: August 2022

Objectives

To evaluate the effects of four flow rates on the functional residual capacity (FRC) and pulmonary ventilation distribution while using a high‐flow nasal cannula (HFNC).

Working Hypothesis

Our hypothesis is that flow rates below 1.5 L·kg−1·min−1 lead to FRC loss and respiratory distress.

Study Design

A single‐center, prospective clinical study.

Patient Selection

Infants diagnosed with acute viral bronchiolitis were given HFNC.

Methodology

Through a prospective clinical study, the effects of four different flow rates, 2.0, 1.5, 1.0, and 0.5 L·kg−1·min−1, on FRC and the pulmonary ventilation pattern were evaluated using electrical impedance tomography. The impedance variation (delta Z), end‐expiratory lung volume (EELZ), respiratory rate, heart rate, respiratory distress score, and saturation/fraction of inspired oxygen ratio (SpO2/FIO2), were also evaluated at each flow rate.

Results

Among the 11 infants included, There was a decrease in respiratory distress score at a flow rate of 1.5 L·kg−1·min−1 (*p = 0.021), and at a flow rate of 2.0 L·kg−1·min−1 (**p = 0.003) compared to 0.5 L·kg−1·min−1. There was also a small but significant increase in SpO2/FiO2 at flow rates of 1.5 (*p = 0.023), and 2.0 L·kg−1·min−1 (**p = 0.008) compared to 0.5 L·kg−1·min−1. There were no other significant changes in the clinical parameters. In the global EELZ measurements, there was a significant increase under a flow rate of 2.0 L·kg−1·min−1 as compared to 0.5 L·kg−1·min−1 (p = 0.03). In delta Z values, there were no significant variations between the different flow rates.

Conclusion

The ∆EELZ increases at the highest flow rates were accompanied by decreased distress scores and improved oxygenation.
Building a pediatric rare lung disease program: It takes a community of villages
Authors: Vece Timothy J. , Gower William A. , Davis Stephanie D. , Austin Ashley , McKinzie Cameron J. , Hatch Joseph E. , Davis Miriam , Hagood James S.
Published: August 2022

Pediatric rare lung disease programs are increasing in number due to an increase in recognition of the diseases, increased clinical and research interest in children's interstitial lung disease, and the expansion of the children's interstitial lung disease research network. Due to this increased interest newly graduated trainees in pediatric pulmonology and other physicians are often starting new programs, which can be daunting. We provide some guidance for new programs based on our experiences.
Feasibility and acceptability of a CF‐specific cognitive‐behavioral preventive intervention for adults integrated into team‐based care
Authors: Friedman Deborah , Smith Beth A. , Bruce Amanda , Schwartz Carolyn E. , Lee Hang , Pinsky Hanna , Gootkind Elizabeth , Hardcastle Margot , Shea Nicole , Roach Christine M. , Miller Caitlin , Polineni Deepika , Salathe Matthias , Quittner Alexandra L. , Georgiopoulos Anna M.
Published: August 2022

Background

A cystic fibrosis (CF)‐specific cognitive‐behavioral therapy intervention (CF‐CBT) was developed in partnership with the CF community to advance preventive mental health care. Multidisciplinary providers across three centers were trained to deliver CF‐CBT for this pilot assessing feasibility/acceptability and preliminary effectiveness of an integrated model of care.

Methods

The 8‐session CF‐CBT was delivered to 14 adults with mild depression and/or anxiety symptoms in‐person and via audio telehealth. Assessment of attrition, engagement, homework completion, treatment satisfaction, and treatment fidelity informed feasibility/acceptability assessment. Mental health outcomes included depression, anxiety, quality of life (Cystic Fibrosis Questionnaire‐Revised [CFQ‐R), perceived stress and coping. Preliminary effectiveness was evaluated with Cohen's d metric of effect sizes (ES) of pre‐post mean change scores.

Results

A total of 108 sessions were conducted; 13 adults completed the intervention; 1 discontinued early. Engagement, homework completion, and treatment acceptability were highly rated (mean = 30; SD = 2, range: 27–32 on a 32‐point scale). Fidelity scores ranged from 85.7% to 93.6%. Large ES changes reflected improvements in depressive symptoms (−0.83), CFQ‐R (Vitality scale: 1.11), and Relaxation Skills (0.93); moderate ES for CFQ‐R Role Functioning (0.63), Awareness of Tension (0.62), Coping Confidence (0.70) and CF‐specific Coping (0.55); and small ES for anxiety symptoms (−0.22), perceived stress (−0.25), Behavioral Activation (0.29), and several CFQ‐R domains, including Emotional Functioning (0.29). Two CFQ‐R subscales decreased (Body Image, Eating Concerns).

Conclusions

Results indicated feasibility and acceptability of CF‐CBT and its integration into team‐based CF care with promising effectiveness, especially for depression. A multicenter randomized controlled trial of CF‐CBT will further examine effectiveness of a CF‐specific integrated care model.
Front Cover Image, Volume 78, Issue 9
Authors: Zhang Mengdi , Yan Junjie , Ali Abid , Gao Yulin
Published: August 2022

The cover image is based on the Research Article Potato plant variety affects the performance and oviposition preference of Phthorimaea operculella Zeller (Lepidoptera: Gelechiidae) by Mengdi Zhang et al., https://doi.org/10.1002/ps.6625. Image Credit: Yulin Gao.

image
Assessment of a zinc finger protein gene (MPZC3H10) as potential RNAi target for green peach aphid Myzus persicae control
Authors: Xie Xiucheng , Shang Feng , Ding Bi‐Yue , Yang Li , Wang Jin‐Jun
Published: August 2022

BACKGROUND

RNA interference (RNAi) has potential application in pest control, and selection of the specific target gene is one of the key steps in RNAi. As an important effector, the zinc finger protein (ZFP) gene has high similarity among aphid species, and may have potential use in an RNAi‐based pest control strategy. This study assessed the control efficiency of an RNAi target, MPZC3H10, a CCCH‐type ZFP gene, against green peach aphid.

RESULTS

ZC3H10 amino acid sequence similarity is more than 97.71% among the five tested aphid species: Myzus persicae, Aphis citricidus, Acyrthosiphon pisum, Diuraphis noxia and Rhopalosiphum maidis. However, no homologous sequence was found in the transcriptome of their ladybeetle predator, Propylaea japonica. Spatial expression patterns revealed that MPZC3H10 showed high expression in the muscle and fat body of M. persicae. The RNAi bioassay revealed that silencing of MPZC3H10 resulted in high mortality (53.33%) in M. persicae. By contrast, there were no observed negative effects on the growth and development of P. japonica when fed on aphids treated with double‐stranded RNA (dsRNA) or injected with a “high dose” of dsRNA.

CONCLUSION

Targeting MPZC3H10 showed promising efficiency for green peach aphid control via artificially designed dsRNA, and was safe for the predatory ladybeetle. © 2022 Society of Chemical Industry.
Synergistic effects of short peptides and antibiotics against bacterial and fungal strains
Authors: Sharma Lalita , Bisht Gopal Singh
Published: August 2022

There is a rising tide of concern about the antibiotic resistance issue. To reduce the possibility of antibiotic‐resistant infections, a new generation of antimicrobials must be developed. Antimicrobial peptides are potential alternatives to antibiotics that can be used alone or together with conventional antibiotics to combat antimicrobial resistance. In this work, lead compounds LP‐23, DP‐23, SA4, and SPO from previously published studies were synthesized by solid‐phase peptide synthesis and their antimicrobial evaluation was carried out against various bacterial and fungal strains. Peptide combinations with antibiotics were evaluated by using the checkerboard method and their minimal inhibitory concentration (MIC) in combination was calculated by using the fractional inhibitory concentration (FIC) index. Cytotoxicity evaluations of these peptides further confirmed their selectivity toward microbial cells. Based on the FIC values, LP‐23, DP‐23, and SPO demonstrated synergy in combination with gentamicin against a gentamicin‐resistant clinical isolate of Escherichia coli. For Staphylococcus aureus, Escherichia coli, and Salmonella typhimurium, seven combinations exhibited synergistic effects between peptide/peptoids and the tested antibiotics. Additionally, almost all the combinations of peptides/peptoids with amphotericin B and fluconazole also showed effective synergy against Aspergillus niger and Aspergillus flavus. The synergy found between LP‐23, DP‐23, SA4, and SPO with the selected antibiotics may have the potential to be used as a combination therapy against various microbial infections.
The basics of quantum computing for chemists
Authors: Claudino Daniel
Published: August 2022

The rapid and successful strides in quantum chemistry in the past decades can be largely credited to a conspicuous synergy between theoretical and computational advancements. However, the architectural computer archetype that enabled such a progress is approaching a state of more stagnant development. One of the most promising technological avenues for the continuing progress of quantum chemistry is the emerging quantum computing paradigm. This revolutionary proposal comes with several challenges, which span a wide array of disciplines. In chemistry, it implies, among other things, a need to reformulate some of its long established cornerstones in order to adjust to the operational demands and constraints of quantum computers. Due to its relatively recent emergence, much of quantum computing may still seem fairly nebulous and largely unknown to most chemists. It is in this context that here we review and illustrate the basic aspects of quantum information and their relation to quantum computing insofar as enabling simulations of quantum chemistry. We consider some of the most relevant developments in light of these aspects and discuss the current landscape when of relevance to quantum chemical simulations in quantum computers.
Daily sleep in relation to subjective and physiological stress in an occupational context: Daily vigour as a mediator
Authors: Kinnunen Ulla , Van Laethem Michelle , Sianoja Marjaana , de Bloom Jessica
Published: August 2022

Studies on the stress‐sleep relationship consistently demonstrate negative effects of stress on sleep. The reversed relation, however, has received less research attention. Also, field studies on physiological stress are scarce. The aim of this day‐level diary study was to examine daily relationships between sleep quality and quantity, and subjective and physiological stress in an occupational context. Moreover, we examined daily vigour as an underlying mechanism of the sleep‐stress relationship. Participants were 167 knowledge workers who filled in daily questionnaires measuring sleep quality and quantity, morning vigour and subjective afternoon stress on Tuesdays and Thursdays for 5 weeks. Physiological stress was assessed with cortisol decline from morning peak to evening, and with blood pressure in the afternoon. Multilevel path analysis results showed that better sleep quality and longer sleep hours predicted increased vigour the following morning, which in turn predicted lower subjective stress in the afternoon. Sleep quality and quantity were not related to physiological stress neither directly nor indirectly via morning vigour. On the basis of our results, sleep should be considered as a factor affecting vigour which in turn seems to lower stress.
Stress Analysis and Q‐Factor of Free‐Standing (La,Sr)MnO3Oxide Resonators
Authors: Manca Nicola , Remaggi Federico , Plaza Alejandro E. , Varbaro Lucia , Bernini Cristina , Pellegrino Luca , Marré Daniele
Published: August 2022

High‐sensitivity nanomechanical sensors are mostly based on silicon technology and related materials. The use of functional materials, such as complex oxides having strong interplay between structural, electronic, and magnetic properties, may open possibilities for developing new mechanical transduction schemes and for further enhancement of the device performances. The integration of these materials into micro/nano‐electro‐mechanical systems (MEMS/NEMS) is still at its very beginning and critical basic aspects related to the stress state and the quality factors of mechanical resonators made from epitaxial oxide thin films need to be investigated. Here, suspended micro‐bridges are realized from single‐crystal thin films of (La0.7,Sr0.3)MnO3(LSMO), a prototypical complex oxide showing ferromagnetic ground state at room temperature. These devices are characterized in terms of resonance frequency, stress state, and Q‐factor. LSMO resonators are highly stressed, with a maximum value of ≈260 MPa. The temperature dependence of their mechanical resonance is discussed considering both thermal strain and the temperature‐dependent Young's modulus. The measured Q‐factors reach few tens of thousands at room temperature, with indications of further improvements by optimizing the fabrication protocols. These results demonstrate that complex oxides are suitable to realize high Q‐factor mechanical resonators, paving the way toward the development of full‐oxide MEMS/NEMS sensors.
Cation‐Selective Oxide Semiconductor Mesoporous Membranes for Biomimetic Ion Rectification and Light‐Powered Ion Pumping
Authors: Li Li , Sun Mingyan , Hu Ziying , Nie Xiaoyan , Xiao Tianliang , Liu Zhaoyue
Published: August 2022

Artificial membranes precisely imitating the biological functions of ion channels and ion pumps have attracted significant attention to explore nanofluidic energy conversion. Herein, inspired by the cyclic ion transport for the photosynthesis in purple bacteria, a bilayer inorganic membrane (TiO2/AAO) composed of oxide semiconductor (TiO2) mesopores on anodic alumina (AAO) macropores is we developed. This inorganic membrane achieves the functions of ion channels and ion pumps, including the ion rectification and light‐powered ion pumping. The asymmetric charge distribution across the bilayer membrane contributes to the cationic selectivity and ion rectification characteristics. The electrons induced by ultraviolet irradiation introduce a built‐in electric field across TiO2/AAO membrane, which pumps the active ion transport from a low to a high concentration. This work integrates the functions of biological ion channels and ion pumps within an artificial membrane for the first time, which paves the way to explore multifunctional membranes analogous to its biological counterpart.
A Hierarchical Si/C Nanocomposite of Stable Conductive Network Formed Through Thermal Phase Separation of Asphaltenes for High‐Performance Li‐Ion Batteries
Authors: Tan Wen , Wang Lina , Lu Zhouguang , Yang Fan , Xu Zhenghe
Published: August 2022

Silicon is one of the most promising anode materials for lithium‐ion batteries. However, the huge volume change of silicon during lithiation/delithiation triggers continuous growth of solid‐electrolyte interphase, loss of conductive contacts and structural collapse of the electrode, which causes a rapid deterioration of battery capacities. Inspired by the polyaromatic molecular nature and phase separation of asphaltenes in bitumen during thermal cracking, a hierarchical Si/C nanocomposite of robust carbon coatings and a firmly connected carbon framework on the silicon surface is synthesized by controlling the concentration of asphaltenes as carbon source and hence desired phase separation during the subsequent carbonization. The electrode made using this special Si/C nanocomposite exhibits a high reversible capacity of 1149 mAh g−1 after 600 cycles with a capacity retention of 98.5% and the operation ability at a high mass loading over 10 mg cm−2 or an area capacity of 23.8 mAh cm−2, which represents one of the highest area capacities reported in open literature but with much more stable and prolonged operations. This simple and efficient strategy is easy to scale up for commercial production to meet the rapid growth of the electric vehicle industry.
Brain Wave‐Like Signal Modulator by Ionic Nanochannel Rectifier Bridges
Authors: Lu Bingxin , Xiao Tianliang , Zhang Caili , Jiang Jiaqiao , Wang Yuting , Diao Xungang , Zhai Jin
Published: August 2022

Smart modulation of bioelectric signals is of great significance for the development of brain‐computer interfaces, bio‐computers, and other technologies. The regulation and transmission of bioelectrical signals are realized through the synergistic action of various ion channels in organisms. The bionic nanochannels, which have similar physiological working environment and ion rectification as their biological counterparts, can be used to construct ion rectifier bridges to modulate the bioelectric signals. Here, the artificial smart ionic rectifier bridge with light response is constructed by anodic aluminum oxide (AAO)/poly (spiropyran acrylate) (PSP) nanochannels. The output ion current of the rectifier bridge can be switched between “ON” and “OFF” states by irradiation with UV and visible (Vis) light, and the conversion efficiency (η) of the system in “ON” state is ≈70.5%. The controllable modulation of brain wave‐like signal can be realized by ionic rectifier bridge. The ion transport properties and processes of ion rectifier bridges are explained using theoretical calculations based on Poisson–Nernst–Planck (PNP) equations. These findings have significant implications for the understanding of the intelligent ionic circuit and combination of artificial smart ionic channels to organisms, which provide new avenues for development of intelligent ion devices.
Achieving and Understanding of Highly Efficient Ternary Organic Photovoltaics: From Morphology and Energy Loss to Working Mechanism
Authors: Li Shuixing , Zhan Lingling , Li Yaokai , He Chengliang , Zuo Lijian , Shi Minmin , Chen Hongzheng
Published: August 2022

Ternary strategy, adding an additional donor (D) or acceptor (A) into conventional binary D:A blend, has shown great potential in improving photovoltaic performances of organic photovoltaics (OPVs) for practical applications. Herein, this review is presented on how efficient ternary OPVs are realized from the aspects of morphology, energy loss, and working mechanism. As to morphology, the role of third component on the formation of preferred alloy‐like‐phase and vertical‐phase, which are driven by the miscibility tuning, is discussed. For energy loss, the effect of the third component on the luminescence enhancement and energetic disordering suppression, which lead to favorable increase of voltage, is presented. Regarding working mechanism, dilution effect and relationships between two acceptors or donor/acceptor, which explain the observed device parameters variations, are analyzed. Finally, some future directions concerning ternary OPVs are pointed out. Therefore, this review can provide a comprehensive understanding of working principles and effective routes for high‐efficiency ternary systems, advancing the commercialization of OPVs.
Evaluating the benefits of empowering model‐driven development with a machine learning classifier
Authors: Marcén Ana C. , Pérez Francisca , Pastor Óscar , Cetina Carlos
Published: August 2022

Increasingly, the model driven engineering (MDE) community is paying more attention to the techniques offered by the machine learning (ML) community. This has led to the application of ML techniques to MDE related tasks in hope of increasing the current benefits of MDE. Nevertheless, there is a lack of empirical experiments that evaluate the benefits that ML brings to MDE. In this work, we evaluate the benefits of empowering model engineers of model‐driven development (MDD) with an ML classifier. To do this, we tackled how to embed the ML classifier as part of the MDD. Then, this was evaluated using two different real industrial cases. Our results show that despite the ML part takes an extra effort, the use of the ML classifier pays off in terms of the quality results, the perceived usefulness, and intention to use.
Understanding perceived influencers on project outcomes and quantifying disciplinary similarities in academic literature
Authors: Eaton Casey , Banks Amanda , Weger Kristin , Mesmer Bryan , Moreland Robert
Published: August 2022

Modern systems rely on contributions from many disciplines, requiring a systems perspective when evaluating project outcomes. This investigation provides insight into categorizations of influencers on project outcomes across a range of disciplines and the challenges in categorizing perceived influencers on project outcomes when multiple disciplines are collaborating on a project. This research identifies 390 categorizations from 12 disciplines through systematic review, extracts over 4000 perceived influencers on project outcomes as metadata and analyses the categorizations with a focus on disciplinary similarities. The results of the meta‐analysis indicate that contents of categorizations of perceived influencers on project outcomes are diverse, both within and across disciplines, highlighting the significance of understanding the disciplinary contributions to project outcomes, in order to develop successful systems. Findings indicate that practising systems engineers need to consider the many perspectives that are entangled in the design of complex multidisciplinary systems into a holistic view of the system.
The Effect of the Thermal Deformation of Casting Roll on Strip Thickness in the Strip Casting Process
Authors: Wang Yuchen , Zhang Xiaoming , Zhang Yuanxiang , Li Zhenlei , Fang Feng , Wang Yang , Yuan Guo
Published: August 2022

Many factors affect the strip thickness in the industrial production process of twin‐roll strip casting, such as pouring temperature, casting speed, cooling capacity, cast‐rolling force, and so on. When the pouring temperature and cooling capacity are specified, the magnitude of the cast‐rolling force is determined by the actual roll gap, which has a significant effect on the thickness, shape, and surface quality of the cast strip. As a result, the actual roll gap size is critical for smooth realization. In the actual casting process, thermal deformation is a direct factor influencing the change in roll gap shape for a given roll gap value. Hence, any factor influencing the thermal deformation indirectly influences the roll gap shape. Thus, the critical factors determining the thermal deformation are simulated and studied in this research, which is integrated with actual production, based on the application and secondary development of ANSYS. The effect law of each process parameter on the thermal deformation of the casting roll is given, and corresponding mathematical models are established. This research lays the foundation for the establishment of the cast strip thickness control model and the realization of online control of strip thickness.
Hot Deformation Behavior and 3D Processing Maps of Mn18Cr18N Steel
Authors: Zhang Mei , Wang Weijun , Cen Qiongying , Wang Yang , Zhu Delong , Gan Bin
Published: August 2022

The isothermal hot deformation behavior in the ranges of 1023–1473 K (750–1200 °C) and 0.001–10 s−1 for 0.53 wt% N‐bearing Mn18Cr18N steel is studied with a Gleeble‐3500 thermomechanical simulator. The results indicate that the peak stress decreases with decreasing strain rate and increasing temperature. The calculated deformation activation energy of the experimental steel is 449.118 kJ mol−1 by regression analysis. At the same time, 3D processing maps are established based on experimental data and the principles of the dynamic materials model. The domain of stable deformation gradually expands with the increase in strain, while the instability region shrinks accordingly. From the microstructure of specimens and the processing maps established, it is clear that dynamic recrystallization emerges in the peak power dissipation efficiency domain, 1000–1150 °C/0.002–0.1 s−1, which is the optimum region of hot working of the steel.
Exchange of ammine‐ and fluorido‐ligands in complex salts: The series [Cr(NH3)6][AlF6], [Cr(NH3)5F][SiF6] and K2[Cr(NH3)4F2][Si(NH3)0.5F5.5]2
Authors: Bäucker Christian , Niewa Rainer
Published: August 2022

The three amminechromium(III) complex compounds [Cr(NH3)6][AlF6], [Cr(NH3)5F][SiF6] and K2[Cr(NH3)4F2][Si(NH3)0.5F5.5]2 were obtained from ammonothermal synthesis at Tmax=724 K and pmax=2120 bar. Crystal structures were determined from single crystal X‐ray diffraction. The gradual exchange of ammine ligands by fluoride ligands in the amminechromium(III) ions is reflected by an intriguing change in color. The mutual ligand exchange between ammonia ligands and fluoride ions occurs in both the cations and the anions, indicating the various dissolved species present under the synthetic conditions.
Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning
Authors: Jin Peng , Tian Jiaxu , Zhi Dapeng , Wen Xuejun , Zhang Min
Published: August 2022

Deep Reinforcement Learning (DRL) has demonstrated its strength in developing intelligent systems. These systems shall be formally guaranteed to be trustworthy when applied to safety-critical domains, which is typically achieved by formal verification performed after training. This train-then-verify process has two limits: (i) trained systems are difficult to formally verify due to their continuous and infinite state space and inexplicable AI components (i.e., deep neural networks), and (ii) the ex post facto detection of bugs increases both the time- and money-wise cost of training and deployment. In this paper, we propose a novel verification-in-the-loop training framework called Trainify for developing safe DRL systems driven by counterexample-guided abstraction and refinement. Specifically, Trainify trains a DRL system on a finite set of coarsely abstracted but efficiently verifiable state spaces. When verification fails, we refine the abstraction based on returned counterexamples and train again on the finer abstract states. The process is iterated until all predefined properties are verified against the trained system. We demonstrate the effectiveness of our framework on six classic control systems. The experimental results show that our framework yields more reliable DRL systems with provable guarantees without sacrificing system performance such as cumulative reward and robustness than conventional DRL approaches.
Proof-Guided Underapproximation Widening for Bounded Model Checking
Authors: Chatterjee Prantik , Meda Jaydeepsinh , Lal Akash , Roy Subhajit
Published: August 2022

Bounded Model Checking (BMC) is a popularly used strategy for program verification and it has been explored extensively over the past decade. Despite such a long history, BMC still faces scalability challenges as programs continue to grow larger and more complex. One approach that has proven to be effective in verifying large programs is called Counterexample Guided Abstraction Refinement (CEGAR). In this work, we propose a complementary approach to CEGAR for bounded model checking of sequential programs: in contrast to CEGAR, our algorithm gradually widens underapproximations of a program, guided by the proofs of unsatisfiability. We implemented our ideas in a tool called Legion. We compare the performance of Legion against that of Corral, a state-of-the-art verifier from Microsoft, that utilizes the CEGAR strategy. We conduct our experiments on 727 Windows and Linux device driver benchmarks. We find that Legion is able to solve 12% more instances than Corral and that Legion exhibits a complementary behavior to that of Corral. Motivated by this, we also build a portfolio verifier, $$\textsc {Legion}^{+}$$

L

E
G
I
O
N

+

, that attempts to draw the best of Legion and Corral. Our portfolio, $$\textsc {Legion}^{+}$$

L

E
G
I
O
N

+

, solves 15% more benchmarks than Corral with similar computational resource constraints (i.e. each verifier in the portfolio is run with a time budget that is half of the time budget of Corral). Moreover, it is found to be $$2.9\times $$

2.9
×

faster than Corral on benchmarks that are solved by both Corral and $$\textsc {Legion}^{+}$$

L

E
G
I
O
N

+

.
SolCMC: Solidity Compiler’s Model Checker
Authors: Alt Leonardo , Blicha Martin , Hyvärinen Antti E. J. , Sharygina Natasha
Published: August 2022

Formally verifying smart contracts is important due to their immutable nature, usual open source licenses, and high financial incentives for exploits. Since 2019 the Ethereum Foundation’s Solidity compiler ships with a model checker. The checker, called SolCMC, has two different reasoning engines and tracks closely the development of the Solidity language. We describe SolCMC’s architecture and use from the perspective of developers of both smart contracts and tools for software verification, and show how to analyze nontrivial properties of real life contracts in a fully automated manner.
UCLID5: Multi-modal Formal Modeling, Verification, and Synthesis
Authors: Polgreen Elizabeth , Cheang Kevin , Gaddamadugu Pranav , Godbole Adwait , Laeufer Kevin , Lin Shaokai , Manerkar Yatin A. , Mora Federico , Seshia Sanjit A.
Published: August 2022

UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems for heterogeneous systems such as combinations of hardware and software, or those that have multiple, varied specifications, or systems that require hybrid modes of modeling. A novel aspect of UCLID5 is an emphasis on the use of syntax-guided and inductive synthesis to automate steps in modeling and verification. This tool paper presents new developments in the UCLID5 tool including new language features, integration with new techniques for syntax-guided synthesis and satisfiability solving, support for hyperproperties and combinations of axiomatic and operational modeling, demonstrations on new problem classes, and a robust implementation.
Does a Program Yield the Right Distribution?
Authors: Chen Mingshuai , Katoen Joost-Pieter , Klinkenberg Lutz , Winkler Tobias
Published: August 2022

We study discrete probabilistic programs with potentially unbounded looping behaviors over an infinite state space. We present, to the best of our knowledge,the first decidability result for the problem of determining whether such a program generates exactly a specified distribution over its outputs(provided the program terminates almost-surely). The class of distributions that can be specified in our formalism consists of standard distributions (geometric, uniform, etc.) and finite convolutions thereof. Our method relies on representing these (possibly infinite-support) distributions asprobability generating functionswhich admit effective arithmetic operations. We have automated our techniques in a tool called$$\textsc {Prodigy}$$PRODIGY, which supports automatic invariance checking, compositional reasoning of nested loops, and efficient queries to the output distribution, as demonstrated by experiments.
Abstraction-Refinement for Hierarchical Probabilistic Models
Authors: Junges Sebastian , Spaan Matthijs T. J.
Published: August 2022

Markov decision processes are a ubiquitous formalism for modelling systems with non-deterministic and probabilistic behavior. Verification of these models is subject to the famous state space explosion problem. We alleviate this problem by exploiting a hierarchical structure with repetitive parts. This structure not only occurs naturally in robotics, but also in probabilistic programs describing, e.g., network protocols. Such programs often repeatedly call a subroutine with similar behavior. In this paper, we focus on a local case, in which the subroutines have a limited effect on the overall system state. The key ideas to accelerate analysis of such programs are (1) to treat the behavior of the subroutine as uncertain and only remove this uncertainty by a detailed analysis if needed, and (2) to abstract similar subroutines into a parametric template, and then analyse this template. These two ideas are embedded into an abstraction-refinement loop that analyses hierarchical MDPs. A prototypical implementation shows the efficacy of the approach.
Automatic Detection of Epileptic Seizures with Recurrent and Convolutional Neural Networks
Authors: Carrión Salvador , López-Chilet Álvaro , Martínez-Bernia Javier , Coll-Alonso Joan , Chorro-Juan Daniel , Gómez Jon Ander
Published: August 2022

Computer-aided diagnosis based on intelligent systems is an effective strategy to improve the efficiency of healthcare systems while reducing their costs. In this work, the epilepsy detection task is approached in two different ways, recurrent and convolutional neural networks, within a patient-specific scheme. Additionally, a detector function and its effects on seizure detection performance are presented. Our results suggest that it is possible to detect seizures from scalp EEGs with acceptable results for some patients, and that the DeepHealth framework is a proper deep learning software for medical research.
Evaluierung
Authors: Kirchner Aljoscha
Published: August 2022

Die in dieser Arbeit entwickelte modellbasierte Entwicklungsmethode wurde mittels zweier verschiedener Techniken evaluiert. Zum einen fand die Evaluierung des Einflusses der modellbasierten Entwicklungsmethode auf die SoC-Entwicklung, wie nachfolgend in Abschnitt 6.1 beschrieben, durch Interviews statt. Zum anderen wurde der als Ergebnis der modellgetriebenen Automatisierung erhaltene Code auf Korrektheit und Performance-Eigenschaften mittels Co-Simulation getestet und mit dem manuell implementierten Code verglichen.
Neuronal-specific septin-3 binds Atg8/LC3B, accumulates and localizes to autophagosomes during induced autophagy
Authors: Tóth Vilmos , Vadászi Henrietta , Ravasz Lilla , Mittli Dániel , Mátyás Dominik , Molnár Tamás , Micsonai András , Szaniszló Tamás , Lőrincz Péter , Kovács Réka Á. , Juhász Tünde , Beke-Somfai Tamás , Juhász Gábor , Györffy Balázs András , Kékesi Katalin A. , Kardos József
Published: August 2022

In synapses that show signs of local apoptosis and mitochondrial stress and undergo neuro-immunological synapse pruning, an increase in the levels of the presynaptic protein, neuronal-specific septin-3 can be observed. Septin-3 is a member of the septin GTPase family with the ability to form multimers and contribute to the cytoskeleton. However, the function of septin-3 remains elusive. Here, we provide evidence that septin-3 is capable of binding the most-studied autophagy protein Atg8 homolog microtubule-associated protein 1 light chain 3B (LC3B), besides another homolog, GABA receptor-associated protein-like 2 (GABARAPL2). Moreover, we demonstrate that colocalization of septin-3 and LC3B increases upon chemical autophagy induction in primary neuronal cells. Septin-3 is accumulated in primary neurons upon autophagy enhancement or blockade, similar to autophagy proteins. Using electron microscopy, we also show that septin-3 localizes to LC3B positive membranes and can be found at mitochondria. However, colocalization results of septin-3 and the early mitophagy marker PTEN-induced kinase 1 (PINK1) do not support that binding of septin-3 to mitochondria is mitophagy related. We conclude that septin-3 correlates with synaptic/neuronal autophagy, binds Atg8 and localizes to autophagic membranes that can be enhanced with chemical autophagy induction. Based on our results, elevated septin-3 levels might indicate enhanced or impeded autophagy in neurons.
Economic analysis using higher-frequency time series: challenges for seasonal adjustment
Authors: Ollech Daniel , Bundesbank Deutsche
Published: August 2022

The COVID-19 pandemic has increased the need for timely and granular information to assess the state of the economy in real time. Weekly and daily indices have been constructed using higher-frequency data to address this need. Yet the seasonal and calendar adjustment of the underlying time series is challenging. Here, we analyse the features and idiosyncracies of such time series relevant in the context of seasonal adjustment. Drawing on a set of time series for Germany—namely hourly electricity consumption, the daily truck toll mileage, and weekly Google Trends data—used in many countries to assess economic development during the pandemic, we discuss obstacles, difficulties, and adjustment options. Furthermore, we develop a taxonomy of the central features of seasonal higher-frequency time series.
On cryptographic properties of cubic and splitting Boolean functions
Authors: Musukwa Augustine , Sala Massimiliano , Villa Irene , Zaninelli Marco
Published: August 2022

The weight, balancedness and nonlinearity are important properties of Boolean functions, but they can be difficult to determine in general. In this paper, we study how to compute them for two classes of functions where these problems are more tractable. In particular, we study functions of degree three and the so-called “splitting” functions. The latter are functions that can be written as the sum of two functions defined over disjoint sets of variables. We show how, for splitting functions, studying these properties reduces to the study of simpler functions. We provide then a procedure to compute the weight of a cubic Boolean function. We show computationally that, for a cubic Boolean function with limited number of terms, this procedure is on average significantly more efficient than some other methods.
Metabolic profiling as a powerful tool for the analysis of cellular alterations caused by 20 mycotoxins in HepG2 cells
Authors: Gerdemann Andrea , Behrens Matthias , Esselen Melanie , Humpf Hans-Ulrich
Published: August 2022

Mycotoxins are secondary fungal metabolites which exhibit toxic effects in low concentrations. Several mycotoxins are described as carcinogenic or immunosuppressive, but their underlying modes of action especially on molecular level have not yet been entirely elucidated. Metabolic profiling as part of the omics methods is a powerful tool to study the toxicity and the mode of action of xenobiotics. The use of hydrophilic interaction chromatography in combination with targeted mass spectrometric detection enables the selective and sensitive analysis of more than 100 polar and ionic metabolites and allows the evaluation of metabolic alterations caused by xenobiotics such as mycotoxins. For metabolic profiling, the hepato-cellular carcinoma cell line HepG2 was treated with sub-cytotoxic concentrations of 20 mycotoxins. Moniliformin and citrinin significantly affected target elements of the citric acid cycle, but also influenced glycolytic pathways and energy metabolism. Penitrem A, zearalenone, and T2 toxin mainly interfered with the urea cycle and the amino acid homeostasis. The formation of reactive oxygen species seemed to be influenced by T2 toxin and gliotoxin. Glycolysis was altered by ochratoxin A and DNA synthesis was affected by several mycotoxins. The observed effects were not limited to these metabolic reactions as the metabolic pathways are closely interrelated. In general, metabolic profiling proved to be a highly sensitive tool for hazard identification in comparison to single-target cytotoxicity assays as metabolic alterations were already observed at sub-toxic concentrations. Metabolic profiling could therefore be a powerful tool for the overall evaluation of the toxic properties of xenobiotics.
Effect of alginate-based coating charged with hydroxyapatite and quercetin on colour, firmness, sugars and volatile compounds of fresh cut papaya during cold storage
Authors: Malvano Francesca , Corona Onofrio , Pham Phuong Ly , Cinquanta Luciano , Pollon Matteo , Bambina Paola , Farina Vittorio , Albanese Donatella
Published: August 2022

Active alginate-based coatings with quercetin glycoside and complexes of hydroxyapatite/quercetin-glycoside were used to study the shelf life of fresh cut papaya stored at 6 °C. Hydroxyapatite was used as a carrier for the release of the bioactive compound. The parameters considered affecting the quality of the fruit during storage were weight loss, color, texture, sugars and volatile compounds. Active coatings with hydroxyapatite and quercetin glycoside proved a higher capacity to slow down the degradation phenomena studied, showing less weight loss, a lower reduction in glucose and fructose, as well as better firmness, than the other samples after 14 days of cold storage. Benzyl isothiocyanate, the characteristic odor compound of papaya fruit, ranged from approximately 10.0 μg/kg in fresh cut fruit to approximately 7.50 μg/kg in samples coated by alginate with hydroxyapatite/quercetin and 3.6 μg/kg in the fresh cut papaya without coating after 14 days of cold storage. The trials also indicated greater effectiveness of alginate coatings alone and with quercetin-glucoside in preserving the color of freshly cut papaya.
Characterization of proteins from the 3N5M family reveals an operationally stable amine transaminase
Authors: Kollipara Manideep , Matzel Philipp , Sowa Miriam , Brott Stefan , Bornscheuer Uwe , Höhne Matthias
Published: August 2022

Amine transaminases (ATA) convert ketones into optically active amines and are used to prepare active pharmaceutical ingredients and building blocks. Novel ATA can be identified in protein databases due to the extensive knowledge of sequence-function relationships. However, predicting thermo- and operational stability from the amino acid sequence is a persisting challenge and a vital step towards identifying efficient ATA biocatalysts for industrial applications. In this study, we performed a database mining and characterized selected putative enzymes of the β-alanine:pyruvate transaminase cluster (3N5M) — a subfamily with so far only a few described members, whose tetrameric structure was suggested to positively affect operational stability. Four putative transaminases (TA-1: Bilophilia wadsworthia, TA-5: Halomonas elongata, TA-9: Burkholderia cepacia, and TA-10: Burkholderia multivorans) were obtained in a soluble form as tetramers in E. coli. During comparison of these tetrameric with known dimeric transaminases we found that indeed novel ATA with high operational stabilities can be identified in this protein subfamily, but we also found exceptions to the hypothesized correlation that a tetrameric assembly leads to increased stability. The discovered ATA from Burkholderia multivorans features a broad substrate specificity, including isopropylamine acceptance, is highly active (6 U/mg) in the conversion of 1-phenylethylamine with pyruvate and shows a thermostability of up to 70 °C under both, storage and operating conditions. In addition, 50% (v/v) of isopropanol or DMSO can be employed as co-solvents without a destabilizing effect on the enzyme during an incubation time of 16 h at 30 °C.

Key points

• Database mining identified a thermostable amine transaminase in the β-alanine:pyruvate transaminase subfamily.

• The tetrameric transaminase tolerates 50% DMSO and isopropanol under operating conditions at 30 °C.

• A tetrameric structure is not necessarily associated with a higher operational stability

Graphical abstract
Seemingly unrelated clusterwise linear regression for contaminated data
Authors: Perrone Gabriele , Soffritti Gabriele
Published: August 2022

Clusterwise regression is an approach to regression analysis based on finite mixtures which is generally employed when sample observations come from a population composed of several unknown sub-populations. Whenever the response is continuous, Gaussian clusterwise linear regression models are usually employed. Such models have been recently robustified with respect to the possible presence of mild outliers in the sub-populations. However, in some fields of research, especially in the modelling of multivariate economic data or data from the social sciences, there may be prior information on the specific covariates to be considered in the linear term employed in the prediction of a certain response. As a consequence, covariates may not be the same for all responses. Thus, a novel class of multivariate Gaussian linear clusterwise regression models is proposed. This class provides an extension to mixture-based regression analysis for modelling multivariate and correlated responses in the presence of mild outliers that let the researcher free to use a different vector of covariates for each response. Details about the model identification and maximum likelihood estimation via an expectation-conditional maximisation algorithm are given. The performance of the new models is studied by simulation in comparison with other clusterwise linear regression models. A comparative evaluation of their effectiveness and usefulness is provided through the analysis of a real dataset.
The prognostic value of the ratio of standard uptake value of lymph node to primary tumor before treatment of locally advanced nasopharyngeal carcinoma
Authors: Lou Yunlong , Chen Dandan , Lin Zheng , Sun Jianda , Song Li , Chen Wenzhong , Zhang Ming , Chen Yibiao
Published: August 2022

Background

To evaluate the prognostic value of the ratio of the standard uptake value of the lymph node and primary tumor before the treatment of locally advanced nasopharyngeal carcinoma and examine the prognostic value of the tumor metabolic parameters (SUVmax, MTV, and TLG) of the lymph node and primary tumor of locally advanced nasopharyngeal carcinoma.

Methods

A total of 180 patients with locally advanced nasopharyngeal carcinoma diagnosed pathologically from January 1, 2016 to December 31, 2018 were selected, and the MEDEX system was used to automatically delineate the SUVmax, MTV, and TLG of the lymph node metastases and nasopharyngeal carcinoma primary tumor. In addition, the ratio of LN-SUVmax (SUVmax of the lymph node metastases) to T-SUVmax (SUVmax of the nasopharyngeal carcinoma primary tumor) was calculated, and a ROC curve was drawn to obtain the best cut-off value. Kaplan–Meier and Cox regression models were used for survival and multivariate analyses, respectively.

Results

The median follow-up period for participants was 32 (4–62) months. Univariate analysis showed that age (P = 0.013), LN-SUVmax (P = 0.001), LN-TLG (P = 0.007) and NTR (P = 0.001) were factors influencing the overall survival (OS). Factors affecting local progression-free survival (LPFS) were LN-SUVmax (P = 0.005), LN-TLG (P = 0.003) and NTR (P = 0.020), while clinical stage (P = 0.023), LN-SUVmax (P = 0.007), LN-TLG (P = 0.006), and NTR (P = 0.032) were factors affecting distant metastasis-free survival (DMFS). Multivariate analysis showed that NTR was an independent influencing factor of OS (HR 3.00, 95% CI 1.06–8.4, P = 0.038), LPFS (HR 3.08, 95% CI 1.27–7.50, P = 0.013), and DMFS (HR 1.84, 95% CI 0.99–3.42, P = 0.054). Taking OS as the main observation point, the best cut-off point of NTR was 0.95. Kaplan–Meier results showed that the 3-year OS (97.0% vs 85.4%, χ2 = 11.25, P = 0.001), 3-year LPFS (91.3% vs 82.1%, χ2 = 4.035, P = 0.045), and 3-year DMFS (92.3% vs 87.9%, χ2 = 4.576, P = 0.032) of patients with NTR < 0.95 were higher than those with NTR > 0.95.

Conclusions

High NTR before treatment indicates a poor prognosis for patients with nasopharyngeal carcinoma. This can serve as a reference value for the reasonable treatment and prognosis monitoring of such patients.