Publications of year 2007

Thesis

S. Hong Tuan Ha. Programmation par aspects et tissage de propriétés - Application à l'ordonnancement et à la disponibilité.. PhD thesis, Université Rennes 1, January 2007.

@PhdThesis{hongtuanha:phd:07,
author = {S. {Hong~Tuan~Ha}},
title = {Programmation par aspects et tissage de propriétés - Application à l'ordonnancement et à la disponibilité.},
school = {Université Rennes 1},
year = 2007,
month = {January} 
}

G. Le Guernic. Confidentiality Enforcement Using Dynamic Information Flow Analyses. PhD thesis, Université Rennes 1 and Kansas State University, September 2007.

@PhdThesis{Guernic:phd:07,
author = {G. {Le Guernic}},
title = {Confidentiality Enforcement Using Dynamic Information Flow Analyses},
school = {Université Rennes 1 and Kansas State University},
year = 2007,
month = {September} 
}

Articles in journal or book chapters

Benjamin Blanc, Arnaud Gotlieb, and Claude Michel. Constraints in Software Testing, Verification and Analysis. In Frédéric Benhamou, Narendra Jussien, and Barry O'Sullivan, editors, Trends in Constraint Programming, Part 7, pages 333-368. ISTE, London, UK, May 2007.

@InCollection{wscp/part7,
author = {Benjamin Blanc and Arnaud Gotlieb and Claude Michel},
title = {Constraints in Software Testing, Verification and Analysis},
chapter = {7},
type = {Part},
pages = {333--368},
editor = {Fr{\'e}d{\'e}ric Benhamou and Narendra Jussien and Barry O'Sullivan},
booktitle = {Trends in Constraint Programming},
publisher = {ISTE},
year = {2007},
month = may,
isbn = 9781905209972,
address = {London, UK},

}

A. Gotlieb, T. Denmat, and B. Botella. Goal-oriented test data generation for pointer programs. Information and Software Technology, 49(9-10):1030-1044, Sep. 2007.

@Article{GDB07,
author = {Gotlieb, A. and Denmat, T. and Botella, B.},
title = {Goal-oriented test data generation for pointer programs},
journal = {Information and Software Technology},
volume = {49},
number = {9-10},
pages = {1030-1044},
address = {Elsevier},
month = {Sep.},
year = {2007},

}

Conference articles

Elvira Albert, Miguel Gómez-Zamalloa, Laurent Hubert, and Germán Puebla. Verification of Java Bytecode Using Analysis and Transformation of Logic Programs. In PADL, pages 124-139, 2007. [PDF]

@InProceedings{albert07:_verif_java_bytec_trans_analy,
author = {Elvira Albert and Miguel G{\'o}mez-Zamalloa and Laurent Hubert and Germ{\'a}n Puebla},
title = {Verification of Java Bytecode Using Analysis and Transformation of Logic Programs},
booktitle = {PADL},
year = 2007,
pages = {124-139},
pdf = {http://www.trebuh.net/publi/padl07.pdf} 
}

Gilles Barthe, David Pichardie, and Tamara Rezk. A Certified Lightweight Non-Interference Java Bytecode Verifier. In Proc. of 16th European Symposium on Programming (ESOP'07), volume 4421 of Lecture Notes in Computer Science, pages 125-140, 2007. Springer-Verlag.

@InProceedings{BPR07,
AUTHOR = {Gilles Barthe and David Pichardie and Tamara Rezk},
TITLE = {{A Certified Lightweight Non-Interference Java Bytecode Verifier}},
BOOKTITLE = {Proc.\ of 16th European Symposium on Programming (ESOP'07)},
YEAR = {2007},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
volume = {4421},
pages = {125-140},

}

Frédéric Besson, Thomas Jensen, and Tiphaine Turpin. Small Witnesses for Abstract Interpretation-Based proofs. In Proc. of 16th European Symposium on Programming, volume 4421 of Lecture Notes in Computer Science, pages 268-283, 2007. Springer.

@InProceedings{BJT07,
author = "Frédéric Besson and Thomas Jensen and Tiphaine Turpin",
title = "Small Witnesses for Abstract Interpretation-Based proofs",
booktitle = "Proc. of 16th European Symposium on Programming",
pages = "268--283",
series = {Lecture Notes in Computer Science},
volume = {4421},
publisher = "Springer",
year = 2007 
}

Y. Boichut, T. Genet, Y. Glouche, and O. Heen. Using Animation to Improve Formal Specifications of Security Protocols. In Joint conference SAR-SSI, 2007.

@inproceedings{BoichutGGH-SAR07,
author = {Boichut, Y. and Genet, T. and Glouche, Y. and Heen, O.},
title = {{U}sing {A}nimation to {I}mprove {F}ormal {S}pecifications of {S}ecurity {P}rotocols},
booktitle = {Joint conference SAR-SSI},
year = {2007} 
}

Y. Boichut, T. Genet, T. Jensen, and L. Leroux. Rewriting Approximations for Fast Prototyping of Static Analyzers. In RTA, volume 4533 of LNCS, pages 48-62, 2007. Springer Verlag.

@inproceedings{BoichutGJL-RTA07,
author = {Boichut, Y. and Genet, T. and Jensen, T. and Leroux, L.},
title = {Rewriting {A}pproximations for {F}ast {P}rototyping of {S}tatic {A}nalyzers},
booktitle = {RTA},
year = {2007},
pages = {48-62},
volume = {4533},
series = {LNCS},
publisher = {Springer Verlag} 
}

F. Charreteur, B. Botella, and A. Gotlieb. Modelling dynamic memory management in Constraint-Based Testing. In TAIC-PART (Testing: Academic and Industrial Conference), Windsor, UK, Sep. 2007.

@InProceedings{CBG07,
author = {Charreteur, F. and Botella, B. and Gotlieb, A.},
title = {Modelling dynamic memory management in Constraint-Based Testing},
booktitle = {TAIC-PART (Testing: Academic and Industrial Conference)},
address = {Windsor, UK},
month = {Sep.},
year = 2007,

}

T. Denmat, A. Gotlieb, and M. Ducasse. An Abstract Interpretation Based Combinator for Modeling While Loops in Constraint Programming. In Proceedings of Principles and Practices of Constraint Programming (CP'07), Springer Verlag, LNCS 4741, Providence, USA, pages 241-255, Sep. 2007.

@InProceedings{DGD07a,
author = {Denmat, T. and Gotlieb, A. and Ducasse, M.},
title = {An Abstract Interpretation Based Combinator for Modeling While Loops in Constraint Programming},
booktitle = {Proceedings of Principles and Practices of Constraint Programming (CP'07)},
series = {Springer Verlag, LNCS 4741},
pages = {241--255},
month = {Sep.},
year = 2007,
address = {Providence, USA},

}

T. Denmat, A. Gotlieb, and M. Ducasse. Improving Constraint-Based Testing with Dynamic Linear Relaxations. In 18th IEEE International Symposium on Software Reliability Engineering (ISSRE' 2007), Trollhättan, Sweden, Nov. 2007.

@InProceedings{DGD07b,
author = {Denmat, T. and Gotlieb, A. and Ducasse, M.},
title = {Improving Constraint-Based Testing with Dynamic Linear Relaxations},
booktitle = {18th IEEE International Symposium on Software Reliability Engineering (ISSRE' 2007)},
address = {Trollhättan, Sweden},
month = {Nov.},
year = 2007,

}

G. Le Guernic. Automaton-based Confidentiality Monitoring of Concurrent Programs. In Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSFS20), JUL 6--8 2007. IEEE Computer Society.

Noninterference is typically used as a baseline security policy to formalize confidentiality of secret i nformation manipulated by a program. In contrast to static checking of noninterference, this paper consid ers dynamic, au\-to\-maton-based, monitoring of information flow for a single execution of a concurrent p rogram. The monitoring mechanism is based on a combination of dynamic and static analyses. During program execution, abstractions of program events are sent to the automaton, which uses the abstractions to track information flows and to control the execution by forbidding or editing dangerous actions. All monitore d executions are proved to be noninterfering (soundness) and executions of programs that are well-typed i n a security type system similar to the one of Smith and Volpano are proved to be unaltered by the monitor (partial transparency).

@INPROCEEDINGS{LeGuernic2007acmocp,
BOOKTITLE = {Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSFS20)},
YEAR = 2007,
MONTH = JUL # { 6--8},
LOCATION = {S. Servolo island, Venice, Italy},
PUBLISHER = {IEEE Computer Society},
ISBN = {0-7695-2819-8},
ISSN = {1063-6900},
AUTHOR = {G. Le~Guernic},
TITLE = {{A}utomaton-based {C}onfidentiality {M}onitoring of {C}oncurrent {P}rograms},
ABSTRACT = {Noninterference is typically used as a baseline security policy to formalize confidentiality of secret i nformation manipulated by a program. In contrast to static checking of noninterference, this paper consid ers dynamic, au\-to\-maton-based, monitoring of information flow for a single execution of a concurrent p rogram. The monitoring mechanism is based on a combination of dynamic and static analyses. During program execution, abstractions of program events are sent to the automaton, which uses the abstractions to track information flows and to control the execution by forbidding or editing dangerous actions. All monitore d executions are proved to be noninterfering (soundness) and executions of programs that are well-typed i n a security type system similar to the one of Smith and Volpano are proved to be unaltered by the monitor (partial transparency).} 
}

G. Le Guernic. Information Flow Testing. In Proceedings of the Annual Asian Computing Science Conference, Lecture Notes in Computer Science, DEC 9--11 2007. Note: To appear.

Noninterference, which is an information flow property, is typically used as a baseline security policy to formalize confidentiality of secret information manipulated by a program. Noninterference verification mechanisms are usually based on static analyses and, to a lesser extent, on dynamic analyses. In contrast to those works, this paper proposes an information flow testing mechanism. This mechanism is sound from the point of view of noninterference. It is based on standard testing techniques and on a combination of dynamic and static analyses. Concretely, a semantics integrating a dynamic information flow analysis is proposed. This analysis makes use of static analyses results. This special semantics is built such that, once a path coverage property has been achieved on a program, a sound conclusion regarding the noninterfering behavior of the program can be established.

@INPROCEEDINGS{leguernic07ift,
AUTHOR = {G. Le~Guernic},
TITLE = {{I}nformation {F}low {T}esting},
BOOKTITLE = {Proceedings of the Annual Asian Computing Science Conference},
YEAR = 2007,
SERIES = {Lecture Notes in Computer Science},
MONTH = DEC # { 9--11},
LOCATION = {Doha, Qatar},
NOTE = {To appear},
ABSTRACT = {Noninterference, which is an information flow property, is typically used as a baseline security policy to formalize confidentiality of secret information manipulated by a program. Noninterference verification mechanisms are usually based on static analyses and, to a lesser extent, on dynamic analyses. In contrast to those works, this paper proposes an information flow testing mechanism. This mechanism is sound from the point of view of noninterference. It is based on standard testing techniques and on a combination of dynamic and static analyses. Concretely, a semantics integrating a dynamic information flow analysis is proposed. This analysis makes use of static analyses results. This special semantics is built such that, once a path coverage property has been achieved on a program, a sound conclusion regarding the noninterfering behavior of the program can be established.} 
}

G. Le Guernic and J. Perret. FLIC: Application to Caching of a Dynamic Dependency Analysis for a 3D Oriented CRS. In Proceedings of the International Workshop on Rule-Based Programming, Electronic Notes in Theoretical Computer Science (ENTCS), JUN 29 2007. Elsevier. Note: To appear.

FL-systems are conditional rewriting systems. They are used for programming (describing) and evaluating (generating) huge 3D virtual environments, such as cities and forests. This paper presents a formal semantics and a dynamic dependency analysis for FL-systems. This analysis allows the characterization of a set of terms which are joinable with the currently rewritten term. Consequently, it is possible to speed up the rewriting steps of the environments generation by using a cache mechanism which is smarter than standard ones. This work can be seen as a dynamic completion of a set of rewriting rules. This completion increases the number of terms which are rewritten in normal form by the application of a single rewriting rule.

@INPROCEEDINGS{leguernic07flic,
TITLE = {RULE 2007: The Eighth International Workshop on Rule-Based Programming},
YEAR = 2007,
BOOKTITLE = {Proceedings of the International Workshop on Rule-Based Programming},
SERIES = {Electronic Notes in Theoretical Computer Science (ENTCS)},
MONTH = JUN # { 29},
LOCATION = {Paris, France},
PUBLISHER = {Elsevier},
NOTE = {Part of RDP'07},
AUTHOR = {G. Le~Guernic and J. Perret},
TITLE = {{FLIC}: {A}pplication to {C}aching of a {D}ynamic {D}ependency {A}nalysis for a {3D} {O}riented {CRS}},
NOTE = {To appear},
ABSTRACT = {FL-systems are conditional rewriting systems. They are used for programming (describing) and evaluating (generating) huge 3D virtual environments, such as cities and forests. This paper presents a formal semantics and a dynamic dependency analysis for FL-systems. This analysis allows the characterization of a set of terms which are joinable with the currently rewritten term. Consequently, it is possible to speed up the rewriting steps of the environments generation by using a cache mechanism which is smarter than standard ones. This work can be seen as a dynamic completion of a set of rewriting rules. This completion increases the number of terms which are rewritten in normal form by the application of a single rewriting rule.} 
}

M. Petit and A. Gotlieb. Boosting Probabilistic Choice Operators. In Proceedings of Principles and Practices of Constraint Programming, Springer Verlag, LNCS 4741, Providence, USA, pages 559-573, September 2007.

Probabilistic Choice Operators (PCOs) are convenient tools to model uncertainty in CP. They are useful to implement randomized algorithms and stochastic processes in the concurrent constraint framework. Their implementation is based on the random selection of a value inside a finite domain according to a given probability distribution. Unfortunately, the probabilistic choice of a PCO is usually delayed until the probability distribution is completely known. This is inefficient and penalizes their broader adoption in real-world applications. In this paper, we associate to PCO a filtering algorithm that prunes the variation domain of its random variable during constraint propagation. Our algorithm runs in O(n) where n denotes the size of the domain of the probabilistic choice. Experimental results show the practical interest of this approach.

@InProceedings{PG07,
author = {Petit, M. and Gotlieb, A.},
title = {Boosting Probabilistic Choice Operators},
booktitle = {Proceedings of Principles and Practices of Constraint Programming},
series = {Springer Verlag, LNCS 4741},
pages = {559--573},
month = {September},
year = 2007,
address = {Providence, USA},
abstract = {Probabilistic Choice Operators (PCOs) are convenient tools to model uncertainty in CP. They are useful to implement randomized algorithms and stochastic processes in the concurrent constraint framework. Their implementation is based on the random selection of a value inside a finite domain according to a given probability distribution. Unfortunately, the probabilistic choice of a PCO is usually delayed until the probability distribution is completely known. This is inefficient and penalizes their broader adoption in real-world applications. In this paper, we associate to PCO a filtering algorithm that prunes the variation domain of its random variable during constraint propagation. Our algorithm runs in O(n) where n denotes the size of the domain of the probabilistic choice. Experimental results show the practical interest of this approach.},

}

M. Petit and A. Gotlieb. Uniform Selection of Feasible Paths as a Stochastic Constraint Problem. In Proceedings of International Conference on Quality Software (QSIC'07), IEEE, Portland, USA, October 2007.

Automatic structural test data generation is a real challenge of Software Testing. Statistical structural testing has been proposed to address this problem. This testing method aims at building an input probability distribution to maximize the coverage of some structural criteria. Under the all_paths testing objective, statistical structural testing aims at selecting each feasible path of the program with the same probability. In this paper, we propose to model a uniform selector of feasible paths as a stochastic constraint program. Stochastic constraint programming is an interesting framework which combines stochastic decision problem and constraint solving. This paper reports on the translation of uniform selection of feasible paths problem into a stochastic constraint problem. An implementation which uses the library PCC(FD) of SICStus Prolog designed for this problem is detailed. First experimentations, conducted over a few academic examples, show the interest of our approach.

@InProceedings{PG07b,
author = {Petit, M. and Gotlieb, A.},
title = {Uniform Selection of Feasible Paths as a Stochastic Constraint Problem},
booktitle = {Proceedings of International Conference on Quality Software (QSIC'07)},
series = {IEEE},
pages = {},
month = {October},
year = 2007,
address = {Portland, USA},
abstract = {Automatic structural test data generation is a real challenge of Software Testing. Statistical structural testing has been proposed to address this problem. This testing method aims at building an input probability distribution to maximize the coverage of some structural criteria. Under the all_paths testing objective, statistical structural testing aims at selecting each feasible path of the program with the same probability. 

In this paper, we propose to model a uniform selector of feasible paths as a stochastic constraint program. Stochastic constraint programming is an interesting framework which combines stochastic decision problem and constraint solving. This paper reports on the translation of uniform selection of feasible paths problem into a stochastic constraint problem. An implementation which uses the library PCC(FD) of SICStus Prolog designed for this problem is detailed. First experimentations, conducted over a few academic examples, show the interest of our approach.},

}

Internal reports

F. Besson, T. Jensen, D. Pichardie, and T. Turpin. Result certification for relational program analysis. Research Report 6333, Inria, September 2007. [WWW]

@TECHREPORT{BJPT:polycert:techreport,
AUTHOR = {F. Besson and T. Jensen and D. Pichardie and T. Turpin},
TITLE = {Result certification for relational program analysis},
INSTITUTION = {Inria},
YEAR = 2007,
NUMBER = {6333},
TYPE = {Research Report},
MONTH = SEP,
URL = {http://hal.inria.fr/inria-00166930/} 
}

Frédéric Besson, Thomas Jensen, and Tiphaine Turpin. Computing stack maps with interfaces. Technical report 1879, Irisa, 2007. [WWW]

@TechReport{BJT:Stackmaps,
author = {Frédéric Besson and Thomas Jensen and Tiphaine Turpin},
title = {Computing stack maps with interfaces},
institution = {Irisa},
year = {2007},
number = {1879},
url = {http://www.irisa.fr/centredoc/publis/PI/irisafolder.2007-01-11.2880718947/irisapublication.2007-12-21.3303136537},

}

David Cachera, Thomas Jensen, and Pascal Sotin. Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. Research Report 6338, INRIA, 10 2007. [WWW]

@TechReport{CacJenSotRR07,
author = {Cachera, David and Jensen, Thomas and Sotin, Pascal},
title = {Long-Run Cost Analysis by Approximation of Linear Operators over Dioids},
year = {2007},
month = {10},
institution = {INRIA},
number = {6338},
type = {Research Report},
url= {https://hal.inria.fr/inria-00182338} 
}

G. Le Guernic. Automaton-based Non-interference Monitoring of Concurrent Programs. Technical report 2007-1, Kansas State University, 234 Nichols Hall, Manhattan, KS 66506, USA, February 2007. [WWW]

Earlier work [LGBJS06] presents an automaton-based non-interference monitoring mechanism for sequential programs. This technical report extends this work to a concurrent setting. Monitored programs are constituted of a set of threads running in parallel. Those threads run programs equivalent to those of [LGBJS06] except for the inclusion of a synchronization command. The monitoring mechanism is still based on a security automaton and on a combination of dynamic and static analyses. As in [LGBJS06], the monitoring semantics sends abstractions of program events to the automaton, which uses the abstractions to track information flows and to control the execution by forbidding or editing dangerous actions. All monitored executions are proved to be non-interfering (soundness).

@TECHREPORT{LeGuernic2007anmocp,
AUTHOR = {G. Le~Guernic},
TITLE = {{A}utomaton-based {N}on-interference {M}onitoring of {C}oncurrent {P}rograms},
OPTINSTITUTION = {{D}epartment of {C}omputing and {I}nformation {S}ciences, {C}ollege of {E}ngineering, {K}ansas {S}tate {U}niversity},
INSTITUTION = {{K}ansas {S}tate {U}niversity},
YEAR = 2007,
NUMBER = {2007-1},
ADDRESS = {234 Nichols Hall, Manhattan, KS 66506, USA},
OPTADDRESS = {Manhattan, KS, USA},
MONTH = FEB,
URL = {http://www.cis.ksu.edu/~schmidt/techreport/2007.list.html},
ABSTRACT = {Earlier work [LGBJS06] presents an automaton-based non-interference monitoring mechanism for sequential programs. This technical report extends this work to a concurrent setting. Monitored programs are constituted of a set of threads running in parallel. Those threads run programs equivalent to those of [LGBJS06] except for the inclusion of a synchronization command. The monitoring mechanism is still based on a security automaton and on a combination of dynamic and static analyses. As in [LGBJS06], the monitoring semantics sends abstractions of program events to the automaton, which uses the abstractions to track information flows and to control the execution by forbidding or editing dangerous actions. All monitored executions are proved to be non-interfering (soundness).} 
}

G. Le Guernic. Dynamic Noninterference Analysis Using Context Sensitive Static Analyses. Technical report 2007-5, Kansas State University, 234 Nichols Hall, Manhattan, KS 66506, USA, July 2007. [WWW] [PDF]

This report proposes a dynamic noninterference analysis for sequential programs. This analysis is well-suited for the development of a monitor enforcing the absence of information flows between the secret inputs and the public outputs of a program. This implies a sound detection of information flows and a sound correction of forbidden flows during the execution. The monitor relies on a dynamic information flow analysis. For unexecuted pieces of code, this dynamic analysis uses any context sensitive static information flow analysis which respects a given set of three hypotheses. The soundness of the overall monitoring mechanism with regard to noninterference enforcement is proved, as well as its higher precision than the automaton-based mechanism proposed in previous work.

@TECHREPORT{LeGuernic2007dnaucssa,
AUTHOR = {G. Le~Guernic},
TITLE = {{D}ynamic {N}oninterference {A}nalysis {U}sing {C}ontext {S}ensitive {S}tatic {A}nalyses},
OPTINSTITUTION = {{D}epartment of {C}omputing and {I}nformation {S}ciences, {C}ollege of {E}ngineering, {K}ansas {S}tate {U}niversity},
INSTITUTION = {{K}ansas {S}tate {U}niversity},
YEAR = 2007,
NUMBER = {2007-5},
ADDRESS = {234 Nichols Hall, Manhattan, KS 66506, USA},
MONTH = JUL,
URL = {http://www.cis.ksu.edu/~schmidt/techreport/2007.list.html},
PDF = {http://hal.inria.fr/docs/00/16/26/09/PDF/contextSensitiveNIA_report.pdf},
ABSTRACT = {This report proposes a dynamic noninterference analysis for sequential programs. This analysis is well-suited for the development of a monitor enforcing the absence of information flows between the secret inputs and the public outputs of a program. This implies a sound detection of information flows and a sound correction of forbidden flows during the execution. The monitor relies on a dynamic information flow analysis. For unexecuted pieces of code, this dynamic analysis uses any context sensitive static information flow analysis which respects a given set of three hypotheses. The soundness of the overall monitoring mechanism with regard to noninterference enforcement is proved, as well as its higher precision than the automaton-based mechanism proposed in previous work.} 
}

BACK TO INDEX

This document was translated from BibT_EX by bibtex2html

Publications

Menu

Publications of year 2007

Thesis

Articles in journal or book chapters

Conference articles

Internal reports