bluuebunny/crossref_metadata_2025_split huggingface dataset:
The Static Analyzer Frama-C in SV-COMP (Competition Contribution)
Authors: Beyer Dirk , Spiessl Martin 
Published: March 2022

AbstractFrama-C is a well-known platform for source-code analysis of programs written in C. It can be extended via its plug-in architecture by various analysis backends and features an extensive annotation language called ACSL. So far it was hard to compare Frama-C to other software verifiers. Our competition participation contributes an adapter named Frama-C-SV, which makes it possible to evaluate Frama-C against other software verifiers. The adapter transforms standard verification tasks (from the well-known SV-Benchmarks collection) in a way that can be understood by Frama-C and produces a verification witness as output. While Frama-C provides many different analyses, we focus on the Evolved Value Analysis (EVA), which uses a combination of different domains to over-approximate the behavior of the analyzed program.
Graves-CPA: A Graph-Attention Verifier Selector (Competition Contribution)
Authors: Leeson Will , Dwyer Matthew B. 
Published: March 2022

AbstractGraves-CPA is a verification tool which uses algorithm selection to decide an ordering of underlying verifiers to most effectively verify a given program. Graves-CPA represents programs using an amalgam of traditional program graph representations and uses state-of-the-art graph neural network techniques to dynamically decide how to run a set of verification techniques. The Graves technique is implementation agnostic, but it’s competition submission, Graves-CPA, is built using several CPAchecker configurations as its underlying verifiers.
The Static Analyzer Infer in SV-COMP (Competition Contribution)
Authors: Kettl Matthias , Lemberger Thomas 
Published: March 2022

AbstractWe present Infer-sv, a wrapper that adapts Infer for SV-COMP. Infer is a static-analysis tool for C and other languages, developed by Facebook and used by multiple large companies. It is strongly aimed at industry and the internal use at Facebook. Despite its popularity, there are no reported numbers on its precision and efficiency. With Infer-sv, we take a first step towards an objective comparison of Infer with other SV-COMP participants from academia and industry.
Ultimate GemCutter and the Axes of Generalization
Authors: Klumpp Dominik , Dietsch Daniel , Heizmann Matthias , Schüssele Frank , Ebbinghaus Marcel , Farzan Azadeh , Podelski Andreas 
Published: March 2022

AbstractUltimate GemCutter verifies concurrent programs using the CEGAR paradigm, by generalizing from spurious counterexample traces to larger sets of correct traces. We integrate classical CEGAR generalization with orthogonal generalization across interleavings. Thereby, we are able to prove correctness of programs otherwise out-of-reach for interpolation-based verification. The competition results show significant advantages over other concurrency approaches in the Ultimate family.
Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution)
Authors: Wu Tong , Schrammel Peter , Cordeiro Lucas C. 
Published: March 2022

AbstractWe describe and evaluate a violation-witness validator for Java verifiers called Wit4Java. It takes a Java program with a safety property and the respective violation-witness output by a Java verifier to generate a new Java program whose execution deterministically violates the property. We extract the value of the program variables from the counterexample represented by the violation-witness and feed this information back into the original program. In addition, we have two implementations for instantiating source programs by injecting counterexamples. Experimental results show that Wit4Java can correctly validate the violation-witnesses produced by JBMC and GDart in a few seconds.
A Direct Symbolic Algorithm for Solving Stochastic Rabin Games
Authors: Banerjee Tamajit , Majumdar Rupak , Mallik Kaushik , Schmuck Anne-Kathrin , Soudjani Sadegh 
Published: March 2022

AbstractWe consider turn-based stochastic 2-player games on graphs with$$\omega $$ω-regular winning conditions. We provide a direct symbolic algorithm for solving such games when the winning condition is formulated as a Rabin condition. For a stochastic Rabin game withkpairs over a game graph withnvertices, our algorithm runs in$$O(n^{k+2}k!)$$O(nk+2k!)symbolic steps, which improves the state of the art.We have implemented our symbolic algorithm, along with performance optimizations including parallellization and acceleration, in a BDD-based synthesis tool called . We demonstrate the superiority of compared to the state of the art on a set of synthetic benchmarks derived from the VLTS benchmark suite and on a control system benchmark from the literature. In our experiments, performed significantly faster with up totwoorders of magnitude improvement in computation time.
Sky Is Not the Limit
Authors: Havlena Vojtěch , Lengál Ondřej , Šmahlíková Barbora 
Published: March 2022

