bluuebunny/crossref_metadata_2025_split huggingface dataset:
Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers
Authors: Heule Marijn , Manthey Norbert , Philipp Tobias 
Published: January 2018

As satisfiability (SAT) solver performance has improved, so has their complexity, which make it more likely that SAT solvers contain bugs. One important source of increased complexity is clause sharing in parallel SAT solvers. SAT solvers can emit a proof of unsatisfiability to gain confidence that the their results are correct. Such proofs must contain deletion information in order to check them efficiently. Computing deletion information is easy and cheap for parallel solvers without clause sharing, but tricky for parallel solvers with clause sharing.We present a method to generate unsatisfiability proofs from clause sharing parallel SAT solvers. We show that the overhead of our method is small and that the produced proofs can be validated in a time similar to the solving (CPU) time. However, proofs produced by parallel solvers without clause sharing can be checked in a similar to the solving (wall-clock) time. This raises the question whether our method can be improved such that the checking time of proofs from parallel solvers without clause sharing is comparable to the time to check proofs from parallel solver with clause sharing.
Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures
Authors: Aigner Martin , Biere Armin , Kirsch Christoph , Niemetz Aina , Preiner Mathias 
Published: January 2018

Effectively parallelizing SAT solving is an open andimportant issue. The current state-of-the-art isbased on parallel portfolios. This technique relieson running multiple solvers on the same instance inparallel. As soon one instance finishes the entirerun stops. Several succesful systems even use plainparallel portfolio (PPP), where the individual solversdo not exchange any information. This paper containsa thorough experimental evaluation which shows that PPPcan improve wall-clock running time because memory accessis still local, respectively the memory system can hidethe latency of memory access. In particular, there doesnot seem as much cache congestion as one might imagine.We also present some limits on the scalibility of PPP.Thus this paper gives one argument why PPP solvers are agood fit for todays multi-core architectures.
Critical Pair Analysis in Nominal Rewriting
Authors: Suzuki Takaki , Kikuchi Kentaro , Aoto Takahito , Toyama Yoshihito 
Published: January 2018

Nominal rewriting (Fernández, Gabbay &amp; Mackie, 2004;Fernández &amp; Gabbay, 2007) is a framework that extendsfirst-order term rewriting by a binding mechanismbased on the nominal approach (Gabbay &amp; Pitts, 2002;Pitts, 2003). In this paper, we investigate confluenceproperties of nominal rewriting, following the study oforthogonal systems in (Suzuki et al., 2015), but herewe treat systems in which overlaps of the rewrite rulesexist. First we present an example where choice ofbound variables (atoms) of rules affects joinability ofthe induced critical pairs. Then we give a detailedproof of the critical pair lemma, and illustrate someof its applications including confluence results fornon-terminating systems.
Implementing Polymorphism in Zenon
Authors: Bury Guillaume , Cauderlier Raphaël , Halmagrand Pierre 
Published: January 2018

Extending first-order logic with ML-style polymorphism allows to definegeneric axioms dealing with several sorts. Until recently, mostautomated theorem provers relied on preprocess encodings intomono/many-sorted logic to reason within such theories. In this paper, wediscuss the implementation of polymorphism into thefirst-order tableau-based automated theorem prover Zenon. Thisimplementation leads to slightly modify some basic parts of the code,from the representation of expressions to the proof-search algorithm.
Lebesgue Constants and Optimal Node Systems via Symbolic Computations
Authors: Vajda Robert 
Published: January 2018

