Bibliography

AB01

E. Asarin and A. Bouajjani.
Perturbed Turing Machines and Hybrid Systems.
In Proc. 6th IEEE Symp. on Logic in Computer Science (LICS'01), Boston (MA), USA, June 2001. IEEE.
gzipped Postscript, Postscript

ABB01

P. Abdulla, L. Boasson, and A. Bouajjani.
Effective Lossy Queue Languages.
In Proc. 28th Intern. Coll. on Automata, Languages and Programming (ICALP'01), Crete, Greece, July 2001. Lecture Notes in Computer Science 2076, Springer-Verlag.
gzipped Postscript, Postscript

ABLS01

A. Annichini, A. Bouajjani, Y. Lakhnech, and M. Sighireanu.
Analysis of Fair Extended Automata.
In Proc. 8th Intern. Static Analysis Symposium (SAS'01), Paris, France, July 2001. Lecture Notes in Computer Science 2126, Springer-Verlag.
gzipped Postscript, Postscript

ABS01

A. Annichini, A. Bouajjani, and M. Sighireanu.
TReX: A Tool for Reachability Analysis of Complex Systems.
In Proc. 13th Intern. Conf. on Computer Aided Verification (CAV'01), Paris, France, July 2001. Lecture Notes in Computer Science 2102, Springer-Verlag.
gzipped Postscript, Postscript

AJ01a

Parosh Aziz Abdulla and Bengt Jonsson.
Channel representations in protocol verification.
In Proc. CONCUR 2001, 12th Int. Conf. on Concurrency Theory, volume 2154 of Lecture Notes in Computer Science, pages 1-15, 2001.
gzipped Postscript, Postscript

AJ01b

Parosh Aziz Abdulla and Bengt Jonsson.
Ensuring completeness of symbolic verification methods for infinite-state systems.
Theoretical Computer Science, 256:145-167, 2001.
gzipped Postscript, Postscript

AJ01c

Parosh Aziz Abdulla and Bengt Jonsson.
Model checking of systems with many identical timed processes, 2001.
To appear in the journal of Theoretical Computer Science.
gzipped Postscript, Postscript

AN01

Parosh Aziz Abdulla and Aletta Nylén.
Timed Petri nets and BQOs.
In Proc. ICATPN'2001: 22nd Int. Conf. on application and theory of Petri nets, volume 2075 of Lecture Notes in Computer Science, pages 53 -70, 2001.
gzipped Postscript, Postscript

APR+01

T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. Zuck.
Parameterized verification with automatically computed inductive assertions.
In CAV'01, pages 221-234, 2001.
gzipped Postscript, Postscript

BFG01

M. Bozga, J-Cl. Fernandez, and L. Ghirvu.
Using static analysis to improve automated test generation.
Software Tools for Tehnology Transfer, 2001.
submitted.
gzipped Postscript, Postscript

BGM01

M. Bozga, S. Graf, and L. Mounier.
Automated validation of distributed software using the IF environment.
In Proceedings of Software Model Checking Workshop, Electronic Notes in Theoretical Computer Science, Paris, France, July 2001.
gzipped Postscript, Postscript

BHM01

A. Bouajjani, P. Habermehl, and R. Mayr.
Automatic Verification of Recursive Procedures with one Integer Parameter.
In Proc. 26th Intern. Symp. on Mathematical Foundations of Computer Science (MFCS 2001), Marianske Lazne, Czech Republic, August 2001. Lecture Notes in Computer Science, Springer-Verlag.
gzipped Postscript, Postscript

BJW01

B. Boigelot, S. Jodogne, and P. Wolper.
On the use of weak automata for deciding linear arithmetic with integer and real variables.
In Proceedings of IJCAR '01, number 2083 in LNAI, pages 611-625, 2001.
gzipped Postscript, Postscript

BL01

B. Boigelot and L. Latour.
Counting the solutions of Presburger equations without enumerating them.
In Proceedings of CIAA '01, LNCS, 2001.
To appear.
gzipped Postscript, Postscript

BLS01

K. Baukus, Y. Lakhnech, and K. Stahl.
Verification of parameterized networks.
Journal of Universal Computer Science, 7(2), 2001.
gzipped Postscript, Postscript

BMT01

A. Bouajjani, A. Muscholl, and T. Touili.
Permutation Rewriting and Algorithmic Verification.
In Proc. 16th Symp. on Logic in Computer Science (LICS'01), Boston (MA), USA, 2001. IEEE.
gzipped Postscript, Postscript

Bou01

A. Bouajjani.
Languages, Rewriting systems, and Verification of Infinte-State Systems.
In Proc. 28th Intern. Coll. on Automata, Languages and Programming (ICALP'01), Crete, Greece, July 2001. Lecture Notes in Computer Science 2076, Springer-Verlag.
invited paper
gzipped Postscript, Postscript

BSBL01

K. Baukus, K. Stahl, S. Bensalem, and Y. Lakhnech.
Networks of processes with parameterized state space.
Electonic Notes of Theoretical Computer Science, 50(4), 2001.
Proc. Workshop on Verification of Parametrized Systems (VEPAS'01), Crete, July, 2001.
gzipped Postscript, Postscript

CAS01

A Collomb-Annichini and M. Sighireanu.
Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX.
In Proc. Workshop on Real-Time Tools (RT-TOOLS'01), Aalborg, August 2001. Aalborg University.
gzipped Postscript, Postscript

DLS01

D. Dams, Y. Lakhnech, and M. Steffen.
Iterating transducers.
In G. Berry, H. Comon, and A. Finkel, editors, Computer Aided Verification, volume 2102 of LNCS, 2001.
gzipped Postscript, Postscript

EKS01

J. Esparza, A. Kucera, and Stefan Schwoon.
Model-checking LTL with regular valuations for pushdown systems.
In Proceedings of TACS '01, LNCS, 2001.
To appear.
gzipped Postscript, Postscript

ES01a

J. Esparza and C. Schröter.
Net reductions for LTL model-checking.
In Proceedings of CHARME '01, 2001.
To appear.
gzipped Postscript, Postscript

ES01b

J. Esparza and C. Schröter.
Unfolding based algorithms for the reachability problem.
Fundamenta Informaticae, (34), 2001.
To appear.
gzipped Postscript, Postscript

ES01c

J. Esparza and S. Schwoon.
A BDD-based model checker for recursive programs.
In Proceedings of CAV '01, number 2102 in LNCS, pages 324-336, 2001.
gzipped Postscript, Postscript

FP01

Dana Fisman and Amir Pnueli.
Beyond regular model checking.
In Proc. 21th Conference on the Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, December 2001.
To appear.
gzipped Postscript, Postscript

GJ01

S. Graf and G. Jia.
Verification experiments on the Mascara protocol.
In Proceedings of the SPIN'01 Workshop, 2001.
to appear.
gzipped Postscript, Postscript

KMM+01

Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar.
Symbolic model checking with rich assertional languages.
Theoretical Computer Science, 256:93-112, 2001.
gzipped Postscript, Postscript

LAS

The Liège Automata-based Symbolic Handler (LASH).

LBOB01

Y. Lakhnech, S. Bensalem, S. Owre, and S. Berezin.
Incremental verification by abstraction.
In TACAS 2001, volume 2031 of LNCS, 2001.
gzipped Postscript, Postscript

Mai01

M. Maidl.
A unifying model checking approach for safety properties of parameterized systems.
In CAV'01, pages 324-336, 2001.
gzipped Postscript, Postscript

PRZ01

A. Pnueli, S. Ruah, and L. Zuck.
Automatic deductive verification with invisible invariants.
In TACAS'01, volume 2031, pages 82-97, 2001.
gzipped Postscript, Postscript

Tou01

T. Touili.
Regular Model Checking using Widening Techniques.
Electronic Notes in Theoretical Computer Science, 50(4), 2001.
Proc. Workshop on Verification of Parametrized Systems (VEPAS'01), Crete, July, 2001.
gzipped Postscript, Postscript

VER01

VERIMAG.
The Language IF-2.0.
Technical report, University of Grenoble, September 2001.
Internal tech. report. Verimag. Deliverable 3 of project Advance.
gzipped Postscript, Postscript

VR01

VERIMAG and France-Telecom R&D.
Modeling PGM with IF-2.0.
Technical report, University of Grenoble, September 2001.
Internal tech. report. Verimag.
gzipped Postscript, Postscript