bluuebunny/crossref_metadata_2025 huggingface dataset:
ASMETA Tool Set for Rigorous System Design
Authors: Bombarda Andrea , Bonfanti Silvia , Gargantini Angelo , Riccobene Elvinia , Scandurra Patrizia
Published: September 2024

This tutorial paper introduces ASMETA, a comprehensive suite of integrated tools around the formal method Abstract State Machines to specify and analyze the executable behavior of discrete event systems. ASMETA supports the entire system development life-cycle, from the specification of the functional requirements to the implementation of the code, in a systematic and incremental way. This tutorial provides an overview of ASMETA through an illustrative case study, the Pill-Box, related to the design of a smart pillbox device. It illustrates the practical use of the range of modeling and V&V techniques available in ASMETA and C++ code generation from models, to increase the quality and reliability of behavioral system models and source code.
Practical Deductive Verification of OCaml Programs
Authors: Pereira Mário
Published: September 2024

In this paper, we provide a comprehensive, hands-on tutorial on how to apply deductive verification to programs written in . In particular, we show how one can use the specification language and the tool to conduct mostly-automated verification on code. In our presentation, we focus on two main classes of programs: first, purely functional programs with no mutable state; then on imperative programs, where one can mix mutable state with subtle control-flow primitives, such as locally-defined exceptions.
FM-Weck: Containerized Execution of Formal-Methods Tools
Authors: Beyer Dirk , Wachowitz Henrik
Published: September 2024

Software is ubiquitous in the digital world, and the correct function of software systems is critical for our society, industry, and infrastructure. While testing and static analysis are long-established techniques in software-development processes, it became widely acknowledged only in the past two decades that formal methods are required for giving guarantees of functional correctness. Both academia and industry worked hard to develop tools for formal verification of software during the past two decades, with the result that many software verifiers are available now (for example, 59 freely available verifiers for C and Java programs). However, most software verifiers are challenging to find, install, and use for both external researchers and potential users. FM-Weck changes this: It provides a fully automatic, zero-configuration container-based setup and execution for more than 50 software verifiers for C and Java. Both the setup requirements and execution parameters of every supported verifier are provided by the tool developers themselves as part of the FM-Tools metadata format that was established recently and was already used by the international competitions SV-COMP and Test-Comp. With our solution FM-Weck, anyone gets fast and easy access to state-of-the-art formal verifiers, no expertise required, fully reproducible.
The Java Verification Tool KeY:A Tutorial
Authors: Beckert Bernhard , Bubel Richard , Drodt Daniel , Hähnle Reiner , Lanzinger Florian , Pfeifer Wolfram , Ulbrich Mattias , Weigl Alexander
Published: September 2024

The KeY tool is a state-of-the-art deductive program verifier for the Java language. Its verification engine is based on a sequent calculus for dynamic logic, realizing forward symbolic execution of the target program, whereby all symbolic paths through a program are explored. Method contracts make verification scalable. KeY combines auto-active and fine-grained proof interaction, which is possible both at the level of the verification target and its specification, as well as at the level of proof rules and program logic. This makes KeY well-suited for teaching program verification, but also permits proof debugging at the source code level. The latter made it possible to verify some of the most complex Java code to date. The article provides a self-contained introduction to the working principles and the practical usage of KeY for anyone with basic knowledge in logic and formal methods.
A Tutorial on Stream-Based Monitoring
Authors: Baumeister Jan , Finkbeiner Bernd , Kohn Florian , Scheerer Frederik
Published: September 2024

Stream-based runtime monitoring frameworks are safety assurance tools that check the runtime behavior of a system against a formal specification. This tutorial provides a hands-on introduction to RTLola, a real-time monitoring toolkit for cyber-physical systems and networks. RTLola processes, evaluates, and aggregates streams of input data, such as sensor readings, and provides a real-time analysis in the form of comprehensive statistics and logical assessments of the system’s health. RTLola has been applied successfully in monitoring autonomous systems such as unmanned aircraft. The tutorial guides the reader through the development of a stream-based specification for an autonomous drone observing other flying objects in its flight path. Each tutorial section provides an intuitive introduction, highlighting useful language features and specification patterns, and gives a more in-depth explanation of technical details for the advanced reader. Finally, we discuss how runtime monitors generated from RTLola specifications can be integrated into a variety of systems and discuss different monitoring applications.
DFAMiner: Mining Minimal Separating DFAs from Labelled Samples
Authors: Dell’Erba Daniele , Li Yong , Schewe Sven
Published: September 2024

We propose , a passive learning tool for learning minimal separating deterministic finite automata (DFA) from a set of labelled samples. Separating automata are an interesting class of automata that occurs generally in regular model checking and has raised interest in foundational questions of parity game solving. We first propose a simple and linear-time algorithm that incrementally constructs a three-valued DFA (3DFA) from a set of labelled samples given in the usual lexicographical order. This 3DFA has accepting and rejecting states as well as don’t-care states, so that it can exactly recognise the labelled examples. We then apply our tool to mining a minimal separating DFA for the labelled samples by minimising the constructed automata via a reduction to SAT solving. Empirical evaluation shows that our tool outperforms current state-of-the-art tools significantly on standard benchmarks for learning minimal separating DFAs from samples. Progress in the efficient construction of separating DFAs can also lead to finding the lower bound of parity game solving, where we show that can create optimal separating automata for simple languages with up to 7 colours. Future improvements might offer inroads to better data structures.
Automated Static Analysis of Quality of Service Properties of Communicating Systems
Authors: Pombo Carlos G. Lopez , Suñé Agustín Eloy Martinez , Tuosto Emilio
Published: September 2024

