bluuebunny/crossref_metadata_2025_split huggingface dataset:
Online Causation Monitoring of Signal Temporal Logic
Authors: Zhang Zhenya , An Jie , Arcaini Paolo , Hasuo Ichiro 
Published: July 2023

AbstractOnline monitoring is an effective validation approach for hybrid systems, that, at runtime, checks whether the (partial) signals of a system satisfy a specification in, e.g., Signal Temporal Logic (STL). The classic STL monitoring is performed by computing a robustness interval that specifies, at each instant, how far the monitored signals are from violating and satisfying the specification. However, since a robustness interval monotonically shrinks during monitoring, classic online monitors may fail in reporting new violations or in precisely describing the system evolution at the current instant. In this paper, we tackle these issues by considering the causation of violation or satisfaction, instead of directly using the robustness. We first introduce a Boolean causation monitor that decides whether each instant is relevant to the violation or satisfaction of the specification. We then extend this monitor to a quantitative causation monitor that tells how far an instant is from being relevant to the violation or satisfaction. We further show that classic monitors can be derived from our proposed ones. Experimental results show that the two proposed monitors are able to provide more detailed information about system evolution, without requiring a significantly higher monitoring cost.
Automated Verification of Correctness for Masked Arithmetic Programs
Authors: Liu Mingyang , Song Fu , Chen Taolue 
Published: July 2023

AbstractMasking is a widely-used effective countermeasure against power side-channel attacks for implementing cryptographic algorithms. Surprisingly, few formal verification techniques have addressed a fundamental question, i.e., whether the masked program and the original (unmasked) cryptographic algorithm are functional equivalent. In this paper, we study this problem for masked arithmetic programs over Galois fields of characteristic 2. We propose an automated approach based on term rewriting, aided by random testing and SMT solving. The overall approach is sound, and complete under certain conditions which do meet in practice. We implement the approach as a new tool and carry out extensive experiments on various benchmarks. The results confirm the effectiveness, efficiency and scalability of our approach. Almost all the benchmarks can be proved for the first time by the term rewriting system solely. In particular, detects a new flaw in a masked implementation published in EUROCRYPT 2017.
Automatic Program Instrumentation for Automatic Verification
Authors: Amilon Jesper , Esen Zafer , Gurov Dilian , Lidström Christian , Rümmer Philipp 
Published: July 2023

AbstractIn deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to transform, for verification purposes, the program to an equivalent one not using the problematic constructs, and to reason about its correctness instead. In this paper, we propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches, has a clear formal correctness criterion, can be applied automatically, and can transfer back witnesses and counterexamples. We illustrate our approach on the automated verification of programs that involve quantification and aggregation operations over arrays, such as the maximum value or sum of the elements in a given segment of the array, which are known to be difficult to reason about automatically. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation, and evaluate it on example programs, including SV-COMP programs.
Certified Verification for Algebraic Abstraction
Authors: Tsai Ming-Hsien , Fu Yu-Fu , Liu Jiaxiang , Shi Xiaomu , Wang Bow-Yaw , Yang Bo-Yin 
Published: July 2023

AbstractWe present a certified algebraic abstraction technique for verifying bit-accurate non-linear integer computations. In algebraic abstraction, programs are lifted to polynomial equations in the abstract domain. Algebraic techniques are employed to analyze abstract polynomial programs; SMT QF_BV solvers are adopted for bit-accurate analysis of soundness conditions. We explain how to verify our abstraction algorithm and certify verification results. Our hybrid technique has verified non-linear computations in various security libraries such as Bitcoin and OpenSSL. We also report the certified verification of Number-Theoretic Transform programs from the post-quantum cryptosystem Kyber.
Complete Multiparty Session Type Projection with Automata
Authors: Li Elaine , Stutz Felix , Wies Thomas , Zufferey Damien 
Published: July 2023

