Gouraud S.D. and A. Gotlieb.
Using chrs to generate test cases for the jcvm.
In Eighth International Symposium on Practical Aspects of
Declarative Languages, PADL 06, Charleston, South Carolina, January 2006.
LNCS 3819.
@INPROCEEDINGS{GG06,
AUTHOR = {Gouraud S.D. and Gotlieb, A.},
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},
PAGES = {},
NOTE = {LNCS 3819},
YEAR = 2006,
KEYWORDS = {CHR, Software testing, Java Card Virtual Machine}
}
@ARTICLE{g+:jakarta,
AUTHOR = {G. Barthe and P. Courtieu and G. Dufay and S. Melo de
Sousa},
TITLE = {{Jakarta: tool-assisted specification and verification of
the JavaCard Platform}},
YEAR = {2006},
JOURNAL = {{Journal of Automated Reasoning}},
NOTE = {To appear}
}
David Cachera, Thomas Jensen, David Pichardie, and Vlad Rusu.
Extracting a data flow analyser in constructive logic.
tcs, 342(1):56-78, September 2005.
Extended version of [CJPR04].
@ARTICLE{CaJePiRu05TCSExtractAnalyser,
AUTHOR = {David Cachera and Thomas Jensen and David Pichardie
and Vlad Rusu},
TITLE = {Extracting a Data Flow Analyser in Constructive
Logic},
JOURNAL = {tcs},
YEAR = {2005},
VOLUME = {342},
NUMBER = {1},
PAGES = {56-78},
MONTH = {September},
NOTE = {Extended version of \cite{CaJePiRu04ExtractAnalyser}}
}
David Cachera, Thomas Jensen, David Pichardie, and Gerardo Schneider.
Certified memory usage analysis.
In Proc. of 13th International Symposium on Formal Methods
(FM'05), volume 3582 of Lecture Notes in Computer Science, pages
91-106. Springer-Verlag, 2005.
@INPROCEEDINGS{CaJePiSc05MemoryUsage,
AUTHOR = {David Cachera and Thomas Jensen and David Pichardie
and Gerardo Schneider},
TITLE = {Certified Memory Usage Analysis},
CROSSREF = {fm05},
PAGES = {91--106}
}
@PROCEEDINGS{fm05,
YEAR = {2005},
BOOKTITLE = {Proc.\ of 13th International Symposium on Formal Methods (FM'05)},
TITLE = {Proc.\ of 13th International Symposium on Formal Methods (FM'05)},
PUBLISHER = {Springer-Verlag},
VOLUME = {3582},
SERIES = {Lecture Notes in Computer Science}
}
S.-D. Gouraud and A. Gotlieb.
Utilisation des chrs pour générer des cas de test pour la machine
virtuelle java card.
In Journées Francophones de Programmation par Contraintes,
2005.
to appear.
@PROCEEDINGS{jfpc05,
BOOKTITLE = {Journ\'ees Francophones de Programmation par Contraintes},
TITLE = {Journ\'ees Francophones de Programmation par Contraintes},
YEAR = {2005},
NOTE = {to appear}
}
G. Barthe and G. Dufay.
A Tool-Assisted Framework for Certified Bytecode Verification.
In M. Wermelinger and T. Margaria-Steffen, editors, Proceedings
of FASE'04, volume 2984 of Lecture Notes in Computer Science, pages
99-113, Barcelona, Spain, March 2004. Springer-Verlag.
@INPROCEEDINGS{CaJePiRu04ExtractAnalyser,
AUTHOR = {David Cachera and Thomas Jensen and David Pichardie
and Vlad Rusu},
TITLE = {Extracting a Data Flow Analyser in Constructive
Logic},
PAGES = {385--400},
CROSSREF = {esop04}
}
@PROCEEDINGS{esop04,
YEAR = {2004},
BOOKTITLE = {Proceedings of ESOP'04},
TITLE = {Proceedings of ESOP'04},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {2986}
}
Simao Melo de Sousa.
Outils et techniques pour la vérification formelle de la
plate-forme JavaCard.
PhD thesis, INRIA/Universidade de Nice-Sophia Antipolis, February
2003.
@PHDTHESIS{SouPhd,
AUTHOR = {Sim{\~a}o Melo de Sousa},
TITLE = {Outils et techniques pour la v\'erification formelle de la plate-forme JavaCard},
SCHOOL = {INRIA/Universidade de Nice-Sophia Antipolis},
YEAR = {2003},
MONTH = {February},
PSURL = {http://www.di.ubi.pt/~desousa/tese.ps}
}