bluuebunny/crossref_metadata_2025_split huggingface dataset:
LTL Reactive Synthesis with a Few Hints
Authors: Balachander Mrudula , Filiot Emmanuel , Raskin Jean-François 
Published: April 2023

AbstractWe study a variant of the problem of synthesizing Mealy machines that enforce LTL specifications against all possible behaviours of the environment, including hostile ones. In the variant studied here, the user provides the high level LTL specification$$\varphi $$of the system to design, and a setEof examples of executions that the solution must produce. Our synthesis algorithm first generalizes the user-provided examples inEusing tailored extensions of automata learning algorithms, while preserving realizability of$$\varphi $$. Second, it turns the (usually) incomplete Mealy machine obtained by the learning phase into a complete Mealy machine realizing$$\varphi $$. The examples are used to guide the synthesis procedure. We prove learnability guarantees of our algorithm and prove that our problem, while generalizing the classical LTL synthesis problem, matches its worst-case complexity. The additional cost of learning fromEis even polynomial in the size ofEand in the size of a symbolic representation of solutions that realize$$\varphi $$, computed by the synthesis toolAcacia-Bonzai. We illustrate the practical interest of our approach on a set of examples.
Timed Automata Verification and Synthesis via Finite Automata Learning
Authors: Sankur Ocan 
Published: April 2023

AbstractWe present algorithms for model checking and controller synthesis of timed automata, seeing a timed automaton model as a parallel composition of a large finite-state machine and a relatively smaller timed automaton, and using compositional reasoning on this composition. We use automata learning algorithms to learn finite automata approximations of the timed automaton component, in order to reduce the problem at hand to finite-state model checking or to finite-state controller synthesis. We present an experimental evaluation of our approach.
Explainable Online Monitoring of Metric Temporal Logic
Authors: Lima Leonardo , Herasimau Andrei , Raszyk Martin , Traytel Dmitriy , Yuan Simon 
Published: April 2023

AbstractRuntime monitors analyze system execution traces for policy compliance. Monitors for propositional specification languages, such as metric temporal logic (MTL), produce Boolean verdicts denoting whether the policy is satisfied or violated at a given point in the trace. Given a sufficiently complex policy, it can be difficult for the monitor’s user to understand how the monitor arrived at its verdict. We develop an MTL monitor that outputs verdicts capturing why the policy was satisfied or violated. Our verdicts are proof trees in a sound and complete proof system that we design. We demonstrate that such verdicts can serve as explanations for end users by augmenting our monitor with a graphical interface for the interactive exploration of proof trees. As a second application, our verdicts serve as certificates in a formally verified checker we develop using the Isabelle proof assistant.
Multiparty Session Typing in Java, Deductively
Authors: Bouma Jelle , de Gouw Stijn , Jongmans Sung-Shik 
Published: April 2023

AbstractMultiparty session typing (MPST) is a method to automatically prove safety and liveness of protocol implementations relative to specifications. We present BGJ: a new tool to apply the MPST method in combination with Java. The checks performed using our tool are purely static (all errors are reported early at compile-time) and resource-efficient (near-zero cost abstractions at run-time), thereby addressing two issues of existing tools. BGJ is built using VerCors, but our approach is general.
Goblint: Autotuning Thread-Modular Abstract Interpretation
Authors: Saan Simmo , Schwarz Michael , Erhard Julian , Pietsch Manuel , Seidl Helmut , Tilscher Sarah , Vojdani Vesal 
Published: April 2023

AbstractThe static analyzer Goblint is dedicated to the analysis of multi-threaded C programs by abstract interpretation. It provides multiple techniques for increasing analysis precision, e.g., configurable context-sensitivity and a wide range of numerical analyses. As a rule of thumb, more precise analyses decrease scalability, while not always necessary for solving the task at hand. Therefore, Goblint has been enhanced with autotuning which, based on syntactical criteria, adapts analysis configuration to the given program such that relevant precision is obtained with acceptable effort.
Java Ranger: Supporting String and Array Operations in Java Ranger (Competition Contribution)
Authors: Hussein Soha , Yan Qiuchen , McCamant Stephen , Sharma Vaibhav , Whalen Michael W. 
Published: April 2023

AbstractJava Ranger is a path-merging tool for Java Programs. It identifies branching regions of code and summarizes them by generating a disjunctive logical constraint that describes the behavior of the code region. Previously, Java Ranger showed that a reduction of 70% of execution paths is possible when used to merge branching regions of code that support numeric constraints.In this paper, we describe the support of two additional features since participation in SV-COMP 2020: symbolic array and symbolic string operations. Finally, we present a preliminary evaluation of the effect of the structure of the disjunctive constraint on the solver’s performance. Results suggest that certain constraint structures can speed up the performance of Java Ranger.
FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format
Authors: Xiao Shengping , Zhang Chengyu , Li Jianwen , Pu Geguang 
Published: April 2023

