bluuebunny/crossref_metadata_2025 huggingface dataset:
Min3: Predict microRNA target gene using an improved binding-site representation method and support vector machine
Authors: Huang Tinghua , Huang Xiali , Yao Min
Published: December 2019

MicroRNAs are single-stranded noncoding RNAs known to down-regulate target genes at the protein or mRNA level. Computational prediction of targets is essential for elucidating the detailed functions of microRNA. However, prediction specificity and sensitivity of the existing algorithms still need to be improved to generate useful hypotheses for subsequent experimental testing. A new microRNA binding-site representation method was developed, which uses four symbols “[Formula: see text]”, “:”, “[Formula: see text]”, and “[Formula: see text]” (indicating paired, unpaired, insertion, and bulge, respectively) to represent the status of each nucleotide base pair in the microRNA binding site. New features were established with the information of every two adjacent symbols. There are 12 possible combinations and the frequency of each defines a set of novel and useful features. A comprehensive training dataset is constructed for mammalian microRNAs with positive targets obtained from the microRNA target depository in the miRTarbase, while negative targets were derived from pseudo-microRNA bindings. An SVM model was established using the training dataset and a new software called Min3 was developed. Performance of Min3 was assessed with intensively studied examples of miR-155 and miR-92a. Prediction results showed that Min3 can discover 47% of experimental conformed targets on average. The overlapping is above 20% on average when compared with TargetScan and miRanda. Annotations of the public microRNA datasets showed that there is a negative effect (up-regulation) of the Min3 targets for the knock out/down of miR-155 and miR-92a. Six top ranked targets were selected for validation by wet-lab experiments, and five of them showed a regulation effect. The Min3 can be a good alternative to current microRNA target discovery software. This tool is available at https://sourceforge.net/projects/mirt3 .
Preparation and Photocatalytic Hydrogen Production Properties of Mesoporous CdS/TiO2 Composites
Authors: Wang Xiao-Li , Zheng Ren-Rong , Yu Hui , Dong Xiang-Ting
Published: December 2019

The mesoporous CdS/TiO2 composites were synthesized by a sol–gel method combined with solvothermal method. The material showed the gel block-like structures which were composed of heterogeneous spherical gel particles, the average size of the particles was about 14[Formula: see text]nm, with specific surface area as 300.254[Formula: see text]m2[Formula: see text]g[Formula: see text]. The mesoporous CdS/TiO2 composites exhibited a wide absorption band to simulated sunlight whose adsorb wavelength reached to 550[Formula: see text]nm, its absorption intensity and catalytic performance of photocatalytic water-producing hydrogenation were also increased with the increase of CdS contents. When the molar ratio of TiO2:CdS was 1:1, the photocatalytic activity reached the highest, and the average hydrogen production rate reached 2167.32[Formula: see text][Formula: see text]mol[Formula: see text]g[Formula: see text][Formula: see text]h[Formula: see text].
Seamless Parametrization with Arbitrary Cones for Arbitrary Genus
Authors: Campen Marcel , Shen Hanxiao , Zhou Jiaran , Zorin Denis
Published: December 2019

Seamless global parametrization of surfaces is a key operation in geometry processing, e.g., for high-quality quad mesh generation. A common approach is to prescribe the parametric domain structure, in particular, the locations of parametrization singularities (cones), and solve a non-convex optimization problem minimizing a distortion measure, with local injectivity imposed through either constraints or barrier terms. In both cases, an initial valid parametrization is essential to serve as a feasible starting point for obtaining an optimized solution. While convexified versions of the constraints eliminate this initialization requirement, they narrow the range of solutions, causing some problem instances that actually do have a solution to become infeasible.

We demonstrate that for arbitrary given sets of topologically admissible parametric cones with prescribed curvature, a global seamless parametrization always exists (with the exception of one well-known case). Importantly, our proof is constructive and directly leads to a general algorithm for computing such parametrizations. Most distinctively, this algorithm is bootstrapped with a convex optimization problem (solving for a conformal map), in tandem with a simple linear equation system (determining a seamless modification of this map). This initial map can then serve as a valid starting point and be optimized for low distortion using existing injectivity preserving methods.
Next-Item Recommendation via Collaborative Filtering with Bidirectional Item Similarity
Authors: Zeng Zijie , Lin Jing , Li Lin , Pan Weike , Ming Zhong
Published: December 2019

Exploiting temporal effect has empirically been recognized as a promising way to improve recommendation performance in recent years. In real-world applications, one-class data in the form of (user, item, timestamp) are usually more accessible and abundant than numerical ratings. In this article, we focus on exploiting such one-class data in order to provide personalized next-item recommendation services. Specifically, we base our work on the framework of time-aware item-based collaborative filtering and propose a simple yet effective similarity measurement called bidirectional item similarity (BIS) that is able to capture sequential patterns even from noisy data. Furthermore, we extend BIS via some factorization techniques and obtain an adaptive version, i.e., adaptive BIS (ABIS), in order to better fit the behavioral data. We also design a compound weighting function that leverages the complementarity between two well-known time-aware weighting functions. With the proposed similarity measurements and weighting function, we obtain two novel collaborative filtering methods that are able to achieve significantly better performance than the state-of-the-art methods, showcasing their effectiveness for next-item recommendation.
The next 700 relational program logics
Authors: Maillard Kenji , Hriţcu Cătălin , Rivas Exequiel , Van Muylder Antoine
Published: December 2019

