bluuebunny/crossref_metadata_2025 huggingface dataset:
A Summary of Recent Progress on Efficient Parametric Approximations of Viability and Discriminating Kernels
Authors: Mitchell Ian M.
Published: January 2018

Viability and discriminating kernels are powerful constructs for analyzing system safety through model checking, but until recently the only computational algorithms available were nonparametric grid-based approaches which, although accurate, scaled exponentially with the dimension of the system's state space. In contrast, several polynomial complexity reachability algorithms have been developed using various parametric set representations. In a recent series of papers, two of these parametric approaches -- based on ellipsoids and support vectors -- have been adapted to approximate viability and discriminating kernels in the discrete, continuous and sampled data models of time. This paper briefly summarizes these algorithms and compares their key features with one another and with a representative nonparametric approach.
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 means

of 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 parameters

or when performing online analysis for adaptive systems.

We argue the need for incremental quantitative verification techniques

which 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 optimisations

and show experimental results that illustrate significant gains in run-time performance

using the incremental approach.
Vector Addition Systems Reachability Problem (A Simpler Solution)
Authors: Leroux Jerome
Published: January 2018

The reachability problem for Vector Addition Systems (VASs) is a central problem of net theory. The general problem is known to be decidable by algorithms based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition (KLMTS decomposition). Recently from this decomposition, we deduced that a final configuration is not reachable from an initial one if and only if there exists a Presburger inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Preburger formula denotes an inductive invariant, we deduce from this result that there exist checkable certificates of non-reachability in the Presburger arithmetic. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas. In another recent paper we provided the first proof of the VAS reachability problem that is not based on the KLMST decomposition. The proof is based on the notion of production relations that directly proves the existence of Presburger inductive invariants. In this paper we propose new intermediate results simplifying a bit more this last proof.
From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes
Authors: Boumarafi Yazid , Sais Lakhdar , Salhi Yakoub
Published: January 2018

In this paper, we propose a new approach for defining tractable classes in propositional satisfiability problem (in short SAT). The basic idea consists in transforming SAT instances into instances of the problem of finding a maximum independent set. In this context, we only consider propositional formulæ in conjunctive normal form where each clause is either positive or binary negative. Tractable classes are obtained from existing polynomial time algorithms of the problem of finding a maximum independent set in the case of different graph classes, such as claw-free graphs and perfect graphs. We show, in particular, that the pigeonhole principle belongs to one of the defined tractable classes. Furthermore, we propose a characterization of the minimal models in the largest considered fragment based on the maximum independent set problem.
Functional Pearl: the Proof Search Monad
Authors: Protzenko Jonathan
Published: January 2018

We present the proof search monad, a set of combinators that allows one to write a proof search engine in a style that resembles the formal rules closely. The user calls functions such as premise, prove or choice; the library then takes care of generating a derivation tree. Proof search engines written in this style enjoy: first, a one-to-one correspondence between the implementation and the derivation rules, which makes manual inspection easier; second, proof witnesses “for free”, which makes a verified, independent validation approach easier too.
Covered Clause Elimination
Authors: Heule Marijn , Järvisalo Matti , Biere Armin
Published: January 2018

Generalizing the novel clause elimination procedures developed in [1], we introduce explicit (CCE), hidden (HCCE), and asymmetric (ACCE) variants of a procedure that eliminates covered clauses from CNF formulas. We show that these procedures are more effective in reducing CNF formulas than the respective variants of blocked clause elimination, and may hence be interesting as new preprocessing/simplification techniques for SAT solving.
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.
Exploring Steinitz-Rademacher Polyhedra: a Challenge for Automated Reasoning Tools
Authors: Alama Jesse
Published: January 2018

This note reports on some experiments, using a handful of standard automated reasoning tools, for exploring Steinitz-Rademacher polyhedra, which are models of a certain first-order theory of incidence structures. This theory and its models, even simple ones, presents significant, geometrically fascinating challenges for automated reasoning tools are.
Decidable linear list constraints
Authors: Bauer Sabine , Hofmann Martin
Published: January 2018

