bluuebunny/crossref_metadata_2025 huggingface dataset:
Fair Refinement for Asynchronous Session Types
Authors: Bravetti Mario , Lange Julien , Zavattaro Gianluigi
Published: March 2021

Session types are widely used as abstractions of asynchronous message passing systems. Refinement for such abstractions is crucial as it allows improvements of a given component without compromising its compatibility with the rest of the system. In the context of session types, the most general notion of refinement is the asynchronous session subtyping, which allows to anticipate message emissions but only under certain conditions. In particular, asynchronous session subtyping rules out candidates subtypes that occur naturally in communication protocols where, e.g., two parties simultaneously send each other a finite but unspecified amount of messages before removing them from their respective buffers. To address this shortcoming, we study fair compliance over asynchronous session types and fair refinement as the relation that preserves it. This allows us to propose a novel variant of session subtyping that leverages the notion of controllability from service contract theory and that is a sound characterisation of fair refinement. In addition, we show that both fair refinement and our novel subtyping are undecidable. We also present a sound algorithm, and its implementation, which deals with examples that feature potentially unbounded buffering.
Running Time Analysis of Broadcast Consensus Protocols
Authors: Czerner Philipp , Jaax Stefan
Published: March 2021

Broadcast consensus protocols (BCPs) are a model of computation, in which anonymous, identical, finite-state agents compute by sending/receiving global broadcasts. BCPs are known to compute all number predicates in $$\mathsf {NL}=\mathsf {NSPACE}(\log n)$$

NL
=
NSPACE
(
log
n
)

where n is the number of agents. They can be considered an extension of the well-established model of population protocols. This paper investigates execution time characteristics of BCPs. We show that every predicate computable by population protocols is computable by a BCP with expected $$\mathcal {O}(n \log n)$$

O
(
n
log
n
)

interactions, which is asymptotically optimal. We further show that every log-space, randomized Turing machine can be simulated by a BCP with $$\mathcal {O}(n \log n \cdot T)$$

O
(
n
log
n
·
T
)

interactions in expectation, where T is the expected runtime of the Turing machine. This allows us to characterise polynomial-time BCPs as computing exactly the number predicates in $$\mathsf {ZPL}$$
ZPL
, i.e. predicates decidable by log-space, randomised Turing machine with zero-error in expected polynomial time where the input is encoded as unary.
Directed Reachability for Infinite-State Systems
Authors: Blondin Michael , Haase Christoph , Offtermatt Philip
Published: March 2021

Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachability problem has recently been shown to require non-elementary time, which raises questions about the practical applicability of Petri nets as target models. In this paper, we introduce a novel approach for efficiently semi-deciding the reachability problem for Petri nets in practice. Our key insight is that computationally lightweight over-approximations of Petri nets can be used as distance oracles in classical graph exploration algorithms such as $$\mathsf {A}^{*}$$

A

∗

and greedy best-first search. We provide and evaluate a prototype implementation of our approach that outperforms existing state-of-the-art tools, sometimes by orders of magnitude, and which is also competitive with domain-specific tools on benchmarks coming from program synthesis and concurrent program analysis.
cake_lpr: Verified Propagation Redundancy Checking in CakeML
Authors: Tan Yong Kiam , Heule Marijn J. H. , Myreen Magnus O.
Published: March 2021

Modern SAT solvers can emit independently checkable proof certificates to validate their results. The state-of-the-art proof system that allows for compact proof certificates ispropagation redundancy(PR). However, the only existing method to validate proofs in this system with a formally verified tool requires a transformation to a weaker proof system, which can result in a significant blowup in the size of the proof and increased proof validation time. This paper describes the first approach to formally verify PR proofs on a succinct representation; we present (i) a newLinear PR(LPR) proof format, (ii) a tool to efficiently convert PR proofs into LPR format, and (iii) , a verified LPR proof checker developed in CakeML. The LPR format is backwards compatible with the existing LRAT format, but extends the latter with support for the addition of PR clauses. Moreover, is verified using CakeML ’s binary code extraction toolchain, which yields correctness guarantees for its machine code (binary) implementation. This further distinguishes our clausal proof checker from existing ones because unverified extraction and compilation tools are removed from its trusted computing base. We experimentally show that LPR provides efficiency gains over existing proof formats and that the strong correctness guarantees are obtained without significant sacrifice in the performance of the verified executable.
SyReNN: A Tool for Analyzing Deep Neural Networks
Authors: Sotoudeh Matthew , Thakur Aditya V.
Published: March 2021

Deep Neural Networks (DNNs) are rapidly gaining popularity in a variety of important domains. Formally, DNNs are complicated vector-valued functions which come in a variety of sizes and applications. Unfortunately, modern DNNs have been shown to be vulnerable to a variety of attacks and buggy behavior. This has motivated recent work in formally analyzing the properties of such DNNs. This paper introduces SyReNN, a tool for understanding and analyzing a DNN by computing its symbolic representation. The key insight is to decompose the DNN into linear functions. Our tool is designed for analyses using low-dimensional subsets of the input space, a unique design point in the space of DNN analysis tools. We describe the tool and the underlying theory, then evaluate its use and performance on three case studies: computing Integrated Gradients, visualizing a DNN’s decision boundaries, and patching a DNN.
MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers
Authors: Scott Joseph , Niemetz Aina , Preiner Mathias , Nejati Saeed , Ganesh Vijay
Published: March 2021