AbstractMultiparty session types (MSTs) are a type-based approach to verifying communication protocols. Central to MSTs is a projection operator: a partial function that maps protocols represented as global types to correct-by-construction implementations for each participant, represented as a communicating state machine. Existing projection operators are syntactic in nature, and trade efficiency for completeness. We present the first projection operator that is sound, complete, and efficient. Our projection separates synthesis from checking implementability. For synthesis, we use a simple automata-theoretic construction; for checking implementability, we present succinct conditions that summarize insights into the property of implementability. We use these conditions to show that MST implementability is PSPACE-complete. This improves upon a previous decision procedure that is in EXPSPACE and applies to a smaller class of MSTs. We demonstrate the effectiveness of our approach using a prototype implementation, which handles global types not supported by previous work without sacrificing performance.
Ownership Guided C to Rust Translation
Authors: Zhang Hanliang , David Cristina , Yu Yijun , Wang Meng 
Published: July 2023

AbstractDubbed a safer C, Rust is a modern programming language that combines memory safety and low-level control. This interesting combination has made Rust very popular among developers and there is a growing trend of migrating legacy codebases (very often in C) to Rust. In this paper, we present a C to Rust translation approach centred around static ownership analysis. We design a suite of analyses that infer ownership models of C pointers and automatically translate the pointers into safe Rust equivalents. The resulting tool, Crown, scales to real-world codebases (half a million lines of code in less than 10 s) and achieves a high conversion rate.
Compositional Probabilistic Model Checking with String Diagrams of MDPs
Authors: Watanabe Kazuki , Eberhart Clovis , Asada Kazuyuki , Hasuo Ichiro 
Published: July 2023

AbstractWe present a compositional model checking algorithm for Markov decision processes, in which they are composed in the categorical graphical language ofstring diagrams. The algorithm computes optimal expected rewards. Our theoretical development of the algorithm is supported by category theory, while what we call decomposition equalities for expected rewards act as a key enabler. Experimental evaluation demonstrates its performance advantages.
Formally Verified EVM Block-Optimizations
Authors: Albert Elvira , Genaim Samir , Kirchner Daniel , Martin-Martin Enrique 
Published: July 2023

AbstractThe efficiency and the security of smart contracts are their two fundamental properties, but might come at odds: the use of optimizers to enhance efficiency may introduce bugs and compromise security. Our focus is on (Ethereum Virtual Machine) block-optimizations, which enhance the efficiency of jump-free blocks of opcodes by eliminating, reordering and even changing the original opcodes. We reconcile efficiency and security by providing the verification technology to formally prove the correctness of block-optimizations on smart contracts using the Coq proof assistant. This amounts to the challenging problem of proving semantic equivalence of two blocks of instructions, which is realized by means of three novel Coq components: a symbolic execution engine which can execute an block and produce a symbolic state; a number of simplification lemmas which transform a symbolic state into an equivalent one; and a checker of symbolic states to compare the symbolic states produced for the two blocks under comparison.Artifact:https://doi.org/10.5281/zenodo.7863483
Geschlechtsspezifische Unterschiede spezieller Tumorerkrankungen
Authors: Lehnen Nathalie , Hallek Michael 
Published: July 2023

Zusammenfassung
Hintergrund
Zahlreiche Daten zeigen, dass Geschlecht und Gender als relevante Modulatoren bestimmter onkologischer und hämatologischer Erkrankungen einen zunehmenden Stellenwert in der Präzisionsmedizin verdient haben. Dieser Beitrag soll eine Zusammenfassung des aktuellen Wissensstands über Geschlechtsunterschiede in Inzidenz und Outcome spezieller Tumorerkrankungen bieten und mögliche zugrunde liegende Ursachen näher beleuchten.

Material und Methoden
Auswertung und Diskussion von Grundlagenarbeiten, Metaanalysen und klinischen Studien

Ergebnisse
Es bestehen für eine Vielzahl der onkologischen Erkrankungen signifikante geschlechtsspezifische Unterschiede in Inzidenz, Ansprechraten und Mortalität. Zumeist haben Männer ein schlechteres Outcome, während Frauen höhere therapieassoziierte Toxizität und distinkte Präsentationen in jungem Alter aufweisen. Hormonelle, immunologische und pharmakologische Ursachen liegen nahe.

