bluuebunny/crossref_metadata_2025 huggingface dataset:
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.
BliStr: The Blind Strategymaker
Authors: Urban Josef
Published: January 2018

BliStr is a system that automatically develops strong targetted theorem-proving strategies for the E prover on a large set of diverse problems. The main idea is to interleave (i) iterated low-timelimit local search for new strategies on small sets of similar easy problems with (ii) higher-timelimit evaluation of the new strategies on all problems. The accumulated results of the global higher-timelimit runs are used to define and evolve the notion of "similar easy problems'", and to control the evolution of the next strategy. The technique significantly strengthened the set of E strategies used by the MaLARea, E-MaLeS, and E systems in the CASC@Turing 2012 competition, particularly in the Mizar division. Similar improvement was obtained on the problems created from the Flyspeck corpus.
A Design Space and its Patterns: Modelling 2phase Asynchronous Pipelines
Authors: Birtwistle Graham , Stevens Kenneth S.
Published: January 2018

We present a systematic way of studying state machine based design spaces and apply it to the study of asynchronous pipelines. Starting with the specification of the most concurrent behaviour as a state machine, all possible valid smaller designs may be generated by systematically removing structured patterns of output states (C cuts) and input states (R cuts). Taking the cartesian product of cuts C X R yields the complete design space which may then be partitioned according to well understood design styles. In this paper we extend previous results by studying mixed asynchronous pipelines of which homogeneous behaviours form a subset. The approach is presented using the much smaller 2phase setting (3 X 6) but the insights and structures revealed carry over to full 4phase designs (35 X 140). We present a complete overview of mixed 2phase linear pipeline behaviours; show how their structuring C cuts and R cuts relate; characterise the behaviours of linear pipelines in terms of these cuts for any depth; and show how the much larger R mixed behaviour patterns can be calculated from knowledge of the C behaviour patterns. Applications of the theory cover mixed linear pipeline and ring behaviours and the automatic generation of quality circuits from our specifications.
Reachability Analysis of Transformer-Isolated DC-DC Converters
Authors: Beg Omar , Davoudi Ali , Johnson Taylor T.
Published: January 2018

Various mission-critical applications necessarily require a transformer in switching converters to obtain DC isolation between the converters’ input and output. Since DC-DC converters are the switching devices, these are modeled as hybrid automata. We present hybrid automaton modeling of two main types of transformer isolated DC-DC converters, namely, flyback and forward converters. We have also catered the non-determinism for both. We use HyST (Hybrid Source Transformation) tool to automatically generate the models in SpaceEx format, perform reachability analysis, and then automatically convert the models into Mathworks Simulink Stateflow (SLSF) using HyST. Thus we demonstrate effectiveness of HyST tool in the model-based design process. The HyST user needs not to manually construct or modify the models thus saving significant amount of time and efforts.
Craig Interpolation for the Integers: Results, Implementation, and Experiences
Authors: Rümmer Philipp
Published: January 2018

Craig interpolation is a versatile tool in formal verification, in particular for generating intermediate assertions in safety analysis and model checking. Over the last years, a variety of interpolation procedures for linear integer arithmetic (and extensions) have been developed. I will give an overview of the existing algorithms and design choices, and then discuss implementations of such procedures within theorem provers and SMT solvers. In particular, I will describe an implementation done using the multi-paradigm language Scala, which is built on top of the Java runtime infrastructure, and evaluate performance and engineering aspects.
Rewriting and Well-Definedness within a Proof System
Authors: Maamria Issam , Butler Michael
Published: January 2018

Term rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving between deduction and computation (i.e., rewriting) steps. If the logic of reasoning supports partial functions, it is necessary that rewriting copes with potentially ill-defined terms. In this paper, we provide a basis for integrating rewriting with a deductive proof system that deals with well-definedness. The definitions and theorems presented in this paper are the theoretical foundations for an extensible rewriting-based prover that has been implemented for the set theoretical formalism Event-B.
Parametric Strategy Iteration
Authors: Seidl Helmut , Gawlitza Thomas Martin , Schwarz Martin
Published: January 2018