AbstractWe propose several heuristics for mitigating one of the main causes of combinatorial explosion in rank-based complementation of Büchi automata (BAs): unnecessarily high bounds on the ranks of states. First, we identifyelevator automata, which is a large class of BAs (generalizing semi-deterministic BAs), occurring often in practice, where ranks of states are bounded according to the structure of strongly connected components. The bounds for elevator automata also carry over to general BAs that contain elevator automata as a sub-structure. Second, we introduce two techniques for refining bounds on the ranks of BA states using data-flow analysis of the automaton. We implement out techniques as an extension of the toolRankerfor BA complementation and show that they indeed greatly prune the generated state space, obtaining significantly better results and outperforming other state-of-the-art tools on a large set of benchmarks.
Distributed Coalgebraic Partition Refinement
Authors: Birkmann Fabian , Deifel Hans-Peter , Milius Stefan 
Published: March 2022

AbstractPartition refinement is a method for minimizing automata and transition systems of various types. Recently we have developed a partition refinement algorithm and the tool that is generic in the transition type of the input system and matches the theoretical run time of the best known algorithms for many concrete system types. Genericity is achieved by modelling transition types as functors on sets and systems as coalgebras. Experimentation has shown that memory consumption is a bottleneck for handling systems with a large state space, while running times are fast. We have therefore extended an algorithm due to Blom and Orzan, which is suitable for a distributed implementation to the coalgebraic level of genericity, and implemented it in . Experiments show that this allows to handle much larger state spaces. Running times are low in most experiments, but there is a significant penalty for some.
Revisiting type-II see-saw: present limits and future prospects at LHC
Authors: Ashanujjaman Saiyad , Ghosh Kirtiman 
Published: March 2022

Abstract
The type-II see-saw mechanism based on the annexation of the Standard Model by weak gauge triplet scalar field proffers a natural explanation for the very minuteness of neutrino masses. Noting that the phenomenology for the non-degenerate triplet Higgs spectrum is substantially contrasting than that for the degenerate one, we perform a comprehensive study for an extensive model parameter space parametrised by the triplet scalar vacuum expectation value (VEV), the mass-splitting between the triplet-like doubly and singly charged scalars and the mass of the doubly charged scalar. Considering all Drell-Yan production mechanisms for the triplet-like scalars and taking into account the all-encompassing complexity of their decays, we derive the most stringent 95% CL lower limits on the mass of the doubly charged scalar for a vast model parameter space by implementing already existing direct collider searches by CMS and ATLAS. These estimated limits are stronger by approximately 50–230 GeV than those reported by CMS and ATLAS. Strikingly, we also find a specific region of the parameter space that is beyond the reach of the existing LHC search strategies. Then, we forecast future limits by extending an ATLAS search at high-luminosity, and we propose a search strategy that yields improved limits for a part of the parameter space.
Functions of ADP-ribose transferases in the maintenance of telomere integrity
Authors: Muoio Daniela , Laspata Natalie , Fouquerel Elise 
Published: March 2022

AbstractThe ADP-ribose transferase (ART) family comprises 17 enzymes that catalyze mono- or poly-ADP-ribosylation, a post-translational modification of proteins. Present in all subcellular compartments, ARTs are implicated in a growing number of biological processes including DNA repair, replication, transcription regulation, intra- and extra-cellular signaling, viral infection and cell death. Five members of the family, PARP1, PARP2, PARP3, tankyrase 1 and tankyrase 2 are mainly described for their crucial functions in the maintenance of genome stability. It is well established that the most describedrole of PARP1, 2 and 3 is the repair of DNA lesions while tankyrases 1 and 2 are crucial for maintaining the integrity of telomeres. Telomeres, nucleoprotein complexes located at the ends of eukaryotic chromosomes, utilize their unique structure and associated set of proteins to orchestrate the mechanisms necessary for their own protection and replication. While the functions of tankyrases 1 and 2 at telomeres are well known, several studies have also brought PARP1, 2 and 3 to the forefront of telomere protection. The singular quality of the telomeric environment has highlighted protein interactions and molecular pathways distinct from those described throughout the genome. The aim of this review is to provide an overview of the current knowledge on the multiple roles of PARP1, PARP2, PARP3, tankyrase 1 and tankyrase 2 in the maintenance and preservation of telomere integrity.
Initiation and progression of α-synuclein pathology in Parkinson’s disease
Authors: Tofaris George K. 
Published: March 2022