Schlussfolgerung
Eine fortschrittliche in Bezug auf die einzelnen Patient*innen individualisierte Therapie in Onkologie und Hämatologie wird sich zukünftig daran messen, die bestehenden relevanten Unterschiede zwischen den Geschlechtern im klinischen Alltag zu berücksichtigen und in Studien zugrunde liegende Mechanismen weiter zu beleuchten, um eine bestmögliche Behandlung für onkologische Patient*innen zu garantieren und zukünftig zu optimieren.
Soil Micro-eukaryotic Diversity Patterns Along Elevation Gradient Are Best Estimated by Increasing the Number of Elevation Steps Rather than Within Elevation Band Replication
Authors: Huang Shuyin , Lentendu Guillaume , Fujinuma Junichi , Shiono Takayuki , Kubota Yasuhiro , Mitchell Edward A. D. 
Published: July 2023

AbstractThe development of high-throughput sequencing (HTS) of environmental DNA (eDNA) has stimulated the study of soil microbial diversity patterns and drivers at all scales. However, given the heterogeneity of soils, a challenge is to define effective and efficient sampling protocols that allow sound comparison with other records, especially vegetation. In studies of elevational diversity pattern, a trade-off is choosing between replication within elevation bands vs. sampling more elevation bands. We addressed this question for soil protists along an elevation gradient on Mt. Asahi, Hokkaido, Japan. We compared two sampling approaches: (1) the replicate strategy (five replicates at six elevational bands, total = 30) and (2) the transect strategy (one sample in each of 16 different elevational bands). Despite a nearly twofold lower sampling effort, the transect strategy yielded congruent results compared to the replicate strategy for the estimation of elevational alpha diversity pattern: the regression coefficients between diversity indices and elevation did not differ between the two options. Furthermore, for a given total number of samples, gamma diversity estimated across the entire transect was higher when sampling more elevational bands as compared to replication from fewer elevational bands. Beta diversity (community composition turnover) was lower within a given elevational band than between adjacent bands and increased with elevation distance. In redundancy analyses, soil organic matter-related variable (the first principal component of soil organic matter, water content, total organic carbon, and nitrogen by whom were highly correlated) and elevation best explained elevational beta diversity pattern for both sampling approaches. Taken together, our results suggest that sampling a single plot per elevation band will be sufficient to obtain a good estimate of soil micro-eukaryotic diversity patterns along elevation gradients. This study demonstrated the effectiveness of the transect strategy in estimating diversity patterns along elevation gradients which is instructive for future environmental or even experimental studies. While not advocating for completely replacing replication-based sampling practices, it is important to note that both replicate and transect strategies have their merits and can be employed based on specific research goals and resource limitations.
Management of Central Venous Stenoses and Occlusions
Authors: Kitrou Panagiotis , Katsanos Konstantinos , Karnabatidis Dimitrios 
Published: July 2023

AbstractSymptomatic central venous stenosis and occlusion remains the gordian knot of vascular access. Advances in techniques, like sharp recanalization, allowed for improved success rates in crossing these difficult lesions. There is also increasing evidence of new devices in treating central venous stenosis and, at the same time, improving the time needed between interventions. High-pressure balloons, paclitaxel-coated balloons, bare metal stents and covered stents have been tested with an aim to offer additional treatment options, although obstacles still exist. In the current review, authors describe relevant techniques and options, provide the evidence and evaluate the actual implementation of these devices in this demanding field.
AgAnimalGenomes: browsers for viewing and manually annotating farm animal genomes
Authors: Triant Deborah A. , Walsh Amy T. , Hartley Gabrielle A. , Petry Bruna , Stegemiller Morgan R. , Nelson Benjamin M. , McKendrick Makenna M. , Fuller Emily P. , Cockett Noelle E. , Koltes James E. , McKay Stephanie D. , Green Jonathan A. , Murdoch Brenda M. , Hagen Darren E. , Elsik Christine G. 
Published: July 2023