Program behavior may depend on parameters, which are either configured

before compilation time, or provided at runtime, e.g., by sensors or other input devices.

Parametric program analysis explores how different parameter settings may affect the

program 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 depending

on surplus parameters. Conceptually, our algorithm performs ordinary strategy iteration

on 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 many

parameters are involved.

Parametric strategy iteration for systems of integer equations

allows to construct parametric integer interval analysis

as well as parametric analysis of differences of integer variables.

It thus provides a general technique to realize precise parametric

program analysis if numerical properties of integer variables are of concern.
Note on Deduction Theorems in Contraction-Free Logics
Authors: Chvalovský Karel , Cintula Petr
Published: January 2018

In this short paper we present a finer analysis of the variants of Local Deduction Theorem in contraction-free logics. We define some natural generalisations called Implicational Deduction Theorems and study their basic properties. The hierarchy of classes of logics defined by these theorems is presented.
Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs
Authors: Kuntz Matthias , Leue Stefan , Scheben Christoph
Published: January 2018

Currently, there are no approaches known that allow for non-termination proofs of concurrent programs which account for asynchronous communication via FIFO message queues. Those programs may be written in high-level languages such as Java or Promela. We present a ﬁrst approach to prove non-termination for such programs. In addition to integers, the programs that we consider may contain queues as data structures. We present a representation of queues and the operations on them in the domain of integers, and generate invariants that help us prove non-termination of selected control ﬂow loops using a theorem proving approach. We illustrate this approach by applying a prototype tool implementation to a number of case studies.
Idempotent generated algebras and Boolean powers of commutative rings
Authors: Bezhanishvili Guram , Marra Vincenzo , Morandi Patrick J. , Olberding Bruce
Published: January 2018

For a commutative ring R, we introduce the notion of a Specker R-algebra and show that Specker R-algebras are Boolean powers of R. For an indecomposable ring R, this yields an equivalence between the category of Specker R-algebras and the category of Boolean algebras. Together with Stone duality this produces a dual equivalence between the category of Specker R-algebras and the category of Stone spaces.
Tableau Calculus for Dummett Logic Based on Present and Next State of Knowledge
Authors: Fiorino Guido
Published: January 2018

In this paper we use the Kripke semantics characterization of Dummett logic to introduce a new way of handling non-forced formulas in tableau proof systems. We pursue the aim of reducing the search space by strictly increasing the number of forced propositional variables after the application of non-invertible rules. The focus of the paper is on a new tableau system for Dummett logic, for which we have an implementation. The ideas presented can be extended to intuitionistic logic and intermediate logics as well.
Relational groupoids and residuated lattices
Authors: Guido Cosimo
Published: January 2018

A quite general order-theoretical approach to implicative structures leads to consider implicative groupoids, which form a wide class of algebras including residuated lattices and their reasonable generalizations. Implicative groupoids find out to be special instances of suitable relational systems and are objects of categories, semicategories and precategories whose morphisms are generalizations of Galois connections.
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. The

alternative approach, (iterative) search space partitioning, cannot keep up, although, ac-

cording to the literature, iterative partitioning systems should scale better than portfolio

solvers. In this paper we identify key problems in current parallel cooperative SAT solving

approaches, most importantly communication, how to partition the search space, and how

to utilize the sequential search engine. First, we improve on each problem separately. In

a further step, we show that combining all the improvements leads to a state-of-the-art

parallel SAT solver, which does not use the portfolio approach, but instead relies on it-

erative partitioning. The experimental evaluation of this system completely changes the

picture about the performance of search space partitioning SAT solvers: on instances of

a combined benchmark of recent SAT competitions, the presented approach can keep up

with the winners of last years SAT competition. The combined improvements improve the

existing cooperative solver splitter by 24%: instead of 561 out of 880 instances, the new

solver Pcasso can solve 696 instances.
Formally Proving the Boolean Pythagorean Triples Conjecture
Authors: Cruz-Filipe Luís , Schneider-Kamp Peter
Published: January 2018