We propose the first framework for defining relational program logics for arbitrary monadic effects. The framework is embedded within a relational dependent type theory and is highly expressive. At the semantic level, we provide an algebraic presentation of relational specifications as a class of relative monads, and link computations and specifications by introducing relational effect observations, which map pairs of monadic computations to relational specifications in a way that respects the algebraic structure. For an arbitrary relational effect observation, we generically define the core of a sound relational program logic, and explain how to complete it to a full-fledged logic for the monadic effect at hand. We show that this generic framework can be used to define relational program logics for effects as diverse as state, input-output, nondeterminism, and discrete probabilities. We, moreover, show that by instantiating our framework with state and unbounded iteration we can embed a variant of Benton's Relational Hoare Logic, and also sketch how to reconstruct Relational Hoare Type Theory. Finally, we identify and overcome conceptual challenges that prevented previous relational program logics from properly dealing with control effects, and are the first to provide a relational program logic for exceptions.
Actris: session-type based reasoning in separation logic
Authors: Hinrichsen Jonas Kastberg , Bengtson Jesper , Krebbers Robbert
Published: December 2019

Message passing is a useful abstraction to implement concurrent programs. For real-world systems, however, it is often combined with other programming and concurrency paradigms, such as higher-order functions, mutable state, shared-memory concurrency, and locks. We present Actris: a logic for proving functional correctness of programs that use a combination of the aforementioned features. Actris combines the power of modern concurrent separation logics with a first-class protocol mechanism—based on session types—for reasoning about message passing in the presence of other concurrency paradigms. We show that Actris provides a suitable level of abstraction by proving functional correctness of a variety of examples, including a distributed merge sort, a distributed load-balancing mapper, and a variant of the map-reduce model, using relatively simple specifications. Soundness of Actris is proved using a model of its protocol mechanism in the Iris framework. We mechanised the theory of Actris, together with tactics for symbolic execution of programs, as well as all examples in the paper, in the Coq proof assistant.
Coq Coq correct! verification of type checking and erasure for Coq, in Coq
Authors: Sozeau Matthieu , Boulier Simon , Forster Yannick , Tabareau Nicolas , Winterhalter Théo
Published: December 2019

Coq is built around a well-delimited kernel that perfoms typechecking for definitions in a variant of the Calculus of Inductive Constructions (CIC). Although the metatheory of CIC is very stable and reliable, the correctness of its implementation in Coq is less clear. Indeed, implementing an efficient type checker for CIC is a rather complex task, and many parts of the code rely on implicit invariants which can easily be broken by further evolution of the code. Therefore, on average, one critical bug has been found every year in Coq.

This paper presents the first implementation of a type checker for the kernel of Coq (without the module system and template polymorphism), which is proven correct in Coq with respect to its formal specification and axiomatisation of part of its metatheory. Note that because of Gödel's incompleteness theorem, there is no hope to prove completely the correctness of the specification of Coq inside Coq (in particular strong normalisation or canonicity), but it is possible to prove the correctness of the implementation assuming the correctness of the specification, thus moving from a trusted code base (TCB) to a trusted theory base (TTB) paradigm.

Our work is based on the MetaCoq project which provides metaprogramming facilities to work with terms and declarations at the level of this kernel. Our type checker is based on the specification of the typing relation of the Polymorphic, Cumulative Calculus of Inductive Constructions (PCUIC) at the basis of Coq and the verification of a relatively efficient and sound type-checker for it. In addition to the kernel implementation, an essential feature of Coq is the so-called extraction: the production of executable code in functional languages from Coq definitions. We present a verified version of this subtle type-and-proof erasure step, therefore enabling the verified extraction of a safe type-checker for Coq.
Trace types and denotational semantics for sound programmable inference in probabilistic languages
Authors: Lew Alexander K. , Cusumano-Towner Marco F. , Sherman Benjamin , Carbin Michael , Mansinghka Vikash K.
Published: December 2019

Modern probabilistic programming languages aim to formalize and automate key aspects of probabilistic modeling and inference. Many languages provide constructs for
programmable inference
that enable developers to improve inference speed and accuracy by tailoring an algorithm for use with a particular model or dataset. Unfortunately, it is easy to use these constructs to write unsound programs that appear to run correctly but produce incorrect results. To address this problem, we present a denotational semantics for programmable inference in higher-order probabilistic programming languages, along with a type system that ensures that well-typed inference programs are sound by construction. A central insight is that the type of a probabilistic expression can track the space of its possible execution traces, not just the type of value that it returns, as these traces are often the objects that inference algorithms manipulate. We use our semantics and type system to establish soundness properties of custom inference programs that use constructs for variational, sequential Monte Carlo, importance sampling, and Markov chain Monte Carlo inference.
Liquidate your assets: reasoning about resource usage in liquid Haskell
Authors: Handley Martin A. T. , Vazou Niki , Hutton Graham
Published: December 2019

