bluuebunny/crossref_metadata_2025 huggingface dataset:
MAHASISWA EKONOMI SYARIAH DI MATA PENGGUNA LULUSAN
Authors: Rosyid Ahmad
Published: January 2018

Penelitian ini bertujuan untuk melihat penilaian mitra PPL atas 1) kinerja mahasiswa PPL prodi ekonomi syariah 2) kepuasan mitra PPL dan 3) tindak lanjut panitia PPL atas keluhan mitra PPL pada pelaksanaanPPL tahun 2015. Data dikumpulkan menggunakan instrumen kuesioner dan hasilnya menunjukkan bahwa secara umum kinerja mahasiswa PPL prodi ekonomi syariah dinilai dalam rentang kategori cukup, baik dan sangat baik dengan prosentase terbesar pada kategori baik. Namun untuk kinerja penguasaan atas bahasa asing muncul penilaian kurang walaupun jumlahnya tidak banyak. Sedangkan untuk penilaian atas panitia PPL dalam menanggapi komplain mitra PPL maka umumnya dijawab baik. This study aims to look at the assessment PPL partner on 1 ) the performance of students Prodi EKOS 2) PPL partner satisfaction and 3 ) follow-up committee on the complaintPPL partner. Data were collected using a questionnaire and the results show that the performance PPL student Prodi EKOS are rated in the range enough categories , good and very good with the largest percentage in good categories . But for the performance mastery of foreign languages appeared less votes despite not many. As for the assessment of the committee in response to a complaint, PPL partner generally considered aswell .
Actividad microbiológica y biomasa microbiana en suelos cafetaleros de los Andes venezolanos
Authors: Paolini Gomez Jorge Emilio
Published: January 2018

In Venezuela approximately 200 000 ha are planted with coffee (Coffea arabica L.) mostly on the steep slopes of the Andes. Traditionally, coffee is cultivated with few or no agrochemical inputs in an agroforestry system, cropped under the shade of tree species of the leguminous family and other bushes. In recent years, with adoption of high yielding, early varieties of short stature, coffee is being produced in full sunlight with addition of mineral fertilizers and pesticides. The soil microbiological properties especially those related with the fluxes of energy and nutrient cycling, respond promptly to changes in soil conditions, often much earlier than organic carbon and, in this way, are early indicators of alterations in soil quality. In this study, we compared the microbiological activity (basal respiration), microbial biomass and derived ecophysiological ratios of topsoils (0-5 cm) collected from eight farms in the municipalities of Merida and Trujillo that practice traditional (agroforestry or shaded coffee), conventional (sun coffee or intensive monoculture) and organic (agroforestry or shaded coffee) production. The organic agriculture farms showed the highest contents of total organic carbon, water soluble carbon, basal respiration and microbial biomass compared with traditional and conventional farms. This means a more sustainable coffee system with better conservation of natural resources and environment-friendly production. On conventional farms, added fertilizers and pesticides negatively affect microorganism performance and are more inefficient in terms of carbon and energy use.
Four-valued modal logic: Kripke semantics and duality
Authors: Jung Achim , Rivieccio Umberto
Published: January 2018

Along the lines of recent investigations combining many-valued and modal systems, we address the problem of defining and axiomatizing the least modal logic over the four-element Belnap lattice. By this we mean the logic determined by the class of all Kripke frames where the accessibility relation as well as semantic valuations are four-valued. Our main result is the introduction of two Hilbert-style calculi that provide complete axiomatizations for, respectively, the local and the global consequence relations associated to the class of all four-valued Kripke models. Our completeness proofs make an extensive and profitable use of algebraic and topological techniques; in fact, our algebraic and topological analyses of the logic have, in our opinion, an independent interest and contribute to the appeal of our approach.
Analyzing Runtime Complexity via Innermost Runtime Complexity
Authors: Frohn Florian , Giesl Jürgen
Published: January 2018

There exist powerful techniques to infer upper bounds on the innermost runtime complexity of term rewrite systems (TRSs), i.e., on the lengths of rewrite sequences that follow an innermost evaluation strategy. However, the techniques to analyze the (full) runtime complexity of TRSs are substantially weaker. In this paper, we present a sufficient criterion to ensure that the runtime complexity of a TRS coincides with its innermost runtime complexity. This criterion can easily be checked automatically and it allows us to use all techniques and tools for innermost runtime complexity in order to analyze (full) runtime complexity. By extensive experiments with an implementation of our results in the tool AProVE, we show that this improves the state of the art of automated complexity analysis significantly.
Computing Nash Equilibria of Unbounded Games
Authors: Escardo Martin , Oliva Paulo
Published: January 2018

