bluuebunny/crossref_metadata_2025 huggingface dataset:
Efficacy and safety of chimeric antigen receptor T-cell (CAR-T) therapy in patients with haematological and solid malignancies: protocol for a systematic review and meta-analysis
Authors: Grigor Emma J M , Fergusson Dean A , Haggar Fatima , Kekre Natasha , Atkins Harold , Shorr Risa , Holt Robert A , Hutton Brian , Ramsay Tim , Seftel Matthew , Jonker Derek , Daugaard Mads , Thavorn Kednapa , Presseau Justin , Lalu Manoj M
Published: December 2017

Introduction

Patients with relapsed or refractory malignancies have a poor prognosis. Immunotherapy with chimeric antigen receptor T (CAR-T) cells redirects a patient’s immune cells against the tumour antigen. CAR-T cell therapy has demonstrated promise in treating patients with several haematological malignancies, including acute B-cell lymphoblastic leukaemia and B-cell lymphomas. CAR-T cell therapy for patients with other solid tumours is also being tested. Safety is an important consideration in CAR-T cell therapy given the potential for serious adverse events, including death. Previous reviews on CAR-T cell therapy have been limited in scope and methodology. Herein, we present a protocol for a systematic review to identify CAR-T cell interventional studies and examine the safety and efficacy of this therapy in patients with haematology malignancies and solid tumours.

Methods and analysis

We will search MEDLINE, including In-Process and Epub Ahead of Print, EMBASE and the Cochrane Central Register of Controlled Trials from 1946 to 22 February 2017. Studies will be screened by title, abstract and full text independently and in duplicate. Studies that report administering CAR-T cells of any chimeric antigen receptor construct targeting antigens in patients with haematological malignancies and solid tumours will be eligible for inclusion. Outcomes to be extracted will include complete response rate (primary outcome), overall response rate, overall survival, relapse and adverse events. A meta-analysis will be performed to synthesise the prevalence of outcomes reported as proportions with 95% CIs. The potential for bias within included studies will be assessed using a modified Institute of Health Economics tool. Heterogeneity of effect sizes will be determined using the CochraneI2statistic.

Ethics and dissemination

The review findings will be submitted for peer-reviewed journal publication and presented at relevant conferences and scientific meetings to promote knowledge transfer.

PROSPERO registration number

CRD42017075331.
Feature Extraction with GMDH-Type Neural Networks for EEG-Based Person Identification
Authors: Schetinin Vitaly , Jakaite Livija , Nyah Ndifreke , Novakovic Dusica , Krzanowski Wojtek
Published: December 2017

The brain activity observed on EEG electrodes is influenced by volume conduction and functional connectivity of a person performing a task. When the task is a biometric test the EEG signals represent the unique “brain print”, which is defined by the functional connectivity that is represented by the interactions between electrodes, whilst the conduction components cause trivial correlations. Orthogonalization using autoregressive modeling minimizes the conduction components, and then the residuals are related to features correlated with the functional connectivity. However, the orthogonalization can be unreliable for high-dimensional EEG data. We have found that the dimensionality can be significantly reduced if the baselines required for estimating the residuals can be modeled by using relevant electrodes. In our approach, the required models are learnt by a Group Method of Data Handling (GMDH) algorithm which we have made capable of discovering reliable models from multidimensional EEG data. In our experiments on the EEG-MMI benchmark data which include 109 participants, the proposed method has correctly identified all the subjects and provided a statistically significant ([Formula: see text]) improvement of the identification accuracy. The experiments have shown that the proposed GMDH method can learn new features from multi-electrode EEG data, which are capable to improve the accuracy of biometric identification.
A mean-curvature flow along a Kähler–Ricci flow
Authors: Han Xiaoli , Li Jiayu , Zhao Liang
Published: December 2017

Let [Formula: see text] be a Kähler surface, and [Formula: see text] an immersed surface in [Formula: see text]. The Kähler angle of [Formula: see text] in [Formula: see text] is introduced by Chern and Wolfson [Am. J. Math. 105 (1983) 59–83]. Let [Formula: see text] evolve along the Kähler–Ricci flow, and [Formula: see text] in [Formula: see text] evolve along the mean-curvature flow. We show that the Kähler angle [Formula: see text] satisfies the evolution equation [Formula: see text] where [Formula: see text] is the scalar curvature of [Formula: see text].

The equation implies that if the initial surface is symplectic (Lagrangian), then, along the flow, [Formula: see text] is always symplectic (Lagrangian) at each time [Formula: see text], which we call a symplectic (Lagrangian) Kähler–Ricci mean-curvature flow.

In this paper, we mainly study the symplectic Kähler–Ricci mean-curvature flow.
Oseen–Frank-type theories of ordered media as the Γ-limit of a non-local mean-field free energy
Authors: Taylor Jamie M.
Published: December 2017

