bluuebunny/crossref_metadata_2025 huggingface dataset:
Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8
Authors: Pulte Christopher , Flur Shaked , Deacon Will , French Jon , Sarkar Susmit , Sewell Peter
Published: December 2017

ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8. Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified by the potential benefits. In particular, the model was originally
non-multicopy-atomic
: writes could become visible to some other threads before becoming visible to all — but this has not been exploited in production implementations, the corresponding potential hardware optimisations are thought to have insufficient benefits in the ARM context, and it gives rise to subtle complications when combined with other ARMv8 features. The ARMv8 architecture has therefore been revised: it now has a multicopy-atomic model. It has also been simplified in other respects, including more straightforward notions of dependency, and the architecture now includes a formal concurrency model.

In this paper we detail these changes and discuss their motivation. We define two formal concurrency models: an operational one, simplifying the Flowing model of Flur et al., and the axiomatic model of the revised ARMv8 specification. The models were developed by an academic group and by ARM staff, respectively, and this extended collaboration partly motivated the above changes. We prove the equivalence of the two models. The operational model is integrated into an executable exploration tool with new web interface, demonstrated by exhaustively checking the possible behaviours of a loop-unrolled version of a Linux kernel lock implementation, a previously known bug due to unprevented speculation, and a fixed version.
A principled approach to ornamentation in ML
Authors: Williams Thomas , Rémy Didier
Published: December 2017

Ornaments are a way to describe changes in datatype definitions reorganizing, adding, or dropping some pieces of data so that functions operating on the bare definition can be partially and sometimes totally lifted into functions operating on the ornamented structure. We propose an extension of ML with higher-order ornaments, demonstrate its expressiveness with a few typical examples, including code refactoring, study the metatheoretical properties of ornaments, and describe their elaboration process. We formalize ornamentation via an a posteriori abstraction of the bare code, returning a generic term, which lives in a meta-language above ML. The lifted code is obtained by application of the generic term to well-chosen arguments, followed by staged reduction, and some remaining simplifications. We use logical relations to closely relate the lifted code to the bare code.
Sound, complete, and tractable linearizability monitoring for concurrent collections
Authors: Emmi Michael , Enea Constantin
Published: December 2017

While many program properties like the validity of assertions and in-bounds array accesses admit nearly-trivial monitoring algorithms, the standard correctness criterion for concurrent data structures does not. Given an implementation of an arbitrary abstract data type, checking whether the operations invoked in one single concurrent execution are linearizable, i.e., indistinguishable from an execution where the same operations are invoked atomically, requires exponential time in the number of operations.

In this work we identify a class of collection abstract data types which admit polynomial-time linearizability monitors. Collections capture the majority of concurrent data structures available in practice, including stacks, queues, sets, and maps. Although monitoring executions of arbitrary abstract data types requires enumerating exponentially-many possible linearizations, collections enjoy combinatorial properties which avoid the enumeration. We leverage these properties to reduce linearizability to Horn satisfiability. As far as we know, ours is the first sound, complete, and tractable algorithm for monitoring linearizability for types beyond single-value registers.
Programming and proving with distributed protocols
Authors: Sergey Ilya , Wilcox James R. , Tatlock Zachary
Published: December 2017

Distributed systems play a crucial role in modern infrastructure, but are notoriously difficult to implement correctly. This difficulty arises from two main challenges: (a) correctly implementing core system components (e.g., two-phase commit), so all their internal invariants hold, and (b) correctly composing standalone system components into functioning trustworthy applications (e.g., persistent storage built on top of a two-phase commit instance). Recent work has developed several approaches for addressing (a) by means of mechanically verifying implementations of core distributed components, but no methodology exists to address (b) by composing such verified components into larger verified applications. As a result, expensive verification efforts for key system components are not easily reusable, which hinders further verification efforts.

In this paper, we present Disel, the first framework for implementation and compositional verification of distributed systems and their clients, all within the mechanized, foundational context of the Coq proof assistant. In Disel, users implement distributed systems using a domain specific language shallowly embedded in Coq and providing both high-level programming constructs as well as low-level communication primitives. Components of composite systems are specified in Disel as protocols, which capture system-specific logic and disentangle system definitions from implementation details. By virtue of Disel's dependent type system, well-typed implementations always satisfy their protocols' invariants and never go wrong, allowing users to verify system implementations interactively using Disel's Hoare-style program logic, which extends state-of-the-art techniques for concurrency verification to the distributed setting. By virtue of the substitution principle and frame rule provided by Disel's logic, system components can be composed leading to modular, reusable verified distributed systems.

We describe Disel, illustrate its use with a series of examples, outline its logic and metatheory, and report on our experience using it as a framework for implementing, specifying, and verifying distributed systems.
Optimal Dyck reachability for data-dependence and alias analysis
Authors: Chatterjee Krishnendu , Choudhary Bhavya , Pavlogiannis Andreas
Published: December 2017

A fundamental algorithmic problem at the heart of static analysis is Dyck reachability. The input is a graph where the edges are labeled with different types of opening and closing parentheses, and the reachability information is computed via paths whose parentheses are properly matched. We present new results for Dyck reachability problems with applications to alias analysis and data-dependence analysis. Our main contributions, that include improved upper bounds as well as lower bounds that establish optimality guarantees, are as follows:

