bluuebunny/crossref_metadata_2025_split huggingface dataset:
Language Kinship between Tulambatu and Tolaki Language in North Konawe
Authors:   Hanna,   Mursidin, Jannah Siti Nur Rochmatul 
Published: January 2018

Abstract
This study was intended to explore the genetic relationship between Tulambatu and Tolaki languages as members of Austronesian family language, particularly those included in the branch of Malay Polynesian sub-group. They have identical and similar lexis, phonetics, as well as corresponding phonemic and different phonemes. The aims of this study were: (1) to describe the level of genetic relationship between Tulambatu and Tolakinese languages in North Konawe regency, (2) to determine the period when the two languages were separated in terms of the basic vocabulary, (3) to predict the age of Tulambatu and Tolakinese languages in North Konawe regency. Data of the study were 200 vocabulary of Tulambatu and Tolakinese languages based on Swadesh lists that have been translated by native speakers of the two languages. The study was a historical comparative linguistics research and used the Lexicostatistics technique to find evidences that explain the genetic relationship of the languages. Based on the Lexicostatistics technique, it was found that the percentage of the vocabulary relationship of Tulambatu and Tolakinese languages was 52.02%. This proved that both languages are members of a sub-family of genetically similar languages (Astronesian Malayo Polinesian). In addition, it is believed that Tulambatu and Tolakinese languages were a single language 1636-1378 years ago, and they began to separate from their mother language around 379-637 AD (as of 2015).
Domestic and Social Violence against Women during the Egyptian Uprising
Authors: Wasef Nevine Henry 
Published: January 2018

AbstractThis study discusses how social and domestic violence against women increased during the period of political violence represented by the Egyptian Uprising of the 25thof January 2011. In this paper, the term political violence had been defined as any use of force practiced by governmental or anti-governmental groups to achieve political goals. Many scholars use the terms political violence and political instability interchangeably while the latter refers to a situation when a government had been toppled which was found to be strongly affiliated with political violence. Political violence includes uprisings and political transition of authority. Social violence is associated with sexual harassment, social norms and gender roles. Domestic violence refers to any physical harm among family members against women and domestic practices like early marriage and female circumcision. The article discusses first how the three types of violence interact and affect one another. The study in turn researches the increase of domestic violence rate against women in reaction to the political conflict resulting from the Egyptian Uprising of January 25th, 2011 through conducting interviews with abused women to investigate how the Egyptian Uprising had affected them socially and domestically. The study concludes that political violence had a direct impact on social and domestic violence against women.
Minimization of Delay Costs in the Realization of Production Orders in Two-Machine System
Authors: Dylewski Robert , Jardzioch Andrzej , Dworak Oliver 
Published: January 2018

Abstract
The article presents a new algorithm that enables the allocation of the optimal scheduling of the production orders in the two-machine system based on the minimum cost of order delays. The formulated algorithm uses the method of branch and bounds and it is a particular generalisation of the algorithm enabling for the determination of the sequence of the production orders with the minimal sum of the delays. In order to illustrate the proposed algorithm in the best way, the article contains examples accompanied by the graphical trees of solutions. The research analysing the utility of the said algorithm was conducted. The achieved results proved the usefulness of the proposed algorithm when applied to scheduling of orders. The formulated algorithm was implemented in the Matlab programme. In addition, the studies for different sets of production orders were conducted.
Boosting the Performance of SLS and CDCL Solvers by Preprocessor Tuning
Authors: Balint Adrian , Manthey Norbert 
Published: January 2018

Preprocessing techniques are crucial for SAT solvers when it comes to reaching state-of-the-art performance as it was shown by the results of the last SAT Competitions. Theusefulness of a preprocessing technique depends highly on its own parameters, on the in-stances on which it is applied and on the used solver. In this paper we first give an extendedanalysis of the performance gain reached by using different preprocessing techniques in-dividually in combination with CDCL solvers on application instances and SLS solverson crafted instances. Further, we provide an analysis of combinations of preprocessingtechniques by means of automated algorithm configuration, where we search for optimalpreprocessor configurations for different scenarios. Our results show that the performanceof CDCL and especially of SLS solvers can be further improved when using appropriatepreprocessor configurations. The solvers augmented with the best found preprocessingconfigurations outperform the original solvers on the instances from the SAT Challenge2012, achieving new state-of-the-art results.
Closing the Gap Between Specification and Programming: VDM++ and Scala
Authors: Havelund Klaus 
Published: January 2018

