next up previous
Next: About this document ... Up: main Previous: The MASCARA case study

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.

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.

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.

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.

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.

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

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.

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

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.

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.

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.

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

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.

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.

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

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

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.

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

LAS
The Liège Automata-based Symbolic Handler (LASH).
Available at http://www.montefiore.ulg.ac.be/~boigelot/research/lash/.

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

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

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