Polynomial interpolation is a classical method to approximatecontinuous functions by polynomials. To measure the correctness of theapproximation, Lebesgue constants are introduced. For a given node system $X^{(n+1)}=\{x_1&lt;\ldots&lt;x_{n+1}\}\, (x_j\in [a,b])$, the Lebesgue function $\lambda_n(x)$ is the sum of the modulus of the Lagrange basis polynomials built on $X^{(n+1)}$. The Lebesgue constant $\Lambda_n$ assigned to the function $\lambda_n(x)$ is its maximum over $[a,b]$. The Lebesgue constant bounds the interpolation error, i.e., the interpolation polynomial is at most $(1+\Lambda_n)$ times worse then the best approximation.The minimum of the $\Lambda_n$'s for fixed $n$ and interval $[a,b]$ is called the optimal Lebesgue constant $\Lambda_n^*$.For specific interpolation node systems such as the equidistant system, numerical results for the Lebesgue constants $\Lambda_n$ and their asymptoticbehavior are known \cite{3,7}. However, to give explicit symbolic expression for the minimal Lebesgue constant $\Lambda_n^*$ is computationally difficult. In this work, motivated by Rack \cite{5,6}, we are interested for expressing the minimalLebesgue constants symbolically on $[-1,1]$ and we are also looking for thecharacterization of the those node systems which realize theminimal Lebesgue constants. We exploited the equioscillation property of the Lebesgue function \cite{4} andused quantifier elimination and Groebner Basis as tools \cite{1,2}. Most of the computation is done in Mathematica \cite{8}.
Relevant logic and relation algebras
Authors: Kowalski Tomasz 
Published: January 2018

In 2007, Maddux observed that certain classes of representable relationalgebras (RRAs) form sound semantics for some relevant logics. In particular,(a) RRAs of transitive relations are sound for R, and (b) RRAs of transitive,dense relations are sound for RM. He asked whether they were complete aswell. Later that year I proved a modest positive result in a similar direction,namely that weakly associative relation algebras, a class (much) larger thanRRA, is sound and complete for positive relevant logic B. In 2008, Mikulas proved anegative result: that RRAs of transitive relations are not complete for R.His proof is indirect: he shows that the quasivariety of appropriatereducts of transitive RRAs is not finitely based. Later Maddux re-establishedthe result in a more direct way. In 2010, Maddux proved a contrasting positive result: that transitive, dense RRAs are complete for RM. He found an embedding of Sugihara algebras into transitive, dense RRAs. I will show that if we give up the requirement of representability, the positive result holds for R as well. To be precise, the following theorem holds.Theorem. Every normal subdirectly irreducible De Morgan monoid in the languagewithout Ackermann constant can be embedded into a square-increasing relationalgebra. Therefore, the variety of such algebras is sound and complete for R.
Abduction for Learning Smart City Rules
Authors: Bjorner Nikolaj , Marinescu Maria-Cristina , Sagiv Mooly 
Published: January 2018

We propose using abduction for inferring implicit rules for Smart City ontologies.We show how we can use Z3 to extract candidate abducers from partial ontologies and leverage them in an iterative process of evolving an ontology by refining relations and restrictions, and populating relations.Our starting point is a Smart City initiative of the city of Barcelona, where a substantial ontology is being developed to support processes such as city planning, social services, or improving the quality of the data concerning (for instance) legal entities, whose incompleteness may sometimes hide fraudulent behavior. In our scenario we are supporting semantic queries over heterogeneous and noisy data. The approach we develop would allow evolving ontologies in an iterative fashion as new relations and restrictions are discovered.
An Algebra of Combined Constraint Solving
Authors: Ternovska Eugenia 
Published: January 2018

The paper describes a project aiming at developing formal foundationsof combined	multi-language constraint solving in the form of an algebra of modular systems.The basis for integration of different formalisms is the classic model theory.Each atomic module is a class of structures.It can be given, e.g., by a set of constraints in a constraint formalismthat has an associated solver.Atomic modules are combined using a small number of algebraic operations.The algebra simultaneously resembles Codd's relational algebra, (but is definedon classes of structures instead of relational tables), and processalgebras originated in the work of Milner and Hoare.The goal of this paper is to establish and justifythe main notions and research directions,make definitions precise.We explain several results, but do not give proofs.The proofs will appear in several forthcoming papers.We keep this paper as a project description paper to discuss the overall project,to establish and bridge individual directions.
Abstract Domains for Bit-Level Machine Integer and Floating-point Operations
Authors: Miné Antoine 
Published: January 2018