We present new results on a constraint satisfaction problem arising from the inference of resource types in automatic amortized analysis for object-oriented programs by Rodriguez and Hofmann.These constraints are essentially linear inequalities between infinite lists of nonnegative rational numbers which are added and compared pointwise. We study the question of satisfiability of a system of such constraints in two variants with significantly different complexity. We show that in its general form (which is the original formulation presented by Hofmann and Rodriguez at LPAR 2012) this satisfiability problem is hard for the famous Skolem-Mahler-Lech problem whose decidability status is still open but which is at least NP-hard. We then identify a subcase of the problem that still covers all instances arising from type inference in the aforementioned amortized analysis and show decidability of satisfiability in polynomial time by a reduction to linear programming. We further give a classification of the growth rates of satisfiable systems in this format and are now able to draw conclusions about resource bounds for programs that involve lists and also arbitrary data structures if we make the additional restriction that their resource annotations are generated by an infinite list (rather than an infinite tree as in the most general case). Decidability of the tree case which was also part of the original formulation by Hofmann and Rodriguez still remains an open problem.
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 methodology

for verifying properties of imperative programs.

By following this methodology, we encode the negation

of a partial correctness property of an imperative

program prog as a predicate incorrect defined by a CLP program P, and we show that

prog is correct by transforming P into

the empty program through the application

of semantics preserving transformation rules.

Some of these rules perform replacements of constraints

that encode properties of the data structures manipulated

by the program prog.

In this paper we show that Constraint Handling Rules (CHR)

are a suitable formalism for representing and applying

constraint replacements during the transformation of CLP programs.

In particular, we consider programs that manipulate integer

arrays and we present a CHR encoding of a constraint replacement

strategy based on the theory of arrays.

We also propose a novel generalization strategy for

constraints on integer arrays that combines

the CHR constraint replacement strategy

with various generalization operator for linear constraints,

such as widening and convex hull.

Generalization is controlled by additional constraints

that relate the variable identifiers in the imperative

program and the CLP representation of their values.

The method presented in this paper has been implemented and

we have demonstrated its

effectiveness on a set of

benchmark programs taken from the literature.
Multiclassifier System with Dynamic Model of Classifier Competence Applied to the Control of Bioprosthetic Hand
Authors: Kurzynski Marek
Published: January 2018

In this paper the problem of recognition of patient's intent to move hand prosthesis is addressed. The proposed method is based on recognition of electromiographic (EMG) and mechanomiographic (MMG) biosignals using a multiclassifier system (MCS) working with dynamic ensemble selection (DES) scheme and original concept of competence function. The competence measure is based on relating the response of the classifier with the decision profile of a test object which is evaluated using K nearest objects from the validation set (static mode). Additionally, feedback information coming from bioprosthesis sensors on the correct/incorrect classification is applied to the adjustment of the combining mechanism during MCS operation through adaptive tuning competences of base classifiers depending on their decisions (dynamic mode). Experimental investigations using real data concerning the recognition of five types of grasping movements and computer-simulated procedure of generating feedback signals are performed. The performance of MCS with the proposed competence measure is experimentally compared against 5 state-of-art MCS's in static mode and furthermore the MCS system developed is evaluated with respect to the effectiveness of the procedure of tuning competence. The results obtained indicate that the modification of competence of base classifiers during the working phase essentially improves performance of the MCS system. The system developed achieved the highest classification accuracy demonstrating the potential of MCS with feedback signals from prosthesis sensors for the control of bioprosthetic hand.
Effectively Monadic Predicates
Authors: Veanes Margus , Bjorner Nikolaj , Nachmanson Lev , Bereg Sergey
Published: January 2018

Monadic predicates play a prominent role in many decidable cases, including decision procedures for symbolic automata. We are here interested in discovering whether a formula can be rewritten into a Boolean combination of monadic predicates. Our setting is quantifier-free formulas over a decidable background theory, such as arithmetic and we here develop a semi-decision procedure for extracting a monadic decomposition of a formula when it exists.
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 logic

into 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.
Utilizing Hoare Logic to Strengthen Testing for Error Detection in Programs
Authors: Liu Shaoying
Published: January 2018