In 2016, Heule, Kullmann and Marek solved the Boolean Pythagorean Triples problem: is there a binary coloring of the natural numbers such that every Pythagorean triple contains an element of each color? By encoding a finite portion of this problem as a propositional formula and showing its unsatisfiability, they established that such a coloring does not exist. Subsequently, this answer was verified by a correct-by-construction checker extracted from a Coq formalization, which was able to reproduce the original proof. However, none of these works address the question of formally addressing the relationship between the propositional formula that was constructed and the mathematical problem being considered. In this work, we formalize the Boolean Pythagorean Triples problem in Coq. We recursively define a family of propositional formulas, parameterized on a natural number n, and show that unsatisfiability of this formula for any particular n implies that there does not exist a solution to the problem. We then formalize the mathematical argument behind the simplification step in the original proof of unsatisfiability and the logical argument underlying cube-and-conquer, obtaining a verified proof of Heule et al.’s solution.
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 of

bisimulation relate to each other and to the numerous suggested behavioral equivalences of linear time -- branching time spectrum, in the setting of timed transition systems.
Cooperation in Adaptive Multi-Agent Systems through System of Systems modeling
Authors: Bouziat Teddy , Camps Valérie , Combettes Stéphanie
Published: January 2018

This paper addresses the modeling and design of Systems of Systems (SoS) as well as inter multi-agent systems cooperation. It presents and illustrates a new generic model to describe formally SoS. Then, this model is used to propose a study of inter-AMAS (Adaptive Multi-Agent System) cooperation. Each AMAS, reified as a component-system of a SoS, uses a cooperative decision process in order to interact with other AMAS and to collectively give rise to a relevant overall function at the SoS level. The proposed model as well as the inter-AMAS study are instantiated to a simulated resources transportation problem.
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, and

translators for translating different logics from one to another, have

been developed and are now available.

Some logics are more expressive than others, and it is easier to express

problems in those logics.

On the other hand, the ATP systems for less expressive logics have been

under development for many years, and are more powerful and reliable.

There is a trade-off between expressivity of a logic, and the power and

reliability of the available ATP systems.

Translators and ATP systems can be combined to try to solve

a problem.

In this research, an experiment has been carried out to compare the

performance of difference combinations of translators and ATP systems.
Using S-TaLiRo on Industrial Size Automotive Models
Authors: Hoxha Bardh , Abbas Houssam , Fainekos Georgios
Published: January 2018

In Model Based Development (MBD) of embedded systems, it is often desirable to verify or falsify certain formal specifications. In some cases it is also desirable to find the range of specification parameters for which the specification does not hold on the system. We illustrate these methods on a challenge problem from the automotive industry on a high-fidelity, industrial scale engine model.
Extensions of ordering sets of states from effect algebras onto their MacNeille completions
Authors: Janda Jiří , Riečanová Zdenka
Published: January 2018

In [Riečanová Z, Zajac M.: Hilbert Space Effect-Representations of Effect Algebras] it was shown that an effect algebra E with an ordering set M of states can by embedded into a Hilbert space effect algebra E(l2(M)). We consider the problem when its effect algebraic MacNeille completion Ê can be also embedded into the same Hilbert space effect algebra E(l2(M)). That is when the ordering set M of states on E can be be extended to an ordering set of states on Ê. We give an answer for all Archimedean MV-effect algebras and Archimedean atomic lattice effect algebras.
A Clausal Normal Form Translation for FOOL
Authors: Kotelnikov Evgenii , Kovács Laura , Suda Martin , Voronkov Andrei
Published: January 2018

Automated theorem provers for first-order logic usually operate on sets of first-order clauses. It is well-known that the translation of a formula in full first-order logic to a clausal normal form (CNF) can crucially affect performance of a theorem prover. In our recent work we introduced a modification of first-order logic extended by the first class boolean sort and syntactical constructs that mirror features of programming languages. We called this logic FOOL. Formulas in FOOL can be translated to ordinary first-order formulas and checked by first-order theorem provers. While this translation is straightforward, it does not result in a CNF that can be efficiently handled by state-of-the-art theorem provers which use superposition calculus. In this paper we present a new CNF translation algorithm for FOOL that is friendly and efficient for superposition-based first-order provers. We implemented the algorithm in the Vampire theorem prover and evaluated it on a large number of problems coming from formalisation of mathematics and program analysis. Our experimental results show an increase of performance of the prover with our CNF translation compared to the naive translation.
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 program

