bluuebunny/crossref_metadata_2025_split huggingface dataset:
Switching Controller Synthesis for Hybrid Systems Against STL Formulas
Authors: Su Han , Feng Shenghua , Zhan Sinong , Zhan Naijun 
Published: September 2024

AbstractSwitching controllers play a pivotal role in directing hybrid systems (HSs) towards the desired objective, embodying a “correct-by-construction” approach to HS design. Identifying these objectives is thus crucial for the synthesis of effective switching controllers. While most of existing works focus on safety and liveness, few of them consider timing constraints. In this paper, we delves into the synthesis of switching controllers for HSs that meet system objectives given by a fragment of STL, which essentially corresponds to a reach-avoid problem with timing constraints. Our approach involves iteratively computing the state sets that can be driven to satisfy the reach-avoid specification with timing constraints. This technique supports to create switching controllers for both constant and non-constant HSs. We validate our method’s soundness, and confirm its relative completeness for a certain subclass of HSs. Experiment results affirms the efficacy of our approach.
On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains
Authors: Wu Hao , Feng Shenghua , Gan Ting , Wang Jie , Xia Bican , Zhan Naijun 
Published: September 2024

AbstractBarrier certificates, serving as differential invariants that witness system safety, play a crucial role in the verification of cyber-physical systems (CPS). Prevailing computational methods for synthesizing barrier certificates are based on semidefinite programming (SDP) by exploiting Putinar Positivstellensatz. Consequently, these approaches are limited by the Archimedean condition, which requires all variables to be bounded, i.e., systems are defined over bounded domains. For systems over unbounded domains, unfortunately, existing methods become incomplete and may fail to identify potential barrier certificates.In this paper, we address this limitation for the unbounded cases. We first give a complete characterization of polynomial barrier certificates by using homogenization, a recent technique in the optimization community to reduce an unbounded optimization problem to a bounded one. Furthermore, motivated by this formulation, we introduce the definition of homogenized systems and propose a complete characterization of a family of non-polynomial barrier certificates with more expressive power. Experimental results demonstrate that our two approaches are more effective while maintaining a comparable level of efficiency.
Tolerance of Reinforcement Learning Controllers Against Deviations in Cyber Physical Systems
Authors: Zhang Changjian , Kapoor Parv , Meira-Góes Rômulo , Garlan David , Kang Eunsuk , Ganlath Akila , Mishra Shatadal , Ammar Nejib 
Published: September 2024

AbstractCyber-physical systems (CPS) with reinforcement learning (RL)-based controllers are increasingly being deployed in complex physical environments such as autonomous vehicles, the Internet-of-Things (IoT), and smart cities. An important property of a CPS is tolerance; i.e., its ability to function safely under possible disturbances and uncertainties in the actual operation. In this paper, we introduce a new, expressive notion of tolerance that describes how well a controller is capable of satisfying a desired system requirement, specified using Signal Temporal Logic (STL), under possible deviations in the system. Based on this definition, we propose a novel analysis problem, called the tolerance falsification problem, which involves finding small deviations that result in a violation of the given requirement. We present a novel, two-layer simulation-based analysis framework and a novel search heuristic for finding small tolerance violations. To evaluate our approach, we construct a set of benchmark problems where system parameters can be configured to represent different types of uncertainties and disturbances in the system. Our evaluation shows that our falsification approach and heuristic can effectively find small tolerance violations.
UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model Checking
Authors: Wang Minghua , Xue Jingling , Huang Lin , Zi Yuan , Wei Tao 
Published: September 2024

AbstractRust has gained popularity as a safer alternative to C/C++ for low-level programming due to its memory-safety features and minimal runtime overhead. However, the use of the “unsafe” keyword allows developers to bypass safety guarantees, posing memory-safety risks. Bounded Model Checking (BMC) is commonly used to detect memory-safety problems, but it has limitations for large-scale programs, as it can only detect bugs within a bounded number of executions.In this paper, we introduce UnsafeCop that utilizes and enhances BMC for analyzing memory safety in real-world unsafe Rust code. Our methodology incorporates harness design, loop bound inference, and both loop and function stubbing for comprehensive analysis. We optimize verification efficiency through a strategic function verification order, leveraging both types of stubbing. We conducted a case study on TECC (Trusted-Environment-based Cryptographic Computing), a proprietary framework consisting of 30,174 lines of Rust code, including 3,019 lines of unsafe Rust code, developed by Ant Group. Experimental results demonstrate that UnsafeCop effectively detects and verifies dozens of memory safety issues, reducing verification time by 73.71% compared to the traditional non-stubbing approach, highlighting its practical effectiveness.
Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0
Authors: Titolo Laura , Moscato Mariano , Feliu Marco A. , Masci Paolo , Muñoz César A. 
Published: September 2024

AbstractSmall round-off errors in safety-critical systems can lead to catastrophic consequences. In this context, determining if the result computed by a floating-point program is accurate enough with respect to its ideal real-number counterpart is essential. This paper presents PRECiSA 4.0, a tool that rigorously estimates the accumulated round-off error of a floating-point program. PRECiSA 4.0 combines static analysis, optimization techniques, and theorem proving to provide a modular approach for computing a provably correct round-off error estimation. PRECiSA 4.0 adds several features to previous versions of the tool that enhance its applicability and performance. These features include support for data collections such as lists, records, and tuples; support for recursion schemas; an updated floating-point formalization that closely characterizes the IEEE-754 standard; an efficient and modular analysis of function calls that improves the performances for large programs; and a new user interface integrated into Visual Studio Code.
Advancing Quantum Computing with Formal Methods
Authors: Quist Arend-Jan , Mei Jingyi , Coopmans Tim , Laarman Alfons 
Published: September 2024

AbstractThis tutorial introduces quantum computing with a focus on the applicability of formal methods in this relatively new domain. We describe quantum circuits and convey an understanding of their inherent combinatorial nature and the exponential blow-up that makes them hard to analyze. Then, we show how weighted model counting (#SAT) can be used to solve hard analysis tasks for quantum circuits.This tutorial is aimed at everyone in the formal methods community with an interest in quantum computing. Familiarity with quantum computing is not required, but basic linear algebra knowledge (particularly matrix multiplication and basis vectors) is a prerequisite. The goal of the tutorial is to inspire the community to advance the development of quantum computing with formal methods.
ASMETA Tool Set for Rigorous System Design
Authors: Bombarda Andrea , Bonfanti Silvia , Gargantini Angelo , Riccobene Elvinia , Scandurra Patrizia 
Published: September 2024

AbstractThis 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

AbstractIn 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

AbstractSoftware 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

AbstractThe 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

AbstractStream-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

AbstractWe 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

AbstractWe 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

AbstractPlatforms 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

ZusammenfassungDer 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

AbstractThe 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

Abstract
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

ZusammenfassungDurch 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.