Using techniques from higher-type computability theory and proof theory we extend the well-known game-theoretic technique of backward induction to finite games of unbounded length. The main application is a closed formula for calculating strategy profiles in Nash equilibrium and subgame perfect equilibrium even in the case of games where the length of play is not a-priori fixed.
Towards Strong Higher-Order Automation for Fast Interactive Verification
Authors: Blanchette Jasmin Christian , Fontaine Pascal , Schulz Stephan , Waldmann Uwe
Published: January 2018

We believe that first-order automatic provers are the best tools available to perform most of the tedious logical work inside proof assistants. From this point of view, it seems desirable to enrich superposition and SMT (satisfiability modulo theories) with higher-order reasoning in a careful manner, to preserve their good properties. Representative benchmarks from the interactive community can guide the design of proof rules and strategies. With higher-order superposition and higher-order SMT in place, highly automatic provers could be built on modern superposition provers and SMT solvers, following a stratified architecture reminiscent of that of modern SMT solvers. We hope that these provers will bring a new level of automation to the users of proof assistants. These challenges and work plan are at the core of the Matryoshka project, funded for five years by the European Research Council. We encourage researchers motivated by the same goals to get in touch with us, subscribe to our mailing list, and join forces.
A Uniform Approach to Incremental Automated Reasoning on Strongly Distributed Structures
Authors: Ravve Elena , Volkovich Zeev , Weber Gerhard
Published: January 2018

We introduce the notion of strongly distributed structures and present a uniform approach to incremental automated reasoning on them. The approach is based on a systematic use of two logical reduction techniques: Feferman-Vaught reductions and syntactically defined translation schemes. The distributed systems are presented as logical structures A’s. We propose a uniform template for methods, which allow for a certain cost evaluation of formulae of logic L over A from values of formulae over its components and values of formulae over the index structure I. Given logic L, structure A as a composition of structures Ai,i ∈ I, index structure I and formula φ of the logic to be evaluated on A, the question is: what is the reduction sequence for φ if any. We show that if we may prove preservation theorems for L as well as if A is a strongly distributed composition of its components then the corresponding reduction sequence for A may be effectively computed. We show that the approach works for many extensions of FOL but not for all. The considered extensions of FOL are suitable candidates for modeling languages for components and services, used in incremental automated reasoning, data mining, decision making, planning and scheduling. A short complexity analysis of the method is also provided.
Parallel Graph Rewriting with Overlapping Rules
Authors: Echahed Rachid , Maignan Aude
Published: January 2018

We tackle the problem of simultaneous transformations of networks represented as graphs. Roughly speaking, one may distinguish two kinds of simultaneous or parallel rewrite relations over complex structures such as graphs: (i) those which transform disjoint subgraphs in parallel and hence can be simulated by successive mere sequential and local transformations and (ii) those which transform overlapping subgraphs simultaneously. In the latter situations, parallel transformations cannot be simulated in general by means of successive local rewrite steps. We investigate this last problem in the framework of overlapping graph transformation systems. As parallel transformation of a graph does not produce a graph in general, we propose first some sufficient conditions that ensure the closure of graphs by parallel rewrite relations. Then we mainly introduce and discuss two parallel rewrite relations over graphs. One relation is functional and thus deterministic, the other one is not functional for which we propose sufficient conditions which ensure its confluence.
Better Proof Output for Vampire
Authors: Reger Giles
Published: January 2018

Vampire produces highly usable and informative proofs, but now they are even better and this paper explains how. It is important that the proofs produced by automated theorem provers are both understandable and machine checkable. Producing something that satisfies both of these goals is challenging, especially when dealing with complex steps performed by the solver. The main areas where proof output has been improved for understanding include (i) introduction of new symbols (such as Skolem functions) in preprocessing, (ii) representation of unifiers (for example, in resolution steps), and (iii) presentation of AVATAR proofs. These improvements will be illustrated via a number of examples. For checkable proofs Vampire provides a mode that outputs the proof as a number of individual (TPTP) problems that can be independently checked. This process is explained and illustrated with examples.
A Parallel Construction of the Symbolic Observation Graph: the Basis for Efficient Model Checking of Concurrent Systems
Authors: Ouni Hiba , Klai Kais , Abid Chiheb Ameur , Zouari Belhassen
Published: January 2018

Model checking is a powerful and widespread technique for the verification of finite dis- tributed systems. It takes as input a formal model of a system and a formal specification (formula) of a property to be checked, and states whether the system satisfies the property or not. Since it is based on state space traversal algorithms, the model checking approach suffers from the well known state space explosion problem. Indeed the space (and conse- quently the time) requirements increase exponentially with the size of the models. One way to deal with this problem is symbolic model checking. It aims at checking the prop- erty on a compact representation of the system by using Binary Decision Diagram (BDD) techniques. Another way is to parallelize the construction/traversal of the state space on multiple processors. In this paper, we combine the two mentioned approaches by propos- ing an efficient multi-threaded algorithm for the construction of the so called Symbolic Observation Graph (SOG). It is a hybrid structure where the transitions of the system are divided into observed and unobserved ones. The nodes of this graph are then defined as sets of states linked with unobserved transitions (and encoded symbolically with a BDD) and edges are labeled with observed transitions only (and represented explicitly). The basic idea is that each thread owns one part of the SOG construction. We measured the runtime of the parallel SOG construction algorithm on several models, and the obtained results are very competitive. The preliminary evaluations we have done on standard examples show that our method outperforms the sequential method which makes it attractive.
Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract)
Authors: Chihani Zakaria , Miller Dale , Renaud Fabien
Published: January 2018