In this work we recover the Oseen–Frank theory of nematic liquid crystals as a [Formula: see text]-limit of a particular mean-field free energy as the sample size becomes infinitely large. The Frank constants are not necessarily all equal. Our analysis takes place in a broader framework however, also providing results for more general systems such as biaxial or polar molecules. We start from a mesoscopic model describing a competition between entropy and a non-local pairwise interaction between molecules. We assume the interaction potential is separable so that the energy can be reduced to a model involving a macroscopic order parameter. We assume only integrability and decay properties of the macroscopic interaction, but no regularity assumptions are required. In particular, singular interactions are permitted. The analysis becomes significantly simpler on a translationally invariant domain, so we first consider periodic domains with increasing domain of periodicity. Then we tackle the problem on a Lipschitz domain with non-local boundary conditions by considering an asymptotically equivalent problem on periodic domains. We conclude by applying the results to a case which reduces to the Oseen–Frank model of elasticity, and give expressions for the Frank constants in terms of integrals of the interaction kernel.
A fully divergence-free finite element method for magnetohydrodynamic equations
Authors: Hiptmair Ralf , Li Lingxiao , Mao Shipeng , Zheng Weiying
Published: December 2017

We propose a finite element method for the three-dimensional transient incompressible magnetohydrodynamic equations that ensures exactly divergence-free approximations of the velocity and the magnetic induction. We employ second-order semi-implicit timestepping, for which we rigorously establish an energy law and, as a consequence, unconditional stability. We prove unique solvability of the linear systems of equations to be solved in every timestep. For those we design an efficient preconditioner so that the number of preconditioned GMRES iterations is uniformly bounded with respect to the number of degrees of freedom. As both meshwidth and timestep size tend to zero, we prove that the discrete solutions converge to a weak solution of the continuous problem. Finally, by several numerical experiments, we confirm the predictions of the theory and demonstrate the efficiency of the preconditioner.
Diffuse-interface two-phase flow models with different densities: A new quasi-incompressible form and a linear energy-stable method
Authors: Shokrpour Roudbari M. , Şimşek G. , van Brummelen E. H. , van der Zee K. G.
Published: December 2017

While various phase-field models have recently appeared for two-phase fluids with different densities, only some are known to be thermodynamically consistent, and practical stable schemes for their numerical simulation are lacking. In this paper, we derive a new form of thermodynamically-consistent quasi-incompressible diffuse-interface Navier–Stokes–Cahn–Hilliard model for a two-phase flow of incompressible fluids with different densities. The derivation is based on mixture theory by invoking the second law of thermodynamics and Coleman–Noll procedure. We also demonstrate that our model and some of the existing models are equivalent and we provide a unification between them. In addition, we develop a linear and energy-stable time-integration scheme for the derived model. Such a linearly-implicit scheme is nontrivial, because it has to suitably deal with all nonlinear terms, in particular those involving the density. Our proposed scheme is the first linear method for quasi-incompressible two-phase flows with non-solenoidal velocity that satisfies discrete energy dissipation independent of the time-step size, provided that the mixture density remains positive. The scheme also preserves mass. Numerical experiments verify the suitability of the scheme for two-phase flow applications with high density ratios using large time steps by considering the coalescence and breakup dynamics of droplets including pinching due to gravity.
Effect of molarity on sol–gel routed nano TiO2thin films
Authors: Lourduraj Stephen , Williams Rayar Victor
Published: December 2017

