Publications : 2005

[BCM05]

P. Bouyer, F. Chevalier, and N. Markey. On the Expressiveness of TPTL and MTL. In Proceedings of the 25th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'05), volume 3821 of Lecture Notes in Computer Science, pages 432--443, Hyderabad, India, December 2005. Springer.
doi: 10.1007/11590156_35.
[ BibTex | DOI | Web page | PS | PDF ]

[Gas05a]

R. Gascon. Verifying qualitative and quantitative properties with LTL over concrete domains. In Proceedings of the 4th Workshop on Methods for Modalities (M4M-4), volume 194 of Informatik Bericht, pages 54--61, Berlin, Germany, December 2005. Humboldt Universität zu Berlin.
[ BibTex | Web page | PS | PDF ]

[Lar05b]

F. Laroussinie. Timed modal logics for the verification of real-time systems. In Proceedings of the 4th Workshop on Methods for Modalities (M4M-4), volume 194 of Informatik Bericht, pages 293--305, Berlin, Germany, December 2005. Humboldt Universität zu Berlin.
[ BibTex | Web page | PS | PDF ]

[KLT05]

S. Kremer, Y. Lakhnech, and R. Treinen. The Prouvé Manual: Specifications, Semantics, and Logics. Technical Report 7, projet RNTL PROUVÉ, December 2005. 49 pages.
[ BibTex | Web page | PS | PDF ]

[PR05b]

S. Pinchinat and S. Riedweg. On the Architectures in Decentralized Supervisory Control. In Proceedings of the 44th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC'05), pages 12--17, Seville, Spain, December 2005. IEEE Control System Society.
[ BibTex | Web page | PS | PDF ]

[Bac05]

M. Baclet. Applications du model-checking à des problèmes de vérification de systèmes sur puce. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2005.
[ BibTex | Web page | PDF ]

[Lar05a]

F. Laroussinie. Model checking temporisé --- Algorithmes efficaces et complexité. Mémoire d'habilitation, Université Paris 7, Paris, France, December 2005.
[ BibTex | Web page | PDF ]

[ABRS05]

P. A. Abdulla, N. Bertrand, A. Rabinovich, and Ph. Schnoebelen. Verification of Probabilistic Systems with Faulty Communication. Information and Computation, 202(2):141--165, November 2005.
doi: 10.1016/j.ic.2005.05.008.
[ BibTex | DOI | Web page | PS | PDF ]

[Bau05]

