Publications of year 2006

Articles in journal or book chapters

Frédéric Besson, Thomas Jensen, and David Pichardie. Proof-Carrying Code from Certified Abstract Interpretation to Fixpoint Compression. Theoretical Computer Science, 364(3):273-291, 2006.

@Article{TCSAppSem:BessonJensenPichardie,
author = "Fr\'ed\'eric Besson and Thomas Jensen and David Pichardie",
title = "Proof-Carrying Code from Certified Abstract Interpretation to Fixpoint Compression",
journal = "Theoretical Computer Science",
year = 2006,
volume = 364,
number = 3,
pages = {273--291},

}

B. Botella, A. Gotlieb, and C. Michel. Symbolic execution of floating-point computations. The Software Testing, Verification and Reliability journal, 2006. Note: To appear. Keyword(s): Symbolic execution, Floating-point computations, Automatic test data generation, Constraint solving.

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

@Article{BGM05,
author = {Botella, B. and Gotlieb, A. and Michel, C.},
title = {Symbolic execution of floating-point computations},
journal = {The Software Testing, Verification and Reliability journal},
year = {2006},
note = {to appear},
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},
keywords = {Symbolic execution, Floating-point computations, Automatic test data generation, Constraint solving} 
}

Conference articles

Gilles Barthe, Julien Forest, David Pichardie, and Vlad Rusu. Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant.. In Proc of 8th International Symposium on Functional and Logic Programming (FLOPS'06), volume 3945 of Lecture Notes in Computer Science, pages 114-129, 2006. Springer-Verlag.

@inproceedings{BartheFPR06,
author = {Gilles Barthe and Julien Forest and David Pichardie and Vlad Rusu},
title = {Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant.},
pages = {114-129},
booktitle = {Proc\. of 8th International Symposium on Functional and Logic Programming (FLOPS'06)},
series = "Lecture Notes in Computer Science",
publisher = "{Springer-Verlag}",
volume = {3945},
year = {2006},

}

F. Besson. Fast Reflexive Arithmetic Tactics: the linear case and beyond. In Types for Proofs and Programs (TYPES'06), volume 4502 of LNCS, pages 48-62, 2006. Springer. [PDF]

@InProceedings{Besson:types06,
author = {F. Besson},
title = {Fast Reflexive Arithmetic Tactics: the linear case and beyond},
booktitle = {Types for Proofs and Programs (TYPES'06)},
year = {2006},
series = {LNCS},
volume = {4502},
publisher = {Springer},
pages = {48-62},
pdf = {http://www.irisa.fr/lande/fbesson/Fast_Reflexive_Arithmetics_Tactics.pdf} 
}

Frédéric Besson, Guillaume Dufay, and Thomas Jensen. A Formal Model of Access Control for Mobile Interactive Devices. In 11th European Symposium On Research In Computer Security (ESORICS'06), volume 4189 of Lecture Notes in Computer Science, 2006. Springer. [WWW]

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{ESORICS-06-BJD,
author = {Frédéric Besson and Guillaume Dufay and Thomas Jensen},
title = {A Formal Model of Access Control for Mobile Interactive Devices},
booktitle = {11th European Symposium On Research In Computer Security (ESORICS'06)},
publisher = {Springer},
URL = {http://www.irisa.fr/lande/fbesson/fbesson.html},
volume = 4189,
series = {Lecture Notes in Computer Science},
year = {2006},
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.},

}

F. Besson, T. Jensen, and D. Pichardie. A PCC Architecture based on Certified Abstract Interpretation. In Proc. of 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06), ENTCS, 2006. Springer-Verlag. [WWW]

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{EAAI:BessonJensenPichardie,
AUTHOR= "F. Besson and T. Jensen and D. Pichardie",
TITLE= "{A PCC Architecture based on Certified Abstract Interpretation}",
PUBLISHER = {Springer-Verlag},
YEAR = 2006,
SERIES = {ENTCS},
URL = {http://www.irisa.fr/lande/fbesson/fbesson.html},
BOOKTITLE={Proc. of 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06)},
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.},

}

B. Blanc, F. Bouquet, A. Gotlieb, B. Jeannet, T. Jéron, B. Legeard, B. Marre, C. Michel, and M. Rueher. The V3F project. In Proceedings of Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA'06), Nantes, France, Sep. 2006.

@InProceedings{BBG06,
author = {Blanc, B. and Bouquet, F. and Gotlieb,A. and Jeannet, B. and Jéron, T. and Legeard, B. and Marre, B. and Michel, C. and Rueher, M.},
title = {The V3F project},
booktitle = {Proceedings of Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA'06)},
address = {Nantes, France},
month = {Sep.},
year = 2006,

}

Y. Boichut and T. Genet. Feasible Trace Reconstruction for Rewriting Approximations.. In RTA, volume 4098 of LNCS, pages 123-135, 2006. Springer.

@inproceedings{BoichutG-RTA06,
author = {Boichut, Y. and Genet, T.},
title = {{F}easible {T}race {R}econstruction for {R}ewriting {A}pproximations.},
booktitle = {RTA},
year = {2006},
pages = {123-135},
publisher = {Springer},
series = {LNCS},
volume = {4098}
}

N. Bonnel and G. Le Guernic. Système de recherche de méthodes Java basé sur leur signature. In Proceedings of Majecstic 2006, November 2006. [PDF]

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{leguernic06jmbrowser,
AUTHOR = {N. Bonnel and G. Le~Guernic},
TITLE = {{S}ystème de recherche de méthodes {J}ava basé sur leur signature},
BOOKTITLE = {Proceedings of Majecstic 2006},
YEAR = 2006,
MONTH = NOV,
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.} 
}

Y. Glouche, T. Genet, O. Heen, and O. Courtay. A Security Protocol Animator Tool for AVISPA. In ARTIST-2 workshop on security of embedded systems, Pisa (Italy), 2006. [WWW]

@INPROCEEDINGS{Animator,
AUTHOR = "Glouche, Y. and Genet, T. and Heen, O. and Courtay, O.",
TITLE = "{A} {S}ecurity {P}rotocol {A}nimator {T}ool for {AVISPA}",
YEAR = {2006},
URL = {http://www.irisa.fr/lande/genet/publications.html},
BOOKTITLE = {ARTIST-2 workshop on security of embedded systems, Pisa (Italy)} 
}

A. Gotlieb and P. Bernard. A Semi-empirical Model of Test Quality in Symmetric Testing: Application to Testing Java Card APIs. In Sixth International Conference on Quality Software (QSIC'06), Beijing, China, Oct. 2006.

@InProceedings{GB06,
author = {Gotlieb, A. and Bernard, P.},
title = {A Semi-empirical Model of Test Quality in Symmetric Testing: Application to Testing Java Card APIs},
booktitle = {Sixth International Conference on Quality Software (QSIC'06)},
address = {Beijing, China},
month = {Oct.},
year = 2006,

}

A. Gotlieb, B. Botella, and M. Watel. Inka: Ten years after the first ideas. In 19th International Conference on Software & Systems Engineering and their Applications (ICSSEA'06), Paris, France, Dec. 2006.

@InProceedings{GBW06,
author = {Gotlieb, A. and Botella, B. and Watel, M.},
title = {Inka: Ten years after the first ideas},
booktitle = {19th International Conference on Software \& Systems Engineering and their Applications (ICSSEA'06)},
address = {Paris, France},
month = {Dec.},
year = 2006,

}

A. Gotlieb and M. Petit. Path-oriented Random Testing. In Proceedings of the 1st ACM Int. Workshop on Random Testing (RT'06), Portland, Maine, July 2006.

@InProceedings{GP06,
author = {Gotlieb, A. and Petit, M.},
title = {Path-oriented Random Testing},
booktitle = {Proceedings of the 1st ACM Int. Workshop on Random Testing (RT'06)},
address = {Portland, Maine},
month = {July},
year = 2006,

}

A. Gotlieb and M. Petit. Path-oriented random testing.. In Proceedings of the International Workshop on Random Testing, Portland, USA, pages 28-35, July 2006. ACM.

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{GP06,
author = {Gotlieb, A. and Petit, M.},
title = {Path-oriented random testing.},
booktitle = {Proceedings of the International Workshop on Random Testing},
year = {2006},
pages = {28--35},
publisher = {ACM},
address = {Portland, USA},
month = {July},
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.},

}

S. Gouraud and A. Gotlieb. Using CHRs to generate test cases for the JCVM. In Eighth International Symposium on Practical Aspects of Declarative Languages, PADL 06, volume 3819 of Lecture Notes in Computer Science, Charleston, South Carolina, January 2006. Keyword(s): CHR, Software testing, Java Card Virtual Machine.

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{GG06,
author = {S. Gouraud and A. Gotlieb},
title = {Using CHRs to generate test cases for the JCVM},
booktitle = {Eighth International Symposium on Practical Aspects of Declarative Languages, PADL 06},
address = {Charleston, South Carolina},
month = {January},
volume = {3819},
series = {Lecture Notes in Computer Science},
year = 2006,
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.},
keywords = {CHR, Software testing, Java Card Virtual Machine},

}

G. Le Guernic, A. Banerjee, T. Jensen, and D. Schmidt. Automata-based Confidentiality Monitoring. In Proceedings of the Annual Asian Computing Science Conference, volume 4435 of Lecture Notes in Computer Science, DEC 6--8 2006. Note: To appear. [PDF]

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{LeGuernic2006acm,
TITLE = {Annual Asian Computing Science Conference: Focusing on Secure Software and Related Issues},
BOOKTITLE = {Proceedings of the Annual Asian Computing Science Conference},
YEAR = 2006,
SERIES = {Lecture Notes in Computer Science},
MONTH = DEC # { 6--8},
LOCATION = {Tokyo, Japan},
AUTHOR = {G. Le~Guernic and A. Banerjee and T. Jensen and D. Schmidt},
TITLE = {{A}utomata-based {C}onfidentiality {M}onitoring},
NOTE = {To appear},
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. } 
}

Gurvan Le Guernic, Anindya Banerjee, Thomas Jensen, and David Schmidt. Automaton-based Confidentiality Monitoring. In 11th Annual Asian Computing Science Conference (ASIAN'06), volume 4435 of Lecture Notes in Computer Science, Tokyo, Japan, December 2006. Note: To appear.

@InProceedings{GBJS06,
author = {Gurvan {Le Guernic} and Anindya Banerjee and Thomas Jensen and David Schmidt},
title = {Automaton-based Confidentiality Monitoring},
booktitle = {11th Annual Asian Computing Science Conference (ASIAN'06)},
address = {Tokyo, Japan},
month = {December},
volume = {4435},
note = {to appear},
series = {Lecture Notes in Computer Science},
year = 2006 
}

M. Petit and A. Gotlieb. Raisonner et filtrer avec un choix probabiliste partiellement connu. In Deuxièmes Journées Francophones de Programmation par Contraintes, Nîmes, France, Juin 2006.

@InProceedings{PG06,
author = {Petit, M. and Gotlieb, A.},
title = {Raisonner et filtrer avec un choix probabiliste partiellement connu},
booktitle = {Deuxi\`emes Journ\'ees Francophones de Programmation par Contraintes},
year = 2006,
address = {N\^imes, France},
month = {Juin},
abstract {La Programmation Concurrente par Contraintes Probabilistes (PCCP) étend la Programmation Concurrente par Contraintes (CCP) par l'ajout d'un opérateur de choix probabiliste. Cet opérateur permet d'introduire de l'aléa dans l'exécution d'un processus de CCP. Dans cet article, les fonctionnalités de cet opérateur sont étendues afin de raisonner avec un choix probabiliste partiellement connu. Pour cela, nous définissons l'opérateur de choix probabiliste comme un nouveau combinateur de contraintes et lui associons un algorithme de filtrage. Cet algorithme de filtrage permet, la plupart du temps, d'accélérer la propagation de contraintes. L'implantation sous la forme d'une nouvelle librairie d'opérateurs de choix probabilistes pour SICStus Prolog ainsi qu'une validation expérimentale est présentée.},

}

Pascal Sotin, David Cachera, and Thomas Jensen. Quantitative Static Analysis over semirings: analysing cache behaviour for Java Card. In 4th International Workshop on Quantitative Aspects of Programming Languages (QAPL 2006), volume 164 of Electronic Notes in Theoretical Computer Science, pages 153-167, 2006. Elsevier.

@InProceedings{SCJ06,
author = {Pascal Sotin and David Cachera and Thomas Jensen},
title = {{Quantitative Static Analysis over semirings: analysing cache behaviour for Java Card}},
booktitle = {4th International Workshop on Quantitative Aspects of Programming Languages (QAPL 2006)},
year = {2006},
series = {Electronic Notes in Theoretical Computer Science},
pages = {153-167},
volume = {164},
publisher = {Elsevier} 
}

Internal reports

G. Le Guernic, A. Banerjee, and D. Schmidt. Automaton-based Non-interference Monitoring. Technical report 2006-1, Department of Computing and Information Sciences, College of Engineering, Kansas State University, 234 Nichols Hall, Manhattan, KS 66506, USA, April 2006.

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",
title = "Automaton-based Non-interference Monitoring",
institution = "Department of Computing and Information Sciences, College of Engineering, Kansas State University",
year = 2006,
number = "2006-1",
address = "234 Nichols Hall, Manhattan, KS 66506, USA",
month = apr,
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." 
}

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},
TITLE = {{A}utomaton-based {N}on-interference {M}onitoring},
INSTITUTION = {{D}epartment of {C}omputing and {I}nformation {S}ciences, {C}ollege of {E}ngineering, {K}ansas {S}tate {U}niversity},
OPTINSTITUTION = {{K}ansas {S}tate {U}niversity},
YEAR = 2006,
NUMBER = {2006-1},
ADDRESS = {234 Nichols Hall, Manhattan, KS 66506, USA},
OPTADDRESS = {Manhattan, KS, USA},
MONTH = APR,
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. },
URL = {http://www.cis.ksu.edu/~schmidt/techreport/2006.list.html} 
}

Manuals, booklets

Y. Glouche and T. Genet. SPAN -- A Security Protocol ANimator for AVISPA -- User Manual. IRISA / Université de Rennes 1, 2006. [WWW]

@Manual{span-manual,
title = {{S}{P}{A}{N} -- A {S}ecurity {P}rotocol {A}{N}imator for {AVISPA} -- {U}ser {M}anual},
AUTHOR = {Glouche, Y. and Genet, T.},
organization = {IRISA / Universit\'e de Rennes 1},
year = {2006},
url = {http://www.irisa.fr/lande/genet/span/} 
}

BACK TO INDEX

This document was translated from BibT_EX by bibtex2html

Publications

Menu

Publications of year 2006

Articles in journal or book chapters

Conference articles

Internal reports

Manuals, booklets