The nanostructured titanium dioxide (TiO[Formula: see text] thin films have been prepared for the molar concentrations of titanium tetra isopropoxide (TTIP) 0.05[Formula: see text]M, 0.1[Formula: see text]M, 0.15[Formula: see text]M and 0.2[Formula: see text]M by sol–gel routed spin coating technique with calcination at 450[Formula: see text]C. The processing parameters such as, pH value (8), catalyst HCl (0.1[Formula: see text]ml), spin speed (3000[Formula: see text]rpm) and calcination temperature (450[Formula: see text]C) are optimized. The crystalline nature and surface morphology were analyzed by XRD, SEM and AFM analysis. The XRD results confirm that the films are crystalline with anatase phase, and are nanostructured. The SEM micrographs of the TiO2film reveal the spherical nature of the particle. AFM analysis establishes that the uniformity of the TiO2thin film was optimized at 0.2[Formula: see text]M. The optical measurements show that the transmittance depends on the molarity, and the optical band gap energy of TiO2films is found to be inversely proportional to molarity. The I–V characteristics exhibit that the molarity strongly influences the electrical conductivity of the film. The results indicate that the significant effect of molarity on structural, optical and electrical properties of the nanostructured TiO2thin films will be useful to photovoltaic application.
Asset liability management for providers in spectrum markets
Authors: de Carvalho Pablo Jose Campos , Gupta Aparna , Kar Koushik
Published: December 2017

Service provision with novel features can be made possible in a more dynamic spectrum marketplace. In this marketplace, a service provider will need to create an appropriate spectrum asset portfolio to support the services offered to its customers. Such an asset portfolio should satisfactorily meet all demand characteristics implied by the novel service features. In this paper, we address this question of optimal asset portfolio construction in an asset-liability management framework from the perspective of a mobile service provider. We find that the provider utilizes a mix of primary and secondary contracts, and uses the costlier spot contracts to fulfil the peak-time demand subject to the budget constraints. The framework allows evaluating a variety of service portfolios, with traditional and novel service mix, for their best matched asset portfolios. Niche premium service providers must also use all three contract types.
A mean bound financial model and options pricing
Authors: Li Yu
Published: December 2017

Most of financial models, including the famous Black–Scholes–Merton options pricing model, rely upon the assumption that asset returns follow a normal distribution. However, this assumption is not justified by empirical data. To be more concrete, the empirical observations exhibit fat tails or heavy tails and implied volatilities against the strike prices demonstrate U-shaped curve resembling a smile, which is the famous volatility smile. In this paper we present a mean bound financial model and show that asset returns per time unit are Pareto distributed and assets are log Gamma distributed under this model. Based on this we study the sensitivity of the options prices to a change in underlying parameters, which are commonly called the Greeks, and derive options pricing formulas. Finally, we reveal the relation between correct volatility and implied volatility in Black–Scholes model and provide a mathematical explanation of volatility smile.
WebRelate: integrating web data with spreadsheets using examples
Authors: Inala Jeevana Priya , Singh Rishabh
Published: December 2017

Data integration between web sources and relational data is a key challenge faced by data scientists and spreadsheet users. There are two main challenges in programmatically joining web data with relational data. First, most websites do not expose a direct interface to obtain tabular data, so the user needs to formulate a logic to get to different webpages for each input row in the relational table. Second, after reaching the desired webpage, the user needs to write complex scripts to extract the relevant data, which is often conditioned on the input data. Since many data scientists and end-users come from diverse backgrounds, writing such complex regular-expression based logical scripts to perform data integration tasks is unfortunately often beyond their programming expertise.

We present WebRelate, a system that allows users to join semi-structured web data with relational data in spreadsheets using input-output examples. WebRelate decomposes the web data integration task into two sub-tasks of i) URL learning and ii) input-dependent web extraction. We introduce a novel synthesis paradigm called "Output-constrained Programming By Examples", which allows us to use the finite set of possible outputs for the new inputs to efficiently constrain the search in the synthesis algorithm. We instantiate this paradigm for the two sub-tasks in WebRelate. The first sub-task generates the URLs for the webpages containing the desired data for all rows in the relational table. WebRelate achieves this by learning a string transformation program using a few example URLs. The second sub-task uses examples of desired data to be extracted from the corresponding webpages and learns a program to extract the data for the other rows. We design expressive domain-specific languages for URL generation and web data extraction, and present efficient synthesis algorithms for learning programs in these DSLs from few input-output examples. We evaluate WebRelate on 88 real-world web data integration tasks taken from online help forums and Excel product team, and show that WebRelate can learn the desired programs within few seconds using only 1 example for the majority of the tasks.
What is decidable about string constraints with the ReplaceAll function
Authors: Chen Taolue , Chen Yan , Hague Matthew , Lin Anthony W. , Wu Zhilin
Published: December 2017

The theory of strings with concatenation has been widely argued as the basis of constraint solving for verifying string-manipulating programs. However, this theory is far from adequate for expressing many string constraints that are also needed in practice; for example, the use of regular constraints (pattern matching against a regular expression), and the string-replace function (replacing either the first occurrence or all occurrences of a ``pattern'' string constant/variable/regular expression by a ``replacement'' string constant/variable), among many others. Both regular constraints and the string-replace function are crucial for such applications as analysis of JavaScript (or more generally HTML5 applications) against cross-site scripting (XSS) vulnerabilities, which motivates us to consider a richer class of string constraints. The importance of the string-replace function (especially the replace-all facility) is increasingly recognised, which can be witnessed by the incorporation of the function in the input languages of several string constraint solvers.

