bluuebunny/crossref_metadata_2025 huggingface dataset:
Stateless Model Checking Under a Reads-Value-From Equivalence
Authors: Agarwal Pratyush , Chatterjee Krishnendu , Pathak Shreya , Pavlogiannis Andreas , Toman Viktor
Published: July 2021

Stateless model checking (SMC) is one of the standard approaches to the verification of concurrent programs. As scheduling non-determinism creates exponentially large spaces of thread interleavings, SMC attempts to partition this space into equivalence classes and explore only a few representatives from each class. The efficiency of this approach depends on two factors: (a) the coarseness of the partitioning, and (b) the time to generate representatives in each class. For this reason, the search for coarse partitionings that are efficiently explorable is an active research challenge.

In this work we present$${\text {RVF-SMC}}$$RVF-SMC, a new SMC algorithm that uses a novelreads-value-from (RVF)partitioning. Intuitively, two interleavings are deemed equivalent if they agree on the value obtained in each read event, and read events induce consistent causal orderings between them. The RVF partitioning is provably coarser than recent approaches based on Mazurkiewicz and “reads-from” partitionings. Our experimental evaluation reveals that RVF is quite often a very effective equivalence, as the underlying partitioning is exponentially coarser than other approaches. Moreover,$${\text {RVF-SMC}}$$RVF-SMCgenerates representatives very efficiently, as the reduction in the partitioning is often met with significant speed-ups in the model checking task.
Gobra: Modular Specification and Verification of Go Programs
Authors: Wolf Felix A. , Arquint Linard , Clochard Martin , Oortwijn Wytse , Pereira João C. , Müller Peter
Published: July 2021

Go is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subtyping and lightweight concurrency through goroutines with message-passing communication. This combination of features poses interesting challenges for static verification, most prominently the combination of a mutable heap and advanced concurrency primitives.

We present Gobra, a modular, deductive program verifier for Go that proves memory safety, crash safety, data-race freedom, and user-provided specifications. Gobra is based on separation logic and supports a large subset of Go. Its implementation translates an annotated Go program into the Viper intermediate verification language and uses an existing SMT-based verification backend to compute and discharge proof obligations.
Delay-Bounded Scheduling Without Delay!
Authors: Johnson Andrew , Wahl Thomas
Published: July 2021

We consider the broad problem of analyzing safety properties of asynchronous concurrent programs under arbitrary thread interleavings.Delay-bounded deterministic scheduling, introduced in prior work, is an efficient bug-finding technique to curb the large cost associated with full scheduling nondeterminism. In this paper we first present a technique tolift the delay boundfor the case of finite-domain variable programs, thus adding to the efficiency of bug detection the ability to prove safety of programs under arbitrary thread interleavings. Second, we demonstrate how, combined with predicate abstraction, our technique can both refute and verify safety properties of programs with unbounded variable domains, even for unbounded thread counts. Previous work has established that, for non-trivial concurrency routines, predicate abstraction induces a highly complex abstract program semantics. Our technique, however, never statically constructs an abstract parametric program; it only requires some abstract-states set to be closed under certain actions, thus eliminating the dependence on the existence of verification algorithms for abstract programs. We demonstrate the efficiency of our technique on many examples used in prior work, and showcase its simplicity compared to earlier approaches on the unbounded-thread Ticket Lock protocol.
Checking Data-Race Freedom of GPU Kernels, Compositionally
Authors: Cogumbreiro Tiago , Lange Julien , Rong Dennis Liew Zhen , Zicarelli Hannah
Published: July 2021

GPUs offer parallelism as a commodity, but they are difficult to program correctly. Static analyzers that guarantee data-race freedom (DRF) are essential to help programmers establish the correctness of their programs (kernels). However, existing approaches produce too many false alarms and struggle to handle larger programs. To address these limitations we formalize a novel compositional analysis for DRF, based on access memory protocols. These protocols are behavioral types that codify the way threads interact over shared memory.

Our work includes fully mechanized proofs of our theoretical results, the first mechanized proofs in the field of DRF analysis for GPU kernels. Our theory is implemented in , a tool that outperforms the state-of-the-art. Notably, it can correctly verify at least $$1.42{\times }$$

1.42
×

more real-world kernels, and it exhibits a linear growth in 4 out of 5 experiments, while others grow exponentially in all 5 experiments.
GenMC: A Model Checker for Weak Memory Models
Authors: Kokologiannakis Michalis , Vafeiadis Viktor
Published: July 2021

GenMC is an LLVM-based state-of-the-art stateless model checker for concurrent C/C++ programs. Its modular infrastructure allows it to support complex memory models, such as RC11 and IMM, and makes it easy to extend to support further axiomatic memory models.

In this paper, we discuss the overall architecture of the tool and how it can be extended to support additional memory models, programming languages, and/or synchronization primitives. To demonstrate the point, we have extended the tool with support for the Linux kernel memory model (LKMM), synchronization barriers, POSIX I/O system calls, and better error detection capabilities.
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming
Authors: Wang Qiuye , Chen Mingshuai , Xue Bai , Zhan Naijun , Katoen Joost-Pieter
Published: July 2021

