bluuebunny/crossref_metadata_2025_split huggingface dataset:
Conflict Resolution in Structured Argumentation
Authors: Baláž Martin , Frtús Jozef , Homola Martin 
Published: January 2018

While several interesting argumentation-based semantics fordefeasible logic programs have been proposed, to our bestknowledge, none of these approaches is able to fully handle theclosure under strict rules in a sufficient manner: they are eithernot closed, or they use workarounds such as transposition of ruleswhich violates the desired directionality of logic programmingrules.We propose a novel argumentation-based semantics, in which thestatus of arguments is determined by attacks between newlyintroduced conflict resolutions instead of attacks betweenarguments. We show that the semantics is closed w.r.t. strictrules and respects the directionality of inference rules, as wellas other desired properties previously published in theliterature.
Spectra of finitely presented lattice-ordered Abelian groups and MV-algebras, part 2
Authors: Marra Vincenzo , Mcneill Daniel , Pedrini Andrea 
Published: January 2018

This is the second part of a series of two abstracts, the first being by Andrea Pedrini. For background and notation on lattice-ordered Abelian groups, vector lattices and Q-vector lattices, and their spectral spaces, please see her submission.We consider the tools of Stone duality and the absolute applied to lattice-ordered Abelian groups, vector lattices and Q-vector lattices. Given a lattice-ordered Abelian group or Q-vector lattice, G, this leads to an interesting parallel between Min(G) and the absolute of Max(G).
Reasoning about Translation Lookaside Buffers
Authors: Syeda Hira , Klein Gerwin 
Published: January 2018

The main security mechanism for enforcing memory isolation in operating systems is provided by page tables. The hardware-implemented Translation Lookaside Buffer (TLB) caches these, and therefore the TLB and its consistency with memory are security crit- ical for OS kernels, including formally verified kernels such as seL4. If performance is paramount, this consistency can be subtle to achieve; yet, all major formally verified ker- nels currently leave the TLB as an assumption.In this paper, we present a formal model of the Memory Management Unit (MMU) for the ARM architecture which includes the TLB, its maintenance operations, and its derived properties. We integrate this specification into the Cambridge ARM model. We derive sufficient conditions for TLB consistency, and we abstract away the functional details of the MMU for simpler reasoning about executions in the presence of cached address translation, including complete and partial walks.
An Automated Framework for Exploitable Fault Identification in Block Ciphers – A Data Mining Approach
Authors: Saha Sayandeep , Kumar Ujjawal , Mukhopadhyay Debdeep , Dasgupta Pallab 
Published: January 2018

Characterization of all possible faults in a cryptosystem exploitable for fault attacks is a problem which is of both theoretical and practical interest for the cryptographic community. The complete knowledge of exploitable fault space is desirable while designing optimal countermeasures for any given crypto-implementation. In this paper, we address the exploitable fault characterization problem in the context of Differential Fault Analysis (DFA) attacks on block ciphers. The formidable size of the fault spaces demands an automated albeit fast mechanism for verifying each individual fault instance and neither thetraditional, cipher-specific, manual DFA techniques nor the generic and automated Algebraic Fault Attacks (AFA) [10] fulfill these criteria. Further, the diversified structures of different block ciphers suggest that such an automation should be equally applicable to any block cipher. This work presents an automatedframework for DFA identification, fulfilling all aforementioned criteria, which, instead of performing the attack just estimates the attack complexity for each individual fault instance. A generic and extendable data-mining assisted dynamic analysis framework capable of capturing a large class of DFA distinguishersis devised, along with a graph-based complexity analysis scheme. The framework significantly outperforms another recently proposed one [6], in terms of attack class coverage and automation effort. Experimental evaluation on AES and PRESENT establishes the effectiveness of the proposed framework in detectingmost of the known DFAs, which eventually enables the characterization of the exploitable fault space.
C2PDLS: A Combination of Combinatory and Converse PDL with Substitutions
Authors: Brenas Jon Hael , Echahed Rachid , Strecker Martin 
Published: January 2018