Recently, it was shown that any theory of strings containing the string-replace function (even the most restricted version where pattern/replacement strings are both constant strings) becomes undecidable if we do not impose some kind of straight-line (aka acyclicity) restriction on the formulas. Despite this, the straight-line restriction is still practically sensible since this condition is typically met by string constraints that are generated by symbolic execution. In this paper, we provide the first systematic study of straight-line string constraints with the string-replace function and the regular constraints as the basic operations. We show that a large class of such constraints (i.e. when only a constant string or a regular expression is permitted in the pattern) is decidable. We note that the string-replace function, even under this restriction, is sufficiently powerful for expressing the concatenation operator and much more (e.g. extensions of regular expressions with string variables). This gives us the most expressive decidable logic containing concatenation, replace, and regular constraints under the same umbrella. Our decision procedure for the straight-line fragment follows an automata-theoretic approach, and is modular in the sense that the string-replace terms are removed one by one to generate more and more regular constraints, which can then be discharged by the state-of-the-art string constraint solvers. We also show that this fragment is, in a way, a maximal decidable subclass of the straight-line fragment with string-replace and regular constraints. To this end, we show undecidability results for the following two extensions: (1) variables are permitted in the pattern parameter of the replace function, (2) length constraints are permitted.
Automated lemma synthesis in symbolic-heap separation logic
Authors: Ta Quang-Trung , Le Ton Chanh , Khoo Siau-Cheng , Chin Wei-Ngan
Published: December 2017

The symbolic-heap fragment of separation logic has been actively developed and advocated for verifying the memory-safety property of computer programs. At present, one of its biggest challenges is to effectively prove entailments containing inductive heap predicates. These entailments are usually proof obligations generated when verifying programs that manipulate complex data structures like linked lists, trees, or graphs.

To assist in proving such entailments, this paper introduces a lemma synthesis framework, which automatically discovers lemmas to serve as eureka steps in the proofs. Mathematical induction and template-based constraint solving are two pillars of our framework. To derive the supporting lemmas for a given entailment, the framework firstly identifies possible lemma templates from the entailment's heap structure. It then sets up unknown relations among each template's variables and conducts structural induction proof to generate constraints about these relations. Finally, it solves the constraints to find out actual definitions of the unknown relations, thus discovers the lemmas. We have integrated this framework into a prototype prover and have experimented it on various entailment benchmarks. The experimental results show that our lemma-synthesis-assisted prover can prove many entailments that could not be handled by existing techniques. This new proposal opens up more opportunities to automatically reason with complex inductive heap predicates.
Foundations for natural proofs and quantifier instantiation
Authors: Löding Christof , Madhusudan P. , Peña Lucas
Published: December 2017

We give foundational results that explain the efficacy of heuristics used for dealing with quantified formulas and recursive definitions. We develop a framework for first order logic (FOL) over an uninterpreted combination of background theories. Our central technical result is that systematic term instantiation is
complete
for a fragment of FOL that we call
safe
. Coupled with the fact that unfolding recursive definitions is essentially term instantiation and with the observation that heap verification engines generate verification conditions in the safe fragment explains the efficacy of verification engines like natural proofs that resort to such heuristics. Furthermore, we study recursive definitions with least fixpoint semantics and show that though they are not amenable to complete procedures, we can systematically introduce induction principles that in practice bridge the divide between FOL and FOL with recursive definitions.
Jones-optimal partial evaluation by specialization-safe normalization
Authors: Brown Matt , Palsberg Jens
Published: December 2017

We present partial evaluation by specialization-safe normalization, a novel partial evaluation technique that is Jones-optimal, that can be self-applied to achieve the Futamura projections and that can be type-checked to ensure it always generates code with the correct type. Jones-optimality is the gold-standard for nontrivial partial evaluation and guarantees that a specializer can remove an entire layer of interpretation. We achieve Jones-optimality by using a novel affine-variable static analysis that directs specialization-safe normalization to always decrease a program’s runtime.

We demonstrate the robustness of our approach by showing Jones-optimality in a variety of settings. We have formally proved that our partial evaluator is Jones-optimal for call-by-value reduction, and we have experimentally shown that it is Jones-optimal for call-by-value, normal-order, and memoized normal-order. Each of our experiments tests Jones-optimality with three different self-interpreters.

We implemented our partial evaluator in F
ω

µ
i

, a recent language for typed self-applicable meta-programming. It is the first Jones-optimal and self-applicable partial evaluator whose type guarantees that it always generates type-correct code.
Migrating gradual types
Authors: Campora John Peter , Chen Sheng , Erwig Martin , Walkingshaw Eric
Published: December 2017

Gradual typing allows programs to enjoy the benefits of both static typing and dynamic typing. While it is often desirable to migrate a program from more dynamically-typed to more statically-typed or vice versa, gradual typing itself does not provide a way to facilitate this migration. This places the burden on programmers who have to manually add or remove type annotations. Besides the general challenge of adding type annotations to dynamically typed code, there are subtle interactions between these annotations in gradually typed code that exacerbate the situation. For example, to migrate a program to be as static as possible, in general, all possible combinations of adding or removing type annotations from parameters must be tried out and compared.