M. Baudet. Deciding Security of Protocols against Off-line Guessing Attacks. In Proceedings of the 12th ACM Conference on Computer and Communications Security (CCS'05), pages 16--25, Alexandria, Virginia, USA, November 2005. ACM Press.
doi: 10.1145/1102120.1102125.
[ BibTex | DOI | Web page | PS | PDF ]

[Gas05b]

P. Gastin. On the synthesis of distributed controllers. Invited talk, Workshop Perspectives in Verification, in honor of Wolfgang Thomas on the occasion of his Doctorate Honoris Causa, Cachan, France, November 2005.
[ BibTex ]

[BLR05]

P. Bouyer, F. Laroussinie, and P.-A. Reynier. Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems. In Proceedings of the 3rd International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'05), volume 3829 of Lecture Notes in Computer Science, pages 112--126, Uppsala, Sweden, November 2005. Springer.
doi: 10.1007/11603009_10.
[ BibTex | DOI | Web page | PS | PDF ]

[CF05]

G. Cécé and A. Finkel. Verification of Programs with Half-Duplex Communication. Information and Computation, 202(2):166--190, November 2005.
doi: 10.1016/j.ic.2005.05.006.
[ BibTex | DOI | Web page | PDF ]

[DZG05]

S. Dal Zilio and R. Gascon. Resource Bound Certification for a Tail-Recursive Virtual Machine. In Proceedings of the 3rd Asian Symposium on Programming Languages and Systems (APLAS'05), volume 3780 of Lecture Notes in Computer Science, pages 247--263, Tsukuba, Japan, November 2005. Springer.
doi: 10.1007/11575467_17.
[ BibTex | DOI | Web page | PS | PDF ]

[VG05]

K. N. Verma and J. Goubault-Larrecq. Karp-Miller Trees for a Branching Extension of VASS. Discrete Mathematics & Theoretical Computer Science, 7(1):217--230, November 2005.
[ BibTex | Web page | PS | PDF ]

[LS05b]

D. Lugiez and Ph. Schnoebelen. Decidable first-order transition logics for PA-processes. Information and Computation, 203(1):75--113, November 2005.
doi: 10.1016/j.ic.2005.02.003.
[ BibTex | DOI | Web page | PS | PDF ]

[S⁺05]

Ph. Schnoebelen et al. ACI Sécurité Informatique PERSÉE --- Rapport à mi-parcours, November 2005. 8 pages.
[ BibTex ]

[DKK05]

S. Delaune, F. Klay, and S. Kremer. Spécification du protocole de vote électronique. Technical Report 6, projet RNTL PROUVÉ, November 2005. 19 pages.
[ BibTex | Web page | PS | PDF ]

[Tre05]

R. Treinen. Résolution symbolique de contraintes. Mémoire d'habilitation, Université Paris-Sud 11, Orsay, France, November 2005.
[ BibTex | Web page | PS | PDF ]

[FL05]

A. Finkel and J. Leroux. The Convex Hull of a Regular Set of Integer Vectors is Polyhedral and Effectively Computable. Information Processing Letters, 96(1):30--35, October 2005.
doi: 10.1016/j.ipl.2005.04.004.
[ BibTex | DOI | Web page | PS | PDF ]

[BFLS05]

S. Bardin, A. Finkel, J. Leroux, and Ph. Schnoebelen. Flat acceleration in symbolic model checking. In Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA'05), volume 3707 of Lecture Notes in Computer Science, pages 474--488, Taipei, Taiwan, October 2005. Springer.
doi: 10.1007/11562948_35.
[ BibTex | DOI | Web page | PS | PDF ]

[BH05]

M. Bidoit and R. Hennicker. Externalized and Internalized Notions of Behavioral Refinement. In Proceedings of the 2nd International Colloquium on Theoretical Aspects of Computing (ICTAC'05), volume 3722 of Lecture Notes in Computer Science, pages 334--350, Hanoi, Vietnam, October 2005. Springer.
doi: 10.1007/11560647_22.
[ BibTex | DOI | Web page | PDF ]

[AMRT05]

K. Altisen, N. Markey, P.-A. Reynier, and S. Tripakis. Implémentabilité des automates temporisés. In Actes du 5ème Colloque sur la Modélisation des Systèmes Réactifs (MSR'05), pages 395--406, Autrans, France, October 2005. Hermès.
[ BibTex | Web page | PS | PDF ]

[BCKT05]

P. Bouyer, F. Chevalier, M. Krichen, and S. Tripakis. Observation partielle des systèmes temporisés. In Actes du 5ème Colloque sur la Modélisation des Systèmes Réactifs (MSR'05), pages 381--393, Autrans, France, October 2005. Hermès.
[ BibTex | Web page | PS | PDF ]

[ABC⁺05]

K. Altisen, P. Bouyer, T. Cachat, F. Cassez, and G. Gardey. Introduction au contrôle des systèmes temps-réel. In Actes du 5ème Colloque sur la Modélisation des Systèmes Réactifs (MSR'05), pages 367--380, Autrans, France, October 2005. Hermès.
[ BibTex | Web page | PS | PDF ]

[Dem05b]

S. Demri. A reduction from DLP to PDL. Journal of Logic and Computation, 15(5):767--785, October 2005.
doi: 10.1093/logcom/exi043.
[ BibTex | DOI | Web page | PDF ]

[DN05]

S. Demri and D. Nowak. Reasoning about transfinite sequences (extended abstract). In Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA'05), volume 3707 of Lecture Notes in Computer Science, pages 248--262, Taipei, Taiwan, October 2005. Springer.
doi: 10.1007/11562948_20.
[ BibTex | DOI | Web page | PS | PDF ]

[LLT05b]

P. Lafourcade, D. Lugiez, and R. Treinen. Intruder Deduction for the Equational Theory of Exclusive-or with Distributive Encryption. Research Report LSV-05-19, Laboratoire Spécification et Vérification, ENS Cachan, France, October 2005. 39 pages.
[ BibTex | Web page | PS | PDF ]

[Bar05]

S. Bardin. Vers un model checking avec accélération plate de systèmes hétérogènes. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, October 2005.
[ BibTex | Web page | PDF ]

[Zha05]

Y. Zhang. Cryptographic logical relations -- What is the contextual equivalence for cryptographic protocols and how to prove it? Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, October 2005.
[ BibTex | Web page | PS | PDF ]

[BBG⁺05]

H. Bel mokadem, B. Bérard, V. Gourcuff, J.-M. Roussel, and O. De Smet. Verification of a timed multitask system with Uppaal. In Proceedings of the 10th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA'05), pages 347--354, Catania, Italy, September 2005. IEEE Industrial Electronics Society.
[ BibTex | Web page | PS | PDF ]

[DKR05]

S. Delaune, S. Kremer, and M. D. Ryan. Receipt-Freeness: Formal Definition and Fault Attacks (Extended Abstract). In Proceedings of the Workshop Frontiers in Electronic Elections (FEE 2005), Milan, Italy, September 2005.
[ BibTex | Web page | PDF ]

[LNZ05]

S. Lasota, D. Nowak, and Y. Zhang. On completeness of logical relations for monadic types. In Proceedings of the 3rd APPSEM II Workshop (APPSEM'05), Frauenchiemsee, Germany, September 2005.
[ BibTex | Web page | PDF ]

[Pin05]

S. Pinot. Analyse de stabilité d'algorithme distribués probabilistes. Rapport de Master, Master de Logique Mathématique et Fondements de l'Informatique, Paris, France, September 2005.
[ BibTex | Web page | PS | PDF ]

[Szn05]

N. Sznajder. Synthèse de contrôleur pour les systèmes distribués synchrones. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2005.
[ BibTex | Web page | PDF ]

[Bou05e]

P. Bouyer. Optimal Timed Games. Invited talk, 5th International Workshop on Automated Verification of Critical Systems (AVoCS'05), Warwick, UK, September 2005.
[ BibTex ]

[Bou05c]

P. Bouyer. An Introduction to Timed Automata. In Actes de la 4ème École Temps-Réel (ETR'05), pages 111--123, Nancy, France, September 2005.
[ BibTex | Web page | PDF ]

[Bou05b]

P. Bouyer. Foundations of Timed Systems. In Proc. of the ARTIST2 Summer School on Component & Modelling, Testing & Verification, and Statical Analysis of Embedded Systems, Nässlingen, Sweden, September-October 2005.
[ BibTex | Web page | PDF ]

[Bou05a]

F. Bouchy. Bibliothèque de méthodes pour la classification. Rapport de Master, Master Recherche Informatique, Tours, France, September 2005.
[ BibTex ]

[GRV05]

J. Goubault-Larrecq, M. Roger, and K. N. Verma. Abstraction and Resolution Modulo AC: How to Verify Diffie-Hellman-like Protocols Automatically. Journal of Logic and Algebraic Programming, 64(2):219--251, August 2005.
doi: 10.1016/j.jlap.2004.09.004.
[ BibTex | DOI | Web page | PS ]

[BBBL05]

H. Bel mokadem, B. Bérard, P. Bouyer, and F. Laroussinie. A New Modality for Almost Everywhere Properties in Timed Automata. In Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05), volume 3653 of Lecture Notes in Computer Science, pages 110--124, San Francisco, California, USA, August 2005. Springer.
doi: 10.1007/11539452_12.
[ BibTex | DOI | Web page | PS | PDF ]

[BCL05]

P. Bouyer, F. Cassez, and F. Laroussinie. Modal Logics for Timed Control. In Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05), volume 3653 of Lecture Notes in Computer Science, pages 81--94, San Francisco, California, USA, August 2005. Springer.
doi: 10.1007/11539452_10.
[ BibTex | DOI | Web page | PS | PDF ]

[Dem05a]

S. Demri. On the complexity of information logics. Invited talk, Workshop on Logical and Algebraic Foundations of Rough Sets, Regina, Canada, August 2005.
[ BibTex ]

[DG05a]

S. Demri and R. Gascon. Verification of Qualitative Z-Constraints. In Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05), volume 3653 of Lecture Notes in Computer Science, pages 518--532, San Francisco, California, USA, August 2005. Springer.
doi: 10.1007/11539452_39.
[ BibTex | DOI | Web page | PDF ]

[Gou05a]

J. Goubault-Larrecq. Deciding H_1 by Resolution. Information Processing Letters, 95(3):401--408, August 2005.
doi: 10.1016/j.ipl.2005.04.007.
[ BibTex | DOI | Web page | PDF ]

[MKR05]

A. Mukhamedov, S. Kremer, and E. Ritter. Analysis of a Multi-Party Fair Exchange Protocol and Formal Proof of Correctness in the Strand Space Model. In Revised Papers from the 9th International Conference on Financial Cryptography and Data Security (FC'05), volume 3570 of Lecture Notes in Computer Science, pages 255--269, Roseau, The Commonwealth Of Dominica, August 2005. Springer.
doi: 10.1007/11507840_23.
[ BibTex | DOI | Web page | PDF ]

[GK05]

P. Gastin and D. Kuske. Uniform Satisfiability Problem for Local Temporal Logics over Mazurkiewicz Traces. In Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05), volume 3653 of Lecture Notes in Computer Science, pages 533--547, San Francisco, California, USA, August 2005. Springer.
doi: 10.1007/11539452_40.
[ BibTex | DOI | Web page | PS | PDF ]

[BJ05b]

A. Bouhoula and F. Jacquemard. Automatic Verification of Sufficient Completeness for Specifications of Complex Data Structures. Research Report LSV-05-17, Laboratoire Spécification et Vérification, ENS Cachan, France, August 2005. 14 pages.
[ BibTex | Web page | PS | PDF ]

[PR05a]

S. Pinchinat and S. Riedweg. A Decidable Class of Problems for Control under Partial Observation. Information Processing Letters, 95(4):454--465, August 2005.
doi: 10.1016/j.ipl.2005.04.011.
[ BibTex | DOI | Web page | PS | PDF ]

[The05]

The Artist Education Group. Guidelines for a graduate curriculum on embedded software and systems. ACM Transactions in Embedded Computing Systems, 4(3):587--611, August 2005.
doi: 10.1145/1086519.1086526.
[ BibTex | DOI | Web page | PDF ]

[Bou05i]

P. Bouyer. Weighted Timed Automata: Model-Checking and Games. Invited talk, Workshop CORTOS'06, Bonn, Germany, August 2005.
[ BibTex ]

[Bou05d]

P. Bouyer. Optimal Reachability Timed Games. Invited talk, 7th International Workshop on Verification of Infinite State Systems (INFINITY'05), San Francisco, USA, August 2005.
[ BibTex ]

[Bou05f]

P. Bouyer. Partial Observation of Timed Systems. Invited talk, 2nd Workshop on Games in Design and Verification, Edinburgh, Scotland, July 2005.
[ BibTex ]

[BCK05]

M. Baudet, V. Cortier, and S. Kremer. Computationally Sound Implementations of Equational Theories against Passive Adversaries. In Proceedings of the 32nd International Colloquium on Automata, Languages and Programming (ICALP'05), volume 3580 of Lecture Notes in Computer Science, pages 652--663, Lisboa, Portugal, July 2005. Springer.
doi: 10.1007/11523468_53.
[ BibTex | DOI | Web page | PDF ]

[FM05]

L. Fribourg and S. Messika. Brief Announcement: Coupling for Markov Decision Processes --- Application to Self-Stabilization with Arbitrary Schedulers. In Proceedings of the Twenty-Fourth Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC'05), page 322, Las Vegas, Nevada, USA, July 2005. ACM Press.
doi: 10.1145/1073814.1073875.
[ BibTex | DOI | Web page | PS | PDF ]

[DG05b]

M. Droste and P. Gastin. Weighted Automata and Weighted Logics. In Proceedings of the 32nd International Colloquium on Automata, Languages and Programming (ICALP'05), volume 3580 of Lecture Notes in Computer Science, pages 513--525, Lisboa, Portugal, July 2005. Springer.
doi: 10.1007/11523468_42.
[ BibTex | DOI | Web page | PS | PDF ]

[BJ05a]

A. Bouhoula and F. Jacquemard. Automated Induction for Complex Data Structures. Research Report LSV-05-11, Laboratoire Spécification et Vérification, ENS Cachan, France, July 2005. 24 pages.
[ BibTex | Web page | PS | PDF ]

[OG05]

J. Olivain and J. Goubault-Larrecq. The Orchids Intrusion Detection Tool. In Proceedings of the 17th International Conference on Computer Aided Verification (CAV'05), volume 3576 of Lecture Notes in Computer Science, pages 286--290, Edinburgh, Scotland, UK, July 2005. Springer.
doi: 10.1007/11513988_28.
[ BibTex | DOI | Web page | PDF ]

[DdN05]

S. Demri and H. de Nivelle. Deciding Regular Grammar Logics with Converse through First-Order Logic. Journal of Logic, Language and Information, 14(3):289--319, June 2005.
doi: 10.1007/s10849-005-5788-9.
[ BibTex | DOI | Web page | PDF ]

[DLN05]

S. Demri, R. Lazić, and D. Nowak. On the Freeze Quantifier in Constraint LTL: Decidability and Complexity. In Proceedings of the 12th International Symposium on Temporal Representation and Reasoning (TIME'05), pages 113--121, Burlington, Vermont, USA, June 2005. IEEE Computer Society Press.
doi: 10.1109/TIME.2005.28.
[ BibTex | DOI | Web page | PS | PDF ]

[BHS⁺05]

S. Bardin, F. Herbreteau, M. Sighireanu, G. Sutre, and A. Vincent. Intégration des outils PERSÉE (Proposition d'architecture). Délivrable 3.1 --- Partie 1 du Projet PERSÉE de l'ACI Sécurité Informatique, June 2005. 35 pages.
[ BibTex | Web page | PDF ]

[PR05c]

S. Pinchinat and S. Riedweg. You Can Always Compute Maximally Permissive Controllers Under Partial Observation When They Exist. In Proceedings of the 24th American Control Conference (ACC'05), pages 2287--2292, Portland, Oregon, USA, June 2005. IEEECSP.
[ BibTex | Web page | PS | PDF ]

[DFH⁺05]

M. Duflot, L. Fribourg, Th. Hérault, R. Lassaigne, F. Magniette, S. Messika, S. Peyronnet, and C. Picaronny. Probabilistic Model Checking of the CSMA/CD Protocol Using PRISM and APMC. In Proceedings of the 4th International Workshop on Automated Verification of Critical Systems (AVoCS'04), volume 128 of Electronic Notes in Theoretical Computer Science, pages 195--214, London, UK, May 2005. Elsevier Science Publishers.
doi: 10.1016/j.entcs.2005.04.012.
[ BibTex | DOI | Web page | PDF ]

[DFV05]

Ch. Darlot, A. Finkel, and L. Van Begin. About Fast and TReX Accelerations. In Proceedings of the 4th International Workshop on Automated Verification of Critical Systems (AVoCS'04), volume 128 of Electronic Notes in Theoretical Computer Science, pages 87--103, London, UK, May 2005. Elsevier Science Publishers.
doi: 10.1016/j.entcs.2005.04.006.
[ BibTex | DOI | Web page | PDF ]

[KR05a]

S. Kremer and M. D. Ryan. Analysing the Vulnerability of Protocols to Produce Known-pair and Chosen-text Attacks. In Proceedings of the 2nd International Workshop on Security Issues in Coordination Models, Languages and Systems (SecCo'04), volume 128 of Electronic Notes in Theoretical Computer Science, pages 84--107, London, UK, May 2005. Elsevier Science Publishers.
doi: 10.1016/j.entcs.2004.11.043.
[ BibTex | DOI | Web page | PDF ]

[BC05a]

M. Baclet and R. Chevallier. Timed Verification of the SPSMALL Memory. In Proceedings of the 1st International Conference on Memory Technology and Design (ICMTD'05), pages 89--92, Giens, France, May 2005.
[ BibTex | Web page | PDF ]

[FGRV05b]

A. Finkel, G. Geeraerts, J.-F. Raskin, and L. Van Begin. On the Omega-Language Expressive Power of Extended Petri Nets. In Proceedings of the 11th International Workshop on Expressiveness in Concurrency (EXPRESS'04), volume 128 of Electronic Notes in Theoretical Computer Science, pages 87--101, London, UK, April 2005. Elsevier Science Publishers.
doi: 10.1016/j.entcs.2004.11.030.
[ BibTex | DOI | Web page | PDF ]

[Gou05b]

J. Goubault-Larrecq. Extensions of Valuations. Mathematical Structures in Computer Science, 15(2):271--297, April 2005.
doi: 10.1017/S096012950400461X.
[ BibTex | DOI | Web page | PS ]

[BCD05]

P. Bouyer, F. Chevalier, and D. D'Souza. Fault Diagnosis Using Timed Automata. In Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'05), volume 3441 of Lecture Notes in Computer Science, pages 219--233, Edinburgh, Scotland, UK, April 2005. Springer.
doi: 10.1007/b106850.
[ BibTex | DOI | Web page | PS | PDF ]

[CD05]

H. Comon-Lundh and S. Delaune. The finite variant property: How to get rid of some algebraic properties. In Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA'05), volume 3467 of Lecture Notes in Computer Science, pages 294--307, Nara, Japan, April 2005. Springer.
doi: 10.1007/b135673.
[ BibTex | DOI | Web page | PS | PDF ]

[B⁺05]

P. Bouyer et al. ACI Sécurité Informatique CORTOS << Control and Observation of Real-Time Open Systems >> --- Rapport à mi-parcours, April 2005. 6 pages.
[ BibTex | Web page | PDF ]

[KR05b]

S. Kremer and M. D. Ryan. Analysis of an Electronic Voting Protocol in the Applied Pi-Calculus. In Programming Languages and Systems --- Proceedings of the 14th European Symposium on Programming (ESOP'05), volume 3444 of Lecture Notes in Computer Science, pages 186--200, Edinburgh, Scotland, UK, April 2005. Springer.
doi: 10.1007/b107380.
[ BibTex | DOI | Web page | PS | PDF ]

[LLT05a]

P. Lafourcade, D. Lugiez, and R. Treinen. Intruder Deduction for AC-like Equational Theories with Homomorphisms. In Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA'05), volume 3467 of Lecture Notes in Computer Science, pages 308--322, Nara, Japan, April 2005. Springer.
doi: 10.1007/b135673.
[ BibTex | DOI | Web page | PS | PDF ]

[LS05a]

F. Laroussinie and J. Sproston. Model Checking Durational Probabilistic Systems. In Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'05), volume 3441 of Lecture Notes in Computer Science, pages 140--154, Edinburgh, Scotland, UK, April 2005. Springer.
doi: 10.1007/b106850.
[ BibTex | DOI | Web page | PS | PDF ]

[Bou05h]

P. Bouyer. Timed Automata and Extensions: Decidability Limits. Invited talk, 5èmes Journées Systèmes Infinis (JSI'05), Cachan, France, March 2005.
[ BibTex ]

[Bou05g]

P. Bouyer. Synthesis of Timed Systems. Invited lecture, Spring School on Infinite Games and Their Applications, Bonn, Germany, March 2005.
[ BibTex ]

[BDKV05]

L. Bozga, S. Delaune, F. Klay, and L. Vigneron. Retour d'expérience sur la validation du porte-monnaie électronique. Technical Report 5, projet RNTL PROUVÉ, March 2005. 29 pages.
[ BibTex | Web page | PS ]

[BCFL05]

P. Bouyer, F. Cassez, E. Fleury, and K. G. Larsen. Synthesis of Optimal Strategies Using HyTech. In Proceedings of the Workshop on Games in Design and Verification (GDV'04), volume 119 of Electronic Notes in Theoretical Computer Science, pages 11--31, Boston, Massachusetts, USA, February 2005. Elsevier Science Publishers.
doi: 10.1016/j.entcs.2004.07.006.
[ BibTex | DOI | Web page | PS | PDF ]

[CC05]

H. Comon and V. Cortier. Tree Automata with One Memory, Set Constraints and Cryptographic Protocols. Theoretical Computer Science, 331(1):143--214, February 2005.
doi: 10.1016/j.tcs.2004.09.036.
[ BibTex | DOI | Web page | PS ]

[Cou05]

J.-M. Couvreur. A BDD-like Implementation of an Automata Package. In Revised Selected Papers of the 9th International Conference on Implementation and Application of Automata (CIAA'04), volume 3317 of Lecture Notes in Computer Science, pages 310--311, Kingston, Ontario, Canada, January 2005. Springer.
doi: 10.1007/b105090.
[ BibTex | DOI ]

[BS05]

B. Bouyssonouse and J. Sifakis, editors. Embedded Systems Design: The ARTIST Roadmap for Research and Development, volume 3436 of Lecture Notes in Computer Science. Springer, 2005.
doi: 10.1007/b106761.
[ BibTex | DOI | Web page ]

[GP05]

J. Goubault-Larrecq and F. Parrennes. Cryptographic Protocol Analysis on Real C Code. In Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), volume 3385 of Lecture Notes in Computer Science, pages 363--379, Paris, France, January 2005. Springer.
doi: 10.1007/b105073.
[ BibTex | DOI | Web page | PDF ]

[FGRV05a]

A. Finkel, G. Geeraerts, J.-F. Raskin, and L. Van Begin. A counter-example the the minimal coverability tree algorithm. Technical Report 535, Université Libre de Bruxelles, Belgium, 2005.
[ BibTex | Web page | PDF ]

[BC05b]

P. Bouyer and F. Chevalier. On Conciseness of Extensions of Timed Automata. Journal of Automata, Languages and Combinatorics, 10(4):393--405, 2005.
[ BibTex | Web page | PS | PDF ]

[Dem05c]

S. Demri. Temporal logics, 2005. Course notes, Master Parisien de Recherche en Informatique, Paris, France.
[ BibTex | Web page | PDF ]

This file was generated by bibtex2html 1.98.