We argue that a modern programming language such as Scala offers a level of succinctness, which makes it suitable for program and systems specification as well as for high-level programming. We illustrate this by comparing the language with the VDM++ specification language. The comparison also identifies areas where Scala perhaps could be improved, inspired by VDM++. We furthermore illustrate Scala's potential as a specification language by augmenting it witha combination of parameterized state machines and temporal logic, defined as a library, thereby forming an expressive but simple runtime verification framework.
Proof theory for lattice-ordered groups
Authors: Metcalfe George 
Published: January 2018

Proof theory can provide useful tools for tackling problems in algebra. In particular, Gentzen systems admitting cut-eliminationhave been used to establish decidability, complexity, amalgamation, admissibility, and generation results for varieties of residuated lattices corresponding to substructural logics. However, for classes of algebras bearing some family resemblance to groups, such as lattice-ordered groups, MV-algebras, BL-algebras, and cancellative residuated lattices, the proof-theoretic approach has met so far only with limited success.The main aim of this talk will be to introduce proof-theoretic methods for the class of lattice-ordered groups and to explain how these methods can be used to obtain new syntactic proofs of two core theorems: namely, Holland's result that this class is generated as a variety by the lattice-ordered group of order-preserving automorphisms of the real numbers, and the decidability of the word problem for free lattice-ordered groups.
The Frame Problem and the Semantics of Classical Proofs
Authors: White Graham 
Published: January 2018

We outline the logic of current approaches to the so-called``frame problem'' (that is, the problem of predicting change in thephysical world by using logical inference), and we show thatthese approaches are not completely extensional sincenone of them is closed under uniform substitution. The underlying difficultyis something known, in the philosophical community, as Goodman's``new riddle of induction'' or the ``Grue paradox''. Although it seems, from the philosophical discussion, that this paradox cannot be solved in purely a priori terms and that a solution will require some form of real-world data, it nevertheless remains obscure both what the logical form of this real-world data might be, and also how this data actually interacts with logical deduction. We show, using work of McCain and Turner, that this data can be captured using the semantics of classical proofs developed by Bellin, Hyland and Robinson, and, consequently, that the appropriate arena for solutions of the frame problem lies in proof theory. We also give a very explicit model for the categorical semantics of classical proof theory using techniques derived from work on the frame problem.
Towards a Reliable Formal Framework for Enhancing Risk Assessment in Access Control Systems
Authors: Evina Pierrette Annie , Labbene Ayachi Faten , Jaidi Faouzi , Bouhoula Adel 
Published: January 2018

The constant evolution of access control requirements and the dynamic environment in which they evolve require nowadays quick and instant decision-making related to risk of illegitimate access in Information Systems. Various contributions defined in the literature aim to overcome or to mitigate related risks and paradoxically adopted the hypothesis of reliability and validity of access control policies. However, the corruption of these policies is a security aspect of great importance and should be handled actively because (i) an access control policy is also exposed to the same threats as the managed data is and (ii) properties and parameters of the concrete policy at a given stage may differ, in a critical manner, from a reference stage. We define a reliable and complete solution for risk management in the context of Database Servers. We intend to define a rigorous risk management approach that mainly verifies recommendations of the standard ISO 31000:2009. Our approach takes into consideration all identified threats on a Database Server and provides an environment for the analysis of the correlationbetween the threats detected in particular by different security devices.To ensure a high level of surety, we opt for defining a formal framework that allows to efficiently address this problematic and to formally represent and verify our risk managementprocesses.
Nonlinear Hybrid Automata Model of Excitable Cardiac Tissue
Authors: Abbas Houssam , Jang Kuk Jin , Mangharam Rahul 
Published: January 2018

Implantable cardiac devices like pacemakers and defibrillators are life-saving medical devices.To verify their functionality, there is a need for heart models that can simulate interesting phenomena and are relatively computationally tractable.In this benchmark we implement a model of the electrical activity in excitable cardiac tissue as a network of nonlinear hybrid automata.The model has previously been shown to simulate fast arrhythmias.The hybrid automata are arranged in a square n-by-n grid and communicate via their voltages.Our Matlab implementation allows the user to specify any size of model n, thus rendering it ideal for benchmarking purposes since we can study tool efficiency as a function of size.We expect the model to be used to analyze parameter ranges and network connectivity that lead to dangerous heart conditions.It can also be connected to device models for device verification.
A new Glivenko Theorem
Authors: Alizadeh Majid , Ardeshir Mohammad , Ruitenburg Wim 
Published: January 2018

We generalize the double negation construction of Boolean algebras in Heytingalgebras, to a double negation construction of the same in Visser algebras (alsoknown as basic algebras).This result allows us to generalize Glivenko's Theorem from intuitionisticpropositional logic and Heyting algebras to Visser's basic propositional logicand Visser algebras.
Why Attackers Lose: Design and Security Analysis of Arbitrarily Large XOR Arbiter PUFs
Authors: Wisiol Nils , Graebnitz Christoph , Margraf Marian , Oswald Manuel , Soroceanu Tudor , Zengin Benjamin 
Published: January 2018

