A. Legay. Generic Techniques for the Verification of Infinite-State Systems. PhD thesis. Ulg December 2007. Abstract. Thesis.

P. Aziz Abdulla, A. Legay, J. d'Orso, A. Rezine. Tree Regular Model Checking: A Simulation-Based Approach. Volume 19 of Journal of Logic and Algebraic Programming 2006, pages 92-121. Abstract. Paper.

K. Chatterjee, L. de Alfaro, M. Faella, A. Legay. Qualitative Logics and Equivalences for Probabilistic Systems. Volume 5(2) of Logical Methods in Computer Science, 2009. Paper.

F. Cantin, A. Legay, P. Wolper. Computing Convex hulls by automata iteration. Volume 20(4) of International Journal of Foundations of Computer Science, pages 647-667, 2009. Paper.

E. M. Clarke, A. Donze, A. Legay. On Simulation-Based Probabilistic Model Checking of Mixed-Analog Circuits. To appear in Formal Methods in System Design (2009). Paper.

A. Legay, P. Wolper. On (Omega-)Regular Model Checking. To appear in Transactions on Computational Logic (2009). Paper.

J-B. Raclet, E. Badouel, A. Benveniste, B. Caillaud, A. Legay, R. Passerone. Modal Interfaces: Unifying Interface Automata and Modal Specifications. To appear in Fundamenta Informaticae (2010).Paper.

L. de Alfaro, M. Faella, A. Legay. An Introduction to the Tool TICC. Proc. of TrustWorthy Workshop Software 2006. Saarbrücken, Août 2006. Published in Dagstuhl online proceedings. This paper describes the new features of Ticc that have been implemented after the CAV06 paper. Abstract. Paper.

A. Legay and B. Delahaye. Statistical Model Checking: A brief Overview. Proc of Quantitative Models: Expressiveness and Analysis 2010. Wadern, January 2010. Published in Dagstuhl online proceedings series

B. Boigelot, A. Legay, P. Wolper. Iterating Transducers in the Large. Proc. 15th International Conference on Computer-Aided Verification, volume 2725, Lecture Notes in Computer Science, pages 223-235, Boulder, July 2003, Springer-Verlag. Abstract. Paper.

B. Boigelot, A. Legay, P. Wolper. Omega-regular Model Checking. Proc. 10th International Conference on Tools ans Algorithms for the Construction and Analysis of Systems, volume 2988, Lecture Notes in Computer Science, pages 561-575, Barcelona, April 2004, Springer-Verlag. Abstract. Paper.

- A. Bouajjani, A. Legay, P. Wolper. Handling Liveness properties in (Omega-)Regular Model Checking. Proc of Infinity04 Workshop, pages 37-48, London, September 2004. Also: Volume 138(3) of ENTCS, pages 101-115. (2005). Abstract. Paper.
P. Aziz Abdulla, A. Legay, J. d'Orso, A. Rezine. Simulation-Based Iteration of Tree Transducers (short version). Proc. 10th Nordic Workshop on Programming Theory, pages 11-13, Uppsala, October 2004.

P. Aziz Abdulla, A. Legay, J. d'Orso, A. Rezine. Simulation-Based Iteration of Tree Transducers. Proc. 11th International Conference on Tools ans Algorithms for the Construction and Analysis of Systems, volume 3440, Lecture Notes in Computer Science, pages 30-44, Edinburgh, April 2005, Springer-Verlag. Abstract. Paper.

A. Legay, P. Wolper. On the use of Automata-based Techniques in Symbolic Model Checking. Invited Contribution. To appear in Proc of MTCoord05 Workshop, Namur, April 2005. Also: Volume 150(1) of ENTCS, pages 3-8. (2006). Abstract. Paper.

A. Legay, M. Faella. Some Models and Tools for Open Systems. Proc of FIT05 Workshop, San Fransisco, August 2005. Also to appear in a volume of ENTCS. Abstract. Paper.

L. de Alfaro, L.Dias da Silva, M. Faella, A. Legay, P. Roy, M. Sorea. Sociable Interfaces. Proc. 5th International Workshop on Frontiers of Combining Systems, volume 3717, Lecture Notes in Computer Science, pages 81-105, Vienna, September 2005, Springer-Verlag. Abstract. Paper.