AbstractCurrent genome sequencing technologies have made it possible to generate highly contiguous genome assemblies for non-model animal species. Despite advances in genome assembly methods, there is still room for improvement in the delineation of specific gene features in the genomes. Here we present genome visualization and annotation tools to support seven livestock species (bovine, chicken, goat, horse, pig, sheep, and water buffalo), available in a new resource called AgAnimalGenomes. In addition to supporting the manual refinement of gene models, these browsers provide visualization tracks for hundreds of RNAseq experiments, as well as data generated by the Functional Annotation of Animal Genomes (FAANG) Consortium. For species with predicted gene sets from both Ensembl and RefSeq, the browsers provide special tracks showing the thousands of protein-coding genes that disagree across the two gene sources, serving as a valuable resource to alert researchers to gene model issues that may affect data interpretation. We describe the data and search methods available in the new genome browsers and how to use the provided tools to edit and create new gene models.
Controlled prospective study on ultrasound simulation training in fetal echocardiography: FESIM II
Authors: Janzing Paul , Nourkami-Tutdibi Nasenien , Tutdibi Erol , Freundt Paula , von Ostrowski Thomas , Langer Martin , Zemlin Michael , Steinhard Johannes 
Published: July 2023

Abstract
Purpose
To analyze the learning curves of ultrasound novices in fetal echocardiography during structured simulation-based ultrasound training (SIM-UT) including a virtual, randomly moving fetus.

Methods
11 medical students with minimal (< 10 h) prior obstetric ultrasound experience underwent 12 h of structured fetal echocardiography SIM-UT in individual hands-on sessions during a 6-week training program. Their learning progress was assessed with standardized tests after 2, 4, and 6 weeks of SIM-UT. Participants were asked to obtain 11 fetal echocardiography standard planes (in accordance with ISUOG and AHA guidelines) as quickly as possible. All tests were carried out under real life, examination-like conditions on a healthy, randomly moving fetus. Subsequently, we analyzed the rate of correctly obtained images and the total time to completion (TTC). As reference groups, 10 Ob/Gyn physicians (median of 750 previously performed Ob/Gyn scans) and 10 fetal echocardiography experts (median of 15,000 previously performed Ob/Gyn scans) were examined with the same standardized tests.

Results
The students showed a consistent and steady improvement of their ultrasound performance during the training program. After 2 weeks, they were able to obtain > 95% of the standard planes correctly. After 6 weeks, they were significantly faster than the physician group (p < 0.001) and no longer significantly slower than the expert group (p = 0.944).

Conclusion
SIM-UT is highly effective to learn fetal echocardiography. Regarding the acquisition of the AHA/ISUOG fetal echocardiography standard planes, the students were able to reach the same skill level as the expert group within 6 weeks.
Analytic Morphomics in Myositis-Related Interstitial Lung Disease
Authors: O’Mahony Alexander T. , Henry Patrick J. , Coghlan Patrick , Waldron Michael , Crowley Claire , Ryan David , Moore Niamh , Bennett Deirdre M. , O’Connor Owen J. , Maher Michael M. , Henry Michael T. 
Published: July 2023

Abstract
Purpose
Interstitial lung disease (ILD) is the most common non-musculoskeletal manifestation of idiopathic inflammatory myopathies (IIM). Identification of body composition change may enable early intervention to improve prognosis. We investigated muscle quantity and quality derived from cross-sectional imaging in IIM, and its relationship to ILD severity.

Methods
A retrospective cohort study assessing IIM of ILD patients (n = 31) was conducted. Two datasets separated in time were collected, containing demographics, biochemical data, pulmonary function testing and thoracic CT data. Morphomic analysis of muscle quantity (cross-sectional area) and quality (density in Hounsfield Units) on thoracic CT were analysed utilising a web-based tool allowing segmentation of muscle and fat. Bilateral erector spinae and pectoralis muscle (ESM&PM) were measured at defined vertebral levels.

Results
FVC and DLCO decreased but within acceptable limits of treatment response (FVC: 83.7–78.7%, p < 0.05, DLCO 63.4–60.6%, p < 0.05). The cross-sectional area of the PM and ESM increased (PM: 39.8 to 40.7 cm2, p = 0.491; ESM: 35.2 to 39.5 cm2, p = 0.098). Density significantly fell for both the PM and ESM (PM: 35.3–31 HU, p < 0.05; ESM: 38–33.7, p < 0.05). Subcutaneous fat area increased from 103.9 to 136.1 cm2 (p < 0.05), while the visceral fat area increased but not reaching statistical significance. The change in PM density between time points demonstrated an inverse correlation with DLCO (p < 0.05, R =  − 0.49).