In this paper, we address this problem by developing migrational typing, which efficiently types all possible ways of adding or removing type annotations from a gradually typed program. The typing result supports automatically migrating a program to be as static as possible, or introducing the least number of dynamic types necessary to remove a type error. The approach can be extended to support user-defined criteria about which annotations to modify. We have implemented migrational typing and evaluated it on large programs. The results show that migrational typing scales linearly with the size of the program and takes only 2–4 times longer than plain gradual typing.
Progress of concurrent objects with partial methods
Authors: Liang Hongjin , Feng Xinyu
Published: December 2017

Various progress properties have been proposed for concurrent objects, such as wait-freedom, lock-freedom, starvation-freedom and deadlock-freedom. However, none of them applies to concurrent objects with partial methods, i.e., methods that are supposed not to return under certain circumstances. A typical example is the lock_acquire method, which must not return when the lock has already been acquired.

In this paper we propose two new progress properties, partial starvation-freedom (PSF) and partial deadlock-freedom (PDF), for concurrent objects with partial methods. We also design four patterns to write abstract specifications for PSF or PDF objects under strongly or weakly fair scheduling, so that these objects contextually refine the abstract specifications. Our Abstraction Theorem shows the equivalence between PSF (or PDF) and the progress-aware contextual refinement. Finally, we generalize the program logic LiLi to have a new logic to verify the PSF (or PDF) property and linearizability of concurrent objects.
Decidability of conversion for type theory in type theory
Authors: Abel Andreas , Öhman Joakim , Vezzosi Andrea
Published: December 2017

Type theory should be able to handle its own meta-theory, both to justify its foundational claims and to obtain a verified implementation. At the core of a type checker for intensional type theory lies an algorithm to check equality of types, or in other words, to check whether two types are convertible. We have formalized in Agda a practical conversion checking algorithm for a dependent type theory with one universe à la Russell, natural numbers, and η-equality for Π types. We prove the algorithm correct via a Kripke logical relation parameterized by a suitable notion of equivalence of terms. We then instantiate the parameterized fundamental lemma twice: once to obtain canonicity and injectivity of type formers, and once again to prove the completeness of the algorithm. Our proof relies on inductive-recursive definitions, but not on the uniqueness of identity proofs. Thus, it is valid in variants of intensional Martin-Löf Type Theory as long as they support induction-recursion, for instance, Extensional, Observational, or Homotopy Type Theory.
Safety and conservativity of definitions in HOL and Isabelle/HOL
Authors: Kunčar Ondřej , Popescu Andrei
Published: December 2017

Definitions are traditionally considered to be a safe mechanism for introducing concepts on top of a logic known to be consistent. In contrast to arbitrary axioms, definitions should in principle be treatable as a form of abbreviation, and thus compiled away from the theory without losing provability. In particular, definitions should form a conservative extension of the pure logic. These properties are crucial for modern interactive theorem provers, since they ensure the consistency of the logic, as well as a valid environment for total/certified functional programming.

We prove these properties, namely, safety and conservativity, for Higher-Order Logic (HOL), a logic implemented in several mainstream theorem provers and relied upon by thousands of users. Some unique features of HOL, such as the requirement to give non-emptiness proofs when defining new types and the impossibility to unfold type definitions, make the proof of these properties, and also the very formulation of safety, nontrivial.

Our study also factors in the essential variation of HOL definitions featured by Isabelle/HOL, a popular member of the HOL-based provers family. The current work improves on recent results which showed a weaker property, consistency of Isabelle/HOL's definitions.
Reducing liveness to safety in first-order logic
Authors: Padon Oded , Hoenicke Jochen , Losa Giuliano , Podelski Andreas , Sagiv Mooly , Shoham Sharon
Published: December 2017

We develop a new technique for verifying temporal properties of infinite-state (distributed) systems. The main idea is to reduce the temporal verification problem to the problem of verifying the safety of infinite-state systems expressed in first-order logic. This allows to leverage existing techniques for safety verification to verify temporal properties of interesting distributed protocols, including some that have not been mechanically verified before. We model infinite-state systems using first-order logic, and use first-order temporal logic (FO-LTL) to specify temporal properties. This general formalism allows to naturally model distributed systems, while supporting both unbounded-parallelism (where the system is allowed to dynamically create processes), and infinite-state per process.

The traditional approach for verifying temporal properties of infinite-state systems employs well-founded relations (e.g. using linear arithmetic ranking functions). In contrast, our approach is based the idea of fair cycle detection. In finite-state systems, temporal verification can always be reduced to fair cycle detection (a system contains a fair cycle if it revisits a state after satisfying all fairness constraints). However, with both infinitely many states and infinitely many fairness constraints, a straightforward reduction to fair cycle detection is unsound. To regain soundness, we augment the infinite-state transition system by a dynamically computed finite set, that exploits the locality of transitions. This set lets us define a form of fair cycle detection that is sound in the presence of both infinitely many states, and infinitely many fairness constraints. Our approach allows a new style of temporal verification that does not explicitly involve ranking functions. This fits well with pure first-order verification which does not explicitly reason about numerical values. In particular, it can be used with effectively propositional first-order logic (EPR), in which case checking verification conditions is decidable. We applied our technique to verify temporal properties of several interesting protocols. To the best of our knowledge, we have obtained the first mechanized liveness proof for both TLB Shootdown, and Stoppable Paxos.
Alone together: compositional reasoning and inference for weak isolation
Authors: Kaki Gowtham , Nagar Kartik , Najafzadeh Mahsa , Jagannathan Suresh
Published: December 2017

