Publications of year 1998

Thesis

1. J. Mallet. Compilation d'un langage spécialisé pour machine massivement parallèle. PhD thesis, Université de Rennes I, Ifsic, Irisa, 1998. [WWW] Keyword(s): parallelism, compilation, specialized language, program skeleton, data distribution, program transformation, cost analysis.

   The programming languages used for the parallel computers are either efficient languages with explicit parallelism but no portable and very complex to use, either simple portable languages but their compilation is complex and relatively inefficient. We propose a specialized language based on program skeletons encapsulating data and control flow for which an accurate cost analysis of the parallel implementation exists. The compilation process deals with the automatic choice of the data distributions on the processors through the accurate cost guaranteed by the source language. This allows to obtain an automatic compilation with an efficient parallel code (the distributions representing a global choice of parallel implementation). The compilation process is described as a series of program transformations, each transformation mapping one intermediate skeleton-based language into another. The target language is an SPMD-like skeleton-based language straightforwardly translating into a sequential language with calls to communication library routines. The main compilation steps are : the size analysis, the in-place updating transformation, the explicitation of the communications and the data distributions choice.

   
   

   @PHDTHESIS{Mallet98c,
   author = {J. Mallet},
   school = {Université de Rennes I, Ifsic, Irisa},
   title = {Compilation d'un langage spécialisé pour machine massivement parallèle},
   year = {1998},
   url = {ftp://ftp.irisa.fr/techreports/theses/1998/mallet.ps.gz},
   abstract = {The programming languages used for the parallel computers are either efficient languages with explicit parallelism but no portable and very complex to use, either simple portable languages but their compilation is complex and relatively inefficient. 
   
   We propose a specialized language based on program skeletons encapsulating data and control flow for which an accurate cost analysis of the parallel implementation exists. The compilation process deals with the automatic choice of the data distributions on the processors through the accurate cost guaranteed by the source language. This allows to obtain an automatic compilation with an efficient parallel code (the distributions representing a global choice of parallel implementation). 
   
   
   
   The compilation process is described as a series of program transformations, each transformation mapping one intermediate skeleton-based language into another. The target language is an SPMD-like skeleton-based language straightforwardly translating into a sequential language with calls to communication library routines. The main compilation steps are : the size analysis, the in-place updating transformation, the explicitation of the communications and the data distributions choice.},
   keywords = {parallelism, compilation, specialized language, program skeleton, data distribution, program transformation, cost analysis},
   
   }
   




2. V.-A. Nicolas. Preuves de propriétés de classes de programmes par dérivation systématique de jeux de test. PhD thesis, Université de Rennes I, Ifsic, Irisa, December 1998. [WWW] Keyword(s): Software engineering, program verification, white-box testing, automated test data generation, program analysis, program schemes.

   The problem addressed in this thesis is the automatic generation of test data sets enabling the proof of program properties. We thus place ourselves half-way between the domain of software testing and that of program verification. The work on software testing has lead to easy-to-use semi-automatic tools, but which rely on hypothesis difficult to verify in practice. In the domain of verification, some tools based on formal methods have been developed but they often require an user very experienced with the proof techniques used by the tool. This fact is due to indecidability problems generated by the Turing completeness of the formalisms treated. Our primary contribution is a new approach to program verification, combining the techniques of software testing and static analysis. We propose a formal method for the generation of finite test data sets, allowing one to prove that a program satisfies a given property. This method uses the program source and the property, which must belong to certain class of programs (or properties). These classes are represented by hierarchies of program schemes, which can be seen as modeling some test hypothesis. Every program belonging to one of our schemes and passing the generated test data set satisfy the tested property. For a given property our method is completely automatic and thus does not require any special competence of the user. We have implemented this method in a prototype (for a restricted functional language), for properties expressible in terms of list length.

   
   

   @PhDThesis{Nicolas-these98,
   author = {V.-A. Nicolas},
   school = {Université de Rennes I, Ifsic, Irisa},
   title = {Preuves de propriétés de classes de programmes par dérivation systématique de jeux de test},
   month = {December},
   year = {1998},
   url = {ftp://ftp.irisa.fr/techreports/theses/1998/nicolas.ps.gz},
   keywords = {Software engineering, program verification, white-box testing, automated test data generation, program analysis, program schemes},
   abstract = {The problem addressed in this thesis is the automatic generation of test data sets enabling the proof of program properties. We thus place ourselves half-way between the domain of software testing and that of program verification. The work on software testing has lead to easy-to-use semi-automatic tools, but which rely on hypothesis difficult to verify in practice. In the domain of verification, some tools based on formal methods have been developed but they often require an user very experienced with the proof techniques used by the tool. This fact is due to indecidability problems generated by the Turing completeness of the formalisms treated. Our primary contribution is a new approach to program verification, combining the techniques of software testing and static analysis. 
   
   We propose a formal method for the generation of finite test data sets, allowing one to prove that a program satisfies a given property. This method uses the program source and the property, which must belong to certain class of programs (or properties). These classes are represented by hierarchies of program schemes, which can be seen as modeling some test hypothesis. Every program belonging to one of our schemes and passing the generated test data set satisfy the tested property. For a given property our method is completely automatic and thus does not require any special competence of the user. We have implemented this method in a prototype (for a restricted functional language), for properties expressible in terms of list length.} 
   }
   

Conference articles

1. T. Jensen. Inference of polymorphic and conditional strictness properties. In Proc. of 25th ACM Symposium on Principles of Programming Languages, pages 209-221, 1998. ACM Press. [WWW]

   We define an inference system for modular strictness analysis of functional programs by extending a conjunctive strictness logic with polymorphic and conditional properties. This extended set of properties is used to define a syntax-directed, polymorphic strictness analysis based on polymorphic recursion whose soundness is established via a translation from the polymorphic system into the conjunctive system. From the polymorphic analysis, an inference algorithm based on constraint resolution is derived and shown complete for variant of the polymorphic analysis. The algorithm deduces at the same time a property and a set of hypotheses on the free variables of an expression which makes it suitable for analysis of program with module structure.

   
   

   @InProceedings{Jensen:98:Inference,
   author = {T. Jensen},
   url = {http://www.irisa.fr/lande/jensen/papers/popl98.ps},
   title = {Inference of polymorphic and conditional strictness properties},
   booktitle = {Proc. of 25th {ACM} Symposium on Principles of Programming Languages},
   year = {1998},
   pages = {209--221},
   publisher = {ACM Press},
   abstract = {We define an inference system for modular strictness analysis of functional programs by extending a conjunctive strictness logic with polymorphic and conditional properties. This extended set of properties is used to define a syntax-directed, polymorphic strictness analysis based on polymorphic recursion whose soundness is established via a translation from the polymorphic system into the conjunctive system. From the polymorphic analysis, an inference algorithm based on constraint resolution is derived and shown complete for variant of the polymorphic analysis. The algorithm deduces at the same time a property and a set of hypotheses on the free variables of an expression which makes it suitable for analysis of program with module structure.} 
   }
   




2. T. Jensen, D. Le Métayer, and T. Thorn. Security and Dynamic Class Loading in Java: A Formalisation. In Proceedings of the 1998 IEEE International Conference on Computer Languages, pages 4-15, May 1998. New York: IEEE Computer Society. [WWW]

   We give a formal specification of the dynamic loading of classes in the Java Virtual Machine (JVM) and of the visibility of members of the loaded classes. This specification is obtained by identifying the part of the run-time state of the JVM that is relevant for dynamic loading and visibility and consists of a set of inference rules defining abstract operations for loading, linking and verification of classes. The formalisation of visibility includes an axiomatisation of the rules for membership of a class under inheritance, and of accessibility of a member in the presence of accessibility modifiers such as exttt{private} and exttt{protected}. The contribution of the formalisation is twofold. First, it provides a clear and concise description of the loading process and the rules for member visibility compared to the informal definitions of the Java language and the JVM. Second, it is sufficiently simple to allow calculations of the effects of load operations in the JVM.

   
   

   @InProceedings{tjdlmtt-iccl98,
   author = {T. Jensen and D. Le~Métayer and T. Thorn},
   title = {Security and Dynamic Class Loading in Java: A Formalisation},
   url = {ftp://ftp.irisa.fr/local/lande/tjdlmtt-iccl98.ps.gz},
   booktitle = {Proceedings of the 1998 IEEE International Conference on Computer Languages},
   year = {1998},
   pages = {4--15},
   publisher = IEEECSP,
   month = may,
   abstract = {We give a formal specification of the dynamic loading of classes in the Java Virtual Machine (JVM) and of the visibility of members of the loaded classes. This specification is obtained by identifying the part of the run-time state of the JVM that is relevant for dynamic loading and visibility and consists of a set of inference rules defining abstract operations for loading, linking and verification of classes. The formalisation of visibility includes an axiomatisation of the rules for membership of a class under inheritance, and of accessibility of a member in the presence of accessibility modifiers such as 	exttt{private} and 	exttt{protected}. The contribution of the formalisation is twofold. First, it provides a clear and concise description of the loading process and the rules for member visibility compared to the informal definitions of the Java language and the JVM. Second, it is sufficiently simple to allow calculations of the effects of load operations in the JVM.} 
   }
   

Internal reports

1. T. Jensen, D. Le Métayer, and T. Thorn. Verification of control flow based security policies. Technical report 1210, IRISA, 1998. [WWW] Keyword(s): security, verification, finite-state system, control flow, object orientation.

   A fundamental problem in software-based security is whether extit{local} security checks inserted into the code are sufficient to implement a given extit{global} security policy. We introduce a formalism based on a two-level linear-time temporal logic for specifying global security policies pertaining to the control-flow of the program, and illustrate its expressive power with a number of existing policies. We define a minimalistic, security-dedicated program model that only contains procedure call and dynamic security checks and propose an automatic method for verifying that an implementation using local security constructs satisfies a global security policy. 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).

   
   

   @TechReport{jensen:98:verification,
   author = {T. Jensen and D. Le~Métayer and T. Thorn},
   institution = {IRISA},
   title = {Verification of control flow based security policies},
   number = {1210},
   year = {1998},
   url = {ftp://ftp.irisa.fr/techreports/1998/PI-1210.ps.gz},
   
   
   keywords = {security, verification, finite-state system, control flow, object orientation},
   abstract = {A fundamental problem in software-based security is whether 	extit{local} security checks inserted into the code are sufficient to implement a given 	extit{global} security policy. We introduce a formalism based on a two-level linear-time temporal logic for specifying global security policies pertaining to the control-flow of the program, and illustrate its expressive power with a number of existing policies. We define a minimalistic, security-dedicated program model that only contains procedure call and dynamic security checks and propose an automatic method for verifying that an implementation using local security constructs satisfies a global security policy. 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).} 
   }
   

This document was translated from BibT_EX by bibtex2html