Abstractα-Synuclein aggregation is a critical molecular process that underpins the pathogenesis of Parkinson’s disease. Aggregates may originate at synaptic terminals as a consequence of aberrant interactions between α-synuclein and lipids or evasion of proteostatic defences. The nature of these interactions is likely to influence the emergence of conformers or strains that in turn could explain the clinical heterogeneity of Parkinson’s disease and related α-synucleinopathies. For neurodegeneration to occur, α-synuclein assemblies need to exhibit seeding competency, i.e. ability to template further aggregation, and toxicity which is at least partly mediated by interference with synaptic vesicle or organelle homeostasis. Given the dynamic and reversible conformational plasticity of α-synuclein, it is possible that seeding competency and cellular toxicity are mediated by assemblies of different structure or size along this continuum. It is currently unknown which α-synuclein assemblies are the most relevant to the human condition but recent advances in the cryo-electron microscopic characterisation of brain-derived fibrils and their assessment in stem cell derived and animal models are likely to facilitate the development of precision therapies or biomarkers. This review summarises the main principles of α-synuclein aggregate initiation and propagation in model systems, and their relevance to clinical translation.
New Expression for CDF of $$\chi _\nu '^2(\lambda )$$ Distribution and Marcum $$Q_1$$ Function
Authors: Brychkov Yury A. , Maširević Dragana Jankov , Pogány Tibor K. 
Published: March 2022

AbstractClosed form expression is established for the cumulative distribution function of the non-central $$\chi _\nu '^2(\lambda )$$

χ
ν

′
2

(
λ
)

probability distribution with integer degrees of freedom $$\nu $$
ν
. This expression includes the Humbert $$\Phi _1$$

Φ
1

(confluent Appell) hypergeometric function of two variables. A new representation of the Marcum $$Q_1$$

Q
1

function of the first order is obtained, interconnection formula accompanied with a reduction formula for specific, equal unit-parameter case of the Humbert function $$\Phi _1$$

Φ
1

and the function $$\Phi _3$$

Φ
3

are established.
COVID-19 lockdown impact on familial relationships and mental health in a large representative sample of Italian adults
Authors: Zeduri Margherita , Vigezzi Giacomo Pietro , Carioli Greta , Lugo Alessandra , Stival Chiara , Amerio Andrea , Gorini Giuseppe , Pacifici Roberta , Politi Pierluigi , Gallus Silvano , Odone Anna 
Published: March 2022

Abstract
Purpose
Benefits of national-level stay-at-home order imposed in Italy to prevent SARS-CoV-2 transmission need to be carefully weighed against its impact on citizens’ health. In a country with a strong familial culture and where welfare relies on households, confinement drastically decreased support provided by elder relatives, which may have resulted in mental health worsening.

Methods
A web-based cross-sectional study (LOST in Italy) was conducted on a representative sample of Italian adults during lockdown (27th of April–3rd of May 2020). We asked 3156 subjects to report on reduced help in housework and childcare from retired parents to assess the impact of confinement on mental health, through validated scales before and during lockdown.

Results
Overall, 1484 (47.0%) subjects reported reduced housework help from parents, and 769 (64.0%, of the 1202 subjects with children) diminished babysitting support. Subjects reporting reduced housework help had worsened sleep quality (multivariate odds ratio, OR = 1.74, 95% confidence interval, CI 1.49–2.03) and quantity (OR = 1.50, 95% CI 1.28–1.76), depressive (OR = 1.32, 95% CI 1.14–1.53) and anxiety symptoms (OR = 1.53, 95% CI 1.32–1.78), compared to those reporting unreduced help. Worsening in sleep quality (OR = 2.32, 95% CI 1.76–3.05), and quantity (OR = 1.80, 95% CI 1.36–2.37), depressive (OR = 1.79, 95% CI 1.39–2.31) and anxiety symptoms (OR = 1.90, 95% CI 1.48–2.46) was also associated with reduced babysitting help. Mental health outcomes were worse in subjects with poorer housing and teleworking during lockdown.