Serializability is a well-understood correctness criterion that simplifies reasoning about the behavior of concurrent transactions by ensuring they are isolated from each other while they execute. However, enforcing serializable isolation comes at a steep cost in performance because it necessarily restricts opportunities to exploit concurrency even when such opportunities would not violate application-specific invariants. As a result, database systems in practice support, and often encourage, developers to implement transactions using weaker alternatives. These alternatives break the strong isolation guarantees offered by serializable transactions to permit greater concurrency. Unfortunately, the semantics of weak isolation is poorly understood, and usually explained only informally in terms of low-level implementation artifacts. Consequently, verifying high-level correctness properties in such environments remains a challenging problem. To address this issue, we present a novel program logic that enables compositional reasoning about the behavior of concurrently executing weakly-isolated transactions. Recognizing that the proof burden necessary to use this logic may dissuade application developers, we also describe an inference procedure based on this foundation that ascertains the weakest isolation level that still guarantees the safety of high-level consistency assertions associated with such transactions. The key to effective inference is the observation that weakly-isolated transactions can be viewed as functional (monadic) computations over an abstract database state, allowing us to treat their operations as state transformers over the database. This interpretation enables automated verification using off-the-shelf SMT solvers. Our development is parametric over a transaction’s specific isolation semantics, allowing it to be applicable over a range of concurrency control mechanisms. Case studies and experiments on real-world applications (written in an embedded DSL in OCaml) demonstrate the utility of our approach, and provide strong evidence that automated verification of weakly-isolated transactions can be placed on the same formal footing as their strongly-isolated serializable counterparts.
Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs
Authors: Agrawal Sheshansh , Chatterjee Krishnendu , Novotný Petr
Published: December 2017

Probabilistic programs extend classical imperative programs with real-valued random variables and random branching. The most basic liveness property for such programs is the termination property. The qualitative (aka almost-sure) termination problem asks whether a given program program terminates with probability 1. While ranking functions provide a sound and complete method for non-probabilistic programs, the extension of them to probabilistic programs is achieved via ranking supermartingales (RSMs). Although deep theoretical results have been established about RSMs, their application to probabilistic programs with nondeterminism has been limited only to programs of restricted control-flow structure. For non-probabilistic programs, lexicographic ranking functions provide a compositional and practical approach for termination analysis of real-world programs. In this work we introduce lexicographic RSMs and show that they present a sound method for almost-sure termination of probabilistic programs with nondeterminism. We show that lexicographic RSMs provide a tool for compositional reasoning about almost-sure termination, and for probabilistic programs with linear arithmetic they can be synthesized efficiently (in polynomial time). We also show that with additional restrictions even asymptotic bounds on expected termination time can be obtained through lexicographic RSMs. Finally, we present experimental results on benchmarks adapted from previous work to demonstrate the effectiveness of our approach.
An axiomatic basis for bidirectional programming
Authors: Ko Hsiang-Shang , Hu Zhenjiang
Published: December 2017

Among the frameworks of bidirectional transformations proposed for addressing various synchronisation (consistency maintenance) problems, Foster et al.’s [2007] asymmetric lenses have influenced the design of a generation of bidirectional programming languages. Most of these languages are based on a declarative programming model, and only allow the programmer to describe a consistency specification with ad hoc and/or awkward control over the consistency restoration behaviour. However, synchronisation problems are diverse and require vastly different consistency restoration strategies, and to cope with the diversity, the programmer must have the ability to fully control and reason about the consistency restoration behaviour. The putback-based approach to bidirectional programming aims to provide exactly this ability, and this paper strengthens the putback-based position by proposing the first fully fledged reasoning framework for a bidirectional language — a Hoare-style logic for Ko et al.’s [2016] putback-based language BiGUL. The Hoare-style logic lets the BiGUL programmer precisely characterise the bidirectional behaviour of their programs by reasoning solely in the putback direction, thereby offering a unidirectional programming abstraction that is reasonably straightforward to work with and yet provides full control not achieved by previous approaches. The theory has been formalised and checked in Agda, but this paper presents the Hoare-style logic in a semi-formal way to make it easily understood and usable by the working BiGUL programmer.
Why is random testing effective for partition tolerance bugs?
Authors: Majumdar Rupak , Niksic Filip
Published: December 2017