AbstractWe present , a fuzzer to generate random word-level model checking problems in Btor2 format. Btor2 is one of the mainstream input formats for word-level hardware model checking and was used in the most recent hardware model checking competition. Compared to bit-level one, word-level model checking is a more complex research field at an earlier stage of development. Therefore, it is necessary to develop a tool that can produce a large number of test cases in Btor2 format to test either existing or under-developed word-level model checkers. To evaluate the practicality of , we tested the state-of-the-art word-level model checkers and with the generated benchmarks. Experimental results show that both tools are buggy and not mature enough, which reflects the practical value of .
Verified reductions for optimization
Authors: Bentkamp Alexander , Mir Ramon Fernández , Avigad Jeremy 
Published: April 2023

AbstractNumerical and symbolic methods for optimization are used extensively in engineering, industry, and finance. Various methods are used to reduce problems of interest to ones that are amenable to solution by these methods. We develop a framework for designing and applying such reductions, using the Lean programming language and interactive proof assistant. Formal verification makes the process more reliable, and the availability of an interactive framework and ambient mathematical library provides a robust environment for constructing the reductions and reasoning about them.
ACoRe: Automated Goal-Conflict Resolution
Authors: Carvalho Luiz , Degiovanni Renzo , Brizzio Matías , Cordy Maxime , Aguirre Nazareno , Traon Yves Le , Papadakis Mike 
Published: April 2023

AbstractSystem goals are the statements that, in the context of software requirements specification, capture how the software should behave. Many times, the understanding of stakeholders on what the system should do, as captured in the goals, can lead to different problems, from clearly contradicting goals, to more subtle situations in which the satisfaction of some goals inhibits the satisfaction of others. These latter issues, calledgoal divergences, are the subject ofgoal conflict analysis, which consists of identifying, assessing, and resolving divergences, as part of a more general activity known as goal refinement.While there exist techniques that, when requirements are expressed formally, can automatically identify and assess goal conflicts, there is currently no automated approach to support engineers inresolvingidentified divergences. In this paper, we presentACoRe, the first approach that automatically proposes potential resolutions to goal conflicts, in requirements specifications formally captured using linear-time temporal logic.ACoResystematically explores syntactic modifications of the conflicting specifications, aiming at obtaining resolutions that disable previously identified conflicts, while preserving specification consistency.ACoReintegrates modern multi-objective search algorithms (in particular, NSGA-III, WBGA, and AMOSA) to produce resolutions that maintain coherence with the original conflicting specification, by searching for specifications that are eithersyntacticallyorsemanticallysimilar to the original specification.We assessACoReon 25 requirements specifications taken from the literature. We show thatACoRecan successfully produce various conflict resolutions for each of the analyzed case studies, including resolutions that resemble specification repairs manually provided as part of conflict analyses.
Vamos: Middleware for Best-Effort Third-Party Monitoring
Authors: Chalupa Marek , Muehlboeck Fabian , Lei Stefanie Muroya , Henzinger Thomas A. 
Published: April 2023

AbstractAs the complexity and criticality of software increase every year, so does the importance of run-time monitoring. Third-party monitoring, with limited knowledge of the monitored software, and best-effort monitoring, which keeps pace with the monitored software, are especially valuable, yet underexplored areas of run-time monitoring. Most existing monitoring frameworks do not support their combination because they either require access to the monitored code for instrumentation purposes or the processing of all observed events, or both.We present a middleware framework, Vamos, for the run-time monitoring of software which is explicitly designed to support third-party and best-effort scenarios. The design goals of Vamos are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the ability to monitor black-box code through a variety of different event channels, and the connectability to monitors written in different specification languages), and (iii) ease-of-use. To achieve its goals, Vamos combines aspects of event broker and event recognition systems with aspects of stream processing systems.We implemented a prototype toolchain for Vamos and conducted experiments including a case study of monitoring for data races. The results indicate that Vamos enables writing useful yet efficient monitors, is compatible with a variety of event sources and monitor specifications, and simplifies key aspects of setting up a monitoring system from scratch.
FuSeBMC_IA: Interval Analysis and Methods for Test Case Generation
Authors: Aldughaim Mohannad , Alshmrany Kaled M. , Gadelha Mikhail R. , de Freitas Rosiane , Cordeiro Lucas C. 
Published: April 2023