We present the design philosophy of a proof checker based on a notion of foundational proof certificates. At the heart of this design is a semantics of proof evidence that arises from recent advances in the theory of proofs for classical and intuitionistic logic. That semantics is then performed by a (higher-order) logic program: successful performance means that a formal proof of a theorem has been found. We describe how the lambda Prolog programming language provides several features that help guarantee such a soundness claim. Some of these features (such as strong typing, abstract datatypes, and higher-order programming) were features of the ML programming language when it was first proposed as a proof checker for LCF. Other features of lambda Prolog (such as support for bindings, substitution, and backtracking search) turn out to be equally important for describing and checking the proof evidence encoded in proof certificates. Since trusting our proof checker requires trusting a programming language implementation, we discuss various avenues for enhancing one's trust of such a checker.
ARCH-COMP17 Repeatability Evaluation Report
Authors: Johnson Taylor T.
Published: January 2018

This report presents the results of the repeatability evaluation for a friendly competition for formal verification of continuous and hybrid systems. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, thirteen tools have been applied to solve benchmark problems for the six competition categories, of which, ten tools were evaluated and passed the repeatability evaluation. The repeatability results represent a snapshot of the current landscape of tools and the types of benchmarks for which they are particularly suited and for which others may repeat their analyses. Due to the diversity of problems in verification of continuous and hybrid systems, as well as basing on standard practice in repeatability evaluations, we evaluate the tools with pass and/or failing being repeatable. These re- sults probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems up to this date.
A uniform framework for substructural logics with modalities
Authors: Lellmann Bjoern , Olarte Carlos , Pimentel Elaine
Published: January 2018

It is well known that context dependent logical rules can be problematic both to implement and reason about. This is one of the factors driving the quest for better behaved, i.e., local, logical systems. In this work we investigate such a local system for linear logic (LL) based on linear nested sequents (LNS). Relying on that system, we propose a general framework for modularly describing systems combining, coherently, substructural behaviors inherited from LL with simply dependent multimodalities. This class of systems includes linear, elementary, affine, bounded and subexponential linear logics and extensions of multiplicative additive linear logic (MALL) with normal modalities, as well as general combinations of them. The resulting LNS systems can be adequately encoded into (plain) linear logic, supporting the idea that LL is, in fact, a “universal framework” for the specification of logical systems. From the theoretical point of view, we give a uniform presentation of LL featuring different axioms for its modal operators. From the practical point of view, our results lead to a generic way of constructing theorem provers for different logics, all of them based on the same grounds. This opens the possibility of using the same logical framework for reasoning about all such logical systems.
Automated Verification of Equivalence on Quantum Cryptographic Protocols
Authors: Kubota Takahiro , Kakutani Yoshihiko , Kato Go , Kawano Yasuhito , Sakurada Hideki
Published: January 2018

t is recognized that security verification of cryptographic protocols tends to be difficult and in fact, some flaws on protocol designs or security proofs were found after they had been presented. The use of formal methods is a way to deal with such complexity. Especially, process calculi are suitable to describe parallel systems. Bisimilarity, which denotes that two processes behave indistinguishably from the outside, is a key notion in process calculi. However, by-hand verification of bisimilarity is often tedious when the processes have many long branches in their transitions. We developed a software tool to automatically verify bisimulation relation in a quantum process calculus qCCS and applied it to Shor and Preskill's security proof of BB84. The tool succeeds to verify the equivalence of BB84 and an EDP-based protocol, which are discussed in their proof.
Initial Experiments on Deriving a Complete HOL Simplification Set
Authors: Kaliszyk Cezary , Sternagel Thomas
Published: January 2018

Rewriting is a common functionality in proof assistants, that allows to simplify theorems and goals. The set of equations to use in a rewrite step has to be manually specified, and therefore often includes rules which may lead to non-termination. Even in the case of termination another desirable property of a simplification set would be confluence. A well-known technique from rewriting to transform a terminating system into a terminating and confluent one is completion. But the sets of equations we find in the context of proof assistants are typically huge and most state-of-the-art completion tools only work on relatively small problems. In this paper we describe our initial experiments with the aim to close the gap and use rewriting to compute a complete first-order simplification set for a HOL-based proof assistant fully automatically.
Computational Coverage of TLG: Nonlinearity
Authors: Morrill Glyn , Valentín Oriol
Published: January 2018

We study nonlinear connectives (exponentials) in the context of Type Logical Grammar