B. Thomas Adler, L. de Alfaro, L. Dias Da Silva, M. Faella, A. Legay, V. Raman, P. Roy. Ticc: A Tool for Interface Compatibility and Composition. Proc. 18th International Conference on Computer-Aided Verification, volume 4144, Lecture Notes in Computer Science, pages 59-62, Seattle, August 2006, Springer-Verlag. Abstract. Paper.

A. Legay. On the Implementation of a Game-Based Model for Specifying Open Systems. Short paper presentation. Proc 18th International Workshop on Algebraic Development Techniques. La Roche en Ardenne, June 2006.

M. Faella, A. Legay. On the Implementation of a Game-Based Model for Specifying Open Systems. Proc. 10th Conference on Approches Formelles dans l'Assistance au Développement de Logiciels. Presses Universitaires de Namur, pages ,75-90, Namur, June 2007. Abstract. Paper.

F. Cantin, A. Legay, P. Wolper. Computing Convex hulls by automata iteration. Proc 1th AUTOMATHA 07. Abstract. Paper.

K. Chatterjee, L. de Alfaro, M. Faella, A. Legay. Qualitative Logics and Equivalences for Probabilistic Systems. Proc. 4th International Conference on Quantitative Evaluation of Systems. IEEE, pages 237-246. Edinburgh, September 2007. Abstract. Paper.

A. Legay, A. Murawski, J. Ouaknine, J. Worrell. On Automated Verification of Probabilistic Programs. Proc. 14th International Conference on Tools ans Algorithms for the Construction and Analysis of Systems, volume 4963, Lecture Notes in Computer Science, pages 173-187, Budapest, April 2008, Springer-Verlag. Abstract. Paper.

M. Faella, A. Legay, M. Stoelinga. Model checking Quantitative Linear Time Logic. Proc 6th Workshop on Quantitative Aspects of Programming Languages, volume 220(3), Electronic Notes in Computer Science, pages 61-77, Budapest, April 2008. Abstract. Paper.

A. Legay. T(O)RMC: a Tool for (Omega-)Regular Model Checking. Proc. 20th International Conference on Computer-Aided Verification, volume 5123, Lecture Notes in Computer Science, pages 548-551, Princeton, July 2008, Springer-Verlag. Abstract. Paper.

B. Aminof, A. Legay, A. Murano. O. Serre. Mu-calculus Pushdown Module Checking with Imperfect State Information. Proc 5th IFIP International Conference on Theoretical Computer Science, volume 273, Springer Science and Business Media, pages 333-348, Milano, September 2008. Abstract. Paper.

F. Cantin, A. Legay, P. Wolper. Computing Convex Hull by Automata Iteration. Proc 13th International Conference on Implementation and Application of Automata, volume 5148, Lecture Notes in Computer Science, pages 112-121, San Fransisco, July 2008, Springer-Verlag. Abstract. Paper.

E. M. Clarke, A. Donzé, A. Legay. Statistical Model Checking of Mixed-Analog Circuits. Proc. 2sd Workshop on Formal Verification of Analog Circuits. See the Haifa 2008 improved version.

E.M. Clarke, J.R. Faeder. L.A. Harris, C.J. Langmead, A. Legay, S. K. Jha. Statistical Model Checking in BioLab: Application to the automated analysis of the T-Cell Receptor Signalling Pathway. Proc. 6th Annual Conference on Computational Methods in Systems Biology, volume 5307, Lecture Notes in Computer Science (Bioinformatics), pages 231-250, Rostock, October 2008, Springer-Verlag. Abstract. Paper.

E. M. Clarke, A. Donzé, A. Legay. Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Delta-Sigma Modulator. Proc. 3rd International Haifa Verification Conference, volume 5394, Lecture Notes in Computer Science, pages 149-163, Haifa, October 2008, Springer-Verlag. Abstract. Paper.

A. Donzé, G. Clermont, C. J. Langmead, A. Legay. Parameter Synthesis in Nonlinear Dynamical Systems: Application to Systems Biology, Proc. 13th Annual International Conference on Research in Computational Molecular Biology, volume 5541, Lecture Notes in Computer Science, pages 155-169, Tucson, May 2009. Paper.