We present "Image missing", a bounded "Image missing""Image missing"to statically analyse Quality of Service ( "Image missing") properties of message-passing systems. We consider QoS properties on measurable application-level attributes as well as resource consumption metrics, for example, those relating monetary cost to memory usage. The applicability of "Image missing"is evaluated through case studies and experiments. A first case study is based on the AWS cloud while a second one analyses a communicating system automatically extracted from code. Additionally, we consider synthetically generated experiments to assess the scalability of "Image missing". These experiments showed that our model can faithfully capture and effectively analyse QoS properties in industrial-strength scenarios.
Alloy Repair Hint Generation Based on Historical Data
Authors: Barros Ana , Neto Henrique , Cunha Alcino , Macedo Nuno , Paiva Ana C. R.
Published: September 2024

Platforms to support novices learning to program are often accompanied by automated next-step hints that guide them towards correct solutions. Many of those approaches are data-driven, building on historical data to generate higher quality hints. Formal specifications are increasingly relevant in software engineering activities, but very little support exists to help novices while learning. Alloy is a formal specification language often used in courses on formal software development methods, and a platform—Alloy4Fun—has been proposed to support autonomous learning. While non-data-driven specification repair techniques have been proposed for Alloy that could be leveraged to generate next-step hints, no data-driven hint generation approach has been proposed so far. This paper presents the first data-driven hint generation technique for Alloy and its implementation as an extension to Alloy4Fun, being based on the data collected by that platform. This historical data is processed into graphs that capture past students’ progress while solving specification challenges. Hint generation can be customized with policies that take into consideration diverse factors, such as the popularity of paths in those graphs successfully traversed by previous students. Our evaluation shows that the performance of this new technique is competitive with non-data-driven repair techniques. To assess the quality of the hints, and help select the most appropriate hint generation policy, we conducted a survey with experienced Alloy instructors.
Ethik – normativ gesetzter Baustein in Pflegekammern
Authors: Kuhn Andrea
Published: September 2024

Der erste Argumentationsstrang umfasst die Rezeption von Ethik in Pflegekammern. Pflegekammern ermöglichen als Körperschaften des öffentlichen Rechtes die Selbstverwaltung der Profession Pflege zur Sicherstellung der pflegerischen Gesundheitsversorgung der Bevölkerung. Das Professionsmerkmal Berufsethik wurde professionspolitisch über Jahrzehnte der ausstehenden Verkammerung zugeordnet. Nun haben Pflegekammern den Sprung auf die politische Agenda geschafft. In mehreren Bundesländern ist die Gesetzgebung abgeschlossen, Pflegekammern befinden sich im Aufbau. In sieben Bundesländern wird die politische Situation mit Fokus auf dem Themenkomplex Ethik nachgezeichnet und Lücken aufgezeigt. Rheinland-Pfalz ist Vorreiter, die Landespflegekammer nahm 2016 ihre Arbeit auf und ist mittlerweile voll etabliert, das Thema Ethik im Aufbauprozess wird nachgezeichnet. Schleswig–Holstein und Niedersachsen starteten zwei Jahre später, dargelegt wird, inwieweit das Thema Ethik Beachtung fand, auch wird die rückwärtsgewandte Situation im Norden aufgenommen. Bayern führte bereits 2013 eine repräsentative Befragung durch. Trotz des mehrheitlichen Votums der Pflegefachpersonen für eine Pflegekammer hat sich der Freistaat bis heute für einen anderen Weg entschieden. Andere Bundesländer sondierten noch 2021 die Errichtung einer Pflegekammer. Absichtserklärungen fanden sich in den Koalitionsverträgen von Hessen, Baden-Württemberg und Nordrhein-Westfalen. Es herrschte politische Unsicherheit über die Etablierung einer solchen Körperschaft. Zur politischen Entscheidungsfindung wurden Befragungen der Berufsgruppe durchgeführt. Die Ergebnisse zeitigten unterschiedliche Konsequenzen. Die Analyseergebnisse des ersten Pipeline Logic Models fassen die aktuelle Situation zusammen: Zum einen fehlt die Konkretion des ethischen Mandates zur nachhaltigen Unterstützung von Pflegefachpersonen; zum anderen wird der Status der deutschen Pflege als Spielball politischer Mächte als Ursache und Wirkung dieses Defizits gleichermaßen deutlich.
Reliability of Moment Tensor Inversion for Different Seismic Networks
Authors: Tymińska Anna , Lizurek Grzegorz
Published: September 2024

The article investigates the reliability of moment tensor (MT) inversion in time domain with use of first P-wave amplitude, a method used to determine the source mechanisms of earthquakes, across four different seismic networks. The study compares the synthetic tests results of MT inversion for two underground mining and two artificial reservoir monitoring seismic networks. The analysis was performed to assesses how consistency and accuracy of the results depend on different factors like: network configuration, events depth, velocity model, focal mechanism of event and applied noise. The findings highlight the impact of network configuration compared to other variables and data quality on the reliability of moment tensor inversion and provide insights into different factors which have to be considered to enhance MT accuracy. The significance of events depth in P-wave amplitude MT inversion and the necessity to consider velocity model influence, especially presence of high velocity gradient, is highlighted by the presented results.
Epidemiology of postinjury multiple organ failure: a prospective multicenter observational study
Authors: Ting Ryan S. , Weaver Natasha A. , King Kate L. , Way Teagan L. , Sarrami Pooria , Daniel Lovana , Dinh Michael , Nair Priya , Hsu Jeremy , D’Amours Scott K. , Balogh Zsolt J.
Published: September 2024