Liquid Haskell is an extension to the type system of Haskell that supports formal reasoning about program correctness by encoding logical properties as refinement types. In this article, we show how Liquid Haskell can also be used to reason about program efficiency in the same setting. We use the system's existing verification machinery to ensure that the results of our cost analysis are valid, together with custom invariants for particular program contexts to ensure that the results of our analysis are precise. To illustrate our approach, we analyse the efficiency of a wide range of popular data structures and algorithms, and in doing so, explore various notions of resource usage. Our experience is that reasoning about efficiency in Liquid Haskell is often just as simple as reasoning about correctness, and that the two can naturally be combined.
Abstract extensionality: on the properties of incomplete abstract interpretations
Authors: Bruni Roberto , Giacobazzi Roberto , Gori Roberta , Garcia-Contreras Isabel , Pavlovic Dusko
Published: December 2019

In this paper we generalise the notion of extensional (functional) equivalence of programs to
abstract equivalences
induced by
abstract interpretations
. The standard notion of extensional equivalence is recovered as the special case, induced by the concrete interpretation. Some properties of the extensional equivalence, such as the one spelled out in Rice’s theorem, lift to the abstract equivalences in suitably generalised forms. On the other hand, the generalised framework gives rise to interesting and important new properties, and allows refined, non-extensional analyses. In particular, since programs turn out to be extensionally equivalent if and
only if
they are equivalent just for the concrete interpretation, it follows that any non-trivial abstract interpretation uncovers some intensional aspect of programs. This striking result is also effective, in the sense that it allows constructing, for any non-trivial abstraction, a pair of programs that are extensionally equivalent, but have different abstract semantics. The construction is based on the fact that abstract interpretations are always sound, but that they can be made incomplete through suitable code transformations. To construct these transformations, we introduce a novel technique for building
incompleteness cliques
of extensionally equivalent yet abstractly distinguishable programs: They are built together with abstract interpretations that produce false alarms. While programs are forced into incompleteness cliques using both control-flow and data-flow transformations, the main result follows from limitations of data-flow transformations with respect to control-flow ones. A further consequence is that the class of incomplete programs for a non-trivial abstraction is Turing complete. The obtained results also shed a new light on the relation between the techniques of code obfuscation and the precision in program analysis.
Spy game: verifying a local generic solver in Iris
Authors: de Vilhena Paulo Emílio , Pottier François , Jourdan Jacques-Henri
Published: December 2019

We verify the partial correctness of a "local generic solver", that is, an on-demand, incremental, memoizing least fixed point computation algorithm. The verification is carried out in Iris, a modern breed of concurrent separation logic. The specification is simple: the solver computes the optimal least fixed point of a system of monotone equations. Although the solver relies on mutable internal state for memoization and for "spying", a form of dynamic dependency discovery, it is apparently pure: no side effects are mentioned in its specification. As auxiliary contributions, we provide several illustrations of the use of prophecy variables, a novel feature of Iris; we establish a restricted form of the infinitary conjunction rule; and we provide a specification and proof of Longley's modulus function, an archetypical example of spying.
Aiming low is harder: induction for lower bounds in probabilistic program verification
Authors: Hark Marcel , Kaminski Benjamin Lucien , Giesl Jürgen , Katoen Joost-Pieter
Published: December 2019

We present a new inductive rule for verifying lower bounds on expected values of random variables after execution of probabilistic loops as well as on their expected runtimes. Our rule issimplein the sense that loop body semantics need to be applied only finitely often in order to verify that the candidates are indeed lower bounds. In particular, it is not necessary to find the limit of a sequence as in many previous rules.
Executable formal semantics for the POSIX shell
Authors: Greenberg Michael , Blatt Austin J.
Published: December 2019

The POSIX shell is a widely deployed, powerful tool for managing computer systems. The shell is the expert’s control panel, a necessary tool for configuring, compiling, installing, maintaining, and deploying systems. Even though it is powerful, critical infrastructure, the POSIX shell is maligned and misunderstood. Its power and its subtlety are a dangerous combination.

We define a formal, mechanized, executable small-step semantics for the POSIX shell, which we call Smoosh. We compared Smoosh against seven other shells that aim for some measure of POSIX compliance (bash, dash, zsh, OSH, mksh, ksh93, and yash). Using three test suites—the POSIX test suite, the Modernish test suite and shell diagnostic, and a test suite of our own device—we found Smoosh’s semantics to be the most conformant to the POSIX standard. Modernish judges Smoosh to have the fewest bugs (just one, from using dash’s parser) and no quirks. To show that our semantics is useful beyond yielding a conformant, executable shell, we also implemented a symbolic stepper to illuminate the subtle behavior of the shell.