We introduce a logic called C2PDLS, motivated by some reasoningabout graph rewriting systems. C2PDLS is an extension of bothcombinatory propositional dynamic logic, usually written CPDL,and converse propositional dynamic logic, usually written CPDLtoo. In addition to the existing features of both CPDLs, theintroduced logic offers the possibility to use the notion ofsubstitutions à la Hoare within its formulae. Such substitutionsreflect the effect of some actions on graph structures such asaddition or deletion of edges or nodes. These last features ledus to introduce restricted universal roles over subsets of theuniverse. We propose a sound and complete deductive system forC2PDLS and show that its validity problem is decidable.
Unranked Anti-Unification with Hedge and Context Variables
Authors: Baumgartner Alexander , Kutsia Temur 
Published: January 2018

In this work we study anti-unification for unranked terms and hedges, permitting context and hedge variables.Hedges are sequences of unranked terms.The anti-unification problem of two hedges s and q is concerned with finding their generalization, a hedge g such that both s and q are instances of g under some substitutions.Context variables are used to abstract vertical differences in the input hedges,and hedge variables are used to abstract horizontal differences.A rule based system in Huet's style will be presented, which computes a set ofgeneralizations of input hedges and records all the differences.The computed generalizations are least general among a certain class of generalizations.
Experiments on the feasibility of using a floating-point simplex in an SMT solver
Authors: Caminha Barbosa de Oliveira Diego , Monniaux David 
Published: January 2018

SMT solvers use simplex-based decision procedures to solve decision problems whose formulas are quantifier-free and atoms are linear constraints over the rationals. State-of-art SMT solvers use rational (exact) simplex implementations, which have shown good performance for typical software, hardware or protocol verification problems over the years.Yet, most other scientific and technical fields use (inexact) floating-point computations, which are deemed far more efficient than exact ones.It is therefore tempting to use a floating-point simplex implementation inside an SMT solver, though special precautions must be taken to avoid unsoundness.In this work, we describe experimental results, over common benchmarks (SMT-LIB) of the integration of a mature floating-point implementation of the simplex algorithm (GLPK) into an existing SMT solver (OpenSMT).We investigate whether commonly cited reasons for and against the use of floating-point truly apply to real cases from verification problems.
The use of types in designing unification algorithms: two case studies
Authors: Erbatur Serdar , Escobar Santiago , Narendran Paliath 
Published: January 2018

We discuss the use of type systems in a non-strict sensewhen designing unification algorithms. We first give anew (rule-based) algorithm for an equational theory which representsa property of El-Gamal signature schemes and show howa type system can be used to prove termination of the algorithm.Lastly, we reproduce termination result for theory of partialexponentiation given earlier.
Replaceability and the Substitutability Hierarchy for Constraint Satisfaction Problems
Authors: Freuder Eugene , Wallace Richard 
Published: January 2018

Problem simplification is a topic of continuing interest in the field of constraint satisfaction. In this paper we examine properties associated with the basic idea of substitutability and show how certain forms of substitutabilitycan be organized into a strict hierarchy. One of these properties, here called replaceability, has been identified by other authors as being of special interest. In this work we confirm these earlier claims and show that replaceability is significant because it is the most general property in the hierarchy that allows inferences from local to global versions of this property. To make use of this discovery, we introduce two algorithms for establishing neighbourhood replaceability, and we present an initial experimental examination of these algorithms including ways to improve their performance through ordering heuristics and various kinds of inference.
Challenges for Safe Autonomous Flight
Authors: Scherer Sebastian 
Published: January 2018