In a novel analysis, we show that arbitrarily many Arbiter PUFs can be combined into a stable XOR Arbiter PUF. To the best of our knowledge, this design cannot be modeled by any known oracle access attack in polynomial time.Using majority vote of Arbiter Chain responses, our analysis shows that with a polynomial number of votes the XOR Arbiter PUF stability of almost all challenges can be boosted exponentially close to 1; that is, the stability gain through majority voting can exceed the stability loss introduced by large XORs for a feasible number of votes. Hence, our proposal enables the designer to increase the attacker's effort exponentially while still maintaining polynomial design effort for all known oracle access modeling attacks. This is the first result that relates PUF design to this traditional cryptographic design principle.
Heliostat Field Layout Optimization with Evolutionary Algorithms
Authors: Richter Pascal , Laukamp David , Gerdes Levin , Frank Martin , Ábrahám Erika 
Published: January 2018

The exploitation of solar power for energy supply is of increasing importance. While technical development mainly takes place in the engineering disciplines, computer science offers adequate techniques for optimization. This work addresses the problem of finding an optimal heliostat field arrangement for a solar tower power plant.We propose a solution to this global, non-convex optimization problem by using an evolutionary algorithm. We show that the convergence rate of a conventional evolutionary algorithm is too slow, such that modifications of the recombination and mutation need to be tailored to the problem. This is achieved with a new genotype representation of the individuals.Experimental results show the applicability of our approach.
Implementation of Incremental Learning in Artificial Neural Networks
Authors: Andrade Mariela , Gasca Eduardo , Rendón Eréndira 
Published: January 2018

Nowadays, the use of artificial neural networks (ANN), in particular the Multilayer Perceptron (MLP), is very popular for executing different tasks such as pattern recognition, data mining, and process automation. However, there are still weaknesses in these models when compared with human capabilities. A characteristic of human memory is the ability for learning new concepts without forgetting what we learned in the past, which has been a disadvantage in the field of artificial neural networks. How can we add new knowledge to the network without forgetting what has already been learned, without repeating the exhaustive ANN process? In an exhaustively training is used a complete training set, with all objects of all classes.In this work, we present a novel incremental learning algorithm for the MLP. New knowledge is incorporated into the target network without executing an exhaustive retraining. Objects of a new class integrate this knowledge, which was not included in the training of a source network. The algorithm consists in taking the final weights from the source network, doing a correction of these with the Support Vector Machine tools, and transferring the obtained weights to a target network. This last net is trained with a training set that it is previously preprocessed. The efficiency resulted of the target network is comparable with a net that is exhaustively trained.
Parametric Strategy Iteration
Authors: Seidl Helmut , Gawlitza Thomas Martin , Schwarz Martin 
Published: January 2018

Program behavior may depend on parameters, which are either configuredbefore compilation time, or provided at runtime, e.g., by sensors or other input devices.Parametric program analysis explores how different parameter settings may affect theprogram behavior.In order to infer invariants depending on parameters, we introduce parametric strategy iteration.This algorithm determines the precise least solution of systems of integer equations dependingon surplus parameters. Conceptually, our algorithm performs ordinary strategy iterationon the given integer system for all possible parameter settings in parallel.This is made possible by means of region trees to represent the occurring piecewise affine functions.We indicate that each required operation on these trees is polynomial-time if only constantly manyparameters are involved.Parametric strategy iteration for systems of integer equationsallows to construct parametric integer interval analysisas well as parametric analysis of differences of integer variables.It thus provides a general technique to realize precise parametricprogram analysis if numerical properties of integer variables are of concern.
On the Expressiveness of some Runtime Validation Techniques
Authors: Falcone Yliès , Fernandez Jean-Claude , Laurent Mounier 
Published: January 2018

Runtime validation techniques have been proposed as artifacts to detect and/or correct unforeseen behaviours of computer systems.Their common features is to give only partial validation results, based on a restricted set of system executions produced in the real execution environment. A key issue is thus to better understand which kind of properties can (or cannot) be validated using such techniques.We focus on three techniques known as runtime verification, property-oriented testing, and runtime enforcement. We present these approaches at an abstract level and in a unified framework, and we discuss their respective ability to deal with properties on infinite execution sequences, that are commonly encountered in many application domains.
A refutation procedure for proving satisfiability of constraint specifications on XML documents
Authors: Navarro Marisa , Orejas Fernando 
Published: January 2018