Smoosh will serve as a foundation for formal study of the POSIX shell, supporting research on and development of new shells, new tooling for shells, and new shell designs.
The future is ours: prophecy variables in separation logic
Authors: Jung Ralf , Lepigre Rodolphe , Parthasarathy Gaurav , Rapoport Marianna , Timany Amin , Dreyer Derek , Jacobs Bart
Published: December 2019

Early in the development of Hoare logic, Owicki and Gries introduced
auxiliary variables
as a way of encoding information about the
history
of a program’s execution that is useful for verifying its correctness. Over a decade later, Abadi and Lamport observed that it is sometimes also necessary to know in advance what a program will do in the
future
. To address this need, they proposed
prophecy variables
, originally as a proof technique for refinement mappings between state machines. However, despite the fact that prophecy variables are a clearly useful reasoning mechanism, there is (surprisingly) almost no work that attempts to integrate them into Hoare logic. In this paper, we present the first account of prophecy variables in a Hoare-style program logic that is flexible enough to verify
logical atomicity
(a relative of linearizability) for classic examples from the concurrency literature like RDCSS and the Herlihy-Wing queue. Our account is formalized in the Iris framework for separation logic in Coq. It makes essential use of
ownership
to encode the exclusive right to resolve a prophecy, which in turn enables us to enforce soundness of prophecies with a very simple set of proof rules.
Disentanglement in nested-parallel programs
Authors: Westrick Sam , Yadav Rohan , Fluet Matthew , Acar Umut A.
Published: December 2019

Nested parallelism has proved to be a popular approach for programming the rapidly expanding range of multicore computers. It allows programmers to express parallelism at a high level and relies on a run-time system and a scheduler to deliver efficiency and scalability. As a result, many programming languages and extensions that support nested parallelism have been developed, including in C/C++, Java, Haskell, and ML. Yet, writing efficient and scalable nested parallel programs remains challenging, primarily due to difficult concurrency bugs arising from destructive updates or effects. For decades, researchers have argued that functional programming can simplify writing parallel programs by allowing more control over effects but functional programs continue to underperform in comparison to parallel programs written in lower-level languages. The fundamental difficulty with functional languages is that they have high demand for memory, and this demand only grows with parallelism.

In this paper, we identify a memory property, called disentanglement, of nested-parallel programs, and propose memory management techniques for improved efficiency and scalability. Disentanglement allows for (destructive) effects as long as concurrently executing threads do not gain knowledge of the memory objects allocated by each other. We formally define disentanglement by considering an ML-like higher-order language with mutable references and presenting a dynamic semantics for it that enables reasoning about computation graphs of nested parallel programs. Based on this graph semantics, we formalize a classic correctness property---determinacy race freedom---and prove that it implies disentanglement. This establishes that disentanglement applies to a relatively broad class of parallel programs. We then propose memory management techniques for nested-parallel programs that take advantage of disentanglement for improved efficiency and scalability. We show that these techniques are practical by extending the MLton compiler for Standard ML to support this form of nested parallelism. Our empirical evaluation shows that our techniques are efficient and scale well.
Interaction trees: representing recursive and impure programs in Coq
Authors: Xia Li-yao , Zakowski Yannick , He Paul , Hur Chung-Kil , Malecha Gregory , Pierce Benjamin C. , Zdancewic Steve
Published: December 2019