transformation technique with unfolding. The questions of representation and analysis

of the protocols as prefix rewriting grammars are discussed. In these aspects Higman and

Turchin embeddings on computational paths are considered, and a refinement of Turchin’s

relation is presented that allows to algorithmically decide the empty word problem for

prefix rewriting grammars.
The Soul of a New Cliché: Conventions and Meta-Conventions in the Creative Linguistic Variation of Familiar Forms
Authors: Veale Tony
Published: January 2018

Creativity – whether in humans or machines – is more than a matter of simple creation. To be “creative” implies an ability to do more than invent, but an ability to recognize and appreciate the inventions of others. After all, the ability to recognize surprising value in the efforts of others is the same ability we use to guide our own creative efforts. Solipsistic creativity is rare indeed, and most creativity relies on an audience that is creative enough to value our efforts. Of what value is an ability to e.g. speak ironically if we cannot also understand or appreciate the irony of others? The goal of imbuing computers with creative abilities must thus include a sub-goal of enabling computers to recognize and respond appropriately to the creativity of others. As computers are increasingly used to analyze the burgeoning texts of the world-wide-web, the ability to automatically detect and analyze the linguistic creativity of speakers has become more important than ever. In this paper we consider how speakers engage creatively with cliché, to achieve creative ends through the novel variation of familiar linguistic forms. Our computational analysis of a large collection of linguistic patterns on the Web shows that speakers are surprisingly conservative in their variation strategies, and novelty alone rarely leads to creativity. This conformity can make it easier for computers to detect when speakers are using familiar language in truly original ways.
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 unfold

a 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 and

describe 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.
Unication Problems Modulo a Theory of Until
Authors: Brahmakshatriya Shreyaben , Danturi Sushma , Gero Kimberly , Narendran Paliath
Published: January 2018

Our main aim in this paper is to investigate an equational theory consisting of a number of identities or equivalences in Linear Temporal Logic (LTL) with the “until” operator U, but without the “next-time” operator. We investigate unification problems modulo this theory. Two variants of unification are also studied, namely asymmetric unification and disunification. Our main focus is on algorithmic complexity.
Authorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning
Authors: Crampton Jason , Huth Michael , Kuo Jim Huan-Pu
Published: January 2018

We investigate automated reasoning techniques as a means of supporting authorization enforcement functions of security-aware workflow management systems. The aim of such support is that one may statically or dynamically guarantee the realizability of a workflow instance given the security constraints of the underlying workflow specification. We develop two such automated reasoning methods and experimentally evaluate their suitability for giving such support. One method uses a propositional encoding of realizability implemented through binary decision diagrams, another method uses a linear-time temporal logic encoding implemented via bounded model checking. Preliminary experimental results identify issues of scalability and of balancing flexibility in task allocation with complexity of computing such allocations.
Origami folds in higher-dimension
Authors: Ida Tetsuo , Watt Stephen
Published: January 2018

We present a generalization of mathematical origami to higher dimensions. We briefly explain Huzita- Justin’s axiomatic treatment of mathematical origami. Then, for concreteness, we apply it to origami on 3-dimensional Euclidean space in which the fold operation consists of selecting a half-plane and reflect- ing one half-plane across it. We finally revisit the subject from an n-dimensional point of view.
General Topos Semantics for Higher-Order Modal Logic
Authors: Awodey Steve , Kishida Kohei , Kotzsch Hans-Christoph
Published: January 2018

Topos-theoretic semantics for modal logic usually uses structures induced by a surjective geometric morphism between toposes. This talk develops an algebraic generalization of this framework. We take internal adjoints between certain internal frames within a topos, which provides semantics for (intuitionistic) higher-oder modal logic.
A Theory of Arrays with set and copy Operations
Authors: Falke Stephan , Sinz Carsten , Merz Florian
Published: January 2018