First, we consider Dyck reachability on bidirected graphs, which is the standard way of performing field-sensitive points-to analysis. Given a bidirected graph with
n
nodes and
m
edges, we present: (i) an algorithm with worst-case running time
O
(
m
+
n
· α(
n
)), where α(
n
) is the inverse Ackermann function, improving the previously known
O
(
n
2
) time bound; (ii) a matching lower bound that shows that our algorithm is optimal wrt to worst-case complexity; and (iii) an optimal average-case upper bound of
O
(
m
) time, improving the previously known
O
(
m
· log
n
) bound.

Second, we consider the problem of context-sensitive data-dependence analysis, where the task is to obtain analysis summaries of library code in the presence of callbacks. Our algorithm preprocesses libraries in almost linear time, after which the contribution of the library in the complexity of the client analysis is only linear, and only wrt the number of call sites.

Third, we prove that combinatorial algorithms for Dyck reachability on general graphs with truly sub-cubic bounds cannot be obtained without obtaining sub-cubic combinatorial algorithms for Boolean Matrix Multiplication, which is a long-standing open problem. Thus we establish that the existing combinatorial algorithms for Dyck reachability are (conditionally) optimal for general graphs. We also show that the same hardness holds for graphs of constant treewidth.

Finally, we provide a prototype implementation of our algorithms for both alias analysis and data-dependence analysis. Our experimental evaluation demonstrates that the new algorithms significantly outperform all existing methods on the two problems, over real-world benchmarks.
Data-centric dynamic partial order reduction
Authors: Chalupa Marek , Chatterjee Krishnendu , Pavlogiannis Andreas , Sinha Nishant , Vaidya Kapil
Published: December 2017

We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited states (aka
stateless
exploration). As the number of distinct traces grows exponentially, dynamic partial-order reduction (DPOR) techniques have been successfully used to partition the space of traces into equivalence classes (
Mazurkiewicz
partitioning), with the goal of exploring only few representative traces from each class.

We introduce a new equivalence on traces under sequential consistency semantics, which we call the
observation
equivalence. Two traces are observationally equivalent if every read event observes the same write event in both traces. While the traditional Mazurkiewicz equivalence is control-centric, our new definition is data-centric. We show that our observation equivalence is coarser than the Mazurkiewicz equivalence, and in many cases even exponentially coarser. We devise a DPOR exploration of the trace space, called
data-centric
DPOR, based on the observation equivalence.

For acyclic architectures, our algorithm is guaranteed to explore
exactly
one representative trace from each observation class, while spending polynomial time per class. Hence, our algorithm is
optimal
wrt the observation equivalence, and in several cases explores exponentially fewer traces than
any
enumerative method based on the Mazurkiewicz equivalence.

For cyclic architectures, we consider an equivalence between traces which is finer than the observation equivalence; but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence.

Finally, we perform a basic experimental comparison between the existing Mazurkiewicz-based DPOR and our data-centric DPOR on a set of academic benchmarks. Our results show a significant reduction in both running time and the number of explored equivalence classes.
Analytical modeling of cache behavior for affine programs
Authors: Bao Wenlei , Krishnamoorthy Sriram , Pouchet Louis-Noel , Sadayappan P.
Published: December 2017

Optimizing compilers implement program transformation strategies aimed at reducing data movement to or from main memory by exploiting the data-cache hierarchy. However, instead of attempting to minimize the number of cache misses, very approximate cost models are used, due to the lack of precise compile-time models for misses for hierarchical caches. The current state of practice for cache miss analysis is based on accurate simulation. However, simulation requires time proportional to the dataset/problem size, as well as the number of distinct cache configurations of interest to be evaluated.

This paper takes a fundamentally different approach, by focusing on polyhedral programs with static control flow. Instead of relying on costly simulation, a closed-form solution for modeling of misses in a set associative cache hierarchy is developed. This solution can enable program transformation choice at compile time to optimize cache misses. A tool implementing the approach has been developed and used for validation of the framework.
A new proof rule for almost-sure termination
Authors: McIver Annabelle , Morgan Carroll , Kaminski Benjamin Lucien , Katoen Joost-Pieter
Published: December 2017

We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism.

An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates "almost surely". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice.

Like others, we use variant functions (a.k.a. "super-martingales") that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains.
Parametricity versus the universal type
Authors: Devriese Dominique , Patrignani Marco , Piessens Frank
Published: December 2017

There has long been speculation in the scientific literature on how to dynamically enforce parametricity such as that yielded by System F. Almost 20 years ago, Sumii and Pierce proposed a formal compiler from System F into the cryptographic lambda calculus: an untyped lambda calculus extended with an idealised model of encryption. They conjectured that this compiler was fully abstract, i.e. that compiled terms are contextually equivalent if and only if the original terms were, a property that can be seen as a form of secure compilation. The conjecture has received attention in several other publications since then, but remains open to this day.

More recently, several researchers have been looking at gradually-typed languages that extend System F. In this setting it is natural to wonder whether embedding System F into these gradually-typed languages preserves contextual equivalence and thus parametricity.

In this paper, we answer both questions negatively. We provide a concrete counterexample: two System F terms whose contextual equivalence is not preserved by the Sumii-Pierce compiler, nor the embedding into the polymorphic blame calculus. This counterexample relies on the absence in System F of what we call a universal type, i.e., a type that all other types can be injected into and extracted from. As the languages in which System F is compiled have a universal type, the compilation cannot be fully abstract; this paper explains why.

We believe this paper thus sheds light on recent results in the field of gradually typed languages and it provides a perspective for further research into secure compilation of polymorphic languages.
Univalent higher categories via complete Semi-Segal types
Authors: Capriotti Paolo , Kraus Nicolai
Published: December 2017

