Beyond their differences, most black-box explanation methods share a number of features and can be framed in a common structure. We identify these features and propose a generic and parameterized framework which makes it possible to combine them in different ways. This framework has been implemented in a proof of concept system called IBEX (for "Interactive Black-box EXplanation system"). IBEX makes it possible to address a variety of needs of different types of explainees (e.g. local or global explanations, detailed or simple explanations, explanations in the form of counterfactuals, rules, plots, etc.). We illustrate the benefit of the approach in terms of versatility through several case studies corresponding to different types of explainees.

While the control of individuals over their personal data is increasingly seen as an essential component of their privacy, the word "control" is usually used in a very vague way, both by lawyers and by computer scientists. This lack of precision may lead to misunderstandings and makes it difficult to check compliance. To address this issue, we propose a formal framework based on capacities to specify the notion of control over personal data and to reason about control properties. We illustrate our framework with social network systems and show that it makes it possible to characterize the types of control over personal data that they provide to their users and to compare them in a rigorous way.

The privacy by design approach has already been applied in different areas. We believe that the next challenge in this area today is to go beyond individual cases and to provide methodologies to explore the design space in a systematic way. As a first step in this direction, we focus in this paper on the data minimization principle and consider different options using decentralized architectures in which actors do not necessarily trust each other. We propose a framework to express the parameters to be taken into account (the service to be performed, the actors involved, their respective requirements, etc.) and an inference system to derive properties such as the possibility for an actor to detect potential errors (or frauds) in the computation of a variable. This inference system can be used in the design phase to check if an architecture meets the requirements of the parties or to point out conflicting requirements.

LISE is a multidisciplinary project involving lawyers and computer scientists with the aim to put forward a set of methods and tools to (1) define software liability in a precise and unambiguous way and (2) establish such liability in case of incident. This paper provides an overview of the overall approach taken in the project based on a case study. The case study illustrates a situation where, in order to reduce legal uncertainties, the parties to a contract wish to include in the agreement specific clauses to define as precisely as possible the share of liabilities between them for the main types of failures of the system.

Establishing contractual liabilities in case of litigation is generally a delicate matter. It becomes even more challenging when IT systems are involved. At the core of the problem lies the issue of the evidence provided by the opposing parties. We believe that the means to constitute evidence that could be used in case of conflict should be considered from the onset of IT projects and be part of the requirements for the design of IT systems. This paper proposes criteria for acceptable log architectures depending on the features of the system and the potential claims between the parties. We establish properties guaranteed by acceptable architectures and illustrate our framework with a travel booking system.

A fundamental problem in software-based security is whether local security checks inserted into the code are sufficient to implement a global security property. This article introduces a formalism based on a linear-time temporal logic for specifying global security properties pertaining to the control flow of the program, and illustrates its expressive power with a number of existing properties. We define a minimalistic, security-dedicated program model that only contains procedure call and run-time security checks and propose an automatic method for verifying that an implementation using local security checks satisfies a global security property. We then show how to instantiate the framework to the security architecture of Java 2 based on stack inspection and privileged method calls.

A fundamental problem in software based security is whether local security checks inserted into the code are sufficient to implement a global security property. We introduce a formalism based on a two-level linear time temporal logic for specifying global security properties pertaining to the control flow of the program, and illustrate its expressive power with a number of existing properties. We define a minimalistic, security dedicated program model that only contains procedure call and run time security checks and propose an automatic method for verifying that an implementation using local security checks satisfies a global security property. For a given formula in the temporal logic, we prove that there exists a bound on the size of the states that have to be considered in order to assure the validity of the formula: this reduces the problem to finite state model checking. Finally, we instantiate the framework to the security architecture proposed for Java (JDK 1.2).

Slicing analyses have been proposed for different programming languages. Rather than defining a new analysis from scratch for each programming language, we would like to specify such an analysis once and for all, in a language-independent way, and then specialize it for different programming languages. In order to achieve this goal, we propose a notion of natural semantics format and a dynamic slicing analysis format. The natural semantics format formalizes a class of natural semantics and the analysis format is a generic, language-independent, slicing analysis. The correctness of the generic analysis is established as a relation between the derivation trees of the original program and the slice. This generic analysis is then instantiated to several programming languages conforming to the semantics format (an imperative language, a logic programming language and a functional language), yielding a dynamic slicing analyzer for each of these languages.

We believe that software architectures should provide an appropriate basis for the proof of properties of large software. This goal can be achieved through a clearcut separation between computation and communication and a formal definition of the interactions between individual components. We present a formalism for the definition of software architectures in terms of graphs. Nodes represent the individual agents and edges define their interconnection. Individual agents can communicate only along the links specified by the architecture. The dynamic evolution of an architecture is defined independently by a "coordinator". An architecture style is a class of architectures specified by a graph grammar. The class characterizes a set of architectures sharing a common communication pattern. The rules of the coordinator are statically checked to ensure that they preserve the constraints imposed by the architecture style.

