bluuebunny/crossref_metadata_2025 huggingface dataset:
Effects of the Annealing Temperature on the Structure Evolution and Antifungal Performance of TiO2/Fe3O4 Nanocomposites Manufactured from Natural Sand
Authors: Taufiq Ahmad , Listanti Anita , Saputro Rosy Eko , Hidayat Nurul , Subadra ST. Ulfawanti Intan , Sunaryono Sunaryono , Mufti Nandang , Susanto Hendra , Soontaranon Siriwat
Published: November 2020

This study investigated the effects of annealing temperature on the structure evolution and antifungal performance of TiO2/Fe3O4 nanocomposites. The TiO2/Fe3O4 nanocomposites were fabricated through a combination of sonochemical and coprecipitation routes. The TiO2 structure evolved from an amorphous phase to a crystalline anatase phase starting at an annealing temperature of [Formula: see text]C while Fe3O4 evolved to [Formula: see text]-Fe2O3 and [Formula: see text]-Fe2O3 starting at an annealing temperature of [Formula: see text]C. The increases in the crystallite sizes and lattice parameters were also identified because of the increase in the annealing temperature. The TiO2/Fe3O4 nanocomposites tended to agglomerate due to van der Waals forces. The molecular structural dynamics of TiO2/Fe3O4 nanocomposites were also studied by infrared spectroscopy within the wavenumber range of 400–4000[Formula: see text]cm[Formula: see text]. The antifungal activity of TiO2/Fe3O4 nanocomposites was better than those of individual TiO2 and Fe3O4. These results showed that structure evolution plays an essential role in the antifungal performance of TiO2/Fe3O4 nanocomposites.
Molecularly Imprinted Fluorescent Sensors Based on Nitrogen-Doped CDs for Highly Selective Detection of Aspirin
Authors: Peng Long , Xu Yeqing , Huang Ting , Liu Xiqing , Yang Xinyan , Meng Minjia , Yan Yongsheng
Published: November 2020

In this paper, we prepared a fluorescent sensor based on carbon quantum dots (CDs) and molecularly imprinted technology (MIT) that was successfully synthesized and applied to the detection of aspirin (Asp) residues in biological and pharmaceutical samples. The molecularly imprinted fluorescence sensor had the high sensitivity of quantum dots and the high selectivity of molecularly imprinted polymers (MIPs). Nitrogen-doped carbon quantum dots (N-CDs) with high fluorescence intensity were prepared and then was coated with silicon by the reverse microemulsion method. Finally, 3-aminopropyltriethoxysilane (APTES) was used as the functional monomer and Asp as the template molecule, molecularly imprinted layers were formed around the N-CDs. Under the best experimental conditions, the detection limit of the sensor was 0.198[Formula: see text]mg[Formula: see text]L[Formula: see text]. Between 0.9–9.0[Formula: see text]mg[Formula: see text]L[Formula: see text], this fluorescence sensor had a good linear relationship with the concentration of Asp. To test the practicability of the sensor, we used this fluorescent sensor to detect Asp in human urine and saliva. Satisfied recovery rate between 101.1–105.1% and 102.1–106.0% were obtained, respectively.
SDCN
Authors: Liu Liang , Chen Bo , Ma Huadong
Published: November 2020

Building an open global sensing layer is critical for the Internet of Things (IoT). In this article, we present a Sensory Data-Centric Networking (SDCN) architecture for inter-networking two main networked sensing systems in IoT—wireless sensor networks and mobile sensing networks. Specifically, the proposed SDCN is a systematic solution including NDNs for sensor nodes in the Zigbee network, NDNm for mobilephones in the Wi-Fi network, and NDNg for gateways. Considering the sensing requirement of IoT, we first design a novel Spatio-Temporal 16 Tree (ST16T) naming scheme associated with the scope-matching method. Based on the naming scheme, we further propose the related discovery methods, network switching mechanism, forwarding, and routing strategies according to the features of large-scale sensing and resource-constrained environment. A proof-of-concept prototype is implemented and further is deployed on our campus (BUPT) and the Great Wall (Shaanxi, China) for Environment Monitoring Project. Several experiments are conducted on the deployed platform. The experimental results show that SDCN outperforms the state-of-the-arts and gains a great performance improvement in terms of energy consumption, data collection efficiency, memory footprint, and time delay.
The Impact of Weighting Schemes and Stemming Process on Topic Modeling of Arabic Long and Short Texts
Authors: Ma Tinghuai , Al-Sabri Raeed , Zhang Lejun , Marah Bockarie , Al-Nabhan Najla
Published: November 2020

