Inferring Disjunctive Postconditions
Polyhedral analysis is an abstract interpretation used for automatic discovery of invariant linear inequalities among numerical variables of a program. Convexity of this abstract domain allows efficient analysis but also loses precision via convex-hull and widening operators. To selectively recover the loss of precision, sets of polyhedra (disjunctive elements) may be used to capture more precise invariants. However a balance must be struck between precision and cost. We introduce the notion of affinity to characterize how closely related is a pair of polyhedra. Finding related elements in the polyhedron (base) domain allows the formulation of precise hull and widening operators lifted to the disjunctive (powerset extension of the) polyhedron domain. We have implemented a modular static analyzer based on the disjunctive polyhedral analysis where the relational domain and the proposed operators can progressively enhance precision at a reasonable cost.
Static Approximation of Dynamically Generated Web Pages
Server-side programming is one of the key technologies that support today's WWW environment. It makes it possible to generate Web pages dynamically according to a user's request and to customize pages for each user. However, the flexibility obtained by server-side programming makes it much harder to guarantee validity and security of dynamically generated pages.
To check statically the properties of Web pages generated dynamically by a server-side program, we develop a static program analysis that approximates the string output of a program with a context-free grammar. The approximation obtained by the analyzer can be used to check various properties of a server-side program and the pages it generates.
To demonstrate the effectiveness of the analysis, we have implemented a string analyzer for the server-side scripting language PHP. The analyzer is successfully applied to publicly available PHP programs to detect cross-site scripting vulnerabilities and to validate pages they generate dynamically.
An Introduction to Relational Program Derivation
Program derivation is the synthesis of a program from its specification by mathematical means. In this talk, we are going to briefly review the history of program derivation, its objective and goals, and focus on the development from functional to relational program derivation. We will review Bird and de Moor's work on optimisation problems as an example of the application of program derivation.
Empirical Studies of Relations Between Uniform and Non-uniform Complexity
Not much is know about the relations between uniform and non-uniform complexity classes. We convert different uniform computational devices into circuit-like non-uniform devices by specializing them with respect to the size of their inputs. These automatically generated circuits are then optimized using combinatorial logic. By repeating this process for different input sizes, we attempt to see how good an estimate of the non-uniform complexity of a decision problem can be attained by automatic conversion from a uniform device solving the same problem.
Representing Cyclic Structures as Nested Datatypes
We show that cyclic structures, i.e., finite or possibly
infinite structures with back-pointers, unwindable into
possibly infinite structures, can be elegantly represented
as nested datatypes. This representation is free of the
various deficiencies characterizing the more naive
representation as mixed-variant datatypes. It is inspired by
Fiore, Plotkin and Turi's algebraic semantics of higher-order
abstract syntax and Bird and Paterson's representation of
lambda-terms as a nested datatype via the de Bruijn
notation.
(Joint work with Neil Ghani, Tarmo Uustalu and Varmo Vene)
Open data types and open functions
In object-oriented languages, it is easy to extend data by defining new classes, but it is difficult to add new functions. In functional languages, the situation is reversed: adding new functions poses no problems, but extending data (adding new data constructors) requires modifying existing code. The problem of supporting both directions of extensibility is known as the expression problem. We present open data types and open functions as a lightweight solution to the expression problem in the Haskell language. The idea is that constructors of open data types, and equations of open functions can appear scattered throughout a program. In particular, they may reside in different modules. The intended semantics is as follows: the program should behave as if the data types and functions were closed, defined in one place. The order of function equations is determined by best-fit pattern matching, where a specific pattern takes precedence over an unspecific one. We show that our solution is applicable to the expression problem, generic programming, and exceptions. We sketch possible implementations.
This is joint work with Ralf Hinze.
Type systems vs. Abstract Interpretations
We focus here on the verification of mobile systems described by process calculi, in particular, by an actor calculus.
The actor model was introduced in 87 by Agha. This model, based on a network of autonomous entities, communicating via an asynchronous protocol by sending labeled messages, is suited to represent concurrent objects. CAP, a Primitive Actor Calculus, is one of those calculi. We are interested to infere properties about mobile systems described in this formalism such as linearity (not more then one "actor" on a channel), stuck-freeness or to bound the system.
We will present the two following approaches to infere those properties: (1) behavioral type systems. With a denotational and more data-flow oriented point of view, we present type systems, similar to those of Kobayashi, Yonezawa or Ravara, intended to capture behavioral properties, but without any type annotation; (2) abstract interpretations. With an operational and more control-flow oriented conceit, we present how we express CAP into the generic framework of J. Feret.
Finally, we will compare those two guidelines and discuss which kind of properties, and how, could be captured by each framework.
An Algebraic Approach to Shortcut Fusion of Functions with a Parameter
It is known that shortcut fusion of functions with a parameter yields unsatisfactory results. In this talk, we tackle this problem in the framework of universal algebra. We first give an algebraic reformulation of the shortcut fusion by exploiting some good properties of polynomial algebras over monoids. We then propose a sufficient condition to improve the results of the algebraic shortcut fusion using concrete examples.
Jones-optimality of the partial evaluator Unmix
A natural question that comes to mind when using a partial evaluator is: "How good is it?". To answer this question one must formalize what is meant by "good" and give criteria for assessing this. In 1987, professor Neil Jones gave one such criteria which is now referred to as Jones' optimality criterion (a refined version of the original criteria can be found in Jones et al. [1]). Despite the usefulness of the criterion not much research has been done in establishing whether particular partial evaluators are Jones-optimal. For this reason I decided to investigate if the partial evaluator Unmix (a descendant of the Moscow specializer [2]) was Jones-optimal.
It turns out that Unmix actually is Jones-optimal. This talk will describe some of the key features of Unmix that makes it Jones-optimal as well as some intricacies involved in proving it.
[1] N. D. Jones, C. K. Gomard and P. Sestoft, Partial Evaluation and Automatic Program Generation. 1993. http://www.dina.kvl.dk/~sestoft/pebook/pebook.html
[2] Sergei A. Romanenko. A compiler generator produced by a self-applicable specializer can have a surprisingly natural and understandable structure. In D. Bjorner, A. P. Ershov and N. D. Jones, editors, Partial Evaluation and Mixed Computation, pages 445--463, North-Holland, 1988.
Back to the top page