Purpose

Postinjury multiple organ failure (MOF) is the sequela to the disease of polytrauma. We aimed to describe the contemporary population-based epidemiology of MOF within a mature trauma system, to analyse the time taken for MOF to develop, and to evaluate the temporal patterns and contributions of the individual constituent organ failures.

Methods

Prospective observational study conducted across five Level-1 trauma centers in New South Wales, Australia. Trauma patients at-risk of MOF (Denver > 3 from 48 h post-admission), aged > 16 years, ISS > 15, and who stayed in ICU for ≥ 48 h were eligible for inclusion.

Results

From May 2018–February 2021, 600 at-risk polytrauma patients were prospectively enrolled (mean(SD)age = 49(21)years, males = 453/600(76%),median(IQR)ISS = 26(20,34)). MOF incidence was 136/600(23%) among at-risk patients, 142/6248(2%) among major trauma patients (ISS > 12 per Australian definition), and 0.8/100,000 in the general population. The mortality rate was 55/600(11%) in the overall study population, and 34/136(25%) in MOF patients. 82/136(60%) of MOF patients developed MOF on day-3. No patients developed MOF after day-13. Among MOF patients, 60/136(44%) had cardiac failures (mortality = 37%), 39/136(29%) had respiratory failures (mortality = 23%), 24/136(18%) had renal failures (mortality = 63%), and 12/136(9%) had hepatic failures (mortality = 50%).

Conclusion

Although a rare syndrome in the general population, MOF occurred in 23% of the most severely injured polytrauma patients. When compared to previous risk-matched cohorts, MOF become more common, but not more lethal, despite a decade older cohort. The heart has superseded the lungs as the most common organ to fail. Cardiac and respiratory failures occurred earlier and were associated with lower mortality than renal and hepatic failures.
Beinachsenkorrektur mit Osteotomie der proximalen Tibia – Update
Authors: Kastner Josephine , Mengis Natalie , Rippke Jules-Nikolaus , Ammann Elias , Toth Laszlo , Koch Matthias , Hirschmann Michael T.
Published: September 2024

Durch eine deutliche Zunahme der Inzidenz von Knorpel‑, Kreuzband- und Meniskusverletzungen im Freizeitbereich ist auch bei jüngeren Patienten eine steigende Inzidenz von degenerativen Veränderungen wie einer Kniegelenkarthrose festzustellen. Um eine sinnvolle Therapieempfehlung geben zu können, ist die eingehende Kenntnis der zugrundeliegenden Pathologien und deren Therapieoptionen unabdingbar. Die hohe Tibiaosteotomie (HTO) stellt in diesem Zusammenhang eine der möglichen Behandlungsoptionen dar, die insbesondere bei jüngeren Patienten mit einer Beinachsenfehlstellung und hohen körperlichen Anforderungen in Betracht gezogen werden sollte. In dieser Übersichtsarbeit soll eine zusammenhängende Darstellung von der Indikationsstellung über die korrekte Vermessung und Beurteilung der Beinachse bis hin zur Planung und operativen Versorgung gegeben werden. Besonderes Augenmerk wird auf die aktuellen wissenschaftlichen Erkenntnisse und Parameter gelegt, die in den letzten Jahren gewonnen wurden.
Solitär fibröser Tumor in einem follikulären Adenom der Schilddrüse
Authors: Theurer Sarah , Schimmack Simon , Baba Hideo A.
Published: September 2024

Bei einer 28-jährigen Patientin lag ein größenprogredienter Knoten der Schilddrüse vor, der aufgrund einer lokalen Beschwerdesymptomatik operativ entfernt wurde. Histologisch konnte ein solitär fibröser Tumor (SFT) in einem Schilddrüsenadenom diagnostiziert werden. Molekulargenetisch lag eine spezifische NAB2-STAT6-Fusion vor.

Solitär Fibröse Tumoren kommen selten in der Schilddrüse vor und sind dort sowohl als Primär- wie auch als Sekundärmanifestation beschrieben. Dabei erfolgen die Diagnostik, die Prognoseabschätzung und die Therapieentscheidung analog zu SFT anderer Lokalisation.
Simulating the aftermath of Northern European Enclosure Dam (NEED) break and flooding of European coast
Authors: Maczuga Paweł , Łoś Marcin , Valseth Eirik , Serra Albert Oliver , Siwik Leszek , Celaya Elisabede Alberdi , Paszyńska Anna , Paszyński Maciej
Published: September 2024

The Northern European Enclosure Dam (NEED) is a hypothetical project to prevent flooding in European countries following the rising ocean level due to melting arctic glaciers. This project involves the construction of two large dams between Scotland and Norway, as well as England and France. The anticipated cost of this project is 250 to 500 billion euros. In this paper, we present the simulation of the aftermath of flooding on the European coastline caused by a catastrophic break of this hypothetical dam. From our simulation results, we can observe a traveling wave after the accident, with a velocity of approximately 45 kms per hour, raising the sea level permanently inside the dammed region. This observation implies a need to construct additional dams or barriers protecting the Netherlands’ northern coastline and the Baltic Sea’s interior. Our simulations have been obtained using the following building blocks. First, a graph transformation model was applied to generate an adaptive mesh, refined towards the seabed and the seashore topography, approximating the topography of the Earth. We employ the composition graph grammar model to break the mesh’s triangular elements without generating hanging nodes. Second, the wave equation is formulated in a spherical latitude-longitude system of coordinates and solved by a high-order time integration scheme using the generalized $$\alpha$$
α
method. While our paper mainly focuses on the simulation of the NEED dam break, we also provide a stand-alone tool to generate an adaptive mesh of the whole Earth. We can use our software as a stand-alone package in FEniCS or other simulation software.
Photoneuroendocrine, circadian and seasonal systems: from photoneuroendocrinology to circadian biology and medicine
Authors: Korf Horst-Werner
Published: September 2024