Random testing has proven to be an effective way to catch bugs in distributed systems in the presence of network partition faults. This is surprising, as the space of potentially faulty executions is enormous, and the bugs depend on a subtle interplay between sequences of operations and faults.

We provide a theoretical justification of the effectiveness of random testing in this context. First, we show a general construction, using the probabilistic method from combinatorics, that shows that whenever a random test covers a fixed coverage goal with sufficiently high probability, a small randomly-chosen set of tests achieves full coverage with high probability. In particular, we show that our construction can give test sets exponentially smaller than systematic enumeration. Second, based on an empirical study of many bugs found by random testing in production distributed systems, we introduce notions of test coverage relating to network partition faults which are effective in finding bugs. Finally, we show using combinatorial arguments that for these notions of test coverage we introduce, we can find a lower bound on the probability that a random test covers a given goal. Our general construction then explains why random testing tools achieve good coverage---and hence, find bugs---quickly.

While we formulate our results in terms of network partition faults, our construction provides a step towards rigorous analysis of random testing algorithms, and can be applicable in other scenarios.
On automatically proving the correctness of math.h implementations
Authors: Lee Wonyeol , Sharma Rahul , Aiken Alex
Published: December 2017

Industry standard implementations of math.h claim (often without formal proof) tight bounds on floating-point errors. We demonstrate a novel static analysis that proves these bounds and verifies the correctness of these implementations. Our key insight is a reduction of this verification task to a set of mathematical optimization problems that can be solved by off-the-shelf computer algebra systems. We use this analysis to prove the correctness of implementations in Intel's math library automatically. Prior to this work, these implementations could only be verified with significant manual effort.
Non-linear reasoning for invariant synthesis
Authors: Kincaid Zachary , Cyphert John , Breck Jason , Reps Thomas
Published: December 2017

Automatic generation of non-linear loop invariants is a long-standing challenge in program analysis, with many applications. For instance, reasoning about exponentials provides a way to find invariants of digital-filter programs, and reasoning about polynomials and/or logarithms is needed for establishing invariants that describe the time or memory usage of many well-known algorithms. An appealing approach to this challenge is to exploit the powerful recurrence-solving techniques that have been developed in the field of computer algebra, which can compute exact characterizations of non-linear repetitive behavior. However, there is a gap between the capabilities of recurrence solvers and the needs of program analysis: (1) loop bodies are not merely systems of recurrence relations---they may contain conditional branches, nested loops, non-deterministic assignments, etc., and (2) a client program analyzer must be able to reason about the closed-form solutions produced by a recurrence solver (e.g., to prove assertions).

This paper presents a method for generating non-linear invariants of general loops based on analyzing recurrence relations. The key components are an abstract domain for reasoning about non-linear arithmetic, a semantics-based method for extracting recurrence relations from loop bodies, and a recurrence solver that avoids closed forms that involve complex or irrational numbers. Our technique has been implemented in a program analyzer that can analyze general loops and mutually recursive procedures. Our experiments show that our technique shows promise for non-linear assertion-checking and resource-bound generation.
Verifying equivalence of database-driven applications
Authors: Wang Yuepeng , Dillig Isil , Lahiri Shuvendu K. , Cook William R.
Published: December 2017

This paper addresses the problem of verifying equivalence between a pair of programs that operate over databases with different schemas. This problem is particularly important in the context of web applications, which typically undergo database refactoring either for performance or maintainability reasons. While web applications should have the same externally observable behavior before and after schema migration, there are no existing tools for proving equivalence of such programs. This paper takes a first step towards solving this problem by formalizing the equivalence and refinement checking problems for database-driven applications. We also propose a proof methodology based on the notion of bisimulation invariants over relational algebra with updates and describe a technique for synthesizing such bisimulation invariants. We have implemented the proposed technique in a tool called Mediator for verifying equivalence between database-driven applications written in our intermediate language and evaluate our tool on 21 benchmarks extracted from textbooks and real-world web applications. Our results show that the proposed methodology can successfully verify 20 of these benchmarks.
Proving expected sensitivity of probabilistic programs
Authors: Barthe Gilles , Espitau Thomas , Grégoire Benjamin , Hsu Justin , Strub Pierre-Yves
Published: December 2017

Program sensitivity, also known as Lipschitz continuity, describes how small changes in a program’s input lead to bounded changes in the output. We propose an average notion of program sensitivity for probabilistic programs—expected sensitivity—that averages a distance function over a probabilistic coupling of two output distributions from two similar inputs. By varying the distance, expected sensitivity recovers useful notions of probabilistic function sensitivity, including stability of machine learning algorithms and convergence of Markov chains.