A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set of states, and hence is widely used in proving safety of hybrid systems possibly over the infinite time horizon. We present a novel condition on barrier certificates, termed theinvariant barrier-certificate condition, that witnesses unbounded-time safety of differential dynamical systems. The proposed condition is by far the least conservative one on barrier certificates, and can be shown as the weakest possible one to attain inductive invariance. We show that discharging the invariant barrier-certificate condition—thereby synthesizing invariant barrier certificates—can be encoded as solving anoptimization problem subject to bilinear matrix inequalities(BMIs). We further propose a synthesis algorithm based on difference-of-convex programming, which approaches a local optimum of the BMI problem via solvinga series of convex optimization problems. This algorithm is incorporated in a branch-and-bound framework that searches for the global optimum in a divide-and-conquer fashion. We present a weak completeness result of our method, in the sense that a barrier certificate is guaranteed to be found (under some mild assumptions) whenever there exists an inductive invariant (in the form of a given template) that suffices to certify safety of the system. Experimental results on benchmark examples demonstrate the effectiveness and efficiency of our approach.
Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems
Authors: Mover Sergio , Cimatti Alessandro , Griggio Alberto , Irfan Ahmed , Tonetta Stefano
Published: July 2021

Semi-algebraic abstraction is an approach to the safety verification problem for polynomial dynamical systems where the state space is partitioned according to the sign of a set of polynomials. Similarly to predicate abstraction for discrete systems, the number of abstract states is exponential in the number of polynomials. Hence, semi-algebraic abstraction is expensive to explicitly compute and then analyze (e.g., to prove a safety property or extract invariants).

In this paper, we propose an implicit encoding of the semi-algebraic abstraction, which avoids the explicit enumeration of the abstract states: the safety verification problem for dynamical systems is reduced to a corresponding problem for infinite-state transition systems, allowing us to reuse existing model-checking tools based on Satisfiability Modulo Theory (SMT). The main challenge we solve is to express the semi-algebraic abstraction as a first-order logic formula that is linear in the number of predicates, instead of exponential, thus letting the model checker lazily explore the exponential number of abstract states with symbolic techniques. We implemented the approach and validated experimentally its potential to prove safety for polynomial dynamical systems.
IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability
Authors: André Étienne
Published: July 2021

Real-time systems are notoriously hard to verify due to nondeterminism, concurrency and timing constraints. When timing constants are uncertain (in early the design phase, or due to slight variations of the timing bounds), timed model checking techniques may not be satisfactory. In contrast, parametric timed model checking synthesizes timing values ensuring correctness. takes as input an extension of parametric timed automata (PTAs), a powerful formalism to formally verify critical real-time systems. extends PTAs with multi-rate clocks, global rational-valued variables and a set of additional useful features. We describe here the new features and algorithms offered by  3, that moved along the years from a simple prototype dedicated to robustness analysis to a standalone parametric model checker for timed systems.
Formally Verified Switching Logic for Recoverability of Aircraft Controller
Authors: Lal Ratan , McKinnis Aaron , Hauptman Dustin , Keshmiri Shawn , Prabhakar Pavithra
Published: July 2021