We present CASTING, a computer assisted software test engineering method. The method, supported by a prototype tool, generates realistic software test suites in a formal and semi-automatic way. Based on a two-layer modular architecture, CASTING is not tied to any particular style of input. Initially designed to engineer functional test suites from formal specifications, CASTING can easily be instantiated to accept other formal description levels, seamlessly supporting the main industrial testing techniques, ranging from functional testing to structural testing. A simple process scheduler specification is used in this paper to illustrate the interaction facilities of CASTING and to provide a sample of the resulting test suites.

Type systems currently available for imperative languages are too weak to detect a significant class of programming errors. For example, they cannot express the property that a list is doubly-linked or circular. We propose a solution to this problem based on a notion of shape types defined as context-free graph grammars. We define graphs in set-theoretic terms, and graph modifications as multiset rewrite rules. These rules can be checked statically to ensure that they preserve the structure of the graph specified by the grammar. We provide a syntax for a smooth integration of shape types in C. The programmer can still express pointer manipulations with the expected constant time execution and benefits from the additional guarantee that the property specified by the shape type is an invariant of the program.

We present a formalism for the definition of software architectures in terms of graphs. Nodes represent the individual agents and edges define their interconnection. Individual agents can communicate only along the links specified by the architecture. The dynamic evolution of the overall architecture is defined independently by a 'coordinator'. An architecture style is a class of architectures characterised by a graph grammar. The rules of the coordinator are statically checked to ensure that they preserve the constraints imposed by the architecture style.

Abstract A substantial amount of work has been devoted to the proof of correctness of various program analyses but much less attention has been paid to the correctness of compiler optimisations based on these analyses. In this paper we tackle the problem in the context of strictness analysis for lazy functional languages. We show that compiler optimisations based on strictness analysis can be expressed formally in the functional framework using continuations. This formal presentation has two benefits: it allows us to give a rigorous correctness proof of the optimised compiler; and it exposes the various optimisations made possible by a strictness analysis.

We present a technique for the mechanical proof of correctness properties of programs.We define a language of properties over recursive data structures and an inference system to assign properties to programs.In order to be able to design a tractable inference algorithm, we impose restrictions on both the programming language and the language of properties.We show that these restrictions do not preclude the treat ment of int cresting programs and properties.As an example, our analyser is able to prove automatically that a sort program returns a list of non-increasing values.

The role of non-standard type inference in static program analysis has been much studied recently. Early work emphasised the efficiency of type inference algorithms and paid little attention to the correctness of the inference system. Recently more powerful inference systems have been investigated but the connection with efficient inference algorithms has been obscured. The contribution of this paper is twofold: first we show how to transform a program logic into an algorithm and, second, we introduce the notion of lazy types and show how to derive an efficient algorithm or strictness analysis.

We tackle the problems of correctness and efficiency of paralled implementations of functional languages. We present a compilation technique described in terms of program transformations in the functional framework. The original functional expression is transformed into a functional term, which can be seen as traditional machine code. The main feature of the parallel implementation is the use of continuations. We introduce a parallel abstract machine describing lazy task creation in terms of exportation of continuations. The advantages of the approach are twofold: (1)correetness proofs are made simpler and (2) the implementation is efficient because the use of continuations reduces the task management overhead.

One of the most important issues concerning functional languages is the efficiency and the correctness of their implementation. We focus on sequential implementations for conventional von Neumann computers. The compilation process is described in terms of program transformations in the functional framework. The original functional expression is transformed into a functional term that can be seen as a traditional machine code. The two main steps are the compilation of the computation rule by the introduction of continuation functions and the compilation of the environment management using combinators. The advantage of this approach is that we do not have to introduce an abstract machine, which makes correctness proofs much simpler. As far as efficiency is concerned, this approach is promising since many optimizations can be described and formally justified in the functional framework.

There has been a great deal of research done on the evaluation of the complexity of particular algorithms; little effort, however, has been devoted to the mechanization of this evaluation. The ACE (Automatic Complexity Evaluator) system is able to analyze reasonably large programs, like sorting programs, in a fully mechanical way. A time-complexity function is derived from the initial functional program. This function is transformed into its nonrecursive equivalent according to MacCarthy's recursion induction principle, using a predefined library of recursive definitions. As the complexity is not a decidable property, this transformation will not be possible in all cases. The richer the predefined library is, the more likely the system is to succeed. The operations performed by ACE are described and the use of the system is illustrated with the analysis of a sorting algorithm. Related works and further improvements are discussed in the conclusion.