ABSTRACT. Electronic voting should offer at least the same guarantees than traditional paper-based voting systems. In order to achieve this, electronic voting protocols make use of cryptographic primitives, as in the more traditional case of authentication or key exchange protocols. All these protocols are notoriously difficult to design and flaws may be found years after their first release. Formal models, such as process algebra, Horn clauses, or constraint systems, have been successfully applied to automatically analyze traditional protocols and discover flaws. Electronic voting protocols however significantly increase the difficulty of the analysis task. Indeed, they involve for example new and sophisticated cryptographic primitives, new dedicated security properties, and new execution structures.

After an introduction to electronic voting, we will describe the current techniques for e-voting protocols analysis and review the key challenges towards a fully automated verification.

ABSTRACT. The CADE and IJCAR conferences are the major forums for the presentation of new research in all aspects of automated deduction. In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference. CASC-J7 will be held on 20th July 2014, during the 7th International Joint Conference on Automated Reasoning (IJCAR, which incorporates CADE), CASC evaluates the performance of sound, fully automatic, ATP systems. The evaluation is in terms of:

• the number of problems solved,
• the number of problems solved with a solution output, and
• the average runtime for problems solved;

in the context of:

• a bounded number of eligible problems,
• chosen from the TPTP Problem Library, and
• specified time limits on solution attempts.

The competition organizer is Geoff Sutcliffe. The competition is overseen by a panel of knowledgeable researchers who are not participating in the event. The panel members are Bernhard Beckert, Maria Paola Bonacina, and Aart Middeldorp.

ABSTRACT. The termination competition focuses on automated termination analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programming, logic programming, and functional programming. Moreover, there are also categories for automated complexity analysis. In all categories, participation of tools providing certified proofs is welcome.

In every category, all participating tools of that category are run on a randomly selected subset of the available problems. The goal of the termination competition is to demonstrate the power of the leading tools in each of these areas.

The 2014 execution of the competition is organized by Johannes Waldmann and Stefan von der Krone. The Steering Committee is formed by Jürgen Giesl, Frederic Mesnard, Albert Rubio (Chair), René Thiemann and Johannes Waldmann.

ABSTRACT. Generating the prime implicates of a formula consists in finding its most general consequences. This has many fields of application in automated reasoning, like planning and diagnosis, and although the subject has been extensively studied (and still is) in propositional logic, very few have approached the problem in more expressive logics because of its intrinsic complexity. This paper presents one such approach for flat ground equational logic. Aiming at efficiency, it intertwines an existing method to generate all prime implicates of a formula with a rewriting technique that uses atomic equations to simplify the problem by removing constants during the search. The soundness, completeness and termination of the algorithm are proven. The algorithm has been implemented and an experimental analysis is provided.

ABSTRACT. Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arithmetic. A major unsolved research challenge is to design theorem provers that are ``reasonably complete'' even in the presence of free function symbols ranging into a background theory sort. In this paper we consider the case when all variables occurring below such function symbols are quantified over a finite subset of their domains. We present a (non-naive) decision procedure for background theories extended this way on top of black-box decision procedures for the EA-fragment of the background theory. In its core, it employs a model-guided instantiation strategy for obtaining pure background formulas that are equi-satisfiable with the original formula. Unlike traditional finite model finders, it avoids exhaustive instantiation and, hence, is expected to scale better with the size of the domains. Our main results in this paper are a correctness proof and first experimental results.

ABSTRACT. Consequence finding is used in many applications of deduction.  This paper develops and evaluates a suite of optimized SMT-based algorithms for computing equality consequences over arbitrary formulas and theories supported by SMT solvers.  It is inspired by an application in the SLAyer analyzer, where our new algorithms are commonly 10-100x faster than simpler algorithms.  The main idea is to incrementally refine an initially coarse partition using models extracted from a solver.  Our approach requires only O(N) solver calls for N terms, but in the worst case creates O(N²) fresh subformulas.  Simpler algorithms, in contrast, require O(N²) solver calls.  We also describe an asymptotically superior algorithm that requires O(N) solver calls and only O(N log N) fresh subformulas.  We evaluate algorithms which reduce the number of fresh formulas required either by using specialized data structures or by relying on subformula sharing.

ABSTRACT. AProVE is a system for automated termination and complexity proofs of Java, Haskell, Prolog, and term rewrite systems (TRSs). To analyze programs in high-level programming languages, AProVE automatically converts them to TRSs. Then, a wide range of techniques is employed to prove termination and to infer complexity bounds for the resulting TRSs. Finally, the generated proofs can be exported to certify their correctness using automatic theorem proving techniques. For use in software construction, we present an AProVE plug-in for the popular Eclipse software development environment.

ABSTRACT. In this paper, we build upon our previous work on using constrained clauses in order to finitely represent possibly infinite sets of clauses.

We explore theories and theory extensions that are axiomatized by sets of constrained clauses, and we characterize syntactic criteria for their locality. We have previously shown that constrained axiomatizations are local if they are saturated under a version of resolution. The appearing constraints often capture interesting properties like reachability or extensions thereof.

We extend this result by proving that locality of saturated axiomatizations is maintained if we enrich the base theory by introducing new predicates instead of using constraints for these properties. Often, these new predicates are reachability predicates.

Applications of these results include reasoning about data structures; we indicate how the ideas can be adapted for also handling certain theories with greatest/smallest fixpoints.

ABSTRACT. While automated verification of imperative programs has been studied intensively, proving termination of programs with explicit pointer arithmetic is still an open problem. To close this gap, we introduce a novel abstract domain that can track allocated memory in detail. We use it to automatically construct a symbolic execution graph that represents all possible runs of the program. This graph is then transformed into an integer transition system, whose termination can be proved by standard techniques. We implemented this approach in the automated termination prover AProVE and demonstrate its capability of analyzing C programs with pointer arithmetic that existing tools cannot handle.

ABSTRACT. SAT and QBF solving techniques have applications in various areas. SAT-solving has also been applied in the area of formal verification of temporal properties of transition system models. Because of the limited expressive succinctness, complicated verification problems cannot be naturally represented with SAT-formulas succinctly. This paper investigates QBF-applications in this area, aiming at the verification of branching-time temporal logic properties of transition system models. Branching-time temporal logic properties involve operators that may require whether there exist certain kinds of paths starting at different states of a system model. This requires the use of quantifiers in the encoding of such properties. The focus of this paper is on temporal logic properties specified by the extended computation tree logic that allows some sort of fairness, and the main contribution of this paper is a bounded semantics for the extended computation tree logic. Then a QBF encoding of the temporal logic is developed from the definition of the bounded semantics, and then an implementation of QBF-based verification follows from the QBF encoding. Experimental evaluation of the feasibility and the computational properties of such a QBF-based verification algorithm is reported.

ABSTRACT. Answer Set Programming (ASP) is a well-established paradigm of declarative programming that has been developed in the field of logic programming and nonmonotonic reasoning. The ASP Modeling Competition 2014, held on-site collocated with the 30th International Conference on Logic Programming (ICLP), follows the spirit of Prolog Programming Contests from previous ICLP editions. That is, complex problems of various kinds are waiting to be modeled, using the ASP-Core-2 standard input language of ASP systems. Dauntless programmers, novices and experts, are encouraged to team up, take the challenge and the glory.

ABSTRACT. Cut-introduction is a technique for structuring and compressing formal proofs. In this paper we generalize our cut-introduction method for the introduction of quantified lemmas of the form ∀ x.A (for quantifier-free A) to a method generating lemmas of the form ∀ x_1 ... ∀ x_n.A. Moreover, we extend the original method to predicate logic with equality. The new method was implemented and applied to the TSTP proof database. It is shown that the extension of the method to handle equality and quantifier-blocks leads to a substantial improvement of the old algorithm.

ABSTRACT. The proof of many foundational results in structural proof theory, such as the admissibility of the cut rule and the completeness of the focusing discipline, rely on permutation lemmas. It is often a tedious and error prone task to prove such lemmas as they involve many cases. This paper describes the tool Quati which is an automated tool capable of proving a wide range of inference rule permutations for a wide number of proof systems. Given a proof system specification in the form of a theory in linear logic with subexponentials, Quati outputs in LaTeX the permutation transformations for which it was able to prove correctness and also the possible derivations for which it was not able to do so. As illustrated in this paper, Quati's output is very similar to proof derivation figures one would normally find in a proof theory book.

ABSTRACT. We describe an implementation of a new theorem prover for Intuitionistic Propositional Logic based on a sequent calculus with histories due to Corsi and Tassi. The main novelty of the prover lies in its use of dependency directed backtracking for global caching. We analyse the performance of the prover, and various optimisations, in comparison to current state of the art theorem provers and show that it produces competitive results on many classes of formulae.

ABSTRACT. MleanCoP is an automated theorem prover for first-order modal logic. The proof search is based on a prefixed connection calculus and an additional prefix unification, which captures the Kripke semantics of different modal logics. MleanCoP is implemented in Prolog and the source code of the core proof search procedure consists only of a few lines. It supports the standard modal logics D, T, S4, and S5 with constant, cumulative, and varying domain conditions. The most recent version supports heterogeneous multimodal logics and outputs a compact prefixed connection proof. An experimental evaluation shows the strong performance of MleanCoP.