Category theory in homotopy type theory is intricate as categorical laws can only be stated "up to homotopy", and thus require coherences. The established notion of a
univalent category
(as introduced by Ahrens et al.) solves this by considering only truncated types, roughly corresponding to an ordinary category. This fails to capture many naturally occurring structures, stemming from the fact that the naturally occurring structures in homotopy type theory are not ordinary, but rather
higher
categories.

Out of the large variety of approaches to higher category theory that mathematicians have proposed, we believe that, for type theory, the
simplicial
strategy is best suited. Work by Lurie and Harpaz motivates the following definition. Given the first (
n
+3) levels of a semisimplicial type
S
, we can equip
S
with three properties: first, contractibility of the types of certain horn fillers; second, a completeness property; and third, a truncation condition. We call this a
complete semi-Segal
n
-type
. This is very similar to an earlier suggestion by Schreiber.

The definition of a univalent (1-) category by Ahrens et al. can easily be extended or restricted to the definition of a
univalent
n
-category
(more precisely, (
n
,1)-category) for
n
∈ {0,1,2}, and we show that the type of complete semi-Segal
n
-types is equivalent to the type of univalent
n
-categories in these cases. Thus, we believe that the notion of a complete semi-Segal
n
-type can be taken as the definition of a univalent
n
-category.

We provide a formalisation in the proof assistant Agda using a completely explicit representation of semi-simplicial types for levels up to 4.
Generating good generators for inductive relations
Authors: Lampropoulos Leonidas , Paraskevopoulou Zoe , Pierce Benjamin C.
Published: December 2017

Property-based random testing (PBRT) is widely used in the functional programming and verification communities. For testing simple properties, PBRT tools such as QuickCheck can automatically generate random inputs of a given type. But for more complex properties, effective testing often demands generators for random inputs that belong to a given type and satisfy some logical condition. QuickCheck provides a library of combinators for building such generators by hand, but this can be tedious for simple conditions and error prone for more complex ones. Fortunately, the process can often be automated. The most prominent method, narrowing, works by traversing the structure of the condition, lazily instantiating parts of the data structure as constraints involving them are met.

We show how to use ideas from narrowing to compile a large subclass of Coq's inductive relations into efficient generators, avoiding the interpretive overhead of previous implementations. More importantly, the same compilation technique allows us to produce proof terms certifying that each derived generator is good---i.e., sound and complete with respect to the inductive relation it was derived from. We implement our algorithm as an extension of QuickChick, an existing tool for property-based testing in Coq. We evaluate our method by automatically deriving good generators for the majority of the specifications in Software Foundations, a formalized textbook on programming language foundations.
Online detection of effectively callback free objects with applications to smart contracts
Authors: Grossman Shelly , Abraham Ittai , Golan-Gueta Guy , Michalevsky Yan , Rinetzky Noam , Sagiv Mooly , Zohar Yoni
Published: December 2017

Callbacks are essential in many programming environments, but drastically complicate program understanding and reasoning because they allow to mutate object's local states by external objects in unexpected fashions, thus breaking modularity. The famous DAO bug in the cryptocurrency framework Ethereum, employed callbacks to steal $150M. We define the notion of Effectively Callback Free (ECF) objects in order to allow callbacks without preventing modular reasoning.

An object is ECF in a given execution trace if there exists an equivalent execution trace without callbacks to this object. An object is ECF if it is ECF in every possible execution trace. We study the decidability of dynamically checking ECF in a given execution trace and statically checking if an object is ECF. We also show that dynamically checking ECF in Ethereum is feasible and can be done online. By running the history of all execution traces in Ethereum, we were able to verify that virtually all existing contract executions, excluding these of the DAO or of contracts with similar known vulnerabilities, are ECF. Finally, we show that ECF, whether it is verified dynamically or statically, enables modular reasoning about objects with encapsulated state.
Correctness of speculative optimizations with dynamic deoptimization
Authors: Flückiger Olivier , Scherer Gabriel , Yee Ming-Ho , Goel Aviral , Ahmed Amal , Vitek Jan
Published: December 2017

High-performance dynamic language implementations make heavy use of speculative optimizations to achieve speeds close to statically compiled languages. These optimizations are typically performed by a just-in-time compiler that generates code under a set of assumptions about the state of the program and its environment. In certain cases, a program may execute code compiled under assumptions that are no longer valid. The implementation must then deoptimize the program on-the-fly; this entails finding semantically equivalent code that does not rely on invalid assumptions, translating program state to that expected by the target code, and transferring control. This paper looks at the interaction between optimization and deoptimization, and shows that reasoning about speculation is surprisingly easy when assumptions are made explicit in the program representation. This insight is demonstrated on a compiler intermediate representation, named sourir, modeled after the high-level representation for a dynamic language. Traditional compiler optimizations such as constant folding, unreachable code elimination, and function inlining are shown to be correct in the presence of assumptions. Furthermore, the paper establishes the correctness of compiler transformations specific to deoptimization: namely unrestricted deoptimization, predicate hoisting, and assume composition.
Soft contract verification for higher-order stateful programs
Authors: Nguyễn Phúc C. , Gilray Thomas , Tobin-Hochstadt Sam , Van Horn David
Published: December 2017