We present a few lightweight numeric abstract domains to analyze C programs thatexploit the binary representation of numbers in computers, for instance toperform ``compute-through-overflow'' on machine integers, or to directlymanipulate the exponent and mantissa of floating-point numbers.On integers, we propose an extension of intervals with a modular component,as well as a bitfield domain.On floating-point numbers, we propose a predicate domain to match, infer,and propagate selected expression patterns.These domains are simple, efficient, and extensible.We have included them into the Astree and AstreeA static analyzers tosupplement existing domains. Experimental results show that they can improvethe analysis precision at a reasonable cost.
Coq without Type Casts: A Complete Proof of Coq Modulo Theory
Authors: Jouannaud Jean-Pierre , Strub Pierre-Yves 
Published: January 2018

Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions provides with stronger type-checking capabilities and makes the proof development closer to intuition. Since strong forms of extensionality lead to undecidable type-checking, a good trade-off is to extend intensional equality with a decidable first-order theory T, as done in CoqMT, which uses matching modulo T for the weak and strong elimination rules, we call these rules T-elimination. So far, type-checking in CoqMT is known to be decidable in presence of a cumulative hierarchy of universes and weak T-elimination. Further, it has been shown by Wang with a formal proof in Coq that consistency is preserved in presence of weak and strong elimination rules, which actually implies consistency in presence of weak and strong T-elimination rules since T is already present in the conversion rule of the calculus.We justify here CoqMT’s type-checking algorithm by showing strong normalization as well as the Church-Rosser property of β-reductions augmented with CoqMT’s weak and strong T -elimination rules. This therefore concludes successfully the meta-theoretical study of CoqMT.
On Incremental Quantitative Verification for Probabilistic Systems
Authors: Kwiatkowska Marta , Parker David , Qu Hongyang , Ujma Mateusz 
Published: January 2018

Quantitative verification techniques offer an effective meansof computing performance and reliability properties for a wide range of systems.In many cases, it is necessary to perform repeated analyses of a system,for example to identify trends in results, determine optimal system parametersor when performing online analysis for adaptive systems.We argue the need for incremental quantitative verification techniqueswhich are able to re-use results from previous verification runs in order to improve efficiency.We report on recently proposed techniques for incremental quantitative verification of Markov decision processes,based on a decomposition of the model into its strongly connected components.We give an overview of the method, describe a number of useful optimisationsand show experimental results that illustrate significant gains in run-time performanceusing the incremental approach.
A Condensed Goal-Independent Fixpoint Semantics Modeling the Small-Step Behavior of Rewriting
Authors: Comini Marco , Torella Luca 
Published: January 2018

In this paper we present a novel condensed narrowing-like semantics that contains the minimal information which is needed to describe compositionally all possible rewritings of a term rewriting system. We provide its goal-dependent top-down definition and, more importantly, an equivalent goal-independent bottom-up fixpoint characterization.We prove soundness and completeness w.r.t. the small-step behavior of rewriting for the full class of term rewriting systems.
CheAPS: a Checker of Asynchronous Parameterized Systems
Authors: Konnov Igor 
Published: January 2018

We present CheAPS, the checker of asynchronous parameterized communicating systems. It is a set of tools for verification of parameterized families F = M_n of finite-state models against LTL specification S. Each model M_n from a family F is composed of a fixed number of control processes and n processes from a fixed set of prototypes. Given a description of a family CheAPS generates finite-state models M_n and checks if one of such models can be used as an invariant of the family. As soon as an invariant is detected it is model checked by Spin to verify it against a specification S. If Spin completes the verification successfully, then all the models of F satisfy S.We are going to demonstrate an application of CheAPS to several examples: Chandy-Lamport snapshot algorithm, Awerbuch distributed depth-first search algorithm, Milner's scheduler, and the model of RSVP protocol, where invariants were detected successfully on that models by our tools. The project homepage is http://lvk.cs.msu.su/\~konnov/cheaps/. It is available under BSD-like license.The full version of the abstract is uploaded.
Program Verification using Constraint Handling Rules and Array Constraint Generalizations
Authors: De Angelis Emanuele , Fioravanti Fabio , Pettorossi Alberto , Proietti Maurizio 
Published: January 2018

