%
%
%
% automatically generated
% % bib2html lande.bib -force -html-links -sort-criterium year
% Date: Fri Dec 21 15:16:27 2007
% Author: pichardie
%
%
%
@PHDTHESIS{hongtuanha:phd:07,
AUTHOR = {Hong Tuan Ha, S.},
SCHOOL = {Université Rennes 1},
TITLE = {Programmation par aspects et tissage de propriétés -
Application à l'ordonnancement et à la disponibilité.},
YEAR = {2007},
OPTADDRESS = {},
MONTH = {January},
OPTNOTE = {},
OPTTYPE = {}
}
@PHDTHESIS{Guernic:phd:07,
AUTHOR = {Le Guernic, G.},
SCHOOL = {Université Rennes 1 and Kansas State University},
TITLE = {Confidentiality Enforcement Using Dynamic Information
Flow Analyses},
YEAR = {2007},
OPTADDRESS = {},
MONTH = {September},
OPTNOTE = {},
OPTTYPE = {}
}
@INCOLLECTION{wscp/part7,
AUTHOR = {Benjamin Blanc and Arnaud Gotlieb and Claude Michel},
BOOKTITLE = {Trends in Constraint Programming},
PUBLISHER = {ISTE},
TITLE = {Constraints in Software Testing, Verification and
Analysis},
YEAR = {2007},
ADDRESS = {London, UK},
CHAPTER = {7},
OPTCROSSREF = {},
OPTEDITION = {},
EDITOR = {Frédéric Benhamou and Narendra Jussien and
Barry O'Sullivan},
MONTH = {May},
OPTNOTE = {},
OPTNUMBER = {},
PAGES = {333--368},
OPTSERIES = {},
TYPE = {Part},
OPTVOLUME = {}
}
@ARTICLE{GDB07,
AUTHOR = {A. Gotlieb and T. Denmat and B. Botella},
JOURNAL = {Information and Software Technology},
TITLE = {Goal-oriented test data generation for pointer programs},
YEAR = {2007},
MONTH = {Sep.},
OPTNOTE = {},
NUMBER = {9-10},
PAGES = {1030-1044},
VOLUME = {49},
ADDRESS = {Elsevier}
}
@INPROCEEDINGS{albert07:_verif_java_bytec_trans_analy,
AUTHOR = {Elvira Albert and Miguel Gómez-Zamalloa and
Laurent Hubert and Germán Puebla},
BOOKTITLE = {PADL},
TITLE = {Verification of Java Bytecode Using Analysis and
Transformation of Logic Programs},
YEAR = {2007},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {124-139},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {},
PDF = {http://www.trebuh.net/publi/padl07.pdf}
}
@INPROCEEDINGS{BPR07,
AUTHOR = {Gilles Barthe and David Pichardie and Tamara Rezk},
BOOKTITLE = {Proc. of 16th European Symposium on Programming (ESOP'07)},
TITLE = {A Certified Lightweight Non-Interference Java Bytecode
Verifier},
YEAR = {2007},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {125-140},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4421}
}
@INPROCEEDINGS{BJT07,
AUTHOR = {Frédéric Besson and Thomas Jensen and Tiphaine Turpin},
BOOKTITLE = {Proc. of 16th European Symposium on Programming},
TITLE = {Small Witnesses for Abstract Interpretation-Based proofs},
YEAR = {2007},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {268--283},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4421}
}
@INPROCEEDINGS{BoichutGGH-SAR07,
AUTHOR = {Y. Boichut and T. Genet and Y. Glouche and O. Heen},
BOOKTITLE = {Joint conference SAR-SSI},
TITLE = {Using Animation to Improve Formal Specifications of
Security Protocols},
YEAR = {2007},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{BoichutGJL-RTA07,
AUTHOR = {Y. Boichut and T. Genet and T. Jensen and L. Leroux},
BOOKTITLE = {RTA},
TITLE = {Rewriting Approximations for Fast Prototyping of Static
Analyzers},
YEAR = {2007},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {48-62},
PUBLISHER = {Springer Verlag},
SERIES = {LNCS},
VOLUME = {4533}
}
@INPROCEEDINGS{CBG07,
AUTHOR = {F. Charreteur and B. Botella and A. Gotlieb},
BOOKTITLE = {TAIC-PART (Testing: Academic and Industrial Conference)},
TITLE = {Modelling dynamic memory management in Constraint-Based
Testing},
YEAR = {2007},
ADDRESS = {Windsor, UK},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {Sep.},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{DGD07a,
AUTHOR = {T. Denmat and A. Gotlieb and M. Ducasse},
BOOKTITLE = {Proceedings of Principles and Practices of Constraint Programming (CP'07)},
TITLE = {An Abstract Interpretation Based Combinator for Modeling
While Loops in Constraint Programming},
YEAR = {2007},
ADDRESS = {Providence, USA},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {Sep.},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {241--255},
OPTPUBLISHER = {},
SERIES = {Springer Verlag, LNCS 4741},
OPTVOLUME = {}
}
@INPROCEEDINGS{DGD07b,
AUTHOR = {T. Denmat and A. Gotlieb and M. Ducasse},
BOOKTITLE = {18th IEEE International Symposium on Software Reliability Engineering (ISSRE' 2007)},
TITLE = {Improving Constraint-Based Testing with Dynamic Linear
Relaxations},
YEAR = {2007},
ADDRESS = {Trollhättan, Sweden},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {Nov.},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{LeGuernic2007acmocp,
AUTHOR = {G. Le Guernic},
BOOKTITLE = {Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSFS20)},
TITLE = {Automaton-based Confidentiality Monitoring of Concurrent
Programs},
YEAR = {2007},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {JUL 6--8},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {IEEE Computer Society},
OPTSERIES = {},
OPTVOLUME = {},
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).}
}
@INPROCEEDINGS{leguernic07ift,
AUTHOR = {G. Le Guernic},
BOOKTITLE = {Proceedings of the Annual Asian Computing Science Conference},
TITLE = {Information Flow Testing},
YEAR = {2007},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {DEC 9--11},
NOTE = {To appear},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
SERIES = {Lecture Notes in Computer Science},
OPTVOLUME = {},
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.}
}
@INPROCEEDINGS{leguernic07flic,
AUTHOR = {G. Le Guernic and J. Perret},
BOOKTITLE = {Proceedings of the International Workshop on Rule-Based Programming},
TITLE = {FLIC: Application to Caching of a Dynamic Dependency
Analysis for a 3D Oriented CRS},
YEAR = {2007},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {JUN 29},
NOTE = {To appear},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {Elsevier},
SERIES = {Electronic Notes in Theoretical Computer Science (ENTCS)},
OPTVOLUME = {},
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.}
}
@INPROCEEDINGS{PG07,
AUTHOR = {M. Petit and A. Gotlieb},
BOOKTITLE = {Proceedings of Principles and Practices of Constraint Programming},
TITLE = {Boosting Probabilistic Choice Operators},
YEAR = {2007},
ADDRESS = {Providence, USA},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {September},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {559--573},
OPTPUBLISHER = {},
SERIES = {Springer Verlag, LNCS 4741},
OPTVOLUME = {},
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.}
}
@INPROCEEDINGS{PG07b,
AUTHOR = {M. Petit and A. Gotlieb},
BOOKTITLE = {Proceedings of International Conference on Quality Software (QSIC'07)},
TITLE = {Uniform Selection of Feasible Paths as a Stochastic
Constraint Problem},
YEAR = {2007},
ADDRESS = {Portland, USA},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {October},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
SERIES = {IEEE},
OPTVOLUME = {},
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.}
}
@TECHREPORT{BJPT:polycert:techreport,
AUTHOR = {F. Besson and T. Jensen and D. Pichardie and T. Turpin},
INSTITUTION = {Inria},
TITLE = {Result certification for relational program analysis},
YEAR = {2007},
OPTADDRESS = {},
MONTH = {September},
OPTNOTE = {},
NUMBER = {6333},
TYPE = {Research Report},
URL = {http://hal.inria.fr/inria-00166930/}
}
@TECHREPORT{BJT:Stackmaps,
AUTHOR = {Frédéric Besson and Thomas Jensen and Tiphaine Turpin},
INSTITUTION = {Irisa},
TITLE = {Computing stack maps with interfaces},
YEAR = {2007},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {1879},
OPTTYPE = {},
URL = {http://www.irisa.fr/centredoc/publis/PI/irisafolder.2007-01-11.2880718947/irisapublication.2007-12-21.3303136537}
}
@TECHREPORT{CacJenSotRR07,
AUTHOR = {David Cachera and Thomas Jensen and Pascal Sotin},
INSTITUTION = {INRIA},
TITLE = {Long-Run Cost Analysis by Approximation of Linear
Operators over Dioids},
YEAR = {2007},
OPTADDRESS = {},
MONTH = {10},
OPTNOTE = {},
NUMBER = {6338},
TYPE = {Research Report},
URL = {https://hal.inria.fr/inria-00182338}
}
@TECHREPORT{LeGuernic2007anmocp,
AUTHOR = {G. Le Guernic},
INSTITUTION = {Kansas State University},
TITLE = {Automaton-based Non-interference Monitoring of
Concurrent Programs},
YEAR = {2007},
ADDRESS = {234 Nichols Hall, Manhattan, KS 66506, USA},
MONTH = {February},
OPTNOTE = {},
NUMBER = {2007-1},
OPTTYPE = {},
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).}
}
@TECHREPORT{LeGuernic2007dnaucssa,
AUTHOR = {G. Le Guernic},
INSTITUTION = {Kansas State University},
TITLE = {Dynamic Noninterference Analysis Using Context Sensitive
Static Analyses},
YEAR = {2007},
ADDRESS = {234 Nichols Hall, Manhattan, KS 66506, USA},
MONTH = {July},
OPTNOTE = {},
NUMBER = {2007-5},
OPTTYPE = {},
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.}
}
@ARTICLE{TCSAppSem:BessonJensenPichardie,
AUTHOR = {Frédéric Besson and Thomas Jensen and David Pichardie},
JOURNAL = {Theoretical Computer Science},
TITLE = {Proof-Carrying Code from Certified Abstract
Interpretation to Fixpoint Compression},
YEAR = {2006},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {3},
PAGES = {273--291},
VOLUME = {364}
}
@ARTICLE{BGM05,
AUTHOR = {B. Botella and A. Gotlieb and C. Michel},
JOURNAL = {The Software Testing, Verification and Reliability journal},
TITLE = {Symbolic execution of floating-point computations},
YEAR = {2006},
OPTMONTH = {},
NOTE = {to appear},
OPTNUMBER = {},
OPTPAGES = {},
OPTVOLUME = {},
KEYWORDS = {Symbolic execution, Floating-point computations,
Automatic test data generation, Constraint solving},
ABSTRACT = {Symbolic execution is a classical program testing
technique which evaluates a selected control flow path with symbolic
input data. A constraint solver can be used to enforce the
satisfiability of the extracted path conditions as well as to derive
test data. Whenever path conditions contain floating-point
computations, a common strategy consists of using a constraint solver
over the rationals or the reals. Unfortunately, even in a fully
IEEE-754 compliant environment, this leads not only to approximations
but also can compromise correctness: a path can be labelled as
infeasible although there exists floating-point input data that
satisfy it. In this paper, we address the peculiarities of the
symbolic execution of program with floating-point numbers. Issues in
the symbolic execution of this kind of programs are carefully
examined and a constraint solver is described that supports
constraints over floating-point numbers. Preliminary experimental
results demonstrate the value of our approach}
}
@INPROCEEDINGS{BartheFPR06,
AUTHOR = {Gilles Barthe and Julien Forest and David Pichardie and
Vlad Rusu},
BOOKTITLE = {Proc of 8th International Symposium on Functional and Logic Programming (FLOPS'06)},
TITLE = {Defining and Reasoning About Recursive Functions: A
Practical Tool for the Coq Proof Assistant.},
YEAR = {2006},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {114-129},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {3945}
}
@INPROCEEDINGS{Besson:types06,
AUTHOR = {F. Besson},
BOOKTITLE = {Types for Proofs and Programs (TYPES'06)},
TITLE = {Fast Reflexive Arithmetic Tactics: the linear case and
beyond},
YEAR = {2006},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {48-62},
PUBLISHER = {Springer},
SERIES = {LNCS},
VOLUME = {4502},
PDF = {http://www.irisa.fr/lande/fbesson/Fast_Reflexive_Arithmetics_Tactics.pdf}
}
@INPROCEEDINGS{ESORICS-06-BJD,
AUTHOR = {Frédéric Besson and Guillaume Dufay and Thomas Jensen},
BOOKTITLE = {11th European Symposium On Research In Computer Security (ESORICS'06)},
TITLE = {A Formal Model of Access Control for Mobile Interactive
Devices},
YEAR = {2006},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4189},
URL = {http://www.irisa.fr/lande/fbesson/fbesson.html},
ABSTRACT = { This paper presents an access control model for
programming applications in which the access control to resources can
employ user interaction to obtain the necessary permissions. This
model is inspired by and improves on the Java MIDP security
architecture used in Java-enabled mobile telephones. We consider
access control permissions with multiplicities in order to allow to
use a permission a certain number of times. An operational semantics
of the model and a formal definition of what it means for an
application to respect the security model is given. A static analysis
which enforces the security model is defined and proved correct. A
constraint solving algorithm implementing the analysis is presented.}
}
@INPROCEEDINGS{EAAI:BessonJensenPichardie,
AUTHOR = {F. Besson and T. Jensen and D. Pichardie},
BOOKTITLE = {Proc. of 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06)},
TITLE = {A PCC Architecture based on Certified Abstract
Interpretation},
YEAR = {2006},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {Springer-Verlag},
SERIES = {ENTCS},
OPTVOLUME = {},
URL = {http://www.irisa.fr/lande/fbesson/fbesson.html},
ABSTRACT = { Proof-Carrying Code (PCC) is a technique for
downloading mobile code on a host machine while ensuring that the
code adheres to the host's security policy. We show how certified
abstract interpretation can be used to build a PCC architecture where
the code producer can produce program certificates automatically.
Code consumers use proof checkers derived from certified analysers to
check certificates. Proof checkers carry their own correctness proofs
and accepting a new proof checker amounts to type checking the
checker in Coq. Fixpoint compression techniques are used to obtain
compact certificates. The PCC architecture has been evaluated
experimentally on a byte code language for which we have designed an
interval analysis that allows to generate certificates ascertaining
that no array-out-of-bounds accesses will occur.}
}
@INPROCEEDINGS{BBG06,
AUTHOR = {B. Blanc and F. Bouquet and A. Gotlieb and B. Jeannet and
T. Jéron and B. Legeard and B. Marre and C. Michel and M. Rueher},
BOOKTITLE = {Proceedings of Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA'06)},
TITLE = {The V3F project},
YEAR = {2006},
ADDRESS = {Nantes, France},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {Sep.},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{BoichutG-RTA06,
AUTHOR = {Y. Boichut and T. Genet},
BOOKTITLE = {RTA},
TITLE = {Feasible Trace Reconstruction for Rewriting
Approximations.},
YEAR = {2006},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {123-135},
PUBLISHER = {Springer},
SERIES = {LNCS},
VOLUME = {4098}
}
@INPROCEEDINGS{leguernic06jmbrowser,
AUTHOR = {N. Bonnel and G. Le Guernic},
BOOKTITLE = {Proceedings of Majecstic 2006},
TITLE = {Système de recherche de méthodes Java basé sur leur
signature},
YEAR = {2006},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {November},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {},
PDF = {http://hal.inria.fr/docs/00/11/32/31/PDF/Bonnel_MajecSTIC06_web.pdf},
ABSTRACT = {L'objectif de cet article est de proposer une démarche
permettant de mettre en place un moteur de recherche de méthodes au
sein d'un langage de programmation. Un tel outil s'avère
particulièrement utile aux développeurs. Des solutions ont déjà été
proposées mais elles sont pour la plupart basées sur une recherche
textuelle, c'est-à-dire uniquement basées sur le contenu textuel de
la description des différentes méthodes. Nous proposons dans cet
article une nouvelle approche basée sur la signature des méthodes. Le
langage utilisé tout au long de cet article est le langage Java.}
}
@INPROCEEDINGS{Animator,
AUTHOR = {Y. Glouche and T. Genet and O. Heen and O. Courtay},
BOOKTITLE = {ARTIST-2 workshop on security of embedded systems, Pisa (Italy)},
TITLE = {A Security Protocol Animator Tool for AVISPA},
YEAR = {2006},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {},
URL = {http://www.irisa.fr/lande/genet/publications.html}
}
@INPROCEEDINGS{GB06,
AUTHOR = {A. Gotlieb and P. Bernard},
BOOKTITLE = {Sixth International Conference on Quality Software (QSIC'06)},
TITLE = {A Semi-empirical Model of Test Quality in Symmetric
Testing: Application to Testing Java Card APIs},
YEAR = {2006},
ADDRESS = {Beijing, China},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {Oct.},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{GBW06,
AUTHOR = {A. Gotlieb and B. Botella and M. Watel},
BOOKTITLE = {19th International Conference on Software & Systems Engineering and their Applications (ICSSEA'06)},
TITLE = {Inka: Ten years after the first ideas},
YEAR = {2006},
ADDRESS = {Paris, France},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {Dec.},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{GP06,
AUTHOR = {A. Gotlieb and M. Petit},
BOOKTITLE = {Proceedings of the 1st ACM Int. Workshop on Random Testing (RT'06)},
TITLE = {Path-oriented Random Testing},
YEAR = {2006},
ADDRESS = {Portland, Maine},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {July},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{GP06,
AUTHOR = {A. Gotlieb and M. Petit},
BOOKTITLE = {Proceedings of the International Workshop on Random Testing},
TITLE = {Path-oriented random testing.},
YEAR = {2006},
ADDRESS = {Portland, USA},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {July},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {28--35},
PUBLISHER = {ACM},
OPTSERIES = {},
OPTVOLUME = {},
ABSTRACT = {Test campaigns usually require only a restricted subset
of paths in a program to be thoroughly tested. As random testing (RT)
offers interesting fault-detection capacities at low cost, we face
the problem of building a sequence of random test data that execute
only a subset of paths in a program. We address this problem with an
original technique based on backward symbolic execution and
constraint propagation to generate random test data based on an
uniform distribution. Our approach derives path conditions and
computes an over-approximation of thier associated subdomain to find
such a uniform sequence. The challenging problem consists in building
efficiently a path-oriented random test data generator by minimizing
the number of rejets within the generated random sequence. Our first
experimental resluts, conducted over a few academic expaples, clearly
show a dramatic improvement of our approach over classical random
testing.}
}
@INPROCEEDINGS{GG06,
AUTHOR = {S. Gouraud and A. Gotlieb},
BOOKTITLE = {Eighth International Symposium on Practical Aspects of Declarative Languages, PADL 06},
TITLE = {Using CHRs to generate test cases for the JCVM},
YEAR = {2006},
ADDRESS = {Charleston, South Carolina},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {January},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {3819},
KEYWORDS = {CHR, Software testing, Java Card Virtual Machine},
ABSTRACT = {Automated functional testing consists in deriving test
cases from the specification model of a program to detect faults
within an implementation. In our work, we investigate using
Constraint Handling Rules (CHRs) to automate the test cases
generation process of functional testing. Our case study is a formal
model of the Java Card Virtual Machine (JCVM) written in a
sub-language of the Coq proof assistant. In this paper we define an
automated translation from this formal model into CHRs and propose to
generate test cases for each bytecode definition of the JCVM. The
originality of our approach resides in the use of CHRs to faithfully
model the formally specified operational semantics of the JCVM. The
approach has been implemented in Eclipse Prolog and a full set of
test cases have been generated for testing the JCVM.}
}
@INPROCEEDINGS{LeGuernic2006acm,
AUTHOR = {G. Le Guernic and A. Banerjee and T. Jensen and
D. Schmidt},
BOOKTITLE = {Proceedings of the Annual Asian Computing Science Conference},
TITLE = {Automata-based Confidentiality Monitoring},
YEAR = {2006},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {DEC 6--8},
NOTE = {To appear},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4435},
PDF = {http://hal.inria.fr/docs/00/13/02/10/PDF/automatonBasedNiMonitoring.pdf},
ABSTRACT = {Non-interference is typically used as a baseline
security policy to formalize confidentiality of secret information
manipulated by a program. In contrast to static checking of
non-interference, this paper considers dynamic, automaton-based,
monitoring of information flow for a single execution of a sequential
program. The 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. The mechanism proposed is proved to be
sound, to preserve executions of well-typed programs (in the security
type system of Volpano, Smith and Irvine), and to preserve some safe
executions of ill-typed programs. }
}
@INPROCEEDINGS{GBJS06,
AUTHOR = {Le Guernic, Gurvan and Anindya Banerjee and Thomas Jensen and
David Schmidt},
BOOKTITLE = {11th Annual Asian Computing Science Conference (ASIAN'06)},
TITLE = {Automaton-based Confidentiality Monitoring},
YEAR = {2006},
ADDRESS = {Tokyo, Japan},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {December},
NOTE = {to appear},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4435}
}
@INPROCEEDINGS{PG06,
AUTHOR = {M. Petit and A. Gotlieb},
BOOKTITLE = {Deuxièmes Journées Francophones de Programmation par Contraintes},
TITLE = {Raisonner et filtrer avec un choix probabiliste
partiellement connu},
YEAR = {2006},
ADDRESS = {Nîmes, France},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {Juin},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{SCJ06,
AUTHOR = {Pascal Sotin and David Cachera and Thomas Jensen},
BOOKTITLE = {4th International Workshop on Quantitative Aspects of Programming Languages (QAPL 2006)},
TITLE = {Quantitative Static Analysis over semirings: analysing
cache behaviour for Java Card},
YEAR = {2006},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {153-167},
PUBLISHER = {Elsevier},
SERIES = {Electronic Notes in Theoretical Computer Science},
VOLUME = {164}
}
@TECHREPORT{LeGuernic2006abnim,
AUTHOR = {G. Le Guernic and A. Banerjee and D. Schmidt},
INSTITUTION = {Department of Computing and Information Sciences, College of Engineering, Kansas State University},
TITLE = {Automaton-based Non-interference Monitoring},
YEAR = {2006},
ADDRESS = {234 Nichols Hall, Manhattan, KS 66506, USA},
MONTH = {April},
OPTNOTE = {},
NUMBER = {2006-1},
OPTTYPE = {},
URL = {http://www.cis.ksu.edu/~schmidt/techreport/2006.list.html},
ABSTRACT = {This report presents a non-interference monitoring
mechanism for sequential programs. Non-interference is a property of
the information flows of a program. It implies the respect of the
confidentiality of the secret information manipulated. The approach
taken uses an automaton based monitor. During the execution,
abstractions of the events occurring are sent to the automaton. The
automaton uses those inputs to track the information flows and to
control the execution by forbidding or editing dangerous actions. The
mechanism proposed is proved to be sound and more efficient than a
type system similar to the historical one developed by Volpano, Smith
and Irvine. }
}
@TECHREPORT{LeGuernic2006abnim,
AUTHOR = {G. Le Guernic and A. Banerjee and D. Schmidt},
INSTITUTION = {Department of Computing and Information Sciences, College of Engineering, Kansas State University},
TITLE = {Automaton-based Non-interference Monitoring},
YEAR = {2006},
ADDRESS = {234 Nichols Hall, Manhattan, KS 66506, USA},
MONTH = {April},
OPTNOTE = {},
NUMBER = {2006-1},
OPTTYPE = {},
ABSTRACT = {This report presents a non-interference monitoring
mechanism for sequential programs. Non-interference is a property of
the information flows of a program. It implies the respect of the
confidentiality of the secret information manipulated. The approach
taken uses an automaton based monitor. During the execution,
abstractions of the events occurring are sent to the automaton. The
automaton uses those inputs to track the information flows and to
control the execution by forbidding or editing dangerous actions. The
mechanism proposed is proved to be sound and more efficient than a
type system similar to the historical one developed by Volpano, Smith
and Irvine.}
}
@MANUAL{span-manual,
TITLE = {SPAN -- A Security Protocol ANimator for AVISPA -- User
Manual},
OPTADDRESS = {},
AUTHOR = {Y. Glouche and T. Genet},
OPTEDITION = {},
OPTMONTH = {},
OPTNOTE = {},
ORGANIZATION = {IRISA / Université de Rennes 1},
YEAR = {2006},
URL = {http://www.irisa.fr/lande/genet/span/}
}
@PHDTHESIS{PicThe05,
AUTHOR = {David Pichardie},
SCHOOL = {Université Rennes 1},
TITLE = {Interprétation abstraite en logique intuitionniste :
extraction d'analyseurs Java certiés},
YEAR = {2005},
ADDRESS = {Rennes, France},
MONTH = {December},
OPTNOTE = {},
OPTTYPE = {}
}
@ARTICLE{Besson:05:Interfaces,
AUTHOR = {F. Besson and de Grenier de Latour, T. and T. Jensen},
JOURNAL = {Journal of Functional Programming},
TITLE = {Interfaces for stack inspection},
YEAR = {2005},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
PAGES = {179--217},
VOLUME = {15(2)},
URL = {http://www.irisa.fr/lande/fbesson/fbesson.html},
ABSTRACT = {Stack inspection is a mechanism for programming secure
applications in the presence of code from various protection domains.
Run-time checks of the call stack allow a method to obtain
information about the code that (directly or indirectly) invoked it
in order to make access control decisions. This mechanism is part of
the security architecture of Java and the .NET Common Language
Runtime. A central problem with stack inspection is to determine to
what extent the local checks inserted into the code are sufficient to
guarantee that a global security property is enforced. A further
problem is how such verification can be carried out in an incremental
fashion. Incremental analysis is important for avoiding re-analysis
of library code every time it is used, and permits the library
developer to reason about the code without knowing its context of
deployment. We propose a technique for inferring interfaces for
stack-inspecting libraries in the form of secure calling context for
methods. By a secure calling context we mean a pre-condition on the
call stack sufficient for guaranteeing that execution of the method
will not violate a given global property. The technique is a
constraint-based static program analysis implemented via fixed point
iteration over an abstract domain of linear temporal logic
properties.}
}
@ARTICLE{CaJePiRu05TCSExtractAnalyser,
AUTHOR = {David Cachera and Thomas Jensen and David Pichardie and
Vlad Rusu},
JOURNAL = {Theoretical Computer Science},
TITLE = {Extracting a Data Flow Analyser in Constructive Logic},
YEAR = {2005},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTVOLUME = {},
ABSTRACT = {We show how to formalise a constraint-based data flow
analysis in the specification language of the Coq proof assistant.
This involves defining a dependent type of lattices together with a
library of lattice functors for modular construction of complex
abstract domains. Constraints are expressed in an intermediate
representation that allows for both efficient constraint resolution
and correctness proof of the analysis with respect to an operational
semantics. The proof of existence of a correct, minimal solution to
the constraints is constructive which means that the extraction
mechanism of Coq provides a provably correct data flow analyser in
Ocaml. The library of lattices together with the intermediate
representation of constraints are defined in an analysis-independent
fashion that provides a basis for a generic framework for proving and
extracting static analysers in Coq.}
}
@ARTICLE{CacMorTECS05,
AUTHOR = {David Cachera and Katell Morin-Allory},
JOURNAL = {Trans. on Embedded Computing Systems},
TITLE = {Verification of safety properties for parameterized
regular systems},
YEAR = {2005},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {2},
PAGES = {228--266},
VOLUME = {4},
ADDRESS = {New York, NY, USA},
PUBLISHER = {ACM Press},
ABSTRACT = {We propose a combination of heuristic methods to prove
properties of control signals for regular systems defined by means of
affine recurrence equations (AREs). We benefit from the intrinsic
regularity of the underlying polyhedral model to handle parameterized
systems in a symbolic way. Our techniques apply to safety properties.
The general proof process consists in an iteration that alternates
two heuristics. We are able to identify the cases when this iteration
will stop in a finite number of steps. These techniques have been
implemented in a high level synthesis environment based on the
polyhedral model.}
}
@INPROCEEDINGS{CaJePiSc05MemoryUsage,
AUTHOR = {David Cachera and Thomas Jensen and David Pichardie and
Gerardo Schneider},
BOOKTITLE = {Proc of 13th International Symposium on Formal Methods (FM'05)},
TITLE = {Certified Memory Usage Analysis},
YEAR = {2005},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
OPTVOLUME = {},
ABSTRACT = {We present a certified algorithm for resource usage
analysis, applicable to languages in the style of Java byte code. The
algorithm verifies that a program executes in bounded memory. The
algorithm is destined to be used in the development process of
applets and for enhanced byte code verification on embedded devices.
We have therefore aimed at a low-complexity algorithm derived from a
loop detection algorithm for control flow graphs. The expression of
the algorithm as a constraint-based static analysis of the program
over simple lattices provides a link with abstract interpretation
that allows to state and prove formally the correctness of the
analysis with respect to an operational semantics of the program. The
certification is based on an abstract interpretation framework
implemented in the Coq proof assistant which has been used to provide
a complete formalisation and formal verification of all correctness
proofs.}
}
@INPROCEEDINGS{Sotin05,
AUTHOR = {David Cachera and Thomas Jensen and Pascal Sotin},
BOOKTITLE = {Proc. of IST-APPSEM II Workshop on Applied Semantics},
TITLE = {Estimating Cache Misses with Semi-Modules and
Quantitative Abstraction},
YEAR = {2005},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{denmat05b,
AUTHOR = {T. Denmat and M. Ducassé and O. Ridoux},
BOOKTITLE = {Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering},
TITLE = {Data mining and cross-checking of execution traces. A
re-interpretation of Jones, Harrold and Stasko test information
visualization},
YEAR = {2005},
OPTADDRESS = {},
OPTCROSSREF = {},
EDITOR = {T. Ellman and A. Zisman},
MONTH = {November},
NOTE = {See RR-5661 for a long version of this article},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {ACM Press},
OPTSERIES = {},
OPTVOLUME = {},
KEYWORDS = {Software Engineering, Debugging,
Artificial Intelligence, Learning, Knowledge acquisition},
ABSTRACT = {The current trend in debugging and testing is to
cross-check information collected during several executions. Jones et
al., for example, propose to use the instruction coverage of passing
and failing runs in order to visualize suspicious statements. This
seems promising but lacks a formal justification. In this paper, we
show that the method of Jones et al. can be re-interpreted as a data
mining procedure. More particularly, they define an indicator which
characterizes association rules between data. With this formal
framework we are able to explain intrinsic limitations of the above
indicator.}
}
@INPROCEEDINGS{DGD05,
AUTHOR = {T. Denmat and A. Gotlieb and M. Ducassé},
BOOKTITLE = {Proceedings of the 15th Workshop on Logic-based Method for Programming Environments},
TITLE = {Proving or Disproving Likely Invariants with Constraint
Reasoning},
YEAR = {2005},
ADDRESS = {Sitges, SPAIN},
OPTCROSSREF = {},
EDITOR = {A. Serebrenik},
MONTH = {October},
NOTE = {Satelite event of International Conference on Logic Programming (ICLP'2005). Published in Computer Research Repository cs.SE/0508108},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {},
KEYWORDS = {Software Engineering, Testing and Debugging,
Program verification, Constraint and logic languages},
URL = {http://arxiv.org/abs/cs.pl/0508108},
ABSTRACT = {A program invariant is a property that holds for every
execution of the program. Recent work suggest to infer likely-only
invariants, via dynamic analysis. A likely invariant is a property
that holds for some executions but is not guaranteed to hold for all
executions. In this paper, we present work in progress addressing the
challenging problem of automatically verifying that likely invariants
are actual invariants. We propose a constraint-based reasoning
approach that is able, unlike other approaches, to both prove or
disprove likely invariants. In the latter case, our approach provides
counter-examples. We illustrate the approach on a motivating example
where automatically generated likely invariants are verified. }
}
@INPROCEEDINGS{GDB05b,
AUTHOR = {A. Gotlieb and T. Denmat and B. Botella},
BOOKTITLE = {20th IEEE/ACM International Conference on Automated Software Engineering (ASE'05)},
TITLE = {Constraint-based test data generation in the presence of
stack-directed pointers},
YEAR = {2005},
ADDRESS = {Long Beach, CA, USA},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {Nov.},
NOTE = {4 pages, short paper},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {},
KEYWORDS = {Constraint-Based Test data generation,
Constraint satisfaction, stack-directed pointers},
ABSTRACT = {Constraint-Based Test data generation (CBT) exploits
constraint satisfaction techniques to generate test data able to kill
a given mutant or to reach a selected branch in a program. When
pointer variables are present in the program, aliasing problems may
arise and may lead to the failure of current CBT approaches. In our
work, we propose an overall CBT method that exploits the results of
an intraprocedural points-to analysis and provides two specific
constraint combinators for automatically generating test data able to
reach a selected branch. Our approach correctly handles multi-levels
stack-directed pointers that are mainly used in real-time control
systems. The method has been fully implemented in the test data
generation tool INKA and first experiences in applying it to a
variety of existing programs tend to show the interest of the
approach.}
}
@INPROCEEDINGS{GDB05a,
AUTHOR = {A. Gotlieb and T. Denmat and B. Botella},
BOOKTITLE = {29th IEEE Annual International Computer Software and Applications Conference (COMPSAC'05)},
TITLE = {Goal-oriented test data generation for programs with
pointer variables},
YEAR = {2005},
ADDRESS = {Edinburh, Scotland},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {July},
NOTE = {6 pages},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {449-454},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {},
KEYWORDS = {Goal-oriented test data generation,
Constraint Logic Programming, Static Single Assignment form,
pointer variables},
ABSTRACT = {Automatic test data generation leads to the
identification of input values on which a selected path or a selected
branch is executed within a program (path-oriented vs goal-oriented
methods). In both cases, several approaches based on constraint
solving exist, but in the presence of pointer variables only
path-oriented methods have been proposed. This paper proposes to
extend an existing goal-oriented test data generation technique to
deal with multi-level pointer variables. The approach exploits the
results of an intraprocedural flow-sensitive points-to analysis to
automatically generate goal-oriented test data at the unit testing
level. Implementation is in progress and a few examples are
presented.}
}
@INPROCEEDINGS{GG05,
AUTHOR = {S.D. Gouraud and A. Gotlieb},
BOOKTITLE = {Premières Journées Francophones de Programmation par Contraintes (JFPC'05)},
TITLE = {Utilisation des CHRs pour générer des cas de test
fonctionnel pour la Machine Virtuelle Java Card},
YEAR = {2005},
ADDRESS = {Lens, FRANCE},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {8-10 juin},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {},
ABSTRACT = {Le test fonctionnel basé sur une spécification formelle
consiste à dériver des cas de test à partir d'un modèle formel pour
détecter des fautes dans son implémentation. Dans nos travaux, nous
étudions l'utilisation des \emph{Constraint Handling Rules} (CHRs)
pour automatiser la génération de cas de test fonctionnel basée sur
un modèle formel. Notre étude de cas est un modèle de la
spécification de la Machine Virtuelle Java Card (JCVM) écrite dans un
sous ensemble du langage Coq. Dans cet article, nous définissons une
traduction automatique de ce modèle sous forme de règles CHR dans le
but de générer des cas de test pour la JCVM. Le point clé de notre
approche réside dans l'utilisation des \emph{deep guards} pour
modéliser fidèlement la sémantique de notre modèle formel de la JCVM.
Ensuite, nous proposons une approche globale pour la génération de
cas de test fonctionnel basée sur les CHRs qui peut \^etre appliquée
à d'autres modèles formels.}
}
@INPROCEEDINGS{LeGuernic2005mif,
AUTHOR = {G. Le Guernic and T. Jensen},
BOOKTITLE = {Proceedings of the 2005 Workshop on Foundations of Computer Security (FCS'05)},
TITLE = {Monitoring Information Flow},
YEAR = {2005},
OPTADDRESS = {},
OPTCROSSREF = {},
EDITOR = {Andrei Sabelfeld},
MONTH = {June},
NOTE = {LICS'05 Affiliated Workshop},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {19--30},
PUBLISHER = {DePaul University},
OPTSERIES = {},
OPTVOLUME = {},
ABSTRACT = {We present an information flow monitoring mechanism for
sequential programs. The monitor executes a program on standard data
that are tagged with labels indicating their security level. We
formalize the monitoring mechanism as a big-step operational
semantics that integrates a static information flow analysis to
gather information flow properties of non-executed branches of the
program. Using the information flow monitoring mechanism, it is then
possible to partition the set of all executions in two sets. The
first one contains executions which are safe and the other one
contains executions which may be unsafe. Based on this information,
we show that, by resetting the value of some output variables, it is
possible to alter the behavior of executions belonging to the second
set in order to ensure the confidentiality of secret data. }
}
@INPROCEEDINGS{LeGuernic2005mif,
AUTHOR = {G. Le Guernic and T. Jensen},
BOOKTITLE = {Proceedings of the Workshop on Foundations of Computer Security},
TITLE = {Monitoring Information Flow},
YEAR = {2005},
OPTADDRESS = {},
OPTCROSSREF = {},
EDITOR = {Andrei Sabelfeld},
MONTH = {June},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {19--30},
PUBLISHER = {DePaul University},
OPTSERIES = {},
OPTVOLUME = {},
PDF = {http://hal.inria.fr/docs/00/06/50/99/PDF/le-guernic05monitoringInformationFlow.pdf},
ABSTRACT = {We present an information flow monitoring mechanism for
sequential programs. The monitor executes a program on standard data
that are tagged with labels indicating their security level. We
formalize the monitoring mechanism as a big-step operational
semantics that integrates a static information flow analysis to
gather information flow properties of non-executed branches of the
program. Using the information flow monitoring mechanism, it is then
possible to partition the set of all executions in two sets. The
first one contains executions which \emph{are safe} and the other one
contains executions which may be unsafe. Based on this information,
we show that, by resetting the value of some output variables, it is
possible to alter the behavior of executions belonging to the second
set in order to ensure the confidentiality of secret data.}
}
@INPROCEEDINGS{leguernic05flic,
AUTHOR = {G. Le Guernic and J. Perret},
BOOKTITLE = {Proceedings of Majecstic 2005},
TITLE = {FL-system's Intelligent Cache},
YEAR = {2005},
OPTADDRESS = {},
OPTCROSSREF = {},
EDITOR = {Alexandre Vautier and Sylvie Saget},
MONTH = {November},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {79--88},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {},
PDF = {http://hal.inria.fr/docs/00/04/36/98/PDF/43.pdf},
ABSTRACT = {Cet article présente une application de techniques
issues du génie logiciel à la modélisation d'environnements virtuels.
Ces derniers, dès lors qu'ils sont complexes, constituent des masses
de données particulièrement volumineuses et, de ce fait, difficiles à
manipuler. De plus, les descriptions exhaustives de ces
environnements, c'est-à-dire explicites, sont peu évolutives. Pour
résoudre ces problèmes, il existe des méthodes basées sur des
systèmes de réécriture permettant de décrire de fac¸on générique les
objets de l'environnement. Chaque objet est ainsi décrit par un
axiome qui est réécrit lors de la génération de l'environnement. Lors
de cette phase, il est fréquent de retrouver deux séquences de
réécriture aboutissant à un même objet. Il est alors possible
d'utiliser un mécanisme tel que le cache afin d'améliorer les
performances en profitant des calculs déjà effectués. Cependant, se
contenter de mettre en correspondance les noms et paramètres des
axiomes n'est pas suffisant pour établir l'ensemble des réécritures
identiques. En effet, les réécritures d'un même axiome avec des
paramètres effectifs différents peuvent aboutir au même objet. Le
système proposé dans cet article effectue une analyse dynamique des
réécritures afin d'améliorer les performances du cache en d´etectant
de tels cas. La première partie de cet article présente le système de
réécriture, la seconde l'analyse utilisée, et la dernière le
mécanisme proposé.}
}
@INPROCEEDINGS{leguernic05flic,
AUTHOR = {G. Le Guernic and Julien Perret},
BOOKTITLE = {Proceedings of Majecstic 2005},
TITLE = {FL-system's Intelligent Cache},
YEAR = {2005},
OPTADDRESS = {},
OPTCROSSREF = {},
EDITOR = {Alexandre Vautier and Sylvie Saget},
MONTH = {November},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {79--88},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{MorCacCHARME05,
AUTHOR = {Katell Morin-Allory and David Cachera},
BOOKTITLE = {Proc. of 13th CHARME conference},
TITLE = {Proving Parameterized Systems: The Use of
Pseudo-Pipelines in Polyhedral Logic},
YEAR = {2005},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {376--379},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
OPTVOLUME = {}
}
@INPROCEEDINGS{Pich05ParamConcr,
AUTHOR = {David Pichardie},
BOOKTITLE = {Proc. of 2nd International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS 2005)},
TITLE = {Modular proof principles for parameterized
concretizations},
YEAR = {2005},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {3956},
OPTORGANIZATION = {},
PAGES = {138--154},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
OPTVOLUME = {}
}
@TECHREPORT{RR-5751,
AUTHOR = {F. Besson and T. Jensen and D. Pichardie},
INSTITUTION = {INRIA},
TITLE = {A PCC Architecture based on Certified Abstract
Interpretation},
YEAR = {2005},
OPTADDRESS = {},
MONTH = {November},
NOTE = {Also Publication Interne IRISA PI-1764},
NUMBER = {RR-5751},
TYPE = {Research Report},
PDF = {ftp://ftp.inria.fr/INRIA/publication/publi-pdf/RR/RR-5751.pdf}
}
@TECHREPORT{CacMorRR05,
AUTHOR = {David Cachera and Katell Morin-Allory},
INSTITUTION = {TIMA-IMAG},
TITLE = {Proving Parameterized Systems: the use of a widening
operator and pseudo-pipelines in polyhedral logic},
YEAR = {2005},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {TIMA-RR--05/04-01--FR},
OPTTYPE = {},
ABSTRACT = {We propose proof techniques and tools for the formal
verification of regular parameterized systems. These systems are
expressed in the polyhedral model, which combines affine recurrence
equations with index sets of polyhedral shape. We extend a previously
defined proof system based on a polyhedral logic with the detection
of pseudo-pipelines, that are particular patterns in the variable
definitions generalizing the notion of pipeline. The combination of
pseudo-pipeline detection with the use of a simple widening operator
greatly improves the effectiveness of our proof techniques.}
}
@TECHREPORT{denmat05c,
AUTHOR = {T. Denmat and M. Ducassé and O. Ridoux},
INSTITUTION = {INRIA},
TITLE = {Data Mining and Cross-checking of Execution Traces. A
re-interpretation of Jones, Harrold and Stasko test information
visualization (Long version)},
YEAR = {2005},
OPTADDRESS = {},
MONTH = {August},
NOTE = {Also Publication Interne IRISA PI-1743},
NUMBER = {RR-5661},
TYPE = {Research Report},
URL = {http://www.inria.fr/rrrt/rr-5661.html}
}
@MISC{LeGuernic2003ras_misc,
AUTHOR = {G. Le Guernic},
OPTHOWPUBLISHED = {},
MONTH = {October},
NOTE = {Dagstuhl Seminar 03411: Language-Based Security},
TITLE = {Roles & Security},
YEAR = {2005},
ADDRESS = {Dagstuhl, Germany},
BOOKTITLE = {03411 Abstracts Collection -- Language-Based Security},
EDITOR = {Anindya Banerjee and Heiko Mantel and David A. Naumann and
Andrei Sabelfeld},
NUMBER = {03411},
PUBLISHER = {Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany},
SERIES = {Dagstuhl Seminar Proceedings},
URL = {http://drops.dagstuhl.de/opus/volltexte/2005/173 [date of citation: 2005-01-01]}
}
@PROCEEDINGS{Huisman:04:JLAPSmartCards,
TITLE = {J. Logic and Algebraic Programming. Special issue on
Formal Methods for Smart Cards, vol. 58(1-2)},
YEAR = {2004},
OPTADDRESS = {},
EDITOR = {M. Huisman and T. Jensen},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PUBLISHER = {Elsevier},
OPTSERIES = {},
OPTVOLUME = {}
}
@PHDTHESIS{Morin04,
AUTHOR = {B. Morin},
SCHOOL = {INSA de Rennes},
TITLE = {Corrélation d'alertes issues d'outils de détection
d'intrusions avec prise en compte d'informations sur le système
surveillé},
YEAR = {2004},
OPTADDRESS = {},
MONTH = {Février},
OPTNOTE = {},
OPTTYPE = {}
}
@PHDTHESIS{alloy-morin04,
AUTHOR = {Katell Morin-Allory},
SCHOOL = {Université de Rennes 1},
TITLE = {Vérification formelle dans le modèle polyédrique},
YEAR = {2004},
OPTADDRESS = {},
MONTH = {Octobre},
OPTNOTE = {},
OPTTYPE = {}
}
@ARTICLE{Eluard:04:TSI,
AUTHOR = {M. Eluard and T. Jensen},
JOURNAL = {Technique et Science Informatiques},
TITLE = {Vérification du contrôle d'accès dans des cartes à puce
multi-application},
YEAR = {2004},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {3},
PAGES = {323--358},
VOLUME = {23}
}
@ARTICLE{FeuilladeGVTT-JAR04,
AUTHOR = {G. Feuillade and T. Genet and Viet Triem Tong, V.},
JOURNAL = {Journal of Automated Reasoning},
TITLE = {Reachability Analysis over Term Rewriting Systems},
YEAR = {2004},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
PAGES = {341-383},
VOLUME = {33 (3-4)},
KEYWORDS = {Term Rewriting, Reachability, Tree Automata,
Approximations, Verification, Timbuk, Abstract Interpretation},
URL = {http://www.irisa.fr/lande/genet/publications.html},
ABSTRACT = {This paper surveys some techniques and tools for
achieving reachability analysis over term rewriting systems. The core
of those techniques is a generic tree automata completion algorithm
used to compute in an exact or approximated way the set of
descendants (or reachable terms). This algorithm has been implemented
in the Timbuk tool. Furthermore, we show that many classes with
regular sets of descendants of the literature corresponds to specific
instances of the tree automata completion algorithm and can thus be
efficiently computed by Timbuk. An extension of the completion
algorithm to conditional term rewriting systems and some applications
are also presented.}
}
@ARTICLE{Jensen:04:CartesAPuce,
AUTHOR = {T. Jensen and J.-L. Lanet},
JOURNAL = {Revue d'électricité et de l'électronique},
TITLE = {Modélisation et vérification dans les cartes à puce},
YEAR = {2004},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
PAGES = {89--94},
VOLUME = {6/7}
}
@INPROCEEDINGS{CachJen:esop04,
AUTHOR = {David Cachera and Thomas Jensen and David Pichardie and
Vlad Rusu},
BOOKTITLE = {Proc. ESOP'04},
TITLE = {Extracting a data flow analyser in constructive logic},
YEAR = {2004},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {2986},
OPTORGANIZATION = {},
PAGES = {385 -- 400},
OPTPUBLISHER = {},
SERIES = {Springer LNCS},
OPTVOLUME = {}
}
@INPROCEEDINGS{PG04,
AUTHOR = {Matthieu Petit and Arnaud Gotlieb},
BOOKTITLE = {Proc. of SIVOES-MODEVA workshop},
TITLE = {An ongoing work on statistical structural testing via
probabilistic concurrent constraint programming},
YEAR = {2004},
ADDRESS = {St Malo, France},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {November},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {IEEE},
OPTSERIES = {},
OPTVOLUME = {},
ABSTRACT = {The use of a model to describe and test the expected
behavior of a program is a well-proved software testing technique.
Statistical structural testing aims at building a model from which an
input probability distribution can be derived that maximizes the
coverage of some structural criteria by a random test data generator.
Our approach consists in converting statistical structural testing
into a Probabilistic Concurrent Constraint Programming (PCCP) problem
in order 1) to exploit the high declarativity of the probabilistic
choice operators of this paradigm and 2) to benefit from its
automated constraint solving capacity. This paper reports on an
ongoing work to implement PCCP and exploit it to solve instances of
statistical structural testing problems. Application to testing Java
Card applets is discussed.}
}
@INPROCEEDINGS{PetitGotlieb:04:poster,
AUTHOR = {Matthieu Petit and Arnaud Gotlieb},
BOOKTITLE = {Poster presentation in ICLP'04},
TITLE = {Probabilistic choice operators as global constraints :
application to statistical software testing},
YEAR = {2004},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {3132},
OPTORGANIZATION = {},
PAGES = {471 -- 472},
OPTPUBLISHER = {},
SERIES = {Springer LNCS},
OPTVOLUME = {}
}
@PHDTHESIS{VietTriemTong-PhD03,
AUTHOR = {Viet Triem Tong, V.},
SCHOOL = {Université Rennes 1},
TITLE = {Automates d'arbres et réécriture pour l'étude de
problèmes d'accessibilité},
YEAR = {2003},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
OPTTYPE = {}
}
@ARTICLE{Banerjee:03:Rank2,
AUTHOR = {A. Banerjee and T. Jensen},
JOURNAL = {Mathematical Structures in Computer Science},
TITLE = {Control-flow analysis with rank-2 intersection types},
YEAR = {2003},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {1},
PAGES = {87--124},
VOLUME = {13}
}
@ARTICLE{Spoto:ClassAnalysis:03,
AUTHOR = {F. Spoto and T. Jensen},
JOURNAL = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
TITLE = {Class Analyses as Abstract Interpretations of Trace
Semantics},
YEAR = {2003},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {5},
PAGES = {578--630},
VOLUME = {25}
}
@INPROCEEDINGS{Besson:03:Modular,
AUTHOR = {F. Besson and T. Jensen},
BOOKTITLE = {Proc. of 10th Static Analysis Symposium (SAS 2003)},
TITLE = {Modular Class Analysis with DATALOG},
YEAR = {2003},
OPTADDRESS = {},
OPTCROSSREF = {},
EDITOR = {R. Cousot},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {19--36},
PUBLISHER = {Springer LNCS vol. 2694},
OPTSERIES = {},
OPTVOLUME = {},
URL = {http://www.irisa.fr/lande/fbesson/fbesson.html},
ABSTRACT = {datalog can be used to specify a variety of class
analyses for object oriented programs as variations of a common
framework. In this framework, the result of analyzing a class is a
set of datalog clauses whose least fixpoint is the information
analysed for. Modular class analysis of program fragments is then
expressed as the resolution of open datalog programs. We provide a
theory for the partial resolution of sets of open clauses and define
a number of operators for reducing such open clauses. }
}
@INPROCEEDINGS{CacMor03,
AUTHOR = {David Cachera and Katell Morin-Allory},
BOOKTITLE = {Proc. 1st MEMOCODE conference},
TITLE = {Verification of Control Properties in the Polyhedral
Model},
YEAR = {2003},
ADDRESS = {Mont-St-Michel, France},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {June},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {},
URL = {ftp://ftp.irisa.fr/local/lande/dckmaMEMOCODE03.ps.gz}
}
@INPROCEEDINGS{CacPic03,
AUTHOR = {David Cachera and David Pichardie},
BOOKTITLE = {Proc. TPHOLs 2003, 16th International Conference on Theorem Proving in Higher Order Logics},
TITLE = {Embedding of Systems of Affine Recurrence Equations in
Coq},
YEAR = {2003},
ADDRESS = {Rome, Italy},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {September},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
SERIES = {LNCS},
OPTVOLUME = {},
URL = {ftp://ftp.irisa.fr/local/lande/dcdpTPHOL03.ps.gz}
}
@INPROCEEDINGS{FeuilladeG-FTP03,
AUTHOR = {G. Feuillade and T. Genet},
BOOKTITLE = {FTP'2003, International Workshop on First-Order Theorem Proving},
TITLE = {Reachability in conditional term rewriting systems},
YEAR = {2003},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {June},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {Elsevier},
SERIES = {Electronic Notes in Theoretical Computer Science},
VOLUME = {86 n. 1},
KEYWORDS = {Term Rewriting, Conditional Term Rewriting,
Reachability, Tree Automata},
URL = {http://www.irisa.fr/lande/genet/publications.html}
}
@INPROCEEDINGS{GenetJKP-COCV03,
AUTHOR = {T. Genet and T. Jensen and V. Kodati and D. Pichardie},
BOOKTITLE = {Proceedings of the 2nd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2003)},
TITLE = {A Java Card CAP Converter in PVS},
YEAR = {2003},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {ENTCS 82(2)},
OPTSERIES = {},
OPTVOLUME = {},
KEYWORDS = {Java, Java Card, CAP Format, Compiler, Verification,
Proof Assistant, PVS},
URL = {http://www.irisa.fr/lande/genet/publications.html}
}
@INPROCEEDINGS{GenetTTVTT-wits03,
AUTHOR = {T. Genet and Y.-M. Tang-Talpin and Viet Triem Tong, V.},
BOOKTITLE = {In Proceedings of Workshop on Issues in the Theory of Security},
TITLE = {Verification of Copy Protection Cryptographic Protocol
using Approximations of Term Rewriting Systems},
YEAR = {2003},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {},
KEYWORDS = {Cryptographic Protocol, Verification, Term Rewriting,
Reachability, Approximation, Timbuk},
URL = {http://www.irisa.fr/lande/genet/publications.html}
}
@INPROCEEDINGS{Gotlieb:03:SymTest,
AUTHOR = {Arnaud Gotlieb},
BOOKTITLE = {Proc. of 14th IEEE International Symposium on Software Reliability Engineering (ISSRE 2003)},
TITLE = {Exploiting Symmetries to Test Programs},
YEAR = {2003},
ADDRESS = {Denver, Colorado, USA},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
NOTE = {17th to 20th November},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{Gotlieb:03:MetaTest,
AUTHOR = {A. Gotlieb and B. Botella},
BOOKTITLE = {Proc. of the 27th IEEE Annual International Computer Software and Applications Conference (COMPSAC)},
TITLE = {Automated Metamorphic Testing},
YEAR = {2003},
ADDRESS = {Dallas, TX, USA},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
NOTE = {3th to 7th November},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{Aertryck:03:UMLCasting,
AUTHOR = {van Aertryck, Lionel and Thomas Jensen},
BOOKTITLE = {Proc. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'2003)},
TITLE = {UML-CASTING: Test synthesis from UML models using
constraint resolution},
YEAR = {2003},
OPTADDRESS = {},
OPTCROSSREF = {},
EDITOR = {J-M. Jézéquel},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {INRIA},
OPTSERIES = {},
OPTVOLUME = {}
}
@TECHREPORT{CacMorRR03,
AUTHOR = {David Cachera and Katell Morin-Allory},
INSTITUTION = {INRIA},
TITLE = {Verification of Control Properties in the Polyhedral
Model},
YEAR = {2003},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {1515},
OPTTYPE = {},
URL = {ftp://ftp.irisa.fr/techreports/2003/PI-1515.ps.gz}
}
@TECHREPORT{CacPicRR03,
AUTHOR = {David Cachera and David Pichardie},
INSTITUTION = {INRIA},
TITLE = {Proof Tactics for the Verification of Structured Systems
of Affine Recurrence Equations},
YEAR = {2003},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {1511},
OPTTYPE = {},
URL = {ftp://ftp.irisa.fr/techreports/2003/PI-1511.ps.gz}
}
@TECHREPORT{FeuilladeGVTT-RR03,
AUTHOR = {G. Feuillade and T. Genet and Viet Triem Tong, V.},
INSTITUTION = {INRIA},
TITLE = {Reachability Analysis over Term Rewriting Systems},
YEAR = {2003},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {RR-4970},
OPTTYPE = {},
KEYWORDS = {Term Rewriting, Reachability, Tree Automata,
Approximations, Verification, Timbuk, Abstract Interpretation},
URL = {ftp://ftp.irisa.fr/local/lande/gf-tg-vvtt-inria03.ps.gz},
ABSTRACT = {This paper surveys some techniques and tools for
achieving reachability analysis over term rewriting systems. The core
of those techniques is a generic tree automata completion algorithm
used to compute in an exact or approximated way the set of
descendants (or reachable terms). This algorithm has been implemented
in the Timbuk tool. Furthermore, we show that classes with regular
sets of descendants of the literature corresponds to specific
instances of the tree automata completion algorithm and can thus be
efficiently computed by Timbuk. An extension of the completion
algorithm to conditional term rewriting systems and some applications
are also presented.}
}
@MANUAL{Timbuk-manual,
TITLE = {Timbuk 2.0 -- A Tree Automata Library -- Reference
Manual and Tutorial},
OPTADDRESS = {},
AUTHOR = {T. Genet},
OPTEDITION = {},
OPTMONTH = {},
NOTE = {81 pages},
OPTORGANIZATION = {},
YEAR = {2003},
HOWPUBLISHED = {IRISA / Université de Rennes 1},
URL = {http://www.irisa.fr/lande/genet/timbuk/}
}
@PHDTHESIS{Besson:02:PhD,
AUTHOR = {F. Besson},
SCHOOL = {Université de Rennes 1},
TITLE = {Analyse modulaire de programmes},
YEAR = {2002},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
OPTTYPE = {},
URL = {http://www.irisa.fr/lande/fbesson/fbesson.html}
}
@PHDTHESIS{Rouvrais02a,
AUTHOR = {Siegfried Rouvrais},
SCHOOL = {Université de Rennes 1},
TITLE = {Utilisation d'agents mobiles pour la construction de
services distribués},
YEAR = {2002},
OPTADDRESS = {},
MONTH = {juillet},
NOTE = {N. d'ordre : 2614},
OPTTYPE = {}
}
@INCOLLECTION{Jensen:02:Types,
AUTHOR = {T. Jensen},
BOOKTITLE = {The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones},
PUBLISHER = {Springer-Verlag},
TITLE = {Types in program analysis},
YEAR = {2002},
OPTADDRESS = {},
OPTCHAPTER = {},
OPTCROSSREF = {},
OPTEDITION = {},
EDITOR = {Torben Mogensen and David Schmidt and I. Hal Sudborough},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
PAGES = {204--222},
SERIES = {Lecture Notes in Computer Science 2566},
OPTTYPE = {},
OPTVOLUME = {}
}
@ARTICLE{Denney:02:Correctness,
AUTHOR = {E. Denney and T. Jensen},
JOURNAL = {Theoretical Computer Science},
TITLE = {Correctness of Java Card method lookup via logical
relations},
YEAR = {2002},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
PAGES = {305--331},
VOLUME = {283}
}
@INPROCEEDINGS{Besson:02:CallingContexts,
AUTHOR = {F. Besson and de Grenier de Latour, Thomas and T. Jensen},
BOOKTITLE = {Proc. of 4th Int Conf. on Principles and Practice of Declarative Programming (PPDP 2002)},
TITLE = {Secure calling contexts for stack inspection},
YEAR = {2002},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {76--87},
PUBLISHER = {ACM Press},
OPTSERIES = {},
OPTVOLUME = {},
URL = {http://www.irisa.fr/lande/fbesson/fbesson.html},
ABSTRACT = {Stack inspection is a mechanism for programming secure
applications by which a method can obtain information from the call
stack about the code that (directly or indirectly) invoked it. This
mechanism plays a fundamental role in the security architecture of
Java and the .NET Common Language Runtime. A central problem with
stack inspection is to determine to what extent the local checks
inserted into the code are sufficient to guarantee that a global
security property is enforced. In this paper, we present a technique
for inferring a secure calling context for a method. By a secure
calling context we mean a pre-condition on the call stack sufficient
for guaranteeing that execution of the method will not violate a
given global property. This is particularly useful for annotating
library code in order to avoid having to re-analyse libraries for
every new application. The technique is a constraint based static
program analysis implemented via fixed point iteration over an
abstract domain of linear temporal logic properties.}
}
@INPROCEEDINGS{Jensen:02:Iteration,
AUTHOR = {Thomas Jensen and Florimond Ployette and Olivier Ridoux},
BOOKTITLE = {Proc. of 4th Int workshop on Fixed Points in Computer Science (FICS'02)},
TITLE = {Iteration schemes for fixed point conputation},
YEAR = {2002},
OPTADDRESS = {},
OPTCROSSREF = {},
EDITOR = {A. Ingolfsdottir and Z. Esik},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {69--76},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{Eluard:02:SecureObjectFlow,
AUTHOR = {Marc Éluard and Thomas Jensen},
BOOKTITLE = {Proc. of 5th Smart Card Research and Advanced Application Conference (Cardis'02)},
TITLE = {Secure object flow analysis for Java Card},
YEAR = {2002},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
ORGANIZATION = {IFIP/USENIX},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@TECHREPORT{GenetVTTong-RR02,
AUTHOR = {T. Genet and Viet Triem Tong, V.},
INSTITUTION = {INRIA},
TITLE = {Proving Negative Conjectures on Equational Theories
using Induction and Abstract Interpretation},
YEAR = {2002},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {RR-4576},
OPTTYPE = {},
KEYWORDS = {Equational theories, proof by induction,
abstract interpretation, rewriting},
URL = {ftp://ftp.irisa.fr/local/lande/tg-vvtt-inria02.ps.gz},
ABSTRACT = {In this paper we present a method to prove automatically
initial negative properties on equational specifications. This method
tends to combine induction and abstract interpretation. Induction is
performed in a classical way using cover sets. Abstract
interpretation is done using an additional set of equations used to
approximate the initial model into an abstract one. Like in the
methods dedicated to the proof by induction of positive properties,
the equational specification is supposed to be oriented into a
terminating, confluent and complete term rewriting system.}
}
@PROCEEDINGS{Attali:01:EsmartProceedings,
TITLE = {Smart Card Programming and Security (e-Smart 2001)},
YEAR = {2001},
OPTADDRESS = {},
EDITOR = {Isabelle Attali and Thomas Jensen},
MONTH = {September},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PUBLISHER = {Springer LNCS vol. 2140},
OPTSERIES = {},
OPTVOLUME = {},
AUTHOR = {Isabelle Attali and Thomas Jensen}
}
@PHDTHESIS{Eluard:01:PhD,
AUTHOR = {Marc Éluard},
SCHOOL = {Université de Rennes 1},
TITLE = {Analyse de sécurité pour la certification d'applications
Java Card},
YEAR = {2001},
OPTADDRESS = {},
MONTH = {December},
NOTE = {N. d'ordre : 2614},
OPTTYPE = {}
}
@ARTICLE{Besson:01:ModelChecking,
AUTHOR = {F. Besson and T. Jensen and D. Le Métayer and T. Thorn},
JOURNAL = {Journal of Computer Security},
TITLE = {Model ckecking security properties of control flow
graphs},
YEAR = {2001},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
PAGES = {217--250},
VOLUME = {9},
URL = {http://www.irisa.fr/lande/fbesson/fbesson.html},
ABSTRACT = {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.}
}
@INPROCEEDINGS{GenetVTTong-LPAR01,
AUTHOR = {T. Genet and Viet Triem Tong, Valérie},
BOOKTITLE = {8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
TITLE = {Reachability Analysis of Term Rewriting Systems with
Timbuk},
YEAR = {2001},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {691--702},
PUBLISHER = {Springer Verlag},
SERIES = {Lectures Notes in Artificial Intelligence},
VOLUME = {2250},
KEYWORDS = {Timbuk, Term Rewriting, Reachability, Tree Automata,
Descendants, Verification},
URL = {ftp://ftp.irisa.fr/local/lande/tg-vvtt-lpar01.ps.gz},
ABSTRACT = {We present Timbuk -- a tree automata library -- which
implements usual operations on tree automata as well as a completion
algorithm used to compute an over-approximation of the set of
descendants R*(E) for a regular set E and a term rewriting system R,
possibly non linear and non terminating. On several examples of term
rewriting systems representing programs and systems to verify, we
show how to use Timbuk to construct their approximations and then
prove unreachability properties of these systems.}
}
@INPROCEEDINGS{Jensen:01:ClassAnalysis,
AUTHOR = {T. Jensen and F. Spoto},
BOOKTITLE = {Proc. of Foundations of Software Science and Computation Structures (FoSSaCS'01)},
TITLE = {Class analysis of object-oriented programs through
abstract interpretation},
YEAR = {2001},
OPTADDRESS = {},
OPTCROSSREF = {},
EDITOR = {F. Honsell and M. Miculan},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {261--275},
PUBLISHER = {Springer LNCS vol .2030},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{BePi01Convexhull,
AUTHOR = {David Pichardie and Yves Bertot},
BOOKTITLE = {Proc. of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01)},
TITLE = {Formalizing Convex Hulls Algorithms},
YEAR = {2001},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {2152},
OPTORGANIZATION = {},
PAGES = {346--361},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
OPTVOLUME = {}
}
@INPROCEEDINGS{Siveroni:01:Nordsec,
AUTHOR = {Igor Siveroni and Thomas Jensen and Marc Éluard},
BOOKTITLE = {Nordic Workshop on Secure IT-Systems},
TITLE = {A Formal Specification of the Java Card Applet Firewall},
YEAR = {2001},
OPTADDRESS = {},
OPTCROSSREF = {},
EDITOR = {Hanne Riis Nielson},
MONTH = {November},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
OPTVOLUME = {}
}
@INPROCEEDINGS{Eluard:01:Esmart,
AUTHOR = {Marc Éluard and Thomas Jensen and Ewen Denney},
BOOKTITLE = {Smart Card Programming and Security (e-Smart 2001},
TITLE = {An Operational Semantics of the Java Card Firewall},
YEAR = {2001},
OPTADDRESS = {},
OPTCROSSREF = {},
EDITOR = {Isabelle Attali and Thomas Jensen},
MONTH = {September},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
OPTPUBLISHER = {},
OPTSERIES = {},
VOLUME = {Springer LNCS vol. 2140}
}
@TECHREPORT{GenetVTTong-RR01,
AUTHOR = {Thomas Genet and Viet Triem Tong, Valérie},
INSTITUTION = {INRIA},
TITLE = {Reachability Analysis of Term Rewriting Systems with
Timbuk (extended version)},
YEAR = {2001},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {RR-4266},
TYPE = {Technical Report},
URL = {ftp://ftp.irisa.fr/local/lande/tg-vvtt-inria01.ps.gz},
ABSTRACT = {We present Timbuk -- a tree automata library -- which
implements usual operations on tree automata as well as a completion
algorithm used to compute an over-approximation of the set of
descendants R*(E) for a regular set E and a term rewriting system R,
possibly non linear and non terminating. On several examples of term
rewriting systems representing programs and systems to verify, we
show how to use Timbuk to construct their approximations and then
prove unreachability properties of these systems.}
}
@PROCEEDINGS{Jensen:00:JavaCard,
TITLE = {Proceedings of the International Workshop on Java Card
(Java Card 2000)},
YEAR = {2000},
ADDRESS = {Cannes, France},
EDITOR = {I. Attali and T. Jensen},
MONTH = {Septembre},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PUBLISHER = {Inria},
OPTSERIES = {},
OPTVOLUME = {}
}
@PHDTHESIS{HDR-PF,
AUTHOR = {Pascal Fradet},
SCHOOL = {Université de Rennes 1},
TITLE = {Approches langages pour la conception et la mise en
oeuvre de programmes},
YEAR = {2000},
OPTADDRESS = {},
MONTH = {novembre},
OPTNOTE = {},
TYPE = {document d'habilitation à diriger des recherches}
}
@PHDTHESIS{ThesePerin,
AUTHOR = {Michaël Périn},
SCHOOL = {IFSIC},
TITLE = {Spécifications graphiques multi-vues : formalisation et
vérification de cohérence},
YEAR = {2000},
OPTADDRESS = {},
MONTH = {October},
OPTNOTE = {},
OPTTYPE = {}
}
@INPROCEEDINGS{Denney:00:Correctness,
AUTHOR = {E. Denney and T. Jensen},
BOOKTITLE = {Proc. of European Symp. on Programming (ESOP 2000)},
TITLE = {Correctness of Java Card method lookup via logical
relations},
YEAR = {2000},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {104--118},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
OPTVOLUME = {}
}
@INPROCEEDINGS{GenetKlay-CADE00,
AUTHOR = {T. Genet and F. Klay},
BOOKTITLE = {Proceedings 17th International Conference on Automated Deduction},
TITLE = {Rewriting for Cryptographic Protocol Verification},
YEAR = {2000},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1831},
KEYWORDS = {Cryptographic Protocol, Verification, Term Rewriting,
Reachability, Approximation, Timbuk},
URL = {ftp://ftp.irisa.fr/local/lande/tg-fk-cade00.ps.gz},
ABSTRACT = {On a case study, we present a new approach for verifying
cryptographic protocols, based on rewriting and on tree automata
techniques. Protocols are operationally described using Term
Rewriting Systems and the initial set of communication requests is
described by a tree automaton. Starting from these two
representations, we automatically compute an over-approximation of
the set of exchanged messages (also recognized by a tree automaton).
Then, proving classical properties like confidentiality or
authentication can be done by automatically showing that the
intersection between the approximation and a set of prohibited
behaviors is the empty set. Furthermore, this method enjoys a simple
and powerful way to describe intruder work, the ability to consider
an unbounded number of parties, an unbounded number of interleaved
sessions, and a theoretical property ensuring safeness of the
approximation.}
}
@TECHREPORT{GenetK-CNET99,
AUTHOR = {T. Genet and F. Klay},
INSTITUTION = {INRIA},
TITLE = {Rewriting for Cryptographic Protocol Verification
(extended version)},
YEAR = {2000},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {3921},
TYPE = {Technical Report},
URL = {ftp://ftp.irisa.fr/local/lande/tg-fk-inria00.ps.gz},
ABSTRACT = {On a case study, we present a new approach for verifying
cryptographic protocols, based on rewriting and on tree automata
techniques. Protocols are operationally described using Term
Rewriting Systems and the initial set of communication requests is
described by a tree automaton. Starting from these two
representations, we automatically compute an over-approximation of
the set of exchanged messages (also recognized by a tree automaton).
Then, proving classical properties like confidentiality or
authentication can be done by automatically showing that the
intersection between the approximation and a set of prohibited
behaviors is the empty set. Furthermore, this method enjoys a simple
and powerful way to describe intruder work, the ability to consider
an unbounded number of parties, an unbounded number of interleaved
sessions, and a theoretical property ensuring safeness of the
approximation.}
}
@PHDTHESIS{Jensen:99:Hab,
AUTHOR = {Thomas Jensen},
SCHOOL = {Université de Rennes 1},
TITLE = {Analyse statiques de programmes : fondements et
applications},
YEAR = {1999},
OPTADDRESS = {},
MONTH = {décembre},
OPTNOTE = {},
TYPE = {document d'habilitation à diriger des recherches}
}
@PHDTHESIS{TT99,
AUTHOR = {T. Thorn},
SCHOOL = {Université de Rennes I, Ifsic, Irisa},
TITLE = {Vérification de politiques de sécurité par analyse de
programmes},
YEAR = {1999},
OPTADDRESS = {},
MONTH = {février},
OPTNOTE = {},
OPTTYPE = {}
}
@INPROCEEDINGS{SAS99:BJT,
AUTHOR = {F. Besson and T. Jensen and J.P. Talpin},
BOOKTITLE = {International Static Analysis Symposium, SAS'99},
TITLE = {Polyhedral Analysis for Synchronous Languages},
YEAR = {1999},
OPTADDRESS = {},
OPTCROSSREF = {},
EDITOR = {Gilberto Filé},
MONTH = {September},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
OPTPAGES = {},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1694},
KEYWORDS = {synchronous languages, abstract interpretation,
reachability analysis, infinite state systems},
ABSTRACT = {We define an operational semantics for the Signal
language and design an analysis which allows to verify properties
pertaining to the relation between values of the numeric and boolean
variables of a reactive system. A distinguished feature of the
analysis is that it is expressed and proved correct with respect to
the source program rather than on an intermediate representation of
the program. The analysis calculates a safe approximation to the set
of reachable states by a symbolic fixed point computation in the
domain of convex polyhedra using a novel widening operator based on
the convex hull representation of polyhedra.}
}
@INPROCEEDINGS{SSP99,
AUTHOR = {T. Jensen and D. Le Métayer and T. Thorn},
BOOKTITLE = {Proc. of the 20th IEEE Symp. on Security and Privacy},
TITLE = {Verification of control flow based security properties},
YEAR = {1999},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {mai},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {89--103},
PUBLISHER = {New York: IEEE Computer Society},
OPTSERIES = {},
OPTVOLUME = {}
}
@MISC{brevet99,
AUTHOR = {E. Denney and P. Fradet and C. Goire and T. Jensen and
D. Le Métayer},
OPTHOWPUBLISHED = {},
MONTH = {juillet},
NOTE = {Brevet d'invention},
TITLE = {Procédé de vérification de transformateurs de codes pour
un système embarqué, notamment sur une carte à puce},
YEAR = {1999}
}
@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},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
OPTTYPE = {},
KEYWORDS = {parallelism, compilation, specialized language,
program skeleton, data distribution, program transformation,
cost analysis},
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.}
}
@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},
YEAR = {1998},
OPTADDRESS = {},
MONTH = {December},
OPTNOTE = {},
OPTTYPE = {},
KEYWORDS = {Software engineering, program verification,
white-box testing, automated test data generation, program analysis,
program schemes},
URL = {ftp://ftp.irisa.fr/techreports/theses/1998/nicolas.ps.gz},
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.}
}
@INPROCEEDINGS{Jensen:98:Inference,
AUTHOR = {T. Jensen},
BOOKTITLE = {Proc. of 25th ACM Symposium on Principles of Programming Languages},
TITLE = {Inference of polymorphic and conditional strictness
properties},
YEAR = {1998},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
OPTMONTH = {},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {209--221},
PUBLISHER = {ACM Press},
OPTSERIES = {},
OPTVOLUME = {},
URL = {http://www.irisa.fr/lande/jensen/papers/popl98.ps},
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.}
}
@INPROCEEDINGS{tjdlmtt-iccl98,
AUTHOR = {T. Jensen and D. Le Métayer and T. Thorn},
BOOKTITLE = {Proceedings of the 1998 IEEE International Conference on Computer Languages},
TITLE = {Security and Dynamic Class Loading in Java: A
Formalisation},
YEAR = {1998},
OPTADDRESS = {},
OPTCROSSREF = {},
OPTEDITOR = {},
MONTH = {May},
OPTNOTE = {},
OPTNUMBER = {},
OPTORGANIZATION = {},
PAGES = {4--15},
PUBLISHER = {New York: IEEE Computer Society},
OPTSERIES = {},
OPTVOLUME = {},
URL = {ftp://ftp.irisa.fr/local/lande/tjdlmtt-iccl98.ps.gz},
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 \texttt{private} and
\texttt{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.}
}
@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},
YEAR = {1998},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {1210},
OPTTYPE = {},
KEYWORDS = {security, verification, finite-state system,
control flow, object orientation},
URL = {ftp://ftp.irisa.fr/techreports/1998/PI-1210.ps.gz},
ABSTRACT = {A fundamental problem in software-based security is
whether \textit{local} security checks inserted into the code are
sufficient to implement a given \textit{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).}
}
@PHDTHESIS{Gouranton:97:DerivationD,
AUTHOR = {V. Gouranton},
SCHOOL = {Université de Rennes I, Ifsic, Irisa},
TITLE = {Dérivation d'analyseurs dynamiques et statiques à partir
de spécifications opérationnelles},
YEAR = {1997},
OPTADDRESS = {},
OPTMONTH = {},
OPTNOTE = {},
OPTTYPE = {},
KEYWORDS = {analyse dynamique, analyse statique,
sémantique naturelle, transformation de programmes,
interprétation abstraite, analyse de durée de vie,
analyse de nécessité, élagage de programmes},
URL = {ftp://ftp.irisa.fr/local/lande/vgthese.ps.gz},
ABSTRACT = {Nous présentons un cadre de conception d'analyseurs
dynamiques et d'analyseurs statiques à partir de spécifications
opérationnelles. Nous proposons des spécifications d'analyseurs en
deux parties : la sémantique du langage de programmation considéré et
la définition de la propriété recherchée. Nous considérons le cadre
de la sémantique naturelle pour la définition du langage de
programmation. Ces sémantiques présentent un double avantage : elles
sont à la fois compositionnelles et intentionnelles. Les propriétés
sont définies comme des fonctions sur les arbres de preuves de la
sémantique. Celles qui ne sont pas spécifiques à un langage donné
peuvent ainsi être définies une fois pour toutes et spécialisées pour
des langages particuliers. La composition de la sémantique et de la
propriété définit une analyse dynamique {\em a posteriori} ; il
s'agit en effet d'une fonction qui calcule dans un premier temps la
trace d'exécution (arbre de preuve) complète d'un programme avant
d'en extraire la propriété recherchée. Des transformations de
programmes permettent d'obtenir une définition récursive autonome de
l'analyseur. Cette fonction est en fait un analyseur dynamique {\em à
la volée} dans le sens où il calcule la propriété recherchée au fur
et à mesure de l'exécution du programme. On réalise ensuite une
abstraction de cet analyseur pour obtenir un analyseur statique : on
applique pour ce faire la théorie de l'interprétation abstraite. Nous
illustrons notre cadre à l'aide d'exemples d'analyses spécifiques
comme la durée de vie d'un langage impératif et l'analyse de
nécessité d'un langage fonctionnel d'ordre supérieur. Nous montrons
aussi comment une analyse d'intérêt général, en l'occurrence le
filtrage de programmes, peut être définie sur un format de
sémantique, puis instanciée à différents langages.}
}
@ARTICLE{Jensen:97:Disjunctive,
AUTHOR = {T. Jensen},
JOURNAL = {ACM Transactions on Programming Languages and Systems},
TITLE = {Disjunctive Program Analysis for Algebraic Data Types},
YEAR = {1997},
OPTMONTH = {},
OPTNOTE = {},
NUMBER = {5},
PAGES = {752--804},
VOLUME = {19},
URL = {http://www.irisa.fr/lande/jensen/papers/toplas97.ps},
ABSTRACT = {We describe how binding-time, data-flow, and strictness
analyses for languages with higher-order functions and algebraic data
types can be obtained by instantiating a generic program logic and
axiomatization of the properties analyzed for. A distinctive feature
of the analyses is that disjunctions of program properties are
represented exactly. This yields analyses of high precision and
provides a logical characterization of abstract interpretations
involving tensor products and uniform properties of recursive data
structures. An effective method for proving properties of a program
based on fixed-point iteration is obtained by grouping logically
equivalent formulae of the same type into equivalence classes,
obtaining a lattice of properties of that type, and then defining an
abstract interpretation over these lattices. We demonstrate this in
the case of strictness analysis by proving that the strictness
abstract interpretation of a program is the equivalence class
containing the strongest property provable of the program in the
strictness logic.}
}