Software contracts allow programmers to state rich program properties using the full expressive power of an object language. However, since they are enforced at runtime, monitoring contracts imposes significant overhead and delays error discovery. So contract veri cation aims to guarantee all or most of these properties ahead of time, enabling valuable optimizations and yielding a more general assurance of correctness. Existing methods for static contract verification satisfy the needs of more restricted target languages, but fail to address the challenges unique to those conjoining untyped, dynamic programming, higher-order functions, modularity, and statefulness. Our approach tackles all these features at once, in the context of the full Racket system—a mature environment for stateful, higher-order, multi-paradigm programming with or with- out types. Evaluating our method using a set of both pure and stateful benchmarks, we are able to verify 99.94% of checks statically (all but 28 of 49, 861).

Stateful, higher-order functions pose significant challenges for static contract verification in particular. In the presence of these features, a modular analysis must permit code from the current module to escape permanently to an opaque context (unspecified code from outside the current module) that may be stateful and therefore store a reference to the escaped closure. Also, contracts themselves, being predicates wri en in unrestricted Racket, may exhibit stateful behavior; a sound approach must be robust to contracts which are arbitrarily expressive and interwoven with the code they monitor. In this paper, we present and evaluate our solution based on higher-order symbolic execution, explain the techniques we used to address such thorny issues, formalize a notion of behavioral approximation, and use it to provide a mechanized proof of soundness.
Collapsing towers of interpreters
Authors: Amin Nada , Rompf Tiark
Published: December 2017

Given a tower of interpreters, i.e., a sequence of multiple interpreters interpreting one another as input programs, we aim to collapse this tower into a compiler that removes all interpretive overhead and runs in a single pass. In the real world, a use case might be Python code executed by an x86 runtime, on a CPU emulated in a JavaScript VM, running on an ARM CPU. Collapsing such a tower can not only exponentially improve runtime performance, but also enable the use of base-language tools for interpreted programs, e.g., for analysis and verification. In this paper, we lay the foundations in an idealized but realistic setting.

We present a multi-level lambda calculus that features staging constructs and stage polymorphism: based on runtime parameters, an evaluator either executes source code (thereby acting as an interpreter) or generates code (thereby acting as a compiler). We identify stage polymorphism, a programming model from the domain of high-performance program generators, as the key mechanism to make such interpreters compose in a collapsible way.

We present Pink, a meta-circular Lisp-like evaluator on top of this calculus, and demonstrate that we can collapse arbitrarily many levels of self-interpretation, including levels with semantic modifications. We discuss several examples: compiling regular expressions through an interpreter to base code, building program transformers from modi ed interpreters, and others. We develop these ideas further to include reflection and reification, culminating in Purple, a reflective language inspired by Brown, Blond, and Black, which realizes a conceptually infinite tower, where every aspect of the semantics can change dynamically. Addressing an open challenge, we show how user programs can be compiled and recompiled under user-modified semantics.
Refinement reflection: complete verification with SMT
Authors: Vazou Niki , Tondwalkar Anish , Choudhury Vikraman , Scott Ryan G. , Newton Ryan R. , Wadler Philip , Jhala Ranjit
Published: December 2017

We introduce
Refinement Reflection
, a new framework for building SMT-based deductive verifiers. The key idea is to reflect the code implementing a user-defined function into the function’s (output) refinement type. As a consequence, at
uses
of the function, the function definition is instantiated in the SMT logic in a precise fashion that permits decidable verification. Reflection allows the user to write
equational proofs
of programs just by writing other programs using pattern-matching and recursion to perform case-splitting and induction. Thus, via the propositions-as-types principle, we show that reflection permits the
specification
of arbitrary functional correctness properties. Finally, we introduce a proof-search algorithm called
Proof by Logical Evaluation
that uses techniques from model checking and abstract interpretation, to completely automate equational reasoning. We have implemented reflection in Liquid Haskell and used it to verify that the widely used instances of the Monoid, Applicative, Functor, and Monad typeclasses actually satisfy key algebraic laws required to make the clients safe, and have used reflection to build the first library that actually verifies assumptions about associativity and ordering that are crucial for safe deterministic parallelism.
Denotational validation of higher-order Bayesian inference
Authors: Ścibior Adam , Kammar Ohad , Vákár Matthijs , Staton Sam , Yang Hongseok , Cai Yufei , Ostermann Klaus , Moss Sean K. , Heunen Chris , Ghahramani Zoubin
Published: December 2017

We present a modular semantic account of Bayesian inference algorithms for probabilistic programming languages, as used in data science and machine learning. Sophisticated inference algorithms are often explained in terms of composition of smaller parts. However, neither their theoretical justification nor their implementation reflects this modularity. We show how to conceptualise and analyse such inference algorithms as manipulating intermediate representations of probabilistic programs using higher-order functions and inductive types, and their denotational semantics.

Semantic accounts of continuous distributions use measurable spaces. However, our use of higher-order functions presents a substantial technical difficulty: it is impossible to define a measurable space structure over the collection of measurable functions between arbitrary measurable spaces that is compatible with standard operations on those functions, such as function application. We overcome this difficulty using quasi-Borel spaces, a recently proposed mathematical structure that supports both function spaces and continuous distributions.

We define a class of semantic structures for representing probabilistic programs, and semantic validity criteria for transformations of these representations in terms of distribution preservation. We develop a collection of building blocks for composing representations. We use these building blocks to validate common inference algorithms such as Sequential Monte Carlo and Markov Chain Monte Carlo. To emphasize the connection between the semantic manipulation and its traditional measure theoretic origins, we use Kock's synthetic measure theory. We demonstrate its usefulness by proving a quasi-Borel counterpart to the Metropolis-Hastings-Green theorem.
A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST
Authors: Timany Amin , Stefanesco Léo , Krogh-Jespersen Morten , Birkedal Lars
Published: December 2017