In this paper, we present MachSMT, an algorithm selection tool for Satisfiability Modulo Theories (SMT) solvers. MachSMT supports the entirety of the SMT-LIB language. It employs machine learning (ML) methods to construct both empirical hardness models (EHMs) and pairwise ranking comparators (PWCs) over state-of-the-art SMT solvers. Given an SMT formula $$\mathcal {I}$$
I
as input, MachSMT leverages these learnt models to output a ranking of solvers based on predicted run time on the formula $$\mathcal {I}$$
I
. We evaluate MachSMT on the solvers, benchmarks, and data obtained from SMT-COMP 2019 and 2020. We observe MachSMT frequently improves on competition winners, winning $$54$$

54

divisions outright and up to a $$198.4$$

198.4

% improvement in PAR-2 score, notably in logics that have broad applications (e.g., BV, LIA, NRA, etc.) in verification, program analysis, and software engineering. The MachSMT tool is designed to be easily tuned and extended to any suitable solver application by users. MachSMT is not a replacement for SMT solvers by any means. Instead, it is a tool that enables users to leverage the collective strength of the diverse set of algorithms implemented as part of these sophisticated solvers.
HLola: a Very Functional Tool for Extensible Stream Runtime Verification
Authors: Gorostiaga Felipe , Sánchez César
Published: March 2021

We present , an extensible Stream Runtime Verification (SRV) tool, that borrows from the functional language Haskell (1) rich types for data in events and verdicts; and (2) functional features for parametrization, libraries, high-order specification transformations, etc.