In this article, first a comprehensive study of the impact of term weighting schemes on the topic modeling performance (i.e., LDA and DMM) on Arabic long and short texts is presented. We investigate six term weighting methods including Word count method (standard topic models), TFIDF, PMI, BDC, CLPB, and CEW. Moreover, we propose a novel combination term weighting scheme, namely, CmTLB. We utilize the mTFIDF that takes into account the missing terms and the number of the documents in which the term appears when calculating the term weight. For further robust term weight, we combine mTFIDF with two weighting methods. We evaluate CmTLB against the studied weighting schemes by the quality of the learned topics (topic visualization and topic coherence), classification, and clustering tasks. We applied weighting schemes to Latent Dirichlet allocation (LDA) and Dirichlet multinomial mixture (DMM) on eight Arabic long and short document datasets, respectively. The experiment results outline that appropriate weighting schemes can effectively improve topic modeling performance on Arabic texts. More importantly, our proposed CmTLB significantly outperforms the other weighting schemes. Secondly, we investigate whether the Arabic stemming process can improve topic modeling performance. We study the three approaches of Arabic stemming including root-based, stem-based, and statistical approaches. We also train topic models with weighting schemes on documents after applying four stemmers related to different stemming approaches. The results outline that applying the stemming process not only reduces the dimensionality of term-document matrix leading to fast estimation process, but also show enhancement of topic modeling performance both on short and long Arabic documents. Moreover, Farasa stemmer achieves the highest performance in most cases, since it prevents the ambiguity that may happen because of the blind removal of the affixes such as in root-based or stem-based stemmers.
Session-based Hotel Recommendations Dataset
Authors: Adamczak Jens , Deldjoo Yashar , Moghaddam Farshad Bakhshandegan , Knees Peter , Leyson Gerard-Paul , Monreal Philipp
Published: November 2020

In 2019, the Recommender Systems Challenge [17] dealt for the first time with a real-world task from the area of e-tourism, namely the recommendation of hotels in booking sessions. In this context, we present the release of a new dataset that we believe is vitally important for recommendation systems research in the area of hotel search, from both academic and industry perspectives. In this article, we describe the qualitative characteristics of the dataset and present the comparison of several baseline algorithms trained on the data.
A Novel Multi-task Tensor Correlation Neural Network for Facial Attribute Prediction
Authors: Duan Mingxing , Li Kenli , Li Keqin , Tian Qi
Published: November 2020

Multi-task learning plays an important role in face multi-attribute prediction. At present, most researches excavate the shared information between attributes by sharing all convolutional layers. However, it is not appropriate to treat the low-level and high-level features of the face multi-attribute equally, because the high-level features are more biased toward the specific content of the category. In this article, a novel multi-attribute tensor correlation neural network (MTCN) is used to predict face attributes. MTCN shares all attribute features at the low-level layers, and then distinguishes each attribute feature at the high-level layers. To better excavate the correlations among high-level attribute features, each sub-network explores useful information from other networks to enhance its original information. Then a tensor canonical correlation analysis method is used to seek the correlations among the highest-level attributes, which enhances the original information of each attribute. After that, these features are mapped into a highly correlated space through the correlation matrix. Finally, we use sufficient experiments to verify the performance of MTCN on the CelebA and LFWA datasets and our MTCN achieves the best performance compared with the latest multi-attribute recognition algorithms under the same settings.
Proving highly-concurrent traversals correct
Authors: Feldman Yotam M. Y. , Khyzha Artem , Enea Constantin , Morrison Adam , Nanevski Aleksandar , Rinetzky Noam , Shoham Sharon
Published: November 2020

Modern highly-concurrent search data structures, such as search trees, obtain multi-core scalability and performance by having operations traverse the data structure without any synchronization. As a result, however, these algorithms are notoriously difficult to prove linearizable, which requires identifying a point in time in which the traversal's result is correct. The problem is that traversing the data structure as it undergoes modifications leads to complex behaviors, necessitating intricate reasoning about all interleavings of reads by traversals and writes mutating the data structure.

In this paper, we present a general proof technique for proving unsynchronized traversals correct in a significantly simpler manner, compared to typical concurrent reasoning and prior proof techniques. Our framework relies only on sequential properties of traversals and on a conceptually simple and widely-applicable condition about the ways an algorithm's writes mutate the data structure. Establishing that a target data structure satisfies our condition requires only simple concurrent reasoning, without considering interactions of writes and reads. This reasoning can be further simplified by using our framework.

To demonstrate our technique, we apply it to prove several interesting and challenging concurrent binary search trees: the logical-ordering AVL tree, the Citrus tree, and the full contention-friendly tree. Both the logical-ordering tree and the full contention-friendly tree are beyond the reach of previous approaches targeted at simplifying linearizability proofs.
Semiring optimizations: dynamic elision of expressions with identity and absorbing elements
Authors: Leobas Guilherme Vieira , Pereira Fernando Magno Quintão
Published: November 2020