AbstractThe cooperative verification of Bounded Model Checking and Fuzzing has proved to be one of the most effective techniques when testing C programs. FuSeBMC is a test-generation tool that employs BMC and Fuzzing to produce test cases. In Test-Comp 2023, we present an interval approach to FuSeBMC_IA, improving the test generator to use interval methods and abstract interpretation (via Frama-C) to strengthen our instrumentation and fuzzing. Here, an abstract interpretation engine instruments the program as follows. It analyzes different program branches, combines the conditions of each branch, and produces a Constraint Satisfaction Problem (CSP), which is solved using Constraint Programming (CP) by interval manipulation techniques called Contractor Programming. This process has a set of invariants for each branch, which are introduced back into the program as constraints. Experimental results show improvements in reducing CPU time (37%) and memory (13%), while retaining a high score.
Compositional Automata Learning of Synchronous Systems
Authors: Neele Thomas , Sammartino Matteo 
Published: April 2023

AbstractAutomata learning is a technique to infer an automaton model of a black-box system via queries to the system. In recent years it has found widespread use both in industry and academia, as it enables formal verification when no model is available or it is too complex to create one manually. In this paper we consider the problem of learning the individual components of a black-box synchronous system, assuming we can only query the whole system. We introduce a compositional learning approach in which several learners cooperate, each aiming to learn one of the components. Our experiments show that, in many cases, our approach requires significantly fewer queries than a widely-used non-compositional algorithm such as $$\mathtt {L^*}$$

L
∗

.
Democratizing Quality-Based Machine Learning Development through Extended Feature Models
Authors: d’Aloisio Giordano , Di Marco Antinisca , Stilo Giovanni 
Published: April 2023

AbstractML systems have become an essential tool for experts of many domains, data scientists and researchers, allowing them to find answers to many complex business questions starting from raw datasets. Nevertheless, the development of ML systems able to satisfy the stakeholders’ needs requires an appropriate amount of knowledge about the ML domain. Over the years, several solutions have been proposed to automate the development of ML systems. However, an approach taking into account the new quality concerns needed by ML systems (like fairness, interpretability, privacy, and others) is still missing.In this paper, we propose a new engineering approach for the quality-based development of ML systems by realizing a workflow formalized as a Software Product Line through Extended Feature Models to generate an ML System satisfying the required quality constraints. The proposed approach leverages an experimental environment that applies all the settings to enhance a given Quality Attribute, and selects the best one. The experimental environment is general and can be used for future quality methods’ evaluations. Finally, we demonstrate the usefulness of our approach in the context of multi-class classification problem and fairness quality attribute.
Vertical Schools as Community Hubs
Authors: Matthews Tony , Newton Clare , Guaralda Mirko , Mayere Severine 
Published: April 2023

AbstractVertical schools are an emerging form of school design in Australia. Hundreds of vertical schools, usually between four and seventeen stories, will be required in coming decades to respond to increasing student numbers in Australian cities. Locations will be in inner urban areas, where population densities are high and land availability is limited. School facilities for traditional academic programs, plus infrastructure for drama, music, exercise, sport, socialising, craft, play, and food preparation/dining, may all be useful to both students and groups from beyond the immediate school population, aiding the development of school-community connections. This chapter examines Australian vertical schools relative to more established European precedents. It traces community connections that can be discovered from visual analysis of plans and occupied buildings to investigate which spaces have potential for community use. How and why communities use different types of school spaces is explored. Consideration is given to the private, privileged, and public spaces of vertical schools. Questions are asked about whether schools operate as open or closed facilities and about how schools with more porous boundaries address children’s’ safety. The comparison of three Australian vertical schools with seven European examples provides helpful lessons to better understand opportunities for further improvement and innovation.
Theorising the Development, Implementation and Sustainability of Schools as Community Hubs
Authors: Rivera-Yevenes Carolina 
Published: April 2023

AbstractIncreasingly, school-based community hubs are aiming to engage and connect communities and service organisations in their daily operations. While some schools offer additional services to community members and share their facilities, there is limited research in the Australian context into how schools succeed in making their infrastructure and extended services accessible to both school and community members. This chapter proposes a research framework to investigate how schools as community hubs (SaCH) have been developed, implemented, and sustained, for the purpose of seeking insights into the processes, challenges, and lessons that have been learned by those involved. The chapter presents findings from the PhD study being undertaken by the author to illustrate how the framework guides attention to the socio-material relations at play within schools operating as community hubs, helping to make connections between the built environment and inhabitants’ practices, activities, and behaviours. The framework supports qualitative inquiry into the lived experiences of those associated with conceiving, delivering, operating, and using schools as community hubs, privileging the voices of policymakers, planners, designers, operators, and users.
A Framework for Building Schools as Community Hubs: If It Were Simpler Would It Happen Everywhere?
Authors: Cleveland Benjamin 
Published: April 2023