The transformation of constraint logic programs (CLP programs)has been shown to be an effective methodologyfor verifying properties of imperative programs.By following this methodology, we encode the negationof a partial correctness property of an imperativeprogram prog as a predicate incorrect defined by a CLP program P, and we show thatprog is correct by transforming P intothe empty program through the applicationof semantics preserving transformation rules.Some of these rules perform replacements of constraintsthat encode properties of the data structures manipulatedby the program prog.In this paper we show that Constraint Handling Rules (CHR)are a suitable formalism for representing and applyingconstraint replacements during the transformation of CLP programs.In particular, we consider programs that manipulate integerarrays and we present a CHR encoding of a constraint replacementstrategy based on the theory of arrays.We also propose a novel generalization strategy forconstraints on integer arrays that combinesthe CHR constraint replacement strategywith various generalization operator for linear constraints,such as widening and convex hull.Generalization is controlled by additional constraintsthat relate the variable identifiers in the imperativeprogram and the CLP representation of their values.The method presented in this paper has been implemented andwe have demonstrated itseffectiveness on a set ofbenchmark programs taken from the literature.
Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic
Authors: Wisniewski Max , Steen Alexander 
Published: January 2018

In this paper, we present an embedding of higher-order nominal modal logicinto classical higher-order logic, and study its automation. There exists no automated theorem prover for first-order or higher-order nominal logic at the moment, hence, this is the first automation for this kind of logic.In our work, we focus on nominal tense logic and have successfully proven some first theorems.
Extending the Description Logic ALC with More Expressive Cardinality Constraints on Concepts
Authors: Baader Franz , Ecke Andreas 
Published: January 2018

We extend the terminological formalism of the well-known description logic ALC from concept inclusions (CIs) to more general constraints formulated in the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA). In QFBAPA one can formulate Boolean combinations of inclusion constraints and numerical constraints on the cardinalities of sets.Our new formalism extends, on the one hand, so-called cardinality restrictions on concepts, which have been introduced two decades ago, and on the other hand the recently introduced statistical knowledge bases. Though considerably more expressive, our formalism has the same complexity (NExpTime) as cardinality restrictions on concepts. We will also introduce a restricted version of our formalism for which the complexity is ExpTime. This yields the until now unknown exact complexity of the consistency problem for statistical knowledge bases.
A Shallow Embedding of Resolution and Superposition Proofs into the $\lambda\Pi$-Calculus Modulo
Authors: Burel Guillaume 
Published: January 2018

The λΠ-calculus modulo is a proof language that has been proposed as a proof standardfor (re-)checking and interoperability. Resolution and superposition are proof-search methods that are used in state-of-the-art first-order automated theorem provers. We provide a shallow embedding of resolution and superposition proofs in the λΠ-calculus modulo, thus offering a way to check these proofs in a trusted setting, and to combine them with other proofs. We implement this embedding as a backend of the prover iProver Modulo.
BluSTL: Controller Synthesis from Signal Temporal Logic Specifications
Authors: Donzé Alexandre , Raman Vasumathi 
Published: January 2018

We present BluSTL, a MATLAB toolbox for generating controllers fromspecifications written in Signal Temporal Logic (STL). The toolbox takes as input a system and aset of constraints expressed in STL and constructs an open-loop or a closed-loop (in a recedinghorizon or Model Predictive fashion) controller that enforces these constraints on the systemwhile minimizing some cost function. The controller can also be made reactive or robust to someexternal input or disturbances.
Verifying a PI Controller using SoapBox and Stabhyli
Authors: Möhlmann Eike , Hagemann Willem , Rakow Astrid 
Published: January 2018

We describe practical experiences on verifying a steeringcontroller specification. The hybrid automaton implements a PI control rule andconsiders the vehicle's velocity as input from the environment. By combiningthe tools Stabhyli and SoapBox, we establish several safety and livenessproperties for the steering controller, including convergence towards anequilibrium.
Verification of Fault-Tolerant Clock Synchronization Algorithms
Authors: Bogomolov Sergiy , Herrera Christian , Steiner Wilfried 
Published: January 2018

