Publications

[1] T. Touili and M. Sighireanu. Bounded communication reachability analysis of process rewrite systems with ordered parallelism. In Proc. 8th Int. Workshop on Verification of Infinite State Systems (INFINITY 2006), Electronic Notes in Theor. Comp. Sci. Elsevier Science, 2007. To appear.
[ bib | .ps.gz ]
[2] A. Bouajjani, J. Strejcek, and T. Touili. On symbolic verification of weakly extended PAD. In Proc. 13th Int. Workshop on Expressiveness in Concurrency (EXPRESS 2006), Electronic Notes in Theor. Comp. Sci. Elsevier Science, 2007. To appear.
[ bib | .ps.gz ]
[3] Ch. Baier, N. Bertrand, and Ph. Schnoebelen. Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties. ACM Transactions on Computational Logic, 2007. To appear.
[ bib | http ]
[4] M. Adélaïde and G. Sutre. Parametric analysis and abstraction of genetic regulatory networks. In Proc. 2nd Workshop on Concurrent Models in Molecular Biology (BioCONCUR'04), Electronic Notes in Theor. Comp. Sci. Elsevier Science, 2007. To appear.
[ bib | .ps.gz ]
[5] Ch. Baier, N. Bertrand, and Ph. Schnoebelen. On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems. In Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), volume 4246 of Lecture Notes in Artificial Intelligence, pages 347-361. Springer, November 2006.
[ bib | .pdf ]
[6] S. Demri, A. Finkel, V. Goranko, and G. van Drimmelen. Towards a model-checker for counter systems. In Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), volume 4218 of Lecture Notes in Computer Science, pages 493-507. Springer, October 2006.
[ bib | .pdf ]
[7] N. Bertrand. Modèles stochastiques pour les pertes de messages dans les protocoles asynchrones et techniques de vérification automatique. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, September 2006.
[ bib | .pdf ]
[8] Ch. Baier, N. Bertrand, and Ph. Schnoebelen. Symbolic verification of communicating systems with probabilistic message losses: liveness and fairness. In Proceedings of 26th IFIP WG6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'06), volume 4229 of Lecture Notes in Computer Science, pages 212-227. Springer, September 2006.
[ bib | .pdf ]
[9] A. Bouajjani and J. Esparza. Rewriting models of boolean programs. In Proc. 17th Int. Conf. Term Rewriting and Applications (RTA 2006), volume 4098 of Lecture Notes in Computer Science, pages 136-150. Springer, August 2006.
[ bib | .pdf ]
[10] A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with lists are counter automata. In Proc. 18th Int. Conf. Computer Aided Verification (CAV 2006), volume 4144 of Lecture Notes in Computer Science, pages 517-531. Springer, August 2006.
[ bib | .pdf ]
[11] B. Boigelot and F. Herbreteau. The power of hybrid acceleration. In Proc. of the 18th Int. Conf. on Computer Aided Verification (CAV06), volume 4144 of Lecture Notes in Computer Science, pages 438-451. Springer, August 2006.
[ bib | .pdf ]
[12] A. Kucera and Ph. Schnoebelen. A general approach to comparing infinite-state systems with their finite-state specifications. Theoretical Computer Science, 358(2-3):315-333, August 2006.
[ bib | .pdf ]
[13] N. Bertrand and Ph. Schnoebelen. A short visit to the STS hierarchy. In Proceedings of the 12th International Workshop on Expressiveness in Concurrency (EXPRESS 2005), volume 154 of Electronic Notes in Theor. Comp. Sci., pages 59-69. Elsevier Science, July 2006.
[ bib | .pdf ]
[14] A. Finkel, G. Geeraerts, J.-F. Raskin, and L. Van Begin. On the ω-language expressive power of extended Petri nets. Theoretical Computer Science, 356(3):374-386, May 2006.
[ bib | .pdf ]
[15] S. Chaki, E. M. Clarke, N. Kidd, Th. W. Reps, and T. Touili. Verifying concurrent message-passing C programs with recursive calls. In Proc. 12th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2006), volume 3920 of Lecture Notes in Computer Science, pages 334-349. Springer, March 2006.
[ bib | .ps.gz ]
[16] A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar. Abstract regular tree model checking. In Proc. 7th Int. Workshop on Verification of Infinite State Systems (INFINITY 2005), volume 149(1) of Electronic Notes in Theor. Comp. Sci., pages 37-48. Elsevier Science, February 2006.
[ bib | .ps.gz ]
[17] S. Bardin, J. Leroux, and G. Point. FAST Extended Release. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV'06), Seattle, Washington, USA, Aug. 2006, volume 4144 of Lecture Notes in Computer Science, pages 63-66. Springer, 2006.
[ bib ]
[18] T. Touili. Dealing with communication for dynamic multithreaded recursive programs. In Proc. NATO Advanced Research Workshop on Verification of Infinite State Systems with Applications to Security (VISSAS 2005), pages 213-227. IOS Press, 2006.
[ bib | .ps.gz ]
[19] A. Bouajjani. Regular model checking for programs with dynamic memory. In Proc. NATO Advanced Research Workshop on Verification of Infinite State Systems with Applications to Security (VISSAS 2005), pages 17-22. IOS Press, 2006.
[ bib ]
[20] Ch. Baier, N. Bertrand, and Ph. Schnoebelen. A note on the attractor-property of infinite-state Markov chains. Information Processing Letters, 97(2):58-63, January 2006.
[ bib | .pdf ]
[21] A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejcek. Reachability analysis of multithreaded software with asynchronous communication. In Proc. 25th Conf. Found. of Software Technology and Theor. Comp. Sci. (FST&TCS 2005), volume 3821 of Lecture Notes in Computer Science, pages 348-359. Springer, December 2005.
[ bib | .ps.gz ]
[22] J.-M. Couvreur. A BDD-like implementation of an automata package. In Proc. 9th Int. Conf. Implementation and Application of Automata (CIAA'2004), volume 3317 of Lecture Notes in Computer Science, pages 310-311. Springer, December 2005.
[ bib ]
[23] P. Habermehl and T. Vojnar. Regular Model Checking Using Inference of Regular Languages. In Proc. 6th Int. Workshop on Verification of Infinite State Systems (INFINITY 2004), volume 138(3) of Electronic Notes in Theor. Comp. Sci., pages 21-36. Elsevier Science, December 2005.
[ bib | .ps.gz ]
[24] A. Bouajjani, A. Legay, and P. Wolper. Handling Liveness Properties in (ω-)Regular Model Checking. In Proc. 6th Int. Workshop on Verification of Infinite State Systems (INFINITY 2004), volume 138(3) of Electronic Notes in Theor. Comp. Sci., pages 101-115. Elsevier Science, December 2005.
[ bib | .pdf.gz ]
[25] A. Bouajjani, J. Esparza, and T. Touili. Reachability Analysis of Synchronized PA Systems. In Proc. 6th Int. Workshop on Verification of Infinite State Systems (INFINITY 2004), volume 138(3) of Electronic Notes in Theor. Comp. Sci., pages 153-178. Elsevier Science, December 2005.
[ bib | .ps.gz ]
[26] S. Chaki, E. M. Clarke, O. Grumberg, J. Ouaknine, N. Sharygina, T. Touili, and H. Veith. State/event software verification for branching-time specifications. In Proc. 5th Int. Conf. Integrated Formal Methods (IFM 2005), volume 3771 of Lecture Notes in Computer Science, pages 53-69. Springer, November 2005.
[ bib | .ps.gz ]
[27] G. Cécé and A. Finkel. Verification of programs with half-duplex communication. Information and Computation, 202(2):166-190, November 2005.
[ bib | .pdf ]
[28] 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.
[ bib | .pdf ]
[29] D. Lugiez and Ph. Schnoebelen. Decidable first-order transition logics for PA-processes. Information and Computation, 203(1):75-113, November 2005.
[ bib | .pdf ]
[30] K. Barkaoui, J.-M. Couvreur, and K. Klai. On the equivalence between liveness and deadlock-freeness in Petri nets. In Proc. 26th Int. Conf Applications and Theory of Petri Nets, (ICATPN'2005), volume 3536 of Lecture Notes in Computer Science, pages 90-107. Springer, November 2005.
[ bib ]
[31] 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.
[ bib | .pdf ]
[32] 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.
[ bib | .pdf ]
[33] 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. Springer, October 2005.
[ bib | .pdf ]
[34] A. Bouajjani, M. Müller-Olm, and T. Touili. Regular symbolic analysis of dynamic networks of pushdown systems. In Proc. 16th Int. Conf. Concurrency Theory (CONCUR 2005), volume 3653 of Lecture Notes in Computer Science, pages 474-487. Springer, August 2005.
[ bib | .ps.gz ]
[35] J. Leroux. A polynomial time Presburger criterion and synthesis for number decision diagrams. In Proc. 20th IEEE Symp. Logic in Computer Science (LICS 2005), pages 147-156. IEEE Comp. Soc. Press, June 2005.
[ bib | .ps ]
[36] 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 Theor. Comp. Sci., pages 87-103. Elsevier Science, May 2005.
[ bib | .pdf ]
[37] 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. Elsevier Science Publishers, April 2005.
[ bib | .pdf ]
[38] A. Bouajjani and T. Touili. On computing reachability sets of process rewrite systems. In Proc. 16th Int. Conf. Term Rewriting and Applications (RTA 2005), volume 3467 of Lecture Notes in Computer Science, pages 484-499. Springer, April 2005.
[ bib | .ps.gz ]
[39] A. Bouajjani, P. Habermehl, P. Moro, and T. Vojnar. Verifying programs with dynamic 1-selector-linked structures in regular model checking. In Proc. 11th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), volume 3440 of Lecture Notes in Computer Science, pages 13-39, April 2005.
[ bib | .ps.gz ]
[40] J. Leroux. A polynomial-time presburger criterion and synthesis for number decision diagrams. In Proc. 20th Annual IEEE Symposium on Logic in Computer Science (LICS'05), Chicago, USA June 2005, pages 147-156. IEEE Comp. Soc. Press, 2005.
[ bib ]
[41] J. Leroux and G. Sutre. Flat counter automata almost everywhere! In Proc. 3rd Int. Symp. Automated Technology for Verification and Analysis (ATVA'05), Taipei, Taiwan, Oct. 2005, volume 3707 of Lecture Notes in Computer Science, pages 489-503. Springer, 2005.
[ bib ]
[42] A. Bouajjani and A. Meyer. Symbolic Reachability Analysis of Higher-Order Context-Free Processes. In Proc. 24th Conf. Found. of Software Technology and Theor. Comp. Sci. (FST&TCS 2004), volume 3328 of Lecture Notes in Computer Science, pages 135-147. Springer, December 2004.
[ bib | .ps.gz ]
[43] J. Leroux. Disjunctive invariants for numerical systems. In Proc. 2nd Int. Symp. Automated Technology for Verification and Analysis (ATVA 2004), volume 3299 of Lecture Notes in Computer Science, pages 93-107. Springer, November 2004.
[ bib ]
[44] A. Finkel, P. McKenzie, and C. Picaronny. A well-structured framework for analysing Petri nets extensions. Information and Computation, 195(1-2):1-29, November 2004.
[ bib | .ps ]
[45] S. Bardin and A. Finkel. Composition of accelerations to verify infinite heterogeneous systems. In Proc. 2nd Int. Symp. Automated Technology for Verification and Analysis (ATVA 2004), volume 3299 of Lecture Notes in Computer Science, pages 248-262. Springer, October 2004.
[ bib | .ps.gz ]
[46] J. Leroux and G. Sutre. On flatness for 2-dimensional vector addition systems with states. In Proc. 15th Int. Conf. Concurrency Theory (CONCUR 2004), volume 3170 of Lecture Notes in Computer Science, pages 402-416. Springer, August 2004.
[ bib | .ps.gz ]
[47] A. Kucera and Ph. Schnoebelen. A general approach to comparing infinite-state systems with their finite-state specifications. In Proc. 15th Int. Conf. Concurrency Theory (CONCUR 2004), volume 3170 of Lecture Notes in Computer Science, pages 371-386. Springer, August 2004.
[ bib | .pdf ]
[48] 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, August 2004.
[ bib | .ps ]
[49] J. Leroux. The affine hull of a binary automaton is computable in polynomial time. In Proc. 5th Int. Workshop on Verification of Infinite State Systems (INFINITY 2003), volume 98 of Electronic Notes in Theor. Comp. Sci., pages 89-104. Elsevier Science, August 2004.
[ bib | .ps ]
[50] A. Griffault and A. Vincent. The mec 5 model-checker. In Proc. 16th Int. Conf. Computer Aided Verification (CAV 2004), volume 3114 of Lecture Notes in Computer Science, pages 488-491. Springer, July 2004.
[ bib | .ps ]
[51] A. Finkel and J. Leroux. Image computation in infinite state model checking. In Proc. 16th Int. Conf. Computer Aided Verification (CAV 2004), volume 3114 of Lecture Notes in Computer Science, pages 361-371. Springer, July 2004.
[ bib | .ps ]
[52] P. A. Abdulla, A. Collomb-Annichini, A. Bouajjani, and B. Jonsson. Using Forward Reachability Analysis for Verification of Lossy Channel Systems. Formal Methods in System Design, 25(1):39-65, July 2004.
[ bib | .ps.gz ]
[53] A. Bouajjani, P. Habermehl, and T. Vojnar. Abstract Regular Model Checking. In Proc. 16th Int. Conf. Computer Aided Verification (CAV 2004), volume 3114 of Lecture Notes in Computer Science, pages 372-386, July 2004.
[ bib | .ps.gz ]
[54] S. Bardin, Ch. Darlot, and A. Finkel. FAST : un model-checker pour systèmes à compteurs. In J. Julliand, editor, Actes du 6ème atelier Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL 2004), Besançon, France, pages 377-380, June 2004.
[ bib | .ps ]
[55] S. Bardin and L. Petrucci. From PNML to counter systems for accelerating Petri Nets with FAST. In Ekkart Kindler, editor, Proc. Workshop on Interchange Format for Petri Nets, Bologna, Italy, pages 26-40, June 2004.
[ bib | .ps ]
[56] A. Meyer. On term rewriting systems having a rational derivation. In Proc. 7th Int. Conf. Foundations of Software Science and Computation Structures (FOSSACS 2004), volume 2987 of Lecture Notes in Computer Science, pages 378-392. Springer, April 2004.
[ bib | .pdf ]
[57] N. Bertrand and Ph. Schnoebelen. Verifying nondeterministic channel systems with probabilistic message losses. In Ramesh Bharadwaj, editor, Proc. 3rd Int. Workshop on Automated Verification of Infinite-State Systems (AVIS 2004), Barcelona, Spain, April 2004.
[ bib | .pdf ]
[58] S. Bardin, A. Finkel, and D. Nowak. Toward symbolic verification of programs handling pointers. In Ramesh Bharadwaj, editor, Proc. 3rd Int. Workshop on Automated Verification of Infinite-State Systems (AVIS 2004), Barcelona, Spain, April 2004.
[ bib | .ps ]
[59] S. Bardin, A. Finkel, and J. Leroux. FASTer acceleration of counter automata in practice. In Proc. 10th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), volume 2988 of Lecture Notes in Computer Science, pages 576-590. Springer, April 2004.
[ bib | .ps ]
[60] A. Finkel and J. Leroux. Polynomial time image computation with interval-definable counters systems. In Proc. 11th Int. SPIN Workshop on Model Checking Software, volume 2989 of Lecture Notes in Computer Science, pages 182-197. Springer, April 2004.
[ bib | .ps ]
[61] J. Leroux. Disjunctive invariants for numerical systems. In Proc. 2nd Int. Symp. Automated Technology for Verification and Analysis (ATVA'2004), Taipei, Taiwan, Nov. 2004, volume 3299 of Lecture Notes in Computer Science, pages 99-107. Springer, 2004.
[ bib ]
[62] F. Bréant, J.-M. Couvreur, F. Gilliers, F. Kordon, I. Mounier, E. Paviot-Adet, D. Poitrenaud, D. 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, 2004.
[ bib ]
[63] J. Leroux. Algorithmique de la vérification des systèmes à compteurs. Approximation et accélération. Implémentation de l'outil FAST. Thèse ENS de Cachan, December 2003.
[ bib | .ps ]
[64] A. Bouajjani and T. Touili. Reachability Analysis of Process Rewrite Systems. In Proc. 23rd Conf. Found. of Software Technology and Theor. Comp. Sci. (FST&TCS 2003), volume 2914 of Lecture Notes in Computer Science, pages 74-87, December 2003.
[ bib | .ps.gz ]
[65] M. Boyer and M. Sighireanu. Synthesis and Verification of Constraints in the PGM protocol. In Proc. 12th Int. Symposium of Formal Methods Europe (FME '03), volume 2805 of Lecture Notes in Computer Science, pages 264-281. Springer, September 2003.
[ bib ]
[66] A. Bouajjani, J. Esparza, and T. Touili. A Generic Approach to the Static Analysis of Concurrent Programs with Procedures. Int. J. of Foundations Computer Science, 14(4):551-582, August 2003.
[ bib | .ps.gz ]
[67] S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: Fast Acceleration of Symbolic Transition systems. In Proc. 15th Int. Conf. Computer Aided Verification (CAV 2003), volume 2725 of Lecture Notes in Computer Science, pages 118-121. Springer, July 2003.
[ bib | .ps ]
[68] B. Boigelot, F. Herbreteau, and S. Jodogne. Hybrid acceleration using real vector automata. In Proc. 15th Int. Conf. Computer Aided Verification (CAV 2003), volume 2725 of Lecture Notes in Computer Science, pages 193-205. Springer, July 2003.
[ bib | .ps.gz ]
[69] N. Bertrand and Ph. Schnoebelen. Model checking lossy channels systems is probably decidable. In Proc. 6th Int. Conf. Foundations of Software Science and Computation Structures (FOSSACS 2003), volume 2620 of Lecture Notes in Computer Science, pages 120-135. Springer, April 2003.
[ bib | .ps ]
[70] A. Finkel, S. Purushothaman Iyer, and G. Sutre. Well-abstracted transition systems: Application to FIFO automata. Information and Computation, 181(1):1-31, February 2003.
[ bib | .ps ]
[71] A. Bouajjani, P. Habermehl, and R. Mayr. Automatic verification of recursive procedures with one integer parameter. Theoretical Computer Science, 295(1-3):85-106, February 2003.
[ bib | .ps.gz ]
[72] J.-M. Couvreur, E. Encrenaz, E. Paviot-Adet, D. Poitrenaud, and P.-A. Wacrenier. Data decision diagrams for Petri net analysis. In Proc. 23rd Int. Conf. Applications and Theory of Petri Nets, (ICATPN'2002), volume 2360 of Lecture Notes in Computer Science, pages 101-120. Springer, October 2002.
[ bib ]
[73] A. Bouajjani and A. Merceron. Parametric Verification of a Group Membership Algorithm. In Proc. 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02), volume 2469 of Lecture Notes in Computer Science, pages 311-330. Springer, September 2002.
[ bib | .ps.gz ]
[74] A. Bouajjani and T. Touili. Extrapolating Tree Transformations. In Proc. 14th Int. Conf. Computer Aided Verification (CAV 2002), volume 2404 of Lecture Notes in Computer Science, pages 539-554. Springer, July 2002.
[ bib | .ps.gz ]
[75] T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Proc. 29th ACM Symp. Principles of Programming Languages (POPL 2002), pages 58-70. ACM Press, January 2002.
[ bib | .ps.gz ]
[76] T. Touili. Regular model-checking using widening techniques. In Proc. Workshop on Verification of Parametrized Systems (VEPAS'01), volume 50 of Electronic Notes in Theor. Comp. Sci., pages 342-356. Elsevier Science, August 2001.
[ bib ]
[77] A. Bouajjani. Languages, Rewriting systems, and Verification of Infinte-State Systems. In Proc. 28th Int. Coll. Automata, Languages, and Programming (ICALP 2001), volume 2076 of Lecture Notes in Computer Science. Springer, July 2001. invited paper.
[ bib | .ps.gz ]
[78] P.A. Abdulla, L. Boasson, and A. Bouajjani. Effective lossy queue languages. In Proc. 28th Int. Coll. Automata, Languages, and Programming (ICALP 2001), volume 2076 of Lecture Notes in Computer Science, pages 639-651. Springer, July 2001.
[ bib | .ps.gz ]
[79] A Annichini, A. Bouajjani, Y. Lakhnech, and M. Sighireanu. Analysis of Fair Extended Automata. In Proc. 8th Int. Symp. Static Analysis (SAS 2001), volume 2126 of Lecture Notes in Computer Science, pages 335-355. Springer, July 2001.
[ bib | .ps.gz ]
[80] A. Annichini, A. Bouajjani, and M. Sighireanu. TReX: A Tool for Reachability Analysis of Complex Systems. In Proc. 13th Int. Conf. Computer Aided Verification (CAV 2001), volume 2102 of Lecture Notes in Computer Science, pages 368-372. Springer, July 2001.
[ bib | .ps.gz ]
[81] A. Collomb-Annichini and M. Sighireanu. Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX. In P. Pettersson and S. Yovine, editors, Proc. Workshop on Real-Time Tools (RTTOOLS'01), Aalborg, August 2001. Uppsala University, Department of Information Technology, 2001. Appears as technical report 2001-014.
[ bib ]
[82] A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In Proc. 12th Int. Conf. Computer Aided Verification (CAV 2000), number 1855 in Lecture Notes in Computer Science, pages 403-418, July 2000.
[ bib | .ps.gz ]
[83] A. Annichini, E. Asarin, and A. Bouajjani. Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. In Proc. 12th Int. Conf. Computer Aided Verification (CAV 2000), volume 1855 of Lecture Notes in Computer Science, pages 419-434. Springer, July 2000.
[ bib | .ps.gz ]
[84] A. Bouajjani and P. Habermehl. Symbolic Reachability Analysis of Fifo-Channel Systems with Nonregular Sets of Configurations. Theoretical Computer Science, 221(1-2):211-250, June 1999.
[ bib | .ps.gz ]
[85] A. Bouajjani and R. Mayr. Model Checking Lossy Vector Addition Systems. In Proc. 16th Ann. Symp. Theoretical Aspects of Computer Science (STACS '99), volume 1563 of Lecture Notes in Computer Science, pages 323-333. Springer, March 1999.
[ bib | .ps.gz ]
[86] P.A. Abdulla, A. Annichini, S. Bensalem, A. Bouajjani, and Y. Lakhnech P. Habermehl. Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. In Proc. 11th Int. Conf. Computer Aided Verification (CAV '99), Trento, Italy, July 1999, volume 1633 of Lecture Notes in Computer Science, 1999.
[ bib | .ps.gz ]
[87] H. Comon and Y. Jurski. Timed Automata and the Theory of Real Numbers. In Proc. 10th Int. Conf. Concurrency Theory (CONCUR '99), Eindhoven, The Netherlands, Aug. 1999, volume 1664 of Lecture Notes in Computer Science, 1999.
[ bib | .ps ]

This file has been generated by bibtex2html 1.75

Valid HTML 4.01! Valid CSS!