(TLG). We devise four conservative extensions of the

Displacement calculus with brackets, \DbC, \DbCM, \DbCb and \DbCbMr which contain the universal and existential exponential modalities of linear logic (\LL). These modalities

do not exhibit the same structural properties as in \LL, which in TLG are especially adapted for linguistic purposes. The universal modality \univexp

for TLG allows only the commutative and contraction rules, but not weakening, whereas the existential modality \exstexp allows the so-called (intuitionistic) mingle rule, which

derives a restricted version of weakening called \emph{expansion}. We provide a Curry-Howard labelling for both exponential connectives. As it turns out,

controlled contraction by \univexp gives a way to account for the so-called parasitic gaps, and controlled Mingle \exstexp iterability, in particular iterated

coordination. Finally, the four calculi are proved to be Cut-Free but decidability is only proved for $\DbCb$, whereas

for the rest the question of decidability remains open.
Turing Tests with Turing Machines
Authors: Hernandez-Orallo Jose , Insa Javier , Dowe David , Hibbard Bill
Published: January 2018

Comparative tests work by finding the difference (or the absence of difference) between a reference subject and an evaluee. The Turing Test, in its standard interpretation, takes (a subset of) the human species as a reference.

Motivated by recent findings and developments in the area of machine intelligence evaluation, we discuss what it would be like to have a Turing Test where the reference and the interrogator subjects are replaced by Turing Machines.

This question sets the focus on several issues that are usually disregarded when dealing with the Turing Test, such as the degree of intelligence of reference and interrogator, the role of imitation (and not only prediction) in intelligence, its view from the perspective of game theory and others.

Around these issues, this paper finally brings the Turing Test to the realm of Turing machines.
Formula partitioning revisited
Authors: Mann Zoltan , Papp Pal
Published: January 2018

Dividing a Boolean formula into smaller independent sub-formulae can be a useful technique for accelerating the solution of Boolean problems, including SAT and #SAT. Nevertheless, and despite promising early results, formula partitioning is hardly used in state-of-the-art solvers. In this paper, we show that this is rooted in a lack of consistency of the usefulness of formula partitioning techniques. In particular, we evaluate two existing and a novel partitioning model, coupled with two existing and two novel partitioning algorithms, on a wide range of benchmark instances. Our results show that there is no one-size-fits-all solution: for different formula types, different partitioning models and algorithms are the most suitable. While these results might seem negative, they help to improve our understanding about formula partitioning; moreover, the findings also give some guidance as to which method to use for what kinds of formulae.
Incremental Construction of Counterexamples in Model Checking Web Documents
Authors: Weitl Franz , Nakajima Shin
Published: January 2018

A new algorithm for incrementally generating counterexamples for the temporal description logic ALCCTL is presented. ALCCTL is a decidable combination of the description logic ALC and computation tree logic CTL that is expressive for content- and structure-related properties of web documents being verified by model checking. In the case of a specification violation, existing model checkers provide a single counterexample which may be large and complex. We extend existing algorithms for generating counterexamples in two ways. First, a coarse counterexample is generated initially that can be refined subsequently to the desired level of detail in an incremental manner. Second, the user can choose where and in which way a counterexample is refined. This enables the interactive step-by-step analysis of error scenarios according to the user's interest.

We demonstrate in a case study on a web-based training document that the proposed approach reveals more errors and explains the cause of errors more precisely than the counterexamples of existing model checkers. In addition, we demonstrate that the proposed algorithm is sufficiently fast to enable smooth interaction even in the case of large documents.
Motor-Transmission Drive System: a Benchmark Example for Safety Verification
Authors: Chen Hongxu , Mitra Sayan , Tian Guangyu
Published: January 2018

This paper introduces the Motor-Transmission Drive System as a benchmark example for the safety analysis of hybrid systems.

In particular, we illustrate the problem of checking the gear meshing duration and the impact impulse (both of which we refer to as safety) of the Motor-Transmission Drive System.

We aim to provide a complete problem description to which different verification tools or approaches for safety analysis can be applied and compared.

For this reason, we first elaborate on a hybrid automaton (HA) model of the Motor-Transmission Drive System to describe the gear meshing process with uncertain initial states, and then we specify the safety property of interest.

Next, we clarify the characteristic phenomena exhibited by the benchmark which make the verification problem hard to solve.

Finally, we show some simulation results to illustrate the influences of the initial states on the safety property.

This benchmark example can help the researchers and engineers to find appropriate methods for safety verification of this kind of hybrid system.
Typical-case complexity and the SAT competitions
Authors: Mann Zoltan
Published: January 2018

