Visibly pushdown Kleene algebra is an algebraic system using only propositional reasoning while still being able to represent well-known constructs of programming languages (sequences, alternatives, loops and code blocks) in a natural way. In this paper, this system is used to verify the following interprocedural compiler optimizations: interprocedural dead code elimination, inlining of functions, tail-recursion elimination, procedure reordering and function cloning. The proofs are equational and machine-verifiable.

This paper presents a complete framework for the specification and the detection of patterns as well as the abstraction of kernel traces. We propose a declarative, and easy-to-use scripting language, for the pattern specification. The compiled patterns are then fed-to a detection engine which analyzes the traces, and gradually communicates with an output module to warn the administrator about the underlying problems executing on the system. We consider that our approach is general enough to be used with any kind of traces (net work or host-based) or even combined traces. Moreover, the proposed language can describe efficiently patterns related to different types of domains like security, performance, and abstraction.

Invited Talks.- The Algorithmics of Solitaire-Like Games.- Compositionality of Secure Information Flow.- Process Algebras for Collective Dynamics.- Contributed Talks.- On Automated Program Construction and Verification.- The Logic of Large Enough.- Dependently Typed Grammars.- Abstraction of Object Graphs in Program Verification.- Subtyping, Declaratively.- Compositional Action System Derivation Using Enforced Properties.- Designing an Algorithmic Proof of the Two-Squares Theorem.- Partial, Total and General Correctness.- Unifying Theories of Programming That Distinguish Nontermination and Abort.- Adjoint Folds and Unfolds.- An Abstract Machine for the Old Value Retrieval.- A Tracking Semantics for CSP.- Matrices as Arrows!.- Lucy-n: a n-Synchronous Extension of Lustre.- Sampling, Splitting and Merging in Coinductive Stream Calculus.- Generic Point-free Lenses.- Formal Derivation of Concurrent Garbage Collectors.- Temporal Logic Verification of Lock-Freedom.- Gradual Refinement.

Kleene algebra is a great formalism for doing intraprocedural analysis and verification of programs, but it seems difficult to deal with interprocedural analysis where the power of context-free languages is often needed to represent both the program and the property. In the model checking framework, Alur and Madhusudan defined visibly pushdown automata, which accept a subclass of context-free languages called visibly pushdown languages, to do some interprocedural analyses of programs while remaining decidable. We present visibly pushdown Kleene algebra, an extension of Kleene algebra that axiomatises exactly the equational theory of visibly pushdown languages. The algebra is simply Kleene algebra along with a family of implicit least fixed point operators. Some interprocedural analyses of (mutually) recursive programs are possible in this formalism and it can deal with some non-regular properties.

This work aims to investigate conditions under which program analysis can be viewed as algebraically solving equations involving terms of subclasses of Kleene algebras and variables. In this paper, we show how to solve a kind of linear equations in which variables appear only on one side of the equality sign, over a *-continuous action lattice. Furthermore, based on the method developed for solving equations, we present how model checking of a restricted version of the linear μ-calculus over finite traces can be done by algebraic manipulations. Finally, we give some ideas on how to extend the resolution method to other classes of equations and algebraic structures.

The Lyee methodology allows the development of a software by simply defining its requirements. More precisely, a developer has only to provide words, calculation formulae, calculation conditions and layout of screens and printouts, and then leaves in the hands of the computer all subsequent troublesome programming process, i.e. control logic aspects. The formalization of Lyee methodology led to the definition of Lyee-Calculus, a formal process algebra, that easily and naturally supports the basic concepts of the Lyee methodology. Moreover, we provided an implementation of the constructs of the Lyee-Calculus in Java language in order to concretely show the efficiency of this calculus and its suitability for the Lyee methodology. In other words, this Java implementation of the Lyee-Calculus provides a means of bridging the gap between Lyee requirement specifications and their implementations. In this paper, we present a new software development environment, LyeeBuilder, that allows to automatically generate applications from specifications using a GUI interface. This software aims to give to programmers an environment that allows them to automatically generate applications from screens and word definitions.

This work aims to investigate conditions under which program analysis can be viewed as algebraically solving equations involving terms of subclasses of Kleene algebras and variables. In this paper, we show how to solve a kind of linear equations in which the variables appear only on one side of the equality sign, over an idempotent semiring with identity and zero. Furthermore, we give some ideas showing how to extend the resolution method to other classes of equations and algebraic structures.

The Lyee methodology allows the development of a software by simply defining its requirements. More precisely, a developer has only to provide words, calculation formulae, calculation conditions and layout of screens and printouts, and then leaves in the hands of the computer, all subsequent troublesome programming process, i.e. control logic aspects. The formalization of Lyee methodology led to the definition of Lyee–Calculus, a formal process algebra, that easily and naturally supports the basic concepts of the Lyee methodology. In fact, this calculus can be seen as an abstract machine, which is more suitable to support the Lyee methodology concepts than the Von Newman one. This machine considers a program as a set of molecules that interact together to produce the desired result. Basically, the Lyee–Calculus allows a high level specification of sequential, parallel and alternative processes that synchronized through communicating channels.

The goal of this paper is to present a translation function of programs written in an imperative language with array to programs written in a declarative language. The two languages used, L1 and L2, are extensions of the languages introduced by [1] which supported expressions needed by a programming language such as assignment, loops and conditional branching. To those, were added expressions related to array creation (x = allocate(y)), manipulation (x[1] = 9) and destruction (free(x)). The original translation function also needed some modifications to migrate program with array definitions from L1 to L2. Indeed, the original translation function could not handle a single variable having multiple definitions at different offsets (indexes).