E.M. Clarke, C.J. Langmead, A. Legay, S. K. Jha, A. Platzer, P. Zuliani. A Bayesian Approach to Model Checking Biological Systems. Proc. 7th Annual Conference on Computational Methods in Systems Biology, volume 5688, Lecture Notes in Computer Science (Bioinformatics), pages 218-234, Bologna, September 2009, Springer-Verlag. Paper.

A. Legay, M. Viswanathan. Simulation + Hypothesis Testing for Model Checking of Probabilistic Systems (tutorial). Proc. 6th International Conference on Quantitative Evaluation of Systems. IEEE, pages 3. Budapest, September 2009. Paper.

J-B. Raclet, E. Badouel, A. Benveniste, B. Caillaud, A. Legay, R. Passerone. Modal Interfaces: Unifying Interface Automata and Modal Specifications. Proc. 9th International Conference on Embedded Software. IEEE. pages 87-96, Grenoble, October 2009. Paper.

B. Delahaye, B. Caillaud, A. Legay. Compositinal Reasoning for Assume/Guarantee Contracts Combining Stochastic and Nondeterministic Aspects. Proc. 21th Nordic Workshop on Programming Theory, Lyngby, October 2009.

N. Bertrand, A. Legay, J-B. Raclet, S. Pinchinat. A Compositional Approach on Modal Specifications for Timed Systems. Proc 11th International Conference on Formal Engineering Methods, volume 5885, Lecture Notes in Computer Science, pages 679-697, Rio, December 2009, Springer-verlag. To appear. Paper.

L. Bozzelli, A. Legay, S. Pinchinat. On Timed Alternating Simulation for Concurrent Timed Games. Proc 29th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, pages 85-96, Kanpur, December 2009. Paper.

R. Chadha, A. Legay, P. Prabhakar, M. Viswanathan. Complexity bounds for the verification of real-time software. Proc 11th International Conference on Verification, Model Checking, and Abstraction Interpretation, volume 5944, Lecture Notes in Computer Science, pages 95-111, Madrid, January 2010, Springer-verlag. Paper.

A. Classen, P. Heymans, P-Y. Schobbens, A. Legay, J-F. Raskin. Model Checking Lots of Systems: Efficient Verification of Temporal Properties in Software Product Lines, Proc of ICSE. Cape Town, May 2010. Paper.

A. David, K.G. Larsen, A. Legay, U. Nyman, A. Wasowski. Timed I/O automata: a complete specification theory for real-time systems. Proc 13th International Conference on Hybrid Systems: Computation and Control, ACM, pages 91-100, Stockholm, April 2010. Paper.

L. Bozzelli, A. Legay, S. Pinchinat. Hardness of preorder checking for basic formalisms. Proc 16th International Conference on Logic for Programming Artificial Intelligence and Reasoning, volume XXXX, Lecture Notes in Computer Science, pages XXXX, Dakar, May 2010, Springer-verlag. To appear. Paper.

B. Delahaye, B. Caillaud, A. Legay. Probabilistic Contracts : A Compositional Reasoning Methodology for the Design of Stochastic Systems. Proc 10th International Conference on Application of Concurrency to System Design, volume XXX, ACM, pages XXXX, Braga, July 2010. To appear. Paper.

L. Doyen, A. Legay, D. Nickovic, T.A. Henzinger. Robustness of Sequential Circuits. Proc 10th International Conference on Application of Concurrency to System Design, volume XXX, ACM, pages XXXX, Braga, July 2010. To appear. Paper.

A. Basu, M. Bozga. S. Bensalem, B. Caillaud, B. Delahaye, A. Legay. Statistical Abstraction and Model-Checking of Large Heterogeneous Systems. Proc 30th International Conference on Formal Techniques for Distributed Systems, volume XXXX, Lecture Notes in Computer Science, pages XXXX, Amsterdam, June 2010, Springer-verlag. To appear. Paper.

A. David, K.G. Larsen, A. Legay, U. Nyman, A. Wasowski. Methodologies for Specification of Real-Time Systems Using Timed I/O Automata. Proc 8th International Simposium on Formal Methods for Components and Objects, volume XXXX, Lecture Notes in Computer Science, pages XXXX, Eindhoven, November 2009, Springer-verlag. Post Proceedings, to appear. Paper.