This contribution highlights the scientific development of two intertwined disciplines, photoneuroendocrinology and circadian biology. Photoneuroendocrinology has focused on nonvisual photoreceptors that translate light stimuli into neuroendocrine signals and serve rhythm entrainment. Nonvisual photoreceptors first described in the pineal complex and brain of nonmammalian species are luminance detectors. In the pineal, they control the formation of melatonin, the highly conserved hormone of darkness which is synthesized night by night. Pinealocytes endowed with both photoreceptive and neuroendocrine capacities function as “photoneuroendocrine cells.” In adult mammals, nonvisual photoreceptors controlling pineal melatonin biosynthesis and pupillary reflexes are absent from the pineal and brain and occur only in the inner layer of the retina. Encephalic photoreceptors regulate seasonal rhythms, such as the reproductive cycle. They are concentrated in circumventricular organs, the lateral septal organ and the paraventricular organ, and represent cerebrospinal fluid contacting neurons. Nonvisual photoreceptors employ different photopigments such as melanopsin, pinopsin, parapinopsin, neuropsin, and vertebrate ancient opsin. After identification of clock genes and molecular clockwork, circadian biology became cutting-edge research with a focus on rhythm generation. Molecular clockworks tick in every nucleated cell and, as shown in mammals, they drive the expression of more than 3000 genes and are of overall importance for regulation of cell proliferation and metabolism. The mammalian circadian system is hierarchically organized; the central rhythm generator is located in the suprachiasmatic nuclei which entrain peripheral circadian oscillators via multiple neuronal and neuroendocrine pathways. Disrupted molecular clockworks may cause various diseases, and investigations of this interplay will establish a new discipline: circadian medicine.
Noninvasive biomarkers for the detection of GERD-induced pulmonary injury
Authors: Latorre-Rodríguez Andrés R. , Mittal Sumeet K. , Ravichandran Ranjithkumar , Reynolds Austin , Isaza-Restrepo Andrés , Mittal Jahanvi , Hahn Mary F. , Bremner Ross M. , Mohanakumar Thalachallour
Published: September 2024

Background

The role of gastroesophageal reflux in progressive lung damage is increasingly recognized. We have proposed, based on our work with lung transplant recipients, a novel immune mechanism of pulmonary injury after aspiration of gastric contents, during which higher levels of normally sequestered lung self-antigens (SAgs) collagen V (Col-V) and K-alpha-1 tubulin (Kα1T) in circulating small extracellular vesicles (EVs) induce the production of self-antibodies (SAbs) anti-Col-V and anti-Kα1T. Thus, we aimed to determine whether levels of SAbs or SAgs increased in an animal model of aspiration-induced lung damage in a nontransplant setting.

Methods

We created a murine model of repetitive lung aspiration using C57BL/6J mice. Mice were aspirated weekly with 1 mL/kg of hydrochloric acid (n = 9), human gastric contents (n = 9), or combined (1:1) fluid (n = 9) once, three, or six times (n = 3 in each subgroup; control group, n = 9). Blood samples were periodically obtained, and all animals were sacrificed at day 90 for pathological assessment. SAbs were measured using an enzyme-linked immunosorbent assay; SAgs and NF-κB contained in small EVs were assessed by western blot.

Results

Aspirated mice weighed significantly less than controls throughout the study and had histological evidence of pulmonary injury at day 90. Overall, aspirated mice developed higher concentrations of anti-Col-V at day 28 (53.9 ± 28.7 vs. 29.9 ± 4.5 ng/mL, p < 0.01), day 35 (42.6 ± 19.8 vs. 28.6 ± 7.2 ng/mL, p = 0.038), and day 90 (59.7 ± 27.7 vs. 34.1 ± 3.2 ng/mL, p = 0.014) than the control group. Circulating small EVs isolated from aspirated mice on day 90 contained higher levels of Col-V (0.7 ± 0.56 vs. 0.18 ± 0.6 m.o.d., p = 0.009) and NF-κB (0.42 ± 0.27 vs. 0.27 ± 0.09 m.o.d., p = 0.095) than those from controls.

Conclusions

This experimental study supports the theory that gastroesophageal reflux leads to the development of lung damage and an increase of humoral markers that may serve as noninvasive biomarkers to detect asymptomatic lung injury among patients with gastroesophageal reflux disease.
Open versus robotic retromuscular ventral hernia repair: outcomes of the ORREO prospective randomized controlled trial
Authors: Warren Jeremy A. , Blackhurst Dawn , Ewing Joseph A. , Carbonell Alfredo M.
Published: September 2024

Background

Robotic retromuscular ventral hernia repair (rRMVHR) potentially combines the best features of open and minimally invasive VHR: myofascial release with abdominal wall reconstruction (AWR) with the lower wound morbidity of laparoscopic VHR. Proliferation of this technique has outpaced the data supporting this claim. We report 2-year outcomes of the first randomized controlled trial of oRMVHR vs rRMVHR.