Interaction trees
(ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant of “free monads,” ITrees are built out of uninterpreted events and their continuations. They support compositional construction of interpreters from
event handlers
, which give meaning to events by defining their semantics as monadic actions. ITrees are expressive enough to represent impure and potentially nonterminating, mutually recursive computations, while admitting a rich equational theory of equivalence up to weak bisimulation. In contrast to other approaches such as relationally specified operational semantics, ITrees are executable via code extraction, making them suitable for debugging, testing, and implementing software artifacts that are amenable to formal verification.

We have implemented ITrees and their associated theory as a Coq library, mechanizing classic domain- and category-theoretic results about program semantics, iteration, monadic structures, and equational reasoning. Although the internals of the library rely heavily on coinductive proofs, the interface hides these details so that clients can use and reason about ITrees without explicit use of Coq’s coinduction tactics.

To showcase the utility of our theory, we prove the termination-sensitive correctness of a compiler from a simple imperative source language to an assembly-like target whose meanings are given in an ITree-based denotational semantics. Unlike previous results using operational techniques, our bisimulation proof follows straightforwardly by structural induction and elementary rewriting via an equational theory of combinators for control-flow graphs.
Semantics of higher-order probabilistic programs with conditioning
Authors: Dahlqvist Fredrik , Kozen Dexter
Published: December 2019

We present a denotational semantics for higher-order probabilistic programs in terms of linear operators between Banach spaces. Our semantics is rooted in the classical theory of Banach spaces and their tensor products, but bears similarities with the well-known semantics of higher-order programs a la Scott through the use of ordered Banach spaces which allow definitions in terms of fixed points. Our semantics is a model of intuitionistic linear logic: it is based on a symmetric monoidal closed category of ordered Banach spaces which treats randomness as a linear resource, but by constructing an exponential comonad we can also accommodate non-linear reasoning. We apply our semantics to the verification of the classical Gibbs sampling algorithm.
Provenance-guided synthesis of Datalog programs
Authors: Raghothaman Mukund , Mendelson Jonathan , Zhao David , Naik Mayur , Scholz Bernhard
Published: December 2019

We propose a new approach to synthesize Datalog programs from input-output specifications. Our approach leverages query provenance to scale the counterexample-guided inductive synthesis (CEGIS) procedure for program synthesis. In each iteration of the procedure, a SAT solver proposes a candidate Datalog program, and a Datalog solver evaluates the proposed program to determine whether it meets the desired specification. Failure to satisfy the specification results in additional constraints to the SAT solver. We propose efficient algorithms to learn these constraints based on “
why
” and “
why not
” provenance information obtained from the Datalog solver. We have implemented our approach in a tool called ProSynth and present experimental results that demonstrate significant improvements over the state-of-the-art, including in synthesizing invented predicates, reducing running times, and in decreasing variances in synthesis performance. On a suite of 40 synthesis tasks from three different domains, ProSynth is able to synthesize the desired program in 10 seconds on average per task—an order of magnitude faster than baseline approaches—and takes only under a second each for 28 of them.
Pointer life cycle types for lock-free data structures with memory reclamation
Authors: Meyer Roland , Wolff Sebastian
Published: December 2019

We consider the verification of lock-free data structures that manually manage their memory with the help of a safe memory reclamation (SMR) algorithm. Our first contribution is a type system that checks whether a program properly manages its memory. If the type check succeeds, it is safe to ignore the SMR algorithm and consider the program under garbage collection. Intuitively, our types track the protection of pointers as guaranteed by the SMR algorithm. There are two design decisions. The type system does not track any shape information, which makes it extremely lightweight. Instead, we rely on invariant annotations that postulate a protection by the SMR. To this end, we introduce angels, ghost variables with an angelic semantics. Moreover, the SMR algorithm is not hard-coded but a parameter of the type system definition. To achieve this, we rely on a recent specification language for SMR algorithms. Our second contribution is to automate the type inference and the invariant check. For the type inference, we show a quadratic-time algorithm. For the invariant check, we give a source-to-source translation that links our programs to off-the-shelf verification tools. It compiles away the angelic semantics. This allows us to infer appropriate annotations automatically in a guess-and-check manner. To demonstrate the effectiveness of our type-based verification approach, we check linearizability for various list and set implementations from the literature with both hazard pointers and epoch-based memory reclamation. For many of the examples, this is the first time they are verified automatically. For the ones where there is a competitor, we obtain a speed-up of up to two orders of magnitude.
Will deepfakes do deep damage?
Authors: Greengard Samuel
Published: December 2019

The ability to produce fake videos that appear amazingly real is here. Researchers are now developing ways to detect and prevent them.
The Effects of Task Complexity on the Use of Different Types of Information in a Search Assistance Tool
Authors: Choi Bogeum , Ward Austin , Li Yuan , Arguello Jaime , Capra Robert
Published: December 2019

In interactive information retrieval, an important research question is: How do task characteristics influence users’ needs and behaviors? We report on a laboratory study (
N
=32) that investigated the effects of task complexity on the types of information used by participants while searching. Participants completed tasks of four complexity levels and had access to four different types of information provided through a search-assistance tool referred to as the InfoBoxes (IB). The IB tool presented the following types of task-related information (
info-types
) on different tabs: (1) facts, (2) concepts, (3) opinions, and (4) insights. Facts (and opinions) were defined as objective (and subjective) statements relevant to the task. Concepts were defined as important ideas, principles, or entities related to the task. Insights were defined as tips or advice about the task. The study investigated six research questions that considered the effects of task complexity on: (RQ1) participants’ pre-/post-task perceptions about useful info-types; (RQ2) use of different info-types during the task; (RQ3) motivations for engaging with the IB; (RQ4) gains from using it; (RQ5) the search stage participants were in while engaging with the IB; and (RQ6) motivations for sometimes avoiding the IB. Our results suggest that task complexity influenced all six types of outcomes. We discuss implications of our results for designing search assistance tools and systems that favor certain types of content based on task characteristics.
Lithography Hotspot Detection with FFT-based Feature Extraction and Imbalanced Learning Rate
Authors: He Xu , Deng Yu , Zhou Shizhe , Li Rui , Wang Yao , Guo Yang
Published: December 2019

With the increasing gap between transistor feature size and lithography manufacturing capability, the detection of lithography hotspots becomes a key stage of physical verification flow to enhance manufacturing yield. Although machine learning approaches are distinguished for their high detection efficiency, they still suffer from problems such as large-scale layout and class imbalance. In this article, we develop a hotspot detection model based on machine learning with high performance. In the proposed model, we first apply an Fast Fourier Transform--based feature extraction method that can compress large-scale layout to a multi-dimensional representation with much smaller size while preserving the discriminative layout pattern information to improve the detection efficiency. Second, addressing the class imbalance problem, we propose a new technique called imbalanced learning rate and embed it into the convolutional neural network model to further reduce false alarms without accuracy decay. Compared with the results of current state-of-the-art approaches on ICCAD 2012 Contest benchmarks, our proposed model can achieve better solutions in many evaluation metrics, including the official metrics.
An interview with Jeronimo Castrillon
Authors: Anjum Bushra
Published: December 2019

In this series of interviews with innovation leaders, Ubiquity Associate Editor and software engineer, Dr. Bushra Anjum sits down with Jeronimo Castrillon, a professor in the Department of Computer Science at the TU Dresden, to discuss the need for novel programming abstractions and methodologies for efficient computing on future systems.
LncRNA TUG1 mediates ischemic myocardial injury by targeting miR-132-3p/HDAC3 axis
Authors: Su Qiang , Liu Yang , Lv Xiang-Wei , Dai Ri-Xin , Yang Xi-Heng , Kong Bing-Hui
Published: December 2019

Increased production of reactive oxygen species (ROS) significantly contributed to the pathogenesis of acute myocardial infarction (AMI). Recent studies suggest that hypoxia upregulated the long noncoding RNA taurine upregulated gene 1 (TUG1). In this study, we explored the functional significance and molecular mechanisms of TUG1/miR-132-3p axis in ischemia-challenged cardiomyocytes. In primary cardiomyocytes challenged with H2O2, expressions of miR-132-3p, TUG1, and other target proteins were measured by RT quantitative PCR or Western blot analysis; cell viability by 3-(4,5-dimethylthiazolyl-2)-2,5-diphenyltetrazolium bromide assay; apoptosis by annexin V and propidium iodide staining; the abundance of acetylated H3K9 or histone deacetylase 3 (HDAC3) within the promoter of target genes by chromatin immunoprecipitation; the direct interaction between miR-132-3p and HDAC3 or TUG1 by luciferase reporter assay. The biological significance of miR-132-3p, TUG1, and HDAC3 was assessed using miR-132-3p mimic, siRNA-targeting TUG1 and HDAC3 inhibitor RGF966, respectively, in H2O2-challenged cells in vitro or ischemia-reperfusion (I/R)-induced AMI in vivo. miR-132-3p was downregulated, whereas TUG1 upregulated in H2O2-challenged cardiomyocytes. Overexpressing miR-132-3p or knocking down TUG1 significantly improved viability, inhibited apoptosis, and reduced ROS production in H2O2-stressed cardiomyocytes in vitro and alleviated I/R-induced AMI in vivo. Mechanistically, TUG1 sponged miR-132-3p and upregulated HDAC3, which reduced the acetylation of H3K9 and epigenetically inhibited expressions of antioxidative genes, including Bcl-xL, Prdx2, and Hsp70. The TUG1/miR-132-3p/HDAC3 axis critically regulates ROS production and the pathogenic development of AMI. Targeting TUG1, upregulating miR-132-3p, or inhibiting HDAC3 may benefit AMI treatment.

NEW & NOTEWORTHY Increased production of reactive oxygen species (ROS) significantly contributed to the pathogenesis of acute myocardial infarction (AMI). Recent studies suggest that hypoxia upregulated the long noncoding RNA taurine upregulated gene 1 (TUG1). However, the underlying mechanisms remain elusive. In the present study, we reported for the first time that H2O2 or ischemia-reperfusion-induced TUG1, by sponging microRNA 132-3p, activated histone deacetylase 3, which in turn targeted multiple protective genes, stimulated intracellular ROS accumulation, and aggravated the injury of AMI. Our findings might provide some insight to seek new targets for AMI treatment.
Effect of Industrial Dust Deposition on Photovoltaic Module Performance: Experimental Measurements in the Tropical Region
Authors: Andrea Yotham , Pogrebnaya Tatiana , Kichonge Baraka
Published: December 2019

Dust particle accumulation affects outdoor photovoltaic module transmittance of solar cell glazing and thus leads to significant degradation of conversion efficiency owing to lower irradiance reaching the surface. In this study, the sensitivity of the polycrystalline silicon photovoltaic module towards industrial dust deposition was experimentally investigated under the tropical climatic condition of Arusha, Tanzania. Dust involved in the study came from fertilizer, gypsum, aggregate crusher, and coal mine industries. The experimental measurements were outdoor conducted under 720 W/m2, 800 W/m2, and 900 W/m2 solar irradiances. Results indicated that dust accumulation on the polycrystalline silicon photovoltaic module negatively affected output power as well as short-circuit current, however having no significant impact on open-circuit voltage. Maximum module efficiency loss was observed to be 64%, 42%, 30%, and 29% for coal, aggregate, gypsum, and organic fertilizer dust, respectively; hence, coal dust was the most effecting dust among the four. It was also demonstrated that PV module performance deteriorated with temperature rise owing to heat dissipation caused by dust accumulation.
Prognostic and Clinicopathological Significance of MUC Family Members in Colorectal Cancer: A Systematic Review and Meta-Analysis
Authors: Li Chao , Zuo Didi , Liu Tao , Yin Libin , Li Chenyao , Wang Lei
Published: December 2019

Objective. To assess the association between MUC expression levels in colorectal cancer (CRC) tissues and prognosis and investigate the associations between MUC expression levels and CRC clinicopathological characteristics. Methods. The PubMed, Embase, Cochrane Library, and Web of Science databases were searched from inception through September 13, 2019, to identify studies investigating the association between MUC expression levels in CRC tissues and prognosis. Pooled hazard ratios (HRs) or odds ratio (ORs) with 95% confidence intervals (CIs) were used to evaluate associations between MUC expression levels and prognosis or clinicopathological characteristics, respectively. The heterogeneity between studies was assessed by the I2 values, whereas the likelihood of publication bias was assessed by Egger’s linear regression and Begg’s rank correlation test. Results. Among 33 included studies (n=6032 patients), there were no associations between combined MUC phenotype expression levels and overall survival (OS) or disease-free survival (DFS)/relapse-free survival (RFS) in patients with CRC. In subgroup analyses, the upregulated MUC1 expression (HR=1.50; 95% CI, 1.29–1.74; P<0.00001) was associated with poor OS. However, the upregulated MUC2 expression (HR=0.64; 95% CI, 0.52–0.79; P<0.00001) was associated with better OS. Furthermore, a high level of MUC1 expression (HR=1.99; 95% CI, 0.99–3.99; P=0.05) was associated with shorter DFS/RFS. However, patients with a low level of MUC2 tumors showed better DFS/RFS than patients with a high level of MUC2 tumors (HR=0.71; 95% CI, 0.49–1.04; P=0.08; P=0.0.009, I2=67%) and MUC5AC expression (HR=0.56; 95% CI, 0.38–0.82; P=0.003) was associated with longer DFS/RFS. In addition, a high level of MUC1 expression was associated with CRC in the rectum, deeper invasion, lymph node metastasis, distant metastasis, advanced tumor stage, and lymphatic invasion. A high level of MUC2 expression had a protective effect. High secretion of MUC5AC is associated with colon cancer compared with rectal cancer. Conclusion. The protein expression of MUC1 might be a poor biomarker in colorectal cancer and might play a role in tumor transformation and metastasis. However, the protein expression of MUC2 expression might have a protective effect. Furthermore, randomized controlled trials (RCTs) of large patients are needed to confirm the results.
Success and Challenge When Returning to Clinical Practice: A Case Series in Anesthesiologist Re-Entry
Authors: Green Michael S. , Iqbal Usama , Hoffman Christopher R. , Green Parmis , Varjavand Nielufar
Published: December 2019

Introduction. Anesthesiologists returning to clinical practice pose unique challenges for licensing and credentialing boards. Few institutions provide re-education. We describe the physician refresher/re-entry program at our College of Medicine. Methods. We launched the physician re-entry program in 2006. This individualized program re-educates physicians who left clinical practice for any reason and are seeking to return. We report results achieved for 12 anesthesiologists who successfully completed the course between August 2012 and February 2018. Results. Seven men and five women left their practices for various reasons, which included relocation, family or medical reasons, substance use, and burnout. None left practice for medical negligence. Range away from clinical activity was 0–10 years. Five had active licenses. Seven were US graduates and five were international. Nine of 12 achieved their goals. Of the 3 others, 1 did not pursue her goal, another did not obtain a residency, and the other just finished the program. Seven out of 9 (78%) achieved their goal within 1 year of course completion. Discussion. Despite our small sample size, our experience to successfully return inactive physicians to the workforce adds to the scant literature and experience in refreshing inactive physicians. Our trainees return to practice serving communities across the country and are now a pivotal part of the anesthesiology workforce. Thus, this program not only services individual physicians, but the whole community affected by their absence.
Congenital Microphthalmia with Intraorbital Cyst: A Rare Case Report
Authors: Timalsina Bishow Raj , Shrestha Gulshan Bahadur , Thapa Madhu
Published: December 2019

Microphthalmia is considered to be the most common congenital malformation of the eye after congenital cataract. However, its association with intraorbital cyst is considered to be very rare. Most of the lesions are still misdiagnosed as orbital tumor and teratomas as there is a general paucity of data reported in literature. Herein, we report a rare case of congenital microphthalmia with intraorbital cyst in an eight-month-old male patient.
Clinical Characteristics and Prognosis of Gastrointestinal Metastases in Solid Tumor Patients: A Retrospective Study and Review of Literatures
Authors: Lin Li , Wang Xiangyi , Tang Chuanhao , Liang Jun
Published: December 2019

Background. According to the literature and our experience, patients with gastrointestinal metastases are relatively rare. Numerous case reports and literature reviews have been reported. We present one of the larger case series of gastrointestinal metastases.Objectives. To explore the clinical characteristics and prognosis of patients with gastrointestinal tract metastases, which are rare metastatic sites.Methods. Patients with gastrointestinal metastases in the setting of stage IV primary carcinomas treated at Beijing Ditan Hospital and Peking University International Hospital from November 1992 to August 2017 were included in this study. The diagnosis of gastrointestinal tract metastases was based on histopathology.Results. 30 patients (median age 56 years, 56.7% female) were included. The most common primary carcinomas associated with gastrointestinal metastases were breast (11 patients, 36.7%), stomach (9 patients, 30.0%), and lung (4 patients, 13.3%) cancer. The major pathological types were adenocarcinoma (16 patients, 53.3%) and ductal carcinoma (9 patients, 30.0%). Ten patients (33.3%) underwent local gastrointestinal treatment, and 20 patients (66.7%) underwent nonlocal treatment (involving chemotherapy alone or best supportive care). For breast cancer patients and gastric cancer patients who underwent local therapy, a significant survival advantage was observed (p=0.001andp=0.012, respectively). The presence of other common metastases was identified as an independent poor prognostic factor through multivariate analysis with a HR (hazard ratio) of survival of 0.182 (95% confidence interval (CI) 0.11-0.523,p=0.031).Conclusion. Gastrointestinal metastases are most frequently from breast invasive ductal carcinoma. The presentation of other common metastases with gastrointestinal metastasis indicates poor prognosis, and selected patients may benefit from surgical intervention.
Understanding of ROS-Inducing Strategy in Anticancer Therapy
Authors: Kim Su Ji , Kim Hyun Soo , Seo Young Rok
Published: December 2019

Redox homeostasis is essential for the maintenance of diverse cellular processes. Cancer cells have higher levels of reactive oxygen species (ROS) than normal cells as a result of hypermetabolism, but the redox balance is maintained in cancer cells due to their marked antioxidant capacity. Recently, anticancer therapies that induce oxidative stress by increasing ROS and/or inhibiting antioxidant processes have received significant attention. The acceleration of accumulative ROS disrupts redox homeostasis and causes severe damage in cancer cells. In this review, we describe ROS-inducing cancer therapy and the anticancer mechanism employed by prooxidative agents. To understand the comprehensive biological response to certain prooxidative anticancer drugs such as 2-methoxyestradiol, buthionine sulfoximine, cisplatin, doxorubicin, imexon, and motexafin gadolinium, we propose and visualize the drug-gene, drug-cell process, and drug-disease interactions involved in oxidative stress induction and antioxidant process inhibition as well as specific side effects of these drugs using pathway analysis with a big data-based text-mining approach. Our review will be helpful to improve the therapeutic effects of anticancer drugs by providing information about biological changes that occur in response to prooxidants. For future directions, there is still a need for pharmacogenomic studies on prooxidative agents as well as the molecular mechanisms underlying the effects of the prooxidants and/or antioxidant-inhibitor agents for effective anticancer therapy through selective killing of cancer cells.
Stress Measurement of Steel Strands Based on System Identification Method
Authors: Qian Ji , Li Jianbin , Li Changchun , Zhou Jianting , Yao Guowen
Published: December 2019

Steel strands are crucial components of a prestressed structure, but their performance degrades inevitably with time. Among the existing nondestructive testing methods for measuring the stress state of steel strands, ultrasonic guided wave methods have received the most research attention and are most likely to be applied to actual engineering. This work views the propagation of ultrasonic guided wave as an individual system, and the variations in the stress state in steel strands can be related to the parameters gained by the system identification model. The finite element simulation and experimental results show the propagation characteristics of the guided wave are influenced distinctly by the stress state. The index constructed by the system parameters exhibits good monotonic linear with stress level variation, and the slope of the fitted line from experimental data is similar to the simulation result. The sensor placement and loading path have a limited effect on the stress state and the proposed index.
Numerical Techniques for Solving Linear Volterra Fractional Integral Equation
Authors: Hamdan Safa’ , Qatanani Naji , Daraghmeh Adnan
Published: December 2019

Two numerical techniques, namely, Haar Wavelet and the product integration methods, have been employed to give an approximate solution of the fractional Volterra integral equation of the second kind. To test the applicability and efficiency of the numerical method, two illustrative examples with known exact solution are presented. Numerical results show clearly that the accuracy of these methods are in a good agreement with the exact solution. A comparison between these methods shows that the product integration method provides more accurate results than its counterpart.
Headache and MRI Changes after Endovascular Treatment of a Cerebral Aneurysm
Authors: Høllesli Liv Jorunn , Kurz Martin W. , Behzadi Gry Inger N. , Solbakken Tore , Harald Mørkve Svein , Kurz Kathinka D.
Published: December 2019

Background. The main complications after endovascular therapy of intracranial aneurysms are aneurysm rupture and thromboembolic events. Yet, the widespread use of magnetic resonance imaging (MRI) in follow-up of these patients also demonstrates other, rarely known complications such as aseptic meningitis and foreign body reaction. Case Presentation. A small aneurysm in the right posterior communicating artery was treated with endovascular therapy in a 65 year old woman. Two weeks after successful interventional treatment, the patient developed a headache. On MRI performed five months after intervention, vasogenic edema was seen in the vascular territory of the right internal carotid artery. The edema and the symptoms diminished without specific treatment within a year. Interpretation. The clinical and radiological presentation of this case are suggestive of a foreign body reaction, a treatable condition that radiologists and clinicians should be aware of.