SRV is a formal dynamic analysis technique that generalizes Runtime Verification (RV) algorithms from temporal logics like LTL to stream monitoring, allowing the computation of verdicts richer than Booleans (quantitative values and beyond). The keystone of SRV is the clean separation between temporal dependencies and data computations. However, in spite of this theoretical separation previous engines include hardwired implementations of just a few datatypes, requiring complex changes in the tool chain to incorporate new data types. Additionally, when previous tools implement features like parametrization these are implemented in an ad-hoc way. In contrast, is implemented as a Haskell embedded DSL, borrowing datatypes and functional aspects from Haskell, resulting in an extensible engine (The tool is available open-source athttp://github.com/imdea-software/hlola). We illustrate through several examples, including a UAV monitoring infrastructure with predictive characteristics that has been validated in online runtime verification in real mission planning.
Bridging Arrays and ADTs in Recursive Proofs
Authors: Fedyukovich Grigory , Ernst Gidon
Published: March 2021

We present an approach to synthesize relational invariants to prove equivalences between object-oriented programs. The approach bridges the gap between recursive data types and arrays that serve to represent internal states. Our relational invariants are recursively-defined, and thus are valid for data structures of unbounded size. Based on introducing recursion into the proofs by observing and lifting the constraints from joint methods of the two objects, our approach is fully automatic and can be seen as an algorithm for solving Constrained Horn Clauses (CHC) of a specific sort. It has been implemented on top of the SMT-based CHC solver AdtChc and evaluated on a range of benchmarks.
Momba: JANI Meets Python
Authors: Köhl Maximilian A. , Klauck Michaela , Hermanns Holger
Published: March 2021

JANI-model [6] is a model interchange format for networks of interacting automata. It is well-entrenched in the quantitative model checking community and allows modeling a variety of systems involving concurrency, probabilistic and real-time aspects, as well as continuous dynamics. Python is a general purpose programming language preferred by many for its ease of use and vast ecosystem. In this paper, we presentMomba, a flexible Python framework for dealing with formal models centered around the JANI-model format and formalism. Momba strives to deliver an integrated and intuitive experience for experimenting with formal models making them accessible to a broader audience. To this end, it provides a pythonic interface for model construction, validation, and analysis. Here, we demonstrate these capabilities.
Software Verification: 10th Comparative Evaluation (SV-COMP 2021)
Authors: Beyer Dirk
Published: March 2021

SV-COMP 2021 is the 10th edition of the Competition on Software Verification (SV-COMP), which is an annual comparative evaluation of fully automatic software verifiers for C and Java programs. The competition provides a snapshot of the current state of the art in the area, and has a strong focus on reproducibility of its results. The competition was based on 15 201 verification tasks for C programs and 473 verification tasks for Java programs. Each verification task consisted of a program and a property (reachability, memory safety, overflows, termination). SV-COMP 2021 had 30 participating verification systems from 27 teams from 11 countries.
A Two-Phase Approach for Conditional Floating-Point Verification
Authors: Lohar Debasmita , Jeangoudoux Clothilde , Sobel Joshua , Darulova Eva , Christakis Maria
Published: March 2021

Tools that automatically prove the absence or detect the presence of large floating-point roundoff errors or the special values NaN and Infinity greatly help developers to reason about the unintuitive nature of floating-point arithmetic. We show that state-of-the-art tools, however, support or provide non-trivial results only for relatively short programs. We propose a framework for combining different static and dynamic analyses that allows to increase their reach beyond what they can do individually. Furthermore, we show how adaptations of existing dynamic and static techniques effectively trade some soundness guarantees for increased scalability, providing conditional verification of floating-point kernels in realistic programs.
JDart: Portfolio Solving, Breadth-First Search and SMT-Lib Strings (Competition Contribution)
Authors: Mues Malte , Howar Falk
Published: March 2021

JDartperforms dynamic symbolic execution ofJavaprograms: it executes programs with concrete inputs while recording symbolic constraints on executed program paths. A portfolio of constraint solvers is then used for generating new concrete values from recorded constraints that drive execution along previously unexplored paths. For SV-COMP 2021, we improvedJDartby implementing exploration strategies, bounded analysis, and path-specific constraint solving strategies, as well as by enabling the use of SMT-Lib string theory for encoding of string operations.
Symbiotic 8: Beyond Symbolic Execution
Authors: Chalupa Marek , Jašek Tomáš , Novák Jakub , Řechtáčková Anna , Šoková Veronika , Strejček Jan
Published: March 2021

Symbiotic 8 extends the traditional combination of static analyses, instrumentation, program slicing, and symbolic execution with one substantial novelty, namely a technique mixing symbolic execution with k-induction. This technique can prove the correctness of programs with possibly unbounded loops, which cannot be done by classic symbolic execution.Symbiotic 8 delivers also several other improvements. In particular, we have modified our fork of the symbolic executorKleeto support the comparison of symbolic pointers. Further, we have tuned the shape analysis toolPredator(integrated already inSymbiotic 7) to perform better onllvmbitcode. We have also developed a light-weight analysis of relations between variables that can prove the absence of out-of-bound accesses to arrays.
Local Search with a SAT Oracle for Combinatorial Optimization
Authors: Cohen Aviad , Nadel Alexander , Ryvchin Vadim
Published: March 2021

NP-hard combinatorial optimization problems are pivotal in science and business. There exists a variety of approaches for solving such problems, but for problems with complex constraints and objective functions, local search algorithms scale the best. Such algorithms usually assume that finding a non-optimal solution with no other requirements is easy. However, what if it is NP-hard? In such case, a SAT solver can be used for finding the initial solution, but how can one continue solving the optimization problem? We offer a generic methodology, called Local Search with SAT Oracle (), to solve such problems. facilitates implementation of advanced local search methods, such as variable neighbourhood search, hill climbing and iterated local search, while using a SAT solver as an oracle. We have successfully applied our approach to solve a critical industrial problem of cell placement and productized our solution at Intel.
Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities
Authors: Lepiller Julien , Piskac Ruzica , Schäf Martin , Santolucito Mark
Published: March 2021

Infrastructure as Code is a new approach to computing infrastructure management that allows users to leverage tools such as version control, automatic deployments, and program analysis for infrastructure configurations. This approach allows for faster and more homogeneous configuration of a complete infrastructure. Infrastructure as Code languages, such as CloudFormation or TerraForm, use a declarative model so that users only need to describe the desired state of the infrastructure. However, in practice, these languages are not processed atomically. During an upgrade, the infrastructure goes through a series of intermediate states. We identify a security vulnerability that occurs during an upgrade even when the initial and final states of the infrastructure are secure, and we show that those vulnerability are possible in Amazon’s AWS and Google Cloud. We call such attacks intra-update sniping vulnerabilities. In order to mitigate this shortcoming, we present a technique that detects such vulnerabilities and pinpoints the root causes of insecure deployment migrations. We implement this technique in a tool, Häyhä, that uses dataflow graph analysis. We evaluate our tool on a set of open-source CloudFormation templates and find that it is scalable and could be used as part of a deployment workflow.
Syntax-Guided Quantifier Instantiation
Authors: Niemetz Aina , Preiner Mathias , Reynolds Andrew , Barrett Clark , Tinelli Cesare
Published: March 2021

This paper presents a novel approach for quantifier instantiation in Satisfiability Modulo Theories (SMT) that leverages syntax-guided synthesis (SyGuS) to choose instantiation terms. It targets quantified constraints over background theories such as (non)linear integer, reals and floating-point arithmetic, bit-vectors, and their combinations. Unlike previous approaches for quantifier instantiation in these domains which rely on theory-specific strategies, the new approach can be applied to any (combined) theory, when provided with a grammar for instantiation terms for all sorts in the theory. We implement syntax-guided instantiation in the SMT solver CVC4, leveraging its support for enumerative SyGuS. Our experiments demonstrate the versatility of the approach, showing that it is competitive with or exceeds the performance of state-of-the-art solvers on a range of background theories.
For a Few Dollars More
Authors: Haslbeck Maximilian P. L. , Lammich Peter
Published: March 2021

We present a framework to verify both, functional correctness and worst-case complexity of practically efficient algorithms. We implemented a stepwise refinement approach, using the novel concept of resource currencies to naturally structure the resource analysis along the refinement chain, and allow a fine-grained analysis of operation counts. Our framework targets the LLVM intermediate representation. We extend its semantics from earlier work with a cost model. As case study, we verify the correctness and $$O(n\log n)$$

O
(
n
log
n
)

worst-case complexity of an implementation of the introsort algorithm, whose performance is on par with the state-of-the-art implementation found in the GNU C++ Library.
Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols
Authors: Keizer Alex C. , Basold Henning , Pérez Jorge A.
Published: March 2021

Compositional methods are central to the development and verification of software systems. They allow breaking down large systems into smaller components, while enabling reasoning about the behaviour of the composed system. For concurrent and communicating systems, compositional techniques based on behavioural type systems have received much attention. By abstracting communication protocols as types, these type systems can statically check that programs interact with channels according to a certain protocol, whether the intended messages are exchanged in a certain order. In this paper, we put on our coalgebraic spectacles to investigate session types, a widely studied class of behavioural type systems. We provide a syntax-free description of session-based concurrency as states of coalgebras. As a result, we rediscover type equivalence, duality, and subtyping relations in terms of canonical coinductive presentations. In turn, this coinductive presentation makes it possible to elegantly derive a decidable type system with subtyping for $$\pi $$
π
-calculus processes, in which the states of a coalgebra will serve as channel protocols. Going full circle, we exhibit a coalgebra structure on an existing session type system, and show that the relations and type system resulting from our coalgebraic perspective agree with the existing ones.
Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere
Authors: Mak Carol , Ong C.-H. Luke , Paquet Hugo , Wagner Dominik
Published: March 2021

We study the differential properties of higher-order statistical probabilistic programs with recursion and conditioning. Our starting point is an open problem posed by Hongseok Yang: what class of statistical probabilistic programs have densities that are differentiable almost everywhere? To formalise the problem, we consider Statistical PCF (SPCF), an extension of call-by-value PCF with real numbers, and constructs for sampling and conditioning. We give SPCF a sampling-style operational semantics à la Borgström et al., and study the associated weight (commonly referred to as the density) function and value function on the set of possible execution traces.

Our main result is that almost surely terminating SPCF programs, generated from a set of primitive functions (e.g. the set of analytic functions) satisfying mild closure properties, have weight and value functions that are almost everywhere differentiable. We use a stochastic form of symbolic execution to reason about almost everywhere differentiability. A by-product of this work is that almost surely terminatingdeterministic(S)PCF programs with real parameters denote functions that are almost everywhere differentiable.

Our result is of practical interest, as almost everywhere differentiability of the density function is required to hold for the correctness of major gradient-based inference algorithms.
Automated Termination Analysis of Polynomial Probabilistic Programs
Authors: Moosbrugger Marcel , Bartocci Ezio , Katoen Joost-Pieter , Kovács Laura
Published: March 2021

The termination behavior of probabilistic programs depends on the outcomes of random assignments. Almost sure termination (AST) is concerned with the question whether a program terminates with probability one on all possible inputs. Positive almost sure termination (PAST) focuses on termination in a finite expected number of steps. This paper presents a fully automated approach to the termination analysis of probabilistic while-programs whose guards and expressions are polynomial expressions. As proving (positive) AST is undecidable in general, existing proof rules typically provide sufficient conditions. These conditions mostly involve constraints on supermartingales. We consider four proof rules from the literature and extend these with generalizations of existing proof rules for (P)AST. We automate the resulting set of proof rules by effectively computing asymptotic bounds on polynomials over the program variables. These bounds are used to decide the sufficient conditions – including the constraints on supermartingales – of a proof rule. Our software tool Amber can thus check AST, PAST, as well as their negations for a large class of polynomial probabilistic programs, while carrying out the termination reasoning fully with polynomial witnesses. Experimental results show the merits of our generalized proof rules and demonstrate that Amber can handle probabilistic programs that are out of reach for other state-of-the-art tools.
Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains
Authors: Athaiya Snigdha , Komondoor Raghavan , Kumar K. Narayan
Published: March 2021

Asynchronous message-passing systems are employed frequently to implement distributed mechanisms, protocols, and processes. This paper addresses the problem of precise data flow analysis for such systems. To obtain good precision, data flow analysis needs to somehow skip execution paths that read more messages than the number of messages sent so far in the path, as such paths are infeasible at run time. Existing data flow analysis techniques do elide a subset of such infeasible paths, but have the restriction that they admit only finite abstract analysis domains. In this paper we propose a generalization of these approaches to admit infinite abstract analysis domains, as such domains are commonly used in practice to obtain high precision. We have implemented our approach, and have analyzed its performance on a set of 14 benchmarks. On these benchmarks our tool obtains significantly higher precision compared to a baseline approach that does not elide any infeasible paths and to another baseline that elides infeasible paths but admits only finite abstract domains.
Sound and Complete Concolic Testing for Higher-order Functions
Authors: You Shu-Hung , Findler Robert Bruce , Dimoulas Christos
Published: March 2021

Higher-order functions have become a staple of modern programming languages. However, such values stymie concolic testers, as the SMT solvers at their hearts are inherently first-order.

This paper lays a formal foundations for concolic testing higher-order functional programs. Three ideas enable our results: (i) our tester considers only program inputs in a canonical form; (ii) it collects novel constraints from the evaluation of the canonical inputs to search the space of inputs with partial help from an SMT solver and (iii) it collects constraints from canonical inputs even when they are arguments to concretized calls. We prove that (i) concolic evaluation is sound with respect to concrete evaluation; (ii) modulo concretization and SMT solver incompleteness, the search for a counter-example succeeds if a user program has a bug and (iii) this search amounts to directed evolution of inputs targeting hard-to-reach corners of the program.
Verified Software Units
Authors: Beringer Lennart
Published: March 2021

Modularity - the partitioning of software into units of functionality that interact with each other via interfaces - has been the mainstay of software development for half a century. In case of the C language, the main mechanism for modularity is the compilation unit / header file abstraction. This paper complements programmatic modularity for C with modularity idioms for specification and verification in the context of Verifiable C, an expressive separation logic for CompCert . Technical innovations include (i)abstract predicate declarations– existential packages that combine Parkinson & Bierman’s abstract predicates with their client-visible reasoning principles; (ii)residualpredicates, which help enforcing data abstraction in callback-rich code; and (iii) an application to pure (Smalltalk-style) objects that connects code verification to model-level reasoning about features such as subtyping,self, inheritance, and late binding. We introduce our techniques using concrete example modules that have all been verified using the Coq proof assistant and combine to fully linked verified programs using a novel, abstraction-respecting component composition rule for Verifiable C.
Correction to: Decision Science for Future Earth: A Conceptual Framework
Authors: Yahara Tetsukazu , Tanaka Wataru , Inoue Yukako , Lee Jounghun , Qian Kun , Javadi Firouzeh , Onda Nariaki , Yokota Fumihiko , Eguchi Kumi , Nishikitani Mariko , Kikuchi Kimiyo , Kawasaki Nobuyoshi , Jeong Yukyong , Ide Jun’ichiro , Ota Tetsuji , Fujiwara Takahiro , Hosoya Tadatsugu , Kano Yuichi , Sugimoto Megumi , Ahmed Ashir , Shimatani Yukihiro , Tokunaga Shota , Nagahama Ai , Hiramatsu Michikazu , Murakami Takahiro
Published: March 2021

Correction to Chapter 1 in: Yahara T. et al. (2021) Decision Science for Future Earth: A Conceptual Framework. In: Yahara T. (eds) Decision Science for Future Earth. Springer, Singapore. 10.1007/978-981-15-8632-3_1
Perturbative calculations of entanglement entropy
Authors: Dadras Pouria , Kitaev Alexei
Published: March 2021

Abstract

This paper is an attempt to extend the recent understanding of the Page curve for evaporating black holes to more general systems coupled to a heat bath. Although calculating the von Neumann entropy by the replica trick is usually a challenge, we have identified two solvable cases. For the initial section of the Page curve, we sum up the perturbation series in the system-bath coupling κ; the most interesting contribution is of order 2s, where s is the number of replicas. For the saturated regime, we consider the effect of an external impulse on the entropy at a later time and relate it to OTOCs. A significant simplification occurs in the maximal chaos case such that the effect may be interpreted in terms of an intermediate object, analogous to the branching surface of a replica wormhole.
Health-related quality of life in refugee minors from Syria, Iraq and Afghanistan resettled in Sweden: a nation-wide, cross-sectional study
Authors: Solberg Øivind , Sengoelge Mathilde , Johnson-Singh Charisse M. , Vaez Marjan , Eriksson Anna-Karin , Saboonchi Fredrik
Published: March 2021

Purpose

To examine health-related quality of life (HRQoL) in refugee minors resettled in Sweden and compare results to a European reference population, while exploring associations between sociodemographic factors and HRQoL dimensions.

Methods

A cross-sectional, nation-wide study was conducted with a stratified sample of refugee minors ages 12–15 and 16–18 from Afghanistan, Iraq and Syria, resettled in Sweden between 2014 and 2018. HRQoL was measured using KIDSCREEN-27. HRQoL dimension scores of the sample were compared to mean scores of European age and gender-matched reference population. Associations between sociodemographic factors and HRQoL dimensions were investigated with independent t tests and ANOVA. A multivariable regression analysis was performed to identify the sociodemographic factors associated with HRQoL.

Results

The questionnaire was sent to 10,000 potential respondents. The response rate was 26%, yielding n = 2559 refugee minors (boys 55%, girls 45%) in the study sample. Compared to European references, minors in the present study had significantly lower scores of HRQoL within psychological wellbeing and peers and social support, whereas levels for autonomy and parent/guardian relations and school environment were higher. Several sociodemographic factors were significantly associated with all HRQoL dimensions, with those 16–18 years old, having average or poor family economy, and living with an unrelated adult or family reporting lower levels of HRQoL. Minors from Afghanistan had significantly lower scores of HRQoL for all dimensions compared to those from Iraq and Syria.

Conclusion

Refugee minors had significantly lower levels of HRQoL for psychological wellbeing and peers and social support compared to European references. Future research should further investigate this potential HRQoL gap further.
The mental health of ex-prisoners: analysis of the 2014 English National Survey of Psychiatric Morbidity
Authors: Bebbington Paul E. , McManus Sally , Coid Jeremy W. , Garside Richard , Brugha Terry
Published: March 2021

Purpose

Prisoners experience extremely high rates of psychiatric disturbance. However, ex-prisoners have never previously been identified in representative population surveys to establish how far this excess persists after release. Our purpose was to provide the first community-based estimate of ex-prisoners’ mental health in England using the data from the 2014 Adult Psychiatric Morbidity Survey (APMS).

Methods

APMS 2014 provides cross-sectional data from a random sample (N = 7546) of England’s household population aged 16 or above. Standardised instruments categorised psychiatric disorders and social circumstances. Participants who had been in prison were compared with the rest of the sample.

Results

One participant in seventy had been in prison (1.4%; 95% CI 1.1–1.7; n = 103). Ex-prisoners suffered an excess of current psychiatric problems, including common mental disorders (CMDs), psychosis, post-traumatic disorder, substance dependence, and suicide attempts. They were more likely to screen positive for attention-deficit/hyperactivity disorder and autistic traits, to have low verbal IQ, and to lack qualifications. They disclosed higher rates of childhood adversity, including physical and sexual abuse and local authority care. The odds (1.88; 95% CI 1.02–3.47) of CMDs were nearly doubled in ex-prisoners, even after adjusting for trauma and current socioeconomic adversity.

Conclusions

Prison experience is a marker of enduring psychiatric vulnerability, identifying an important target population for intervention and support. Moreover, the psychiatric attributes of ex-prisoners provide the context for recidivism. Without effective liaison between the criminal justice system and mental health services, the vulnerability of ex-prisoners to relapse and to reoffending will continue, with consequent personal and societal costs.
Local Spatialized Knowledge of Threats to Forest Conservation in Ghana’s High Forest Zone
Authors: Somuah Dorcas Peggy , Ros–Tonen Mirjam A. F. , Baud Isa
Published: March 2021

Although deforestation rates are declining, protected forest areas remain under threat. While the importance of spatialized (‘mapped’) community knowledge for conservation planning is acknowledged in scientific literature, the integration of such knowledge in forest governance and conservation planning remains scarce, particularly in Ghana. This paper aims to make clear how participatory spatial knowledge tools and geographic information systems can be used to assess the threats to forest conservation in Ghana’s high forest zone. The results show that holders of spatial community-embedded knowledge not only sketch-mapped the location and spatial distribution of the threats to forest conservation in the forest reserves, but also provided information on the actors they perceived to be causing such threats. Such information is not available in forest inventories conducted by the responsible government agencies, but is needed to focus conservation strategies and make them more effective. Maps with the anticipated condition of the forest in 10 years’ time furthermore provided insights which can help governance actors to deal with the underlying drivers of forest degradation. This suggests that local spatialized knowledge needs to be integrated into the institutional arrangements for the governance of forested landscapes, and that such governance cannot be effective without the inclusion of local people’s knowledge. Due consideration is however to be given to the conditions that ensure that spatialized knowledge production and its use in landscape management decision-making occurs in an inclusive manner.
Two Marine Desulfotomaculum spp. of Different Origin are Capable of Utilizing Acetone and Higher Ketones
Authors: Frey Jasmin , Kaßner Sophie , Schink Bernhard
Published: March 2021

Degradation of acetone and higher ketones has been described in detail for aerobic and nitrate-reducing bacteria. Among sulfate-reducing bacteria, degradation of acetone and other ketones is still an uncommon ability and has not been understood completely yet. In the present work, we show that Desulfotomaculum arcticum and Desulfotomaculum geothermicum are able to degrade acetone and butanone. Total proteomics of cell-free extracts of both organisms indicated an involvement of a thiamine diphosphate-dependent enzyme, a B12-dependent mutase, and a specific dehydrogenase during acetone degradation. Similar enzymes were recently described to be involved in acetone degradation by Desulfococcus biacutus. As there are so far only two described sulfate reducers able to degrade acetone, D. arcticum and D. geothermicum represent two further species with this capacity. All these bacteria appear to degrade acetone via the same set of enzymes and therefore via the same pathway.
Pelagic deep-sea fauna observed on video transects in the southern Norwegian Sea
Authors: Neitzel Philipp , Hosia Aino , Piatkowski Uwe , Hoving Henk-Jan
Published: March 2021

Observations of the diversity, distribution and abundance of pelagic fauna are absent for many ocean regions in the Atlantic, but baseline data are required to detect changes in communities as a result of climate change. Gelatinous fauna are increasingly recognized as vital players in oceanic food webs, but sampling these delicate organisms in nets is challenging. Underwater (in situ) observations have provided unprecedented insights into mesopelagic communities in particular for abundance and distribution of gelatinous fauna. In September 2018, we performed horizontal video transects (50–1200 m) using the pelagic in situ observation system during a research cruise in the southern Norwegian Sea. Annotation of the video recordings resulted in 12 abundant and 7 rare taxa. Chaetognaths, the trachymedusa Aglantha digitale and appendicularians were the three most abundant taxa. The high numbers of fishes and crustaceans in the upper 100 m was likely the result of vertical migration. Gelatinous zooplankton included ctenophores (lobate ctenophores, Beroe spp., Euplokamis sp., and an undescribed cydippid) as well as calycophoran and physonect siphonophores. We discuss the distributions of these fauna, some of which represent the first record for the Norwegian Sea.
Arthroscopic anatomy of the posterolateral corner of the knee: anatomic relations and arthroscopic approaches
Authors: Frings Jannik , Weiß Sebastian , Kolb Jan , Behrendt Peter , Frosch Karl-Heinz , Krause Matthias
Published: March 2021

Introduction

Although open-surgical techniques for the reconstruction of the posterolateral corner (PLC) are well established, the use of arthroscopic procedures has recently increased. When compared with open surgical preparation, arthroscopic orientation in the PLC is challenging and anatomic relations may not be familiar. Nevertheless, a profound knowledge of anatomic key structures and possible structures at risk as well as technical variations of arthroscopic approaches are mandatory to allow a precise and safe surgical intervention.

Materials and methods

In a cadaveric video demonstration, an anterolateral (AL), anteromedial (AM), posteromedial (PM) and posterolateral (PL) portal, as well as a transseptal approach (TSA) were developed. Key structures of the PLC were defined and sequentially exposed during posterolateral arthroscopy. Finally, anatomic relations of all key structures were demonstrated.

Results

All key structures of the PLC can be visualized during arthroscopy. Thereby, careful portal placement is crucial in order to allow an effective exposure. Two alternatives of the TSA were described, depending on the region of interest. The peroneal nerve can be visualized dorsal to the biceps femoris tendon (BT), lateral to the soleus muscle (SM) and about 3 cm distal to the fibular styloid (FS). The distal attachment of the fibular collateral ligament (FCL) can be exposed on the lateral side of the fibular head (FH). The fibular attachment of the popliteofibular ligament (PFL) is exposed at the tip of the FS.

Conclusion

Arthroscopy of the posterolateral recessus allows full visualization of all key structures of the posterolateral corner, which provides the basis for anatomic and safe drill channel placement in PLC reconstruction. A sufficient exposure of relevant anatomic landmarks and precise portal preparation reduce the risk of iatrogenic vascular and peroneal nerve injury.
Anti-pruritic effect of nemolizumab in hemodialysis patients with uremic pruritus: a phase II, randomized, double-blind, placebo-controlled clinical study
Authors: Kinugasa Eriko , Igawa Ken , Shimada Hisaki , Kondo Morihiro , Funakoshi Satoshi , Imada Naoki , Itami Noritomo , Fukazawa Naoki , Takubo Ryoko , Kawata Yuichi , Murota Hiroyuki
Published: March 2021

Background

The pathophysiology of uremic pruritus (UP), which is characterized by systemic and intractable itching, remains unclear. As interleukin (IL)-31 may be involved, we conducted a phase II, randomized, controlled study to evaluate nemolizumab (anti-IL-31 receptor A antibody) in Japanese hemodialysis patients with UP.

Methods

Patients were randomly assigned (1:1:1:1:1) to one of four double-blind groups (receiving a single subcutaneous injection of nemolizumab 0.125, 0.5, or 2.0 mg/kg, or placebo on Day 1) or an open-label reference group (receiving oral nalfurafine hydrochloride 2.5–5 μg once daily for 12 weeks). The primary endpoint was the difference in the absolute change in pruritus visual analog scale (VAS) at Week 4 between placebo and each nemolizumab group.

Results

The primary efficacy endpoint was not met. The mean change from baseline with all three nemolizumab doses at Week 1, and with 0.5 mg/kg at Week 4, was greater than with placebo. Least square mean differences (95% confidence intervals) in the absolute changes between the placebo arm and each nemolizumab arm were − 2.4 (− 19.7, 14.9) for 0.125 mg/kg, − 8.7 (− 26.6, 9.2) for 0.5 mg/kg, and 0.4 (− 17.0, 17.8) for 2.0 mg/kg. Secondary efficacy parameters including the Shiratori severity score and 5-D itch score failed to show between-group differences. Patients with higher serum IL-31 levels at screening tended to have greater pruritus VAS reductions following nemolizumab treatment.

Conclusions

In this phase II study in patients with UP, the primary efficacy parameter was not met. Nemolizumab was generally well tolerated with no clinically significant safety concerns.

Clinical trial registration

JAPIC: JapicCTI-152961, https://www.clinicaltrials.jp/cti-user/trial/ShowDirect.jsp?japicId=JapicCTI-152961.
An empirical study on changing leadership in agile teams
Authors: Spiegler Simone V. , Heinecke Christoph , Wagner Stefan
Published: March 2021

An increasing number of companies aim to enable their development teams to work in an agile manner. When introducing agile teams, companies face several challenges. This paper explores the kind of leadership needed to support teams to work in an agile way. One theoretical agile leadership concept describes a Scrum Master who is supposed to empower the team to lead itself. Empirical findings on such a leadership role are controversial. We still have not understood how leadership unfolds in a team that is by definition self-organizing. Further exploration is needed to better understand leadership in agile teams. Our goal is to explore how leadership changes while the team matures using the example of the Scrum Master. Through a grounded theory study containing 75 practitioners from 11 divisions at the Robert Bosch GmbH we identified a set of nine leadership roles that are transferred from the Scrum Master to the Development Team while it matures. We uncovered that a leadership gap and a supportive internal team climate are enablers of the role transfer process, whereas role conflicts may diminish the role transfer. To make the Scrum Master change in a mature team, team members need to receive trust and freedom to take on a leadership role which was previously filled by the Scrum Master. We conclude with practical implications for managers, Product Owners, Development Teams and Scrum Masters which they can apply in real settings.
Using Synthetic Adjustments and Controlling to Improve County Population Forecasts from the Hamilton–Perry Method
Authors: Tayman Jeff , Swanson David A. , Baker Jack
Published: March 2021

Tayman and Swanson (J Popul Res 34(3):209–231, 2017) found in Washington State counties that a forecast based on the Hamilton–Perry method using a synthetic adjustment (SYN) of cohort change ratios and child-woman ratios had greater accuracy and less bias compared to forecasts holding these ratios constant (CONST). In this paper, we assess the robustness of SYN’s efficacy by evaluating forecast accuracy, bias, and distributional error across age groups in counties nationwide. We also investigate whether forecast errors and their patterns change for SYN and CONST if forecasts by age and gender are adjusted to an independent total population forecast for each county. Our main findings are as follows: (1) SYN lowers forecast error compared to CONST whether the forecasts are controlled or not; (2) controlling also leads to the improvements in forecast error, often exceeding those in SYN; and (3) using SYN and controlling together has the greatest effect in reducing forecast error. These findings remain after controlling for population size and growth rate, but the positive impacts on forecast error of SYN and controlling are most evident in counties with less than 30,000 population and that grow by 15% or more.
Putative invasive pulmonary aspergillosis within medical wards and intensive care units: a 4-year retrospective, observational, single-centre study
Authors: Corcione Silvia , Lupia Tommaso , Raviolo Stefania , Montrucchio Giorgia , Trentalange Alice , Curtoni Antonio , Cavallo Rossana , De Rosa Francesco Giuseppe
Published: March 2021

Blot and colleagues have proposed putative invasive pulmonary aspergillosis (PIPA) definitions for troublesome diagnosis in suspected patients outside the classical criteria of immunosuppression. We retrospectively included in the study all admitted patients with an Aspergillus spp. positive culture within lower airway samples. Overall, Aspergillus spp. positivity in respiratory samples was 0.97 every 1000 hospital admissions (HA): 4.94 and 0.28/1000/HA, respectively, in intensive care units (ICUs) and medical wards (MW). 66.6% fulfilled PIPA criteria, and 33.4% were defined as colonized. 69.2% of PIPA diagnosis occurred in the ICU. Antifungal therapy was appropriate in 88.5% of subjects with PIPA and 37.5% of colonized, confirming the comparison between deads and lives. Patients with PIPA in the ICUs had more frequent COPD, sepsis or septic shock, acute kidney injury (AKI), needed more surgery, mechanical ventilation (MV), vasopressors, hemodialysis, blood or platelets transfusions. PIPA in MW had associated with a history of smoking, interstitial lung disease and inhaled steroid therapy. Overall mortality within 21 days was 50%: 54.2% in ICU, 36,8% in MW. Factors associated with death were length of hospitalization, influenza, pneumonia, liver transplant, AKI, ARDS, sepsis and septic shock. PIPA in the ICU had higher disease severity and needed more organ support than MW cases, despite that cases of PIPA in MW are emerging with trends difficult to demonstrate given the problematic diagnosis.
A comprehensive KPI network for the performance measurement and management in global production networks
Authors: Verhaelen B. , Mayer F. , Peukert S. , Lanza G.
Published: March 2021

The trend of globalization has led to a structural change in the sales and procurement markets of manufacturing companies in recent decades. In order not to be left behind by this change, companies have internationalized their production structures. Global production networks with diverse supply and service interdependencies are the result. However, the management of global production networks is highly complex. Key performance indicator (KPI) networks already exist at the corporate level and site level to support the management of complex systems. However, such KPI networks are not yet available to support the management of entire production networks. In this article, a KPI network for global production networks is presented, which links the key figures of the site level and the corporate level. By integrating both levels into a comprehensive KPI network, cause and effect relationship between the production-related KPIs and the strategic KPIs of a corporate strategy become transparent. To this end, this KPI network is integrated into a Performance Measurement and Management (PMM) methodology. This methodology consists of three phases: performance planning, performance improvement, and performance review. For testing the practical suitability, the PMM methodology is applied to the production network of an automotive supplier using a simulation model to estimate the effects of proposed improvement actions of the methodology.