The aim of this paper is to gather insight into typical-case complexity of the Boolean Satisfiability (SAT) problem by mining the data from the SAT competitions. Specifically, the statistical properties of the SAT benchmarks and their impact on complexity are investigated, as well as connections between different metrics of complexity. While some of the investigated properties and relationships are "folklore" in the SAT community, this study aims at scientifically showing what is true from the folklore and what is not.
Direct Verification of Linear Systems with over 10000 Dimensions
Authors: Bak Stanley , Duggirala Parasara Sridhar
Published: January 2018

We evaluate a recently-proposed reachability method on a set of high-dimensional lin- ear system benchmarks taken from model order reduction and presented in ARCH 2016. The approach uses a state-set representation called a generalized star set and the principle of superposition of linear systems to achieve scalability. The method was previously shown to have promise in terms of scalability for direct analysis of large linear systems. For each benchmark, we also compare computing the basis matrix, a core part of the reachabil- ity method, using numerical simulations versus a matrix exponential formulation. The approach successfully analyzes systems with hundreds of dimensions in minutes, and can scale to systems that have over 10000 dimensions with a computation time ranging from tens of minutes to tens of hours, depending on the desired time step.
New Techniques in Clausal Form Generation
Authors: Reger Giles , Suda Martin , Voronkov Andrei
Published: January 2018

In automated reasoning it is common that first-order formulas need to be translated into clausal normal form for proof search. The structure of this normal form can have a large impact on the performance of first-order theorem provers, influencing whether a proof can be found and how quickly. It is common folklore that transformations should ideally minimise both the size of the generated clause set and extensions to the signature. This paper introduces a new top-down approach to clausal form generation for first-order formulas that aims to achieve this goal in a new way. The main advantage of this approach over existing bottom-up techniques is that more contextual information is available at points where decisions such as subformula-naming and Skolemisation occur. Experimental results show that our implementation of the transformation in Vampire can lead to clausal forms which are smaller and better suited to proof search.
Everything's Bigger in Texas: "The Largest Math Proof Ever"
Authors: Heule Marijn
Published: January 2018

Progress in satisfiability (SAT) solving has enabled answering long-standing open questions in mathematics completely automatically resulting in clever though potentially gigantic proofs. We illustrate the success of this approach by presenting the solution of the Boolean Pythagorean triples problem. We also produced and validated a proof of the solution, which has been called the “largest math proof ever”. The enormous size of the proof is not important. In fact a shorter proof would have been preferable. However, the size shows that automated tools combined with super computing facilitate solving bigger problems. Moreover, the proof of 200 terabytes can now be validated using highly trusted systems, demonstrating that we can check the correctness of proofs no matter their size.
Simulated Annealing Application to Maximum Lifetime Coverage Problem in Wireless Sensor Networks
Authors: Tretyakova Antonina , Seredynski Franciszek
Published: January 2018

Energy optimization problem in Wireless Sensor Networks (WSN) is a backbone of efficient performance of sensor network consisting of small devices with limited and non-recovering battery. WSN lifetime maximization problem under assumption of that the coverage is main task of the network is known as Maximal lifetime coverage problem (MLCP).

This problem belongs to a class of NP-hard problems. In this paper we propose a novel simulated annealing (SA) algorithm to solve MLCP. The proposed algorithm is studied for high dense WSN instances under different parameter setup.
Cryptographic Protocol Verification via Supercompilation (A Case Study)
Authors: Ahmed Abdulbasit , Lisitsa Alexei , Nemytykh Andrei
Published: January 2018

It has been known for a while that program transformation techniques, in particular, program specialization, can be used to prove the properties of programs automatically. For example, if a program actually implements (in a given context of use) a constant function, sufficiently powerful and semantics preserving program transformation may reduce the program to a syntactically trivial ``constant'' program, pruning unreachable branches and proving thereby the property. Viability of such an approach to verification has been demonstrated in previous works where it was applied to the verification of parameterized cache coherence protocols and Petri Nets models.

In this paper we further extend the method and present a case study on its appication to the verification of a cryptographic protocol. The protocol is modeled by functional programs at different levels of abstraction and verification via program specialization is done by using Turchin's supercompilation method.
Cyclic Proofs and Coinductive Principles
Authors: Mendel-Gleason Gavin , Hamilton Geoff
Published: January 2018

It is possible to provide a proof for a coinductive type using a corecursive function coupled with a guardedness condition. The guardedness condition, however, is quite restrictive and many programs which are in fact productive and do not compromise soundness will be rejected. We present a system of cyclic proof for an extension of System $F$ extended with sums, products and (co)inductive types. Using program transformation techniques we are able to take some programs whose productivity is suspected and transform them, using a suitable theory of equivalence, into programs for which guardedness is syntactically apparent. The equivalence of the proof prior and subsequent to transformation is given by a bisimulation relation.
Anti-Unification: Algorithms and Applications
Authors: Kutsia Temur
Published: January 2018

The anti-unification problem of two terms t1 and t2 is concerned with finding a term t which generalizes both t1 and t2. That is, the input terms should be substitution instances of the generalization term. Interesting generalizations are the least general ones. The purpose of anti-unification algorithms is to compute such least general generalizations.