The theory of arrays is widely used in order to model main memory in program analysis, software verification, bounded model checking, symbolic execution, etc. Nonetheless, the basic theory as introduced by McCarthy is not expressive enough for important practical cases since it only supports array updates at single locations. In programs, the memory is often modified using functions such as memset or memcpy/memmove, which modify a user-specified range of locations whose size might not be known statically. In this paper we present an extension of the theory of arrays with set and copy operations which make it possible to reason about such functions. We also discuss further applications of the theory.
Abstract Interpretation over Zones without Widening
Authors: Gawlitza Thomas Martin , Seidl Helmut
Published: January 2018

We present a practical algorithm for computing least

solutions 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 this

algorithm to compute the abstract semantics of

programs over integer intervals as well as over integer zones.
Molecular computations with competitive neural networks that exploit linear and nonlinear kinetics
Authors: Genot Anthony J. , Fujii Teruo , Rondelez Yannick
Published: January 2018

We show how to exploit enzymatic saturation -an ubiquitous nonlinear effects in biochemistry- in order to process information in molecular networks. The networks rely on the linearity of DNA strand displacement and the nonlinearity of enzymatic replication. We propose a pattern-recognition network that is compact and should be robust to leakage.
Feature Selection Ensemble
Authors: Shen Qiang , Diao Ren , Su Pan
Published: January 2018

Many strategies have been exploited for the task of feature selection, in an effort to identify more compact and better quality feature subsets. Such techniques typically involve the use of an individual feature significance evaluation, or a measurement of feature subset consistency, that work together with a search algorithm in order to determine a quality subset. Feature selection ensemble aims to combine the outputs of multiple feature selectors, thereby producing a more robust result for the subsequent classifier learning tasks. In this paper, three novel implementations of the feature selection ensemble concept are introduced, generalising the ensemble approach so that it can be used in conjunction with many subset evaluation techniques, and search algorithms. A recently developed heuristic algorithm: harmony search is employed to demonstrate the approaches. Results of experimental comparative studies are reported in order to highlight the benefits of the present work. The

paper ends with a proposal to extend the application of feature selection ensemble to aiding the development of biped robots (inspired by the authors’ involvement in the joint celebration of Olympic and the centenary of the birth of Alan Turing).
Checkable Proofs for First-Order Theorem Proving
Authors: Reger Giles , Suda Martin
Published: January 2018

Inspired by the success of the DRAT proof format for certification of boolean satisfiability (SAT),

we argue that a similar goal of having unified automatically checkable proofs should be sought

by the developers of automated first-order theorem provers (ATPs). This would not only

help to further increase assurance about the correctness of prover results,

but would also be indispensable for tools which rely on ATPs,

such as ``hammers'' employed within interactive theorem provers.

The current situation, represented by the TSTP format is unsatisfactory,

because this format does not have a standardised semantics and thus cannot be checked automatically.

Providing such semantics, however, is a challenging endeavour. One would ideally

like to have a proof format which covers only-satisfiability-preserving operations such as Skolemisation

and is versatile enough to encompass various proving methods (i.e. not just superposition)

or is perhaps even open ended towards yet to be conceived methods or at least easily extendable in principle.

Going beyond pure first-order logic to theory reasoning in the style of SMT or

beyond proofs to certification of satisfiability are further interesting challenges.

Although several projects have already provided partial solutions in this direction,

we would like to use the opportunity of ARCADE to further promote the idea and

gather critical mass needed for its satisfactory realisation.
Cauliflower: a Solver Generator for Context-Free Language Reachability
Authors: Hollingum Nicholas , Scholz Bernhard
Published: January 2018

Context-free language reachability (CFL-R) is a fundamental solving vehicle for computing essential compiler optimisations and static program analyses. Unfortunately, solvers for CFL- R encounter both inherently expensive problem formulations and frequent alterations to the underlying formalism. As such, tool designers are forced to create custom-tailored implementations with long development times and limited reusability. A better framework is crucial to facilitate research and development in CFL-R.