This paper describes a compiler optimization to eliminates dynamic occurrences of expressions in the format
a
←
a
⊕
b
⊗
c
. The operation ⊕ must admit an identity element
z
, such that
a
⊕
z
=
a
. Also,
z
must be the absorbing element of ⊗, such that
b
⊗
z
=
z
⊗
c
=
z
. Semirings where ⊕ is the additive operator and ⊗ is the multiplicative operator meet this contract. This pattern is common in high-performance benchmarks—its canonical representative being the multiply-add operation
a
←
a
+
b
×
c
. However, several other expressions involving arithmetic and logic operations satisfy the required algebra. We show that the runtime elimination of such assignments can be implemented in a performance-safe way via online profiling. The elimination of dynamic redundancies involving identity and absorbing elements in 35 programs of the LLVM test suite that present semiring patterns brings an average speedup of 1.19x (total optimized time over total unoptimized time) on top of clang -O3. When projected onto the entire test suite (259 programs) the optimization leads to a speedup of 1.025x. Once added onto clang, semiring optimizations approximates it to TACO, a specialized tensor compiler.
Precise inference of expressive units of measurement types
Authors: Xiang Tongtong , Luo Jeff Y. , Dietl Werner
Published: November 2020

Ensuring computations are unit-wise consistent is an important task in software development. Numeric computations are usually performed with primitive types instead of abstract data types, which results in very weak static guarantees about correct usage and conversion of units. This paper presents PUnits, a pluggable type system for expressive units of measurement types and a precise, whole-program inference approach for these types. PUnits can be used in three modes: (1) modularly check the correctness of a program, (2) ensure a possible unit typing exists, and (3) annotate a program with units. Annotation mode allows human inspection and is essential since having a valid typing does not guarantee that the inferred specification expresses design intent. PUnits is the first units type system with this capability. Compared to prior work, PUnits strikes a novel balance between expressiveness, inference complexity, and annotation effort. We implement PUnits for Java and evaluate it by specifying the correct usage of frequently used JDK methods. We analyze 234k lines of code from eight open-source scientific computing projects with PUnits. We compare PUnits against an encapsulation-based units API (the javax.measure package) and discovered unit errors that the API failed to find. PUnits infers 90 scientific units for five of the projects and generates well-specified applications. The experiments show that PUnits is an effective, sound, and scalable alternative to using encapsulation-based units APIs, enabling Java developers to reap the performance benefits of using primitive types instead of abstract data types for unit-wise consistent scientific computations.
Statically verified refinements for multiparty protocols
Authors: Zhou Fangyi , Ferreira Francisco , Hu Raymond , Neykova Rumyana , Yoshida Nobuko
Published: November 2020

With distributed computing becoming ubiquitous in the modern era, safe distributed programming is an open challenge. To address this, multiparty session types (MPST) provide a typing discipline for message-passing concurrency, guaranteeing communication safety properties such as deadlock freedom.

While originally MPST focus on the communication aspects, and employ a simple typing system for communication payloads, communication protocols in the real world usually contain constraints on the payload. We introduce refined multiparty session types (RMPST), an extension of MPST, that express data dependent protocols via refinement types on the data types.

We provide an implementation of RMPST, in a toolchain called Session*, using Scribble, a toolchain for multiparty protocols, and targeting F*, a verification-oriented functional programming language. Users can describe a protocol in Scribble and implement the endpoints in F* using refinement-typed APIs generated from the protocol. The F* compiler can then statically verify the refinements. Moreover, we use a novel approach of callback-styled API generation, providing static linearity guarantees with the inversion of control. We evaluate our approach with real world examples and show that it has little overhead compared to a naive implementation, while guaranteeing safety properties from the underlying theory.
Projection-based runtime assertions for testing and debugging Quantum programs
Authors: Li Gushu , Zhou Li , Yu Nengkun , Ding Yufei , Ying Mingsheng , Xie Yuan
Published: November 2020

In this paper, we propose Proq, a runtime assertion scheme for testing and debugging quantum programs on a quantum computer. The predicates in Proq are represented by projections (or equivalently, closed subspaces of the state space), following Birkhoff-von Neumann quantum logic. The satisfaction of a projection by a quantum state can be directly checked upon a small number of projective measurements rather than a large number of repeated executions. On the theory side, we rigorously prove that checking projection-based assertions can help locate bugs or statistically assure that the semantic function of the tested program is close to what we expect, for both exact and approximate quantum programs. On the practice side, we consider hardware constraints and introduce several techniques to transform the assertions, making them directly executable on the measurement-restricted quantum computers. We also propose to achieve simplified assertion implementation using local projection technique with soundness guaranteed. We compare Proq with existing quantum program assertions and demonstrate the effectiveness and efficiency of Proq by its applications to assert two sophisticated quantum algorithms, the Harrow-Hassidim-Lloyd algorithm and Shor’s algorithm.
DiffStream: differential output testing for stream processing programs
Authors: Kallas Konstantinos , Niksic Filip , Stanford Caleb , Alur Rajeev
Published: November 2020