Research on anti-unification has been initiated more than four decades ago, with the pioneering works by Gordon~D.~Plotkin and John~C.~Reynolds. Since then, a number of algorithms and their modifications have been developed, addressing the problem in first-order or higher-order languages, for syntactic or equational theories, over ranked or unranked alphabets, with or without sorts/types, etc. Anti-unification has found applications in machine learning, inductive logic programming, case-based reasoning, analogy making, symbolic mathematical computing, software maintenance, program analysis, synthesis, transformation, and verification. Some of these algorithms and applications will be reviewed in the talk. We will also consider recent developments in unranked and higher-order generalization computation.
Automatic detection and correction of firewall misconfigurations- A formal approach
Authors: Saâdaoui Amina , Ben Youssef Nihel , Bouhoula Adel
Published: January 2018

Firewall has been at the center of intense research in the last decade owing to the increase of malicious attacks on networks. Constant updating of the firewall configuration by modifying, adding and removing rules increases the complexity of the configuration resulting in overlapping and often conflicting filtering rules. As a consequence, the set of filtering rules becomes unreliable and contains multiple misconfigurations creating ambiguity in classification of new traffic, not only affecting the performance of the firewall, but also putting the system in a vulnerable position. Manual management of this problem can be overwhelming and potentially inaccurate. Therefore, there is a need of automated methods to analyze, detect and fix misconfigurations. The objective of our work is to propose (1) a new formal approach to discover effective firewall configurations errors, (2) an optimal and automatic method with the minimum number of operations to correct these misconfigurations in both centralized firewalls and firewalls in a distributed environment and (3) a tool that implements proposed techniques and significantly helps user in discovering and resolving firewall misconfigurations.
νZ - Maximal Satisfaction with Z3
Authors: Bjorner Nikolaj , Phan Anh-Dung
Published: January 2018

Satisfiability Modulo Theories, SMT, solvers are used in

many applications. These applications benefit from the

power of tuned and scalable theorem proving technologies

for supported logics and specialized theory solvers.

SMT solvers are primarily used to determine whether formulas are satisfiable.

Furthermore, when formulas are satisfiable, many applications need models

that assign values to free variables.

Yet, in many cases arbitrary assignments are insufficient,

and what is really needed is an optimal assignment

with respect to objective functions. So far, users of Z3,

an SMT solver from Microsoft Research, build custom loops

to achieve objective values. This is no longer necessary

with νZ (new-Z, or max-Z), an extension within Z3 that lets

users formulate objective functions directly with Z3. Under the hood there is a

portfolio of approaches for solving linear optimization problems over

SMT formulas, MaxSMT, and their combinations. Objective functions are combined

as either Pareto fronts, lexicographically, or each objective is optimized independently.
What kind of machine is the mind?
Authors: Bach Joscha , Verdicchio Mario
Published: January 2018

Many computational modeling approaches of the mind seem to be characterized by an implicit strong physicalism, which frequently leads to confusion in philosophy of AI. This work aims at pointing out some fundamental aspects of this problem, both with respect to the relation between epistemological computationalism and physical realization, and the view of symbol manipulation as constrained computation.
SGGS Theorem Proving: an Exposition
Authors: Bonacina Maria Paola , Plaisted David
Published: January 2018

We present in expository style the main ideas in SGGS, which stands for Semantically-Guided Goal-Sensitive theorem proving. SGGS uses sequences of constrained clauses to represent models, instance generation to go from a candidate model to the next, and resolution as well as other inferences to repair the model. SGGS is refutationally complete for first-order logic, DPLL-style model based, semantically guided, goal sensitive, and proof confluent, which appears to be a rare combination of features. In this paper we describe the core of SGGS in a narrative style, emphasizing ideas and trying to keep technicalities to a minimum, in order to advertise it to builders and users of theorem provers.
Transforming Prefix-constrained or Controlled Rewrite Systems
Authors: Andrianarivelo Nirina , Pelletier Vivien , Réty Pierre
Published: January 2018

We present two techniques for transforming any prefix-constrained and any controlled term rewrite system into an ordinary rewrite system. We prove that both transformations preserve the rewrite com- putations, and preserve termination. In this way, prefix-constrained rewriting and controlled rewriting can be run, and termination can be checked, using the usual tools for ordinary rewriting.
A simple proof system for lock-free concurrency
Authors: Caires Luís , Ferreira Carla , Ravara António
Published: January 2018

Concurrent algorithms classically relied on locks to guarantee the absence of interference when accessing shared resources. The massive use of distributed systems and of new multi-core architectures makes this approach unfeasible, and novel techniques are needed. Lock-Free algorithms have thus gained momentum. We define a core imperative calculus, equipped with concurrency and low level lock-free synchronization primitives, based on the Load-Link/Store-Conditional model. We propose a Hoare-Separation-style system to prove correct lock-free algorithms implemented in this language. Judgements distinguish local from global state, transfering knowledge between the worlds in the rules for loading and copying variables. We present a simple yet illustrative example of a proof for a concurrent data structure.
Generalizing the concept of quantum triads
Authors: Šlesinger Radek
Published: January 2018

