Publications : 2004

[Bou04c]

P. Bouyer. Timed Automata --- From Theory to Implementation. Invited tutorial, 6th Winter School on Modelling and Verifying Parallel Processes (MOVEP'04), Brussels, Belgium, December 2004. 27 pages.
[ BibTex ]

[Gas04a]

P. Gastin. Basics of model checking. Invited tutorial, 6th Winter School on Modelling and Verifying Parallel Processes (MOVEP'04), Brussels, Belgium, December 2004.
[ BibTex ]

[BCFL04]

P. Bouyer, F. Cassez, E. Fleury, and K. G. Larsen. Optimal Strategies in Priced Timed Game Automata. In Proceedings of the 24th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'04), volume 3328 of Lecture Notes in Computer Science, pages 148--160, Chennai, India, December 2004. Springer.
[ BibTex | Web page | PS | PDF ]

[Mes04]

S. Messika. Méthodes probabilistes pour la vérification des systèmes distribués. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2004.
[ BibTex | Web page | PDF ]

[BCC⁺04]

V. Bernat, H. Comon-Lundh, V. Cortier, S. Delaune, F. Jacquemard, P. Lafourcade, Y. Lakhnech, and L. Mazaré. Sufficient conditions on properties for an automated verification: theoretical report on the verification of protocols for an extended model of the intruder. Technical Report 4, projet RNTL PROUVÉ, December 2004. 33 pages.
[ BibTex | Web page | PS ]

[GLZ04]

P. Gastin, B. Lerman, and M. Zeitoun. Distributed games with causal memory are decidable for series-parallel systems. In Proceedings of the 24th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'04), volume 3328 of Lecture Notes in Computer Science, pages 275--286, Chennai, India, December 2004. Springer.
[ BibTex | Web page | PS | PDF ]

[DG04]

V. Diekert and P. Gastin. Local temporal logic is expressively complete for cograph dependence alphabets. Information and Computation, 195(1-2):30--52, November 2004.
doi: 10.1016/j.ic.2004.08.001.
[ BibTex | DOI | Web page | PS | PDF ]

[FMP04a]

A. Finkel, P. McKenzie, and C. Picaronny. A Well-Structured Framework for Analysing Petri Net Extensions. Information and Computation, 195(1-2):1--29, November 2004.
doi: 10.1016/j.ic.2004.01.005.
[ BibTex | DOI | Web page | PS ]

[DK04]

S. Delaune and F. Klay. Vérification automatique appliquée à un protocole de commerce électronique. In Actes des 6èmes Journées Doctorales Informatique et Réseau (JDIR'04), pages 260--269, Lannion, France, November 2004.
[ BibTex | Web page | PDF ]

[BF04]

S. Bardin and A. Finkel. Composition of accelerations to verify infinite heterogeneous systems. In Proceedings of the 2nd International Symposium on Automated Technology for Verification and Analysis (ATVA'04), volume 3299 of Lecture Notes in Computer Science, pages 248--262, Taipei, Taiwan, October-November 2004. Springer.
[ BibTex | Web page | PS ]

[FMP04b]

L. Fribourg, S. Messika, and C. Picaronny. Coupling and Self-Stabilization. In Proceedings of the 18th International Symposium on Distributed Computing (DISC'04), volume 3274 of Lecture Notes in Computer Science, pages 201--215, Amsterdam, The Netherlands, October 2004. Springer.
[ BibTex | Web page | PDF ]

[Ler04b]

J. Leroux. Disjunctive Invariants for Numerical Systems. In Proceedings of the 2nd International Symposium on Automated Technology for Verification and Analysis (ATVA'04), volume 3299 of Lecture Notes in Computer Science, pages 93--107, Taipei, Taiwan, October-November 2004. Springer.
[ BibTex | Web page | PS ]

[DJ04a]

S. Delaune and F. Jacquemard. A Decision Procedure for the Verification of Security Protocols with Explicit Destructors. In Proceedings of the 11th ACM Conference on Computer and Communications Security (CCS'04), pages 278--287, Washington, D.C., USA, October 2004. ACM Press.
[ BibTex | Web page | PS ]

[Bou04d]

P. Bouyer. Timed Automata --- From Theory to Implementation. Invited tutorial, 1st International Conference on the Quantitative Evaluation of System (QEST'04), Twente, The Netherlands, September 2004.
[ BibTex ]

[Che04]

F. Chevalier. Détection d'erreurs dans les systèmes temporisés. Rapport de DEA, DEA Algorithmique, Paris, France, September 2004. 59 pages.
[ BibTex | Web page | PS ]

[DDMR04]

M. De Wulf, L. Doyen, N. Markey, and J.-F. Raskin. Robustness and Implementability of Timed Automata. In Proceedings of the Joint Conferences Formal Modelling and Analysis of Timed Systems (FORMATS'04) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'04), volume 3253 of Lecture Notes in Computer Science, pages 118--133, Grenoble, France, September 2004. Springer.
[ BibTex | Web page | PS | PDF ]

[GLNZ04]

J. Goubault-Larrecq, S. Lasota, D. Nowak, and Y. Zhang. Complete Lax Logical Relations for Cryptographic Lambda-Calculi. In Proceedings the 18th International Workshop on Computer Science Logic (CSL'04), volume 3210 of Lecture Notes in Computer Science, pages 400--414, Karpacz, Poland, September 2004. Springer.
[ BibTex | Web page | PS ]

[MS04b]

N. Markey and Ph. Schnoebelen. Symbolic Model Checking for Simply-Timed Systems. In Proceedings of the Joint Conferences Formal Modelling and Analysis of Timed Systems (FORMATS'04) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'04), volume 3253 of Lecture Notes in Computer Science, pages 102--117, Grenoble, France, September 2004. Springer.
[ BibTex | Web page | PS | PDF ]

[MS04c]

N. Markey and Ph. Schnoebelen. TSMV: A Symbolic Model Checker for Quantitative Analysis of Systems. In Proceedings of the 1st International Conference on Quantitative Evaluation of Systems (QEST'04), pages 330--331, Enschede, The Netherlands, September 2004. IEEE Computer Society Press.
doi: 10.1109/QEST.2004.10028.
[ BibTex | DOI | Web page | PS | PDF ]

[Rat04]

B. Ratti. Automates d'arbre d'ordre deux. Rapport de DEA, DEA Programmation, Paris, France, September 2004. 45 pages.
[ BibTex | Web page | PS ]

[Rey04]

P.-A. Reynier. Analyse en avant des automates temporisés. Rapport de DEA, DEA Algorithmique, Paris, France, September 2004. 68 pages.
[ BibTex | Web page | PS ]

[BHKB04]

M. Bidoit, R. Hennicker, A. Knapp, and H. Baumeister. Glass-Box and Black-Box Views on Object-Oriented Specifications. In Proceedings of the 2nd IEEE International Conference on Software Engineering and Formal Methods (SEFM'04), pages 208--217, Beijing, China, September 2004. IEEE Computer Society Press.
doi: 10.1109/SEFM.2004.10014.
[ BibTex | DOI | Web page | PDF ]

[Oli04b]

J. Olivain. Net-entropy v1.0: An entropy checker for ciphered network connections, September 2004.
[ BibTex | Web page ]

[BDFP04]

P. Bouyer, C. Dufourd, E. Fleury, and A. Petit. Updatable Timed Automata. Theoretical Computer Science, 321(2-3):291--345, August 2004.
doi: 10.1016/j.tcs.2004.04.003.
[ BibTex | DOI | Web page | PS | PDF ]

[KS04]

A. Kučera and Ph. Schnoebelen. A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications. In Proceedings of the 15th International Conference on Concurrency Theory (CONCUR'04), volume 3170 of Lecture Notes in Computer Science, pages 372--386, London, UK, August 2004. Springer.
doi: 10.1007/978-3-540-28644-8_24.
[ BibTex | DOI | Web page | PDF ]

[LMS04]

F. Laroussinie, N. Markey, and Ph. Schnoebelen. Model Checking Timed Automata with One or Two Clocks. In Proceedings of the 15th International Conference on Concurrency Theory (CONCUR'04), volume 3170 of Lecture Notes in Computer Science, pages 387--401, London, UK, August 2004. Springer.
doi: 10.1007/978-3-540-28644-8_25.
[ BibTex | DOI | Web page | PS | PDF ]

[LS04]

J. Leroux and G. Sutre. On Flatness for 2-dimensional Vector Addition Systems with States. In Proceedings of the 15th International Conference on Concurrency Theory (CONCUR'04), volume 3170 of Lecture Notes in Computer Science, pages 402--416, London, UK, August 2004. Springer.
doi: 10.1007/978-3-540-28644-8_26.
[ BibTex | DOI | Web page | PS ]

[Ler04a]

J. Leroux. The Affine Hull of a Binary Automaton is Computable in Polynomial Time. In Proceedings of the 5th International Workshop on Verification of Infinite State Systems (INFINITY'03), volume 98 of Electronic Notes in Theoretical Computer Science, pages 89--104, Marseilles, France, August 2004. Elsevier Science Publishers.
[ BibTex | Web page | PS ]

[MR04]

N. Markey and J.-F. Raskin. Model Checking Restricted Sets of Timed Paths. In Proceedings of the 15th International Conference on Concurrency Theory (CONCUR'04), volume 3170 of Lecture Notes in Computer Science, pages 432--447, London, UK, August 2004. Springer.
doi: 10.1007/978-3-540-28644-8_28.
[ BibTex | DOI | Web page | PS | PDF ]

[Sch04a]

Ph. Schnoebelen, editor. Proceedings of the 5th International Workshop on Verification of Infinite State Systems (INFINITY'03), volume 98 of Electronic Notes in Theoretical Computer Science, Marseilles, France, August 2004. Elsevier Science Publishers.
doi: 10.1016/j.entcs.2003.10.001.
[ BibTex | DOI ]

[Tre04a]

R. Treinen. The PROUVÉ Specification Language. Technical Report 3, Projet RNTL PROUVÉ, August 2004. 10 pages.
[ BibTex | Web page | PS ]

[BBP04]

B. Bérard, P. Bouyer, and A. Petit. Analysing the PGM Protocol with Uppaal. International Journal of Production Research, 42(14):2773--2791, July 2004.
[ BibTex | Web page | PS | PDF ]

[FL04a]

A. Finkel and J. Leroux. Image Computation in Infinite State Model Checking. In Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04), volume 3114 of Lecture Notes in Computer Science, pages 361--371, Boston, Massachusetts, USA, July 2004. Springer.
[ BibTex | Web page | PS ]

[BH04]

M. Bidoit and R. Hennicker. Glass Box and Black Box Views of State-Based System Specifications. In Proceedings of the 10th International Conference on Algebraic Methodology and Software Technology (AMAST'04), volume 3116 of Lecture Notes in Computer Science, page 19, Stirling, UK, July 2004. Springer. Invited talk.
[ BibTex ]

[BJ04]

A. Bouhoula and F. Jacquemard. Constrained Tree Grammars to Pilot Automated Proof by Induction. In Proceedings of the 5th Workshop on Strategies in Automated Deduction (STRATEGIES'04), pages 64--78, Cork, Ireland, July 2004.
[ BibTex | Web page | PDF ]

[Oli04a]

J. Olivain. EVTGEN v1.0: A Programmable Generic Generator of Event Sequences, July 2004. Written in C (about 5000 lines).
[ BibTex | Web page ]

[Cou04]

J.-M. Couvreur. Contribution à l'algorithmique de la vérification. Mémoire d'habilitation, Université de Bordeaux I, Bordeaux, France, July 2004.
[ BibTex | Web page | PDF ]

[Rob04]

A. Robin. Aux frontières de la décidabilité... Rapport de DEA, DEA Algorithmique, Paris, France, July 2004. 33 pages.
[ BibTex | Web page | PS ]

[Hug04]

Th. Hugel. SSP: Stochastic Shortest Paths, July 2004. Written in Caml (about 500 lines).
[ BibTex ]

[DFH⁺04]

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. Contract Report (Lot 4.2 fourniture 2), projet RNTL Averroes, June 2004. 22 pages.
[ BibTex | Web page | PS ]

[Bau04]

M. Baudet. Random Polynomial-Time Attacks and Dolev-Yao Models. In Proceedings of the Workshop on Security of Systems: Formalism and Tools (SASYFT'04), Orléans, France, June 2004.
[ BibTex | Web page | PS | PDF ]

[BBD04]

M. Ben Gaid, B. Bérard, and O. De Smet. Modélisation et vérification d'un évaporateur en Uppaal. In Actes du 6ème Atelier sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'04), pages 223--238, Besançon, France, June 2004.
[ BibTex | Web page | PS | PDF ]

[BDF04a]

S. Bardin, Ch. Darlot, and A. Finkel. FAST: un model-checker pour systèmes à compteurs. In Actes du 6ème Atelier sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'04), pages 377--380, Besançon, France, June 2004.
[ BibTex | Web page | PS ]

[BP04a]

S. Bardin and L. Petrucci. COAST: des réseaux de Petri à la planification assistée. In Actes du 6ème Atelier sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'04), pages 285--298, Besançon, France, June 2004.
[ BibTex | Web page | PS ]

[BP04b]

S. Bardin and L. Petrucci. From PNML to Counter Systems for Accelerating Petri Nets with FAST. In Proceedings of the Workshop on Interchange Format for Petri Nets, pages 26--40, Bologna, Italy, June 2004.
[ BibTex | Web page | PS ]

[BDF⁺04b]

S. Bardin, Ch. Darlot, A. Finkel, J. Leroux, and L. Van Begin. FAST v1.5: Fast Acceleration of Symbolic Transition Systems. Available at http://www.lsv.ens-cachan.fr/fast/, June 2004.
[ BibTex | Web page ]

[FMP04c]

L. Fribourg, S. Messika, and C. Picaronny. Mixing Time of the Asymmetric Simple Exclusion Problem on a Ring with Two Particles. Research Report LSV-04-12, Laboratoire Spécification et Vérification, ENS Cachan, France, June 2004. 15 pages.
[ BibTex | Web page | PS ]

[Mar04b]

N. Markey. TSMV: model-checking symbolique de systèmes simplement temporisés. In Actes du 6ème Atelier sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'04), pages 349--352, Besançon, France, June 2004.
[ BibTex | Web page | PS | PDF ]

[BDKT04]

L. Bozga, S. Delaune, F. Klay, and R. Treinen. Spécification du protocole de porte-monnaie électronique. Technical Report 1, projet RNTL PROUVÉ, June 2004. 12 pages.
[ BibTex | Web page | PS ]

[CDL04]

V. Cortier, S. Delaune, and P. Lafourcade. A Survey of Algebraic Properties Used in Cryptographic Protocols. Technical Report 2, projet RNTL PROUVÉ, June 2004. 19 pages.
[ BibTex | Web page | PS ]

[BCG⁺04]

F. Bréant, J.-M. Couvreur, F. Gilliers, F. Kordon, I. Mounier, E. Paviot-Adet, D. Poitrenaud, D. M. Regep, and G. Sutre. Modeling and Verifying Behavioral Aspects. In Formal Methods for Embedded Distributed Systems: How to Master the Complexity, chapter 6, pages 171--211. Kluwer Academic Publishers, June 2004.
[ BibTex ]

[DJ04b]

S. Delaune and F. Jacquemard. A Theory of Dictionary Attacks and its Complexity. In Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW'04), pages 2--15, Asilomar, Pacific Grove, California, USA, June 2004. IEEE Computer Society Press.
[ BibTex | Web page | PS ]

[MJ04]

O. Michel and F. Jacquemard. An Analysis of the Needham-Schroeder Public-Key Protocol with MGS. In Proceedings of the 5th Workshop on Membrane Computing (WMC'04), pages 295--315, Milano, Italy, June 2004.
[ BibTex | Web page | PDF ]

[BPP04]

M. Baclet, R. Pacalet, and A. Petit. Register Transfer Level Simulation. Research Report LSV-04-10, Laboratoire Spécification et Vérification, ENS Cachan, France, May 2004. 15 pages.
[ BibTex | Web page | PS ]

[BC04a]

M. Baclet and R. Chevallier. Using UPPAAL to Verify an On-Chip Memory. Research Report LSV-04-11, Laboratoire Spécification et Vérification, ENS Cachan, France, May 2004. 12 pages.
[ BibTex | Web page | PS ]

[BC04b]

M. Baclet and R. Chevallier. Using UPPAAL to verify an on-chip memory. Contract Report (Work Package 3.2 Fourniture 1), projet T126 MEDEA+ Blueberries, May 2004. 12 pages.
[ BibTex | Web page | PS ]

[Bou04b]

P. Bouyer. Forward Analysis of Updatable Timed Automata. Formal Methods in System Design, 24(3):281--320, May 2004.
doi: 10.1023/B:FORM.0000026093.21513.31.
[ BibTex | DOI | Web page | PS | PDF ]

[Now04]

D. Nowak. Logical Relations for Monadic Types. Invited talk, International Workshop on Formal Methods and Security (IWFMS'04), Nanjing, China, May 2004.
[ BibTex ]

[Mar04a]

N. Markey. Past is for Free: On the Complexity of Verifying Linear Temporal Properties with Past. Acta Informatica, 40(6-7):431--458, May 2004.
doi: 10.1007/s00236-003-0136-5.
[ BibTex | DOI | Web page | PS | PDF ]

[Bou04e]

P. Bouyer. Timed Models for Concurrent Systems. Invited lecture, 32nd Spring School on Theoretical Computer Science (Concurrency Theory), Luminy, France, April 2004.
[ BibTex ]

[Gas04b]

P. Gastin. Specifications for distributed systems. Invited lecture, 32nd Spring School on Theoretical Computer Science (Concurrency Theory), Luminy, France, April 2004.
[ BibTex ]

[BFN04]

S. Bardin, A. Finkel, and D. Nowak. Toward Symbolic Verification of Programs Handling Pointers. In Proceedings of the 3rd International Workshop on Automated Verification of Infinite-State Systems (AVIS'04), Barcelona, Spain, April 2004.
[ BibTex | Web page | PS ]

[BS04]

N. Bertrand and Ph. Schnoebelen. Verifying Nondeterministic Channel Systems With Probabilistic Message Losses. In Proceedings of the 3rd International Workshop on Automated Verification of Infinite-State Systems (AVIS'04), Barcelona, Spain, April 2004.
[ BibTex | Web page | PDF ]

[FL04b]

A. Finkel and J. Leroux. Polynomial Time Image Computation With Interval-Definable Counters Systems. In Proceedings of the 11th International SPIN Workshop on Model Checking Software (SPIN'04), volume 2989 of Lecture Notes in Computer Science, pages 182--197, Barcelona, Spain, April 2004. Springer.
[ BibTex | Web page | PS ]

[BBL04]

P. Bouyer, E. Brinksma, and K. G. Larsen. Staying Alive As Cheaply As Possible. In Proceedings of the 7th International Conference on Hybrid Systems: Computation and Control (HSCC'04), volume 2993 of Lecture Notes in Computer Science, pages 203--218, Philadelphia, Pennsylvania, USA, March 2004. Springer.
[ BibTex | Web page | PS | PDF ]

[BBLP04]

G. Behrmann, P. Bouyer, K. G. Larsen, and R. Pelánek. Lower and Upper Bounds in Zone Based Abstractions of Timed Automata. In Proceedings of the 10th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'04), volume 2988 of Lecture Notes in Computer Science, pages 312--326, Barcelona, Spain, March 2004. Springer.
[ BibTex | Web page | PS | PDF ]

[BFL04]

S. Bardin, A. Finkel, and J. Leroux. FASTer Acceleration of Counter Automata in Practice. In Proceedings of the 10th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'04), volume 2988 of Lecture Notes in Computer Science, pages 576--590, Barcelona, Spain, March 2004. Springer.
[ BibTex | Web page | PS ]

[CC04]

H. Comon-Lundh and V. Cortier. Security Properties: Two Agents are Sufficient. Science of Computer Programming, 50(1-3):51--71, March 2004.
[ BibTex | Web page | PS ]

[DCMM04]

J. M. Davoren, V. Coulthard, N. Markey, and Th. Moor. Non-deterministic Temporal Logics for General Flow Systems. In Proceedings of the 7th International Conference on Hybrid Systems: Computation and Control (HSCC'04), volume 2993 of Lecture Notes in Computer Science, pages 280--295, Philadelphia, Pennsylvania, USA, March 2004. Springer.
[ BibTex | Web page | PS | PDF ]

[Dem04b]

S. Demri. LTL over Integer Periodicity Constraints. In Proceedings of the 7th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'04), volume 2987 of Lecture Notes in Computer Science, pages 121--135, Barcelona, Spain, March 2004. Springer.
[ BibTex | Web page | PS | PDF ]

[Com04]

H. Comon-Lundh. Intruder Theories (Ongoing Work). In Proceedings of the 7th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'04), volume 2987 of Lecture Notes in Computer Science, pages 1--4, Barcelona, Spain, March 2004. Springer. Invited talk.
[ BibTex ]

[Bou04a]

P. Bouyer. Automates temporisés, de la théorie à l'implémentation. Invited talk, Journées Formalisation des Activit?s Concurrentes (FAC'04), Toulouse, France, March 2004.
[ BibTex ]

[DFP04]

M. Duflot, L. Fribourg, and C. Picaronny. Randomized Dining Philosophers Without Fairness Assumption. Distributed Computing, 17(1):65--76, February 2004.
doi: 10.1007/s00446-003-0102-z.
[ BibTex | DOI | Web page | PS ]

[BM04]

M. Bidoit and P. D. Mosses. CASL User Manual --- Introduction to Using the Common Algebraic Specification Language, volume 2900 of Lecture Notes in Computer Science. Springer, 2004.
doi: 10.1007/b11968.
[ BibTex | DOI | Web page ]

[Sch04b]

Ph. Schnoebelen. The Verification of Probabilistic Lossy Channel Systems. In Validation of Stochastic Systems: A Guide to Current Research, volume 2925 of Lecture Notes in Computer Science, pages 445--465. Springer, 2004.
[ BibTex | Web page | PS | PDF ]

[BST04]

M. Bidoit, D. Sannella, and A. Tarlecki. Toward Component-Oriented Formal Software Development: An Algebraic Approach. In Revised Papers of the 9th International Workshop on Radical Innovations of Software and Systems Engineering in the Future (RISSEF'02), volume 2941 of Lecture Notes in Computer Science, pages 75--90, Venice, Italy, 2004. Springer.
[ BibTex | Web page | PS | PDF ]

[MS04a]

N. Markey and Ph. Schnoebelen. A PTIME-Complete Matching Problem for SLP-Compressed Words. Information Processing Letters, 90(1):3--6, January 2004.
doi: 10.1016/j.ipl.2004.01.002.
[ BibTex | DOI | Web page | PS | PDF ]

[Tre04b]

R. Treinen. RTALOOP: The RTA List of Open Problems. Web site at http://www.lsv.ens-cachan.fr/rtaloop/, started 1997, 2004. Size as of July 2004: 100 problems, 90 pages, 432 references.
[ BibTex | Web page ]

[Dem04a]

S. Demri. Complexité algorithmique de variantes de LTL pour la vérification, 2004. Course notes, DEA Algorithmique, Paris, France.
[ BibTex | Web page | PDF ]

This file was generated by bibtex2html 1.98.