In this paper we propose a benchmark for verification of properties of fault-tolerantclock synchronization algorithms, namely, a benchmark of a TTEthernet network, whereproperties of the clock synchronization algorithm as implemented in a TTEthernet network can be verified, and optimization techniques for verification purposes can be applied.Our benchmark, which assumes non-faulty components, aims to be a basis for verifyingconfigurations which include faulty components, information consistency mechanisms, and for verifying other clock synchronization algorithms.
Generalizations of Rice's Theorem, Applicable to Executable and Non-Executable Formalisms
Authors: Huizing Cornelis , Kuiper Ruurd , Verhoeff Tom 
Published: January 2018

We formulate and prove two Rice-like theoremsthat characterize limitations on nameability of propertieswithin a given naming scheme for partial functions.Such a naming scheme can, but need not be, an executable formalism.A programming language is an example of an executable naming scheme,where the program text names the partial function it implements.Halting is an example of a propertythat is not nameable in that naming scheme.The proofs reveal requirements on the naming schemeto make the characterization work.Universal programming languages satisfy these requirements,but also other formalisms can satisfy them.We present some non-universal programming languagesand a non-executable specification languagesatisfying these requirements.Our theorems haveTuring's well-known Halting Theorem and Rice's Theorem as special cases,by applying them to a universal programming language or Turing Machines as naming scheme.Thus, our proofs separate the nature of the naming scheme(which can, but need not, coincide with computability) from the diagonal argument.This sheds further light on how far reaching and simple the `diagonal' argument is in itself.
Proving Simpson's Four-Slot Algorithm Using Ownership Transfer
Authors: Wang Shuling , Wang Xu 
Published: January 2018

Simpson's four-slot algorithm has been an instructive example in studying various assertional proof methods/logics geared towards shared variable concurrency. Previously, techniques like rely-guarantee, data refinement and resource separation have been applied to simplify the construction of its correctness proof. Still, an elegant, concise and insightful proof is elusive.Recently with the new generation of logics coming of age which are, for the first time, equipped with ownership transfer, it becomes imperative to ask to what extent can ownership transfer facilitate a nice proof of the algorithm. Ownership transfer is especially promising here because the conflict resolution mechanism in the four-slot algorithm can be easily recast as an implementation based on ownership transfer.
A Tableau Proof System with Names for Modal Mu-calculus
Authors: Stirling Colin 
Published: January 2018

Howard Barringer was a pioneer in the study of temporal logics withfixpoints. Their addition adds considerable expressive power.One general issue is how to defineproof systems for such logics. Here we examine proof systems formodal logic with fixpoints. We present a tableau proof systemfor checking validity of formulaswhich uses names to keep track of unfoldings of fixpoint variables.
From free algebras to proof bounds
Authors: Ghilardi Silvio 
Published: January 2018

(This is joint work with Nick Bezhanishvili).In the first part of our contribution, we review and compare existing constructions of finitely generated free algebras in modal logic focusing on step-by-step methods. We discuss the notions of step algebras and step frames arising from recent investigations, as well as the role played by finite duality.In the second part of the contribution, we exploit the potential of step frames for investigating proof-theoretic aspects. This includes developing a method which detects when a specific rule-based calculus Ax axiomatizing a given logic L has the so-called bounded proof property. This property is a kind of an analytic subformula property limiting the proof search space. We prove that every finite conservative step frame for Ax is a p-morphic image of a finite Kripke frame for L iff Ax has the bounded proof property and L has the finite model property. This result, combined with a `step version' of the classical correspondence theory turns out to be quite powerful in applications.
EasyChair
Authors: Voronkov Andrei 
Published: January 2018

EasyChair is the most commonly used conference management system. Currently about twelve conferences or workshops per day register for using EasyChair. There are about 1,200 papers submitted to EasyChair every day. The number of users of EasyChair at the time of writing this abstract is over 300,000, which is greater than the population of Linz.In this talk we give an overview of EasyChair and describe its philosophy, design, implementation, evolution and future. We will also discuss issues related to formal analysis and verification of Web services.