Autonomy holds a great promise by improving the applications, safety, and efficiency of flight. If little operator input is necessary, unmanned rotorcraft have a wide range of applications ranging from cargo delivery to inspection. Currently unmanned rotorcraft are underutilized because they either have to fly on preplanned missions at high altitude or require careful teleoperation. A capable autonomous rotorcraft will have to react quickly to previously unknown obstacles, land at unprepared sites, and fly with semantic information to enable long-term autonomy in cluttered environments.In this talk we give an overview of how autonomy systems are currently designed and how pushing the performance and safety of these systems challenges current verification paradigms. In particular we will address how a supervisory layer in the motion planning system can improve safety, a sensor steering system enables us to optimize coverage for safe trajectories, and how semantic information can help us guide the rotorcraft.
Towards High-Assurance Multiprocessor Virtualisation
Authors: von Tessin Michael 
Published: January 2018

Virtualisation is increasingly being used in security-critical systems to provide isolation between system components. Being the foundation of any virtualised system, hypervisors need to provide a high degree of assurance with regards to correctness and isolation. Microkernels, such as seL4, can be used as hypervisors. Functional correctness of seL4's uniprocessor C implementation has been formally verified. The framework employed to verify seL4 is tailored to facilitate reasoning about sequential programs. However, we want to be able to use the full power of multiprocessor/multicore systems, and at the same time, leverage the high assurance seL4 already gives us for uniprocessors.This work-in-progress paper explores possible multiprocessor designs of seL4 and their amenability to verification. For the chosen design, it contributes a formal multiprocessor execution model to lift seL4's uniprocessor model and proofs into a multiprocessor context using only minor modifications. The theorems proving the validity of the lift operation are machine-checked in Isabelle/HOL and walked-through in the paper.
Chains of Integrators as a Benchmark for Scalability of Hybrid Control Synthesis
Authors: Livingston Scott , Raman Vasumathi 
Published: January 2018

Formal methods refers broadly to techniques for the verification andautomatic synthesis of transition systems that satisfy desirable propertiesexactly or within some statistical tolerance. Though historically developed forconcurrent software, recent work has brought these methods to bear on motionplanning in robotics. Challenges specific to robotics, such as uncertainty andreal-time constraints, have motivated extensions to existing methods andentirely novel treatments. However, compared to other areas within roboticsresearch, demonstrations of formal methods have been surprisingly small-scale.The proposed benchmark seeks to motivate advancement of the state ofthe art toward practical realization by testing scalability of existing tools, andmotivating improvements.
PDT Logic for Stream Reasoning in Multi-agent Systems
Authors: Martiny Karsten , Moeller Ralf 
Published: January 2018

We present Probabilistic Doxastic Temporal (PDT) Logic for streams, a formalism to reason aboutprobabilistic beliefs and their infinite temporal evolution in multi-agent systems. Extending previouswork on PDT Logic, this formalism builds on a Markov chain model to represent infinite streamsof possible worlds. Within these streams, it enables the quantification of beliefs through probabilityintervals as well as the representation of temporal relations and epistemic actions. We show howagents can update their beliefs with respect to their observations, provide a model for infinite streams of possible worlds and show how we can map clippings of these streams to finite time windows.Based on these time windows, we introduce an adoption of the semantics of PDT Logic for finitetime frames, and show how this provides a means to overcome the limitation of finite time domains.
Well-founded Functions and Extreme Predicates in Dafny: A Tutorial
Authors: Leino Rustan 
Published: January 2018

A recursive function is well defined if its every recursive callcorresponds a decrease in some well-founded order. Such a function issaid to be _terminating_ and is in many applications the standard wayto define a function. A boolean function can also be defined asan extreme solution to a recurrence relation, that is, as a least orgreatest fixpoint of some functor. Such _extreme predicates_ areuseful to encode a set of inductive or coinductive inference rulesand are at the core of many a constructive logic. Theverification-aware programming language Dafny supports bothterminating functions and extreme predicates. This tutorialdescribes the difference in general terms, and then describes novelsyntactic support in Dafny for defining and proving lemmas withextreme predicates. Various examples and considerations are given.Although Dafny's verifier has at its core a first-order SMT solver,Dafny's logical encoding makes it possible to reason about fixpointsin an automated way.
Hierarchic Superposition Revisited
Authors: Waldmann Uwe 
Published: January 2018