In this paper we first present three sorts of constraints (positive, negative and conditional ones) to specify that certain patterns must be satisfied in a XML document. These constraints are built on boolean XPath patterns. We define a specification as a set of clauses whose literals are constraints.Then, to reason about these specifications, we study some sound rules which permit to infer, subsume or simplify clauses. The main goal is to design a refutation procedure (based on these rules) to test if a given specification is satisfiable or not. We have formally proven the soundness of our procedure and we study the completeness and termination of the proposed method.
Modern Cooperative Parallel SAT Solving
Authors: Manthey Norbert , Lanti Davide , Irfan Ahmed 
Published: January 2018

Nowadays, powerful parallel SAT solvers are based on an algorithm portfolio. Thealternative approach, (iterative) search space partitioning, cannot keep up, although, ac-cording to the literature, iterative partitioning systems should scale better than portfoliosolvers. In this paper we identify key problems in current parallel cooperative SAT solvingapproaches, most importantly communication, how to partition the search space, and howto utilize the sequential search engine. First, we improve on each problem separately. Ina further step, we show that combining all the improvements leads to a state-of-the-artparallel SAT solver, which does not use the portfolio approach, but instead relies on it-erative partitioning. The experimental evaluation of this system completely changes thepicture about the performance of search space partitioning SAT solvers: on instances ofa combined benchmark of recent SAT competitions, the presented approach can keep upwith the winners of last years SAT competition. The combined improvements improve theexisting cooperative solver splitter by 24%: instead of 561 out of 880 instances, the newsolver Pcasso can solve 696 instances.
Unifying Equivalences for Timed Transition Systems
Authors: Virbitskaite Irina , Gribovskaya Natalya , Best Eike 
Published: January 2018

Timed transition systems are a widely studied model for real-time systems.The intention of the paper is to show how several categorical (open maps, path-bisimilarity and coalgebraic) approaches to an abstract characterization ofbisimulation relate to each other and to the numerous suggested behavioral equivalences of linear time -- branching time spectrum, in the setting of timed transition systems.
The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics
Authors: Arhami Negin , Sutcliffe Geoff 
Published: January 2018

Many Automated Theorem Prover (ATP) systems for different logics, andtranslators for translating different logics from one to another, havebeen developed and are now available.Some logics are more expressive than others, and it is easier to expressproblems in those logics.On the other hand, the ATP systems for less expressive logics have beenunder development for many years, and are more powerful and reliable.There is a trade-off between expressivity of a logic, and the power andreliability of the available ATP systems.Translators and ATP systems can be combined to try to solvea problem.In this research, an experiment has been carried out to compare theperformance of difference combinations of translators and ATP systems.
Ping-Pong Protocols as Prefix Grammars and Turchin Relation
Authors: Nepeivoda Antonina 
Published: January 2018

The paper describes how to verify cryptographic protocols by a general-purpose programtransformation technique with unfolding. The questions of representation and analysisof the protocols as prefix rewriting grammars are discussed. In these aspects Higman andTurchin embeddings on computational paths are considered, and a refinement of Turchin’srelation is presented that allows to algorithmically decide the empty word problem forprefix rewriting grammars.
On Unfolding for Programs Using Strings as a Data Type
Authors: Nemytykh Andrei 
Published: January 2018

As a rule, program transformation methods based on semantics unfolda semantic tree of a given program. Sometimes that allows to optimize the program or to prove its certain properties automatically.Unfolding is one of the basic operations, which is a meta-extension of one step of the abstract machine executing the program.This paper is interested in unfolding for programs based on pattern matching and manipulating the strings. The corresponding computation model originates from Markov's normal algorithms and extends this theoretical base.Even though algorithms unfolding programs were being intensively studied for a long time in the context of variety of programming languages, as far as we know, the associative concatenation was stood at the wayside of the stream.We define a class of term rewriting systems manipulating with strings anddescribe an algorithm unfolding the programs from the class. The programming language defined by this class is algorithmic complete.Given a word equation, one of the algorithms suggested in this paper results in a description of the corresponding solution set.
Abstract Interpretation over Zones without Widening
Authors: Gawlitza Thomas Martin , Seidl Helmut 
Published: January 2018

We present a practical algorithm for computing leastsolutions of systems of (fixpoint-)equations over the integers with,besides other monotone operators,addition, multiplication by positive constants, maximum, and minimum.The algorithm is based on max-strategy iteration.Its worst-case running-time (w.r.t. a uniform cost measure)is independent of the sizes of occurring numbers.We apply thisalgorithm to compute the abstract semantics ofprograms over integer intervals as well as over integer zones.