High performance architectures for processing distributed data streams, such as Flink, Spark Streaming, and Storm, are increasingly deployed in emerging data-driven computing systems. Exploiting the parallelism afforded by such platforms, while preserving the semantics of the desired computation, is prone to errors, and motivates the development of tools for specification, testing, and verification. We focus on the problem of differential output testing for distributed stream processing systems, that is, checking whether two implementations produce equivalent output streams in response to a given input stream. The notion of equivalence allows reordering of logically independent data items, and the main technical contribution of the paper is an optimal online algorithm for checking this equivalence. Our testing framework is implemented as a library called DiffStream in Flink. We present four case studies to illustrate how our framework can be used to (1) correctly identify bugs in a set of benchmark MapReduce programs, (2) facilitate the development of difficult-to-parallelize high performance applications, and (3) monitor an application for a long period of time with minimal performance overhead.
Compiling symbolic execution with staging and algebraic effects
Authors: Wei Guannan , Bračevac Oliver , Tan Shangyin , Rompf Tiark
Published: November 2020

Building effective symbolic execution engines poses challenges in multiple dimensions: an engine must correctly model the program semantics, provide flexibility in symbolic execution strategies, and execute them efficiently.

This paper proposes a principled approach to building correct, flexible, and efficient symbolic execution engines, directly rooted in the semantics of the underlying language in terms of a high-level definitional interpreter. The definitional interpreter induces algebraic effects to abstract over semantic variants of symbolic execution, e.g., collecting path conditions as a state effect and path exploration as a nondeterminism effect. Different handlers of these effects give rise to different symbolic execution strategies, making execution strategies orthogonal to the symbolic execution semantics, thus improving flexibility. Furthermore, by annotating the symbolic definitional interpreter with binding-times and specializing it to the input program via the first Futamura projection, we obtain a "symbolic compiler", generating efficient instrumented code having the symbolic execution semantics. Our work reconciles the interpretation- and instrumentation-based approaches to building symbolic execution engines in a uniform framework.

We illustrate our approach on a simple imperative language step-by-step and then scale up to a significant subset of LLVM IR. We also show effect handlers for common path selection strategies. Evaluating our prototype's performance shows speedups of 10~30x over the unstaged counterpart, and ~2x over KLEE, a state-of-the-art symbolic interpreter for LLVM IR.
Program equivalence for assisted grading of functional programs
Authors: Clune Joshua , Ramamurthy Vijay , Martins Ruben , Acar Umut A.
Published: November 2020

In courses that involve programming assignments, giving meaningful feedback to students is an important challenge. Human beings can give useful feedback by manually grading the programs but this is a time-consuming, labor intensive, and usually boring process. Automatic graders can be fast and scale well but they usually provide poor feedback. Although there has been research on improving automatic graders, research on scaling and improving human grading is limited.

We propose to scale human grading by augmenting the manual grading process with an equivalence algorithm that can identify the equivalences between student submissions. This enables human graders to give targeted feedback for multiple student submissions at once. Our technique is conservative in two aspects. First, it identifies equivalence between submissions that are algorithmically similar, e.g., it cannot identify the equivalence between quicksort and mergesort. Second, it uses formal methods instead of clustering algorithms from the machine learning literature. This allows us to prove a soundness result that guarantees that submissions will never be clustered together in error. Despite only reporting equivalence when there is algorithmic similarity and the ability to formally prove equivalence, we show that our technique can significantly reduce grading time for thousands of programming submissions from an introductory functional programming course.
A type-and-effect system for object initialization
Authors: Liu Fengyun , Lhoták Ondřej , Biboudis Aggelos , Giarrusso Paolo G. , Odersky Martin
Published: November 2020

Every newly created object goes through several initialization states: starting from a state where all fields are uninitialized until all of them are assigned. Any operation on the object during its initialization process, which usually happens in the constructor via
this
, has to observe the initialization states of the object for correctness, i.e. only initialized fields may be used. Checking safe usage of
this
statically, without manual annotation of initialization states in the source code, is a challenge, due to aliasing and virtual method calls on
this
.

Mainstream languages either do not check initialization errors, such as Java, C++, Scala, or they defend against them by not supporting useful initialization patterns, such as Swift. In parallel, past research has shown that safe initialization can be achieved for varying degrees of expressiveness but by sacrificing syntactic simplicity.

We approach the problem by upholding
local reasoning about initialization
which avoids whole-program analysis, and we achieve
typestate polymorphism
via subtyping. On this basis, we put forward a novel type-and-effect system that can effectively ensure initialization safety while allowing flexible initialization patterns. We implement an initialization checker in the Scala 3 compiler and evaluate on several real-world projects.
Designing types for R, empirically
Authors: Turcotte Alexi , Goel Aviral , Křikava Filip , Vitek Jan
Published: November 2020

The R programming language is widely used in a variety of domains. It was designed to favor an interactive style of programming with minimal syntactic and conceptual overhead. This design is well suited to data analysis, but a bad fit for tools such as compilers or program analyzers. In particular, R has no type annotations, and all operations are dynamically checked at run-time. The starting point for our work are the two questions:
what expressive power is needed to accurately type R code?
and
which type system is the R community willing to adopt?
Both questions are difficult to answer without actually experimenting with a type system. The goal of this paper is to provide data that can feed into that design process. To this end, we perform a large corpus analysis to gain insights in the degree of polymorphism exhibited by idiomatic R code and explore potential benefits that the R community could accrue from a simple type system. As a starting point, we infer type signatures for 25,215 functions from 412 packages among the most widely used open source R libraries. We then conduct an evaluation on 8,694 clients of these packages, as well as on end-user code from the Kaggle data science competition website.
Programming and reasoning with partial observability
Authors: Atkinson Eric , Carbin Michael
Published: November 2020