We present a logical relations model of a higher-order functional programming language with impredicative polymorphism, recursive types, and a Haskell-style ST monad type with runST. We use our logical relations model to show that runST provides proper encapsulation of state, by showing that effectful computations encapsulated by runST are heap independent. Furthermore, we show that contextual refinements and equivalences that are expected to hold for pure computations do indeed hold in the presence of runST. This is the first time such relational results have been proven for a language with monadic encapsulation of state. We have formalized all the technical development and results in Coq.
Intermediary metabolism and fatty acid oxidation: novel targets of electron transport chain-driven injury during ischemia and reperfusion
Authors: Chen Qun , Younus Masood , Thompson Jeremy , Hu Ying , Hollander John M. , Lesnefsky Edward J.
Published: December 2017

Cardiac ischemia-reperfusion (I/R) damages the electron transport chain (ETC), causing mitochondrial and cardiomyocyte injury. Reversible blockade of the ETC at complex I during ischemia protects the ETC and decreases cardiac injury. In the present study, we used an unbiased proteomic approach to analyze the extent of ETC-driven mitochondrial injury during I/R. Isolated-perfused mouse (C57BL/6) hearts underwent 25-min global ischemia (37°C) and 30-min reperfusion. In treated hearts, amobarbital (2 mM) was given for 1 min before ischemia to rapidly and reversibly block the ETC at complex I. Mitochondria were isolated at the end of reperfusion and subjected to unbiased proteomic analysis using tryptic digestion followed by liquid chromatography-mass spectrometry with isotope tags for relative and absolute quantification. Amobarbital treatment decreased cardiac injury and protected respiration. I/R decreased the content ( P < 0.05) of multiple mitochondrial matrix enzymes involved in intermediary metabolism compared with the time control. The contents of several enzymes in fatty acid oxidation were decreased compared with the time control. Blockade of ETC during ischemia largely prevented the decreases. Thus, after I/R, not only the ETC but also multiple pathways of intermediary metabolism sustain damage initiated by the ETC. If these damaged mitochondria persist in the myocyte, they remain a potent stimulus for ongoing injury and the transition to cardiomyopathy during prolonged reperfusion. Modulation of ETC function during early reperfusion is a key strategy to preserve mitochondrial metabolism and to decrease persistent mitochondria-driven injury during longer periods of reperfusion that predispose to ventricular dysfunction and heart failure.

NEW & NOTEWORTHY Ischemia-reperfusion (I/R) damages mitochondria, which could be protected by reversible blockade of the electron transport chain (ETC). Unbiased proteomics with isotope tags for relative and absolute quantification analyzed mitochondrial damage during I/R and found that multiple enzymes in the tricarboxylic acid cycle, fatty acid oxidation, and ETC decreased, which could be prevented by ETC blockade. Strategic ETC modulation can reduce mitochondrial damage and cardiac injury.
RING-Finger Protein 6 Amplification Activates JAK/STAT3 Pathway by Modifying SHP-1 Ubiquitylation and Associates with Poor Outcome in Colorectal Cancer
Authors: Liang Qian , Ma Dan , Zhu Xiaoqiang , Wang Zhenhua , Sun Tian-Tian , Shen Chaoqin , Yan Tingting , Tian Xianglong , Yu TaChung , Guo Fangfang , Tang JiaYin , Lin Yanwei , Chen Huimin , Zhou Chao , Ge Zhizheng , Zhong Ming , Chen Jinxian , Liu Qiang , Wang Zheng , Fang Jing-Yuan , Chen Haoyan , Hong Jie
Published: December 2017

Objective: The E3 ubiquitin ligase RNF6 (RING-finger protein 6) plays a crucial role in carcinogenesis. However, the copy number and expression of RNF6 were rarely reported in colorectal cancer. We aimed to explore the mechanical, biological, and clinical role of RNF6 in colorectal cancer initiation and progression.

Design: The copy number and expression of RNF6 were analyzed from Tumorscape and The Cancer Genome Atlas (TCGA) datasets. Gene expressions were examined by real-time PCR, Western blot, and immunohistochemical staining. Gene expression profiling studies were performed to identify pivotal genes regulated by RNF6. Biological function of RNF6 on tumor growth and metastasis was detected in vivo and in vitro. Role of RNF6 in modulating SHP-1 expression was examined by coimmunoprecipitation and confocal microscopy, respectively.

Results: The copy number of RNF6 was significantly amplified in colorectal cancer, and the amplification was associated with RNF6 expression level. Amplification and overexpression of RNF6 positively correlated with patients with colorectal cancer with poor prognosis. The gene set enrichment analysis (GSEA) revealed cell proliferation, and invasion-related genes were enriched in RNF6 high-expressed colorectal cancer cells as well as in patients from TCGA dataset. Downregulation of RNF6 impaired the colorectal cancer cell proliferation and invasion in vitro and in vivo. RNF6 may activate the JAK/STAT3 pathway and increase pSTAT3 levels by inducing the ubiquitination and degradation of SHP-1.