In 1994,Bachmair, Ganzinger, and Waldmann introduced the hierarchicalsuperposition calculus as a generalization of the superpositioncalculus for black-box style theory reasoning.Their calculus works in a framework of hierarchic specifications.It tries to prove theunsatisfiability of a set of clauses with respect to interpretationsthat extend a background model such as the integers with linear arithmeticconservatively, that is, withoutidentifying distinct elements of old sorts ("confusion") and withoutadding new elements to old sorts ("junk").We show how the calculus can be improved,report on practical experiments,and present a new completeness result fornon-compact classes of background models(i.e., linear integer or rational arithmetic restricted tostandard models).
Building trustworthy refactoring tools
Authors: Thompson Simon 
Published: January 2018

The bar for adoption of refactoring tools is high: not only does a refactoring extract information from your source code, it also transforms it, often in a radical way.After discussing what users require from their tools, we will examine ways in which tool builders can try to increase their users' confidence in the tools. These mechanisms include visualisation, unit testing, property-based testing and verification, and are based on the Kent functional programming group's experience of building the HaRe and Wrangler refactoring systems for Haskell and Erlang.
Metis-based Paramodulation Tactic for HOL Light
Authors: Färber Michael , Kaliszyk Cezary 
Published: January 2018

Metis is an automated theorem prover based on ordered paramodulation.It is widely employed in the interactive theorem provers Isabelle/HOL and HOL4to automate proofs as well as reconstruct proofs found by automated provers.For both these purposes, the tableaux-based MESON tactic is frequently usedin HOL Light. However, paramodulation-based provers such as Metisperform better on many problems involving equality.We created a Metis-based tactic in HOL Light which translates HOL problemsto Metis, runs an OCaml version of Metis, and reconstructs proofsin Metis' paramodulation calculus as HOL proofs.We evaluate the performance of Metis as proof reconstruction methodin HOL Light.
Bounded Higher-order Unification using Regular Terms
Authors: Libal Tomer 
Published: January 2018

We present an algorithm for the bounded unification of higher-order terms.The algorithm extends G. P. Huet's pre-unification algorithm with rules for the generation and folding of regular terms.The concise form of the algorithm allows the reuse of the pre-unification correctness proof. Furthermore, the regular termscan be restricted in order to decide the unifiability problem.Finally, the algorithm avoids re-computation of terms in a non-deterministic search which leads to a better performance in practice when compared to other boundedunification algorithms.
Theory Exploration: a role for Model Theory?
Authors: Smaill Alan 
Published: January 2018

There is an empirical claim that, when exploring amathematical theory, after a succession of key results have beenobtained, a point of equilibrium is reached where any query ofinterest can be resolved by routine reasoning from the resultsalready established. Here is suggested some ways of thinking aboutthe situation, in general. There are at least some situations wherewe can establish that all results (of a certain shape) will followby routine reasoning from a small number of key properties. Anexample is described, and the significance for automated theoryexploration discussed.
Juventud indígena en el Totonacapan Veracruzano
Authors: García Martínez Ariel 
Published: January 2018

El artículo pretende dar a conocer la especificidad de la juventud indígena de Totonacapan, su incorporación a la sociedad adulta y su interacción a través de un comparativo que toma como punto de partida la integración de los poblados pertenecientes a la sierra de Papantla, en el norte del estado de Veracruz, con el resto de la sociedad nacional. El trabajo intenta reconstruir el surgimiento de los "jóvenes indígenas" totonacos como producto de la interacción con su propia cultura y la cultura nacional en las cuatro últimas décadas.
Rosario Castellanos, feminista a partir de sus propias palabras
Authors: Lamas Marta 
Published: January 2018