Computer programs are increasingly being deployed in partially-observable environments. A partially observable environment is an environment whose state is not completely visible to the program, but from which the program receives partial observations. Developers typically deal with partial observability by writing a state estimator that, given observations, attempts to deduce the hidden state of the environment. In safety-critical domains, to formally verify safety properties developers may write an environment model. The model captures the relationship between observations and hidden states and is used to prove the software correct.

In this paper, we present a new methodology for writing and verifying programs in partially observable environments. We present
belief programming
, a programming methodology where developers write an environment model that the program runtime automatically uses to perform state estimation. A belief program dynamically updates and queries a belief state that captures the possible states the environment could be in. To enable verification, we present
Epistemic Hoare Logic
that reasons about the possible belief states of a belief program the same way that classical Hoare logic reasons about the possible states of a program. We develop these concepts by defining a semantics and a program logic for a simple core language called BLIMP. In a case study, we show how belief programming could be used to write and verify a controller for the Mars Polar Lander in BLIMP. We present an implementation of BLIMP called CBLIMP and evaluate it to determine the feasibility of belief programming.
Do you have space for dessert? a verified space cost semantics for CakeML programs
Authors: Gómez-Londoño Alejandro , Åman Pohjola Johannes , Syeda Hira Taqdees , Myreen Magnus O. , Tan Yong Kiam
Published: November 2020

Garbage collectors relieve the programmer from manual memory management, but lead to compiler-generated machine code that can behave differently (e.g. out-of-memory errors) from the source code. To ensure that the generated code behaves exactly like the source code, programmers need a way to answer questions of the form: what is a sufficient amount of memory for my program to never reach an out-of-memory error?

This paper develops a cost semantics that can answer such questions for CakeML programs. The work described in this paper is the first to be able to answer such questions with proofs in the context of a language that depends on garbage collection. We demonstrate that positive answers can be used to transfer liveness results proved for the source code to liveness guarantees about the generated machine code. Without guarantees about space usage, only safety results can be transferred from source to machine code.

Our cost semantics is phrased in terms of an abstract intermediate language of the CakeML compiler, but results proved at that level map directly to the space cost of the compiler-generated machine code. All of the work described in this paper has been developed in the HOL4 theorem prover.
Finding bugs in database systems via query partitioning
Authors: Rigger Manuel , Su Zhendong
Published: November 2020

Logic bugs in Database Management Systems (DBMSs) are bugs that cause an incorrect result for a given query, for example, by omitting a row that should be fetched. These bugs are critical, since they are likely to go unnoticed by users. We propose Query Partitioning, a general and effective approach for finding logic bugs in DBMSs. The core idea of Query Partitioning is to, starting from a given original query, derive multiple, more complex queries (called partitioning queries), each of which computes a partition of the result. The individual partitions are then composed to compute a result set that must be equivalent to the original query's result set. A bug in the DBMS is detected when these result sets differ. Our intuition is that due to the increased complexity, the partitioning queries are more likely to stress the DBMS and trigger a logic bug than the original query. As a concrete instance of a partitioning strategy, we propose Ternary Logic Partitioning (TLP), which is based on the observation that a boolean predicate p can either evaluate to TRUE, FALSE, or NULL. Accordingly, a query can be decomposed into three partitioning queries, each of which computes its result on rows or intermediate results for which p, NOT p, and p IS NULL hold. This technique is versatile, and can be used to test WHERE, GROUP BY, as well as HAVING clauses, aggregate functions, and DISTINCT queries. As part of an extensive testing campaign, we found 175 bugs in widely-used DBMSs such as MySQL, TiDB, SQLite, and CockroachDB, 125 of which have been fixed. Notably, 77 of these were logic bugs, while the remaining were error and crash bugs. We expect that the effectiveness and wide applicability of Query Partitioning will lead to its broad adoption in practice, and the formulation of additional partitioning strategies.
Programming at the edge of synchrony
Authors: Drăgoi Cezara , Widder Josef , Zufferey Damien
Published: November 2020

Synchronization primitives for fault-tolerant distributed systems that ensure an effective and efficient cooperation among processes are an important challenge in the programming languages community. We present a new programming abstraction, ReSync, for implementing benign and Byzantine fault-tolerant protocols. ReSync has a new round structure that offers a simple abstraction for group communication, like it is customary in synchronous systems, but also allows messages to be received one by one, like in the asynchronous systems. This extension allows implementing network and algorithm-specific policies for the message reception, which is not possible in classic round models.

