Publications : 2000
-
[VGPA00]
-
K. N. Verma, J. Goubault-Larrecq, S. Prasad, and
S. Arun-Kumar.
Reflecting BDDs in Coq.
In Proceedings of the 6th Asian Computing Science
Conference (ASIAN 2000), volume 1961 of Lecture Notes in Computer
Science, pages 162--181, Penang, Malaysia, November 2000. Springer.
[ BibTex |
Web page |
PS ]
-
[BJL00]
-
A. Boisseau, F. Jacquemard, and D. Le Métayer.
Exemple de modélisation de protocoles cryptographiques.
Projet EVA, note interne, November 2000.
[ BibTex ]
-
[NDF00]
-
U. Nilsson, M. Duflot, and L. Fribourg.
STABILO, a tool computing inevitable configurations in
distributed protocols, November 2000.
See description in [?]. Written in PROLOG (about
500 lines on top of Gertjan van Noord's finite automata package).
[ BibTex ]
-
[Gou00a]
-
J. Goubault-Larrecq.
Analyse de protocoles cryptographiques.
Invited lecture, Journées ASPROM, Paris, France, October 2000.
[ BibTex ]
-
[Sut00]
-
G. Sutre.
Abstraction et accélération de systèmes infinis.
Thèse de doctorat, Laboratoire Spécification et
Vérification, ENS Cachan, France, October 2000.
[ BibTex |
Web page |
PS ]
-
[DCR+00]
-
O. De Smet, S. Couffin, O. Rossi, G. Canet, J.-J. Lesage,
Ph. Schnoebelen, and H. Papini.
Safe Programming of PLC Using Formal Verification Methods.
In Proceedings of the 4th International PLCopen Conference on
Industrial Control Programming (ICP 2000), pages 73--78, Utrecht, The
Netherlands, October 2000. PLCopen.
[ BibTex |
Web page |
PS ]
-
[CCL+00]
-
G. Canet, S. Couffin, J.-J. Lesage, A. Petit, and
Ph. Schnoebelen.
Towards the Automatic Verification of PLC Programs Written in
Instruction List.
In Proceedings of the IEEE International Conference on
Systems, Man and Cybernetics (SMC 2000), pages 2449--2454, Nashville,
Tennessee, USA, October 2000. Argos Press.
doi:
10.1109/ICSMC.2000.884359.
[ BibTex |
DOI |
Web page |
PS ]
-
[Fri00c]
-
L. Fribourg.
Petri Nets, Flat Languages and Linear Arithmetic.
In Proceedings of the 9th International Workshop on
Functional and Logic Programming (WFLP 2000), pages 344--365,
Benicassim, Spain, September 2000. Universidad Politécnica de Valencia,
Spain.
Invited lecture.
[ BibTex |
Web page |
PS ]
-
[Boi00]
-
A. Boisseau.
Vérification de protocoles cryptographiques.
Rapport de DEA, DEA Programmation, Paris, France, September 2000.
[ BibTex ]
-
[Duf00]
-
M. Duflot.
Configurations récurrentes pour les anneaux de processus ---
Application à l'auto-stabilisation.
Rapport de DEA, DEA Algorithmique, Paris, France, September 2000.
[ BibTex |
Web page |
PS ]
-
[RS00]
-
O. Rossi and Ph. Schnoebelen.
Formal modeling of timed function blocks for the automatic
verification of Ladder Diagram programs.
In Proceedings of the 4th International Conference on
Automation of Mixed Processes: Hybrid Dynamic Systems (ADPM
2000), pages 177--182, Dortmund, Germany, September 2000. Shaker Verlag.
[ BibTex |
Web page |
PS ]
-
[BDFP00b]
-
P. Bouyer, C. Dufourd, E. Fleury, and A. Petit.
Expressiveness of Updatable Timed Automata.
In Proceedings of the 25th International Symposium on
Mathematical Foundations of Computer Science (MFCS 2000), volume
1893 of Lecture Notes in Computer Science, pages 232--242, Bratislava,
Slovakia, August 2000. Springer.
[ BibTex |
Web page |
PS ]
-
[FPS00]
-
A. Finkel, S. Purushothaman Iyer, and G. Sutre.
Well-Abstracted Transition Systems.
In Proceedings of the 11th International Conference on
Concurrency Theory (CONCUR 2000), volume 1877 of Lecture Notes in
Computer Science, pages 566--580, Pennsylvania State University,
Pennsylvania, USA, August 2000. Springer.
[ BibTex |
Web page |
PS ]
-
[FS00a]
-
A. Finkel and G. Sutre.
An Algorithm Constructing the Semilinear Post* for 2-Dim
ResetashTransfer VASS.
In Proceedings of the 25th International Symposium on
Mathematical Foundations of Computer Science (MFCS 2000), volume
1893 of Lecture Notes in Computer Science, pages 353--362, Bratislava,
Slovakia, August 2000. Springer.
[ BibTex |
Web page |
PS ]
-
[CC00]
-
H. Comon and V. Cortier.
Flatness is not a Weakness.
In Proceedings of the 14th International Workshop on Computer
Science Logic (CSL 2000), volume 1862 of Lecture Notes in Computer
Science, pages 262--276, Fischbachau, Germany, August 2000. Springer.
[ BibTex |
Web page |
PS ]
-
[BD00]
-
B. Bérard and C. Dufourd.
Timed Automata and Additive Clock Constraints.
Information Processing Letters, 75(1-2):1--7, July 2000.
[ BibTex |
Web page |
PS ]
-
[CL00]
-
F. Cassez and F. Laroussinie.
Model-Checking for Hybrid Systems by Quotienting and Constraints
Solving.
In Proceedings of the 12th International Conference on
Computer Aided Verification (CAV 2000), volume 1855 of Lecture Notes
in Computer Science, pages 373--388, Chicago, Illinois, USA, July 2000.
Springer.
[ BibTex |
Web page |
PS ]
-
[Pet00]
-
L. Petrucci.
Design and Validation of a Controller.
In Proceedings of the 4th World Multiconference on Systemics,
Cybernetics and Informatics (SCI 2000), pages 684--688, Orlando,
Florida, USA, July 2000.
[ BibTex |
Web page |
PS ]
-
[BDFP00a]
-
P. Bouyer, C. Dufourd, E. Fleury, and A. Petit.
Are Timed Automata Updatable?
In Proceedings of the 12th International Conference on
Computer Aided Verification (CAV 2000), volume 1855 of Lecture Notes
in Computer Science, pages 464--479, Chicago, Illinois, USA, July 2000.
Springer.
[ BibTex |
Web page |
PS ]
-
[CDP+00]
-
G. Canet, B. Denis, A. Petit, O. Rossi, and
Ph. Schnoebelen.
Un cadre pour la vérification automatique de
programmes IL.
In Actes de la 1ère Conférence Internationale
Francophone d'Automatique (CIFA 2000), pages 693--698, Lille, France,
July 2000. Union des Chercheurs Ingénieurs et Scientifiques, Villeneuve
d'Ascq, France.
[ BibTex |
Web page |
PS ]
-
[FL00]
-
A. Finkel and J. Leroux.
A Finite Covering Tree for Analysing Entropic Broadcast
Protocols.
In Proceedings of the International Workshop on Verification
and Computational Logic (VCL 2000), London, UK, July 2000. University
of Southampton, Southampton, UK.
[ BibTex |
Web page |
PS ]
-
[LS00d]
-
D. Lugiez and Ph. Schnoebelen.
Decidable First-Order Transition Logics for PA-Processes.
In Proceedings of the 27th International Colloquium on
Automata, Languages and Programming (ICALP 2000), volume 1853 of
Lecture Notes in Computer Science, pages 342--353, Geneva, Switzerland, July
2000. Springer.
[ BibTex |
Web page |
PS ]
-
[BEF+00]
-
A. Bouajjani, J. Esparza, A. Finkel, O. Maler, P. Rossmanith,
B. Willems, and P. Wolper.
An Efficient Automata Approach to some Problems on Context-Free
Grammars.
Information Processing Letters, 74(5-6):221--227, June 2000.
[ BibTex |
Web page |
PS ]
-
[BP00b]
-
G. Berthelot and L. Petrucci.
Specification and Validation of a Concurrent System: An
Educational Project.
In Proceedings of the Workshop on Practical Use of
High-Level Petri Nets, pages 55--72, Århus, Denmark, June 2000.
[ BibTex |
Web page ]
-
[SS00]
-
Ph. Schnoebelen and N. Sidorova.
Bisimulation and the Reduction of Petri Nets.
In Proceedings of the 21st International Conference on
Applications and Theory of Petri Nets (ICATPN 2000), volume 1825 of
Lecture Notes in Computer Science, pages 409--423, Århus, Denmark, June
2000. Springer.
[ BibTex |
Web page |
PS ]
-
[Pad00]
-
V. Padovani.
Decidability of Fourth-Order Matching.
Mathematical Structures in Computer Science, 10(3):361--372, June
2000.
[ BibTex ]
-
[Mar00]
-
N. Markey.
Complexité de la logique temporelle avec passé.
Rapport de DEA, DEA Algorithmique, Paris, France, June 2000.
[ BibTex ]
-
[Gou00b]
-
J. Goubault-Larrecq.
A Method for Automatic Cryptographic Protocol Verification
(Extended Abstract).
In Proceedings of the Workshops of the 15th International
Parallel and Distributed Processing Symposium, volume 1800 of Lecture
Notes in Computer Science, pages 977--984, Cancun, Mexico, May 2000.
Springer.
[ BibTex |
Web page |
PS ]
-
[CN00]
-
H. Comon and R. Nieuwenhuis.
Inductive Proofs = I-Axiomatization + First-Order
Consistency.
Information and Computation, 159(1-2):151--186, May-June 2000.
[ BibTex |
Web page |
PS ]
-
[BCF+00]
-
B. Bérard, P. Castéran, E. Fleury, L. Fribourg, J.-F.
Monin, Ch. Paulin, A. Petit, and D. Rouillard.
Document de spécification du modèle commun.
Fourniture 1.1 du projet RNRT Calife, April 2000.
[ BibTex ]
-
[LST00]
-
F. Laroussinie, Ph. Schnoebelen, and M. Turuani.
On the Expressivity and Complexity of Quantitative
Branching-Time Temporal Logics.
In Proceedings of the 4th Latin American Symposium on
Theoretical Informatics (LATIN 2000), volume 1776 of Lecture Notes in
Computer Science, pages 437--446, Punta del Este, Uruguay, April 2000.
Springer.
doi:
10.1007/10719839_43.
[ BibTex |
DOI |
Web page |
PS |
PDF ]
-
[BBP00]
-
F. Belala, M. Bettaz, and L. Petrucci-Dauchy.
Concurrent systems analysis using ECATNets.
Logic Journal of the IGPL, 8(2):149--164, March 2000.
doi:
10.1093/jigpal/8.2.149.
[ BibTex |
DOI |
Web page |
PS |
PDF ]
-
[BLS00]
-
B. Bérard, A. Labroue, and Ph. Schnoebelen.
Verifying Performance Equivalence for Timed Basic Parallel
Processes.
In Proceedings of the 3rd International Conference on
Foundations of Software Science and Computation Structures
(FoSSaCS 2000), volume 1784 of Lecture Notes in Computer Science, pages
35--47, Berlin, Germany, March 2000. Springer.
[ BibTex |
Web page |
PS ]
-
[LS00b]
-
F. Laroussinie and Ph. Schnoebelen.
The State-Explosion Problem from Trace to Bisimulation
Equivalence.
In Proceedings of the 3rd International Conference on
Foundations of Software Science and Computation Structures
(FoSSaCS 2000), volume 1784 of Lecture Notes in Computer Science, pages
192--207, Berlin, Germany, March 2000. Springer.
[ BibTex |
Web page |
PS ]
-
[Sch00]
-
Ph. Schnoebelen.
Le problème de l'explosion du nombre d'états.
Invited talk, 8ème Journées Montoises d'Informatique
Théorique (JM 2000), Marne-la-Vallée, France, March 2000.
[ BibTex ]
-
[FS00b]
-
A. Finkel and G. Sutre.
Decidability of Reachability Problems for Classes of Two-Counter
Automata.
In Proceedings of the 17th Annual Symposium on Theoretical
Aspects of Computer Science (STACS 2000), volume 1770 of Lecture
Notes in Computer Science, pages 346--357, Lille, France, February 2000.
Springer.
doi:
10.1007/3-540-46541-3_29.
[ BibTex |
DOI |
Web page |
PS ]
-
[Com00]
-
H. Comon.
Sequentiality, Monadic Second Order Logic and Tree Automata.
Information and Computation, 157(1-2):25--51, February-March 2000.
[ BibTex |
Web page |
PS ]
-
[Wil00]
-
N. Williams.
Application des spécifications algébriques à la
rétro-ingénierie de codes Fortran.
Thèse de doctorat, Laboratoire Spécification et
Vérification, ENS Cachan, France, February 2000.
[ BibTex |
Web page |
PS ]
-
[BP00a]
-
B. Bérard and C. Picaronny.
Accepting Zeno Words: A Way Toward Timed Refinements.
Acta Informatica, 37(1):45--81, 2000.
[ BibTex |
Web page |
PS ]
-
[Fri00b]
-
L. Fribourg.
Document de synthèse sur les techniques d'abstraction.
Fourniture 4.1 du projet RNRT Calife, January 2000.
[ BibTex ]
-
[BFP00]
-
P. Bouyer, E. Fleury, and A. Petit.
Document de synthèse sur les procédures de
vérification des systèmes temps réel : Les automates
temporisés.
Fourniture 4.2 du projet RNRT Calife, January 2000.
[ BibTex ]
-
[Fri00a]
-
L. Fribourg.
Constraint Logic Programming Applied to Model Checking.
In Proceedings of the 9th International Workshop on Logic
Program Synthesis and Transformation (LOPSTR'99), volume 1817 of
Lecture Notes in Computer Science, pages 31--42, Venezia, Italy, 2000.
Springer.
Invited tutorial.
[ BibTex |
Web page |
PS ]
-
[BS00]
-
B. Bérard and L. Sierra.
Comparing Verification with HyTech, Kronos and Uppaal on
the Railroad Crossing Example.
Research Report LSV-00-2, Laboratoire Spécification et
Vérification, ENS Cachan, France, January 2000.
[ BibTex |
Web page |
PS ]
-
[CP00]
-
S. Christensen and L. Petrucci.
Modular Analysis of Petri Nets.
The Computer Journal, 43(3):224--242, 2000.
[ BibTex |
Web page |
PS ]
-
[LS00a]
-
F. Laroussinie and Ph. Schnoebelen.
Specification in CTL+Past for verification in CTL.
Information and Computation, 156(1-2):236--263, January 2000.
doi:
10.1006/inco.1999.2817.
[ BibTex |
DOI |
Web page |
PS ]
-
[LS00c]
-
I. A. Lomazova and Ph. Schnoebelen.
Some Decidability Results for Nested Petri Nets.
In Proceedings of the 3rd International Andrei Ershov
Memorial Conference on Perspectives of System Informatics
(PSI'99), volume 1755 of Lecture Notes in Computer Science, pages 208--220,
Novosibirsk, Russia, 2000. Springer.
[ BibTex |
Web page |
PS ]
-
[Lar00]
-
F. Laroussinie.
HCMC: An Extension of CMC for Hybrid Systems.
Available at http://www.lsv.ens-cachan.fr/~fl/cmcweb.html,
2000.
See [CL00] for description. Written in C++ (about
26000 lines).
[ BibTex |
Web page ]
This file was generated by
bibtex2html 1.98.