The concept of quantum triad has been introduced by D. Kruml, where for a given pair of quantale modules L, R over a common quantale Q, endowed with a bimorphism (a `bilinear map') to Q, a construction equipping L and R with additional module structure and another bimorphism, both compatible with the existing bimorphism and action of the quantale, was presented. As the original concept was only defined in a specific setting of categories of quantale modules, we extend it to a more universal one, which can be applied to other common algebraic structures.
Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis
Authors: Kido Kengo , Chaudhuri Swarat , Hasuo Ichiro
Published: January 2018

Towards the goal of correctness and reliability of hybrid systems, we continue our nonstandard static analysis program (with Suenaga and Sekine) where hybrid dynamics is turned into purely discrete one with explicit use of infinitesimals. While our previous results have focused on deductive verification by program logics, the current work aims at automation and enhanced scalability by extending abstract interpretation—a technique known for its ample scalability and widespread use in various verification tools—with infinitesimals. Our theoretical results include soundness and termination via uniform widening operators; and our prototype implementation successfully verifies some benchmark examples.
Reasoning About Loops Using Vampire
Authors: Kovács Laura , Robillard Simon
Published: January 2018

In 2009, the symbol elimination method for loop invariant generation

was introduced, which used saturation

theorem proving in first-order logic to generate quantified invariants

of programs with arrays. Symbol elimination is fully automatic,

requires no user guidance, and it is the first ever approach able to

generate invariants with alternations of quantifiers. In this paper

we describe a number of improvements and extensions to symbol

elimination and invariant generation using first-order theorem

proving, in particular the Vampire theorem prover. Rather than being

limited to a specific programming language, our approach to reasoning

about loops in Vampire relies on a simple guarded command language for

its input, which can be used as an interface for more complex and

realistic imperative languages. We propose new ways for extending

quantified loop properties describing valid loop properties, by

simplifying the properties over array updates and next state

relations. We also extend symbol elimination with pre- and

post-conditions of loops. We use the loop specification to generate

only invariants that are relevant, that is, invariants that are needed

for proving partial correctness of loops. Further, we turn symbol

elimination into an automatic approach proving program correctness,

providing an alternative method to Hoare-rule based loop verification

or other deductive systems. We present our newly redesigned

implementation of loop reasoning in Vampire and also report on

experimental results.
Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers
Authors: Paulson Lawrence
Published: January 2018

Sledgehammer is a highly successful subsystem of Isabelle/HOL that calls automatic theorem provers to assist with interactive proof construction. It requires no user configuration: it can be invoked with a single mouse gesture at any point in a proof. It automatically finds relevant lemmas from all those currently available. An unusual aspect of its architecture is its use of unsound translations, coupled with its delivery of results as Isabelle/HOL proof scripts: its output cannot be trusted, but it does not need to be trusted. Sledgehammer works well with Isar structured proofs and allows beginners to prove challenging theorems.
Enhanced Simplified Memory-bounded A Star (SMA*+)
Authors: Lovinger Justin , Zhang Xiaoqin
Published: January 2018

In 1992, Stuart Russell briefly introduced a series of memory efficient optimal search algorithms. Among which is the Simplified Memory-bounded A Star (SMA*) algorithm, unique for its explicit memory bound. Despite progress in memory efficient A Star variants, search algorithms with explicit memory bounds are absent from progress. SMA* remains the premier memory bounded optimal search algorithm. In this paper, we present an enhanced version of SMA* (SMA*+), providing a new open list, simplified implementation, and a culling heuristic function, which improves search performance through a priori knowledge of the search space. We present benchmark and comparison results with state-of-the-art optimal search algorithms, and examine the performance characteristics of SMA*+.
Content-Based Image Retrieval System for Real Images
Authors: Huang Yin-Fu , Chen Bo-Rong
Published: January 2018

With the rapid progress of network technologies and multimedia data, information retrieval techniques gradually become content-based, and not text-based yet. In this paper, we propose a content-based image retrieval system to query similar images in a real image database. First, we employ segmentation and main object detection to separate the main object from an image. Then, we extract MPEG-7 features from the object and select relevant features using the SAHS algorithm. Next, two approaches “one-against- all” and “one-against-one” are proposed to build the classifiers based on SVM. To further reduce indexing complexity, K-means clustering is used to generate MPEG-7 signatures. Thus, we combine the classes predicted by the classifiers and the results based on the MPEG-7 signatures, and find out the similar images to a query image. Finally, the experimental results show that our method is feasible in image searching from the real image database and more effective than the other methods.
Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers
Authors: Conchon Sylvain , Melquiond Guillaume , Roux Cody , Iguernelala Mohamed
Published: January 2018

The treatment of the axiomatic theory of floating-point numbers is

out of reach of current SMT solvers, especially when it comes to

automatic reasoning on approximation errors. In this paper, we

describe a dedicated procedure for such a theory, which provides an

interface akin to the instantiation mechanism of an SMT solver.

This procedure is based on the approach of the Gappa tool: it

performs saturation of consequences of the axioms, in order to

refine bounds on expressions. In addition to the original approach,

bounds are further refined by a constraint solver for linear

arithmetic. Combined with the natural support for equalities

provided by SMT solvers, our approach improves the treatment of

goals coming from deductive verification of numeric programs. We

have implemented it in the Alt-Ergo SMT solver.
Turing Incomputable Computation
Authors: Fiske Michael Stephen
Published: January 2018

A new computing model, called the active element machine (AEM), is presented that demonstrates Turing incomputable computation using quantum random input. The AEM deterministically executes a universal Turing machine (UTM) program η with random active element firing patterns. These firing patterns are Turing incomputable when the AEM executes a UTM having an unbounded number of computable steps. For an unbounded number of computable steps, if zero information is revealed to an adversary about the AEM’s representation of the UTM’s state and tape and the quantum random bits that help determine η’s computation and zero information is revealed about the dynamic connections between the active elements, then there does not exist a “reverse engineer” Turing machine that can map the random firing patterns back to the sequence of UTM instructions. This casts a new light on Turing’s notion of a computational procedure. In practical terms, these methods present an opportunity to build a new class of computing machines where the program’s computational steps are hidden. This non-Turing computing behavior may be useful in cybersecurity and in other areas such as machine learning where multiple, dynamic interpretations of firing patterns may be applicable.
Quantified Heap Invariants for Object-Oriented Programs
Authors: Kahsai Temesghen , Kersten Rody , Rümmer Philipp , Schäf Martin
Published: January 2018

Heap and data structures represent one of the biggest challenges when applying model checking to the analysis of software programs: in order to verify (unbounded) safety of a program, it is typically necessary to formulate quantified inductive invariants that state properties about an unbounded number of heap locations. Methods like Craig interpolation, which are commonly used to infer invariants in model checking, are often ineffective when a heap is involved. To address this challenge, we introduce a set of new proof and program transformation rules for verifying object-oriented programs with the help of space invariants, which (implicitly) give rise to quantified invariants. Leveraging advances in Horn solving, we show how space invariants can be derived fully automatically, and how the framework can be used to effectively verify safety of Java programs.
An Epistemic Event Calculus for ASP-based Reasoning About Knowledge of the Past, Present and Future
Authors: Ma Jiefei , Miller Rob , Morgenstern Leora , Patkos Theodore
Published: January 2018

We present a generalisation of the Event Calculus, specified in classical logic and implemented in ASP, that facilitates reasoning about non-binary-valued fluents in domains with non-deterministic, triggered, concurrent, and possibly conflicting actions. We show via a case study how this framework may be used as a basis for a "possible-worlds" style approach to epistemic and causal reasoning in a narrative setting. In this framework an agent may gain knowledge about both fluent values and action occurrences through sensing actions, lose knowledge via non-deterministic actions, and represent plans that include conditional actions whose conditions may be initially unknown.
Presentación
Authors: Zebadúa Carbonell Juan Pablo
Published: January 2018

.
Jóvenes universitarios: desigualdades socioculturales y diversidad de representaciones en torno a la profesión
Authors: Piñero Ramírez Silvia Leticia
Published: January 2018

Se presenta un estudio de caso de las representacionessociales que sobre su profesión tienen los jóvenes de nuevo ingreso a las carreras de Enfermería y de Médico Cirujano de la Universidad Veracruzana. Mi hipótesis es que el origen social de los estudiantes contribuye a configurar las anticipaciones y expectativas profesionales y, por lo tanto, su elección de carrera.El objetivo consiste en establecer si el conjunto de informaciones,creencias y actitudes hacia la carrera que eligieron se asocian con sus volúmenes y tipos de capital cultural.
Hábitos culturales y postproducción en jóvenes estudiantes de la UVI-Huasteca
Authors: Morales Silva Claudia
Published: January 2018

Se identifican, a partir de un trabajo etnográfico realizado en 2007 y 2008, algunos hábitos culturales de jóvenes estudiantes de la Universidad Veracruzana Intercultural. A partir de éstos, se caracterizan procesos de postproducciones de estos universitarios y de las formas en que los estudiantes de la primera y segunda generación, en su trayecto por la misma, incorporaban distintos objetos y relatos, para (post)producir sus propias significaciones. El  referente postproducción servirá de herramienta para observar parte del proceso de reconversión e incorporación de patrimonios culturales, resultado parcial de la inserción a la vida escolar universitaria con enfoque intercultural.