A partir del análisis de sus escritos periodísticos, se recupera a Rosario Castellanos como una pionera intelectual del feminismo mexicano. Se defiende la idea de que en sus artículos periodísticos se plasma con fuerza y lucidez un pensamiento feminista moderno, que gira en torno a los efectos del mandato cultural de la feminidad, aportando a la crítica de la situación de las mujeres mexicanas. Castellanos rechaza el victimismo, reivindica la necesidad de terminar con la autocomplacencia femenina y propone que las mujeres se responsabilicen de sus vidas, madurando y puliendo ideas que hoy en día tienen vigencia y radicalidad notables.
Las relaciones internacionales de los gobiernos locales: el caso de Chiapas
Authors: Rodríguez Gelfenstein Sergio 
Published: January 2018

Como fuerza imperante en la última década del siglo XX, la globalización ha sido dominada por los aspectos económicos y por la expansión de los mercados. Sin embargo, este proceso puede llegar a tener un rostro humano si se logra una nueva aproximación de los gobiernos, una que preserve las ventajas ofrecidas por los mercados globales y la competencia, pero que permita al mismo tiempo que los recursos humanos, comunitarios y ambientales aseguren que la globalización trabaja para los pueblos y no para las ganancias.
Más allá de la hibridad: los medios televisivos y la producción de identidades indígenas en Oaxaca, México
Authors: Cusi Wortham Erica 
Published: January 2018

Esta breve y parcial historia del video indígena y de Radio y Video Tamix, demuestra que el proceso de articular identidades indígenas "en casa" y dentro de los circuitos discursivos fuera de la comunidad, es algo complejo y que debemos mantener esa complejidad y pluralidad en nuestra comprensión de tales procesos sociales tan dinámicos.
¿Antropología de la ciudadanía?... étnica. En construcción desde América Latina
Authors: Leyva Solano Xochitl 
Published: January 2018

En este artículo tomo como hilo conductor el concepto de ciudadanía cruzándolo desde los campos del derecho y la filosofía hacia el de la antropología. Ello es posible gracias a que cientíicos sociales de varias latitudes han acuñado términos como "ciudadanía cultural", "ciudadanía multicultural", "ciudadanía intercultural" y "ciudadanía étnica". Este último concepto ha sido acuñado atendiendo a la historia y la naturaleza de las demandas, los reclamos y las luchas que han llevado a cabo, desde el último cuarto del siglo XX, las comunidades, líderes, organizaciones y movimientos indígenas de América Latina.
Diseño, construcción y evaluación de un secador solar para mango Ataulfo
Authors: Iglesias Díaz Roilan , José Gómez Reynaldo Alonso , Lastres Danguillecourt Orlando , López de Paz Pascual , Farrera Vázquez Nein , Ibáñez Duharte Guillermo Rogelio 
Published: January 2018

Se reporta el diseño, construcción y evaluación de un secador solar para mango Ataulfo cosechado en la región del Soconusco en el estado de Chiapas. En esta región se pierde 15% del mango ya sea por súper producción y por no tener un método de conservación poscosecha. Para el diseño se utilizaron las especificaciones del producto a secar, el registro de las condiciones climáticas del lugar y los ensayos experimentales de secado realizados en la UNICACH. La metodología propuesta se basa en la sistemática combinación de la aplicación de los conceptos básicos de diseño y reglas generales de la transferencia de calor y masa, presentándose los resultados de dichos cálculos en un cuadro. Se obtuvieron de la evaluación en vacío del secador valores promedios de humedad y temperatura del aire en la cámara de secado de 5. (%) y 45 °C respectivamente. La temperatura promedio del aire ambiente fue de 25 °C y la radiación solar promedio de 500 W m-2. El tiempo de secado fue de 8 horas sol, secándose hasta 8.4% desde una humedad inicial de 80%. Se presentan las curvas la evaluación en vacío; además de la variación del peso, humedad y la humedad libre del mango respecto al tiempo. Se demostró que es posible dar tratamiento poscosecha del mango Ataulfo y aprovechar el que se pierde en los campos. Este diseño de secador solar es muy flexible en su funcionamiento.