The execution of ReSync programs is based on a new generic round switch protocol that generalizes the famous theoretical result about consensus in the presence of partial synchrony by of Dwork, Lynch, and Stockmeyer. We evaluate experimentally the performance of ReSync’s execution platform, by comparing consensus implementations in ReSync with LibPaxos3, etcd, and Bft-SMaRt, three consensus libraries tolerant to benign, resp. byzantine faults.
Koord: a language for programming and verifying distributed robotics application
Authors: Ghosh Ritwika , Hsieh Chiao , Misailovic Sasa , Mitra Sayan
Published: November 2020

A robot’s code needs to sense the environment, control the hardware, and communicate with other robots. Current programming languages do not provide suitable abstractions that are independent of hardware platforms. Currently, developing robot applications requires detailed knowledge of signal processing, control, path planning, network protocols, and various platform-specific details. Further, porting applications across hardware platforms remains tedious. We present Koord—a domain specific language for distributed robotics—which abstracts platform-specific functions for sensing, communication, and low-level control. Koord makes the platform-independent control and coordination code portable and modularly verifiable. Koord raises the level of abstraction in programming by providing distributed shared memory for coordination and port interfaces for sensing and control. We have developed the formal executable semantics of Koord in the K framework. With this symbolic execution engine, we can identify assumptions (proof obligations) needed for gaining high assurance from Koord applications. We illustrate the power of Koord through three applications: formation flight, distributed delivery, and distributed mapping. We also use the three applications to demonstrate how platform-independent proof obligations can be discharged using the Koord Prover while platform-specific proof obligations can be checked by verifying the obligations using physics-based models and hybrid verification tools.
Insects: A Potential Source of Protein and Other Nutrients for Feed and Food
Authors: Hawkey Kerensa J. , Lopez-Viso Carlos , Brameld John M. , Parr Tim , Salter Andrew M.
Published: November 2020

Sustainable production of healthy food for a growing global population, in the face of the uncertainties of climate change, represents a major challenge for the coming decade. Livestock provide food with high nutritional value but are frequently fed on human-edible crops and are associated with significant production of greenhouse gases. Recent years have seen increasing interest in the farming of insects as a sustainable source of human food, or as a replacement of ingredients such as soya or fishmeal in the feeds of terrestrial livestock or fish. This review provides an overview of insect physiology and growth regulation, considers the requirements for insect farming and mass production, and summarizes the nutritional value of the 10 most commonly studied insect species, before reviewing the literature on the use of insects as feed and food. We highlight the challenges required to develop a sustainable, safe, and affordable insect farming industry.
Stem Cell Populations as Self-Renewing Many-Particle Systems
Authors: Jörg David J. , Kitadate Yu , Yoshida Shosei , Simons Benjamin D.
Published: November 2020

This article reviews the physical principles of stem cell populations as active many-particle systems that are able to self-renew, control their density, and recover from depletion. We illustrate the dynamical and statistical hallmarks of homeostatic mechanisms, from stem cell density fluctuations and transient large-scale oscillation dynamics during recovery to the scaling behavior of clonal dynamics and front-like boundary propagation during regeneration.
The Effectiveness of the Revised Intermittent Preventive Treatment with Sulphadoxine Pyrimethamine (IPTp-SP) in the Prevention of Malaria among Pregnant Women in Northern Ghana
Authors: Agyeman Yaa Nyarko , Newton Sam Kofi , Annor Raymond Boadu , Owusu-Dabo Ellis
Published: November 2020

This study investigated the effectiveness of the World Health Organization (WHO)-revised Intermittent Preventive Treatment using Sulphadoxine Pyrimethamine (IPTp-SP) dosage regimen in the prevention of malaria infections in pregnancy. The study involved a prospective cohort of pregnant women who attended the antenatal clinic in four health facilities (Tamale Teaching Hospital, Tamale West Hospital, Tamale Central Hospital, and Tamale SDA Hospital) within the Tamale metropolis. Data collection spanned a period of 12 months, from September 2016 to August 2017, to help account for seasonality in malaria. The study included 1181 pregnant women who attended antenatal clinics in four hospitals within the metropolis. The registers at the facilities served as a sampling frame, and the respondents were randomly sampled out from the number of pregnant women available during each visit. They were enrolled consecutively as they kept reporting to the facility to receive antenatal care. The participants were stratified into three groups; the no IPTp-SP, <3 doses of IPTp-SP, and ≥3 doses of IPTp-SP. The participants were followed up until 36 weeks of gestation, and blood samples were analyzed to detect the presence of peripheral malaria parasites. At the end of the study, 42.4% of the women had taken at least 3 doses of SP based on the revised WHO IPTp-SP policy. Pregnant women who had taken at least 3 doses of IPTp-SP had a malaria prevalence of 16.9% at 36 weeks of gestation, compared to 35.8% of those who had not taken IPTp-SP. In the multivariable logistic regression, those who had taken ≥3 doses of SP were associated with 56% reduced odds (aOR 0.44, CI 0.27–0.70,

P
=
0.001

) of late gestational peripheral malaria, compared with those who did not take SP. IPTp-SP served under three or more doses provided a dose-dependent protection of 56% against maternal peripheral malaria parasitaemia detectable at the later stages of gestation (36 weeks). Since the dose-dependent potency of IPTp-SP depletes with time, there is the need for research into more sustainable approaches that offer longer protection.
A Numerical Study of Railway Ballast Subjected to Direct Shearing Using the Discrete Element Method
Authors: Zhao Hongyi , Chen Jing
Published: November 2020