In this paper, we investigate the design of a safe hybrid controller for an aircraft that switches between a classical linear quadratic regulator (LQR) controller and a more intelligent artificial neural network (ANN) controller. Our objective is to switch safely between
the controllers, such that the aircraft is always recoverable within a fixed amount of time while allowing the maximum time of operation for the ANN controller. There is a priori known safety zone for the LQR controller operation in which the aircraft never stalls, over accelerates, or exceeds maximum structural loading, and hence, by switching to the LQR controller just before exiting this zone, one can guarantee safety. However, this priori known safety zone is conservative, and therefore, limits the time of operation for the ANN controller. We apply reachability analysis to expand the known safety zone, such that the LQR controller will always be able to drive the aircraft back to the safe zone from the expanded zone (“recoverable zone") within a fixed duration. The “recoverable zone" extends the time of operation of the ANN controller. We perform simulations using the hybrid controller corresponding to the recoverable zone and observe that the design is indeed safe.
$$\mathsf {SceneChecker}$$: Boosting Scenario Verification Using Symmetry Abstractions
Authors: Sibai Hussein , Li Yangge , Mitra Sayan
Published: July 2021

We present $$\mathsf {SceneChecker}$$
SceneChecker
, a tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. $$\mathsf {SceneChecker}$$
SceneChecker
converts the scenario verification problem to a standard hybrid system verification problem, and solves it effectively by exploiting structural properties in the plan and the vehicle dynamics. $$\mathsf {SceneChecker}$$
SceneChecker
uses symmetry abstractions, a novel refinement algorithm, and importantly, is built to boost the performance of any existing reachability analysis tool as a plug-in subroutine. We evaluated $$\mathsf {SceneChecker}$$
SceneChecker
on several scenarios involving ground and aerial vehicles with nonlinear dynamics and neural network controllers, employing different kinds of symmetries, using different reachability subroutines, and following plans with hundreds of waypoints in complex workspaces. Compared to two leading tools, DryVR and Flow*, $$\mathsf {SceneChecker}$$
SceneChecker
shows 14$$\times $$
×
average speedup in verification time, even while using those very tools as reachability subroutines.
Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness
Authors: Zhang Zhenya , Lyu Deyun , Arcaini Paolo , Ma Lei , Hasuo Ichiro , Zhao Jianjun
Published: July 2021

Hybrid system falsification is an important quality assurance method for cyber-physical systems with the advantage of scalability and feasibility in practice than exhaustive verification. Falsification, given a desired temporal specification, tries to find an input of violation instead of a proof guarantee. The state-of-the-art falsification approaches often employ stochastic hill-climbing optimization that minimizes the degree of satisfaction of the temporal specification, given by its quantitativerobust semantics. However, it has been shown that the performance of falsification could be severely affected by the so-calledscale problem, related to the different scales of the signals used in the specification (e.g., rpm and speed): in the robustness computation, the contribution of a signal could bemaskedby another one. In this paper, we propose a novel approach to tackle this problem. We first introduce a new robustness definition, calledQB-Robustness, which combines classical Boolean satisfaction and quantitative robustness. We prove that QB-Robustness can be used to judge the satisfaction of the specification and avoid the scale problem in its computation. QB-Robustness is exploited by a falsification approach based on Monte Carlo Tree Search over the structure of the formal specification. First, tree traversal identifies the sub-formulas for which it is needed to compute the quantitative robustness. Then, on the leaves, numerical hill-climbing optimization is performed, aiming to falsify such sub-formulas. Our in-depth evaluation on multiple benchmarks demonstrates that our approach achieves better falsification results than the state-of-the-art falsification approaches guided by the classical quantitative robustness, and it is largely not affected by the scale problem.
Fast Zone-Based Algorithms for Reachability in Pushdown Timed Automata
Authors: Akshay S. , Gastin Paul , Prakash Karthik R.
Published: July 2021

Given the versatility of timed automata a huge body of work has evolved that considers extensions of timed automata. One extension that has received a lot of interest is timed automata with a, possibly unbounded, stack, also called pushdown timed automata (PDTA). While different algorithms have been given for reachability in different variants of this model, most of these results are purely theoretical and do not give rise to efficient implementations. One main reason for this is that none of these algorithms (and the implementations that exist) use the so-called zone-based abstraction, but rely either on the region-abstraction or other approaches, which are significantly harder to implement.

In this paper, we show that a naive extension, using simulations, of the zone based reachability algorithm for the control state reachability problem of timed automata is not sound in the presence of a stack. To understand this better we give an inductive rule based view of the zone reachability algorithm for timed automata. This alternate view allows us to analyze and adapt the rules to also work for pushdown timed automata. We obtain the first zone-based algorithm for PDTA which is terminating, sound and complete. We implement our algorithm in the tool TChecker and perform experiments to show its efficacy, thus leading the way for more practical approaches to the verification of timed pushdown systems.
Verified Cryptographic Code for Everybody
Authors: Boston Brett , Breese Samuel , Dodds Joey , Dodds Mike , Huffman Brian , Petcher Adam , Stefanescu Andrei
Published: July 2021

We have completed machine-assisted proofs of two highly-optimized cryptographic primitives, AES-256-GCM and SHA-384. We have verified that the implementations of these primitives, written in a mix of C and x86 assembly, are memory safe and functionally correct, by which we mean input-output equivalent to their algorithmic specifications. Our proofs were completed using SAW, a bounded cryptographic verification tool which we have extended to handle embedded x86. The code we have verified comes from AWS LibCrypto. This code is identical to BoringSSL and very similar to OpenSSL, from which it ultimately derives. We believe we are the first to formally verify these implementations, which protect the security of nearly everybody on the internet.
Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference
Authors: Girol Guillaume , Farinier Benjamin , Bardin Sébastien
Published: July 2021

This paper introduces a new property calledrobust reachabilitywhich refines the standard notion of reachability in order to take replicability into account. A bug is robustly reachable if acontrolled inputcan make it so the bug is reached whatever the value ofuncontrolled input. Robust reachability is better suited than standard reachability in many realistic situations related to security (e.g., criticality assessment or bug prioritization) or software engineering (e.g., replicable test suites and flakiness). We propose a formal treatment of the concept, and we revisit existing symbolic bug finding methods through this new lens. Remarkably, robust reachability allows differentiating bounded model checking from symbolic execution while they have the same deductive power in the standard case. Finally, we propose the first symbolic verifier dedicated to robust reachability: we use it for criticality assessment of 4 existing vulnerabilities, and compare it with standard symbolic execution.
A Temporal Logic for Asynchronous Hyperproperties
Authors: Baumeister Jan , Coenen Norine , Bonakdarpour Borzoo , Finkbeiner Bernd , Sánchez César
Published: July 2021

Hyperpropertiesare properties of computational systems that require more than one trace to evaluate, e.g., many information-flow security and concurrency requirements. Where a trace property defines a set of traces, a hyperproperty defines a set of sets of traces. The temporal logics HyperLTL and HyperCTL* have been proposed to express hyperproperties. However, their semantics aresynchronousin the sense that all traces proceed at the same speed and are evaluated at the same position. This precludes the use of these logics to analyze systems whose traces can proceed at different speeds and allow that different traces take stuttering steps independently. To solve this problem in this paper, we propose anasynchronousvariant of HyperLTL. On the negative side, we show that the model-checking problem for this variant is undecidable. On the positive side, we identify a decidable fragment which covers a rich set of formulas with practical applications. We also propose two model-checking algorithms that reduce our problem to the HyperLTL model-checking problem in the synchronous semantics.
Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security
Authors: Eilers Marco , Meier Severin , Müller Peter
Published: July 2021

Most existing program verifiers check trace properties such as functional correctness, but do not support the verification of hyperproperties, in particular, information flow security. In principle, product programs allow one to reduce the verification of hyperproperties to trace properties and, thus, apply standard verifiers to check them; in practice, product constructions are usually defined only for simple programming languages without features like dynamic method binding or concurrency and, consequently, cannot be directly applied to verify information flow security in a full-fledged language. However, many existing verifiers encode programs from source languages into simple intermediate verification languages, which opens up the possibility of constructing a product program on the intermediate language level, reusing the existing encoding and drastically reducing the effort required to develop new verification tools for information flow security.

In this paper, we explore the potential of this approach along three dimensions: (1) Soundness: We show that the combination of an encoding and a product construction that are individually sound can still be unsound, and identify a novel condition on the encoding that ensures overall soundness. (2) Concurrency: We show how sequential product programs on the intermediate language level can be used to verify information flow security of concurrent source programs. (3) Performance: We implement a product construction in Nagini, a Python verifier built upon the Viper intermediate language, and evaluate it on a number of challenging examples. We show that the resulting tool offers acceptable performance, while matching or surpassing existing tools in its combination of language feature support and expressiveness.
Constraint-Based Relational Verification
Authors: Unno Hiroshi , Terauchi Tachio , Koskinen Eric
Published: July 2021

In recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses ($$\mathrm {CHCs}$$
CHCs
) empower a wide range of verification techniques and tools, they lack the ability to express hyperproperties beyond k-safety such as generalized non-interference and co-termination.

This paper describes a novel and fully automated constraint-based approach to relational verification. We first introduce a new class of predicate Constraint Satisfaction Problems called $$\mathrm {pfwCSP}$$
pfwCSP
where constraints are represented as clauses modulo first-order theories over predicate variables of three kinds: ordinary, well-founded, or functional. This generalization over $$\mathrm {CHCs}$$
CHCs
permits arbitrary (i.e., possibly non-Horn) clauses, well-foundedness constraints, functionality constraints, and is capable of expressing these relational verification problems. Our approach enables us to express and automatically verify problem instances that require non-trivial (i.e., non-sequential and non-lock-step) self-composition by automatically inferring appropriate schedulers (or alignment) that dictate when and which program copies move. To solve problems in this new language, we present a constraint solving method for $$\mathrm {pfwCSP}$$
pfwCSP
based on stratified CounterExample-Guided Inductive Synthesis (CEGIS) of ordinary, well-founded, and functional predicates.

We have implemented the proposed framework and obtained promising results on diverse relational verification problems that are beyond the scope of the previous verification frameworks.
Counterexample-Guided Partial Bounding for Recursive Function Synthesis
Authors: Farzan Azadeh , Nicolet Victor
Published: July 2021

Quantifier bounding is a standard approach in inductive program synthesis in dealing with unbounded domains. In this paper, we propose one such bounding method for the synthesis of recursive functions over recursive input data types. The synthesis problem is specified by an input reference (recursive) function and a recursion skeleton. The goal is to synthesize a recursive function equivalent to the input function whose recursion strategy is specified by the recursion skeleton. In this context, we illustrate that it is possible to selectively bound a subset of the (recursively typed) parameters, each by a suitable bound. The choices are guided by counterexamples. The evaluation of our strategy on a broad set of benchmarks shows that it succeeds in efficiently synthesizing non-trivial recursive functions where standard across-the-board bounding would fail.
Programmable Program Synthesis
Authors: D’Antoni Loris , Hu Qinheping , Kim Jinwoo , Reps Thomas
Published: July 2021

Program synthesis is now a reality, and we are approaching the point where domain-specific synthesizers can now handle problems of practical sizes. Moreover, some of these tools are finding adoption in industry. However, for synthesis to become a mainstream technique adopted at large by programmers as well as by end-users, we need to design programmable synthesis frameworks that (i) are not tailored to specific domains or languages, (ii) enable one to specify synthesis problems with a variety of qualitative and quantitative objectives in mind, and (iii) come equipped with theoretical as well as practical guarantees. We report on our work on designing such frameworks and on building synthesis engines that can handle program-synthesis problems describable in such frameworks, and describe open challenges and opportunities.
PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs
Authors: Andriushchenko Roman , Češka Milan , Junges Sebastian , Katoen Joost-Pieter , Stupinský Šimon
Published: July 2021

This paper presents PAYNT, a tool to automatically synthesise probabilistic programs. PAYNT enables the synthesis of finite-state probabilistic programs from a program sketch representing a finite family of program candidates. A tight interaction between inductive oracle-guided methods with state-of-the-art probabilistic model checking is at the heart of PAYNT. These oracle-guided methods effectively reason about all possible candidates and synthesise programs that meet a given specification formulated as a conjunction of temporal logic constraints and possibly including an optimising objective. We demonstrate the performance and usefulness of PAYNT using several case studies from different application domains; e.g., we find the optimal randomized protocol for network stabilisation among 3M potential programs within minutes, whereas alternative approaches would need days to do so.
Adapting Behaviors via Reactive Synthesis
Authors: Amram Gal , Bansal Suguman , Fried Dror , Tabajara Lucas Martinelli , Vardi Moshe Y. , Weiss Gera
Published: July 2021

In the Adapter Design Pattern, a programmer implements a Target interface by constructing an Adapter that accesses an existing Adaptee code. In this work, we present a reactive synthesis interpretation to the adapter design pattern, wherein an algorithm takes an Adaptee and a Target transducers, and the aim is to synthesize an Adapter transducer that, when composed with the Adaptee, generates a behavior that is equivalent to the behavior of the Target. One use of such an algorithm is to synthesize controllers that achieve similar goals on different hardware platforms. While this problem can be solved with existing synthesis algorithms, current state-of-the-art tools fail to scale. To cope with the computational complexity of the problem, we introduce a special form of specification format, called Separated GR(k), which can be solved with a scalable synthesis algorithm but still allows for a large set of realistic specifications. We solve the realizability and the synthesis problems for Separated GR(k), and show how to exploit the separated nature of our specification to construct better algorithms, in terms of time complexity, than known algorithms for GR(k) synthesis. We then describe a tool, called SGR(k), that we have implemented based on the above approach and show, by experimental evaluation, how our tool outperforms current state-of-the-art tools on various benchmarks and test-cases.
Causality-Based Game Solving
Authors: Baier Christel , Coenen Norine , Finkbeiner Bernd , Funke Florian , Jantsch Simon , Siber Julian
Published: July 2021

We present a causality-based algorithm for solving two-player reachability games represented by logical constraints. These games are a useful formalism to model a wide array of problems arising, e.g., in program synthesis. Our technique for solving these games is based on the notion of subgoals, which are slices of the game that the reachability player necessarily needs to pass through in order to reach the goal. We use Craig interpolation to identify these necessary sets of moves and recursively slice the game along these subgoals. Our approach allows us to infer winning strategies that are structured along the subgoals. If the game is won by the reachability player, this is a strategy that progresses through the subgoals towards the final goal; if the game is won by the safety player, it is a permissive strategy that completely avoids a single subgoal. We evaluate our prototype implementation on a range of different games. On multiple benchmark families, our prototype scales dramatically better than previously available tools.
Robustness Verification of Quantum Classifiers
Authors: Guan Ji , Fang Wang , Ying Mingsheng
Published: July 2021

Several important models of machine learning algorithms have been successfully generalized to the quantum world, with potential speedup to training classical classifiers and applications to data analytics in quantum physics that can be implemented on the near future quantum computers. However, quantum noise is a major obstacle to the practical implementation of quantum machine learning. In this work, we define a formal framework for the robustness verification and analysis of quantum machine learning algorithms against noises. A robust bound is derived and an algorithm is developed to check whether or not a quantum machine learning algorithm is robust with respect to quantum training data. In particular, this algorithm can find adversarial examples during checking. Our approach is implemented on Google’s TensorFlow Quantum and can verify the robustness of quantum machine learning algorithms with respect to a small disturbance of noises, derived from the surrounding environment. The effectiveness of our robust bound and algorithm is confirmed by the experimental results, including quantum bits classification as the “Hello World” example, quantum phase recognition and cluster excitation detection from real world intractable physical problems, and the classification of MNIST from the classical world.
Supersymmetric spectroscopy on AdS4 × S7 and AdS4 × S6
Authors: Cesàro Mattia , Larios Gabriel , Varela Oscar
Published: July 2021

Abstract

New techniques based on Exceptional Field Theory have recently allowed for the calculation of the Kaluza-Klein spectra of certain AdS4 solutions of D = 11 and massive IIA supergravity. These are the solutions that consistently uplift on S7 and S6 from vacua of maximal four-dimensional supergravity with SO(8) and ISO(7) gaugings. In this paper, we provide an algorithmic procedure to compute the complete Kaluza-Klein spectrum of five such AdS4 solutions, all of them $$ \mathcal{N} $$
N
= 1, and give the first few Kaluza-Klein levels. These solutions preserve SO(3) and U(1) × U(1) internal symmetry in D = 11, and U(1) (two of them) and no continuous symmetry in type IIA. Together with previously discussed cases, our results exhaust the Kaluza-Klein spectra of known supersymmetric AdS4 solutions in D = 11 and type IIA in the relevant class.
BMS field theories and Weyl anomaly
Authors: Bagchi Arjun , Dutta Sudipta , Kolekar Kedar S. , Sharma Punit
Published: July 2021

Abstract

Two dimensional field theories with Bondi-Metzner-Sachs symmetry have been proposed as duals to asymptotically flat spacetimes in three dimensions. These field theories are naturally defined on null surfaces and hence are conformal cousins of Carrollian theories, where the speed of light goes to zero. In this paper, we initiate an investigation of anomalies in these field theories. Specifically, we focus on the BMS equivalent of Weyl invariance and its breakdown in these field theories and derive an expression for Weyl anomaly. Considering the transformation of partition functions under this symmetry, we derive a Carrollian Liouville action different from ones obtained in the literature earlier.
Geometry of orientifold vacua and supersymmetry breaking
Authors: Coudarchet Thibaut , Dudas Emilian , Partouche Hervé
Published: July 2021

Abstract

Starting from a peculiar orientifold projection proposed long ago by Angelantonj and Cardella, we elaborate on a novel perturbative scenario that involves only D-branes, together with the two types of orientifold planes O±and anti-orientifold planes$$ {\overline{\mathrm{O}}}_{\pm } $$O¯±. We elucidate the microscopic ingredients of such models, connecting them to a novel realization of brane supersymmetry breaking. Depending on the position of the D-branes in the internal space, supersymmetry can be broken at the string scale on branes, or alternatively only at the massive level. The main novelty of this construction is that it features no NS-NS disk tadpoles, while avoiding open-string instabilities. The one-loop potential, which depends on the positions of the D-branes, is minimized for maximally broken, non-linearly realized supersymmetry. The orientifold projection and the effective field theory description reveal a soft breaking of supersymmetry in the closed-string sector. In such models it is possible to decouple the gravitino mass from the value of the scalar potential, while avoiding brane instabilities.
How a four-dimensional de Sitter solution remains outside the swampland
Authors: Dasgupta Keshav , Emelin Maxim , Faruk Mir Mehedi , Tatar Radu
Published: July 2021

Abstract

We argue that, in the presence of time-dependent fluxes and quantum corrections, four-dimensional de Sitter solutions should appear in the type IIB string landscape and not in the swampland. Our construction considers generic choices of local and non-local quantum terms and satisfies the no-go and the swampland criteria, the latter being recently upgraded using the trans-Planckian cosmic censorship. Interestingly, both time-independent Newton constant and moduli stabilization may be achieved in such backgrounds even in the presence of time-dependent fluxes and internal spaces. However, once the time-dependence is switched off, any four-dimensional solution with de Sitter isometries appears to have no simple effective field theory descriptions and is back in the swampland.
Modelling of BCS1L-related human mitochondrial disease in Drosophila melanogaster
Authors: Brischigliaro Michele , Frigo Elena , Corrà Samantha , De Pittà Cristiano , Szabò Ildikò , Zeviani Massimo , Costa Rodolfo
Published: July 2021

Mutations in BCS1L are the most frequent cause of human mitochondrial disease linked to complex III deficiency. Different forms of BCS1L-related diseases and more than 20 pathogenic alleles have been reported to date. Clinical symptoms are highly heterogenous, and multisystem involvement is often present, with liver and brain being the most frequently affected organs. BCS1L encodes a mitochondrial AAA + -family member with essential roles in the latest steps in the biogenesis of mitochondrial respiratory chain complex III. Since Bcs1 has been investigated mostly in yeast and mammals, its function in invertebrates remains largely unknown. Here, we describe the phenotypical, biochemical and metabolic consequences of Bcs1 genetic manipulation in Drosophila melanogaster. Our data demonstrate the fundamental role of Bcs1 in complex III biogenesis in invertebrates and provide novel, reliable models for BCS1L-related human mitochondrial diseases. These models recapitulate several features of the human disorders, collectively pointing to a crucial role of Bcs1 and, in turn, of complex III, in development, organismal fitness and physiology of several tissues.
Metabolomic analysis to discriminate drug-induced liver injury (DILI) phenotypes
Authors: Quintás Guillermo , Martínez-Sena Teresa , Conde Isabel , Pareja Ibars Eugenia , Kleinjans Jos , Castell José V.
Published: July 2021

Drug-induced liver injury (DILI) is an adverse toxic hepatic clinical reaction associated to the administration of a drug that can occur both at early clinical stages of drug development, as well after normal clinical usage of approved drugs. Because of its unpredictability and clinical relevance, it is of medical concern. Three DILI phenotypes (hepatocellular, cholestatic, and mixed) are currently recognized, based on serum alanine aminotransferase (ALT) and alkaline phosphatase (ALP) values. However, this classification lacks accuracy to distinguish among the many intermediate mixed types, or even to estimate the magnitude and progression of the injury. It was found desirable to have additional elements for better evaluation criteria of DILI. With this aim, we have examined the serum metabolomic changes occurring in 79 DILI patients recruited and monitored using established clinical criteria, along the course of the disease and until recovery. Results revealed that free and conjugated bile acids, and glycerophospholipids were among the most relevant metabolite classes for DILI phenotype characterization. Using an ensemble of PLS–DA models, metabolomic information was integrated into a ternary diagram to display the disease phenotype, the severity of the liver damage, and its progression. The modeling implemented and the use of such compiled information in an easily understandable and visual manner facilitates a straightforward DILI phenotyping and allow to monitor its progression and recovery prediction, usefully complementing the concise information drawn out by the ALT and ALP classification.
Operando tracking of oxidation-state changes by coupling electrochemistry with time-resolved X-ray absorption spectroscopy demonstrated for water oxidation by a cobalt-based catalyst film
Authors: Pasquini Chiara , Liu Si , Chernev Petko , Gonzalez-Flores Diego , Mohammadi Mohammad Reza , Kubella Paul , Jiang Shan , Loos Stefan , Klingan Katharina , Sikolenko Vadim , Mebs Stefan , Haumann Michael , Beyer Paul , D’Amario Luca , Smith Rodney D. L. , Zaharieva Ivelina , Dau Holger
Published: July 2021

Transition metal oxides are promising electrocatalysts for water oxidation, i.e., the oxygen evolution reaction (OER), which is critical in electrochemical production of non-fossil fuels. The involvement of oxidation state changes of the metal in OER electrocatalysis is increasingly recognized in the literature. Tracing these oxidation states under operation conditions could provide relevant information for performance optimization and development of durable catalysts, but further methodical developments are needed. Here, we propose a strategy to use single-energy X-ray absorption spectroscopy for monitoring metal oxidation-state changes during OER operation with millisecond time resolution. The procedure to obtain time-resolved oxidation state values, using two calibration curves, is explained in detail. We demonstrate the significance of this approach as well as possible sources of data misinterpretation. We conclude that the combination of X-ray absorption spectroscopy with electrochemical techniques allows us to investigate the kinetics of redox transitions and to distinguish the catalytic current from the redox current. Tracking of the oxidation state changes of Co ions in electrodeposited oxide films during cyclic voltammetry in neutral pH electrolyte serves as a proof of principle.

Graphical abstract
Bin packing with lexicographic objectives for loading weight- and volume-constrained trucks in a direct-shipping system
Authors: Heßler Katrin , Irnich Stefan , Kreiter Tobias , Pferschy Ulrich
Published: July 2021

We consider a packing problem that arises in a direct-shipping system in the food and beverage industry: Trucks are the containers, and products to be distributed are the items. The packing is constrained by two independent quantities, weight (e.g., measured in kg) and volume (number of pallets). Additionally, the products are grouped into the three categories: standard, cooled, and frozen (the latter two require refrigerated trucks). Products of different categories can be transported in one truck using separated zones, but the cost of a truck depends on the transported product categories. Moreover, splitting orders of a product should be avoided so that (un-)loading is simplified. As a result, we seek for a feasible packing optimizing the following objective functions in a strictly lexicographic sense: minimize the (1) total number of trucks; (2) number of refrigerated trucks; (3) number of refrigerated trucks which contain frozen products; (4) number of refrigerated trucks which also transport standard products; (5) and minimize splitting. This is a real-world application of a bin-packing problem with cardinality constraints a.k.a. the two-dimensional vector packing problem with additional constraints. We provide a heuristic and an exact solution approach. The heuristic meta-scheme considers the multi-compartment and item fragmentation features of the problem and applies various problem-specific heuristics. The exact solution algorithm covering all five stages is based on branch-and-price using stabilization techniques exploiting dual-optimal inequalities. Computational results on real-world and difficult self-generated instances prove the applicability of our approach.
Differences in treatment choices between prostate cancer patients using a decision aid and patients receiving care as usual: results from a randomized controlled trial
Authors: Lamers Romy E. D. , Cuypers Maarten , de Vries Marieke , van de Poll-Franse Lonneke V. , Bosch J. L. H. Ruud , Kil Paul J. M.
Published: July 2021

Objective

To determine whether or not decision aid (DA) use influences treatment decisions in patients with low and intermediate risk prostate cancer (PC).

Patients and methods

In a cluster randomized controlled trial, patients were randomized to either DA use (DA group) or no DA use (control group). Between 2014 and 2016, newly diagnosed patients with low or intermediate risk PC were recruited in 18 hospitals in the Netherlands. DA users had access to a web-based DA that provided general PC information, PC-treatment information, and values clarification exercises to elicit personal preferences towards the treatment options. Control group patients received care as usual. Differences in treatment choice were analysed using multilevel logistic regressions. Differences in eligible treatment options between groups were compared using Pearson Chi-square tests.

Results

Informed consent was given by 382 patients (DA group N = 273, control group N = 109). Questionnaire response rate was 88% (N = 336). Active surveillance (AS) was an option for 38%, radical prostatectomy (RP) for 98%, external beam radiotherapy (EBRT) for 88%, and brachytherapy (BT) for 79% of patients. DA users received AS significantly more often than control group. Patients (29 vs 16%, p = 0.01), whereas the latter more often chose BT (29 vs 18%, p < 0.01). No differences were found between groups regarding RP and EBRT. DA users who were not eligible for AS, received surgery more often compared to the control group (53 vs 35%, p = 0.01). Patient and disease characteristics were evenly distributed between groups.

Conclusion

DA-using PC patients chose the AS treatment option more often than non-DA-using patients did.
Early postoperative pain as a marker of anastomotic leakage in colorectal cancer surgery
Authors: Boström Petrus , Svensson Johan , Brorsson Camilla , Rutegård Martin
Published: July 2021

Purpose

Even though anastomotic leakage after colorectal surgery is a major clinical problem in need of a timely diagnosis, early indicators of leakage have been insufficiently studied. We therefore conducted a population-based observational study to determine whether the patient’s early postoperative pain is an independent marker of anastomotic leakage.

Methods

By combining the Swedish Colorectal Cancer Registry and the Swedish Perioperative Registry, we retrieved prospectively collected data on 3084 patients who underwent anastomotic colorectal surgery for cancer in 2014–2017. Postoperative pain, measured with the numerical rating scale (NRS), was considered exposure, while anastomotic leakage and reoperation due to leakage were outcomes. We performed logistic regression to evaluate associations, estimating odds ratios (ORs) and 95% confidence intervals (CIs), while multiple imputation was used to handle missing data.

Results

In total, 189 patients suffered from anastomotic leakage, of whom 121 patients also needed a reoperation due to leakage. Moderate or severe postoperative pain (NRS 4–10) was associated with an increased risk of anastomotic leakage (OR 1.69, 95% CI 1.21–2.38), as well as reoperation (OR 2.17, 95% CI 1.41–3.32). Severe pain (NRS 8–10) was more strongly related to leakage (OR 2.38, 95% CI 1.44–3.93). These associations were confirmed in multivariable analyses and when reoperation due to leakage was used as an outcome.

Conclusion

In this population-based retrospective study on prospectively collected data, increased pain in the post-anaesthesia care unit is an independent marker of anastomotic leakage, possibly indicating a need for further diagnostic measures.
Characterizing the features and course of psychiatric symptoms in children and adolescents with autoimmune encephalitis
Authors: Rosello R , Girela-Serrano B , Gómez S , Baig B , Lim M , Taylor S
Published: July 2021

Autoimmune encephalitis (AE) can present like a psychiatric disorder. We aimed to illustrate the psychiatric manifestations, course and management of AE in a paediatric cohort. Neuropsychiatric symptoms, investigations and treatment were retrospectively retrieved in 16 patients (mean age 11.31, SD 2.98) with an AE diagnosis at the liaison psychiatry services in two UK tertiary paediatric centres. Psychiatric presentation was characterised by an acute polysymptomatic (predominantly agitation, anger outbursts/aggressiveness, hallucinations, and emotional lability) onset. Antipsychotics produced side effects and significant worsening of symptoms in four cases, and benzodiazepines were commonly used. This psychiatric phenotype should make clinicians suspect the diagnosis of AE and carefully consider use of treatments.
Reliability of the fMRI-based assessment of self-evaluation in individuals with internet gaming disorder
Authors: Bach Patrick , Hill Holger , Reinhard Iris , Gädeke Theresa , Kiefer Falk , Leménager Tagrid
Published: July 2021

The self-concept—defined as the cognitive representation of beliefs about oneself—determines how individuals view themselves, others, and their actions. A negative self-concept can drive gaming use and internet gaming disorder (IGD). The assessment of the neural correlates of self-evaluation gained popularity to assess the self-concept in individuals with IGD. This attempt, however, seems to critically depend on the reliability of the investigated task-fMRI brain activation. As first study to date, we assessed test–retest reliability of an fMRI self-evaluation task. Test–retest reliability of neural brain activation between two separate fMRI sessions (approximately 12 months apart) was investigated in N = 29 healthy participants and N = 11 individuals with pathological internet gaming. We computed reliability estimates for the different task contrasts (self, a familiar, and an unknown person) and the contrast (self > familiar and unknown person). Data indicated good test–retest reliability of brain activation, captured by the “self”, “familiar person”, and “unknown person” contrasts, in a large network of brain regions in the whole sample (N = 40) and when considering both experimental groups separately. In contrast to that, only a small set of brain regions showed moderate to good reliability, when investigating the contrasts (“self > familiar and unknown person”). The lower reliability of the contrast can be attributed to the fact that the constituting contrast conditions were highly correlated. Future research on self-evaluation should be cautioned by the findings of substantial local reliability differences across the brain and employ methods to overcome these limitations.