Conclusion
Patients with IIM ILD demonstrated significant body composition changes on CT imaging unlikely to be detected by traditional measurement tools. An increase in muscle area with an inverse decrease in density suggests poor muscle quality.
Single-port endoscopic-sentinel lymph node biopsy combined with indocyanine green and carbon nanoparticles in breast cancer
Authors: Wang Zi-Han , Gang Tian-Ran , Wu Shan-Shan , Lu Can , Gao Guo-Xuan , Xu Wei , Ding Guo-Qian , Qu Xiang , Zhang Zhong-Tao 
Published: July 2023

Abstract
Background
In order to explore the surgical safety and the reliability of axillary staging of single-port endoscopic-sentinel lymph node biopsy, we combined it with indocyanine green that was excited by near-infrared fluorescence endoscopy and carbon nanoparticles as a tracer and compared this method to conventional open sentinel lymph node biopsy.

Methods
This is a retrospective and observational study, there were 20 patients in each group and the total sample size was 60: Group 1, single-port endoscopic-sentinel lymph node biopsy combined with indocyanine green and carbon nanoparticles; Group 2, single-port endoscopic-sentinel lymph node biopsy with carbon nanoparticles only; Group 3, conventional sentinel lymph node biopsy with indocyanine green and carbon nanoparticles. Sentinel lymph node detection and upper extremity function were determined to measure the safety and efficacy of the novel single-port endoscopic-sentinel lymph node biopsy (SPE-SLNB) technique to the standard conventional sentinel lymph node biopsy technique.

Results
The detection rate of sentinel lymph nodes was 100% in Group 1, 100% in Group 2, and 95% in Group 3. There were no significant differences in upper arm function and pain scores between the three groups.

Conclusion
The novel technique of combining indocyanine green and carbon nanoparticles with single-port endoscopic-sentinel lymph node biopsy achieved a similar detection rate and mean number of sentinel lymph nodes as conventional sentinel lymph node biopsy. Traditional open surgery requires two different incisions for breast surgery and SLNB. While the most important advantage of SPE-SLNB is that two procedures can be effectively performed through a single-port in the axilla Therefore, for patients who meet the indications, single-port endoscopic-sentinel lymph node biopsy is as safe and reliable as conventional sentinel lymph node biopsy but has the aesthetic advantage of only one incision.
Efficacy of different surgical treatments for management of anal fistula: a network meta-analysis
Authors: Bhat S. , Xu W. , Varghese C. , Dubey N. , Wells C. I. , Harmston C. , O’Grady G. , Bissett I. P. , Lin A. Y. 
Published: July 2023

Abstract
Purpose
Currently, the anal fistula treatment which optimises healing and preserves bowel continence remains unclear. The aim of our study was to compare the relative efficacy of different surgical treatments for AF through a network meta-analysis.

Methods
Systematic searches of MEDLINE, EMBASE and CENTRAL databases up to October 2022 identified randomised controlled trials (RCTs) comparing surgical treatments for anal fistulae. Fistulae were classified as simple (inter-sphincteric or low trans-sphincteric fistulae crossing less than 30% of the external anal sphincter (EAS)) and complex (high trans-sphincteric fistulae involving more than 30% of the EAS). Treatments evaluated in only one trial were excluded from the primary analyses to minimise bias. The primary outcomes were rates of success in achieving AF healing and bowel incontinence.

Results
Fifty-two RCTs were included. Of the 14 treatments considered, there were no significant differences regarding short-term (6 months or less postoperatively) and long-term (more than 6 months postoperatively) success rates between any of the treatments in patients with both simple and complex anal fistula. Ligation of the inter-sphincteric fistula tract (LIFT) ranked best for minimising bowel incontinence in simple (99.1% of comparisons; 3 trials, n = 70 patients) and complex anal fistula (86.2% of comparisons; 3 trials, n = 102 patients).

Conclusions
There is insufficient evidence in existing RCTs to recommend one treatment over another regarding their short and long-term efficacy in successfully facilitating healing of both simple and complex anal fistulae. However, LIFT appears to be associated with the least impairment of bowel continence, irrespective of AF classification.