Railway ballast is a coarse granular material used to carry train loads and provide drainage for the rail tracks. This study presents numerical explorations of the mechanical performance of ballast aggregates subjected to direct shear tests. The discrete element method (DEM) was used to investigate the microscopic characteristics of ballast aggregates during shearing while considering contact distribution, particle rotation, and particle displacement. By testing the angle of repose of ballast aggregates, the parameters for the DEM contact model could be calibrated. Four specimens were prepared and then subjected to different normal pressures. The results show that the contact between ballast particles intensifies in terms of the amount and magnitude as the normal pressure increases. A Fourier analysis was applied to investigate the anisotropy of contact normal and the contact forces for ballast aggregates at different shearing phases. The rotational and translational movements of ballast particles were investigated, and this investigation revealed that particle rotation gradually increased as the shearing propagated. Four regions in the aggregates were identified according to the translational pattern of ballast particles. The results of this research provide an in‐depth analysis of microscopic characteristics from a particulate scale.
Predictive and Prognostic Factors of Synchronous Colorectal Lung-Limited Metastasis
Authors: Li Yuqiang , Zhou Zhongyi , Liu Da , Zhou Ming , Tan Fengbo , Liu Wenxue , Zhu Hong
Published: November 2020

Aim. This study is aimed at investigating predictive and prognostic factors of synchronous colorectal lung-limited metastasis (SCLLM) based on The Surveillance, Epidemiology, and End Results (SEER) database. Methods. A multivariate logistic regression model was constructed to identify independent predictors of SCLLM. A multivariate Cox proportional hazards regression model was used to distinguish independent prognostic factors. Results. This study enrolled 168,007 colorectal cancer (CRC) patients without metastatic diseases and 1,298 cases with SCLLM. Eight features, involving race, tumor location, pathological grade, histological type, T stage, N stage, and tumor size as well as CEA, could be used as the independent predictors. As the nomogram shown, the T4 stage contributed the most to SCLLM, followed by the N2 stage, elevated CEA, and rectal cancer. A multivariate regression analysis discriminated 9 independent prognostic factors, including age, race, marital status, pathological grade, T stage, colectomy/proctectomy, chemotherapy, CEA, and TD. The prognostic nomogram illustrated that nonresection/NOS played as the poorest prognostic factor, followed by nonchemotherapy, ≥75-year old and T4 stage. The cumulative survival curves revealed the influence of each prognostic factor on survival after controlling the other variables. Conclusions. This study identified independent predictors and prognostic factors for SCLLM based on a large database of the United States. The predictors and prognostic factors can provide supporting evidence for the prevention and treatment of SCLLM.
Research on Failure Characteristics and Zoning Control Technology of Thick-Soft Surrounding Rock for Deep Gob-Side Entry Retaining
Authors: Wu Jingke , Zhou Wenbin , Tao Hong , Bai Haowen , Yin Wei , Gu Wenhu , Zhang Peng , Liu Zejun , Zhang Jiao
Published: November 2020

Controlling the large deformation caused by bed separation failure of thick and soft surrounding rock in gob-side entry retaining is difficult. The deformation and failure modes of thick and soft surrounding rock are summarized and classified based on field research, theoretical analysis, laboratory tests, and actual measurements. Systematic research is conducted on the lithologic characteristics, failure characteristics, and control methods of the surrounding rock. The research findings are as follows: (1) The low strength, softening, and water swelling of thick mudstone, as well as its cataclasis, dilatancy, and long-term creep under strong mining and high stress are the objective reasons for large deformation of the surrounding rock. (2) Due to the weak stability of the surrounding rock-support structure and low collaborative roof side bearing capacity, no complete supporting structure is formed with the supporting system, causing the support body in each area to be crushed one by one, which is the subjective reason for the deformation and failure of the surrounding rock. (3) The deformation and failure characteristics of thick and soft surrounding rock in gob-side entry retaining are primarily divided into eight types: roof bending and sinking type, roof cutting along filling body, rib spalling type, roof fall type, filling body rotation type, filling body crushing type, roof step type, and roof cutting along the coal side. The initial points and key points for a chain reaction of each failure type are determined. (4) The surrounding rock is divided into 10 support zones at four levels, and control technology for “zonal support and overall reinforcement” is put forward. The mechanical effect of the support body in each zone and its role in maintaining the stability of surrounding rock are analyzed. This technology can ensure the integrity of the surrounding rock structure and improve the roof side collaborative bearing capacity.
Multisensor Prognostic of RUL Based on EMD-ESN
Authors: Pei Jiaxin , Wang Jian
Published: November 2020