Conclusions: Genomic amplification drives RNF6 overexpression in colorectal cancer. RNF6 may be a novel biomarker in colorectal carcinogenesis, and RNF6 may increase pSTAT3 level via promoting SHP-1 ubiquitylation and degradation. Targeting the RNF6/SHP-1/STAT3 axis provides a potential therapeutic option for RNF6-amplified tumors. Clin Cancer Res; 24(6); 1473–85. ©2017 AACR.
COX-2/sEH Dual Inhibitor PTUPB Potentiates the Antitumor Efficacy of Cisplatin
Authors: Wang Fuli , Zhang Hongyong , Ma Ai-Hong , Yu Weimin , Zimmermann Maike , Yang Jun , Hwang Sung Hee , Zhu Daniel , Lin Tzu-yin , Malfatti Michael , Turteltaub Kenneth W. , Henderson Paul T. , Airhart Susan , Hammock Bruce D. , Yuan Jianlin , de Vere White Ralph W. , Pan Chong-Xian
Published: December 2017

Cisplatin-based therapy is highly toxic, but moderately effective in most cancers. Concurrent inhibition of cyclooxygenase-2 (COX-2) and soluble epoxide hydrolase (sEH) results in antitumor activity and has organ-protective effects. The goal of this study was to determine the antitumor activity of PTUPB, an orally bioavailable COX-2/sEH dual inhibitor, in combination with cisplatin and gemcitabine (GC) therapy. NSG mice bearing bladder cancer patient-derived xenografts were treated with vehicle, PTUPB, cisplatin, GC, or combinations thereof. Mouse experiments were performed with two different PDX models. PTUPB potentiated cisplatin and GC therapy, resulting in significantly reduced tumor growth and prolonged survival. PTUPB plus cisplatin was no more toxic than cisplatin single-agent treatment as assessed by body weight, histochemical staining of major organs, blood counts, and chemistry. The combination of PTUPB and cisplatin increased apoptosis and decreased phosphorylation in the MAPK/ERK and PI3K/AKT/mTOR pathways compared with controls. PTUPB treatment did not alter platinum–DNA adduct levels, which is the most critical step in platinum-induced cell death. The in vitro study using the combination index method showed modest synergy between PTUPB and platinum agents only in 5637 cell line among several cell lines examined. However, PTUPB is very active in vivo by inhibiting angiogenesis. In conclusion, PTUPB potentiated the antitumor activity of cisplatin-based treatment without increasing toxicity in vivo and has potential for further development as a combination chemotherapy partner. Mol Cancer Ther; 17(2); 474–83. ©2017 AACR.
НАУКОВІ ФОРУМИ ВСЕУКРАЇНСЬКОЇ АСОЦІАЦІЇ ІНФЕКЦІОНІСТІВ У 2017 РОЦІ
Authors: Ivakhiv O. L.
Published: December 2017

Коротко описаний хід всеукраїнських науково-практичних конференцій інфекціоністів на тему «Медична допомога інфекційним хворим в умовах реформування галузі охорони здоров’я», яка відбулася 18-19 травня ц. р. в Умані (Черкаська обл.), а також «Епідеміологічні та клінічні ускладнення інфекційних і паразитарних хвороб у сучасних умовах», яка проходила 5-6 жовтня ц.р. у Житомирі. Опубліковано рішення обох форумів та звернення пленуму Всеукраїнської асоціації інфекціоністів до очільників держави.
ПІДРУЧНИКУ З ЕПІДЕМІОЛОГІЇ АКАДЕМІКА Д.К. ЗАБОЛОТНОГО – 90 РОКІВ
Authors: Andreychyn M. A.
Published: December 2017

Мовиться про перший навчальний посібник «Основы эпидемиологии» академіка Д.К. Заболотного, виданий 1927 р., що тривалий час використовувався в Радянському Союзі як підручник для вищої медичної школи.
ПІДБІР КІЛЬКІСНОГО СКЛАДУ КОМПОНЕНТІВ ПРИ РОЗРОБЦІ ВЕТЕРИНАРНОГО ПРЕПАРАТУ ДЛЯ ІНТРАЦИСТЕРНАЛЬНОГО ВВЕДЕННЯ
Authors: Polova Zh. M. , Almakayeva L. H.
Published: December 2017

Мета роботи. Розробка якісного складу та підбір оптимального співвідношення компонентів комбінованого ветеринарного препарату для інтрацистернального введення.Матеріали і методи. Об'єктом дослідження були серії препарату антимікробної дії «Аргоцид», який містить цитрат срібла, D – пантенол та L – аргінін та призначений для лікування і профілактики субклінічного маститу великої рогатої худоби (ВРХ). Були вивчені фізико-хімічні показники стабільності препарата при температурі (25±2) оС для довгострокових випробувань та при температурі (40±2) оС для прискорених. Визначали наступні параметри відповідно до вимог Державної Фармакопеї України: кількісний вміст діючих речовин, зовнішній вигляд розчину, прозорість, рН.Результати й обговорення. В результаті дослідження стабільності зразків ветеринарного препарату при зберіганні з наступними співвідношеннями діючих речовин: срібла цитрату –0,01 г; L – аргініну –0,52 г; декспантенолу –0,50 г виявлено, що в умовах довгострокового зберігання в зразках спостерігали незмінність їх фізико-хімічних властивостей протягом лише 6 місяців. Результати прискорених випробувань виявили нестабільність зразків ветеринарного препарату на більш ранніх термінах, яка може бути наслідком деструкції цитрату срібла в досліджуваних зразках. Проведено науково дослідну роботу з метою вивчення стабільності обраної комбінації діючих речовин після зміні її концентрації в розчині. Дослідження проводили, аналізуючи результати спостережень за стабільністю зразків, отриманих двома способами. За першим способом отримували ветеринарну лікарську форму, яка являє собою два стерильні розчини – А та В, які змішують перед введенням в одному шприці-тубі для інтрамамарного застосування. Другий спосіб відрізнявся тим, що розчин готували одразу з такими ж концентраціями всіх компонентів, як у змішаному розчині А + В, при цьому зберігалося вибране співвідношення діючих речовин.Висновки. Підібрано оптимальне співвідношення компонентів нового комбінованого інтрамамарного препарату антимікробної дії у вигляді розчину в ампулах, що містить цитрат срібла – 0,005 г, D – пантенол – 0,260 г та L – аргінін – 0,250 г для лікування та профілактики субклінічного маститу ВРХ під умовною назвою «Аргоцид», що є стабільним при зберіганні протягом 12 місяців.
МЕТОДИЧНІ ПІДХОДИ ДО ПОЗИЦІОНУВАННЯ ЛІКУВАЛЬНО-КОСМЕТИЧНИХ ЗАСОБІВ
Authors: Posilkina O. V. , Kotlyarova V. G. , Chechotka O. V.
Published: December 2017