Conclusion
Confinement came along with reduced familial support from parents, negatively impacting household members’ mental health. Our findings might inform evidence-based family and welfare policies to promote population health within and beyond pandemic times.
Pharmacological modelling of dissociation and psychosis: an evaluation of the Clinician Administered Dissociative States Scale and Psychotomimetic States Inventory during nitrous oxide (‘laughing gas’)-induced anomalous states
Authors: Piazza Giulia G. , Iskandar Georges , Hennessy Vanessa , Zhao Hannah , Walsh Katie , McDonnell Jeffrey , Terhune Devin B. , Das Ravi K. , Kamboj Sunjeev K. 
Published: March 2022

Abstract
Rationale
A significant obstacle to an improved understanding of pathological dissociative and psychosis-like states is the lack of readily implemented pharmacological models of these experiences. Ketamine has dissociative and psychotomimetic effects but can be difficult to use outside of medical and clinical-research facilities. Alternatively, nitrous oxide (N2O) — like ketamine, a dissociative anaesthetic and NMDAR antagonist — has numerous properties that make it an attractive alternative for modelling dissociation and psychosis. However, development and testing of such pharmacological models relies on well-characterized measurement instruments.

Objectives
To examine the factor structures of the Clinician Administered Dissociative States Scale (CADSS) and Psychotomimetic States Inventory (PSI) administered during N2O inhalation in healthy volunteers.

Methods
Secondary analyses of data pooled from three previous N2O studies with healthy volunteers.

Results
Effect sizes for N2O-induced dissociation and psychotomimesis were comparable to effects reported in experimental studies with sub-anaesthetic ketamine in healthy volunteers. Although, like ketamine, a three-factor representation of N2O-induced dissociation was confirmed, and a more parsimonious two-factor model might be more appropriate. Bayesian exploratory factor analysis suggested that N2O-induced psychosis-like symptoms were adequately represented by two negative and two positive symptom factors. Hierarchical cluster analysis indicated minimal item overlap between the CADSS and PSI.

Conclusion
N2O and ketamine produce psychometrically similar dissociative states, although parallels in their psychosis-like effects remain to be determined. The CADSS and PSI tap largely non-overlapping experiences under N2O and we propose the use of both measures (or similar instruments) to comprehensively assess anomalous subjective states produced by dissociative NMDAR antagonists.
Lower Bounds on Anderson-Localised Eigenfunctions on a Strip
Authors: Goldsheid Ilya , Sodin Sasha 
Published: March 2022

AbstractIt is known that the eigenfunctions of a random Schrödinger operator on a strip decay exponentially, and that the rate of decay is not slower than prescribed by the slowest Lyapunov exponent. A variery of heuristic arguments suggest that no eigenfunction can decay faster than at this rate. We make a step towards this conjecture (in the case when the distribution of the potential is regular enough) by showing that, for each eigenfunction, the rate of exponential decay along any subsequence is strictly slower than the fastest Lyapunov exponent, and that there exists a subsequence along which it is equal to the slowest Lyapunov exponent.
Left Renal Vein Division for Juxtarenal Aortic Exposure: Influence on Renal Function and Role of the Communicating Lumbar Vein
Authors: Selberherr Andreas , Mari Marta , Klinger Markus , Burghuber Christopher , Eilenberg Wolf , Gollackner Bernd , Neumayer Christoph , Domenig Christoph 
Published: March 2022

AbstractBackgroundIn this study, we evaluate the outcome of renal function in patients undergoing juxtarenal abdominal aortic aneurysm repair with or without division of the left renal vein with special focus on the role of the communicating lumbar vein.MethodsA retrospective analysis of prospectively collected data of 110 patients undergoing elective juxtarenal abdominal aortic aneurysm repair between 2000 and 2018 was performed.The demographic characteristics and comorbidities were reviewed in detail and the renal function was analysed pre‐ and post‐operatively. The cohort of patients was split into group A (left renal vein divided) and B (left renal vein mobilised). Group A was further sub‐analysed regarding the presence of a communicating lumbar vein on preoperative imaging data (group A+ = vein present, group A− = no communicating lumbar vein present).ResultsThe patients were matched well regarding their demographic characteristics and comorbidities. In the analysis of renal function, no statistically significant difference could be detected between group A and B. In the sub‐analysis of group A, the group with a communicating lumber vein (group A+) turned out to have a significantly better renal function in the long term (sCrea 0.87 vs. 1.51; p = 0.016).ConclusionLigation of the left renal vein is a safe procedure in surgery of juxtarenal aortic aneurysms regarding the outcome of the renal function. A communicating lumbar vein between the left renal vein and the left ascending lumbar vein seems to play a key role to provide venous drainage after division of the left renal vein.
TAP Block Prior to Open Ventral Hernia Repair Improves Surgical Outcome
Authors: Licari Leo , Viola Simona , Salamone Giuseppe 
Published: March 2022