In this work we present Cauliflower, a CFL-R solver generator, that creates parallel executable C++ code from an input CFL-R rule-based specification. With Cauliflower, developers create working tools rapidly, avoiding lengthy and error-prone manual implementations. Cauliflower’s domain-specific language provides semantic extension including reversal, branch- ing, disconnection and templating. In practical experiments, Cauliflower achieves an average speedup of 1.8x compared with the best general purpose tools, and matches the performance of application-specific tools on many benchmarks.
Hybrid Modelling of a Wind Turbine
Authors: Schuler Simone , Daher Adegas Fabiano , Anta Adolfo
Published: January 2018

This paper proposes a simplified nonlinear model of a wind turbine equipped with a switching controller. The composition of wind turbine and controller results in a hybrid system. The control of such a system and the enforcement of numerous safety and performance constraints constitute a relevant benchmark to evaluate tools for proving safety requirements in hybrid systems.
Towards an amortized type system for JavaScript
Authors: Franzen Daniel , Aspinall David
Published: January 2018

JavaScript programs have access to a wide range of resources and many of those have security implications.

Tight bounds on the consumption of those resources can give indication of the functionality provided by the

program and minimize the security risks of mobile applications. Resource consumption is typically dependent

on the input of the user.

In this paper we introduce an amortized type system for a core of JavaScript. The resulting types certify

bounds for the resource usage dependent on the input parameters. We define the amortized types and the

corresponding typing rules. Furthermore we discuss how to fully automatically infer those resource bounds for

arbitrary applications. In addition to the usual example of amortized resource, heap-space, our type system

can be applied to many phone specific resources, which we demonstrate using the example of the GPS sensor

and others.

The main result of this paper is the soundness of the core type system, proving that a valid type for a program

corresponds to a bound on the units used of the specified resource.
Algorithmic correspondence for intuitionistic modal mu-calculus, Part 1
Authors: Conradie Willem , Fomatati Yves , Palmigiano Alessandra , Sourabh Sumit
Published: January 2018

The algorithmic correspondence theory is extended to mu-calculi with a non-classical base. We focus in particular on the language of bi-intuitionistic modal mu-calculus, and we enhance the algorithm, or calculus for correspondence, ALBA for the elimination of monadic second order variables, so as to guarantee its success over a class including the Sahlqvist mu-formulas. Key to the soundness of this enhancement are the order-theoretic properties of the algebraic interpretation of the fixed point operators.
The finite embeddability property for some noncommutative knotted extensions of FL
Authors: Cardona Riquelmi
Published: January 2018

We consider the knotted structural rule xm≤xn for n different than m and m greater or equal than 1. Previously van Alten proved that commutative residuated lattices that satisfy the knotted rule have the finite embeddability property (FEP). Namely, every finite partial subalgebra of an algebra in the class can be embedded into a finite full algebra in the class. In our work we replace the commutativity property by some slightly weaker conditions. Particularly, we prove the FEP for the variety of residuated lattices that satisfy the equation xyx=x2y and the knotted rule. Furthermore, we investigate some generalizations of this noncommutative property by working with equations that allow us to move variables. We also note that the FEP implies the finite model property. Hence the logics modeled by these residuated lattices are decidable.
Implementation of Interval Arithmetic in CORA 2016
Authors: Althoff Matthias , Grebenyuk Dmitry
Published: January 2018

Interval arithmetic can be seen as one of the workhorses for formal verification approaches. The popularity of interval arithmetic stems form the fact that the possible outcomes of almost all frequently occurring mathematical expressions can be bounded. A disadvantage of interval arithmetic is that due to the negligence of dependencies of variables in expressions, results can be overly conservative. For this reason, interval arithmetic is typically used in formal verification tools when formulas are not contributing much to the accuracy of the overall approach, but do not belong to a restrictive class of expressions and are thus hard to evaluate. Although a lot of textbooks and software manuals for interval arithmetic exist, we have not found a complete and detailed description of how all standard mathematical functions are evaluated. This work changes this situation and describes concisely the evaluation of all standard mathematical functions. The described techniques are implemented as a class in CORA, a free MATLAB tool for continuous reachability analysis. Previously, CORA used the MATLAB toolbox INTLAB, but this tool is no longer freely available. Thus, our interval arithmetic class is currently the only freely available implementation of interval arithmetic that runs under current MATLAB versions. We have thoroughly tested our implementation against INTLAB and present the results.
Piecewise-Affine Approximations for a Powertrain Control Verification Benchmark
Authors: Deshmukh Jyotirmoy , Ito Hisahiro , Jin Xiaoqing , Kapinski James , Butts Ken , Gerhard Juergen , Samadi Behzad , Walker Kevin , Xie Yuzhen
Published: January 2018

