Catálogo de publicaciones - libros

The dependency pair approach is one of the most powerful techniques for automated termination proofs of term rewrite systems. Up to now, it was regarded as one of several possible methods to prove termination. In this paper, we show that dependency pairs can instead be used as a general concept to integrate arbitrary techniques for termination analysis. In this way, the benefits of different techniques can be combined and their modularity and power are increased significantly. We[2] refer to this new concept as the “dependency pair ” to distinguish it from the old “dependency pair ”. Moreover, this framework facilitates the development of new methods for termination analysis. To demonstrate this, we present several new techniques within the dependency pair framework which simplify termination problems considerably. We implemented the dependency pair framework in our termination prover AProVE and evaluated it on large collections of examples.

Incompletely defined programs provide an elegant and easy way to write and to reason about programs which may halt with a run time error by throwing an exception or printing an error message, e.g. when attempting to divide by zero. Due to the presence of stuck computations, which arise when calling incompletely defined procedures with invalid arguments, we cannot use the method of argument bounded algorithms for proving termination by machine. We analyze the problem and present a solution to improve this termination analysis method so that it works for incompletely defined programs as well. Our technique of proving the termination of incompletely defined programs maintains performance as well as simplicity of the original method and proved successful by an implementation in the verification tool eriFun.

We present a program logic for verifying the heap consumption of low-level programs. The proof rules employ a uniform assertion format and have been derived from a general purpose program logic [1]. In a proof-carrying code scenario, the inference of invariants is delegated to the code provider, who employs a certifying compiler that generates a certificate from program annotations and analysis. The granularity of the proof rules matches that of the linear type system presented in [6], which enables us to perform verification by replaying typing derivations in a theorem prover, given the specifications of individual methods. The resulting verification conditions are of limited complexity, and are automatically discharged. We also outline a proof system that relaxes the linearity restrictions and relates to the type system of usage aspects presented in [2].

Guessing, or dictionary, attacks arise when an intruder exploits the fact that certain data like passwords may have low entropy, i.e. stem from a small set of values. In the case of off-line guessing, in particular, the intruder may employ guessed values to analyze the messages he has observed. Previous attempts at formalizing off-line guessing consist of extending a Dolev-Yao-style intruder model with inference rules to capture the additional capabilities of the intruder concerning guessable messages. While it is easy to convince oneself that the proposed rules are correct, in the sense that an intruder can actually perform such “guessing steps”, it is difficult to see whether such a system of inference rules is complete in the sense that it captures all the kinds of attacks that we would intuitively call “guessing attacks”. Moreover, the proposed systems are specialized to particular sets of cryptographic primitives and intruder capabilities. As a consequence, these systems are helpful to discover some off-line guessing attacks but are not fully appropriate for formalizing what off-line guessing precisely means and verifying that a given protocol is not vulnerable to such guessing attacks.

In this paper, we give a formalization of off-line guessing by defining a deduction system that is uniform and general in that it is independent of the overall protocol model and of the details of the considered intruder model, i.e. cryptographic primitives, algebraic properties, and intruder capabilities.

(PCC) is a general approach to mobile code safety in which programs are augmented with a certificate (or proof). The practical uptake of PCC greatly depends on the existence of a variety of enabling technologies which allow both to prove programs correct and to replace a costly verification process by an efficient checking procedure on the consumer side. In this work we propose (ACC), a novel approach which uses abstract interpretation as enabling technology. We argue that the large body of applications of abstract interpretation to program verification is amenable to the overall PCC scheme. In particular, we rely on an expressive class of safety policies which can be defined over different abstract domains. We use an (or abstract model) of the program computed by standard static analyzers as a certificate. The validity of the abstraction on the consumer side is checked in a single-pass by a very efficient and specialized abstract-interpreter. We believe that ACC brings the expressiveness, flexibility and automation which is inherent in abstract interpretation techniques to the area of mobile code safety. We have implemented and benchmarked ACC within the system preprocessor. The experimental results show that the checking phase is indeed faster than the proof generation phase, and that the sizes of certificates are reasonable.

We develop a general language model for sequential imperative programs together with a Hoare logic. We instantiate the framework with common programming language constructs and integrate it into Isabelle/HOL, to gain a usable and sound verification environment.

State-of-the-art first-order automated theorem proving systems have reached considerable strength over recent years. However, in many areas of mathematics they are still a long way from reliably proving theorems that would be considered relatively simple by humans. For example, when reasoning about sets, relations, or functions, first-order systems still exhibit serious weaknesses. While it has been shown in the past that higher-order reasoning systems can solve problems of this kind automatically, the complexity inherent in their calculi and their inefficiency in dealing with large numbers of clauses prevent these systems from solving a whole range of problems.

We present a solution to this challenge by combining a higher-order and a first-order automated theorem prover, both based on the resolution principle, in a flexible and distributed environment. By this we can exploit concise problem formulations without forgoing efficient reasoning on first-order subproblems. We demonstrate the effectiveness of our approach on a set of problems still considered non-trivial for many first-order theorem provers.

Relations among program variables like 1 + 3 · + 5 · ≡ 0 [224] have been called . Such a relation is at a program point iff it is satisfied by all reaching program states. Knowledge about non-trivial valid congruence relations is crucial for various aggressive program transformations. It can also form the backbone of a program correctness proof.

In his seminal paper [1], Philippe Granger presents an intraprocedural analysis which is able to infer linear congruence relations between integer variables. For affine programs, i.e., programs where all assignments are affine expressions and branching is non-deterministic, Granger’s analysis is , i.e., infers valid congruence relations between variables. No upper bound, though, has been proven for Granger’s algorithm. Here, we present a variation of Granger’s analysis which runs in polynomial time. Moreover, we provide an interprocedural extension of this algorithm. The polynomial algorithm as well as its interprocedural extension are obtained by means of multiple instances of a general framework for constructing interprocedural analyses of numerical properties. This framework can be used for different numerical domains such as fields or modular rings and thus also covers the interprocedural analyses of [2,3] where valid affine relations are inferred.

We also indicate how the base technique can be extended to deal with equality guards in the interprocedural setting.

Matching is a basic operation extensively used in computation. Second-order matching, in particular, provides an adequate environment for expressing program transformations and pattern recognition for automated deduction. The past few years have established the benefit of using explicit substitutions for theorem proving and higher-order unification. In this paper, we will make use of explicit substitutions to facilitate matching: we develop a second-order matching algorithm via the -style of explicit substitutions. We introduce a convenient notation for matching in the -calculus. This notation keeps the matching equations separated from the incremental graftings. We characterise an important class of second-order matching problems which is essential to prove termination of the algorithm. In addition, we illustrate how the algorithm works through some examples.

To produce a program guaranteed to satisfy a given specification one can synthesize it from a formal constructive proof that a computation satisfying that specification exists. This process is particularly effective if the specifications are written in a high-level language that makes it easy for designers to specify their goals. We consider a high-level specification language that results from adding to a fragment of Nuprl specifically tailored for specifying distributed protocols, called . We then show how high-level can be synthesized from the knowledge-based specifications using a proof development system such as Nuprl. Methods of Halpern and Zuck [15] then apply to convert these knowledge-based protocols to ordinary protocols. These methods can be expressed as heuristic transformation tactics in Nuprl.