Hoare logic (also known as Floyd-Hoare logic) can be used to formally verify the correctness of programs while testing provides a practical way to detect errors in programs. Unfortunately, the former is rarely applied in practice and the later is difficult to detect all existing errors. In this paper, we propose a novel technique that makes good use of Hoare logic to strengthen testing. The essential idea is first to use specification-based testing to discover all traversed program paths and then to use Hoare logic to prove their correctness. During the proof process, all errors on the paths can be detected. A case study is conducted to show its feasibility; an example taken from the case study is used to illustrate how the proposed method is applied; and discussion on the potential challenges to the method is presented.
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 standard

for (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 from

specifications written in Signal Temporal Logic (STL). The toolbox takes as input a system and a

set of constraints expressed in STL and constructs an open-loop or a closed-loop (in a receding

horizon or Model Predictive fashion) controller that enforces these constraints on the system

while minimizing some cost function. The controller can also be made reactive or robust to some

external input or disturbances.
Loopfrog — loop summarization for static analysis
Authors: Kroening Daniel , Sharygina Natasha , Tonetta Stefano , Tsitovich Aliaksei , Wintersteiger Christoph M.
Published: January 2018

Loopfrog is a scalable static analyzer for ANSI-C programs, that combines the precision of model checking and the performance of abstract interpretation. In contrast to traditional static analyzers, it does not calculate the abstract ﬁx-point of a program by iterative application of an abstract transformer. Instead, it calculates symbolic abstract transformers for program fragments (e.g., loops) using a loop summarization algorithm. Loopfrog computes abstract transformers starting from the inner-most loops, which results in linear (in the number of the looping constructs) run-time of the sum- marization procedure and which is often considerably smaller than the traditional saturation procedure of abstract interpetation. It also provides “leaping” counterexamples to aid in the diagnosis of errors.
Adaptive Assertion-Level Proofs
Authors: Benzmüller Christoph , Schiller Marvin
Published: January 2018

(extended abstract submitted as paper 8)
On Logical Relations and Conservativity
Authors: de Groote Philippe
Published: January 2018

This paper, which attempts to develop an abstract construct that generalizes the intensionalization procedure introduced by Kanazawa and de Groote,

advocates for the use of logical relations in order to establish conservativity

results.
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 steering

controller specification. The hybrid automaton implements a PI control rule and

considers the vehicle's velocity as input from the environment. By combining

the tools Stabhyli and SoapBox, we establish several safety and liveness

properties for the steering controller, including convergence towards an

equilibrium.
Development of a Query Language for GML based on XPath
Authors: Almendros-Jimenez Jesus , Becerra-Teron Antonio , Garcia-Garcia Francisco
Published: January 2018

Geography Markup Language (GML) has been established as the standard language for the transport, storage and modelling of geographic information. In this paper we study how to adapt the XPath query language to GML documents. With this aim, we have defined a semantic based XPath language which is not based on the (tree-based) syntactic structure of GML documents, rather than, it is based on the “semantic structure” of GML documents. In order words, the proposed XPath language is based on the GML schema instead of the syntactic structure. We have developed a system called UALGIS, in order to implement the approach. Such system stores GML documents by means of the PostGIS RDBMS. In order to execute semantic-based XPath queries we have defined a translation of the queries into SQL. Such translation takes into account the GML schema. Finally, the system allows to visualize the result. With this aim, the results of a queries are exported to the Keyhole Markup Language (KML) format.
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-tolerant

clock synchronization algorithms, namely, a benchmark of a TTEthernet network, where

properties 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 verifying

configurations which include faulty components, information consistency mechanisms, and for verifying other clock synchronization algorithms.
Using the TPTP Language for Representing Derivations in Tableau and
Connection Calculi
Authors: Otten Jens , Sutcliffe Geoff
Published: January 2018

The TPTP language, developed within the framework of the TPTP library, allows the representation of problems and solutions in first-order and higher-order logic. Whereas the writing of solutions in resolution calculi is well documented and used, an appropriate representation of solutions in tableau or connection calculi using the TPTP syntax has not yet been specified. This paper describes how the TPTP language can be used to represent derivations and solutions in standard tableau, sequent and connection calculi for classical first-order logic.
Tropical linear programming and parametric mean payoff games
Authors: Gaubert Stephane , Katz Ricardo , Sergeev Sergei
Published: January 2018

Tropical polyhedra have been recently used to represent disjunctive invariants in static analysis. To handle larger instances, the tropical analogues of classical linear programming results need to be developed. This motivation leads us to study a general tropical linear programming problem. We construct an associated parametric mean payoff game problem, and show that the optimality of a given point, or the unboundedness of the problem, can be certified by exhibiting a strategy for one of the players having certain infinitesimal properties (involving the value of the game and its derivative) that we characterize combinatorially. In other words, strategies play in tropical linear programming the role of Lagrange multipliers in classical linear programming. We use this idea to design a Newton-like algorithm to solve tropical linear programming problems, by reduction to a sequence of auxiliary mean payoff game problems.
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 theorems

that characterize limitations on nameability of properties

within 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 property

that is not nameable in that naming scheme.

The proofs reveal requirements on the naming scheme

to make the characterization work.

Universal programming languages satisfy these requirements,

but also other formalisms can satisfy them.

We present some non-universal programming languages

and a non-executable specification language

satisfying these requirements.

Our theorems have

Turing'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.
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs
Authors: Habli Nada , Felty Amy P.
Published: January 2018

We describe ongoing work on building an environment to support reasoning in proof assistants that represent formal systems using higher-order abstract syntax (HOAS). We use a simple and general specification language whose syntax supports HOAS. Using this language, we can encode the syntax and inference rules of a variety of formal systems, such as programming languages and logics. We describe our tool, implemented in OCaml, which parses this syntax, and translates it to a Coq library that includes definitions and hints for aiding automated proof in the Hybrid system. Hybrid itself is implemented in Coq, and designed specifically to reason about such formal systems. Given an input specification, the library that is automatically generated by our tool imports the general Hybrid library and adds definitions and hints for aiding automated proof in Hybrid about the specific programming language or logic defined in the specification. This work is part of a larger project to compare reasoning in systems supporting HOAS. Our current work focuses on Hybrid, Abella, Twelf, and Beluga, and the specification language is designed to be general enough to allow the automatic generation of libraries for all of these systems from a single specification.
Reasoning Inside The Box: Deduction in Herbrand Logics
Authors: Cohen Liron , Zohar Yoni
Published: January 2018

Herbrand structures are a subclass of standard first-order structures commonly used in logic and automated reasoning due to their strong definitional character. This paper is devoted to the logics induced by them: Herbrand and semi-Herbrand logics, with and without equality. The rich expressiveness of these logics entails that there is no adequate effective proof system for them. We therefore introduce infinitary proof systems for Herbrand logics, and prove their completeness. Natural and sound finitary approximations of the infinitary systems are also presented.
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.
LEO-II Version 1.5
Authors: Benzmüller Christoph , Sultana Nik
Published: January 2018

LEO-II cooperates with other theorem-provers to prove theorems in classical higher-order logic. It returns hybrid proofs, containing inferences made by LEO-II as well as the backend provers with which it cooperates. This article describes recent improvements made to LEO-II.
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 with

fixpoints. Their addition adds considerable expressive power.

One general issue is how to define

proof systems for such logics. Here we examine proof systems for

modal logic with fixpoints. We present a tableau proof system

for checking validity of formulas

which 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.
Tensor products of modal logics
Authors: Shapirovskiy Ilya , Shehtman Valentin
Published: January 2018

We consider shifted products of modal algebras and logics first introduced by Y. Hasimoto in 2000. For logics this operation is similar to the well-known usual product but it is logically invariant. We prove the conjecture of D. Gabbay that shifted products act on Boolean algebras exactly as tensor products, so we call them tensor products of modal algebras. We also propose a filtration technique for models based on tensor products and obtain some decidability results.
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.
A Case for Query-driven Predicate Answer Set Programming
Authors: Gupta Gopal , Salazar Elmer , Marple Kyle , Chen Zhuo , Shakerin Farhad
Published: January 2018

Answer Set Programming (ASP) has emerged as a successful paradigm for developing intelligent applications. ASP is based on adding negation as failure to logic programming under the stable model semantics regime. ASP allows for sophisticated reasoning mechanisms that are employed by humans to be modeled elegantly. We argue that being able to model common sense reasoning as used by humans is critical for success of automated reasoning. We also argue that extending answer programming systems to general predicates is critical to realizing the full power of ASP. Goal-directed predicate ASP systems are needed to make the ASP technology practical for building large, scalable knowledge-based applications.
SC-square: when Satisfiability Checking and Symbolic Computation join forces
Authors: Abraham Erika , Abbott John , Becker Bernd , Bigatti Anna M. , Brain Martin , Cimatti Alessandro , Davenport James H. , England Matthew , Fontaine Pascal , Forrest Stephen , Ganesh Vijay , Griggio Alberto , Kroening Daniel , Seiler Werner M.
Published: January 2018

Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but with common interests, e.g., in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of the SC-square initiative is to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap from theory along the way to tools and (industrial) applications.
Robotics, Temporal Logic and Stream Reasoning
Authors: Doherty Patrick , Heintz Fredrik , Kvarnström Jonas
Published: January 2018

The area of AI robotics offers a set of fundamentally challenging problems when attempting to integrate logical reasoning functionality in such systems. The problems arise in part from the high degree of complexity in such architectures which include realtime behaviour, distribution, concurrency, various data latencies in operation and several levels of abstraction. For logic to work practically in such systems, traditional theorem proving, although important, is often not feasible for many of the functions of reasoning in such systems. In this article, we present a number of novel approaches to such reasoning functionality based on the use of temporal logic. The functionalities covered include, automated planning, stream-based reasoning and execution monitoring.
Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry
Authors: Urban Josef , Veroff Robert
Published: January 2018

We describe our experiments with several state-of-the-art automated theorem provers on the problems in Tarskian Geometry created by Beeson and Wos. In comparison to the manually-guided Otter proofs by Beeson and Wos, we can solve a large number of problems fully automatically, in particular thanks to the recent large-theory reasoning methods.
HOL Provers for First-order Modal Logics --- Experiments
Authors: Benzmüller Christoph
Published: January 2018

Higher-order automated theorem provers have been employed to automate first-order modal logics. Extending previous work, an experiment has been carried out to evaluate their collaborative and individual performances.
Fractal Sets as Final Coalgebras Obtained by Completing an Initial Algebra
Authors: Moss Larry , Ratnayake Jayampathy , Rose Robert
Published: January 2018

This paper is a contribution to the presentation of fractal sets in terms of final coalgebras.

The first result on this topic was Freyd's Theorem: the unit interval [0,1] is the final coalgebra of

a certain functor on the category of bipointed sets. Leinster 2011 offers

a sweeping generalization of this result. He is able to represent many of what would be intuitively

called "self-similar" spaces using (a) bimodules (also called profunctors or distributors),

(b) an examination of non-degeneracy conditions on functors of various sorts; (c) a construction of

final coalgebras for the types of functors of interest using a notion of resolution. In addition to the

characterization of fractals sets as sets, his seminal paper also characterizes them as topological spaces.

Our major contribution is to suggest that in many cases of interest, point (c) above on resolutions

is not needed in the construction of final coalgebras. Instead, one may obtain a number of spaces of

interest as the Cauchy completion of an initial algebra,

and this initial algebra is the set of points in a colimit of an omega-sequence of finite metric spaces.

This generalizes Hutchinson's 1981 characterization of fractal attractors as

closures of the orbits of the critical points. In addition to simplifying the overall machinery, it also presents a metric space which is ``computationally related'' to the overall fractal. For example, when applied to Freyd's construction, our method yields the metric space.

of dyadic rational numbers in [0,1].

Our second contribution is not completed at this time, but it is a set of results on \emph{metric space}

characterizations of final coalgebras. This point was raised as an open issue in Hasuo, Jacobs, and Niqui 2010,

and our interest in quotient metrics comes from their paper. So in terms of (a)--(c) above, our work

develops (a) and (b) in metric settings while dropping (c).
Global Subsumption Revisited (Briefly)
Authors: Reger Giles , Suda Martin
Published: January 2018

Global subsumption is an existing simplification technique for saturation-based first-order theorem provers. The general idea is that we can replace a clause C by its subclause D if D follows from the initial problem as D will subsume C. The effectiveness of the technique comes from a cheap, global approach for (incompletely) checking whether D is a consequence of the initial problem. The idea is to produce and maintain a set S of ground clauses that follow from the input (e.g. grounded versions of all derived clauses) and to check whether a grounding of D follows from this set. As this is now a propositional problem this check can be performed by a SAT solver, making it efficient. In this paper we review the global subsumption technique and pose a number of questions related to the practical implementation of global subsumption and possible variations of the approach. We consider, for example, which groundings to place in S, how to select the subclause(s) D to check, how to integrate this technique with the AVATAR approach and whether it makes sense to replace the SAT solver with an SMT solver. This discussion takes place within the context of the Vampire theorem prover.
Theory-Specific Reasoning about Loops with Arrays using Vampire
Authors: Chen Yuting , Kovacs Laura , Robillard Simon
Published: January 2018

We describe new extensions of the first-order theorem prover Vampire for supporting program analysis and proving properties of loops with arrays. The common theme of our work is the symbol elimination method for generating loop invariants. In our work, we improve symbol elimination for program analysis in two ways. First, we enhance the program analysis framework of Vampire by simplifying skolemization during consequence finding. Second, we extend symbol elimination with theory-specific reasoning, in particular in the theory of polymorphic arrays, and generate and prove program properties over arrays. We illustrate our approach on a number of challenging examples coming from program analysis and verification. Our experiments show that, thanks to our improvements, programs that could not be analyzed before can now be verified with our method.
Deep Incremental Boosting
Authors: Mosca Alan , Magoulas George
Published: January 2018

This paper introduces Deep Incremental Boosting, a new technique derived from AdaBoost, specifically adapted to work with Deep Learning methods, that reduces the required training time and improves generalisation. We draw inspiration from Transfer of Learning approaches to reduce the start-up time to training each incremental Ensemble member. We show a set of experiments that outlines some preliminary results on some common Deep Learning datasets and discuss the potential improvements Deep Incremental Boosting brings to traditional Ensemble methods

in Deep Learning.
Automatic Inference of Term Equivalence in Term Rewriting Systems
Authors: Comini Marco , Torella Luca
Published: January 2018

In this paper we propose a parametric technique to automatically infer algebraic property-oriented specifications from Term Rewriting Systems. Namely, given the source code of a TRS we infer a specification which consists of a set of most general equations relating terms that rewrite, for all possible instantiations, to the same set of normal forms.

The semantic-based inference method that we propose can cope with non-constructor-based TRSs, and considers non-ground terms. Particular emphasis is posed to avoid the generation of “redundant” equations that can be a logical consequence of other ones.

To experiment on the validity of our proposal we have considered an instance of the method employing a novel (condensed) semantics for left-linear TRSs and we have implemented a “proof of concept” prototype in Haskell which is available online.
Automation for Geometry in Isabelle/HOL
Authors: Meikle Laura , Fleuriot Jacques
Published: January 2018

In this paper we describe a number of automation techniques which we have developed to assist us in reasoning formally about geometry in the interactive theorem prover Isabelle. These range from simplification rules to a user-centric integration of Isabelle with the computer algebra system QEPCAD-B. We demonstrate the power and limitations of these techniques through illustrative examples taken from our verification of a triangulation algorithm.
Efficient Rule-Matching for Hyper-Tableaux
Authors: Holen Bjarne , Hovland Dag , Giese Martin
Published: January 2018

Over the past decades, a number of calculi for automated

reasoning have been proposed that share some core features:

1. proofs are built in a tableau/sequent style as trees where

nodes are labeled with literals, and 2. these proofs are expanded

by interpreting the problem clause set as a set of rules, and

requiring all negative literals in clauses to present on a branch

for expansion. This applies to hyper-tableaux, MGTP, coherent

logic, and others. Existing implementations typically spend much

of their time in the process of matching branch literals with the

negative literals of the input clauses. We present an

alternative to this matching process by applying a modified

version of the RETE algorithm. The RETE algorithm was developed

in the 1970s for production systems in artificial

intelligence. We exploit the similarities between the mentioned

calculi and production systems in order to make the RETE

algorithm solve the matching problem. We also investigate the

effect of working on several independent branches present in

tableau proof search but not in production systems.
A Short-Term Memory for Deliberative Agents in Everyday Environments
Authors: Chichkov Ivo , Kirsch Alexandra
Published: January 2018

Humans have the impressive capability to efficiently find near-optimal solutions to complex, multi-step problems. AI planning can model such problems well, but is inefficient for realistic problems. We propose to use AI planning in combination with a short-term memory, inspired by models of human short-term memory, to structure real-world problem domains and make the planning process more efficient, while still producing satisficing solutions. We evaluate the method in the domain of a household robot.
Empirical Investigation of Learning-Based Imputation Policies
Authors: Skouteli Hara , Michael Loizos
Published: January 2018

Certain approaches for missing-data imputation propose the use of learning techniques to identify regularities and relations between attributes, which are subsequently used to impute some of the missing data. Prior theoretical results suggest that the soundness and completeness of such learning-based techniques can be improved by applying rules anew on the imputed data, as long as one is careful in choosing which rules to apply at each stage. This work presents an empirical investigation of three natural learning-based imputation policies: training rules once and applying them repeatedly; training new rules at each iteration; continuing the training of previous rules at each iteration. We examine how the three policies fare across different settings. In line with the predictions of the theory, we find that an iterative learn-predict approach is preferable.
A Proof System for Reasoning about Probabilistic Concurrent Processes
Authors: Mio Matteo
Published: January 2018

A Proof System for Reasoning about Probabilistic Concurrent Processes
Compiling Hilbert's epsilon operator
Authors: Leino Rustan
Published: January 2018

Hilbert's epsilon operator is a binder that picks an arbitrary element from

a nonempty set. The operator is typically used in logics and proof engines.

This paper contributes a discussion of considerations in supporting this operator

in a programming language. More specifically, the paper presents the design choices

made around supporting this operator in the verification-aware language Dafny.
ARCH-COMP17 Category Report: Bounded Model Checking of Hybrid Systems with Piecewise Constant Dynamics
Authors: Bu Lei , Ray Rajarshi , Schupp Stefan
Published: January 2018

This report presents results of a friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, three tools have been applied to solve three different benchmark problems in the category ofbounded model checking of hybrid systems with piecewise constant dynamics (in alphabetical order): BACH, HyDRA, and XSpeed. The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools and we also welcome more tools to join in this friendly competition in the future event.
Applicative Abstract Categorial Grammar
Authors: Kiselyov Oleg
Published: January 2018

We present the grammar/semantic formalism of Applicative Abstract

Categorial Grammar (AACG), based on the recent techniques from

functional programming: applicative functors, staged languages and

typed final language embeddings. AACG is a generalization of

Abstract Categorial Grammars (ACG), retaining the benefits of ACG as a

grammar formalism and making it possible and convenient to express a

variety of semantic theories.

We use the AACG formalism to uniformly formulate Potts' analyses of

expressives, the dynamic-logic account of anaphora, and the

continuation tower treatment of quantifier strength, quantifier

ambiguity and scope islands. Carrying out these analyses in ACG

required compromises and the ballooning of parsing complexity, or was

not possible at all. The AACG formalism brings modularity, which comes

from the compositionality of applicative functors, in contrast to

monads, and the extensibility of the typed final embedding. The

separately developed analyses of expressives and QNP are used as they

are to compute truth conditions of sentences with both these features.

AACG is implemented as a `semantic calculator', which is the ordinary

Haskell interpreter. The calculator lets us interactively write

grammar derivations in a linguist-readable form and see their yields,

inferred types and computed truth conditions. We easily extend

fragments with more lexical items and operators, and experiment with

different semantic-mapping assemblies. The mechanization lets a

semanticist test more and more complex examples, making empirical tests

of a semantic theory more extensive, organized and systematic.
SMT Encoding of Hybrid Systems in dReal
Authors: Bae Kyungmin , Kong Soonho , Gao Sicun
Published: January 2018

Analysis problems of hybrid systems, involving nonlinear real functions and ordinary differential equations, can be reduced to SMT (satisfiability modulo theories) problems over the real numbers. The dReal solver can automatically check the satisfiability of such SMT formulas up to a given precision δ > 0. This paper explains how bounded model checking problems of hybrid systems are encoded in dReal. In particular, a novel SMT syntax of dReal enables to effectively represent networks of hybrid systems in a modular way. We illustrate SMT encoding in dReal with simple nonlinear hybrid systems.