S. Bensalem, A. Legay, T. Nguyen, J. Sifakis. Incremental Invariant Generation for Compositional Design Proc 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, IEEE, pages XXXX, Taipei, August 2010, to appear. Paper.

J. Ortizs, A. Legay, P-Y. Schobbens. Memory Event Clocks. Proc. 8th International Conference on Formal Modelling and Analysis of Timed Systems, volume XXXX, Lecture Notes in Computer Science, pages XXXX, Vienna, September 2010, Springer-verlag, To appear. Paper.

B. Caillaud, B. Delahaye, K. Larsen, A. Legay, M. Pedersen, A. Wasowski. Proc. 7th International Conference on Quantitative Evaluation of SysTems, IEEE, pages XXX, Williamsburg, September 2010, to appear. Paper.

A. David, K.G. Larsen, A. Legay, U. Nyman, A. Wasowski. Timed I/O automata: ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems . Proc 8th Symposium on Automated Technology for Verification and Analysis, volume XXX, Lecture Notes in Computer Science, pages XXXX, Singapore, September 2010, Springer-verlag. To appear. Paper.

S. Bensalem, M. Bozga, A. Legay, T. Nguyen, J. Sifakis. Incremental Component-based Construction and Verification using Invariants. Proc 10th International Conference on Formal Methods in Computer Aided Design, IEEE, pages XXXX, Lugano, October 2010, to appear. Paper.

A. Basu, M. Bozga. S. Bensalem, B. Delahaye, A. Legay, E. Sifakis. Verification of an AFDX Infrastructure using Simulations and Probabilities. Proc 1st International Conference on Runtime Verification, volume XXXX, Lecture Notes in Computer Science, pages XXXX, Malta, November 2010, Springer-verlag. To appear. Paper.

A. Legay, S. Bensalem, B. Delahaye. Statistical Model Checking: Present and Future: a tutorial. Proc of 1th International Conference on Runtime Verification, volume XXXX, Lecture Notes in Computer Science, pages XXXX, Malta, November 2010, springer-verlag. To appear. Paper.

B. Delahaye, J-P Katoen, K. Larsen, A. Legay, M. Peddersen, F. Sher, A. Wasowski. Abstract Probabilistic Automata Proc 12th International Conference on Verification, Model Checking, and Abstraction Interpretation, volume XXXX, Lecture Notes in Computer Science, pages XXXX, Austin, January 2011, Springer-verlag. Paper.

E. M. Clarke, A. Donzé, A. Legay. On Simulation-Based Probabilistic Model Checking of Mixed-Analog Circuits (DRAFT 2009) (long version of HVC08 paper). Paper.

K. Chatterjee, L. de Alfaro, M. Faella, A. Legay. Qualitative Logics and Equivalences for Probabilistic Systems (DRAFT 2008) (long version of QEST07 paper). Paper.

A. Legay, P. Wolper. On (Omega-)Regular Model Checking (DRAFT 2008) (long version of CAV03, TACAS04, CAV08 papers). Paper.

F. Cantin, A. Legay, P. Wolper. Computing Convex Hull by Automata Iteration (DRAFT 2008) (long version of CIAA08 paper). Paper.

Ahmed Bouajjani, A. Legay, P. Wolper. A Framework to Handle Linear Temporal Properties in (Omega-)Regular Model Checking (DRAFT 2008) (long version of INFINITY04 paper). Paper.

M. Faella and A. Legay. On the Implementation of a Game-Based Model for Specifying Open Systems.

B. Thomas Adler, L. de Alfaro, L. Dias Da Silva, M. Faella, A. Legay, V. Raman, P. Roy. Ticc: A Tool for Interface Compatibility and Composition. Technical Report ucsc-crl-06-01, School of Engineering, University of California, Santa Cruz, 2006.

P. Aziz Abdulla, A. Legay, J. d'Orso, A. Rezine. Tree Regular Model Checking: A Simulation-Based Approach (2005), Technical Report, Centre Fédéré en Vérification, 2005-42, 2005.

B. Boigelot, A. Legay, Jérôme Leroux, Boolean Binary Decision Diagrams (2005). Draft.

A. Legay. Verification of Heterogenous Infinite State systems (2004, improved in 2005). Draft.