Methods

Single-center randomized control trial of open vs rRMVHR. 100 patients were randomized (50 open, 50 robotic). We included patients > 18 y/o with hernias 7–15 cm with at least one of the following: diabetes, chronic obstructive pulmonary disease (COPD), body mass index (BMI) ≥ 30, or current smokers. Primary outcome was occurrence of a composite outcome of surgical site infection (SSI), non-seroma surgical site occurrence (SSO), readmission, or hernia recurrence. Secondary outcomes were length of stay, any SSI or SSO, SSI/SSOPI, operative time, patient reported quality of life, and cost. Analysis was performed in an intention-to-treat fashion. Study was funded by a grant from Society of American Gastrointestinal and Endoscopic Surgeons.

Results

90 patients were available for 30-day and 62 for 2-year analysis (rRMVHR = 46 and 32, oRMVHR = 44 and 30). Hernias in the open group were slightly larger (10 vs 8 cm, p = 0.024) and more likely to have prior mesh (36.4 vs 15.2%; p = 0.030), but were similar in length, prior hernia repairs, mesh use, and myofascial release. There was no difference in primary composite outcome between oRMVHR and rRMVHR (20.5 vs 19.6%, p = 1.000). Median length of stay was shorter for rRMVHR (1 vs 2 days; p < 0.001). All patients had significant improvement in quality of life at 1 and 2 years. Other secondary outcomes were similar.

Conclusion

There is no difference in a composite outcome including SSI, SSOPI, readmission, and hernia recurrence between open and robotic RMVHR.

Graphical abstract
Effect of COVID-19 changes on outcomes and socioeconomic disparities following metabolic and bariatric surgery
Authors: Ahmed Shushmita M. , Johns Alexandra , Timbang Leah , Wang Annie , Singh Navneet Kaur , Lyo Victoria , Ali Mohamed
Published: September 2024

Background

We previously showed worse outcomes among lower socioeconomic status (SES) groups following metabolic/bariatric surgery (MBS). In light of healthcare changes in response to COVID-19, this study aims to evaluate post-pandemic MBS outcomes and determine if prior socioeconomic disparities persisted in the post-COVID era.

Methods

A retrospective chart review of patients undergoing primary Roux-en-Y gastric bypass (RYGB) and sleeve gastrectomy (SG) between 2015 and 2022 was performed. Patients were stratified into pre- and post-COVID groups. Post-COVID cohort was further stratified into high (HT) and low (LT) tier status based on Distressed Communities Index, a geocoded composite measure of SES. Preoperative characteristics and postoperative outcomes were compared between pre- and post-COVID cohorts, as well as between post-COVID HT and LT groups.

Results

Of 709 patients, 82.9% were pre-COVID and 17.1% were post-COVID. Post-COVID cohort had greater rate of public insurance (46% vs. 37%, p < 0.001), longer wait time to surgery (mean 358 ± 609.8 days vs 241.9 ± 368.5 days, p = 0.045), and were more likely to undergo RYGB (69% vs. 56%, p = 0.010). Post-COVID patients also had lower risk of any complications on multivariable analysis (OR 0.599, 95% CI 0.372–0.963), had higher follow-up rates at post-discharge (95.8% vs 79.7%, p < 0.005), 6-month (93% vs. 82%, p < 0.001) and 12-month visits (75% vs. 63%, p = 0.005), and lost more weight at 12 months (67% excess weight loss (%EWL) vs. 58%EWL, p = 0.002). Among post-COVID HT and LT cohorts, previously seen disparities in complications were no longer seen. Finally, there were no differences in weight or follow-up rates between post-COVID HT and LT.

Conclusions

Post-COVID changes to MBS care have resulted in improved short-term outcomes and reduced disparities for patients of lower SES. Further studies are needed to identify these positive factors to perpetuate practice patterns that optimize care for patients of all socioeconomic status.
Neue Empfehlungen zur palliativen Sedierung
Authors: Surges Séverine Marie , Brunsch Holger , Przyborek Marta , Jaspers Birgit , Radbruch Lukas
Published: September 2024

Palliative Sedierung zielt auf die Linderung von refraktärem Leid bei Patienten mit lebenslimitierender Erkrankung ab. Das Rahmenwerk zur palliativen Sedierung der Europäischen Gesellschaft für Palliativmedizin (European Association for Palliative Care [EAPC]) von 2009 wurde vor Kurzem aktualisiert. In Deutschland wurden von der SedPall-Forschungsgruppe ebenfalls Empfehlungen formuliert. Der vorliegende Beitrag beschreibt die soziale und ethische Komplexität der Entscheidungsfindung und fasst die Empfehlungen zusammen. Die Autonomie des Patienten wird hervorgehoben. Die Bestimmung der Refraktärität des Leids soll gemeinsam von Arzt und Patient vorgenommen werden. Die Sedierung soll proportional erfolgen, das heißt, ihre Form und Dauer werden an die individuelle Situation des Patienten angepasst. Die Entscheidungen zur palliativen Sedierung und zur Hydratation sollen getrennt erfolgen. Midazolam gilt als Medikament der ersten Wahl. Besondere Aufmerksamkeit ist den Angehörigen und dem Behandlungsteam zu widmen.
Pain, Substance Use Disorders, Mental Health, and Buprenorphine Treatment among Patients With and Without HIV
Authors: Miller Emily A. , McGinnis Kathleen A. , Edelman E. Jennifer , Feinberg Termeh , Gordon Kirsha S. , Kerns Robert D. , Marshall Brandon D. L. , Patterson Julie A. , McRae MaryPeace
Published: September 2024

