BACK TO INDEX

Publications of year 2003

Thesis

  1. V. Viet Triem Tong. Automates d'arbres et réécriture pour l'étude de problèmes d'accessibilité. PhD thesis, Université Rennes 1, 2003. 
    @PHDTHESIS{VietTriemTong-PhD03,
AUTHOR = {Viet Triem Tong, V.},
TITLE = {Automates d'arbres et réécriture pour l'étude de problèmes d'accessibilité},
SCHOOL = {Université Rennes 1},
YEAR = {2003} 
}


Articles in journal or book chapters

  1. A. Banerjee and T. Jensen. Control-flow analysis with rank-2 intersection types. Mathematical Structures in Computer Science, 13(1):87-124, 2003. 
    @Article{Banerjee:03:Rank2,
author = {A. Banerjee and T. Jensen},
title = {Control-flow analysis with rank-2 intersection types},
Journal = {Mathematical Structures in Computer Science},
volume = "13",
number = "1",
pages = "87--124",
year = "2003" 
}


  2. F. Spoto and T. Jensen. Class Analyses as Abstract Interpretations of Trace Semantics. ACM Transactions on Programming Languages and Systems (TOPLAS), 25(5):578-630, 2003. 
    @Article{Spoto:ClassAnalysis:03,
author = {Spoto, F. and Jensen, T.},
title = {{C}lass {A}nalyses as {A}bstract {I}nterpretations of {T}race {S}emantics},
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
year = {2003},
volume = {25},
number = {5},
pages = {578--630} 
}


Conference articles

  1. F. Besson and T. Jensen. Modular Class Analysis with DATALOG. In R. Cousot, editor, Proc. of 10th Static Analysis Symposium (SAS 2003), pages 19-36, 2003. Springer LNCS vol. 2694. [WWW]
    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{Besson:03:Modular,
author = "F. Besson and T. Jensen",
title = "Modular Class Analysis with DATALOG",
booktitle = "Proc.~of 10th Static Analysis Symposium (SAS 2003)",
year = "2003",
editor = "R.~Cousot",
pages = "19--36",
publisher = "Springer LNCS vol.~2694",
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. } 
}


  2. David Cachera and Katell Morin-Allory. Verification of Control Properties in the Polyhedral Model. In Proc. 1st MEMOCODE conference, Mont-St-Michel, France, June 2003. [WWW] 
    @InProceedings{CacMor03,
author = {David Cachera and Katell Morin-Allory},
title = {{Verification of Control Properties in the Polyhedral Model}},
booktitle = {Proc. 1st MEMOCODE conference},
year = 2003,
address = {Mont-St-Michel, France},
url = {ftp://ftp.irisa.fr/local/lande/dckmaMEMOCODE03.ps.gz},
month = {jun} 
}


  3. David Cachera and David Pichardie. Embedding of Systems of Affine Recurrence Equations in Coq. In Proc. TPHOLs 2003, 16th International Conference on Theorem Proving in Higher Order Logics, LNCS, Rome, Italy, September 2003. [WWW] 
    @InProceedings{CacPic03,
author = {David Cachera and David Pichardie},
title = {{Embedding of Systems of Affine Recurrence Equations in Coq}},
booktitle = {{Proc. TPHOLs 2003, 16th International Conference on Theorem Proving in Higher Order Logics }},
year = 2003,
series = {LNCS},
url = {ftp://ftp.irisa.fr/local/lande/dcdpTPHOL03.ps.gz},
address = {Rome, Italy},
month = {sep} 
}


  4. G. Feuillade and T. Genet. Reachability in conditional term rewriting systems. In FTP'2003, International Workshop on First-Order Theorem Proving, volume 86 n. 1 of Electronic Notes in Theoretical Computer Science, June 2003. Elsevier. [WWW] Keyword(s): Term Rewriting, Conditional Term Rewriting, Reachability, Tree Automata. 
    @InProceedings{FeuilladeG-FTP03,
Author = {Feuillade, G. and Genet, T.},
Title = {Reachability in conditional term rewriting systems},
BookTitle = {FTP'2003, International Workshop on First-Order Theorem Proving},
URL= {http://www.irisa.fr/lande/genet/publications.html},
KEYWORDS = {Term Rewriting, Conditional Term Rewriting, Reachability, Tree Automata},
Month = {June},
series = entcs,
volume = {86 n. 1},
publisher= {Elsevier},
Year = {2003} 
}


  5. T. Genet, T. Jensen, V. Kodati, and D. Pichardie. A Java Card CAP Converter in PVS. In Proceedings of the 2nd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2003), 2003. ENTCS 82(2). [WWW] Keyword(s): Java, Java Card, CAP Format, Compiler, Verification, Proof Assistant, PVS. 
    @InProceedings{GenetJKP-COCV03,
author = "Genet, T. and Jensen, T. and Kodati, V. and Pichardie, D.",
title = "A {J}ava {C}ard {C}{A}{P} Converter in {PVS}",
booktitle = "Proceedings of the 2nd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2003)",
URL = {http://www.irisa.fr/lande/genet/publications.html},
KEYWORDS = {Java, Java Card, CAP Format, Compiler, Verification, Proof Assistant, PVS},
year = "2003",
publisher = "ENTCS 82(2)" 
}


  6. T. Genet, Y.-M. Tang-Talpin, and V. Viet Triem Tong. Verification of Copy Protection Cryptographic Protocol using Approximations of Term Rewriting Systems. In In Proceedings of Workshop on Issues in the Theory of Security, 2003. [WWW] Keyword(s): Cryptographic Protocol, Verification, Term Rewriting, Reachability, Approximation, Timbuk. 
    @InProceedings{GenetTTVTT-wits03,
author = {Genet, T. and Tang-Talpin, Y.-M. and Viet Triem Tong, V.},
title = {{V}erification of {C}opy {P}rotection {C}ryptographic {P}rotocol using {A}pproximations of {T}erm {R}ewriting {S}ystems},
BookTitle = {In Proceedings of {W}orkshop on {I}ssues in the {T}heory of {S}ecurity},
URL = {http://www.irisa.fr/lande/genet/publications.html},
KEYWORDS= {Cryptographic Protocol, Verification, Term Rewriting, Reachability, Approximation, Timbuk},
year = {2003} 
}


  7. Arnaud Gotlieb. Exploiting Symmetries to Test Programs. In Proc. of 14th IEEE International Symposium on Software Reliability Engineering (ISSRE 2003), Denver, Colorado, USA, 2003. Note: 17th to 20th November. 
    @InProceedings{Gotlieb:03:SymTest,
author = "Arnaud Gotlieb",
title = "Exploiting Symmetries to Test Programs",
booktitle = "Proc.~of 14th IEEE International Symposium on Software Reliability Engineering (ISSRE 2003)",
address = "Denver, Colorado, USA",
year = "2003",
note = "17th to 20th November",

}


  8. A. Gotlieb and B. Botella. Automated Metamorphic Testing. In Proc. of the 27th IEEE Annual International Computer Software and Applications Conference (COMPSAC), Dallas, TX, USA, 2003. Note: 3th to 7th November. 
    @InProceedings{Gotlieb:03:MetaTest,
author = "A. Gotlieb and B. Botella",
title = "Automated Metamorphic Testing",
booktitle = "Proc. of the 27th IEEE Annual International Computer Software and Applications Conference (COMPSAC)",
address = "Dallas, TX, USA",
year = "2003",
note = "3th to 7th November",

}


  9. Lionel van Aertryck and Thomas Jensen. UML-CASTING: Test synthesis from UML models using constraint resolution. In J-M. Jézéquel, editor, Proc. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'2003), 2003. INRIA. 
    @InProceedings{Aertryck:03:UMLCasting,
author = {Lionel van~Aertryck and Thomas Jensen},
title = {UML-CASTING: Test synthesis from UML models using constraint resolution},
booktitle = {Proc.~Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'2003)},
year = {2003},
editor = {J-M.~Jézéquel},
publisher = {INRIA} 
}


Internal reports

  1. David Cachera and Katell Morin-Allory. Verification of Control Properties in the Polyhedral Model. Technical report 1515, INRIA, 2003. [WWW] 
    @TechReport{CacMorRR03,
author = {David Cachera and Katell Morin-Allory},
title = {{Verification of Control Properties in the Polyhedral Model}},
institution = {INRIA},
url ={ftp://ftp.irisa.fr/techreports/2003/PI-1515.ps.gz},
year = 2003,
number = 1515 
}


  2. David Cachera and David Pichardie. Proof Tactics for the Verification of Structured Systems of Affine Recurrence Equations. Technical report 1511, INRIA, 2003. [WWW] 
    @TechReport{CacPicRR03,
author = {David Cachera and David Pichardie},
title = {{Proof Tactics for the Verification of Structured Systems of Affine Recurrence Equations}},
institution = {INRIA},
url={ftp://ftp.irisa.fr/techreports/2003/PI-1511.ps.gz},
year = 2003,
number = 1511 
}


  3. G. Feuillade, T. Genet, and V. Viet Triem Tong. Reachability Analysis over Term Rewriting Systems. Technical report RR-4970, INRIA, 2003. [WWW] Keyword(s): Term Rewriting, Reachability, Tree Automata, Approximations, Verification, Timbuk, Abstract Interpretation.
    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.

    @TECHREPORT{FeuilladeGVTT-RR03,
AUTHOR = "Feuillade, G. and Genet, T. and Viet Triem Tong, V.",
TITLE = "{R}eachability {A}nalysis over {T}erm {R}ewriting {S}ystems",
INSTITUTION = {INRIA},
NUMBER = {RR-4970},
YEAR = {2003},
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.} 
}


Manuals, booklets

  1. T. Genet. Timbuk 2.0 -- A Tree Automata Library -- Reference Manual and Tutorial. 2003. Note: 81 pages. [WWW] 
    @Manual{Timbuk-manual,
AUTHOR = {Genet, T.},
TITLE = {{T}imbuk 2.0 -- A {T}ree {A}utomata {L}ibrary -- {R}eference {M}anual and {T}utorial},
HOWPUBLISHED = {IRISA / Université de Rennes 1},
NOTE = {81 pages},
URL = {http://www.irisa.fr/lande/genet/timbuk/},
YEAR = {2003} 
}



BACK TO INDEX

This document was translated from BibTEX by bibtex2html