Мета роботи. Розробка методичних підходів до позиціонування лікувально-косметичних засобів із врахуванням особливостей різних сегментів споживачів.Матеріали та методи. Метод контрольного опитування, метод експертного опитування, шкала Р. Лайкерта.Результати й обговорення. Проведені дослідження показали, що всіх споживачів лікувально-косметичних засобів (ЛКЗ) можна розподілити на дві основні категорії: потенційних та постійних споживачів. Для підвищення ефективності просування ЛКЗ фармацевтичним компаніям (ФК) необхідно позиціонувати ЛКЗ із врахуванням особливостей їх сприйняття кожним із сегментів споживачів. Для цих сегментів розроблені алгоритми позиціонування ЛКЗ, спрямованих на підкреслення переваг, які отримають споживачі від їх використання.Висновки. Впровадження запропонованих підходів позиціонування ЛКЗ спрямоване на підвищення інформованості різних груп споживачів про особливості різних ЛКЗ та формування стійких вподобань споживачів на основі розуміння одержуваних переваг, що буде сприяти підвищенню ефективності просування ЛКЗ.
РОЗРОБКА ТА ВАЛІДАЦІЯ МЕТОДИКИ СПЕКТРОФОТОМЕТРИЧНОГО КІЛЬКІСНОГО ВИЗНАЧЕННЯ ДИЛТІАЗЕМУ В ЛІКАРСЬКИХ ФОРМАХ
Authors: Sulyma M. I. , Ogurtsov V. V. , Zhuk Yu. M. , Vasyuk S. O.
Published: December 2017

Мета роботи. Розробка методів контролю якості, зокрема, спектрофотометричного визначення кількісного вмісту дилтіазему в лікарських формах «Діакордін 60» та «Діакордін 90 Ретард» на основі реакції з бромкрезоловим зеленим, а також валідація розроблених методик.Матеріали і методи. Об’єкти дослідження – таблетки «Діакордін 60» (Zentiva у складі САНОФІ, Чеська Республіка, серія 3010117) та таблетки «Діакордін 90 Ретард» (Zentiva у складі САНОФІ, Чеська Республіка, серія 3510317).Реагенти і розчинники: стандартний зразок дилтіазему, бромкрезоловий зелений, ацетон.Аналітичне обладнання: спектрофотометр Specord 200, ваги електронні АВТ-120-5DM, ультразвукова баня ELMASONICE60 H.Результати й обговорення. Розроблено методику спектрофотометричного визначення кількісного вмісту дилтіазему в лікарських формах «Діакордін 60» та «Діакордін 90 Ретард» на основі реакції з бромкрезоловим зеленим. Стехіометричні співвідношення реагуючих компонентів «дилтіазем – БКЗ», одержані методами неперервних змін та методом насичення, повністю узгоджуються між собою та становлять 1:1. За такими валідаційними характеристиками, як лінійність, прецизійність, правильність та робасність розроблена методика є коректною і може бути використана у відділах технічного контролю хіміко-фармацевтичних підприємств.Висновки. У результаті роботи встановлено, що дилтіазем реагує з БКЗ у середовищі ацетону за кімнатної температури з утворенням забарвленого продукту з максимумом світлопоглинання при 408 нм. Досліджувана реакція є високочутливою: молярний коефіцієнт світлопоглинання становить 11547, а відкривальний мінімум 1,79 мкг/мл.Доведено, що за такими валідаційними характеристиками, як лінійність, прецизійність, правильність та робасність розроблена методика є коректною і може бути використана у відділах технічного контролю хіміко-фармацевтичних підприємств.
ВИЗНАЧЕННЯ ЦІНИ ДОЗИ ДІАГНОСТИЧНОГО ЛІКАРСЬКОГО ЗАСОБУ «ФТОРДЕЗОКСИГЛЮКОЗА 18F, РОЗЧИН ДЛЯ ІН’ЄКЦІЙ»
Authors: Kachaniuk V. V.
Published: December 2017