Treatment of opioid use disorder (OUD) with buprenorphine improves outcomes and mortality among people with HIV (PWH). However, engagement is low and is influenced by comorbidities. We examined the impact of patterns of co-occurring pain, substance use disorders (SUDs), and mental health diagnoses on buprenorphine initiation and retention in PWH. The Veterans Aging Cohort Study contained 7,875 patients (2,702 PWH and 5,173 without HIV) with new OUD clinical encounters (2008–2017). Buprenorphine initiation and retention were derived from prescription data. We identified patterns of co-occurring diagnoses (via ICD codes) and assessed the effects of class membership on both outcomes using latent class analysis and regression analyses. The mean age of patients was 55, 98% were male, 58% Black, 8% Hispanic, and only 8% initiated buprenorphine within 12 months of OUD diagnosis. Four classes of co-occurring diagnoses were identified: “Few Co-occurring Diagnoses” (42.3%); “Multiple Pain Conditions” (21.3%); “Pain + SUD” (18.4%) and “Pain + SUD + Mental Health” (18.0%). Patients in the “Pain + SUD” class and “Pain + SUD + Mental Health” class were significantly less likely to initiate buprenorphine and had 59% and 45% lower odds, respectively, of initiating buprenorphine compared with patients in the “Few Co-occurring Diagnoses” class; this effect did not vary by HIV status. Buprenorphine retention was not significantly associated with HIV status or class membership. However, Black Veterans were less likely to initiate or be retained in buprenorphine treatment. Higher comorbidity burden was negatively associated with buprenorphine initiation but not with retention. More research is warranted to determine other factors that may influence treatment retention.
Reducing the computational effort of symbolic supervisor synthesis
Authors: Thuijsman Sander , Hendriks Dennis , Reniers Michel
Published: September 2024

Supervisor synthesis is a means to algorithmically derive a supervisory controller from a discrete-event model of a system and a requirements specification. For large systems, synthesis suffers from state space explosion. To mitigate this, synthesis can be applied to a symbolic representation of the models by using Binary Decision Diagrams (BDDs). Peak used BDD nodes and BDD operation count are introduced as deterministic and platform independent metrics to express the computational effort of a symbolic synthesis. These BDD-based metrics are useful to analyze the efficiency of the synthesis algorithm. From this analysis, modifications can be made to how BDDs are handled during synthesis, improving synthesis efficiency. We demonstrate this approach by introducing and analyzing: DCSH, a variable ordering heuristic; several edge ordering heuristics; and an approach to efficiently enforce state exclusion requirements in synthesis. These methods were recently implemented in our open source supervisory control tool: Eclipse ESCET. The analysis is based on large scale experiments of performing synthesis on a variety of models from literature. We show that: (1) by using DCSH, synthesis with high computational effort can be avoided, and generally low computational effort is required, relative to the variable ordering heuristics that were used prior to this work; (2) applying reverse-model edge order realizes relatively low synthesis effort; and (3) state exclusion requirements can efficiently be enforced by restricting edge guards prior to synthesis. While these methods reduce computational effort in practice, it should be noted that they do not affect the theoretical (worst-case) complexity of synthesis.
Abstraction Modulo Stability
Authors: Becchi Anna , Cimatti Alessandro
Published: September 2024

The analysis of legacy systems requires the automated extraction of high-level specifications. We propose a framework, called Abstraction Modulo Stability, for the analysis of transition systems operating in stable states, and responding with run-to-completion transactions to external stimuli. The abstraction captures, in the form of a finite state machine, the effects of external stimuli on the system state. This approach is parametric on a set of predicates of interest and on the definition of stability. We consider some possible stability definitions, which yield different practically relevant abstractions, and propose parametric algorithms for abstraction computation. The framework is evaluated in terms of expressivity and adequacy within an industrial project with the Italian Railway Network, on reverse engineering of relay-based interlocking circuits to extract specifications for a computer-based reimplementation.
Evolving code with a large language model
Authors: Hemberg Erik , Moskal Stephen , O’Reilly Una-May
Published: September 2024

Algorithms that use Large Language Models (LLMs) to evolve code arrived on the Genetic Programming (GP) scene very recently. We present LLM_GP, a general LLM-based evolutionary algorithm designed to evolve code. Like GP, it uses evolutionary operators, but its designs and implementations of those operators significantly differ from GP’s because they enlist an LLM, using prompting and the LLM’s pre-trained pattern matching and sequence completion capability. We also present a demonstration-level variant of LLM_GP and share its code. By presentations that range from formal to hands-on, we cover design and LLM-usage considerations as well as the scientific challenges that arise when using an LLM for genetic programming.
Geodesic vector fields, induced contact structures and tightness in dimension three
Authors: Becker Tilman
Published: September 2024

In this paper, we provide new and simpler proofs of two theorems of Gluck and Harrison on contact structures induced by great circle or line fibrations. Furthermore, we prove that a geodesic vector field whose Jacobi tensor is parallel along flow lines (e.g. if the underlying manifold is locally symmetric) induces a contact structure if the ‘mixed’ sectional curvatures are nonnegative, and if a certain nondegeneracy condition holds. Additionally, we prove that in dimension three, contact structures admitting a Reeb flow which is either periodic, isometric, or free and proper, must be universally tight. In particular, we generalise an earlier result of Geiges and the author, by showing that every contact form on $${\mathbb {R}}^3$$