We present approximate PWA models of a powertrain control benchmark.
Automated Theorem Proving by Translation to Description Logic
Authors: Arhami Negin , Sutcliffe Geoff
Published: January 2018

Many Automated Theorem Proving (ATP) systems for different logics,

and translators for translating different logics from one to another,

have been developed and are now available.

Some logics are more expressive than others, and it is easier to express problems in those logics.

However, their ATP systems are relatively newer,

and need more development and testing in order to solve more problems in a reasonable time.

To benefit from the available tools to solve more problems in more expressive logics,

different ATP systems and translators can be combined.

Problems in logics more expressive than CNF can be translated directly to CNF, or indirectly by translation via intermediate logics.

Description Logic (DL) sits between CNF and propositional logic.

Saffron a CNF to DL translator, has been developed, which fills the gap between CNF and DL.

ATP by translation to DL is now an alternative way of solving problems expressed in logics more expressive than DL,

by combining necessary translators from those logics to CNF, Saffron, and a DL ATP system.
Turchin's Relation and Subsequence Relation in Loop Approximation
Authors: Nepeivoda Antonina
Published: January 2018

The paper studies the subsequence relation through a notion of an intransitive binary relation on words in traces generated by prefix-rewriting systems. The relation was introduced in 1988 by V.F. Turchin for loop approximation in supercompilation. We study properties of this relation and introduce some refinements of the subsequence relation that inherit the useful features of Turchin's relation.
Logic, Probability, and Privacy: A Framework for Specifying Privacy Requirements
Authors: Hsu Tsan-Sheng , Liau Churn-Jung , Wang Da-Wei
Published: January 2018

In this paper, we propose a probabilistic hybrid logic for the specification of data privacy requirements. The proposed logic is a combination of quantitative uncertainty logic and basic hybrid logic with a satisfaction operator. We show that it is expressive enough for the specification of many well-known data privacy requirements, such as k-anonymity, l-diversity and its precursor logical safety, t-closeness, and δ-disclosure privacy. The main contribution of the work is twofold. On one hand, the logic provides a common ground to express and compare existing privacy criteria. On the other hand, the uniform framework can meet the specification needs of combining new criteria as well as existing ones.
Instantiations, Zippers and EPR Interpolation
Authors: Bjorner Nikolaj , Gurfinkel Arie , Korovin Konstantin , Lahav Ori
Published: January 2018

This paper describes interpolation procedures for EPR.

In principle, interpolation for EPR is simple:

It is a special case of first-order interpolation.

In practice, we would like procedures that take advantage

of properties of EPR: EPR admits finite models and those models

are sometimes possible to describe very compactly.

Inspired by procedures for propositional logic that use

models and cores, but not proofs, we develop a procedure for EPR

that uses just models and cores.
Benchmarks for Temporal Logic Requirements for Automotive Systems
Authors: Hoxha Bardh , Abbas Houssam , Fainekos Georgios
Published: January 2018

We propose to standardize two Matlab/Simulink models of automotive systems as benchmark problems for hybrid system verification. Both

models can be simulated quickly, making them ideal for testing-based verification methods that require a significant number of system output trajectories. One of the benchmarks is the Automatic Transmission model, which is deterministic. The other benchmark is the Fault-Tolerant Fuel Control System, which exhibits stochastic behavior. Our benchmark standardization defines a number of Metric Temporal Logic requirements that must be satisfied by the models.
Default Reasoning in Action Domains with Conditional, Non-Local Effect Actions
Authors: Strass Hannes , Thielscher Michael
Published: January 2018

