International Conferences

2012

1. S. Chédor, C. Morvan, S. Pinchinat, H. Marchand. Analysis of partially observed recursive tile systems. In 11th Int. Workshop on Discrete Event Systems, Pages 265-271, Guadalajara, Mexico, October 2012.
2. N. Bertrand, J. Fearnley, S. Schewe. Bounded Satisfiability for PCTL. In proceedings of the 21st EACSL Annual Conferences on Computer Science Logic (CSL'12), LIPIcs, Pages 92-106, Fontainebleau, France, September 2012.
3. N. Bertrand, S. Schewe. Playing Optimally on Timed Automata with Random Delays. In proceedings of the 10th International Conference on Formal Modeling and Analysis of Timed Systems (Formats'12), LNCS, Volume 7595, Pages 43-58, London, UK, September 2012.
4. S. Pinisetty, Y. Falcone, T. Jéron, H. Marchand, A. Rollet, O. Nguena Timo. Runtime Enforcement of Timed Properties. In Third International Conference on Runtime Verification RV 2012, Istanbul, Turkey, September 2012.
5. A. Stainer. Frequencies in Forgetful Timed Automata. In proceedings of the 10th International Conference on Formal Modeling and Analysis of Timed Systems (Formats'12), LNCS, Volume 7595, London, UK, September 2012.
6. N. Bertrand, G. Delzanno, B. König, A. Sangnier, J. Stückrath. On the Decidability Status of Reachability and Coverability in Graph Transformation Systems. In 23rd International Conference on Rewriting Techniques and Applications, LIPIcs 15, Pages 101-116, Nagoya, Japan, May 2012.
7. S. Chédor, T. Jéron, C. Morvan. Test generation from recursive tiles systems. In TAP - 6th International Conference on Tests & Proofs - 2012, LNCS, Volume 7305, Pages 99-114, Prague, May 2012.
8. P. Bulychev, D. David, K. Larsen, A. Legay, G. Li, D. Poulsen, A. Stainer. Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic. In The 18th International Conference on Logic for Programming Artificial Intelligence and Reasoning, LNCS, Volume 7180, Pages 168-182, Mérida, Venezuela, March 2012.

2011

1. N. Bertrand, B. Genest. Minimal Disclosure in Partially Observable Markov Decision Processes . In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011), Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, Pages 411-422, Bombay, India, 2011. download
2. Ph. Darondeau, S. Demri, R. Meyer, Ch. Morvan. Petri Net Reachability Graphs: Decidability Status of FO Properties. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011), Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, Pages 140-151, Bombay, India, 2011. download
3. G. Kalyon, T. Le Gall, H. Marchand, T. Massart. Synthesis of Communicating Controllers for Distributed Systems. In 50th IEEE Conference on Decision and Control and European Control Conference, Pages 1803-1810, Orlando, USA, December 2011.
4. Y. Falcone, M. Jaber, Th-Hand Bozga, M. Nguyen, S. Bensalem. Runtime Verification of Component-Based Systems. In SEFM11: International Conference of Software Engineering and Formal Methods, Montevideo, Uruguay, November 2011.
5. P. Bhateja. Test Case Generation Using PDA. In 5th IEEE International Conference on Theoretical Aspects of Software Engineering, Xi'an, China, August 2011.
6. P. Bhateja. A Tagging Protocol for Asynchronous Testing. In 5th IEEE International Conference on Theoretical Aspects of Software Engineering, August 2011.
7. N. Bertrand, P Bouyer, Th. Brihaye, A. Stainer. Emptiness and Universality Problems in Timed Automata with Positive Frequency. In Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP'11), LNCS, Volume 6756, Pages 246-257, Zürich, Switzerland, July 2011.
8. H. Yu, J-P. Talpin, L. Besnard, T. Gautier, H. Marchand, P. Le Guernic. Polychronous Controller Synthesis from MARTE CCSL Timing Specifications. In ACM/IEEE Ninth International Conference on Formal Methods and Models for Codesign (MEMOCODE), Pages 21-30, Cambridge, United Kingdom, July 2011.
9. G. Kalyon, T. Le Gall, H. Marchand, T. Massart. Global State Estimates for Distributed Systems. In 31th IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems, FORTE, LNCS, Volume 6722, Pages 198-212, Reykjavik, Iceland, June 2011.
10. N. Bertrand, T. Jéron, A. Stainer, M. Krichen. Off-line Test Selection with Test Purposes for Non-Deterministic Timed Automata. In 17th International Conference on Tools and Algorithms for the Construction And Analysis of Systems (TACAS), LNCS, Volume 6605, Pages 96-111, Saarbrücken, Germany, April 2011.
11. N. Bertrand, A. Stainer, T. Jéron, M. Krichen. A game approach to determinize timed automata. In 14th International Conference on Foundations of Software Science and Computation Structures (FOSSACS), LNCS, Volume 6604, Pages 245-259, Saarbrücken, Germany, April 2011.
12. W. L. Andrade, P. Machado, T. Jéron, H. Marchand. Abstracting Time and Data for Conformance Testing of Real-Time Systems. In 7th Workshop on Advances in Model Based Testing A-MOST 2011, Berlin, Germany, March 2011.

2010

1. Y. Falcone. You should Better Enforce than Verify (Tutorial). In RV'10: Proceedings of the 1st International Conference on Runtime Verification, LNCS, Volume 6418, Pages 89-105, Malta, November 2010.
2. Y. Falcone, Fernandez J.-C, T. Jéron, H. Marchand, L. Mounier. More Testable Properties. In 22nd IFIP International Conference on Testing Software and Systems, LNCS, Volume 6435, Pages 30-46, Natal, Brazil, November 2010.
3. O. Landry Nguena, H. Marchand, A. Rollet. Automatic Test Generation for Data-Flow Reactive Systems with time constraints (Short paper). In 22nd IFIP International Conference on Testing Software and Systems, Pages 25-30, Natal, Brazil, November 2010.
4. N. Bertrand, C. Morvan. Probabilistic Regular Graphs. In Infinity, EPTCS, Volume 39, Pages 77-90, Singapore, September 2010.
5. Ph. Darondeau, J. Dubreil, H. Marchand. Supervisory Control for Modal Specifications of Services. In Workshop on Discrete Event Systems, WODES'10, Pages 428-435, Berlin, Germany, August 2010.
6. E. Dumitrescu, A. Girault, H. Marchand, E. Rutten. Multicriteria optimal discrete controller synthesis for fault-tolerant real-time tasks. In Workshop on Discrete Event Systems, WODES'10, Pages 366-373, Berlin, Germany, August 2010.
7. C. Morvan. Contextual graph grammars characterising Rational Graphs. In Non-Classical Models of Automata and Applications (NCMA), Pages 141-153, Jena, Germany, August 2010.
8. Y. Falcone, M. Jaber. Towards Automatic Integration of an Or-BAC Security Policy Using Aspects. In World Comp 2010: Software Engineering Research and Practice (SERP'10), Las Vegas, USA, July 2010.
9. A. Gamatié, V. Rusu, E. Rutten. Operational Semantics of the Marte Repetitive Structure Modeling Concepts for Data-Parallel Applications Design. In 9th International Symposium on Parallel and Distributed Computing (ISPDC'10), Pages 25-32, July 2010.
10. V. Rusu. Combining narrowing and theorem proving for rewriting-logic specifications. In 4th International Conference on Tests and Proofs (Tap'10), LNCS, Volume 6143, Pages 135-150, July 2010.
11. G. Delaval, H. Marchand, E. Rutten. Contracts for Modular Discrete Controller Synthesis. In Conference on Languages, Compilers and Tools for Embedded Systems, LCTES 2010, Pages 57-66, Stockholm, Sweden, April 2010.

2009

1. C. Baier, N. Bertrand, M. Grosser. Probabilistic Acceptors for Languages over Infinite Words. In 35th Conference on Current Trends in Theory and Practice of Computer Science, LNCS, Volume 5404, Pages 19-33, Spindleruv Mlyn, Czech, 2009.
2. N. Bertrand, A. Legay, S. Pinchinat, J-P. Raclet. A Compositional Approach on Modal Specifications for Timed Systems. In Proceedings of the 11th International Conference on Formal Engineering Methods (ICFEM'09), LNCS, Volume 5885, Pages 679-697, Rio de Janeiro, Brazil, December 2009.
3. G. Kalyon, T. Le Gall, H. Marchand, T. Massart. Computational Complexity for State-Feedback Controllers with Partial Observation. In 7th International Conference on Control and Automation, ICCA'09, Pages 435-441, Christchurch, New Zealand, December 2009.
4. Vlad Rusu. Formal Executable Semantics for Conformance in the MDE Framework. In UML and FM workshop, Rio de Janeiro, Brazil, December 2009.
5. H. Marchand, J. Dubreil, T. Jéron. Automatic Testing of Access Control for Security Properties. In TestCom'09, LNCS, Volume 5826, Pages 113-128, November 2009.
6. F. Cassez, J. Dubreil, H. Marchand. Dynamic Observers for the Synthesis of Opaque Systems. In 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09), Z. Liu, A.P. Ravn (eds.), LNCS, Volume 5799, Pages 352-367, Macao SAR, China, October 2009.
7. C. Morvan, S. Pinchinat. Diagnosability of pushdown systems. In HVC2009, Haifa Verification Conference, LNCS, Volume 6405, Pages 21-33, Haifa, Israel, October 2009.
8. N. Bertrand, B. Genest, Gimbert. H.. Qualitative Determinacy and Decidability of Stochastic Games with Signals. In 24th Annual IEEE Symposium on Logic in Computer Science (LICS'09), Pages 319-328, Los Angeles, CA, USA, August 2009.
9. J. Dubreil, T. Jéron, H. Marchand. Monitoring Confidentiality by Diagnosis Techniques. In European Control Conference, Pages 2584-2590, Budapest, Hungary, August 2009.
10. G. Kalyon, Le Gall T, H. Marchand, T. Massart. Control of Infinite Symbolic Transition Systems under Partial Observation. In European Control Conference, Pages 1456-1462, Budapest, Hungary, August 2009.
11. C. Morvan. On external presentations of infinite graphs. In 11th International Workshop on Verification of Infinite-State Systems, INFINITY'09, EPTCS, Volume 10, Pages 22-35, Bologna, Italy, August 2009. download
12. C. Baier, N. Bertrand, P. Bouyer, Th. Brihaye. When are timed automata determinizable?. In 36th International Colloquium on Automata, Languages and Programming (ICALP'09), LNCS, Volume 5556, Pages 43-54, Rhodes, Greece, July 2009.
13. J. Dubreil. Opacity and Abstraction. In Proceedings of the First International Workshop on Abstractions for Petri Nets and Other Models of Concurrency (APNOC'09), Paris, France, June 2009.
14. N. Bertrand, S. Pinchinat, J.B. Raclet. Refinement and Consistency of Timed Modal Specifications. In Proceedings of the 3rd International Conference on Language and Automata Theory and Applications (LATA'09), LNCS, Volume 5457, Pages 152-163, Tarragona, Spain, April 2009.

2008

1. N. Bertrand, P. Bouyer, Th. Brihaye, N. Markey. Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics. In Proceedings of the 5th International Conference on the Quantitative Evaluation of SysTems (QEST'08), Pages 55-64, Saint Malo, France, September 2008.
2. T. Jéron, H. Marchand, S. Genc, S. Lafortune. Predictability of Sequence Patterns in Discrete Event Systems. In IFAC World Congress, Pages 537-453, Seoul, Korea, July 2008.
3. Ch. Baier, N. Bertrand, P. Bouyer, Th. Brihaye, M. Groesser. Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata. In Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS'08), Pages 217-226, Pittsburgh, PA, USA, June 2008.
4. G. Delaval. Modular Distribution and Application to Discrete Controller Synthesis. In International Workshop on Model-driven High-level Programming of Embedded Systems (SLA++P'08), Budapest, Hungary, April 2008.
5. Ch. Baier, N. Bertrand, M. Groesser. On Decision Problems for Probabilistic Büchi Automata. In Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), LNCS, Volume 4962, Pages 287-301, Budapest, Hungary, March 2008.
6. J. Dubreil, Ph. Darondeau, H. Marchand. Opacity Enforcing Control Synthesis. In Workshop on Discrete Event Systems, WODES'08, Pages 28-35, Gothenburg, Sweden, March 2008.

2007

1. B. Jeannet, T. Jéron, V. Rusu. Model-based test selection for infinite state reactive systems. In Formal Methods of Components and Objects - FMCO 2006, Amsterdam, Netherlands, Revised Lectures, LNCS, Volume 4709, Pages 47-69, 2007.
2. M. Oostdijk, V. Rusu, J. Tretmans, R. de Vries, T. Willemse. Integrating verification, testing, and learning for cryptographic protocols. In Integrated Formal Methods (IFM'07), Lecture Notes in Computer Science, 2007.
3. T. Le Gall, B. Jeannet. Lattice automata: a representation of languages over an infinite alphabet, and some applications to verification. In The 14th International Static Analysis Symposium, SAS 2007, LNCS, Volume 4634, Pages 52-68, Kongens Lyngby, Denmark, August 2007.
4. C. Constant, B. Jeannet, T. Jéron. Automatic test generation from interprocedural specifications. In TestCom/Fates07, LNCS, Volume 4581, Pages 41-57, Tallinn, Estonia, June 2007.
5. E. Dumitrescu, A. Girault, H. Marchand, E. Rutten. Optimal discrete controller synthesis for the modeling of fault-tolerant distributed systems. In First IFAC Workshop on Dependable Control of Discrete Systems (DCDS'07), Paris, France, June 2007.

2006

1. B. Blanc, F. Bouquet, A. Gotlieb, B. Jeannet, T. Jéron, B. Legeard, B. Marre, C. Michel, M. Rueher. The V3F Project. In Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA06), Nantes, B. Blanc, A. Gotlieb, C. Michel (eds.), 2006.
2. J. Komenda, H. Marchand, S. Pinchinat. A constructive and modular approach to decentralized supervisory Control problems. In 3rd IFAC Workshop on Discrete-Event System Design, 2006.
3. Thierry Jéron. Model-based test selection for infinite state reactive systems. In 5th IFIP Working Conference on Distributed and Parallel Embedded Systems, DIPES'06, Braga, Portugal, Invited paper, October 2006.
4. T. Jéron, H. Marchand, V. Rusu. Symbolic Determinisation of Extended Automata. In 4th IFIP International Conference on Theoretical Computer Science, IFIP book series, Pages 197-212, Stantiago, Chile, August 2006.
5. T. Jéron, H. Marchand, S. Pinchinat, M-O. Cordier. Supervision Patterns in Discrete Event Systems Diagnosis. In Workshop on Discrete Event Systems, WODES'06, Also published in DX'06, Penaranda de Duero (Burgos, Spain), Pages 262-268, Ann-Arbor (MI, USA), July 2006.
6. T. Le Gall, B. Jeannet, T. Jéron. Verification of Communication Protocols using Abstract Interpretation of FIFO queues. In 11th International Conference on Algebraic Methodology and Software Technology, AMAST '06, Kuressaare, Estonia, Michael Johnson, Varmo Vene (eds.), LNCS, Volume 4019, Pages 204-219, July 2006.
7. K. Schmidt, H. Marchand, B. Gaudin.. Modular and Decentralized Supervisory Control of Concurrent Discrete Event Systems Using Reduced System Models. In Workshop on Discrete Event Systems, WODES'06, Pages 149-154, Ann-Arbor (MI, USA), July 2006.
8. G. Barthe, J. Forest, D. Pichardie, V. Rusu. Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In Functional and LOgic Programming Systems (FLOPS'06), LNCS, Volume 3945, Pages 114-129, Fuji Susono, Japan, April 2006.

2005

1. B. Gaudin, H. Marchand. Supervisory Control and Deadlock Avoidance Control Problem for Concurrent Discrete Event Systems. In 44nd IEEE Conference on Decision and Control (CDC'05) and Control and European Control Conference ECC 2005, Pages 2763-2768, Seville (Spain), December 2005.
2. J. Komenda, J. H. van Schuppen, B. Gaudin, H. Marchand. Modular supervisory control with general indecomposable specification languages. In 44nd IEEE Conference on Decision and Control (CDC'05) and Control and European Control Conference ECC 2005, Pages 3474-3479, Seville (Spain), December 2005.
3. T. Le Gall, B. Jeannet, H. Marchand. Supervisory Control of Infinite Symbolic Systems using Abstract Interpretation. In 44nd IEEE Conference on Decision and Control (CDC'05) and Control and European Control Conference ECC 2005, Pages 31-35, Seville (Spain), December 2005.
4. S. Bardin, A. Finkel, J. Leroux, P. Schnoebelen. Flat acceleration in symbolic model checking. In 3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA'05), Springer (ed.), LNCS, Volume 3707, Pages 474-488, Taipei, Taiwan, October 2005.
5. J. Leroux, G. Sutre. Flat counter automata almost everywhere!. In 3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA'05), Springer (ed.), LNCS, Volume 3707, Pages 489-503, Taipei, Taiwan, October 2005.
6. B. Jeannet, D. Gopan, T. Reps. A Relational Abstraction for Functions. In The 12th International Static Analysis Symposium, SAS'05, LNCS, Volume 2672, Pages 186-202, September 2005.
7. B. Gaudin, H. Marchand. Efficient Computation of supervisors for loosely synchronous Discrete Event Systems: A State-Based Approach. In 6th IFAC World Congress, Prague, Czech Republic, July 2005.
8. Vlad Rusu, Hervé Marchand, Thierry Jéron. Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems. In Formal Methods 2005 (FM05), John Fitzgerald, Andrzej Tarlecki, Ian Hayes (eds.), LNCS, Volume 3582, Pages 189-204, July 2005.
9. B. Gaudin, H. Marchand. Safety Control of Hierarchical Synchronous Discrete Event Systems: A State-Based Approach. In 13th Mediterranean Conference on Control and Automation, Pages 889-895, Limassol, Cyprus, June 2005.
10. 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, Chicago, USA, June 2005.
11. B. Jeannet, T. Jéron, V. Rusu, E. Zinovieva. Symbolic Test Selection based on Approximate Analysis. In 11th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), LNCS, Volume 3440, Pages 349-364, Edinburgh (Scottland), April 2005.

2004

1. B. Gaudin, H. Marchand. Modular Supervisory Control of a class of Concurrent Discrete Event Systems. In Workshop on Discrete Event Systems, WODES'04, Pages 181-186, September 2004.
2. B. Jeannet, A. Loginov, T. Reps, M. Sagiv. A Relational Approach to Interprocedural Shape Analysis. In 11th Static Analysis Symposium - SAS 2004. Volume 3148 of LNCS, Verona, Italy, August 2004.
3. B. Jeannet, W. Serwe. Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs. In 10th International Conference on Algebraic Methodology And Software Technology AMAST'2004. Volume 3116 of LNCS, July 2004.
4. N. Bertrand, Ph. Schnoebelen. Verifying Nondeterministic Channel Systems With Probabilistic Message Losses. In Proceedings of the 3rd International Workshop on Automated Verification of Infinite-State Systems (AVIS'04), Ramesh Bharadwaj (ed.), Barcelona, Spain, April 2004.
5. V. Rusu, H. Marchand, V. Tschaen, T. Jéron, B. Jeannet. From Safety Verification to Safety Testing. In The 16th IFIP International Conference on Testing of Communicating Systems (TestCom04). Volume 2978 of LNCS, Oxford, UK, March 2004.
6. D. Cachera, T. Jensen, D. Pichardie, V. Rusu. Extracting a data flow analyser in constructive logic. In European Symposium on Programming,ESOP'04. Volume 2986 of LNCS, Pages 385-400, February 2004.

2003

1. V. Rusu. Compositional verification of an ATM protocol. In Formal Methods Europe (FME'03), (postscript, and PVS files), 2003.
2. T. Jéron, H. Marchand, V. Rusu, V. Tschaen. Ensuring the conformance of reactive discrete-event systems using supervisory control. In 42nd IEEE Conference on Decision and Control, Hawaii, USA, December 2003.
3. A. Khoumsi, Jéron T, H. Marchand. Test Cases Generation for Nondeterministic Real-time Systems. In 3rd International Workshop on Formal Approaches To Testing of Software (FATES 2003), Montréal, Québec, Canada, October 2003.
4. F. Gaucher, E. Jahier, B. Jeannet, F. Maraninchi. Automatic State Reaching for Debugging Reactive Programs. In Fifth International Workshop on Automated and Algorithmic Debugging AADEBUG'2003,Ghent (Belgium), September 2003.
5. B. Gaudin, H Marchand. Modular Supervisory Control of Asynchronous and Hierarchical Finite State Machines. In European Control Conference, ECC 2003, An extended version (with the proofs) is available at http://www.irisa.fr/vertecs/Publis/Ps/2003-ECC-Extended-version.pdf, Cambridge, UK, September 2003.
6. N. Bertrand, Ph. Schnoebelen. Model Checking Lossy Channels Systems Is Probably Decidable. In Proceedings of the 6th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'03), Andrew D. Gordon (ed.), Lecture Notes in Computer Science, Volume 2620, Pages 120-135, Warsaw, Poland, April 2003.

2002

1. D. Clarke, T. Jéron, V. Rusu, E. Zinovieva. STG: a Symbolic Test Generation tool. In (Tool paper) Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02). Volume 2280 of LNCS, 2002.
2. V. Rusu. Verification using test generation techniques. In Formal Methods Europe (FME'02), 2002. download
3. V. Rusu, E. Zinovieva, D. Clarke. Verifying Invariants More Automatically. In Verification and Computatoiional Logic, VCL'02, 2002. download
4. H. Marchand, B. Gaudin. Supervisory Control Problems of Hierarchical Finite State Machines. In 41th IEEE Conference on Decision and Control, Pages 1199-1204, Las Vegas, USA, December 2002.
5. S. Pickin, C. Jard, Y. Le Traon, T. Jéron, J.-M. Jezequel, A. Le Guennec. System Test Synthesis from UML Models of Distributed Software. In Forte 2002, 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems. Volume 2529 of LNCS, Houston, Texas, November 2002.
6. A. Benveniste, P. Caspi, P. Le Guernic, H. Marchand, J.P. Talpin, S. Tripakis. A Protocol for Loosely Time-Triggered Architectures. In Embedded Software Conference (EMSOFT '02), LNCS, Volume 2491, Pages 252-265, Grenoble, France, October 2002.
7. H. Marchand, E. Rutten. A case study in applying discrete control synthesis to excavator operation. In IEEE International Conference on Systems, Man and Cybernetics (IEEE SMC), Hammamet, Tunisia, October 2002.
8. B. Jeannet. Representing and Approximating Transfer Functions in Abstract Interpretation of Hetereogeneous Datatypes. In Static Analysis Symposium, SAS'02, LNCS, Volume 2477, Pages 52-68, Madrid (Spain)), September 2002.
9. B. Jeannet, P. D'Argenio, K.G. Larsen. RAPTURE: A tool for verifying Markov Decision Processes. In Tools Day, International Conference on Concurrency Theory, CONCUR'02, Brno, Czech Republic, August 2002.
10. P. D'Argenio, B. Jeannet, H.E. Jensen, K.G. Larsen. Reduction and Refinement Strategies for Probabilistic Analysis. In Process Algebra and Probabilistic Methods - Performance Modelling and Verification, PAPM-PROBMIV 2002, LNCS, Volume 2399, Copenhagen, Denmark, July 2002.
11. C. Jard, T. Jéron. TGV: theory, principles and algorithms. In The Sixth World Conference on Integrated Design & Process Technology (IDPT'02), Pasadena, California, USA, June 2002.
12. H. Marchand, E. Rutten. Managing multi-mode tasks with time cost and quality levels using optimal discrete control synthesis. In 14th Euromicro Conference on Real-Time Systems (ECRTS'02), Pages 241-248, June 2002.
13. E. Zinovieva. Symbolic Test Generation for Reactive Systems. In Proceedings of the Modelling and Verifying Parallel Processes Summer School (MOVEP'02), June 2002.

2001

1. D. Clarke, T. Jéron, V. Rusu, E. Zinovieva. Automated Test and Oracle Generation for Smart-Card Applications. In International Conference on Research in Smart Cards (e-Smart'01), Volume 2140 of LNCS, Pages 58-70, 2001.
2. D. Clarke, T. Jéron, V. Rusu, E. Zinovieva. STG : A Tool for Generating Symbolic Test Programs and Oracles from Operational Specifications. In Joint 8th European Software Engineering Conference (ESEC) and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-9), 2001.
3. V. Rusu. Verifying that Invariants are Context-Inductive. In Theorem Proving in Higher-Order Logics (TPHOLs'01),, Category B paper, University of Edinburgh research Report EDI-INF-RR-0046, Pages 337-351, 2001.
4. V. Rusu. Verifying a Sliding-Window Protocol using PVS. In Formal Description Techniques (FORTE'01), Pages 251-266, 2001.
5. A. Benveniste, P. Bournai, T. Gautier, M. Le Borgne, P. Le Guernic, H. Marchand. The Signal declarative synchronous language : controller synthesis & systems/architecture design. In 40th IEEE Conference on Decision and Control, Pages 3284-3289, Orlando, Florida, USA, December 2001.
6. H. Marchand, O. Boivineau, S. Lafortune. Optimal control of discrete event systems under partial observation. In 40th IEEE Conference on Decision and Control, Pages 2235-2240, Orlando, Florida, USA, December 2001.
7. P.R. D'Argenio, B. Jeannet, H.E. Jensen, K.J. Larsen. Reachability Analysis of Probabilistic Systems by Successive Refinements. In Process Algebra and Probabilistic Methods - Performance Modelling and Verification, PAPM-PROBM 2001, LNCS, Volume 2165, Aachen, Germany, September 2001.

2000

1. S. Bensalem, V. Ganesh, Y. Lakhnech, C. Munoz, S. Owre, H. Russ, J. Rushby, V. Rusu, H. Saidi, N. Shankar, E. Singerman, A. Tiwari. An Overview of SAL. In LFM 2000: Fifth NASA Langley Formal Methods Workshop, Pages 187-196, 2000. download
2. V. Rusu, L. du Bousquet, T. Jéron. An approach to symbolic test generation. In International Conference on Integrating Formal Methods (IFM'00), LNCS 1945, Pages 338-357, November 2000.
3. A. Belinfante, L. Du Bousquet, S. Ramangalahy, S. Simon, C. Viho, R. De Vries. Formal test automation: the conference protocol with TGV/TorX. In IFIP TC6/WG6.1 13th International Conference on Testing of Communicating Systems, TestCom 2000, Ottawa, Ontario, Canada, Hasan Ural, Robert L. Probert, Gregor v. Bochman (eds.), Pages 221-228, August 2000.
4. C. Jard, T. Jéron, P. Morel. Verification of Test Suites. In TestCom 2000, IFIP TC 6 / WG 6.1, The IFIP 13th International Conference on Testing of Communicating Systems, Ottawa, Ontario, Canada, H. Ural, R.L. Probert, G. v. Bochman (eds.), August 2000.
5. S. Pinchinat, H. Marchand. Symbolic Abstractions of Automata. In Proc of 5th Workshop on Discrete Event Systems, WODES 2000, Pages 39-48, Ghent, Belgium, August 2000.
6. L. Du Bousquet, H. Martin. Automatic test generation for Java-Card applets. In 4th Workshop on Tools for System Design and Verification, July 2000.
7. H. Marchand, S. Pinchinat. Supervisory Control Problem using Symbolic Bisimulation Techniques. In 2000 American Control Conference, Pages 4067-4071, Chicago, Illinois, USA, June 2000.

1999

1. V. Rusu, E. Singerman. On proving safety properties by integrating static analysis, theorem proving and abstraction. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), LNCS 1579, An improved version appeared as INRIA research report 3726, available at http://www.inria.fr/rrrt/rr-3726.html, Pages 178-192, 1999.
2. T. Jéron, J.-M. Jézéquel, Y. Le Traon, P. Morel. Efficient Strategies for Integration and Regression Testing of 00 Systems. In 10th IEEE International Symposium on Software Reliability Engineering, ISSRE'99, Boca Raton, Florida, Pages 260-269, November 1999.
3. C. Jard, T. Jéron, L. Tanguy, C. Viho. Remote testing can be as powerful as local testing. In Formal methods for protocol engineering and distributed systems, FORTE XII/ PSTV XIX' 99, Beijing, China, J. Wu, S. Chanson, Q. Gao (eds.), Pages 25-40, October 1999.
4. H. Marchand, M. Samaan. On the Incremental Design of a Power Transformer Station Controller using Controller Synthesis Methodology. In World Congress on Formal Methods (FM'99), Volume 1709 of LNCS, Pages 1605-1624, Toulouse, France, October 1999.
5. B. Jeannet, N. Halbwachs, P. Raymond. Dynamic Partitioning in Analyses of Numerical Properties. In Static Analysis Symposium, SAS'99, LNCS, Volume 1694, Venezia (Italy), September 1999.
6. T. Jéron, P. Morel. Test generation derived from model-checking. In CAV'99, Trento, Italy, N. Halbwachs, D. Peled (eds.), LNCS, Volume 1633, Pages 108-122, July 1999.
7. R. Groz, T. Jéron, A. Kerbrat. Automated Test Generation from SDL specifications. In SDL'99 The Next Millenium, 9th SDL Forum, Montréal, Québec, R. Dssouli, G. von Bochmann, Y. Lahav (eds.), Pages 135-152, June 1999.
8. S. Ramangalahy, P. Le Gall, T. Jéron. Une application de la théorie des jeux au test de conformité. In Colloque Francophone sur l'Ingénierie des Protocoles, CFIP 99, Nancy, France, A. Schaff (ed.), April 1999.
9. H. Kahlouche, C. Viho, M. Zendri. Hardware Testing using a Communication Protocol Conformance Testing Tool. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), W.R. Cleaveland (ed.), LNCS, Volume 1579, Pages 315-329, March 1999.

1998

1. T.A. Henzinger, V. Rusu. Reachability verification for hybrid automata. In International Workshop on Hybrid Systems: Computation and Control, LNCS 1386, Pages 190-204, Berkeley, California, USA, 1998.
2. C. Jard, T. Jéron, H. Kahlouche, C. Viho. Towards Automatic Distribution of Testers for Distributed Conformance Testing. In FORTE/PSTV'98, Paris, France, November 1998.
3. C. Jard, T. Jéron. Verification and distributed observation of the alternating bit protocol. In FORTE/PSTV'98, ECASP: Special Session on Educational Case Studies in Protocols, Paris, France, November 1998.
4. H. Marchand, O. Boivineau, S. Lafortune. On the Synthesis of Optimal Schedulers in Discrete Event Control Problems with Multiple Goals. In 1998 IEEE International Conf. On Systems, Man, And Cybernetics, Pages 734-739, San Diego, California, USA, October 1998.
5. H. Marchand, P. Bournai, M. Le Borgne, P. Le Guernic. A Design Environment for Discrete-Event Controllers based on the SIGNAL Language. In 1998 IEEE International Conf. On Systems, Man, And Cybernetics, Pages 770-775, San Diego, California, USA, October 1998.
6. H. Kahlouche, C. Viho, M. Zendri. An Industrial Experiment in Automatic Generation of Executable Test Suites for a Cache Coherency Protocol. In IFIP TC6 11th International Workshop on Testing of Communicating Systems, A. Petrenko, N. Yevtushenko (eds.), September 1998.
7. H. Marchand, M. Le Borgne. Partial Order Control of Discrete Event Systems modeled as Polynomial Dynamical Systems. In 1998 IEEE International Conference On Control Applications, Trieste, Italie, September 1998.
8. H. Marchand, M. Le Borgne. On the Optimal Control of Polynomial Dynamical Systems over Z/pZ. In 4th IEE International Workshop on Discrete Event Systems, Pages 385-390, Cagliari, Italie, August 1998.
9. T. Jéron, J.-M. Jézéquel, A. Le Guennec. Validation and Test Generation for Object-Oriented Distributed Software. In IEEE Proc. Parallel and Distributed Software Engineering, PDSE'98, Kyoto, Japan, April 1998.

1997

1. C. Ancourt, D. Barthou, C. Guettier, F. Irigoin, B. Jeannet, J. Jourdan, J. Mattioli. Automatic Data Mapping of Signal Processing Applications. In Int. Conf. on Application-specific Systems, Architectures and Processors (ASAP'97), 1997.
2. F. Boniol, A. Burgueno, O. Roux, V. Rusu. Analysis of slope-parametric hybrid automata. In International Workshop on Hybrid and Real-Time Systems (HART'97), Volume 1201 of LNCS, Pages 75-81, Grenoble, France, 1997.
3. A. Burgueno, V. Rusu. Task-system analysis using slope-parametric hybrid automata. In Proceedings of the European Conference on Parallelism (EuroPar'97) Volume 1300 of LNCS, Pages 1262-1273, Passau (Germany), 1997.
4. V. Rusu. Verifying periodic task-control systems. In International Workshop on Hybrid and Real-Time Systems (HART'97), Volume 1201 of LNCS, Pages 63-69, Grenoble, France, 1997.
5. T. Jéron, P. Morel. Abstraction, $\tau$-réduction et déterminisation à la volée: application à la génération de test. In CFIP'97, Congrès Francophone sur l'Ingéniérie des Protocoles, Liège, Belgique, September 1997.

1996

1. O. Roux, V. Rusu. Deciding time-bounded properties for ELECTRE reactive programs with stopwatch automata. In International workshop on Hybrid Systems and Autonomous Control (WHSAC'94), Volume 999 of LNCS, Pages 405-416, Cornell University, Ithaca (New York, USA), 1996.
2. Y.-M. Quemener, T. Jéron. Finitely Representing Infinite Reachability Graphs of CFSMs with Graph Grammars. In FORTE/PSTV'96, October 1996. download
3. L. Doldi, V. Encontre, J.-C. Fernandez, T. Jéron, S. Le Bricquir, N. Texier, M. Phalippou. Assessment of Automatic Generation Methods of Conformance Test Suites in an Industrial Context. In IFIP TC6 9th International Workshop on Testing of Communicating Systems, B. Baumgarten, H.-J. Burkhardt, A. Giessler (eds.), September 1996.
4. J.-C. Fernandez, C. Jard, T. Jéron, G. Viho. Using on-the-fly Verification Techniques for the Generation of Test Suites. In Conference on Computer-Aided Verification (CAV'96), New Brunswick, New Jersey, USA, A. Alur, T. Henzinger (eds.), LNCS, Volume 1102, July 1996.
5. M. Le Borgne, H. Marchand, E. Rutten, M. Samaan. Formal Verification of SIGNAL programs: Application to a Power Transformer Station Controller. In Proceedings of the Fifth International Conference on Algebraic Methodology and Software Technology AMAST'96, Pages 271-285, Munich, Germany, July 1996.

1995

1. H. Marchand, E. Rutten, M. Samaan. Synchronous design of a transformer station controller in Signal. In Proceedings of the 4th IEEE Conference on Control Applications, CCA '95, Albany, New York, Pages 754-759, September 1995.
2. Y.-M. Quemener, T. Jéron. Model-Checking of Infinite Kripke Structures Defined by Simple Graph Grammars. In SEGRAGRA'95, Joint COMPUGRAPH/SEMAGRAPH Workshop on Graph Rewriting and Computation, Volterra, Italie, A. Corradini, U. Montanari (eds.), ENTCS, Egalement disponible en rapport de recherche Irisa n$^o$ 927 et Inria n$^o$ 2563, Pages 64-74, September 1995. download
3. T. Jéron. Dessin en 3 dimensions de graphes d'accessibilité de processus communicants. In CFIP'95, Colloque Francophone sur l'Ingéniérie des Protocoles, Rennes, France, C. Jard, P. Rolin (eds.), Pages 373-386, May 1995. download

1994

1. C. Jard, T. Jéron. Formal Analysis of Distributed Computations. In (Conférence invitée) Septièmes entretiens du centre Jacques Cartier, Communicating Informatics and Distributed Systems, Grenoble, France, Gv. Bochmann, M. Barbeau, M. Riveill, J. Sifakis (eds.), December 1994.
2. T. Jéron, C. Jard. 3D Layout of Reachability Graphs of Communicating Processes. In Graph Drawing'94, DIMACS Workshop, Princeton, New-Jersey, LNCS, Volume 894, Pages 25-33, October 1994. download
3. C. Jard, T. Jéron, G.-V. Jourdan, J.-X. Rampon. A General Approach to Trace Checking in Distributed Computing Systems. In 14th International Conference on Distributed Computing Systems, Poznan, Pologne, Pages 396-403, June 1994.

1991

1. C. Jard, T. Jéron. Bounded Memory Algorithms for Verification On the fly. In CAV'91: Symposium on Computer Aided Verification, Aalborg, Denmark, LNCS, Volume 575, Pages 192-202, June 1991.
2. T. Jéron. Testing for unboundedness of fifo channels. In STACS 91 : Symposium on Theoretical Aspects of Computer Science, Hamburg, Germany, LNCS, Volume 480, Pages 322-333, February 1991.
3. T. Jéron. Prototype of a verification tool. In STACS 91 (Tool Demonstration): Symposium on Theoretical Aspects of Computer Science, Hamburg, Germany, LNCS, Volume 480, Pages 322-333, February 1991.

1989

1. M. Adam, P. Burgevin, B. Caillaud, A. Couvert, J.-M. Helary, P. Ingels, C. Jard, T. Jeron, J.-M. Jezequel, R. Pedrono, M. Raynal. Distributed Computers in the Design and Analysis of Distributed Algorithms. In 1er Colloque Européen sur les Hypercubes et Calculateurs Distribués, Rennes, October 1989.
2. C. Jard, T. Jéron. On-line model-checking for finite linear temporal logic specifications. In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, LNCS, Volume 407, Pages 275-285, June 1989.

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic