Automated Reasoning

Software model checking has become popular with the successful use of predicate abstraction and refinement techniques to find real bugs in low-level C programs. At the same time, verification approaches based on abstract interpretation and symbolic execution are also making headway in real practice. Much of the recent progress is fueled by advancements in automatic decision procedures and constraint solvers, which lie at the computational heart of these approaches. In this talk, I will describe our experience with several of these verification approaches, highlighting the roles played by automatic decision procedures and their interplay with the applications. Specifically, I will focus on SAT- and SMT-based model checking, combined with abstract domain analysis based on polyhedra representations. I will also describe some challenges from software verification that can motivate interesting research problems in this area.

Interval-based methods are commonly used for computing numerical bounds on expressions and proving inequalities on real numbers. Yet they are hardly used in proof assistants, as the large amount of numerical computations they require keeps them out of reach from deductive proof processes. However, evaluating programs inside proofs is an efficient way for reducing the size of proof terms while performing numerous computations. This work shows how programs combining automatic differentiation with floating-point and interval arithmetic can be used as efficient yet certified solvers. They have been implemented in a library for the Coq proof system. This library provides tactics for proving inequalities on real-valued expressions.

This paper presents verified quantifier elimination procedures for dense linear orders (DLO), for real and for integer linear arithmetic. The DLO procedures are new. All procedures are defined and verified in the theorem prover Isabelle/HOL, are executable and can be applied to HOL formulae themselves (by reflection).

This paper presents an extension of a decidable fragment of Separation Logic for singly-linked lists, defined by Berdine, Calcagno and O’Hearn [8]. Our main extension consists in introducing atomic formulae of the form

ls

k

(

x

,

y

) describing a list segment of length

k

, stretching from

x

to

y

, where

k

is a logical variable interpreted over positive natural numbers, that may occur further inside Presburger constraints.

We study the decidability of the full first-order logic combining unrestricted quantification of arithmetic and location variables. Although the full logic is found to be undecidable, validity of entailments between formulae with the quantifier prefix in the language

$\exists^*{\{\exists_\mathbb{N},\forall_\mathbb{N}\}^*}$

We provide here a model theoretic method, based on a parametric notion of shape graphs.

We have implemented our decision technique, providing a fully automated framework for the verification of quantitative properties expressed as pre- and post-conditions on programs working on lists and integer counters.

Relation algebras provide abstract equational axioms for the calculus of binary relations. They name an established area of mathematics and have found numerous applications in computing. We prove more than hundred theorems of relation algebras with off-the-shelf automated theorem provers. They form a basic calculus from which more advanced applications can be explored. We also present two automation experiments from the formal methods literature. Our results further demonstrate the feasibility of automated deduction with complex algebraic structures. They also open a new perspective for automated deduction in relational formal methods.

We introduce the notion of array-based system as a suitable abstraction of infinite state systems such as broadcast protocols or sorting programs. By using a class of quantified-first order formulae to symbolically represent array-based systems, we propose methods to check safety (invariance) and liveness (recurrence) properties on top of Satisfiability Modulo Theories solvers. We find hypotheses under which the verification procedures for such properties can be fully mechanized.

While program verification environments typically target source programs, there is an increasing need to provide strong guarantees for executable programs.

We establish that it is possible to reuse the proof that a source Java program meets its specification to show that the corresponding JVM program, obtained by non-optimizing compilation, meets the same specification. More concretely, we show that verification condition generators for Java and JVM programs generate the same set of proof obligations, when applied to a program

p

and its compilation [[

p

]] respectively.

Preservation of proof obligations extends the applicability of Proof Carrying Code, by allowing certificate generation to rely on existing verification technology.

Formal specifications often contain partial functions that may lead to ill-defined terms. A common technique to eliminate ill-defined terms is to require well-definedness conditions to be proven. The main advantage of this technique is that it allows us to reason in a two-valued logic even if the underlying specification language has a three-valued semantics. Current approaches generate well-definedness conditions that grow exponentially with respect to the input formula. As a result, many tools prove shorter, but stronger approximations of these well-definedness conditions instead.

We present a procedure which generates well-definedness conditions that grow linearly with respect to the input formula. The procedure has been implemented in the Spec# verification tool. We also present empirical results that demonstrate the improvements made.

Security protocols are small programs designed to ensure properties such as secrecy of messages or authentication of parties in a hostile environment. In this paper we investigate automated verification of a particular type of security protocols, called

group protocols

, in the presence of an eavesdropper, i.e., a passive attacker. The specificity of group protocols is that the number of participants is not bounded. Our approach consists in representing an infinite set of messages exchanged during an unbounded number of sessions, one session for each possible number of participants, as well as the infinite set of associated secrets. We use so-called visibly tree automata with memory and structural constraints (introduced recently by Comon-Lundh et al.) to represent over-approximations of these two sets. We identify restrictions on the specification of protocols which allow us to reduce the attacker capabilities guaranteeing that the above mentioned class of automata is closed under the application of the remaining attacker rules. The class of protocols respecting these restrictions is large enough to cover several existing protocols, such as the GDH family, GKE, and others.

Recent studies have provided many characterisations of the class of polynomial time computable functions through term rewriting techniques. In this paper we describe a (fully automatic and command-line based) system that implements the majority of these techniques and present experimental findings to simplify comparisons.

LogAnswer is an open domain question answering system which employs an automated theorem prover to infer correct replies to natural language questions. For this purpose LogAnswer operates on a large axiom set in first-order logic, representing a formalized semantic network acquired from extensive textual knowledge bases. The logicbased approach allows the formalization of semantics and background knowledge, which play a vital role in deriving answers. We present the functional LogAnswer prototype, which consists of automated theorem provers for logical answer derivation as well as an environment for deep linguistic processing.

An overview of a system modelling an intelligent agent being able to reason by using default rules is given. The semantics of the qualitative default rules is defined via ordinal conditional functions which model the epistemic state of the agent, providing her with the basic equipment to perform different knowledge management and belief revision tasks. Using the concept of Abstract State Machines, the fully operational system was developed in AsmL, allowing for a high-level implementation that minimizes the gap between the mathematical specification of the underlying concepts and the executable code in the implemented system.

Abella [3] is an interactive system for reasoning about aspects of object languages that have been formally presented through recursive rules based on syntactic structure. Abella utilizes a two-level logic approach to specification and reasoning. One level is defined by a specification logic which supports a transparent encoding of structural semantics rules and also enables their execution. The second level, called the reasoning logic, embeds the specification logic and allows the development of proofs of properties about specifications. An important characteristic of both logics is that they exploit the

λ

-tree syntax approach to treating binding in object languages. Amongst other things, Abella has been used to prove normalizability properties of the

λ

-calculus, cut admissibility for a sequent calculus and type uniqueness and subject reduction properties. This paper discusses the logical foundations of Abella, outlines the style of theorem proving that it supports and finally describes some of its recent applications.

LEO-II is a standalone, resolution-based higher-order theorem prover designed for effective cooperation with specialist provers for natural fragments of higher-order logic. At present LEO-II can cooperate with the first-order automated theorem provers E, SPASS, and Vampire. The improved performance of LEO-II, especially in comparison to its predecessor LEO, is due to several novel features including the exploitation of term sharing and term indexing techniques, support for primitive equality reasoning, and improved heuristics at the calculus level. LEO-II is implemented in Objective Caml and its problem representation language is the new TPTP THF language.

KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems. KeYmaera supports

differential dynamic logic

, which is a real-valued first-order dynamic logic for hybrid programs, a program notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically. To overcome the complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy. Our tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying collision avoidance in case studies from train control and air traffic management.

We describe the new software package

Aligator

for automatically inferring polynomial loop invariants. The package combines algorithms from symbolic summation and polynomial algebra with computational logic, and is applicable to the rich class of P-solvable loops.

Aligator

contains routines for checking the P-solvability of loops, transforming them into a system of recurrence equations, solving recurrences and deriving closed forms of loop variables, computing the ideal of polynomial invariants by variable elimination, invariant filtering and completeness check of the resulting set of invariants.

leanCoP

is a very compact theorem prover for classical first-order logic, based on the connection (tableau) calculus and implemented in Prolog.

leanCoP 2.0

enhances

leanCoP

1.0

by adding regularity, lemmata, and a technique for restricting backtracking. It also provides a definitional translation into clausal form and integrates “Prolog technology” into a lean theorem prover.

ileanCoP

is a compact theorem prover for intuitionistic first-order logic and based on the clausal connection calculus for intuitionistic logic.

leanCoP 2.0

extends the classical prover

leanCoP 2.0

by adding prefixes and a prefix unification algorithm. We present details of both implementations and evaluate their performance.

iProver is an instantiation-based theorem prover which is based on Inst-Gen calculus, complete for first-order logic. One of the distinctive features of iProver is a modular combination of instantiation and propositional reasoning. In particular, any state-of-the art SAT solver can be integrated into our framework. iProver incorporates state-of-the-art implementation techniques such as indexing, redundancy elimination, semantic selection and saturation algorithms. Redundancy elimination implemented in iProver include: dismatching constraints, blocking non-proper instantiations and propositional-based simplifications. In addition to instantiation, iProver implements ordered resolution calculus and a combination of instantiation and ordered resolution. In this paper we discuss the design of iProver and related implementation issues.

Goré and Nguyen have recently given the first optimal and sound method for global caching for the description (modal) logic

$\mathcal {ALC}$

, and various extensions. We report on an experimental evaluation for

$\mathcal {ALC}$

plus its reflexive and reflexive-transitive extensions which compares global caching, mixed caching, unsat caching and no caching, all in a single common framework implementing a depth-first search strategy. We also evaluated a version of global caching using an unrestricted search strategy which necessarily sits outside the common framework. We conclude that global caching is an improvement over the other methods in most but not all cases.

In this paper we describe a new tool for performing Knuth-Bendix completion with automatic termination tools. It is based on two ingredients: (1) the inference system for completion with multiple reduction orderings introduced by Kurihara and Kondo (1999) and (2) the inference system for completion with external termination provers proposed by Wehrman, Stump and Westbrook (2006) and implemented in the

Slothrop

system. Our tool can be used with any termination tool that satisfies certain minimal requirements. Preliminary experimental results show the potential of our tool.

Despite the remarkable development of the theory of termination of rewriting, its application to high-level programming languages is far from being optimal. This is due to the need for features such as conditional equations and rules, types and subtypes, (possibly programmable) strategies for controlling the execution, matching modulo axioms, and so on, that are used in many programs and tend to place such programs outside the scope of current termination tools.The operational meaning of such features is often formalized in a proof-theoretic manner by means of an inference system (see, e.g., [2, 3, 17]) rather than just by a rewriting relation. In particular, Generalized Rewrite Theories (GRT) [3] are a recent generalization of rewrite theories at the heart of the most recent formulation of

Maude

[4].

CLF (Concurrent LF) [CPWW02a] is a logical framework for specifying and implementing deductive and concurrent systems from areas, such as programming language theory, security protocol analysis, process algebras, and logics. Celf is an implementation of the CLF type theory that extends the LF type theory by linear types to support representation of state and a monad to support representation of concurrency. It relies on the judgments-as-types methodology for specification and the interpretation of CLF signatures as concurrent logic programs [LPPW05] for experimentation. Celf is written in Standard ML and compiles with MLton, MLKit, and SML/NJ. The source code and a collection of examples are available from

http://www.twelf.org/~celf

.

We introduce a DPLL calculus that is a decision procedure for the Bernays-Schönfinkel class, also known as EPR. Our calculus allows combining techniques for efficient propositional search with data-structures, such as Binary Decision Diagrams, that can efficiently and succinctly encode finite sets of substitutions and operations on these. In the calculus, clauses comprise of a sequence of literals together with a finite set of substitutions; truth assignments are also represented using substitution sets. The calculus works directly at the level of sets, and admits performing simultaneous constraint propagation and decisions, resulting in potentially exponential speedups over existing approaches.

We consider proof systems for effectively propositional logic. First, we show that propositional resolution for effectively propositional logic may have exponentially longer refutations than resolution for this logic. This shows that methods based on ground instantiation may be weaker than non-ground methods. Second, we introduce a generalisation rule for effectively propositional logic and show that resolution for this logic may have exponentially longer proofs than resolution with generalisation. We also discuss some related questions, such as sort assignments for generalisation.

This paper describes a system combining model-based and learning-based methods for automated reasoning in large theories, i.e. on a large number of problems that use many axioms, lemmas, theorems, definitions, and symbols, in a consistent fashion. The implementation is based on the existing

MaLARea

system, which cycles between theorem proving attempts and learning axiom relevance from successes. This system is extended by taking into account semantic relevance of axioms, in a way similar to that of the

SRASS

system. The resulting combined system significantly outperforms both

MaLARea

and

SRASS

on the MPTP Challenge large theory benchmark, in terms of both the number of problems solved and the time taken to find solutions. The design, implementation, and experimental testing of the system are described here.

We define a superposition calculus with explicit splitting and an explicit, new backtracking rule on the basis of labelled clauses. For the first time we show a superposition calculus with explicit backtracking rule sound and complete. The new backtracking rule advances backtracking with branch condensing known from

Spass

. An experimental evaluation of an implementation of the new rule shows that it improves considerably the previous

Spass

splitting implementation. Finally, we discuss the relationship between labelled first-order splitting and DPLL style splitting with intelligent backtracking and clause learning.

Satisfiability Modulo Theories (SMT) solvers have proven highly scalable, efficient and suitable for integrated theory reasoning. The most efficient SMT solvers rely on refutationally incomplete methods for incorporating quantifier reasoning. We describe a calculus and a system that tightly integrates Superposition and DPLL(T). In the calculus, all non-unit ground clauses are delegated to the DPLL(T) core. The integration is tight, dependencies on case splits are tracked as hypotheses in the saturation engine. The hypotheses are discharged during backtracking. The combination is refutationally complete for first-order logic, and its implementation is competitive in performance with E-matching based SMT solvers on problems they are good at.

One of the keys to the success of the Thousands of Problems for Theorem Provers (TPTP) problem library and related infrastructure is the consistent use of the TPTP language. This paper introduces the core of the TPTP language for higher-order logic – THF0, based on Church’s simple type theory. THF0 is a syntactically conservative extension of the untyped first-order TPTP language.