AbstractDeveloping, implementing, and sustaining schools as community hubs is not necessarily easy. Nevertheless, the potential gains for students, parents, carers, and members of the wider community may be significant, as has been documented internationally. Drawing on information from a range of research activities, this chapter outlines the process undertaken by a multi-disciplinary research team to create a framework for planning, designing, governing, and managing schools as community hubs. The ‘How to Hub Australia’ framework offers evidence-based advice on school infrastructure provision and management linked to the activities, programs and services that may be offered from school sites in addition to schooling. Commonly, these include early years and adult education, organised sports, recreation, library and information services, visual and performing arts activities, and health and wellbeing services. The framework is intended to help policymakers, school leaders, and designers overcome the uncertainties and perceived obstacles that tend to limit the provision and use of school facilities for broader community benefit. If it were simpler, would it happen everywhere? This chapter argues that community-facing schools could become commonplace, rather than exceptional, through the establishment of effective and enduring partnerships and updates to governance and funding models.
Connecting Schools with Local Communities Through Walkable Urban Design
Authors: Ergler Christina , Smith Melody 
Published: April 2023

AbstractEducational facilities generate traffic to and from school by car, on foot and on wheels. Which mode of travel dominates in a school community depends on several different factors including but not limited to the neighbourhood design, traffic safety, employment structures, community norms, and school policies. This chapter traces the socio-technical entanglements of traveling to school. We focus on the barriers to, and benefits of, active travel (i.e., walking or wheeling for transport) and showcase what children value on their route to school. Additionally, we highlight how built environments and social practices need to be transformed for creating sustainable, healthy and inclusive urban environments. We argue that to foster inclusive communities and to create a sense of belonging outside the school gates, a multi sector approach is needed to challenge and transform current travel norms and practices together with the physical environment of neighbourhood travel.
IKK1 aggravates ischemia–reperfusion kidney injury by promoting the differentiation of effector T cells
Authors: Song Ning , Xu Yang , Paust Hans-Joachim , Panzer Ulf , de las Noriega Maria Mercedes , Guo Linlin , Renné Thomas , Huang Jiabin , Meng Xianglin , Zhao Mingyan , Thaiss Friedrich 
Published: April 2023

AbstractIschemia–reperfusion injury (IRI) is one of the major causes of acute kidney injury (AKI), and experimental work has revealed detailed insight into the inflammatory response in the kidney. T cells and NFκB pathway play an important role in IRI. Therefore, we examined the regulatory role and mechanisms of IkappaB kinase 1 (IKK1) in CD4+T lymphocytes in an experimental model of IRI. IRI was induced in CD4cre and CD4IKK1Δ mice. Compared to control mice, conditional deficiency of IKK1 in CD4+T lymphocyte significantly decreased serum creatinine, blood urea nitrogen (BUN) level, and renal tubular injury score. Mechanistically, lack in IKK1 in CD4+T lymphocytes reduced the ability of CD4 lymphocytes to differentiate into Th1/Th17 cells. Similar to IKK1 gene ablation, pharmacological inhibition of IKK also protected mice from IRI. Together, lymphocyte IKK1 plays a pivotal role in IRI by promoting T cells differentiation into Th1/Th17 and targeting lymphocyte IKK1 may be a novel therapeutic strategy for IRI.
Entwicklung und Evaluation komplexer Interventionen in der Pflege
Authors: Abraham Jens , Möhler Ralph 
Published: April 2023

ZusammenfassungViele Interventionen in der Pflege sind komplex. Sie bestehen beispielsweise aus verschiedenen Interventionsteilen (Komponenten) und zielen auf Veränderungen von Prozessen oder dem Verhalten von Individuen oder Gruppen ab. Ein Rahmenmodell des britischen Medical Research Council beinhaltet methodische Empfehlungen für die Entwicklung und Evaluation von komplexen Interventionen. Diese narrative Übersichtsarbeit beschreibt die Umsetzung der methodischen Empfehlungen des Rahmenmodells am Beispiel von Interventionen zur Reduktion freiheitsentziehender Maßnahmen, z. B. Bettgitter oder Gurte an Stuhl und Bett, in der Krankenhaus- und der Langzeitpflege. Neben den Merkmalen der komplexen Interventionen werden die Entwicklung und theoretische Fundierung der Interventionen, die Prüfung der Machbarkeit und Wirksamkeit beschrieben.