In a recent paper, Baumann et al. provided a comprehensive framework for default reasoning in action theories. Yet, the approach was only defined for a very basic class of domains where all actions have only unconditional, local effects. In this paper, we show that the framework can be substantially extended to domains with action effects that are conditional (i.e. are context-sensitive to the state in which they are applied) and non-local (i.e. the range of effects is not pre-determined by the action arguments). Notably, these features can be carefully added without sacrificing important nice properties of the basic framework, such as modularity of domain specifications or the existence of default extensions. In the last part of the paper, we demonstrate how (a subclass of) the framework can be straightforwardly implemented using the answer set programming paradigm.
A Machine Learning Technique for Hardness Estimation of QFBV SMT Problems
Authors: Abdul Aziz Mohammad , Wassal Amr , Darwish Nevine
Published: January 2018

In this paper we present an approach for measuring the hardness of SMT problems.

We present the required features, the statistical hardness model used and the machine

learning technique which we used. We apply our method to estimate the hardness of

problems in Quantier Free Bit Vector (QFBV) theory and we used four of the contesting

solvers in SMT2011 to demonstrate our technique. We have qualitatively expanded some

propositional SAT features existing in the literature to directly work on general SMT

problem instances without preprocessing. The results show that our work is a promising

proof of concept.
A Resolution Calculus for Second-order Logic with Eager Unification
Authors: Leitsch Alexander , Libal Tomer
Published: January 2018

The efficiency of the first-order resolution calculus is impaired when lifting it to higher-order logic. The main reason for that is the semi-decidability and infinitary nature

of higher-order unification algorithms, which requires the integration of unification within the calculus and results in a non-efficient search for refutations.

We present a modification of the constrained resolution calculus (Huet'72) which uses an eager unification algorithm while retaining completeness. The

algorithm is complete with regard to bounded unification only, which for many cases, does not pose a problem in practice.
Towards Verified Construction for Planar Class of a Qualitative Spatial Representation
Authors: Moriguchi Sosuke , Goto Mizuki , Takahashi Kazuko
Published: January 2018

PLCA is a framework for qualitative spatial reasoning, using symbolic objects and relationships between them. To show construction of a PLCA expression, the second and the third authors introduced inductive constructions. They also proved that expressions obtained by inductive constructions are planar (planarity) and planar PLCA expressions can be obtained by inductive constructions (realizability). The former one is proven with Coq proof assistant, but the latter is proven with pen-and-paper.

We are currently proving the latter with Coq. We locate some oversights in the original inductive constructions and the proof. In this paper, we report these oversights, re-formalization of inductive constructions and modified proofs. We prove planarity and a base case of realizability with Coq, and induction step of realizability with Coq and pen-and-paper proof.
Parteras tradicionales y parto medicalizado, ¿un conflicto del pasado? Evolución del discurso de los organismos internacionales en los últimos veinte años
Authors: Argüello Avendaño Hilda E. , Mateo González Ana
Published: January 2018

Este artículo se centra en el actual conflicto sobre el papel que deben desempeñar las parteras tradicionales en la asistencia a la reproducción y los paralelismos con el momento en que la partería dejó de ser un oficio de mujeres. Los discursos de organismos internacionales nos recuerdan lo sucedido siglos antes, cuando la práctica médica se consolidaba como profesión y ciencia universal y oficial. Éstos cuestionan las capacidades de las parteras,  para atender complicaciones y para atender partos normales, lo que coloca a las parteras como figuras externas al sistema sanitario oficial.
Del horror a la seducción. Consumo de reguetón en la conformación de identidades musicales juveniles
Authors: Lavielle-Pullés Ligia
Published: January 2018

En este estudio se muestra la heterogeneidad que caracteriza el consumo de reguetón, y en específico sus repercusiones en la conformación diferenciada de identidades musicales juveniles. Mediante la exploración en los significados atribuidos por los jóvenes a un género tan polemizado a la par de consumido: el reguetón, se elaboró una clasificación que expuso las distinciones asociadas a su consumo. Para ello, la ciudad de Santiago de Cuba sirvió como punto de partida, aunque los resultados de la investigación ciertamente extralimitan este espacio urbano.