Furthermore, expected sensitivity satisfies clean compositional properties and is amenable to formal verification. We develop a relational program logic called EpRHL for proving expected sensitivity properties. Our logic features two key ideas. First, relational pre-conditions and post-conditions are expressed using distances, a real-valued generalization of typical boolean-valued (relational) assertions. Second, judgments are interpreted in terms of expectation coupling, a novel, quantitative generalization of probabilistic couplings which supports compositional reasoning.

We demonstrate our logic on examples beyond the reach of prior relational logics. Our main example formalizes uniform stability of the stochastic gradient method. Furthermore, we prove rapid mixing for a probabilistic model of population dynamics. We also extend our logic with a transitivity principle for expectation couplings to capture the path coupling proof technique by Bubley and Dyer, and formalize rapid mixing of the Glauber dynamics from statistical physics.
Bonsai: synthesis-based reasoning for type systems
Authors: Chandra Kartik , Bodik Rastislav
Published: December 2017

When designing a type system, we may want to mechanically check the design to guide its further development. We describe algorithms that perform symbolic reasoning about executable models of type systems. The algorithms support three queries. First, they check type soundness and synthesize a counterexample program if such a soundness bug is found. Second, they compare two versions of a type system, synthesizing a program accepted by one but rejected by the other. Third, they minimize the size of synthesized counterexample programs.

These algorithms symbolically evaluate typecheckers and interpreters, producing formulas that characterize the set of programs that fail or succeed in the typechecker and the interpreter. However, symbolically evaluating interpreters poses efficiency challenges, which are caused by having to merge execution paths of the various possible input programs. Our main contribution is the
bonsai tree
, a novel symbolic representation of programs and program states that addresses these challenges. Bonsai trees encode complex syntactic information in terms of logical constraints, enabling more efficient merging.

We implement these algorithms in the Bonsai tool, an assistant for type system designers. We perform case studies on how Bonsai helps test and explore a variety of type systems. Bonsai efficiently synthesizes counterexamples for soundness bugs previously inaccessible to automatic tools and is the first automated tool to find a counterexample for the recently discovered Scala soundness bug SI-9633.
Recalling a witness: foundations and applications of monotonic state
Authors: Ahman Danel , Fournet Cédric , Hriţcu Cătălin , Maillard Kenji , Rastogi Aseem , Swamy Nikhil
Published: December 2017

We provide a way to ease the verification of programs whose state evolves monotonically. The main idea is that a property
witnessed
in a prior state can be soundly
recalled
in the current state, provided (1) state evolves according to a given preorder, and (2) the property is preserved by this preorder. In many scenarios, such monotonic reasoning yields concise modular proofs, saving the need for explicit program invariants. We distill our approach into the
monotonic-state monad
, a general yet compact interface for Hoare-style reasoning about monotonic state in a dependently typed language. We prove the soundness of the monotonic-state monad and use it as a unified foundation for reasoning about monotonic state in the F
⋆
verification system. Based on this foundation, we build libraries for various mutable data structures like monotonic references and apply these libraries at scale to the verification of several distributed applications.
ПЕРСПЕКТИВИ ПОКРАЩАННЯ ЕФЕКТИВНОСТІ ЛІКУВАННЯ У ХВОРИХ НА МУЛЬТИРЕЗИСТЕНТНИЙ ТУБЕРКУЛЬОЗ: СВІТОВІ ТЕНДЕНЦІЇ ТА ВІТЧИЗНЯНІ ДОСЯГНЕННЯ
Authors: Feshchenko Yu. I. , Lytvynenko N. A. , Varytska H. O. , Chobotar O. P. , Pohrebna M. V. , Senko Yu. O. , Davydenko V. V. , Shcherbakova L. V. , Hrankina N.
Published: December 2017

Мета роботи – вивчити ефективність лікування хворих на мультирезистентний туберкульоз (МРТБ) та туберкульоз із розширеною резистентністю (РРТБ) у разі застосування стандартних підходів до формування режиму антимікобактерійної терапії та представити перші результати щодо ефективності адаптованих до України скорочених 12-місячних режимів антимікобактерійної терапії із включенням лінезоліду.Матеріали і методи. Загалом дизайн роботи включав декілька видів досліджень. У ретроспективному когортному дослідженні вивчали ефективність лікування серед 1038 хворих на МРТБ та РРТБ за період з 2006 по 2015 рр. У проспективному клінічному дослідженні випадок-контроль вивчали ефективність скорочених 12-місячних режимів антимікобактерійної терапії (АМБТ) серед 150 хворих на нові випадки МРТБ, у тому числі з резистентністю до фторхінолонів або аміноглікозидів/поліпептидів (пре-РРТБ) за період з 2015 по 2016 рр. Скорочені 12-місячні режими АМБТ для хворих на МРТБ та пре-РРТБ включали мінімум 6 ефективних ПТП: піразинамід, канаміцин/капреоміцин, левофлоксацин/моксифлоксацин, протіонамід, циклосерин, лінезолід та високі дози ізоніазиду.