R

3

whose Reeb vector field spans a line fibration is necessarily tight. Furthermore, we provide a characterisation of isometric Reeb vector fields. As an application, we recover a result of Kegel and Lange on Seifert fibrations spanned by Reeb vector fields, and we classify closed contact 3-manifolds with isometric Reeb flows (also known as R-contact manifolds) up to diffeomorphism.
COSINUS:TES-instrumented NaI Crystals for Direct Dark Matter Search
Authors: Stahlberg M. , Angloher G. , Bharadwaj M. R. , Cababie M. R. , Dafinei I. , Di Marco N. , Einfalt L. , Ferroni F. , Fichtinger S. , Filipponi A. , Frank T. , Friedl M. , Fuss A. , Ge Z. , Heikinheimo M. , Hughes M. N. , Huitu K. , Kellermann M. , Maji R. , Mancuso M. , Pagnanini L. , Petricca F. , Pirro S. , Pröbst F. , Profeta G. , Puiu A. , Reindl F. , Schäffner K. , Schieck J. , Schmiedmayer D. , Schreiner P. , Schwertner C. , Shera K. , Stendahl A. , Stukel M. , Tresca C. , Wagner F. , Yue S. , Zema V. , Zhu Y.
Published: September 2024

In the last years, the COSINUS (Cryogenic Observatory for SIgnals seen in Next generation Underground Searches) experiment has made significant progress both in the construction of its facility and in pursuing its physics goals: At Laboratori Nazionali del Gran Sasso (LNGS) in Italy, an underground facility was constructed, which will house experimental detectors for dark matter direct detection in a dry dilution cryostat. Construction of the main structures at the COSINUS site is finished, including the control building, the cryostat access level, and the water tank which will serve as a Cherenkov muon veto around the cryostat. With a nuclear recoil threshold of 4 keV, the latest COSINUS detector prototype approaches the design goal of 1 keV, and particle discrimination on event-by-event basis has been demonstrated. This contribution gives a brief overview on the status of COSINUS.
An EOQ model incorporating consumer behavior towards marketing policy change
Authors: Kim Seung-Lae , Kim Eunice Y. , Kim Se-Kwon
Published: September 2024

This paper introduces the Markovian EOQ model, an inventory management tool that considers how consumers respond to different marketing strategies. The model uses the Markov process to estimate the demand for two competing brands in a dynamic market. Its purpose is to create a more practical EOQ model that can be used in real-world scenarios where consumers may switch brands due to advertising, promotions, price adjustments, or dissatisfaction. By using the Markovian EOQ model, companies can make better inventory decisions and choose the most effective marketing strategies. One of the assumptions of the model is that the demand in the next period is a function of marketing expenditure in the current period. Our research found that the optimal lot size increases with marketing expenditure but at a slower rate than the traditional EOQ model due to brand loyalty. We provide a numerical example to demonstrate the effectiveness of the model.
Career Imprints from Diverse Institutional Settings: a Comparative Study of Academic and Non-academic Partnered Ventures in Technopolis
Authors: Aktaş Ülkü Neslihan , Akdeve Erdal
Published: September 2024

This research focused on the effects of prior experiences based on the imprinting theory that how individual-level imprints are transferred to the organizational level. The research attempted to answer the question of how owners’ career imprints affect the performance of ventures. Ventures operating in the technology sector were categorized according to their academic and industry background. The results showed that although academic-partnered ventures were found to generate more patents, their performance is lower than non-academic partnered ventures. This research has theoretical and practical contributions providing results that show different institutional contexts lead to different outcomes through the occupational imprinting effect.
Affordances of Media as Learning and Play: Children’s and Mothers’ Conceptions
Authors: Dore Rebecca A. , Preston Marcia S. , Golinkoff Roberta Michnick , Hirsh-Pasek Kathy
Published: September 2024

Educational and playful forms of media are both pervasive in children’s media landscape. Children tend to see play and learning as distinct, whereas parents tend to recognize the overlap between these categories; however, little research investigates children’s and parents’ conceptions of media as learning or play. Children (N = 80, five- and seven-year-olds) and mothers (N = 40) were shown black-and-white line drawings representing a child engaging in both media and non-media activities and asked to categorize each image as learning/not learning and as play/not play. Both mothers and children were less likely to see media as learning than non-media activities. However, children were less likely than mothers to differentiate between media and non-media activities in their conceptions of play. Both mothers and children were less likely to conceive of media activities than non-media activities as both learning and play, but this effect was stronger for mothers. These results suggest that mothers may see media more negatively and/or instrumentally, whereas children may see media as one of many options for playtime, indicating that parents should be encouraged to see media in a playful light, alongside other non-digital options for childhood play.
Understanding the Challenges for Modelling Islands’ Energy Systems and How to Solve Them
Authors: Handique Akash Jyoti , Peer Rebecca A. M. , Haas Jannik
Published: September 2024

Purpose of Review

As we transition to highly renewable energy systems, island energy systems face challenges different from those well-understood for continents. This paper reviews these challenges to guide energy systems modelling for islands.

Recent Findings

Only a single energy system model is found to be developed especially for islands. Challenges like land scarcity, climate risks, high seasonality of demand, isolation and remoteness, data scarcity, social and political vulnerability, and scarce funding are identified in recent literature. Notably, isolation and remoteness, social and political factors, and insufficient island funding are underrepresented in studies reviewed in this work.