AbstractBackgroundVentral hernias commonly affect patients after major abdominal surgery. To reduce postoperative pain, the effects of the transversus abdominis plane (TAP) block, epidural analgesia and medication‐only protocol have been investigated. The primary outcome was the cumulative dosage of opioids (morphine milligram equivalents MME), of acetaminophen and diclofenac for postoperative pain control on postoperative day (POD) 0, 1, and 2. Secondary outcomes were length of stay (LOS) and the pain scale rating using the numeric rating scale (NRS) on POD 0, 1, and 2.MethodsThe data were retrospectively extracted from the charts of the patients admitted for a surgical operation for OVHR from January 2015 to December 2019.ResultsPatients receiving medication‐only analgesia had longer LOS (mean 6.1 days; p < 0.00001). Cumulative opioid consumption was significantly lower at 24 and 48 h after surgery in the TAP block group than in the other groups (mean MME 1.9 mg and 0.7 mg, respectively; p < 0.05). The cumulative consumption of diclofenac was significantly lower in the TAP block group than in the others (44.1 mg; p ≤ 0.00001 on POD 1; 4.4 mg; p = 0.03 on POD 2). TAP block is more effective in pain control in POD 0 (mean NRS 5.4; p < 0.00001), POD 1 (mean NRS 6.1; p = 0.006), and POD 2 (mean NRS 4.9; p = 0.001) if it is performed after adopting the retromuscular technique.ConclusionsThe comparison between the medication‐only technique, epidural, and TAP block demonstrated the superiority of the last one for the aims considered in this study.
Clinical impact of assessing thrombus age using magnetic resonance venography prior to catheter-directed thrombolysis
Authors: Arnoldussen Carsten W. K. P. , Notten Pascale , Brans Rutger , Vroegindeweij Dammis , Tick Lidwine W. , van de Poel Marlène H. W. , Wikkeling Otmar R. M. , Vleming Louis-Jean , Koster Ad , Jie Kon-Siong G. , Jacobs Esther M. G. , Planken Nils , Wittens Cees H. A. , ten Cate Hugo , Wildberger Joachim E. , ten Cate-Hoek Arina J. 
Published: March 2022

Abstract
Objectives
Magnetic resonance venography (MRV) is underutilized in the evaluation of thrombus properties prior to endovascular treatment but may improve procedural outcomes. We therefore investigated the clinical impact of using a dedicated MRV scoring system to assess thrombus characteristics prior to endovascular intervention for iliofemoral deep vein thrombosis (DVT).

Methods
This is a post hoc analysis of data from the CAVA trial (Clinicaltrials.gov:NCT00970619). MRV studies of patients receiving ultrasound-accelerated catheter-directed thrombolysis (CDT) for iliofemoral DVT were reviewed. Thrombus age-related imaging characteristics were scored and translated into an overall score (acute, subacute, or old). MRV scores were compared to patient-reported complaints. MRV-scored groups were compared for CDT duration and success rate.

Results
Fifty-six patients (29 men; age 50.8 ± 16.4 years) were included. Using MRV, 27 thrombi were classified acute, 17 subacute, and 12 old. Based on patient-reported complaints, 11 (91.7%) of these old thrombi would have been categorized acute or subacute, and one (3.7%) of the acute thrombi as old. Average duration of CDT to > 90% restored patency differed significantly between groups (p < 0.0001): average duration was 23 h for acute thromboses (range: 19–25), 43 h for subacute (range: 41–62), and 85 h for old thromboses (range: 74–96). CDT was almost eleven times more successful in thromboses characterized as acute and subacute compared to old thromboses (OR: 10.7; 95% CI 2.1–55.5).

Conclusion
A dedicated MRV scoring system can safely discriminate between acute, subacute, and old thromboses. MRV-based selection is predictive of procedural duration and success rate and can help avoid unnecessary complications.

Key Points
• Thrombus age, characterized by MRV as acute, subacute, and old, can predict CDT duration and probability of success.
• Accurate pre-interventional MRV-based thrombus aging has the potential to facilitate identification of eligible patients and may thus prevent CDT-related complications.