This paper presents a prognostic method for RUL (remaining useful life) prediction based on EMD (empirical mode decomposition)-ESN (echo state network). The combination method adopts EMD to decompose the multisensor time series into a bunch of IMFs (intrinsic mode functions), which are then predicted by ESNs, and the outputs of each ESN are summarized to obtain the final prediction value. The EMD can decompose the original data into simpler portions and during the decomposition process, much noise is filtered out and the subsequent prediction is much easier. The ESN is a relatively new type of RNN (recurrent neural network), which substitutes the hidden layers with a reservoir remaining unchanged during the training phase. The characteristic makes the training time of ESN is much shorter than traditional RNN. The proposed method is applied to the turbofan engine datasets and is compared with LSTM (Long Short-Term Memory) and ESN. Extensive experimental results show that the prediction performance and efficiency are much improved by the proposed method.
Holistic Approach in Designing the Personalized Bone Scaffold: The Case of Reconstruction of Large Missing Piece of Mandible Caused by Congenital Anatomic Anomaly
Authors: Milovanovic Jelena R. , Stojkovic Milos S. , Husain Karim N. , Korunovic Nikola D. , Arandjelovic Jovan
Published: November 2020

The paper reports on the importance of applying the holistic approach in designing a personalized bone scaffold, but also all other kinds of personalized implants. In addition, the paper attempts to point out the important aspects of the design of a PBS against which the quality of a realistic and applicable design solution should be assessed. The holistic approach refers to the adaptation of design features of a bone scaffold to the multilateral specifics related to the particular patient, its surgical case, and curing treatment. To ensure a successful application, five aspects of personalized bone scaffold design should be considered while it is being adapted: anatomical congruency, mechanical conformity, biochemical compatibility and biodegradability, manufacturability, and implantability. To demonstrate the importance of applying a holistic approach in designing a personalized bone scaffold, the paper shows a case where a patient-specific scaffold aimed at the reconstruction of a large missing piece of mandible was designed. The research resulted in a series of recommendations regarding the methods of bone geometry reconstruction and scaffold design. The paper sheds new light on the desired mechanical properties of a personalized bone scaffold while also recommending possible design parameters for optimizing the construction according to these properties. Finally, it recommends a possible procedure of integral production of personalized bone scaffold and bone graft. The presented so-called holistic approach announces a new systematic process of designing a personalized bone scaffold, which, although requiring a comprehensive consideration of complex requirements, is inevitable to make the designed solution applicable.
Solid Pseudopapillary Neoplasms Are Rare, Indolent Pancreatic Tumors in Young Women
Authors: Dalili Amin , Aliakbarian Mohsen , Karimi-Shahri Mehdi , Samadi Alireza , Raji Sara
Published: November 2020

Introduction. Solid pseudopapillary neoplasm (SPN) is a rare and indolent pancreatic tumor with low malignant potential which frequently occurs in reproductive-age females. Complete resection is almost always the curative option. Case Presentation. We present a 20-year-old woman with acute epigastric pain and vomiting in multiple episodes. Abdominal ultrasound showed a hypoechoic lesion with the probable source in the pancreas. Following that, CT scans and Endoscopic Ultrasound (EUS) manifested a

9
×
7.5
 
cm

-sized hypodense mass with heterogeneous well-defined margins in the pancreas suggesting the diagnosis of SPN. Whipple’s procedure was performed. Histopathological examination and immunohistochemistry confirmed SPN without evidence of malignancy. Discussion. SPN is known as a tumor with a favorable prognosis and a long survival rate after complete resection. However, some literature focused on minimally invasive surgery as an alternative surgical approach.
Study of the Stability of a Soil‐Rock Road Cutting Slope in a Permafrost Region of Hulunbuir
Authors: Zhao Yuxia , Feng Jun , Liu Kangqi , Xu Hongwei , Wang Liqun , Liu Hongyan
Published: November 2020

Due to the threat of global warming and the accelerated melting of glaciers and permafrost, the stability of slopes in permafrost regions has received an increasing amount of attention from scholars. However, research on the stability of soil‐rock road cutting slopes in high‐latitude and low‐altitude permafrost regions of the Greater Khingan Mountains in the Inner Mongolia Autonomous Region has not been reported. For this reason, a study of the stability of a slope with a high ice content in section K105 + 600 to K105 + 700 of National Highway 332 is conducted. The slope is 20 m high and the slope angle is 45°, and the risk of landslides on this slope under the action of freeze‐thaw erosion is very high. Because of this, field in situ monitoring, indoor freeze‐thaw tests, thermal parameter tests, and ABAQUS numerical simulation models are used to study the stability of the slope. After collecting the continuous temperature, moisture, settlement, and slope deformation data, it was found that the slope was undergoing dynamic changes. The creep of shallow slopes increased with the number of freeze‐thaw cycles. After approximately 150 freeze‐thaw cycles, the slope safety factor was less than 1, which means that the slope had reached the limit equilibrium state. Therefore, freeze‐thaw erosion greatly reduced the stability of the slope. Hence, the stability of the slope must be protected during its entire life cycle. This study provides a reference for the design and construction of road cutting slopes in the high‐latitude and low‐altitude permafrost regions of the Greater Khingan Mountains.