This review identifies the specific challenges of island energy systems and compiles the methods employed by researchers to tackle them. We discuss these challenges in detail, highlight gaps, and provide suggestions to improve island energy systems modelling in the future.
Vaccine Hesitancy at Nine Community Sites Across the United States, Early in COVID-19 Vaccine Rollout
Authors: Ratnayake Aneeka , Hernandez Julie H. , Justman Jessica , Farley Jason E. , Hirsch-Moverman Yael , Ho Ken , Mayer Stockton , Oluyomi Abiodun , Sobieszczyk Magdalena E. , Swaminathan Shobha , Skalland Timothy , Tapsoba Jean de Dieu ,   the CoVPN 5002 Study Team, Kissinger Patricia J.
Published: September 2024

Background

Vaccine hesitancy has been a significant concern throughout the COVID-19 pandemic. Vaccine hesitancy can be attributed to lack of confidence in vaccines, complacency about the health threat, or lack of convenience of vaccination. To date, few studies have used methods designed to include populations underrepresented in research when identifying factors associated with vaccine hesitancy.

Methods

Between January and July 2021, potential participants were recruited from community venues selected through time-location sampling in 15 defined communities in the United States. Study staff administered a questionnaire on demographics, COVID-19 behaviors and attitudes, and vaccination status or intention to consenting individuals. Vaccine hesitancy was analyzed among those age 18 years and older from nine of the 15 sites and was defined as self-reported neutral, unlikely, or very unlikely vaccine intention. Logistic regression modeling, adjusted for site, identified factors associated with vaccine hesitancy.

Results

Among 11,559 individuals, vaccine hesitancy by site ranged from 8.7 to 31.1%. Vaccine hesitancy was associated with being Black compared to White, being White compared to Asian, younger age, unstable housing, being unemployed, lower income, having a disability, providing care in home, not reporting inability to visit sick or elderly relatives during the pandemic, not reporting increased anxiety during the pandemic, and not spending more time with loved ones during the pandemic.

Conclusions

In these selected US communities, early in vaccine rollout, there were significant racial disparities in vaccine hesitancy. Additionally, individuals who were more marginalized due to their socioeconomic status were more likely to report vaccine hesitancy. Vaccine campaigns should make efforts to remove barriers to vaccination, by improving convenience.
Strategie terapeutiche nella gestione del diabete mellito secondario a endocrinopatie
Authors: Emanuele Fabrizio , Bonsangue Maria , Salzillo Riccardo , Guarnotta Valentina , Arnaldi Giorgio
Published: September 2024

Sommario

L’acromegalia, la sindrome di Cushing e alcuni tumori neuroendocrini sono caratterizzati da un eccesso di ormoni controregolatori in circolo. Ciò può favorire l’insorgenza di alterazioni del metabolismo del glucosio di varia entità, fino al diabete mellito conclamato. Sebbene il trattamento del diabete secondario in queste endocrinopatie sia conforme alle più recenti evidenze scientifiche e linee guida sulla gestione terapeutica del diabete mellito, ci sono alcuni accorgimenti di cui tenere conto. Lo scopo di questa Rassegna è quello di fornire strumenti di riflessione e conoscenza per migliorare l’approccio terapeutico e diagnostico a questi pazienti che presentano differenze intrinseche alla fisiopatologia di ciascuna condizione affrontata. Un altro aspetto da non sottovalutare riguarda l’insorgenza di diabete mellito (ovvero il peggioramento del compenso glicometabolico nei pazienti diabetici) correlato ad alcuni farmaci utilizzati per trattare la malattia primaria, come il pasireotide. La necessità di trattare il diabete mellito secondario in queste patologie endocrine è finalizzata non solo a ripristinare l’euglicemia ma anche a prevenire e rallentare le complicanze cardio-renali che si associano sia al diabete che alla malattia primaria. A questo proposito si suggerisce, quindi, un algoritmo di trattamento applicabile alle diverse patologie descritte. Il campo delle complicanze metaboliche legate alle endocrinopatie e dei farmaci utilizzati nel trattamento di queste patologie richiede studi più approfonditi e rappresenta un’area di crescente importanza nel campo dell’endocrinologia.
Influence of the air–fuel-ratio and fuel on the reactivity of diesel soot
Authors: Böhmeke Christian , Wagner Uwe , Koch Thomas
Published: September 2024

This work deals with the influence of the variation of the air–fuel-ratio on the emissions as well as on the soot reactivity of a commercial vehicle diesel engine. The emissions and the associated soot reactivity are compared between conventional fossil diesel fuel and the regeneratively produced paraffinic diesel fuel HVO (hydrotreated vegetable oils). All investigations were carried out on a single-cylinder engine and the gaseous and particulate emissions were recorded. Additionally, the collected engine out soot samples were analyzed by thermogravimetric balance (thermogravimetric analysis = TGA) to determine the reactivity of the soot. Regardless of the set engine operating point, it was shown that the particulate mass is significantly reduced when operating with HVO compared to fossil diesel fuel. Other gaseous emissions are also minimally lower compared to fossil diesel. In contrast, however, the HVO fuel has an increased number of particles due to smaller particles. The variation of the engine operating parameters showed the same tendencies with regard to soot reactivity, regardless of the fuel used. However, the parameter variations were more or less pronounced depending on the respective fuel. It is particularly noticeable that the reactivity of soot, which is produced when using HVO, is reduced at every operating point despite the lower particulate mass compared to fossil diesel fuel.