The main issue of this paper is to study the problem of formal translation of programs from an imperative language to a declarative one. To that end, we define a simple imperative language, denoted by L1, that supports the basic types of statements that can be found in imperative paradigm such as assignment, looping, and selection or conditional branching. We also define a declarative language, denoted by L2, where a program is a set of independent variable definitions that may involve some special arithmetic expressions (conditional expression or recursive expression). For instance, x=5+if(a<3,2∗a,a−1) could be a definition in L2 that affects to x the value 5+2*a if a<3 and otherwise it affects the value 5+(a−1). The semantics attached to each language is denotational, where the meaning of a program in a given environment (memory state) is an environment. Finally, we introduce a formal translation function that migrates any program in L1 to an equivalent (with respect to the semantics) one in L2 and we prove its correctness (the semantics of the original version of any program is equal to the semantics of its translated version).

In this paper we present a new approach to stateful intrusion detection. It is based on a temporal logic which has the capability to express temporary properties, which are properties lying between events. The detection of those events can in turn depend of others temporary properties. The aim of this logic is to model knowledge gathering. It is basically propositional logic, to which we’ve added a single temporal operator, which allows to define limits of temporary properties.

The Lyee methodology allows the development of a software by simply defining its requirements. More precisely, a developer has only to provide words, calculation formulae, calculation conditions and layout of screens and printouts, and then leaves in the hands of the computer all subsequent troublesome programming process, i.e. control logic aspects. The formalization of Lyee methodology led to the definition of Lyee-Calculus, a formal process algebra, that easily and naturally supports the basic concepts of the Lyee methodology. In fact, this calculus can be seen as an abstract machine which is more suitable to support the Lyee methodology concepts than the Von Newman one. This machine considers a program as a set of molecules that interact together to produce the desired result. Basically, the Lyee-Calculus allows a high level specification of sequential, parallel and alternative processes that synchronized through communicating channels. This paper provides an implementation of the constructs of the Lyce-Calculus in the Java language in order to concretely show the efficiency of this calculus and its suitability for the Lyee methodology. Moreover, this implementation aims to give to programmers an environment that allows them to automatically generate applications from formal descriptions in Lyee-Calculus. In other words, this Java implementation of the Lyee-Calculus provides a means of bridging the gap between Lyee requirement specifications and their implementations.

This paper introduces an algebraic approach that aims to enforce a security policy on a given computer network. More precisely, given a network and a security policy, we want to automatically generate the necessary monitors (a single fire-wall or many ones where each of them controls a part of the networks) that force the network to be secure according to the security policy definition. In this approach, the network is formalized as a process P , the security policy is formally specified as a formula Φ and the problem is to find a process M (monitor) such that P M |= Φ. Once this step is completed, some results about equivalence between processes can be used to distribute the monitor over the network. In other words, the equivalence results aims to break the monitor M into small slices that will be distributed so that each slice controls only a small part of the network.

The main issue of this paper is to study the problem of formal translation of programs from an imperative language to a declarative one. To that end, we define a simple imperative language, denoted by L-1, that supports the basic types of statements that can be found in imperative paradigm such as assignment, looping, and selection or conditional branching. We also define a declarative language, denoted by L-2, Where a program is a set of independent variable definitions that may involve some special arithmetic expressions (conditional expression or recursive expression). For instance x = 5 + if(a < 3, 2 * a, a - 1) could be a definition in L-2 that affects to x the value 5 + 2 * a if a < 3 and otherwise it affects the value 5 + (a - 1). The semantics attached to each language is denotational, where the meaning of a program in a given environment (memory state) is an environment. Finally, we introduce a formal translation function that migrates any program in L-1 to an equivalent (with respect to the semantics) one in L-2 and we prove its correctness (the semantics of the original version of any program is equal to the semantics of its translated version).

Software development has been suffering, for many decades, from the lack of simple and powerful methodologies and tools. Despite the tremendous advances in this research field, the crisis has still not been overcome and the proposed remedies are far from resolving the problems of software development and maintenance. Lately, a new and very promising methodology, called Lyee, has been proposed. It aims to automatically generate programs from simple user requirements.The purpose of this paper is, on the one hand, to provide a short and technical introduction to the Lyee methodology, and on the other hand, to show how some classical static analysis techniques (execution time and memory space optimization, typing, slicing, etc.) can considerably improve many aspects of this new methodology.

Software development has been suffering, for many decades, from the lack of simple and powerful methodologies and tools. Despite the tremendous advances in this research field, the crisis has still not overcome and the proposed remedies are far from resolving the problems of software development and maintenance. Lately, a new and very promising methodology, called Lyee, has been proposed. It aims to automatically generate programs from simple user requirements. The purpose of this paper is, in one hand, to give a short and technical introduction to the Lyee methodology. And, in the other hand, to show how some classical static analysis techniques (execution time and memory space optimization, typing, slicing, etc.) can considerably improve many aspects of this new methodology.

With the advent and the rising popularity of networks, Internet, intranets and distributed systems, security is becoming one of the major concerns in IT research. An increasing number of approaches have been proposed to ensure the safety and security of programs. Among those approaches, certified code seems to be the most promising. Unfortunately, as of today, most of the research on certified code have focused on simple type safety and memory safety, rather than security issues. We therefore propose to extend this approach to the security aspects of a program. Our intention is to use such an approach as an efficient and realistic solution to the problem of malicious code detection in COTS. In this paper we present our progress in defining and implementing a certifying compiler that produces a secure self-certified code that can be used to ensure both safety and security of the code.