Мета роботи. Визначити ціну дози Фтордезоксиглюкози (ФДГ) для обґрунтування вартості надання медичної послуги з позитронно-емісійної томографії (ПЕТ-дослідження).Матеріали і методи. У роботі використано витратний метод та метод встановлення ціни на основі відчутної цінності товару.Результати й обговорення. Досліджуючи фармацевтичний ринок України з виробництва радіофармацевтичних препаратів (РФП), які застосовують для діагностики злоякісних новоутворень за допомогою ПЕТ-дослідження, виникла необхідність у визначенні ціни однієї дози РФП «Фтордезоксиглюкоза18F, розчин для ін’єкцій» для обґрунтування вартості надання медичної послуги з ПЕТ-дослідження.Висновки. Запропоновано методику розрахунку ціни однієї дози ФДГ, яка базується на поєднанні витратного методу та методу встановлення ціни на основі відчутної цінності товару. За допомогою витратного методу розраховували собівартість виробництва ФДГ. Визначення вартості медичної послуги з ПЕТ-дослідження доцільно здійснювати з використанням методу встановлення ціни на основі відчутної цінності товару. За допомогою запропонованої методики визначено вартість однієї дози діагностичного лікарського засобу «Фтордезоксиглюкоза 18F, розчин для ін’єкцій».
ПОРІВНЯЛЬНИЙ АНАЛІЗ АСОРТИМЕНТУ ЛІКАРСЬКИХ ЗАСОБІВ ДЛЯ ВАГІНАЛЬНОГО ЗАСТОСУВАННЯ НА ФАРМАЦЕВТИЧНИХ РИНКАХ УКРАЇНИ ТА РОСІЙСЬКОЇ ФЕДЕРАЦІЇ
Authors: Hlushchenko O. M. , Polova Zh. M. , Khomenko R. M.
Published: December 2017

Мета роботи. Провести порівняльне дослідження асортименту лікарських засобів для вагінального застосування на фармацевтичних ринках України та Російської Федерації.Матеріали і методи. Об’єктами дослідження були Державні реєстри лікарських засобів України та Російської Федерації, інструкції для медичного застосування препаратів. У процесі досліджень використовували наступні методи аналізу: економіко-статистичні, кореляційні, метод організаційно-функціонального моделювання.Результати й обговорення. Проведено аналіз лікарських засобів для вагінального застосування, що зареєстровані на ринках України та Російської Федерації, встановлено: вітчизняний ринок на 75 % складається з ЛЗ іноземного та 25 % вітчизняного виробництва. Частка іноземних препаратів на ринку РФ становить 53 %, а вітчизняних – 47 %. Згідно з класифікаційною системою АТС, зареєстровані лікарські засоби для вагінального застосування на ринку України представлені двома, а РФ – шістьма фармакотерапевтичними групами. Представлена номенклатура лікарських засобів для вагінального застосування недостатня для задоволення потреб населення України, тому розробка нових конкурентоздатних (за ефективністю, безпечністю і ціною) ліків є актуальною і сучасною.Висновки. Проведено порівняльне дослідження асортименту лікарських засобів для вагінального застосування на фармацевтичних ринках України та Російської Федерації.
АНАЛІЗ СОЦІАЛЬНИХ ІНДИКАТОРІВ ЕПІДЕМІЇ ТБ / ВІЛ В УКРАЇНІ
Authors: Fedyak I. O. , Fedyak Р. І.
Published: December 2017

Мета. Базуючись на аналізі даних медичної карти стаціонарного хворого Ф003/о, визначити і оцінити соціальні індикатори ко-інфекції ТБ/ВІЛ в Україні.Матеріали та методи: 1 200 медичних карт стаціонарних хворих на ТБ / ВІЛ у діапазоні нозологій «А15–А19 Туберкульоз» з ВІЛ-інфекцією, випадково відібрані з архівів 12 обласних протитуберкульозних диспансерів (зі збереженням таємниці персональних даних хворих); соціологічний метод аналізу документів (формалізований, контент-аналіз).Результати і обговорення. Досліджувану вибірку пацієнтів із ТБ / ВІЛ на 91% склали непрацюючі особи, які потребують постійного соціального супроводу. Бо з усіх виписаних лише 49,34% хворих закінчили стаціонарний етап лікування, який у середньому тривав 116±93 ліжко-днів; 25,25% осіб були виписані за порушення лікарняного режиму (18% – самовільно залишили стаціонар, 7,25% – порушили інші правила перебування). Оскільки найвища частка працюючих осіб із ТБ / ВІЛ виявилася в областях найвищої поширеності ВІЛ-інфекції: Одеській (17,14%), м. Києві (14,81%), Дніпропетровській (13,6%), Запорізькій (13,33 %), можна припустити, що ВІЛ-інфекція в Україні виходить за межі «груп ризику».Висновки. У межах областей аналізу за соціально-демографічними характеристиками хворі на ТБ / ВІЛ були: у 72,25±8,33% випадків чоловіками (ймовірність належати до жіночої статі зростала в областях найвищої поширеності ВІЛ); у 94,41±2,32% – віком 22–51 рр., в тому числі у 54,83±8,1% – 32–41 рр.; у 66,39±11,41% – проживали у містах; у 90,84±5,09% – відносились до соціально незахищених верст суспільства: були безробітними працездатного віку (69,17±8,97%), інвалідами (19,92±10,71%), пенсіонерами (0,83±1,31%), перебували у декретній відпустці (0,67±0,99%), студентами (0,25±0,56%), у тому числі належали до осіб без постійного місця проживання (2,33±2,56%), були внутрішніми переселенцями (0,92±1,7%), засудженими (0,75±0,69%). Водночас соціальні індикатори ТБ/ВІЛ, які стосуються перебування хворих у протитуберкульозних закладах, найперше залежали від регіону проживання.