Verimag

Sorted by year

2014

Journal Articles

  1. Comparison of Mean Hitting Times for a Degree-Biased Random Walk. Karine Altisen, Stéphane Devismes, Antoine Gerbaud, Pascal Lafourcade - Discrete Applied Mathematics - [bibtex]
  2. Statically detecting Use-After-Free on Binary Code. Josselin Feist, Laurent Mounier, Marie-Laure Potet - Journal of Computer Virology and Hacking Techniques - [bibtex]

Conference Articles

  1. On Probabilistic Snap-Stabilization. Karine Altisen, Stéphane Devismes - ICDCN'2014, 15th International Conference on Distributed Computing and Networking - [bibtex]
  2. Environment-Model Based Testing of Control Systems: Case Studies. Erwan Jahier, Simplice Djoko-Djoko, Chaouki Maiza, Eric Lafont - International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014), Held as Part of ETAPS 2014. - [bibtex]
  3. Learning Regular Languages over Large Alphabets. Oded Maler, Irini Eleftheria Mens - International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014 - [bibtex]
  4. Formal and Informal Methods for Multi-Core Design Space Exploration. Jean-Francois Kempf, Olivier Lebeltel, Oded Maler - QAPL - [bibtex]
  5. Safety Problems Are NP-complete for Flat Integer Programs with Octagonal Loops. Marius Bozga, Radu Iosif, Filip Konecn\'y - Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings - [bibtex]
  6. Lazart: a symbolic approach for evaluation the robustness of secured codes against control flow fault injection. Marie-Laure Potet, Laurent Mounier, Maxime Puys, Louis Dureuil - ICST - [bibtex]
  7. Compositional Invariant Generation for Timed Systems. Lacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, Jacques Combaz - Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS - [bibtex]
  8. Stabilisation Instantanée Probabiliste. Karine Altisen, Stéphane Devismes - 16èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications (AlgoTel) - [bibtex]

PhD Thesis and HDR

  1. High-level Models for Embedded Systems. Matthieu Moy - Habilitation à Diriger des Recherches (HDR) - [bibtex]

2013

Journal Articles

  1. Self-Stabilizing Small k-Dominating Sets. Ajoy Kumar Datta, Lawrence L. Larmore, Stéphane Devismes, Karel Heurtefeux, Yvan Rivierre - IJNC, International Journal of Networking and Computing - [bibtex]
  2. STL-based analysis of TRAIL-induced apoptosis challenges the notion of type I/type II cell line classification. Szymon Stoma, Alexandre Donzé, Francois Bertaux, Oded Maler, Grégory Batt - PLoS Computational Biology - [bibtex]
  3. Optimal Probabilistic Ring Exploration by Semi-Synchronous Oblivious Robots. Stéphane Devismes, Franck Petit, Sébastien Tixeuil - Theoretical Computer Science (TCS) - [bibtex]
  4. Optimizing two-dimensional DMA transfers for scratchpad Based MPSoCs platforms. Selma Saidi, Pranav Tendulkar, Thierry Lepley, Oded Maler - Microprocessors and Microsystems - Embedded Hardware Design - [bibtex]
  5. Specification and Validation of Embedded Systems: A Case Study of a Fault-Tolerant Data Acquisition System with Lustre Programming environment. Florence Maraninchi, Nicolas Halbwachs, Pascal Raymond, Catherine Parent, R. K. Shyamasundar - CSI Journal of Computing - [bibtex]
  6. Self-Stabilizing Labeling and Ranking in Ordered Trees. Ajoy Kumar Datta, Lawrence L. Larmore, Stéphane Devismes, Yvan Rivierre - Theoretical Computer Science (Special Issue SSS 2011) - [bibtex]
  7. Rigorous embedded design: challenges and perspectives. Saddek Bensalem, Axel Legay, Marius Bozga - STTT - [bibtex]
  8. Rigorous implementation of real-time systems - from theory to application. Tesnim Abdellatif, Jacques Combaz, Joseph Sifakis - Mathematical Structures in Computer Science - [bibtex]
  9. Automata-Based Termination Proofs. Radu Iosif, Adam Rogalewicz - Computing and Informatics - [bibtex]

Book Chapters

  1. Abstraction-Based Guided Search for Hybrid Systems. Sergiy Bogomolov, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor T Johnson, Hamed Ladan, Andreas Podelski, Martin Wehrle - Model Checking Software - [bibtex]

Conference Articles

  1. Fast Leader (Full) Recovery despite Dynamic Faults. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore, Sébastien Tixeuil - ICDCN: 14th International Conference on Distributed Computing and Networking - [bibtex]
  2. Self-stabilizing Silent Disjunction in an Anonymous Network. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore - ICDCN: 14th International Conference on Distributed Computing and Networking - [bibtex]
  3. Parallel Programming with SystemC for Loosely Timed Models: A Non-Intrusive Approach. Matthieu Moy - The Design, Automation, and Test in Europe (DATE) - [bibtex]
  4. Flowpipe Approximation and Clustering in Space-Time. Goran Frehse, Colas Le Guernic, Rajat Kateja - HSCC - [bibtex]
  5. System-Level Modeling of Energy in TLM for Early Validation of Power and Thermal Management. Tayeb Bouhadiba, Matthieu Moy, Florence Maraninchi - Design Automation and Test Europe (DATE) - [bibtex]
  6. The Tree Width of Separation Logic with Recursive Definitions. Radu Iosif, Adam Rogalewicz, Jirí Simácek - CADE - [bibtex]
  7. Underapproximation of Procedure Summaries for Integer Programs. Pierre Ganty, Radu Iosif, Filip Kone\vcn\'y - TACAS - [bibtex]
  8. Fast and Accurate TLM Simulations using Temporal Decoupling for FIFO-based Communications. Claude Helmstetter, Jérôme Cornet, Bruno Galilée, Matthieu Moy, Pascal VIVET - Design, Automation and Test in Europe (DATE) - [bibtex]
  9. Co-Simulation of Functional SystemC TLM Models with Power/Thermal Solvers. Tayeb Bouhadiba, Matthieu Moy, Florence Maraninchi, Jérôme Cornet, Laurent Maillet-Contoz, Ilija Materic - Virtual Prototyping of Parallel and Embedded Systems (VIPES) - [bibtex]
  10. As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty. Jean-Francois Kempf, Marius Bozga, Oded Maler - TACAS - PDF - [bibtex]
  11. Explorer une grille avec un minimum de robots amnésiques. Franck Petit, Anissa Lamani, Stéphane Devismes, Sébastien Tixeuil, Pascal Raymond - 15èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications (AlgoTel) - [bibtex]
  12. Algorithme autostabilisant avec convergence sûre construisant une $(f,g)$-alliance. Fabienne Carrier, Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore, Yvan Rivierre - Algotel : 15èmes Rencontres Francophones pour les Aspects Algorithmiques des Télécommunications - [bibtex]
  13. Routage sécurisé et résilient pour réseaux de capteurs sans fil. Karine Altisen, Stéphane Devismes, Raphaël Jamet, Pascal Lafourcade - 15èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications (AlgoTel) - [bibtex]
  14. A stack model for symbolic buffer overflow exploitability analysis (Extended Abstract). Gustavo Grieco, Laurent Mounier, Marie-Laure Potet, Sanjay Rawat - 5th Workshop on the Constraints in Software Testing, Verification and Analysis CSTVA 2013 (in association with ICST 2013) - [bibtex]
  15. Program Repair without Regret. Christian von Essen, Barbara Jobstmann - Computer Aided Verification (CAV) - [bibtex]
  16. Formal Verification of e-Auction Protocols. Jannik Dreier, Pascal Lafourcade, Yassine Lakhnech - Principles of Security and Trust - Second International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, - [bibtex]
  17. On Unique Decomposition of Processes in the Applied -Calculus. Jannik Dreier, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech - Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, - [bibtex]
  18. Verifiability in E-Auction Protocols. Jannik Dreier, Hugo Jonker, Pascal Lafourcade - 1st Workshop on Hot Issues in Security Principles and Trust (HotSpot 2013) - [bibtex]
  19. Multiple Independent Lazy Intruders. Ali Kassem, Pascal Lafourcade, Yassine Lakhnech, Sebastian M ödersheim - 1st Workshop on Hot Issues in Security Principles and Trust (HotSpot 2013) - [bibtex]
  20. Model-Based Implementation of Parallel Real-Time Systems. Ahlem Triki, Jacques Combaz, Saddek Bensalem, Joseph Sifakis - Fundamental Approaches to Software Engineering - 16th International Conference, FASE 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, M - [bibtex]
  21. Engineering Functional Requirements of Reactive Systems using Synchronous Languages. Erwan Jahier, Nicolas Halbwachs, Pascal Raymond - International Symposium on Industrial Embedded Systems, 2013. SIES'13. - [bibtex]
  22. Efficient Robust Monitoring for STL. Alexandre Donzé, Thomas Ferrére, Oded Maler - CAV - [bibtex]
  23. Verification of embedded control programs. Thao Dang, Bertrand Jeannet, Romain Testylier - Proceedings of European Conrol Conference ECC - [bibtex]
  24. Automated Security Proofs for Almost-Universal Hash for MAC verification. Martin Gagne, Pascal Lafourcade, Yassine Lakhnech - Computer Security - ESORICS 2013 - 18th European Symposium on Research in Computer Security, London, UK, September 2012. Proceedings - [bibtex]
  25. Program Semantics in Model-Based WCET Analysis: A State of the Art Perspective. Mihail Asavoae, Claire Maiza, Pascal Raymond - 13th International Workshop on Worst-Case Execution Time Analysis, WCET 2013, July 9, 2013, Paris, France - [bibtex]
  26. Integrating cache related pre-emption delay analysis into EDF scheduling. Will Lunniss, Sebastian Altmeyer, Claire Maiza, Robert I. Davis - 19th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2013, Philadelphia, PA, USA, April 9-11, 2013 - [bibtex]
  27. Analysis of Probabilistic Cache Related Pre-emption Delays. Rob Davis, Luca Santinelli, Sebastian Altmeyer, Claire Maiza, Liliana Cucu-Grosjean - 25th Euromicro Conference on Real-Time Systems (ECRTS 2013) - [bibtex]
  28. SR3: Secure Resilient Reputation-based Routing. Karine Altisen, Stéphane Devismes, Raphaël Jamet, Pascal Lafourcade - The annual IEEE International Conference on Distributed Computing in Sensor Systems (DCOSS 2013) - [bibtex]
  29. Exploring the Dynamics of Mass Action Systems. Oded Maler, Adam M. Halasz, Olivier Lebeltel, Ouri Maler - Hybrid Systems Biology - PDF - [bibtex]
  30. Self-Stabilizing (f,g)-Alliances with Safe Convergence. Fabienne Carrier, Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore, Yvan Rivierre - SSS'2013, 15th International Symposium on Stabilization, Safety, and Security of Distributed Systems - [bibtex]
  31. Falsifying Oscillation Properties of Parametric Biological Models. Thao Dang, Tommaso Dreossi - Proceedings Second International Workshop on Hybrid Systems and Biology, HSB 2013, Taormina, Italy, 2nd September 2013 - [bibtex]
  32. NLTOOLBOX: A Library for Reachability Computation of Nonlinear Dynamical Systems. Romain Testylier, Thao Dang - Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings - [bibtex]
  33. Timing analysis enhancement for synchronous program. Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Fabienne Carrier - RTNS - [bibtex]
  34. Algorithmic Analysis of Continuous and Hybrid Systems. Oded Maler - Infinity - [bibtex]
  35. CIL Security Proof for a Password-Based Key Exchange. Cristian Ene, Clémentine Gritti, Yassine Lakhnech - Provable Security - 7th International Conference, ProvSec 2013, Melaka, Malaysia, October 23-25, 2013. Proceedings - [bibtex]
  36. Knowledge for the Distributed Implementation of Constrained Systems. Susanne Graf, Sophie Quinton - 10th International Conference on integrated Formal Methods, iFM 2013, Turku, June 10-14. Proceedings - [bibtex]
  37. Stochastic modeling and performance analysis of multimedia SoCs. Balaji Raman, Ayoub Nouri, Deepak Gangadharan, Marius Bozga, Ananda Basu, Mayur Maheshwari, Axel Legay, Saddek Bensalem, Samarjit Chakraborty - 2013 International Conference on Embedded Computer Systems: Architectures, Modeling, and Simulation, SAMOS 2013, Agios Konstantinos, Samos Island, Greece, July 15-18, 2013 - [bibtex]
  38. Performance Evaluation of Process Partitioning Using Probabilistic Model Checking. Saddek Bensalem, Borzoo Bonakdarpour, Marius Bozga, Doron Peled, Jean Quilbeuf - Hardware and Software: Verification and Testing - 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013, Proceedings - [bibtex]
  39. Mixed Critical Earliest Deadline First. Dario Socci, Peter Poplavko, Saddek Bensalem, Marius Bozga - 25th Euromicro Conference on Real-Time Systems, ECRTS 2013, Paris, France, July 9-12, 2013 - [bibtex]
  40. An Abstract Framework for Deadlock Prevention in BIP. Paul C. Attie, Saddek Bensalem, Marius Bozga, Mohamad Jaber, Joseph Sifakis, Fadi A. Zaraket - Formal Techniques for Distributed Systems - Joint IFIP WG 6.1 International Conference, FMOODS/FORTE 2013, Held as Part of the 8th International Federated Conference on Distributed Computing Technique - [bibtex]
  41. Predictive Taint Analysis for Extended Testing of Parallel Executions. Emmanuel Sifakis, Laurent Mounier - Hardware and Software: Verification and Testing - 9th International Haifa Verification Conference - [bibtex]
  42. Brandt's Fully Private Auction Protocol Revisited. Jannik Dreier, Jean-Guillaume Dumas, Pascal Lafourcade - Progress in Cryptology - AFRICACRYPT 2013, 6th International Conference on Cryptology in Africa, Cairo, Egypt, June 22-24, 2013. Proceedings - [bibtex]
  43. Implementing hash-consed data structures in Coq. Thomas Braibant, Jacques-Henri Jourdan, David Monniaux - Interactive theorem proving (ITP) - [bibtex]
  44. Modular, hierarchical models of control systems in SpaceEx. Alexandre Donzé, Goran Frehse - Control Conference (ECC), 2013 European - [bibtex]
  45. Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra. Alexis Fouilhé, David Monniaux, Michaël Périn - Static analysis (SAS) - [bibtex]

PhD Thesis and HDR

  1. Rigorous Design Flow for Programming Manycore Platforms. Paraskevas Bourgos - [bibtex]
  2. Towards efficient and secure shared memory applications. Emmanuel Sifakis - [bibtex]
  3. Self-Stabilizing Algorithms for Constructing Distributed Spanning Structures. Yvan Rivierre - [bibtex]
  4. Analyse statique de programmes manipulant des tableaux. Valentin Perrelle - Thesis - [bibtex]

2012

Journal Articles

  1. Optimizing Explicit Data Transfers for Data Parallel Applications on the Cell Architecture. Selma Saidi, Pranav Tendulkar, Thierry Lepley, Oded Maler - ACM Transactions on Architecture and Code Optimization, Vol. V, - PDF - [bibtex]
  2. Synchronous Programming of Device Drivers for Global Resource Control in Embedded Operating Systems. Nicolas Berthier, Florence Maraninchi, Laurent Mounier - ACM Transactions on Embedded Computing Systems (TECS) - [bibtex]
  3. Achieving distributed control through model checking. Susanne Graf, Doron Peled, Sophie Quinton - Formal Methods in System Design - [bibtex]
  4. Sécuriser les systèmes distribués à base de composants par contrôle de flux d'information. Lilia Sfaxi, Takoua Abdellatif, Yassine Lakhnech, Riadh Robbana - Technique et Science Informatiques - [bibtex]
  5. Statistical abstraction and model-checking of large heterogeneous systems. Ananda Basu, Saddek Bensalem, Marius Bozga, Benoît Delahaye, Axel Legay - STTT - [bibtex]
  6. Synthesis of Reactive(1) designs. Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Yaniv Sa'ar - J. Comput. Syst. Sci. - [bibtex]
  7. Finding and fixing faults. Barbara Jobstmann, Stefan Staber, Andreas Griesmayer, Roderick Bloem - J. Comput. Syst. Sci. - [bibtex]
  8. Monitoring Properties of Analog and Mixed-Signal Designs,. Oded Maler, Dejan Nickovic - Software Tools for Technology Transfer - [bibtex]
  9. Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs. Thomas Gawlitza, David Monniaux - Logical Methods in Computer Science - [bibtex]
  10. Improved cache related pre-emption delay aware response time analysis for fixed priority pre-emptive systems. Sebastian Altmeyer, Robert I. Davis, Claire Maiza - Real-Time Systems - [bibtex]
  11. A framework for automated distributed implementation of component-based models. Borzoo Bonakdarpour, Marius Bozga, Mohamad Jaber, Jean Quilbeuf, Joseph Sifakis - Distributed Computing - [bibtex]
  12. Reachability analysis for polynomial dynamical systems using the Bernstein expansion. Thao Dang, Romain Testylier - Reliable Computing Journal - [bibtex]
  13. Introduction à la calculabilité. David Monniaux - Quadrature - [bibtex]
  14. Algorithme autostabilisant construisant un petit ensemble k-dominant. Ajoy Kumar Datta, Stéphane Devismes, Karel Heurtefeux, Lawrence L. Larmore, Yvan Rivierre - Technique et Science Informatiques - [bibtex]
  15. Rigorous design of robot software: A formal component-based approach. Tesnim Abdellatif, Saddek Bensalem, Jacques Combaz, Lavindra de Silva, Felix Ingrand - Robotics and Autonomous Systems - [bibtex]
  16. Politiques de gestion de protections pour l'implémentation de sections critiques.. Sifakis Emmanuel, Mounier Laurent - Techniques et Sciences Informatiques - [bibtex]
  17. More testable properties. Ylies Falcone, Jean-Claude Fernandez, Thierry Jéron, Hervé Marchand, Laurent Mounier - STTT - [bibtex]
  18. Generating Invariant-based Certificates for Embedded Systems. Jan-Olaf Blech, Michaël Périn - ACM Transactions on Embedded Computing Systems (TECS) - [bibtex]

Book Chapters (inbook)

  1. Formal Model for (k)-Neighborhood Discovery Protocols. Raphël Jamet, Pascal Lafourcade - [bibtex]

Conference Articles

  1. Is RSSI a good choice for localization in Wireless Sensor Network? Karel Heurtefeux, Fabrice Valois - IEEE International Conference on Advanced Information Networking and Applications - [bibtex]
  2. Synthesizing Efficient Controllers. Christian von Essen, Barbara Jobstmann - Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings - [bibtex]
  3. Key Management Protocol in WIMAX revisited. Nacira Ghoualmi, Noudjoud Kahya, Pascal Lafourcade - The Third International Conference on Communications Security and Information Assurance (CSIA 2012) - [bibtex]
  4. Un dispositif pour alerter les étudiants sur leur maîtrise des pré-requis nécessaires pour réussir leur entrée à l'université. Julien Douady, Christian Hoffmann, Fabienne Carrier, Benoit Chabaud, Arnaud Mantoux, Yves Markowicz, Michaël Périn, Virginie Stoppin-Mellet, Gabrielle Tichtinsky, Bernard Ycart, Hubert Borderiou - Congrès de l'Association Internationale de Pédagogie Universitaire - [bibtex]
  5. Deciding Conditional Termination. Marius Bozga, Radu Iosif, Filip Kone\vcn\'y - Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS - [bibtex]
  6. Experiments on the feasibility of using a floating-point simplex in an SMT solver. Diego Caminha Barbosa de Oliveira, David Monniaux - Workshop on Practical Aspects of Automated Reasoning (PAAR) - [bibtex]
  7. Anatomy of Alternating Quantifier Satisfiability (Work in progress). Anh-Dung Phan, Nikolaj Bj\orner, David Monniaux - 10th International Workshop on Satisfiability Modulo Theories (SMT) - [bibtex]
  8. Algorithme de k-partitionnement auto-stabilisant et compétitif. Kumar Ajoy Datta, Stéphane Devismes, Karel Heurtefeux, Lawrence L. Larmore, Yvan Rivierre - 14èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications (AlgoTel) - [bibtex]
  9. Optimal 2D Data Partitioning for DMA Transfers on MPSoCs. Selma Saidi, Pranav Tendulkar, Thierry Lepley, Oded Maler - Proceedings of the 15th EUROMICRO Conference on Digital System Design - [bibtex]
  10. Co-Simulation of a SystemC TLM Virtual Platform with a Power Simulator at the Architectural Level: Case of a Set-Top Box. Jérôme Cornet, Laurent Maillet-Contoz, Ilija Materic, Sylvian Kaiser, Hela Boussetta, Tayeb Bouhadiba, Matthieu Moy, Florence Maraninchi - Design Automation Conference - [bibtex]
  11. PAGAI: a path sensitive static analyzer. Julien Henry, David Monniaux, Matthieu Moy - Tools for Automatic Program Analysis (TAPAS) - [bibtex]
  12. Knowledge-Based Distributed Conflict Resolution for Multiparty Interactions and Priorities. Saddek Bensalem, Marius Bozga, Jean Quilbeuf, Joseph Sifakis - Formal Techniques for Distributed Systems - Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13-16, 2012. - [bibtex]
  13. Analysis of Random Walks using Tabu Lists. Karine Altisen, Stéphane Devismes, Antoine Gerbaud, Pascal Lafourcade - 19th International Colloquium on Structural Information and Communication Complexity (SIROCCO'2012) - PDF - [bibtex]
  14. Optimal Grid Exploration by Asynchronous Oblivious Robots. Stéphane Devismes, Anissa Lamani, Franck Petit, Pascal Raymond, Sébastien Tixeuil - 14th International Symposium on Stabilization, Safety, and Security of Distributed Systems, SSS - [bibtex]
  15. Competitive Self-Stabilizing k-Clustering. Ajoy Kumar Datta, Stéphane Devismes, Karel Heurtefeux, Lawrence L. Larmore, Yvan Rivierre - ICDCS - [bibtex]
  16. Succinct Representations for Abstract Interpretation. Julien Henry, David Monniaux, Matthieu Moy - Static analysis (SAS) - [bibtex]
  17. When the decreasing sequence fails. Nicolas Halbwachs, Julien Henry - 19th International Static Analysis Symposium, SAS'12 - PDF - [bibtex]
  18. Brief Announcement: Self-stabilizing Silent Disjunction in an Anonymous Network. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore - Stabilization, Safety, and Security of Distributed Systems - 14th International Symposium, SSS 2012, Toronto, Canada, October 1-4, 2012. Proceedings - [bibtex]
  19. On efficiency of unison. Stéphane Devismes, Franck Petit - 4th Workshop on Theoretical Aspects of Dynamic Distributed Systems, TADDS - [bibtex]
  20. A formal taxonomy of privacy in voting protocols. Jannik Dreier, Pascal Lafourcade, Yassine Lakhnech - Proceedings of IEEE International Conference on Communications, ICC 2012, Ottawa, ON, Canada, June 10-15, 2012 - [bibtex]
  21. Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin - CPP - [bibtex]
  22. Generic Indifferentiability Proofs of Hash Designs. Marion Daubignard, Pierre-Alain Fouque, Yassine Lakhnech - CSF - 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012 - [bibtex]
  23. Defining Privacy for Weighted Votes, Single and Multi-voter Coercion. Jannik Dreier, Pascal Lafourcade, Yassine Lakhnech - ESORICS - Computer Security - ESORICS 2012 - 17th European Symposium on Research in Computer Security, Pisa, Italy, September 10-12, 2012. Proceedings - [bibtex]
  24. A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx. Sergiy Bogomolov, Goran Frehse, Radu Grosu, Hamed Ladan, Andreas Podelski, Martin Wehrle - Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings - [bibtex]
  25. Flowpipe-Guard Intersection for Reachability Computations with Support Functions. Goran Frehse, Rajarshi Ray - IFAC Conf. Analysis and Design of Hybrid Systems (ADHS) - [bibtex]
  26. Reachability Analysis of Polynomial Systems Using Linear Programming Relaxations. Mohamed Amin Ben Sassi, Romain Testylier, Thao Dang, Antoine Girard - ATVA - [bibtex]
  27. State Estimation and Property-Guided Exploration for Hybrid Systems Testing. Thao Dang, Noa Shalev - ICTSS - [bibtex]
  28. Analysis of parametric biological models with non-linear dynamics. Romain Testylier, Thao Dang - HSB - [bibtex]
  29. Investigation of Scratchpad Memory for Preemptive Multitasking. Jack Whitham, Robert I. Davis, Neil C. Audsley, Sebastian Altmeyer, Claire Maiza - RTSS - [bibtex]
  30. Accelerating Interpolants. Hossein Hojjat, Radu Iosif, Filip Kone\vcn\'y, Viktor Kuncak, Philipp Rümmer - ATVA - [bibtex]
  31. A Verification Toolkit for Numerical Transition Systems - Tool Paper. Hossein Hojjat, Filip Kone\vcn\'y, Florent Garnier, Radu Iosif, Viktor Kuncak, Philipp Rümmer - FM - [bibtex]
  32. On Temporal Logic and Signal Processing. Alexandre Donzé, Oded Maler, Ezio Bartocci, Dejan Nickovic, Radu Grosu, Scott Smolka - ATVA - PDF - [bibtex]
  33. State-of-the-art tools and techniques for quantitative modeling and analysis of embedded systems. Marius Bozga, Alexandre David, Arnd Hartmanns, Holger Hermanns, Kim Guldstrand Larsen, Axel Legay, Jan Tretmans - 2012 Design, Automation & Test in Europe Conference & Exhibition, DATE 2012, Dresden, Germany, March 12-16, 2012 - [bibtex]
  34. Integration of correct-by-construction BIP models into the MetroII design space exploration flow. Alena Simalatsar, Liangpeng Guo, Marius Bozga, Roberto Passerone - 30th International IEEE Conference on Computer Design, ICCD 2012, Montreal, QC, Canada, September 30 - Oct. 3, 2012 - [bibtex]
  35. Statistical Model Checking QoS Properties of Systems with SBIP. Saddek Bensalem, Marius Bozga, Benoît Delahaye, Cyrille Jégourel, Axel Legay, Ayoub Nouri - Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change - 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proc - [bibtex]
  36. Modeling Dynamic Architectures Using Dy-BIP. Marius Bozga, Mohamad Jaber, Nikolaos Maris, Joseph Sifakis - Software Composition - 11th International Conference, SC 2012, Prague, Czech Republic, May 31 - June 1, 2012. Proceedings - [bibtex]
  37. A Theory of Fault Recovery for Component-Based Models. Borzoo Bonakdarpour, Marius Bozga, Gregor Gößler - Stabilization, Safety, and Security of Distributed Systems - 14th International Symposium, SSS 2012, Toronto, Canada, October 1-4, 2012. Proceedings - [bibtex]
  38. Modeling and Validation of PLC-Controlled Systems: A Case Study. Rui Wang, Min Zhou, Liangze Yin, Lianyi Zhang, Jiaguang Sun, Gu Ming, Marius Bozga - Sixth International Symposium on Theoretical Aspects of Software Engineering, TASE 2012, 4-6 July 2012, Beijing, China - [bibtex]
  39. Rigorous Component-Based System Design - (Invited Paper). Ananda Basu, Saddek Bensalem, Marius Bozga, Joseph Sifakis - Rewriting Logic and Its Applications - 9th International Workshop, WRLA 2012, Held as a Satellite Event of ETAPS, Tallinn, Estonia, March 24-25, 2012, Revised Selected Papers - [bibtex]
  40. Optimized distributed implementation of multiparty interactions with observation. Saddek Bensalem, Marius Bozga, Jean Quilbeuf, Joseph Sifakis - Proceedings of the 2nd edition on Programming systems, languages and applications based on actors, agents, and decentralized control abstractions - [bibtex]
  41. A Taint Based Approach for Smart Fuzzing. Sofia Bekrar, Chaouki Bekrar, Roland Groz, Laurent Mounier - Proceedings of SecTest - [bibtex]
  42. Dynamic Information-Flow Analysis for Multi-threaded Applications. Laurent Mounier, Emmanuel Sifakis - Proceedings of ISoLA - [bibtex]
  43. Finding Buffer Overflow Inducing Loops in Binary Executables. Sanjay Rawat, Laurent Mounier - Proceedings of Sixth International Conference on Software Security and Reliability (SERE) - [bibtex]
  44. Formal Model Driven Engineering for Space Onboard Software. Eric Conquet, François-Xavier Dormoy, Iulia Dragomir, Susanne Graf, David Lesens, Piotr Nienaltowski, Iulian Ober - International Congress on Embedded Real Time Software and Systems (ERTS2), Toulouse, February 2012 - [bibtex]

PhD Thesis and HDR

  1. Programmation synchrone de pilotes de périphériques pour un contrôle global de ressources dans les systèmes embarqués. Nicolas Berthier - [bibtex]
  2. On Computer-Aided Design-Space Exploration for Multi-Cores. Jean-Francois Kempf - [bibtex]
  3. Optimizing DMA Data Transfers for Embedded Multi-Cores. Selma Saidi - [bibtex]
  4. A Formal Framework for Specifying and Analyzing Liabilities Using Log as Digital Evidence. Eduardo Sampaio Elesbao Mazza - [bibtex]
  5. Computer-Aider Security for: Cryptographic Primitives, Voting Protocols and Wireless Sensor Networks. Pascal Lafourcade - Habilitation à diriger des recherches - [bibtex]
  6. Rigorous Implementation of Real-Time Systems. Tesnim Abdellatif - [bibtex]
  7. Tirex : a textual target-level intermediate representation. Artur Pietrek - [bibtex]
  8. Formal Methods For Concrete Security Proofs. Marion Daubignard - [bibtex]
  9. Reachability Analysis of Hybrid Systems using Support Functions. Rajarshi Ray - [bibtex]
  10. Harnessing Forest Automata for Verification of Heap Manipulating Programs. Jirí Simácek - [bibtex]

2011

Journal Articles

  1. What can you Verify and Enforce at Runtime ? Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier - Software Tool in Tecnology Transfer (STTT) - [bibtex]
  2. Runtime Enforcement Monitors: composition, synthesis, and enforcement abilities. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier, Jean-Luc Richier - Formal Methods in System Design - [bibtex]
  3. Self-Stabilizing k-out-of-l exclusion on tree networks. Ajoy Kumar Datta, Stéphane Devismes, Florian Horn, Lawrence L. Larmore - International Journal of Foundations of Computer Science - [bibtex]
  4. Computing reachable states for nonlinear biological models. Thao Dang, Colas Le Guernic, Oded Maler - Theoretical Computer Science - [bibtex]
  5. Asymptotically Optimal Deterministic Rendezvous. Fabienne Carrier, Stéphane Devismes, Franck Petit, Yvan Rivierre - International Journal of Foundations of Computer Science (IJFCS) - [bibtex]
  6. A vision for computer science - the system perspective. Joseph Sifakis - Central Europ. J. Computer Science - [bibtex]
  7. Rigorous Component-Based System Design Using the BIP Framework. Ananda Basu, Saddek Bensalem, Marius Bozga, Jacques Combaz, Mohamad Jaber, Thanh-Hung Nguyen, Joseph Sifakis - IEEE Software - [bibtex]
  8. Automated Proofs for Asymmetric Encryption. Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech - J. Autom. Reasoning - [bibtex]
  9. Autour de l'Auto-stabilisation. Partie I : Techniques généralisant l'approche. Stéphane Devismes, Franck Petit, Vincent Villain - Technique et science informatiques (TSI) - [bibtex]
  10. Autour de l'Auto-Stabilisation. Partie II : Techniques spécialisant l'approche. Stéphane Devismes, Franck Petit, Vincent Villain - Technique et science informatiques (TSI) - [bibtex]
  11. Robustness Analysis and Behavior Discrimination in Enzymatic Reaction Networks. Alexandre Donzé, Eric Fanchon, Lucie Martine Gattepaille, Oded Maler, Philippe Tracqui - PLOS One - [bibtex]
  12. Building Distributed Controllers for Systems with Priorities. Imene Ben Hafaiedh, Susanne Graf, Sophie Quinton - J. Log. Algebr. Program. - [bibtex]
  13. Priority scheduling of distributed systems based on model checking. Ananda Basu, Saddek Bensalem, Doron Peled, Joseph Sifakis - Formal Methods in System Design - [bibtex]
  14. Formalisms for Specifying Markovian Population Models. Thomas A. Henzinger, Barbara Jobstmann, Verena Wolf - Int. J. Found. Comput. Sci. - [bibtex]
  15. Liability issues in software engineering: the use of formal methods to reduce legal uncertainties. Daniel Le Métayer, Manuel Maarek, Eduardo Mazza, Marie-Laure Potet, Stéphane Frénot, Valérie Viet Triem Tong, Nicolas Craipeau, Ronan Hardouin - Commun. ACM - [bibtex]
  16. Programs with lists are counter automata. Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar - Formal Methods in System Design - [bibtex]

Book Chapters (inbook)

  1. Formal Models and Techniques for Analyzing Security Protocols. Emmanuel Bresson, Yassine Lakhnech, Laurent Mazaré, Bogdan Warinschi - [bibtex]
  2. Model-Based Testing for Embedded Systems. Thao Dang - [bibtex]

Book Chapters

  1. Efficient Bounded Reachability Computation for Rectangular Automata. Xin Chen, Erika Abraham, Goran Frehse - Reachability Problems - [bibtex]

Conference Articles

  1. Synchronous Programming of Device Drivers for Global Resource Control in Embedded Operating Systems. Nicolas Berthier, Florence Maraninchi, Laurent Mounier - ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools and Theory for Embedded Systems (LCTES) - [bibtex]
  2. Improving Strategies via SMT Solving. Thomas Gawlitza, David Monniaux - ESOP - PDF - [bibtex]
  3. Faithfulness Considerations for Virtual Prototyping of Systems-on-Chip. Giovanni Funchal, Matthieu Moy, Laurent Maillet-Contoz, Florence Maraninchi - 3rd Workshop on: Rapid Simulation and Performance Evaluation: Methods and Tools (RAPIDO) - PDF - [bibtex]
  4. Hybridization Domain Construction using Curvature Estimation. Thao Dang, Romain Testylier - Proceedings HSCC 2011 - PDF - [bibtex]
  5. jTLM: an Experimentation Framework for the Simulation of Transaction-Level Models of Systems-on-Chip. Giovanni Funchal, Matthieu Moy - Design, Automation and Test in Europe (DATE) - PDF - [bibtex]
  6. Efficient and Playful Tools to Teach Unix to New Students. Matthieu Moy - 16th Annual Conference on Innovation and Technology in Computer Science Education ITiCSE - [bibtex]
  7. Information Flow Control of Component-based Distributed Systems. Takoua Abdellatif, Lilia Sfaxi, Riadh Robbana, Yassine Lakhnech - Concurrency and Computation, Practice and Experience - [bibtex]
  8. Offset-Aware Mutation based Fuzzing for Buffer Overflow Vulnerabilities: Few Preliminary Results. Sanjay Rawat, Laurent Mounier - Proc. of The Second International Workshop on Security Testing (SECTEST) - PDF - [bibtex]
  9. A refinement methodology for object-oriented programs. Asma Tafat, Sylvain Boulmé, Claude Marché - Formal Verification of Object-Oriented Software - [bibtex]
  10. Synthesizing Systems with Optimal Average-Case Behavior for Ratio Objectives. Christian von Essen, Barbara Jobstmann - International Workshop on Interactions, Games and Protocols - [bibtex]
  11. Designing a CPU model: from a pseudo-formal document to fast code. Frédéric Blanqui, Claude Helmstetter, Vania Joloboff, Jean-François Monin, Xiaomu Shi - Proceedings of the 3rd Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools - [bibtex]
  12. On Universal Search Strategies for Multi-criteria Optimization Using Weighted Sums. Julien Legriel, Scott Cotton, Oded Maler - CEC - PDF - [bibtex]
  13. Meeting Deadlines Cheaply. Julien Legriel, Oded Maler - ECRTS - PDF - [bibtex]
  14. Coordination de Comités Instantanément Stabilisante. Borzoo Bonakdarpour, Stéphane Devismes, Franck Petit - Algotel - [bibtex]
  15. Routage par marche aléatoire à listes tabous. Karine Altisen, Stéphane Devismes, Pascal Lafourcade, Clément Ponsonnet - Algotel - [bibtex]
  16. SpaceEx: Scalable Verification of Hybrid Systems. Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, Oded Maler - Proc. 23rd International Conference on Computer Aided Verification (CAV) - PDF - [bibtex]
  17. Modeling of Time in Discrete-Event Simulation of Systems-on-Chip. Giovanni Funchal, Matthieu Moy - ACM/IEEE Ninth International Conference on Formal Methods and Models for Codesign MEMOCODE - [bibtex]
  18. AreaCast : une communication par zone dans les réseaux de capteurs sans fil. Karel Heurtefeux, Florence Maraninchi, Fabrice Valois - 13 èmes Rencontres Francophones sur les Aspects Algorithmiques de Télécommunications (AlgoTel) - PDF - [bibtex]
  19. Using bounded model checking to focus fixpoint iterations. David Monniaux, Laure Gonnord - Static analysis (SAS) - PDF - [bibtex]
  20. AreaCast: a Cross-Layer Approach for a Communication by Area in Wireless Sensor Networks. Karel Heurtefeux, Florence Maraninchi, Fabrice Valois - 17th IEEE International Conference on networks - [bibtex]
  21. Cache related pre-emption delay aware response time analysis for fixed priority pre-emptive systems. Sebastian Altmeyer, Robert I. Davis, Claire Maiza - Proceedings of the 32nd IEEE Real-Time Systems Symposium (RTSS) - [bibtex]
  22. A framework for the timing analysis of dynamic branch predictors. Claire Maiza, Christine Rochange - Proceedings of the 19th International Conference on Real-Time and Network Systems (RTNS2011) - PDF - [bibtex]
  23. Contract-Based Reasoning for Component Systems with Complex Interactions. Susanne Graf, Roberto Passerone, Sophie Quinton - TIMOBD'11 - [bibtex]
  24. Methods and tools for component-based system design. Joseph Sifakis - Design, Automation and Test in Europe, DATE 2011, Grenoble, France, March 14-18, 2011 - [bibtex]
  25. Synthesizing Glue Operators from Glue Constraints for the Construction of Component-Based Systems. Simon Bliudze, Joseph Sifakis - Software Composition - 10th International Conference, SC 2011, Zurich, Switzerland, June 30 - July 1, 2011. Proceedings - [bibtex]
  26. Automating information flow control in component-based distributed systems. Takoua Abdellatif, Lilia Sfaxi, Riadh Robbana, Yassine Lakhnech - Proceedings of the 14th International ACM Sigsoft Symposium on Component Based Software Engineering, CBSE 2011, part of Comparch '11 Federated Events on Component-Based Software Engineering and Softwa - [bibtex]
  27. Beyond Provable Security Verifiable IND-CCA Security of OAEP. Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella Béguelin - Topics in Cryptology - CT-RSA 2011 - The Cryptographers' Track at the RSA Conference 2011, San Francisco, CA, USA, February 14-18, 2011. Proceedings - [bibtex]
  28. A Formal Approach for Incremental Construction with an Application to Autonomous Robotic Systems. Saddek Bensalem, Lavindra de Silva, Andreas Griesmayer, Felix Ingrand, Axel Legay, Rongjie Yan - Software Composition - 10th International Conference, SC 2011, Zurich, Switzerland, June 30 - July 1, 2011. Proceedings - [bibtex]
  29. Stratified Static Analysis Based on Variable Dependencies. David Monniaux, Julien Le Guen - Third International Workshop on Numerical and Symbolic Abstract Domains - PDF - [bibtex]
  30. Modular Abstractions of Reactive Nodes using Disjunctive Invariants. David Monniaux, Martin Bodin - Programming Languages and Systems (APLAS) - PDF - [bibtex]
  31. On the Generation of Positivstellensatz Witnesses in Degenerate Cases. David Monniaux, Pierre Corbineau - Interactive Theorem Proving (ITP) - PDF - [bibtex]
  32. Practical Privacy-Preserving Multiparty Linear Programming Based on Problem Transformation. Jannik Dreier, Florian Kerschbaum - Proceedings of the Third IEEE International Conference on Information Privacy, Security, Risk and Trust and Third IEEE International Conference on Social Computing (PASSAT/SocialCom'11) - [bibtex]
  33. On Under-Determined Dynamical Systems. Oded Maler - EMSOFT - PDF - [bibtex]
  34. Automated distributed implementation of component-based models with priorities. Borzoo Bonakdarpour, Marius Bozga, Jean Quilbeuf - Proceedings of the 11th International Conference on Embedded Software, EMSOFT 2011, part of the Seventh Embedded Systems Week, ESWeek 2011, Taipei, Taiwan, October 9-14, 2011 - [bibtex]
  35. Causality closure for a new class of curves in real-time calculus. Karine Altisen, Matthieu Moy - Proceedings of the 1st International Workshop on Worst-Case Traversal Time - [bibtex]
  36. Self-Stabilizing Small k-Dominating Sets. Ajoy Kumar Datta, Stéphane Devismes, Karel Heurtefeux, Lawrence L. Larmore, Yvan Rivierre - The Second International Conference on Networking and Computing (ICNC'11) - [bibtex]
  37. Sorting on Skip Chains. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore - Proceedings of PDAA'2011, 3rd International Workshop on Parallel and Distributed Algorithms and Applications - [bibtex]
  38. Multi-resource Allocation with Unknown Participants.. Ajoy Kumar Datta, Stéphane Devismes, Maria Gradinariu Potop-Butucaru, François Kawala, Lawrence L. Larmore - PDAA'2011, 3rd International Workshop on Parallel and Distributed Algorithms and Applications - [bibtex]
  39. Performance Evaluation of Schedulers in a Probabilistic Setting. Jean-Francois Kempf, Marius Bozga, Oded Maler - FORMATS - [bibtex]
  40. Efficient Encoding of SystemC/TLM in Promela. Kevin Marquet, Matthieu Moy, Bertrand Jeannet - DATICS-IMECS - [bibtex]
  41. Model-based design and distributed implementation of bus arbiter for multiprocessors. Imene Ben Hafaiedh, Susanne Graf, Mohamad Jaber - 18th IEEE International Conference on Electronics, Circuits and Systems, ICECS 2011, Beirut, Lebanon, December 11-14, 2011 - [bibtex]
  42. Distributed Implementation of Systems with Multiparty Interactions and Priorities. Imene Ben Hafaiedh, Susanne Graf, Nejla Mazouz - Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings - [bibtex]
  43. Monitoring Distributed Systems Using Knowledge. Susanne Graf, Doron Peled, Sophie Quinton - Formal Techniques for Distributed Systems - Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011, and 31st IFIP WG 6.1 International Conference, FORTE 2011, Reykjavik, Iceland, June 6-9, 2011. - [bibtex]
  44. Finding Software Vulnerabilities by Smart Fuzzing. Sofia Bekrar, Chaouki Bekrar, Roland Groz, Laurent Mounier - IEEE Fourth International Conference on Software Testing, Verification and Validation, ICST 2011, Berlin, Germany, 21-25 March 2011 - [bibtex]
  45. Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience. Pierre Corbineau, Mathilde Duclos, Yassine Lakhnech - Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings - [bibtex]
  46. D-Finder 2: Towards Efficient Correctness of Incremental Design. Saddek Bensalem, Andreas Griesmayer, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan - NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings - [bibtex]
  47. Time-predictable and composable architectures for dependable embedded systems. Saddek Bensalem, Kees Goossens, Christoph Kirsch, Roman Obermaisser, Edward A. Lee, Joseph Sifakis - Proceedings of the 11th International Conference on Embedded Software, EMSOFT 2011, part of the Seventh Embedded Systems Week, ESWeek 2011, Taipei, Taiwan, October 9-14, 2011 - [bibtex]
  48. Rigorous System Design: The BIP Approach. Ananda Basu, Saddek Bensalem, Marius Bozga, Paraskevas Bourgos, Joseph Sifakis - Mathematical and Engineering Methods in Computer Science - 7th International Doctoral Workshop, MEMICS 2011, Lednice, Czech Republic, October 14-16, 2011, Revised Selected Papers - [bibtex]
  49. Efficient deadlock detection for concurrent systems. Saddek Bensalem, Andreas Griesmayer, Axel Legay, Thanh-Hung Nguyen, Doron Peled - 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011, Cambridge, UK, 11-13 July, 2011 - [bibtex]
  50. Rigorous system level modeling and analysis of mixed HW/SW systems. Paraskevas Bourgos, Ananda Basu, Marius Bozga, Saddek Bensalem, Joseph Sifakis, Kai Huang - 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011, Cambridge, UK, 11-13 July, 2011 - [bibtex]
  51. Runtime Verification of Component-Based Systems. Ylies Falcone, Mohamad Jaber, Thanh-Hung Nguyen, Marius Bozga, Saddek Bensalem - Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings - [bibtex]
  52. Model Construction and Priority Synthesis for Simple Interaction Systems. Chih-Hong Cheng, Saddek Bensalem, Barbara Jobstmann, Rongjie Yan, Alois Knoll, Harald Ruess - NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings - [bibtex]
  53. QUASY: Quantitative Synthesis Tool. Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh - Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS - [bibtex]
  54. On the Hardness of Priority Synthesis. Chih-Hong Cheng, Barbara Jobstmann, Christian Buckl, Alois Knoll - Implementation and Application of Automata - 16th International Conference, CIAA 2011, Blois, France, July 13-16, 2011. Proceedings - [bibtex]
  55. Algorithms for Synthesizing Priorities in Component-Based Systems. Chih-Hong Cheng, Saddek Bensalem, Yu-Fang Chen, Rongjie Yan, Barbara Jobstmann, Harald Ruess, Christian Buckl, Alois Knoll - Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings - [bibtex]
  56. Specification-centered robustness. Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann - Industrial Embedded Systems (SIES), 2011 6th IEEE International Symposium on, Vasteras, Sweden, 15-17 June, 2011 - [bibtex]
  57. A Computational Indistinguishability Logic for the Bounded Storage Model. Gilles Barthe, Mathilde Duclos, Yassine Lakhnech - Foundations and Practice of Security - [bibtex]
  58. A Theory of Fault Recovery for Component-Based Models. Borzoo Bonakdarpour, Marius Bozga, Gregor Göessler - 30th IEEE Symposium on Reliable Distributed Systems (SRDS 2011), Madrid, Spain, October 4-7, 2011 - [bibtex]
  59. Définition des responsabilités pour les dysfonctionnements de logiciels : cadre contractuel et outils de mise en oeuvre.. Sylvain Steer, Nicolas Craipeau, Daniel Le Métayer, Manuel Maareck, Marie-Laure Potet, Valérie Viet Triem Tong - Droit, sciences et techniques : quelles responsabilités ? colloque international du Réseau Droit, sciences et techniques. - [bibtex]
  60. Monitoring Dynamical Signals While Testing Timed Aspects of a System. Goran Frehse, Kim Guldstrand Larsen, Marius Mikucionis, Brian Nielsen - ICTSS - [bibtex]
  61. Snap-Stabilizing Committee Coordination. Borzoo Bonakdarpour, Stéphane Devismes, Franck Petit - IPDPS'2011, 25th IEEE International Parallel and Distributed Processing Symposium - [bibtex]
  62. Self-Stabilizing Labeling and Ranking in Ordered Trees. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore, Yvan Rivierre - SSS'2011, 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems - [bibtex]
  63. Brief Announcement: Sorting on Skip Chains. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore - SSS'2011, 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems - [bibtex]
  64. Algorithme auto-stabilisant construisant un ensemble k-dominant minimal borné. Ajoy Kumar Datta, Stéphane Devismes, Karel Heurtefeux, Lawrence L. Larmore, Yvan Rivierre - 20èmes Rencontres francophones du Parallélisme - PDF - [bibtex]
  65. Vote-Independence: A Powerful Privacy Notion for Voting Protocols. Jannik Dreier, Pascal Lafourcade, Yassine Lakhnech - Foundations and Practice of Security - 4th Canada-France MITACS Workshop, FPS 2011, Paris, France, May 12-13, 2011, Revised Selected Papers - [bibtex]
  66. Template-Based Unbounded Time Verification of Affine Hybrid Automata. Thao Dang, Thomas Gawlitza - APLAS - [bibtex]
  67. Discretizing Affine Hybrid Automata with Uncertainty. Thao Dang, Thomas Gawlitza - ATVA - [bibtex]
  68. Component Assemblies in the Context of Manycore. Ananda Basu, Saddek Bensalem, Marius Bozga, Paraskevas Bourgos, Mayur Maheshwari, Joseph Sifakis - Formal Methods for Components and Objects, 10th International Symposium, FMCO 2011, Turin, Italy, October 3-5, 2011, Revised Selected Papers - [bibtex]
  69. Correct Implementation of Open Real-Time Systems. Tesnim Abdellatif, Jacques Combaz, Marc Poulhiès - 37th EUROMICRO Conference on Software Engineering and Advanced Applications, SEAA 2011, Oulu, Finland, August 30 - September 2, 2011 - [bibtex]
  70. Politiques de gestion de protections pour l'implémentation de sections critiques.. Sifakis Emmanuel, Mounier Laurent - Actes des Rencontres du Parallélisme (RenPar) - [bibtex]
  71. Benaloh's Dense Probabilistic Encryption Revisited. Laurent Fousse, Pascal Lafourcade, Mohamed Alnuaimi - Progress in Cryptology - AFRICACRYPT 2011 - 4th International Conference on Cryptology in Africa, Dakar, Senegal, July 5-7, 2011. Proceedings - [bibtex]

PhD Thesis and HDR

  1. Design, Verification and Implementation of Systems of Components. Sophie Quinton - [bibtex]
  2. Component-based Systems: from Design to Implementation. Imene Ben-Hafaiedh - [bibtex]
  3. Multi-Criteria Optimization and its Application to Multi-Processor Embedded Systems. Julien Legriel - [bibtex]
  4. Contributions to the Transaction-Level Modeling of Systems-on-a-Chip. Giovanni Funchal - [bibtex]
  5. Modélisation des systèmes synchrones en BIP. Vassiliki Sfyrla - [bibtex]

2010

Journal Articles

  1. Stabilizing leader election in partial synchronous systems with crash failures. Carole Delporte-Gallet, Stéphane Devismes, Hugues Fauconnier - J. Parallel Distrib. Comput. - [bibtex]
  2. Automatic Modular Abstractions for Template Numerical Constraints. David Monniaux - Logical Methods in Computer Science - PDF - [bibtex]
  3. Snap-Stabilization in Message-Passing Systems. Sylvie Delaët, Stéphane Devismes, Mikhail Nesterenko, Sébastien Tixeuil - Journal of Parallel and Distributed Computing (JPDC) - [bibtex]
  4. Controle de flux d?Information des systemes distribues a base de composants. Takoua Abdellatif, Lilia Sfaxi, Yassine Lakhnech - NOTERE IEEE - [bibtex]
  5. On Simulation-Based Probabilistic Model-Checking of Mixed-Analog Circuits. Edmund M. Clarke, Alexandre Donzé, Axel Legay - Formal Methods in System Design - [bibtex]
  6. Parameter Synthesis in Nonlinear Dynamical Systems: Application to Systems Biology. Alexandre Donzé, Gilles Clermont, Christopher James Langmead - Journal of Computational Biology - [bibtex]
  7. A Self-Stabilizing 3-Approximation for the Maximum Leaf Spanning Tree Problem in Arbitrary Networks. Stéphane Devismes, Hirotsugu Kakugawa, Sayaka Kamei, Sébastien Tixeuil - Journal of Combinatorial Optimization (Special Issue) - [bibtex]
  8. Compositional verification for component-based systems and application. Saddek Bensalem, Marius Bozga, Thanh-Hung Nguyen, Joseph Sifakis - IET Software - [bibtex]
  9. Causal semantics for the algebra of connectors. Simon Bliudze, Joseph Sifakis - Formal Methods in System Design - [bibtex]
  10. 2009 CAV award announcement. Randal E. Bryant, Orna Grumberg, Joseph Sifakis, Moshe Y. Vardi - Formal Methods in System Design - [bibtex]
  11. Source-to-Source Architecture Transformation for Performance Optimization in BIP. Marius Bozga, Mohamad Jaber, Joseph Sifakis - IEEE Trans. Industrial Informatics - [bibtex]
  12. Detection of deadlock potentials in multithreaded programs. Rahul Agarwal, Saddek Bensalem, Eitan Farchi, Klaus Havelund, Yarden Nir-Buchbinder, Scott D. Stoller, Shmuel Ur, Liqiang Wang - IBM Journal of Research and Development - [bibtex]
  13. Automata-based verification of programs with tree updates. Peter Habermehl, Radu Iosif, Tomás Vojnar - Acta Inf. - [bibtex]
  14. Quantitative Separation Logic and Programs with Lists. Marius Bozga, Radu Iosif, Swann Perarnau - J. Autom. Reasoning - [bibtex]

Conference Articles

  1. Arrival Curves for Real-Time Calculus: the Causality Problem and its Solutions. Karine Altisen, Matthieu Moy - TACAS - [bibtex]
  2. An analysis of permutations in arrays. Valentin Perrelle, Nicolas Halbwachs - 11th International Conference on Verification, Model-checking, and Abstract Interpretation, VMCAI 2010 - [bibtex]
  3. Liability in software Engineering. Daniel Le Métayer, Manuel Maarek, Eduardo Mazza, Marie-Laure Potet, Stéphane Frénot, Valérie Viet Triem Tong, Nicolas Craipeau, Ronan Hardouin - ICSE 2010, International Conference on Software Engineering - [bibtex]
  4. Performance Evaluation of Components Using a Granularity-based Interface Between Real-Time Calculus and Timed Automata. Karine Altisen, Yanhong Liu, Matthieu Moy - Eighth Workshop on Quantitative Aspects of Programming Languages (QAPL) - [bibtex]
  5. Algorithms For Extracting Timeliness Graphs. Stéphane Devismes, Carole Delporte-Gallet, Hugues Fauconnier, Mikel Larrea - 17th International Colloquium on Structural Information and Communication Complexity (SIROCCO 2010) - [bibtex]
  6. A Theoretical and Experimental Review of SystemC Front-ends. Kevin Marquet, Matthieu Moy, Bageshri Karkare - Forum for Design Languages (FDL) - [bibtex]
  7. A Self-Stabilizing 3-Approximation for the Maximum Leaf Spanning Tree Problem in Arbitrary Networks. Stéphane Devismes, Hirotsugu Kakugawa, Sayaka Kamei, Sébastien Tixeuil - COCOON 2010, The 16th Annual International Computing and Combinatorics Conference - [bibtex]
  8. Taint Dependency Sequences: A Characterization of Insecure Execution Paths Based on Input-Sensitive Cause Sequences. Dumitru Ceara, Laurent Mounier, Marie-Laure Potet - ICSTW '10: Proceedings of the 2010 Third International Conference on Software Testing, Verification, and Validation Workshops - [bibtex]
  9. Designing Log Architecture For Legal Evidence. Daniel Le Métayer, Eduardo Mazza, Marie-Laure Potet - Software Engineering And Formal Methods (SEFM) - [bibtex]
  10. Synthesis for regular specifications over unbounded domains. Jad Hamza, Barbara Jobstmann, Viktor Kuncak - Conference on Formal Methods in Computer Aided Design, FMCAD 2010, Lugano, CH - [bibtex]
  11. Robustness in the Presence of Liveness. Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann - Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010 - [bibtex]
  12. Measuring and Synthesizing Systems in Probabilistic Environments. Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh - Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010 - [bibtex]
  13. Gist: A Solver for Probabilistic Games. Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Arjun Radhakrishna - Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010 - [bibtex]
  14. A Unifying View Of Loosely Time-Triggered Architectures. Albert Benveniste, Anne Bouillard, Paul Caspi - International Conference on Embedded Software International Conference on Embedded Software - [bibtex]
  15. Approximation of $\delta$-timeliness. Carole Delporte-Gallet, Stéphane Devismes, Hugues Fauconnier - 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2010) - [bibtex]
  16. Communications Efficaces et Auto-Stabilisation. Stéphane Devismes, Toshimitsu Masuzawa, Sébastien Tixeuil - 12èmes Rencontres Francophones sur les Aspects Algorithmiques de Télécommunications (Algotel 2010) - [bibtex]
  17. Rendez-vous d'agents amnésiques. Fabienne Carrier, Stéphane Devismes, Franck Petit, Yvan Rivierre - 12èmes Rencontres Francophones sur les Aspects Algorithmiques de Télécommunications (Algotel 2010) - [bibtex]
  18. Reasoning about Safety and Progress Using Contracts. Imene Ben-Hafaiedh, Susanne Graf, Sophie Quinton - Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings - [bibtex]
  19. Achieving Distributed Control through Model Checking. Susanne Graf, Doron Peled, Sophie Quinton - Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings - [bibtex]
  20. Contract-Based Reasoning about Progress: Application to Resource Sharing in a Network. Imene Ben-Hafaiedh, Susanne Graf, Sophie Quinton - Proc. of FLACOS'10 - [bibtex]
  21. Implementing Distributed Controllers for Systems with Priorities. Imene Ben-Hafaiedh, Susanne Graf, Hammadi Khairallah - Proceedings Ninth International Workshop on the Foundations of Coordination Languages and Software Architectures, FOCLASA - [bibtex]
  22. More Testable Properties. Ylies Falcone, Jean-Claude Fernandez, Thierry Jéron, Hervé Marchand, Laurent Mounier - Proceedings of ICTSS - 22nd IFIP WG 6.1 International Conference - PDF - [bibtex]
  23. An Evolutionary Computing Approach for Hunting Buffer Overflow Vulnerabilities: A case of aiming in dim light. Sanjay Rawat, Laurent Mounier - Proceedings of 6th EC2ND (European Conference on Computer Network Defense - [bibtex]
  24. ac2lus: Bringing SMT-solving and Abstract Interpretation Techniques to Real-Time Calculus through the Synchronous Language Lustre. Karine Altisen, Matthieu Moy - 22nd Euromicro Conference on Real-Time Systems (ECRTS) - PDF - [bibtex]
  25. Property-Based Monitoring of Analog and Mixed-Signal Systems. John Havlicek, Scott Little, Oded Maler, Dejan Nickovic - Formal Modeling and Analysis of Timed Systems - 8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings - [bibtex]
  26. On the Krohn-Rhodes Cascaded Decomposition Theorem. Oded Maler - Time for Verification, Essays in Memory of Amir Pnueli - PDF - [bibtex]
  27. Robust Satisfaction of Temporal Logic over Real-Valued Signals. Alexandre Donzé, Oded Maler - Formal Modeling and Analysis of Timed Systems - 8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings - PDF - [bibtex]
  28. Amir Pnueli and the dawn of hybrid systems. Oded Maler - Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010 - PDF - [bibtex]
  29. On Zone-Based Analysis of Duration Probabilistic Automata. Oded Maler, Kim Guldstrand Larsen, Bruce H. Krogh - Proceedings 12th International Workshop on Verification of Infinite-State Systems - PDF - [bibtex]
  30. Using Redundant Constraints for Refinement. Eugène Asarin, Thao Dang, Oded Maler, Romain Testylier - Automated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings - [bibtex]
  31. Computational indistinguishability logic. Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech - ACM Conference on Computer and Communications Security - [bibtex]
  32. Approximating the Pareto Front of Multi-criteria Optimization Problems. Julien Legriel, Colas Le Guernic, Scott Cotton, Oded Maler - Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2 - PDF - [bibtex]
  33. A Formal Framework for Specifying and Analyzing Logs as Electronic Evidence. Eduardo Mazza, Marie-Laure Potet, Daniel Le Métayer - 13th Brazilian Symposium of Formal Methods (SBMF) - [bibtex]
  34. Probabilistic Self-Stabilizing Vertex Coloring in Unidirectional Anonymous Networks. Samuel Bernard, Stéphane Devismes, Maria Gradinariu Potop-Butucaru, Katy Paroux, Sébastien Tixeuil - ICDCN'2010, 11th International Conference on Distributed Computing and Networking - [bibtex]
  35. Accurate hybridization of nonlinear systems. Thao Dang, Oded Maler, Romain Testylier - Proceedings of HSCC 2010 - PDF - [bibtex]
  36. Proof Trick: Small Inversions. Jean-François Monin - Second Coq Workshop - [bibtex]
  37. Quantifier elimination by lazy model enumeration. David Monniaux - Computer-aided verification (CAV) - PDF - [bibtex]
  38. Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems. Alexandre Donzé - CAV - [bibtex]
  39. Optimal Exploration of Small Rings. Stéphane Devismes - WRAS'2010, Third International ACM SIGOPS/SIGACT Workshop on Reliability, Availability, and Security - [bibtex]
  40. Incremental component-based construction and verification using invariants. Saddek Bensalem, Marius Bozga, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan - Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23 - [bibtex]
  41. Incremental Invariant Generation for Compositional Design. Saddek Bensalem, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan - 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2010, Taipei, Taiwan, 25-27 August 2010 - [bibtex]
  42. Knowledge Based Scheduling of Distributed Systems. Saddek Bensalem, Doron Peled, Joseph Sifakis - Time for Verification, Essays in Memory of Amir Pnueli - [bibtex]
  43. Model-based implementation of real-time applications. Tesnim Abdellatif, Jacques Combaz, Joseph Sifakis - Proceedings of the 10th International conference on Embedded software, EMSOFT 2010, Scottsdale, Arizona, USA, October 24-29, 2010 - [bibtex]
  44. From high-level component-based models to distributed implementations. Borzoo Bonakdarpour, Marius Bozga, Mohamad Jaber, Jean Quilbeuf, Joseph Sifakis - Proceedings of the 10th International conference on Embedded software, EMSOFT 2010, Scottsdale, Arizona, USA, October 24-29, 2010 - [bibtex]
  45. Automated Conflict-free distributed implementation of component-based models. Borzoo Bonakdarpour, Marius Bozga, Mohamad Jaber, Jean Quilbeuf, Joseph Sifakis - IEEE Fifth International Symposium on Industrial Embedded Systems - SIES 2010, University of Trento, Italy, July 7-9, 2010 - [bibtex]
  46. Component-based Construction of Heterogeneous Real-time Systems in BIP. Joseph Sifakis - The Future of Software Engineering - [bibtex]
  47. Embedded systems design - Scientific challenges and work directions. Joseph Sifakis - Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23 - [bibtex]
  48. Compositional Translation of Simulink Models into Synchronous BIP. Vassiliki Sfyrla, Georgios Tsiligiannis, Iris Safaka, Marius Bozga, Joseph Sifakis - IEEE Fifth International Symposium on Industrial Embedded Systems - SIES 2010, University of Trento, Italy, July 7-9, 2010 - [bibtex]
  49. Systematic Correct Construction of Self-stabilizing Systems: A Case Study. Ananda Basu, Borzoo Bonakdarpour, Marius Bozga, Joseph Sifakis - Stabilization, Safety, and Security of Distributed Systems - 12th International Symposium, SSS 2010, New York, NY, USA, September 20-22, 2010. Proceedings - [bibtex]
  50. Embedded Systems Design - Scientific Challenges and Work Directions. Joseph Sifakis - Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2 - [bibtex]
  51. Automated Proofs for Asymmetric Encryption. Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech - Concurrency, Compositionality, and Correctness, Essays in Honor of Willem-Paul de Roever - [bibtex]
  52. Statistical Model Checking: An Overview. Axel Legay, Benoît Delahaye, Saddek Bensalem - Runtime Verification - First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings - [bibtex]
  53. Privacy by Data Provenance with Digital Watermarking - A Proof-of-Concept Implementation for Medical Services with Electronic Health Records. Jérémie Tharaud, Sven Wohlgemuth, Isao Echizen, Noboru Sonehara, Günter Müller, Pascal Lafourcade - Sixth International Conference on Intelligent Information Hiding and Multimedia Signal Processing (IIH-MSP 2010), Darmstadt, Germany, 15-17 October, 2010, Proceedings - [bibtex]
  54. PinaVM: a SystemC Front-End Based on an Executable Intermediate Representation. Kevin Marquet, Matthieu Moy - International Conference on Embedded Software - [bibtex]
  55. On the Equality of Probabilistic Terms. Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech, Vincent Laporte - Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers - [bibtex]
  56. Fast Acceleration of Ultimately Periodic Relations. Marius Bozga, Radu Iosif, Filip Kone\vcn\'y - Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings - [bibtex]

PhD Thesis and HDR

  1. 42, A Component-Based Approach to Virtual Prototyping of Heterogeneous Embedded Systems. Tayeb Bouhadiba - PDF - [bibtex]
  2. Contributions à l'analyse statique de programmes manipulant des tableaux. Mathias Péron - PDF - [bibtex]
  3. Constructive Verification for Component-based Systems. Thanh-Hung Nguyen - [bibtex]
  4. Automatisation de la Certification Formelle de Systèmes Critiques par Instrumentation d'Interpréteurs Abstraits. Manuel Garnacho - [bibtex]

2009

Journal Articles

  1. Toward a More Dependable Software Architecture for Autonomous Robots. Saddek Bensalem, Matthieu Gallien, Felix Ingrand, Imen Kahloul, Thanh-Hung Nguyen - Special issue on Software Engineering for Robotics of the IEEE Robotics and Automation Magazine - [bibtex]
  2. Full Simulation Coverage for SystemC Transaction-Level Models of Systems-on-a-Chip. Claude Helmstetter, Florence Maraninchi, Laurent Maillet-Contoz - Formal Methods in System Design - [bibtex]
  3. Coverage-Guided Test Generation for Continuous and Hybrid Systems. Thao Dang, Tarik Nahhal - Formal Methods in System Design - [bibtex]
  4. Flush: an example of development by refinements in SCADE/Lustre. Jan Mikác, Paul Caspi - International Journal on Software Tools for Technology Transfer (STTT) - [bibtex]
  5. Meta-models in Europe: Languages, Tools and Applications. Roberto Passerone, Imene Ben-Hafaiedh, Susanne Graf, Albert Benveniste, Daniela Cancila, Arnaud Cuccuru, Sébastien Gérard, François Terrier, Werner Damm, Alberto Ferrari, Leonardo Mangeruca, Bernhard Josko, Thomas Peikenkamp, Alberto L. Sangiovanni-Vincentelli - IEEE Design & Test of Computers - [bibtex]
  6. A minimalistic look at widening operators. David Monniaux - Higher order and symbolic computation - PDF - [bibtex]
  7. Model checking: algorithmic verification and debugging. Edmund M. Clarke, Allen Emerson, Joseph Sifakis - Commun. ACM - [bibtex]
  8. Flat Parametric Counter Automata. Marius Bozga, Radu Iosif, Yassine Lakhnech - Fundam. Inform. - [bibtex]
  9. Convincing Proofs for Program Certification. Manuel Garnacho, Michaël Périn - Electronic Notes in Theoretical Computer Science - [bibtex]

Book Chapters (inbook)

  1. Model-based Design of Heterogeneous Systems. Stavros Tripakis, Thao Dang - [bibtex]

Book Chapters

  1. Relaxing Restrictions on Invariant Composition in the B method by Spec# ownership control à la Spec#. Sylvain Boulmé, Marie-Laure Potet - Rigorous Methods for Software Construction and Analysis - [bibtex]
  2. Tools for the verification of linear hybrid automata models. Goran Frehse - Handbook of Hybrid Systems Control, Theory -- Tools -- Applications - [bibtex]

Conference Articles

  1. Contract-Based Coordination of Hardware Components for the Development of Embedded Software. Tayeb Bouhadiba, Florence Maraninchi - COORDINATION'09, the 11th international conference on Coordination Models and Languages - [bibtex]
  2. Formal and Executable Contracts for Transaction-Level Modeling in SystemC. Tayeb Bouhadiba, Florence Maraninchi, Giovanni Funchal - ACM International Conference on Embedded Sofware (EMSOFT 09) - [bibtex]
  3. Prototyping of Distributed Embedded Systems Using AADL. Mohamed Yassin Chkouri, Marius Bozga - Model Based Architecting and Construction of Embedded Systems ACES-MB - [bibtex]
  4. Think: View-Based Support of Non-functional Properties in Embedded Systems. Matthieu Anne, Ruan He, Tahar Jarboui, Marc Lacoste, Olivier Lobry, Guirec Lorant, Maxime Louvel, Juan Navas, Vincent Olive, Juraj Polakovic, Marc Poulhiès, Jacques Pulou, Stéphane Seyvoz, Julien Tous, Thomas Watteyne - ICESS '09: Proceedings of the 2009 International Conference on Embedded Software and Systems - [bibtex]
  5. Model-Based Design of Embeded Control Systems with a Synchronous Intermediate Model. Mouaiad Alras, Paul Caspi, Alain Girault, Pascal Raymond - 6th IEEE International Conference on Embedded Systems and Software (ICESS-09) - [bibtex]
  6. Volume and Entropy of Regular Timed Languages: Discretization Approach. Eugène Asarin, Aldric Degorre - CONCUR - [bibtex]
  7. Sur le Coloriage Auto-stabilisant dans les Réseaux Unidirectionnels Anonymes. Samuel Bernard, Stéphane Devismes, Katy Paroux, Maria Gradinariu Potop-Butucaru, Sébastien Tixeuil - AlgoTel'09 - [bibtex]
  8. A Model-Based Design and Validation Approach with the OMEGA-UML Profile and the IF Toolset. Imene Ben-Hafaiedh, Olivier Constant, Susanne Graf, Riadh Robbana - 2nd Mediterranean Conference on Intelligent Systems and Automation, CISA 2009, March 23-25, Zarzis, Tunesia - [bibtex]
  9. Using Checker Predicates in Certifying Code Generation. Jan Olaf Blech, Benjamin Grégoire - Workshop on Compiler Optimization meets Compiler Verification (COCV) - [bibtex]
  10. Invariants and Robustness of BIP Models. Jan Olaf Blech, Thanh-Hung Nguyen, Michaël Périn - Workshop on Invariant Generation (WING) - [bibtex]
  11. Certifying Deadlock-freedom for BIP Models. Jan Olaf Blech, Michaël Périn - Software and Compilers for Embedded Systems (SCOPES) - [bibtex]
  12. Evaluating Design Trade-offs in Customizable Processors. Unmesh D. Bordoloi, Huynh Phung Huynh, Samarjit Chakraborty, Tulika Mitra - 46th Annual ACM IEEE Design Automation Conference - [bibtex]
  13. Designing Heterogeneous ECU Networks via Compact Architecture Encoding and Hybrid Timing Analysis. Michael Glaß, Martin Lukasiewycz, Jürgen Teich, Unmesh D. Bordoloi, Samarjit Chakraborty - 46th Annual ACM IEEE Design Automation Conference - [bibtex]
  14. A DECOMSYS Based Tool-Chain for Analyzing FlexRay based Automotive Control Applications. Dip Goswami, Pradeep Seshadri, Unmesh D. Bordoloi, Samarjit Chakraborty - IEEE Conference on Automation Science and Engineering -(CASE) - [bibtex]
  15. Space-Optimal Deterministic Rendezvous. Fabienne Carrier, Stéphane Devismes, Franck Petit, Yvan Rivierre - WRAS'09, Second International Workshop on Reliability, Availability, and Security (associated with PDCAT'09) - [bibtex]
  16. Comparing State Spaces in Automatic Protocol Analysis. Cas J. F. Cremers, Pascal Lafourcade, Philippe Nadeau - Formal to Practical Security - [bibtex]
  17. Image computation for polynomial dynamical systems using the Bernstein expansion. Thao Dang, David Salinas - Computer Aided Verification CAV'09 - [bibtex]
  18. Quand le consensus est plus simple que la diffusion fiable. Carole Delporte-Gallet, Stéphane Devismes, Hugues Fauconnier, Franck Petit, Sam Toueg - AlgoTel'09 - [bibtex]
  19. Self-Stabilizing k-out-of-l exclusion on tree networks. Ajoy Kumar Datta, Stéphane Devismes, Florian Horn, Lawrence L. Larmore - IPDPS'09, International Conference on Parallel and Distributed Processing Symposium - [bibtex]
  20. A Self-Stabilizing O(n)-Round k-Clustering Algorithm. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore - SRDS'09, 28th International Symposium on Reliable Distributed Systems - [bibtex]
  21. Snap-Stabilization in Message-Passing Systems. Sylvie Delaët, Stéphane Devismes, Mikhail Nesterenko, Sébastien Tixeuil - ICDCN, 10th International Conference on Distributed Computing and Networking - [bibtex]
  22. Stabilisation instantanée dans les systèmes à passage de messages. Sylvie Delaët, Stéphane Devismes, Mikhail Nesterenko, Sébastien Tixeuil - AlgoTel'09 - [bibtex]
  23. Communication Efficiency in Self-Stabilizing Silent Protocols. Stéphane Devismes, Toshimitsu Masuzawa, Sébastien Tixeuil - ICDCS'09, International Conference on Distributed Computing Systems - [bibtex]
  24. Parameter synthesis for hybrid systems with an application to simulink models. Alexandre Donzé, Bruce H. Krogh, Akshay Rajhans - Proceedings of the 12th International Conference on Hybrid Systems: Computation and Control (HSCC'09) - [bibtex]
  25. Parameter Synthesis in Nonlinear Dynamical Systems: Application to Systems Biology. Alexandre Donzé, Gilles Clermont, Christopher James Langmead, Axel Legay - Proceedings of the 13th Annual International Conference on Research in Computational Molecular Biology RECOMB'09 - [bibtex]
  26. Optimal Probabilistic Ring Exploration by Semi-synchronous Oblivious Robots. Stéphane Devismes, Franck Petit, Sébastien Tixeuil - Structural Information and Communication Complexity, 16th International Colloquium, SIROCCO 2009 - [bibtex]
  27. Exploration Optimale Probabiliste d'un Anneau par des Robots Semi-Synchrones et Amnésiques. Stéphane Devismes, Franck Petit, Sébastien Tixeuil - AlgoTel'09 - [bibtex]
  28. Synchronous Modeling and Validation of Priority Inheritance Schedulers. Erwan Jahier, Nicolas Halbwachs, Pascal Raymond - Fundamental Approaches to Software Engineering, FASE'09 - [bibtex]
  29. Modular Static Scheduling of Synchronous Data-flow Networks -- An efficient symbolic representation. Marc Pouzet, Pascal Raymond - International Conference on Embedded Software (EMSOFT'09) - [bibtex]
  30. Runtime Verification of Safety Progress Properties. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier - Runtime Verification 2009 - [bibtex]
  31. Enforcement Monitoring wrt. the Safety-Progress Classification of Properties. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier - Proceedings of the 24th Annual ACM Symposium on Applied Computing - Software Verification and Testing Track - [bibtex]
  32. Automated Proofs for Encryption Modes. Martin Gagne, Pascal Lafourcade, Yassine Lakhnech, Reihaneh Safavi - Workshop on Formal and Computational Cryptography, (FCC'09) - [bibtex]
  33. Actors without directors: A Kahnian view of heterogeneous systems. Paul Caspi, Albert Benveniste, Roberto Lublinerman, Stavros Tripakis - Hybrid Systems Computation and Control, HSCC09 - [bibtex]
  34. Deterministic data flow communication in AADL. Mohamed Yassin Chkouri, Marius Bozga - ICESS '09: Proceedings of the 2009 International Conference on Embedded Software and Systems Reachability Analysis of Hybrid Systems using Support Functions. Colas Le Guernic, Antoine Girard - CAV - [bibtex]
  35. Comparison of Cryptographic Verification Tools Dealing with Algebraic Properties. Pascal Lafourcade, Vanessa Terrade, Sylvain Vigier - sixth International Workshop on Formal Aspects in Security and Trust, (FAST'09) - [bibtex]
  36. Polyhedral Domains and Widening for Verification of Numerical Programs. Hitashyam Maka, Goran Frehse, Bruce H. Krogh - NSV-II: Second International Workshop on Numerical Software Verification - [bibtex]
  37. Prudent engineering practices to prevent type-flaw attacks under algebraic properties. Sreekanth Malladi, Pascal Lafourcade - Workshop on Security and Rewriting Techniques, (SecReT'09) - [bibtex]
  38. Synchronous Objects with Scheduling Policies, Introducing safe shared memory in Lustre. Paul Caspi, Jean-louis Colaço, Léonard Gérard, Marc Pouzet, Pascal Raymond - ACM SIGPLAN/SIGBED 2009 Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2009) - [bibtex]
  39. Synthesizing robust systems. Roderick Bloem, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann - Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA - [bibtex]
  40. Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form. Loïc Besnard, Thierry Gautier, Matthieu Moy, Jean-Pierre Talpin, Kenneth Johnson, Florence Maraninchi - Ninth International Workshop on Automated Verification of Critical Systems (AVOCS'09) - [bibtex]
  41. From Orchestration to Choreography: Memoryless and Distributed Orchestrators. Sophie Quinton, Imene Ben-Hafaiedh, Susanne Graf - Proc. of FLACOS'09 - [bibtex]
  42. Model Based Architecting and Construction of Embedded Systems. Iulian Ober, Stefan Van Baelen, Susanne Graf, Mamoun Filali, Thomas Weigert, Sébastien Gérard - Models in Software Engineering, Workshops and Symposia at MODELS 2008, Toulouse, France, September 28 - October 3, 2008. Reports and Revised Selected Papers - [bibtex]
  43. Reachability for Continuous and Hybrid Systems. Oded Maler - Reachability Problems, 3rd International Workshop, RP 2009, Palaiseau, France, September 23-25, 2009. Proceedings - [bibtex]
  44. On Omega-Languages Defined by Mean-Payoff Conditions. Rajeev Alur, Aldric Degorre, Oded Maler, Gera Weiss - FOSSACS - PDF - [bibtex]
  45. Computing Reachable States for Nonlinear Biological Models. Thao Dang, Colas Le Guernic, Oded Maler - Computational Methods in Systems Biology, 7th International Conference, CMSB 2009, Bologna, Italy, August 31-September 1, 2009. Proceedings - [bibtex]
  46. Design Principles for an Extendable Verification Tool for Hybrid Systems. Goran Frehse, Rajarshi Ray - Proceedings of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2009) - [bibtex]
  47. Comparing State Spaces in Automatic Security Protocol Analysis. Cas J. F. Cremers, Pascal Lafourcade, Philippe Nadeau - Formal to Practical Security - Papers Issued from the 2005-2008 French-Japanese Collaboration - [bibtex]
  48. Optimal deterministic self-stabilizing vertex coloring in unidirectional anonymous networks. Samuel Bernard, Stéphane Devismes, Maria Gradinariu Potop-Butucaru, Sébastien Tixeuil - IPDPS '09: Proceedings of the 2009 IEEE International Symposium on Parallel&Distributed Processing - [bibtex]
  49. D-Finder: A Tool for Compositional Deadlock Detection and Verification. Saddek Bensalem, Marius Bozga, Thanh-Hung Nguyen, Joseph Sifakis - Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings - [bibtex]
  50. Source-to-source architecture transformation for performance optimization in BIP. Marius Bozga, Mohamad Jaber, Joseph Sifakis - IEEE Fourth International Symposium on Industrial Embedded Systems - SIES 2009, Ecole Polytechnique Federale de Lausanne, Switzerland, July 8 - 10, 2009 - [bibtex]
  51. Priority Scheduling of Distributed Systems Based on Model Checking. Ananda Basu, Saddek Bensalem, Doron Peled, Joseph Sifakis - Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings - [bibtex]
  52. Component-Based Construction of Heterogeneous Real-Time Systems in Bip. Joseph Sifakis - Applications and Theory of Petri Nets, 30th International Conference, PETRI NETS 2009, Paris, France, June 22-26, 2009. Proceedings - [bibtex]
  53. Component-Based Construction of Real-Time Systems in BIP. Joseph Sifakis - Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings - [bibtex]
  54. Embedded systems design - Scientific challenges and work directions. Joseph Sifakis - Design, Automation and Test in Europe, DATE 2009, Nice, France, April 20-24, 2009 - [bibtex]
  55. The Quest for Correctness-Beyond a Posteriori Verification. Joseph Sifakis - Model Checking Software, 16th International SPIN Workshop, Grenoble, France, June 26-28, 2009. Proceedings - [bibtex]
  56. Brief Announcement: Incremental Component-Based Modeling, Verification, and Performance Evaluation of Distributed Reset. Ananda Basu, Borzoo Bonakdarpour, Marius Bozga, Joseph Sifakis - Distributed Computing, 23rd International Symposium, DISC 2009, Elche, Spain, September 23-25, 2009. Proceedings - [bibtex]
  57. On using floating-point computations to help an exact linear arithmetic decision procedure. David Monniaux - Computer-aided verification (CAV) - PDF - [bibtex]
  58. Automatic Modular Abstractions for Linear Constraints. David Monniaux - POPL (Principles of programming languages) - PDF - [bibtex]
  59. Compositional Timing Analysis. Ramzi Ben Salah, Marius Bozga, Oded Maler - EMSOFT - [bibtex]
  60. Automatic Verification of Integer Array Programs. Marius Bozga, Peter Habermehl, Radu Iosif, Filip Kone\vcn\'y, Tomás Vojnar - Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings - [bibtex]
  61. Iterating Octagons. Marius Bozga, Codruta G\^\irlea, Radu Iosif - Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2 - [bibtex]
  62. "Certfication of Smart-Card Applications in Common Criteria: Proving Representation Correspondences". Iman Narasamdya, Michaël Périn - Fundamental Approaches to Software Engineering - [bibtex]
  63. "Certfication of Smart-Card Applications in Common Criteria". Iman Narasamdya, Michaël Périn - ACM Symposium on Applied Computing - [bibtex]
  64. Formal Indistinguishability Extended to the Random Oracle Model. Cristian Ene, Yassine Lakhnech, Van Chan Ngo - Computer Security - ESORICS 2009, 14th European Symposium on Research in Computer Security, Saint-Malo, France, September 21-23, 2009. Proceedings - [bibtex]
  65. Automata-Based Termination Proofs. Radu Iosif, Adam Rogalewicz - Implementation and Application of Automata, 14th International Conference, CIAA 2009, Sydney, Australia, July 14-17, 2009. Proceedings - [bibtex]
  66. Modeling synchronous systems in BIP. Marius Bozga, Vassiliki Sfyrla, Joseph Sifakis - Proceedings of the 9th ACM & IEEE International conference on Embedded software, EMSOFT 2009, Grenoble, France, October 12-16, 2009 - [bibtex]

PhD Thesis and HDR

  1. On Some Problems in Satisfiability Solving. Scott Cotton - [bibtex]
  2. Study and Implementation of Runtime Validation Techniques. Ylies Falcone - [bibtex]
  3. Analyse statique : de la théorie à la pratique. David Monniaux - Habilitation to direct research - [bibtex]

2008

Journal Articles

  1. Symbolic protocol analysis for monoidal equational theories. Stéphanie Delaune, Pascal Lafourcade, Denis Lugiez, Ralf Treinen - Information and Computation - [bibtex]
  2. PHAVer: Algorithmic Verification of Hybrid Systems past HyTech. Goran Frehse - International Journal on Software Tools for Technology Transfer - [bibtex]
  3. Implementing synchronous models on Loosely Time-Triggered Architectures. Stavros Tripakis, Claudio Pinello, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli, Paul Caspi, Marco Di Natale - IEEE trans. on Computers - [bibtex]
  4. The pitfalls of verifying floating-point computations. David Monniaux - TOPLAS - [bibtex]
  5. Formal Analysis Tools for the Synchronous Aspect Language Larissa. David Stauch - EURASIP Journal on Embedded Systems - [bibtex]
  6. Semantic-preserving multitask implementation of synchronous programs. Paul Caspi, Norman Scaife, Christos Sofronis, Stavros Tripakis - ACM Trans. Embedded Computing Systems - [bibtex]
  7. OMEGA -- Correct development of Real Time Embedded Systems. Susanne Graf - SoSyM, int. Journal on Software & Systems Modelling - [bibtex]
  8. Timing analysis and validation with UML: the case of the embedded MARS bus manager. Iulian Ober, Susanne Graf, Yuri Yushtein, Ileana Ober - Innovations in Systems and Software Engineering - [bibtex]
  9. Symbolic quality control for multimedia applications. Jacques Combaz, Jean-Claude Fernandez, Joseph Sifakis, Loïc Strus - Real-Time Systems - [bibtex]
  10. The Algebra of Connectors - Structuring Interaction in BIP. Simon Bliudze, Joseph Sifakis - IEEE Trans. Computers - [bibtex]
  11. Lutin: a language for specifying and executing reactive scenarios. Pascal Raymond, Yvan Roux, Erwan Jahier - EURASIP Journal on Embedded Systems - [bibtex]

Book Chapters

  1. Synchronous Program Verification with Lustre/Lesar. Pascal Raymond - Modeling and Verification of Real-Time Systems - [bibtex]
  2. Modeling and Verification of Real Time Systems Using the IF Toolbox. Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober - Real Time Systems 1: Modeling and verification techniques - [bibtex]

Conference Articles

  1. A Verifiable Conformance Relationship between Smart Card Applets and B Models. Frédéric Dadeau, Julien Lamboley, Thierry Moutet, Marie-Laure Potet - ABZ'2008, International Conference on ASM, B and Z - [bibtex]
  2. Compositional Verification for Component-Based Systems and Application. Saddek Bensalem, Marius Bozga, Thanh-Hung Nguyen, Joseph Sifakis - ATVA '08: Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis - [bibtex]
  3. Time-robust discrete control over networked Loosely Time-Triggered Architectures. Paul Caspi, Albert Benveniste - IEEE Decision and Control Conference, Cancun, December - [bibtex]
  4. Automated Proofs for Asymmetric Encryption. Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech - Proceedings of the LICS-Affiliated Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis - [bibtex]
  5. A Stochastic Approach for Fine Grain QoS Control. Jacques Combaz, Loïc Strus - Proceedings of the 6th IEEE/ACM/IFIP Workshop on Embedded Systems for Real-Time Multimedia (ESTIMedia 2008) Atlanta, Georgia, USA - [bibtex]
  6. Using Neural Networks for Quality Management. Mohamad Jaber, Jacques Combaz, Loïc Strus, Jean-Claude Fernandez - Proceedings of 13th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2008), Hamburg, Germany - [bibtex]
  7. A New Elimination Rule for the Calculus of Inductive Constructions. Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini - TYPES - [bibtex]
  8. A Model Transformation Tool for Performance Simulation of Complex UML Models. Olivier Constant, Wei Monin, Susanne Graf - ICSE 2008, tool track - [bibtex]
  9. Sensitive State Space Exploration. Thao Dang, Alexandre Donzé, Oded Maler, Noa Shalev - IEEE Conference on Decision and Control (CDC) - [bibtex]
  10. Outils pour l'analyse des modèles hybrides. Thao Dang, Goran Frehse, Antoine Girard, Colas Le Guernic - Approches formelles des systèmes embarqué communicants - [bibtex]
  11. Using Disparity to Enhance Test Generation for Hybrid Systems. Thao Dang, Tarik Nahhal - TestCom/FATES 2008 - [bibtex]
  12. Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Delta-Sigma Modulator. Edmund M. Clarke, Alexandre Donzé, Axel Legay - Haifa Verification Conference - [bibtex]
  13. A fully-non-transparent approach to the code location problem. Hugo Venturini, Frédéric Riss, Jean-Claude Fernandez, Miguel Santana - Proceedings of the 11th International Workshop on Software and Compilers for Embedded Systems, Munich, Germany, March 13-14 (SCOPES), 2008 - [bibtex]
  14. With Finite Memory Consensus Is Easier Than Reliable Broadcast. Carole Delporte-Gallet, Stéphane Devismes, Hugues Fauconnier, Franck Petit, Sam Toueg - OPODIS'09, 12th International Conference On Principles of DIstributed Systems - [bibtex]
  15. On Scheduling Policies for Streams of Structured Jobs. Aldric Degorre, Oded Maler - FORMATS - [bibtex]
  16. j-POST: a Java Toolchain for Property-Oriented Software Testing. Ylies Falcone, Laurent Mounier, Jean-Claude Fernandez, Jean-Luc Richier - Model-Based Testing (MBT) - [bibtex]
  17. Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier - International Conference of Information System Security - [bibtex]
  18. A Counterexample-Guided Approach to Parameter Synthesis for Linear Hybrid Automata. Goran Frehse, Sumit Kumar Jha, Bruce H. Krogh - HSCC - [bibtex]
  19. Zonotope/Hyperplane Intersection for Hybrid Systems Reachability Analysis. Antoine Girard, Colas Le Guernic - HSCC - [bibtex]
  20. Efficient Reachability Analysis for Linear Systems Using Support Functions. Antoine Girard, Colas Le Guernic - IFAC World Congress - [bibtex]
  21. On the timed automata-based verification of Ravenscar systems. Ileana Ober, Nicolas Halbwachs - 13th International Conference on Reliable Software Technologies - Ada-Europe 2008 - [bibtex]
  22. Control software model checking using bisimulation functions for nonlinear systems. James Patrick Kapinski, Flavio Lerda, Alexandre Donzé, Bruce H. Krogh, Hitashyam Maka, Silke Wagner - Proceedings of the 47th IEEE Conference on Decision and Control (CDC'08) - [bibtex]
  23. Relation between intruder deduction problem and unification. Pascal Lafourcade - Proceedings of the LICS-Affiliated 3rd International Workshop on Security and Rewriting Techniques (SecReT'08) - [bibtex]
  24. Approximating Continuous Systems by Timed Automata. Oded Maler, Grégory Batt - FMSB - [bibtex]
  25. Translating AADL into BIP - Application to the Verification of Real-time Systems. Mohamed Yassin Chkouri, Marius Bozga, Joseph Sifakis - Workshops and Symposia at MODELS 2008 - [bibtex]
  26. Combination of Abstractions in the ASTRÉE Static Analyzer. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival - Advances in Computer Science --- ASIAN 2006. Secure Software and Related Issues - [bibtex]
  27. Discovering Properties about Arrays in Simple Programs. Nicolas Halbwachs, Mathias Péron - ACM Conference on Programming Language Design and Implementation, PLDI 2008 - [bibtex]
  28. A Method for the Efficient Development of Timed and Untimed Transaction-Level Models of Systems-on-Chip. Jérôme Cornet, Florence Maraninchi, Laurent Maillet-Contoz - Design Automation and Test in Europe (DATE) - [bibtex]
  29. Contract-Based Verification of Hierarchical Systems of Components. Sophie Quinton, Susanne Graf - 6th IEEE Int. Conferences on Software Engineering and Formal Methods, SEFM08, Cape Town, South Africa, 10-14 November 2008 - [bibtex]
  30. A Framework for Contract-Based Reasoning: Motivation and Application. Sophie Quinton, Susanne Graf - Second Workshop on Formal Languages and Analysis of Contract-Oriented Software, FLACOS, Malta, november 2008 - [bibtex]
  31. A B Formal Framework for Security Developments in the Domain of Smart Card Applications. Frédéric Dadeau, Marie-Laure Potet, Régis Tissot - SEC'2008, 23rd int. Information Security Conference - [bibtex]
  32. A Policy Iteration Technique for Time Elapse over Template Polyhedra. Sriram Sankaranarayanan, Thao Dang, Franjo Ivancic - Hybrid Systems: Computation and Control HSCC'08 - [bibtex]
  33. Symbolic Model Checking of Hybrid Systems Using Template Polyhedra. Sriram Sankaranarayanan, Thao Dang, Franjo Ivancic - TACAS'08 - [bibtex]
  34. SystemC/TLM Semantics for Heterogeneous System-on-Chip Validation. Florence Maraninchi, Matthieu Moy, Jérôme Cornet, Laurent Maillet-Contoz, Claude Helmstetter, Claus Traulsen - 2008 Joint IEEE-NEWCAS and TAISA Conference - [bibtex]
  35. Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. Oded Maler, Dejan Nickovic, Amir Pnueli - Pillars of Computer Science - PDF - [bibtex]
  36. Incremental Component-Based Construction and Verification of a Robotic System. Ananda Basu, Matthieu Gallien, Charles Lesire, Thanh-Hung Nguyen, Saddek Bensalem, Felix Ingrand, Joseph Sifakis - ECAI 2008 - 18th European Conference on Artificial Intelligence, Patras, Greece, July 21-25, 2008, Proceedings - [bibtex]
  37. Compositional Verification for Component-Based Systems and Application. Saddek Bensalem, Marius Bozga, Joseph Sifakis, Thanh-Hung Nguyen - Automated Technology for Verification and Analysis, 6th International Symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008. Proceedings - [bibtex]
  38. A Notion of Glue Expressiveness for Component-Based Systems. Simon Bliudze, Joseph Sifakis - CONCUR 2008 - Concurrency Theory, 19th International Conference, CONCUR 2008, Toronto, Canada, August 19-22, 2008. Proceedings - [bibtex]
  39. Distributed Semantics and Implementation for Systems with Interaction and Priority. Ananda Basu, Philippe Bidinger, Marius Bozga, Joseph Sifakis - Formal Techniques for Networked and Distributed Systems - FORTE 2008, 28th IFIP WG 6.1 International Conference, Tokyo, Japan, June 10-13, 2008, Proceedings - [bibtex]
  40. Translating AADL into BIP - Application to the Verification of Real-Time Systems. Mohamed Yassin Chkouri, Anne Robert, Marius Bozga, Joseph Sifakis - Models in Software Engineering, Workshops and Symposia at MODELS 2008, Toulouse, France, September 28 - October 3, 2008. Reports and Revised Selected Papers - [bibtex]
  41. Specification and Verification of Conurrent Systems in Cesar. Jean-Pierre Queille, Joseph Sifakis - 25 Years of Model Checking - History, Achievements, Perspectives - [bibtex]
  42. A Quantifier Elimination Algorithm for Linear Real Arithmetic. David Monniaux - LPAR (Logic for Programming Artificial Intelligence and Reasoning) - PDF - [bibtex]
  43. Quantitative Separation Logic and Programs with Lists. Marius Bozga, Radu Iosif, Swann Perarnau - Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings - [bibtex]
  44. What Else Is Decidable about Integer Arrays? Peter Habermehl, Radu Iosif, Tomás Vojnar - Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008 - [bibtex]
  45. Towards automated proofs for asymmetric encryption schemes in the random oracle model. Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech - Proceedings of the 2008 ACM Conference on Computer and Communications Security, CCS 2008, Alexandria, Virginia, USA, October 27-31, 2008 - [bibtex]
  46. A Logic of Singly Indexed Arrays. Peter Habermehl, Radu Iosif, Tomás Vojnar - Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings - [bibtex]

PhD Thesis and HDR

  1. Component-based modeling of heterogeneous real time systems in BIP. Ananda Basu - [bibtex]
  2. Separation of Functional and Non-Functional Aspects in Transactional Level Models of Systems-on-Chip. Jérôme Cornet - [bibtex]
  3. Models and Methods for the Construction and Verification of Complex Reactive Systems. Susanne Graf - Habilitation à diriger des recherches - [bibtex]
  4. Checking Timed and Hybrid Properties: Theory and Applications. Dejan Nickovic - [bibtex]
  5. Synthèse de gestionnaires mémoire pour applications Java temps-réel embarquées. Guillaume Salagnac - [bibtex]
  6. Modélisations et analyses de réseaux de capteurs. Ludovic Samper - [bibtex]
  7. Contrôle de qualité de service optimal d'application multimédia. Loïc Strus - [bibtex]
  8. Le débogage de code optimisé dans le contexte des systèmes embarqués. Hugo Venturini - [bibtex]

2007

Journal Articles

  1. Hybridization methods for the analysis of nonlinear systems. Eugène Asarin, Thao Dang, Antoine Girard - Acta Inf. - [bibtex]
  2. Software and architecture modelling with Omega-UML and validation with IF. Susanne Graf, Iulian Ober - Génie Logiciel - [bibtex]
  3. Intruder Deduction for the Equational Theory of Abelian Groups with Distributive Encryption. Pascal Lafourcade, Denis Lugiez, Ralf Treinen - Information and Computation - [bibtex]
  4. On optimal and reasonable control in the presence of adversaries. Oded Maler - Annual Reviews in Control - [bibtex]
  5. Time in Abstract State Machines. Susanne Graf, Andreas Prinz - Fundamentae Informaticae, Special issue on ASM 2005 - [bibtex]
  6. The Discipline of Embedded Systems Design. Thomas A. Henzinger, Joseph Sifakis - IEEE Computer - [bibtex]

Book Chapters

  1. Generating Random Values Using Binary Decision Diagrams and Convex Polyhedra. Erwan Jahier, Pascal Raymond - Trends in Constraint Programming - [bibtex]
  2. Synchronous languages. Paul Caspi, Pascal Raymond, Stavros Tripakis - Handbook of Real-Time And Embedded Systems - [bibtex]
  3. Lucid synchrone: un langage pour la programmation des systèmes réactifs. Paul Caspi, Grégoire Hamon, Marc Pouzet - Systèmes temps réel - [bibtex]
  4. Synchronous Programming. Paul Caspi, Pascal Raymond, Stavros Tripakis - Handbook of Real-Time amd Embedded Systems - [bibtex]

Conference Articles

  1. 42: Programmable Models of Computation for a Component-Based Approach to Heterogeneous Embedded Systems. Florence Maraninchi, Tayeb Bouhadiba - Sixth ACM International Conference on Generative Programming and Component Engineering (GPCE'07) - [bibtex]
  2. On timed components and their abstraction. Ramzi Ben Salah, Marius Bozga, Oded Maler - SAVCBS '07: Proceedings of the 2007 conference on Specification and verification of component-based systems - [bibtex]
  3. Sensor Minimization Problems with Static or Dynamic Observers for Fault Diagnosis. Franck Cassez, Stavros Tripakis, Karine Altisen - ACSD '07: Proceedings of the Seventh International Conference on Application of Concurrency to System Design - [bibtex]
  4. Using BIP for Modeling and Verification of Networked Systems - A Case Study on TinyOS-based Networks. Ananda Basu, Laurent Mounier, Marc Poulhiès, Jacques Pulou, Joseph Sifakis - IEEE NCA'07 - [bibtex]
  5. A generalization of DDH with applications to protocol analysis and computational soundness. Emmanuel Bresson, Yassine Lakhnech, Laurent Mazaré, Bogdan Warinschi - Advances in Cryptology - CRYPTO 2007. 27th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 19-23, 2007. Proceedings - [bibtex]
  6. Non-transparent debugging for software-pipelined loops. Hugo Venturini, Frédéric Riss, Jean-Claude Fernandez, Miguel Santana - Proceedings of the 2007 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES 2007 (CASES), Salzburg, Austria, September 30 - October 3, 2007 - [bibtex]
  7. On Synthesizing Controllers from Bounded-Response Properties. Oded Maler, Dejan Nickovic, Amir Pnueli - CAV - [bibtex]
  8. Test Coverage for Continuous and Hybrid Systems. Tarik Nahhal, Thao Dang - CAV - [bibtex]
  9. On Timed Models of Gene Networks. Grégory Batt, Ramzi Ben Salah, Oded Maler - FORMATS - [bibtex]
  10. AMT: A Property-Based Monitoring Tool for Analog Systems. Dejan Nickovic, Oded Maler - FORMATS - [bibtex]
  11. Computationally Sound Typing for Non-interference: The Case of Deterministic Encryption. Judicaël Courant, Cristian Ene, Yassine Lakhnech - FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, 27th International Conference, New Delhi, India, December 12-14, 2007, Proceedings - [bibtex]
  12. Reachability Analysis of a Switched Buffer Network. Goran Frehse, Oded Maler - HSCC - [bibtex]
  13. Guided Randomized Simulation. Tarik Nahhal, Thao Dang - HSCC - [bibtex]
  14. Systematic Simulation Using Sensitivity Analysis. Alexandre Donzé, Oded Maler - HSCC - [bibtex]
  15. Loosely Time-Triggered Architectures based on Communication by Sampling. Albert Benveniste, Paul Caspi, Marco Di Natale, Claudio Pinello, Alberto L. Sangiovanni-Vincentelli, Stavros Tripakis - 7th Intl. Conf. on Embedded Software (EMSOFT'06) - [bibtex]
  16. A Compositional Testing Framework Driven by Partial Specifications. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier, Jean-Luc Richier - TESTCOM/FATES - [bibtex]
  17. Contracts for BIP: hierarchical interaction models for compositional verification. Susanne Graf, Sophie Quinton - FORTE 2007, Talinn - [bibtex]
  18. Larissa, un langage d'aspects pour le développement des systèmes réactifs sûrs. David Stauch, Karine Altisen, Florence Maraninchi - 3èmes Journées Francophones sur le Développement de Logiciels par Aspects - [bibtex]
  19. Test Generation from Security Policies Specified in Or-BAC. Keqin Li, Laurent Mounier, Roland Groz - IEEE COMPSAC'07 - [bibtex]
  20. Game-based Criterion Partition Applied to Computational Soundness of Adaptive Security. Marion Daubignard, Romain Janvier, Yassine Lakhnech, Laurent Mazaré - International Workshop on Formal Aspects in Security and Trust (FAST'06), Revised Selected Papers, Hamilton, Canada, August 2006 - [bibtex]
  21. Verification of Device Drivers and Intelligent Controllers: a Case Study. David Monniaux - EMSOFT - [bibtex]
  22. Worst-case lifetime computation of a Wireless Sensor Network by model-checking. Laurent Mounier, Ludovic Samper, Wassim Znaidi - Fourth ACM Workshop on Performance Evaluation of Wireless Ad Hoc, Sensor, and Ubiquitous Networks (PE-WASUN) - [bibtex]
  23. An abstract domain extending Difference-Bound Matrices with disequality constraints. Mathias Péron, Nicolas Halbwachs - 8th International Conference on Verification, Model-checking, and Abstract Intepretation, VMCAI'07 - [bibtex]
  24. The ARESA Project: Facilitating Research, Development and Commercialization of WSNs. Mischa Dohler, Dominique Barthel, Florence Maraninchi, Laurent Mounier, Stéphane Aubert, Christophe Dugas, Aurélien Buhrig, Franck Paugnat, Marc Renaudin, Andrzej Duda, Martin Heusse, Fabrice Valois - IEEE SECON'07 (Fourth Annual IEEE Communications Society Conference on Sensor, Mesh and Ad Hoc Communications and Networks) - [bibtex]
  25. Specifying and executing reactive scenarios with Lutin. Pascal Raymond, Yvan Roux, Erwan Jahier - SLA++P'07, ETAPS'07 Satellite Workshop on Model-driven High-level Programming of Embedded Systems - [bibtex]
  26. Lustre as a System Modeling Language: Lussensor, a Case-Study with Sensor Networks. Florence Maraninchi, Ludovic Samper, Kevin Baradon, Antoine Vasseur - SLA++P'07, ETAPS'07 Satellite Workshop on Model-driven High-level Programming of Embedded Systems - [bibtex]
  27. Semi-Automatic Region-Based Memory Management for Real-Time Java Embedded Systems. Guillaume Salagnac, Christophe Rippert, Sergio Yovine - Proceedings of the 13th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications - [bibtex]
  28. A SystemC/TLM semantics in Promela and its possible applications. Claus Traulsen, Jérôme Cornet, Matthieu Moy, Florence Maraninchi - 14th Workshop on Model Checking Software SPIN - [bibtex]
  29. Synthesis Of Optimal-Cost Dynamic Observers for Fault Diagnosis of Discrete-Event Systems. Franck Cassez, Stavros Tripakis, Karine Altisen - TASE '07: Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering - [bibtex]
  30. Virtual execution of AADL models via a translation into synchronous programs. Erwan Jahier, Nicolas Halbwachs, Pascal Raymond, Xavier Nicollin, David Lesens - Proceedings of the 7th ACM & IEEE International conference on Embedded software, EMSOFT 2007, September 30 - October 3, 2007, Salzburg, Austria - [bibtex]
  31. Interpreting invariant composition in the B method using the Spec\# ownership relation: a way to explain and relax B restrictions. Sylvain Boulmé, Marie-Laure Potet - B 2007 - [bibtex]
  32. An Approach to Modeling and Verification of Component Based Systems. Gregor Göessler, Susanne Graf, Mila Majster-Cederbaum, Moritz Martens, Joseph Sifakis - Current Trends in Theory and Practice of Computer Science, SOFSEM'07 - [bibtex]
  33. Intuitionistic Refinement Calculus.. Sylvain Boulmé - Typed Lambda Calculi and Applications - PDF - [bibtex]
  34. Using Speed Diagrams for Symbolic Quality Management. Jacques Combaz, Jean-Claude Fernandez, Joseph Sifakis, Loïc Strus - 21th International Parallel and Distributed Processing Symposium (IPDPS 2007), Proceedings, 26-30 March 2007, Long Beach, California, USA - [bibtex]
  35. The algebra of connectors: structuring interaction in BIP. Simon Bliudze, Joseph Sifakis - Proceedings of the 7th ACM & IEEE International conference on Embedded software, EMSOFT 2007, September 30 - October 3, 2007, Salzburg, Austria - [bibtex]
  36. Causal Semantics for the Algebra of Connectors. Simon Bliudze, Joseph Sifakis - Formal Methods for Components and Objects, 6th International Symposium, FMCO 2007, Amsterdam, The Netherlands, October 24-26, 2007, Revised Lectures - [bibtex]
  37. Using BIP for Modeling and Verification of Networked Systems -- A Case Study on TinyOS-based Networks. Ananda Basu, Laurent Mounier, Marc Poulhiès, Jacques Pulou, Joseph Sifakis - Sixth IEEE International Symposium on Network Computing and Applications (NCA 2007), 12 - 14 July 2007, Cambridge, MA, USA - [bibtex]
  38. Proving Termination of Tree Manipulating Programs. Peter Habermehl, Radu Iosif, Adam Rogalewicz, Tomás Vojnar - Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings - [bibtex]
  39. On Flat Programs with Lists. Marius Bozga, Radu Iosif - Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings - [bibtex]

Master Thesis

  1. Accélération des simulations de systèmes sur puce au niveau transactionnel. Yussef Bouzouzou - Diplôme de Recherche Technologique - PDF - [bibtex]

PhD Thesis and HDR

  1. Trajectoires pour la Vérification et la Commande de Systèmes Continus et Hybrides. Alexandre Donzé - [bibtex]
  2. Acceleration abstraite pour l'amelioration de la precision en analyse des relations lineaires. Laure Gonnord - [bibtex]
  3. Model Based Testing for Real-Time Systems. Moez Krichen - [bibtex]
  4. Model-Based Testing of Hybrid Systems. Tarik Nahhal - [bibtex]
  5. Validation de modèles de systèmes sur puce en présence d'ordonnancements indéterministes et de temps imprécis. Claude Helmstetter - [bibtex]
  6. On Timing Analysis of Large Systems. Ramzi Ben Salah - [bibtex]
  7. Larissa, an Aspect-Oriented Language for Reactive Systems. David Stauch - [bibtex]

2006

Journal Articles

  1. Counter-example Guided Predicate Abstraction of Hybrid Systems. Rajeev Alur, Thao Dang, Franjo Ivancic - Theoretical Computer Science (TCS) - [bibtex]
  2. Reachability Analysis of Hybrid Systems via Predicate Abstraction. Rajeev Alur, Thao Dang, Franjo Ivancic - ACM transactions on embedded computing systems (TECS) - [bibtex]
  3. Aspect-Oriented Programming for Reactive Systems: a Proposal in the Synchronous Framework. Karine Altisen, Florence Maraninchi, David Stauch - Science of Computer Programming - [bibtex]
  4. Pattern-based abstraction for verifying secrecy in protocols. Liana Bozga, Yassine Lakhnech, Michaël Périn - International Journal on Software Tools for Technology Transfer (STTT) - [bibtex]
  5. Scheduling with timed automata. Yasmina Abdeddaïm, Eugène Asarin, Oded Maler - Theor. Comput. Sci. - [bibtex]
  6. LusSy: an open Tool for the Analysis of Systems-on-a-Chip at the Transaction Level. Matthieu Moy, Florence Maraninchi, Laurent Maillet-Contoz - Design Automation for Embedded Systems - [bibtex]
  7. Some ways to reduce the space dimension in polyhedra computations. Nicolas Halbwachs, David Merchat, Laure Gonnord - Formal Methods in System Design - [bibtex]
  8. Tester la conformité d'un réseau à une politique de sécurité. Vianney Darmaillacq, Jean-Claude Fernandez, Roland Groz, Laurent Mounier, Jean-Luc Richier - Revue de l'electricité et de l'Electronique (REE) - [bibtex]
  9. Case Studies with Lurette V2. Erwan Jahier, Pascal Raymond, Philippe Baufreton - Software Tools for Technology Transfer - [bibtex]
  10. Automatic rate desynchronization of embedded reactive programs. Alain Girault, Xavier Nicollin, Marc Pouzet - ACM TECS - PDF - [bibtex]
  11. A real-time profile for UML. Susanne Graf, Ileana Ober, Iulian Ober - STTT, Software Tools for Technology Transfer - [bibtex]
  12. Validating Timed UML models by simulation and verification. Susanne Graf, Ileana Ober, Iulian Ober - STTT, Software Tools for Technology Transfer - [bibtex]
  13. Specification and Validation of Models of Real Time and Embedded Systems in UML. Susanne Graf, Ileana Ober, Oystein Haugen, Bran Selic - STTT, Software Tools for Technology Transfer, a special issue on the SVERTS 2003 workshop - [bibtex]

Book Chapters

  1. La boîte à outils IF pour la modélisation et la vérification de systèmes temps réel. Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober - Systèmes temps réel : techniques de description et de vérification - [bibtex]
  2. Vérification de programmes synchrones avec Lustre/Lesar. Pascal Raymond - Systèmes temps réel 1 -- techniques de description et de vérification - [bibtex]

Conference Articles

  1. Monitoring and Fault Diagnosis with Digital Clocks. Karine Altisen, Franck Cassez, Stavros Tripakis - Application of Concurrency to System Design (ACSD'06) - [bibtex]
  2. Qualification d'architectures fontionnelles. Marius Bozga, Pierre Combes, Susanne Graf, Wei Monin, Nicolas Moteau - Notere'06 - [bibtex]
  3. Recent Progress in Continuous and Hybrid Reachability Analysis. Eugène Asarin, Thao Dang, Goran Frehse, Antoine Girard, Colas Le Guernic, Oded Maler - CACSD 2006 - [bibtex]
  4. Approximate Reachability Computation for Polynomial Systems. Thao Dang - HSCC 2006 - [bibtex]
  5. Scheduling for multi-threaded real-time programs via path planning. Thao Dang, Philippe Gerner - Proceedings of the 6th ACM & IEEE International conference on Embedded software, EMSOFT 2006 - [bibtex]
  6. Simulation of Hybrid Systems For Circuit Validation. Thao Dang, Tarik Nahhal - FDL 2006 - [bibtex]
  7. Test Generation for Network Security Rules. Vianney Darmaillacq, Jean-Claude Fernandez, Roland Groz, Laurent Mounier, Jean-Luc Richier - TestCom'06 - [bibtex]
  8. On Interleaving in Timed Automata. Ramzi Ben Salah, Marius Bozga, Oded Maler - CONCUR 2006 - [bibtex]
  9. On Timed Simulation Relations for Hybrid Systems and Compositionality. Goran Frehse - FORMATS 2006 - [bibtex]
  10. From MITL to Timed Automata. Oded Maler, Dejan Nickovic, Amir Pnueli - FORMATS 2006 - [bibtex]
  11. Efficient Computation of Reachable Sets of Linear Time-Invariant Systems with Inputs. Antoine Girard, Colas Le Guernic, Oded Maler - HSCC 2006 - [bibtex]
  12. Fast and Flexible Difference Constraint Propagation for DPLL(T). Scott Cotton, Oded Maler - SAT 2006 - [bibtex]
  13. A Memory-Optimal Buffering Protocol for Preservation of Synchronous Semantics under Preemptive Scheduling. Christos Sofronis, Stavros Tripakis, Paul Caspi - 6th Intl. Conf. on Embedded Software (EMSOFT'06) - [bibtex]
  14. Communication by Sampling in Time-Sensitive Distributed Systems. Albert Benveniste, Benoît Caillaud, Lucas Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli, Stavros Tripakis - 6th Intl. Conf. on Embedded Software (EMSOFT'06) - [bibtex]
  15. A Test Calculus Framework Applied to Network Security Policies. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier, Jean-Luc Richier - FATES/RV'06 - [bibtex]
  16. Interference of Larissa Aspects. David Stauch, Karine Altisen, Florence Maraninchi - FOAL : Foundations of Aspect-Oriented Languages workshop (an AOSD'06 satellite event) - [bibtex]
  17. MARTES - Modelling and Analysis of Real Time and Embedded Systems Using UML. Susanne Graf, Sébastien Gérard, Oystein Haugen, Iulian Ober, Bran Selic - MoDELS 2006 International Workshops, Doctoral Symposium, Educators Symposium; Genoa, October 2006, Revised Selected Papers - [bibtex]
  18. Combining widening and acceleration in linear relation analysis. Laure Gonnord, Nicolas Halbwachs - 13th International Static Analysis Symposium, SAS'06 - [bibtex]
  19. Simulation and verification of asynchronous systems by means of a synchronous model. Nicolas Halbwachs, Louis Mandel - Sixth International Conference on Application of Concurrency to System Design, ACSD 2006 - [bibtex]
  20. Test Coverage for Loose Timing Annotations. Claude Helmstetter, Florence Maraninchi, Laurent Maillet-Contoz - 11th International Workshop on Formal Methods for Industrial Critical Systems - [bibtex]
  21. Approximation, Sampling and Voting in Hybrid Computing Systems. Chiheb Kossentini, Paul Caspi - Hybrid Systems Computation and Control, HSCC06 - [bibtex]
  22. GLONEMO: Global and Accurate Formal Models for the Analysis of Ad-Hoc Sensor Networks. Ludovic Samper, Florence Maraninchi, Laurent Mounier, Louis Mandel - InterSense: First International Conference on Integrated Internet Ad hoc and Sensor Networks - [bibtex]
  23. Certification of Cryptographic Protocols by Abstract Model-Checking and Proof Concretization. Romain Janvier, Yassine Lakhnech, Michaël Périn - Workshop on Innovative Techniques for the Certification of Embedded Systems On the Importance of Modeling the Environment when Analyzing Sensor Networks. Ludovic Samper, Florence Maraninchi, Laurent Mounier, Erwan Jahier, Pascal Raymond - 3rd International Workshop on Wireless Ad-hoc and Sensor Networks (IWWAN'06) - [bibtex]
  24. Computational soundness of symbolic analysis for protocols using hash functions. Romain Janvier, Yassine Lakhnech, Laurent Mazaré - Workshop on Information and Computer Security (ICS'06) - [bibtex]
  25. Describing and executing random reactive systems. Pascal Raymond, Erwan Jahier, Yvan Roux - SEFM 2006, 4th IEEE International Conference on Software Engineering and Formal Methods - [bibtex]
  26. A case study in UML model-based validation: The Ariane-5 launcher. Iulian Ober, Susanne Graf, David Lesens - Formal Methods for Open Object-Based Distributed Systems, 8th IFIP WG 6.1 International Conference, FMOODS 2006 - [bibtex]
  27. Confirmation of Deadlock Potentials Detected by Runtime Analysis. Saddek Bensalem, Jean-Claude Fernandez, Klaus Havelund, Laurent Mounier - Parallel and Distributed Systems: Testing and Debugging 2006 (PADTAD'06) - [bibtex]
  28. Larissa: Modular Design of Man-Machine Interfaces with Aspects. Karine Altisen, Florence Maraninchi, David Stauch - Fifth International Symposium on Software Composition (an ETAPS satellite event) - [bibtex]
  29. Efficient Region-Based Memory Management for Resource-limited Real-Time Embedded Systems. Guillaume Salagnac, Chaker Nakhli, Christophe Rippert, Sergio Yovine - In proceedings of the workshop on Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems - [bibtex]
  30. Automatic Generation of Schedulings for Improving the Test Coverage of Systems-on-a-Chip. Claude Helmstetter, Florence Maraninchi, Laurent Maillet-Contoz, Matthieu Moy - Formal Methods in Computer Aided Design (FMCAD) - [bibtex]
  31. Ensuring Properties of Interaction Systems by Construction. Gregor Göessler, Susanne Graf, Mila Majster-Cederbaum, Moritz Martens, Joseph Sifakis - Program Analysis and Compilation, Theory and Practice - [bibtex]
  32. Using an UML profile for timing analysis with the IF validation tool-set. Iulian Ober, Susanne Graf, Yuri Yushtein - Proceedings of Model-Based Development of Embedded Systems, MBEES, Dagstuhl, Germany - [bibtex]
  33. Randomized simulation of hybrid systems for circuit validation. Thao Dang, Tarik Nahhal - Proceedings of FDL06 - Forum on specification and Design Languages - [bibtex]
  34. The Embedded Systems Design Challenge. Thomas A. Henzinger, Joseph Sifakis - FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings - [bibtex]
  35. WPDRTS keynote: component-based construction of embedded systems. Joseph Sifakis - 20th International Parallel and Distributed Processing Symposium (IPDPS 2006), Proceedings, 25-29 April 2006, Rhodes Island, Greece - [bibtex]
  36. Modeling Heterogeneous Real-time Components in BIP. Ananda Basu, Marius Bozga, Joseph Sifakis - Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006), 11-15 September 2006, Pune, India - [bibtex]
  37. A Methodology and Supporting Tools for the Development of Component-Based Embedded Systems. Marc Poulhiès, Jacques Pulou, Christophe Rippert, Joseph Sifakis - Composition of Embedded Systems. Scientific and Industrial Issues, 13th Monterey Workshop 2006, Paris, France, October 16-18, 2006, Revised Selected Papers - [bibtex]
  38. Programs with Lists Are Counter Automata. Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar - Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings - [bibtex]
  39. Flat Parametric Counter Automata. Marius Bozga, Radu Iosif, Yassine Lakhnech - Automata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Venice, Italy, July 10-14, 2006, Proceedings, Part II - [bibtex]
  40. Generating Random Values Using Binary Decision Diagrams and Convex Polyhedra. Erwan Jahier, Pascal Raymond - Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA'06) - [bibtex]
  41. Game-Based Criterion Partition Applied to Computational Soundness of Adaptive Security. Marion Daubignard, Romain Janvier, Yassine Lakhnech, Laurent Mazaré - Formal Aspects in Security and Trust, Fourth International Workshop, FAST 2006, Hamilton, Ontario, Canada, August 26-27, 2006, Revised Selected Papers - [bibtex]
  42. Time Domain Verification of Oscillator Circuit Properties. Goran Frehse, Bruce H. Krogh, Rob A. Rutenbar, Oded Maler - Proc. Workshop on Formal Verification of Analog Circuits - [bibtex]
  43. Automata-Based Verification of Programs with Tree Updates. Peter Habermehl, Radu Iosif, Tomás Vojnar - Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 20 - [bibtex]

PhD Thesis and HDR

  1. A Scalable Framework for Modelling and Performance Analysis of Multiprocessor Embedded Systems. Ismail Assayad - [bibtex]
  2. Conception de Systèmes Adaptatifs Surs et Optimaux. Jacques Combaz - [bibtex]
  3. Liens entre modèles symboliques et computationnels pour les protocoles cryptographiques utilisant des hachages. Romain Janvier - [bibtex]
  4. Conditional Scheduling Strategies using Timed Automata. Abdelkarim Kerbaa - [bibtex]
  5. Computational Soundness of Symbolic Models for Cryptographic Protocols. Laurent Mazaré - [bibtex]
  6. Embedded Code Generation from High-level Heterogeneous Components. Christos Sofronis - [bibtex]

2005

Journal Articles

  1. A symbolic decision procedure for cryptographic protocols with time stamps. Liana Bozga, Cristian Ene, Yassine Lakhnech - J. Log. Algebr. Program. - [bibtex]
  2. Un profile UML et un outil pour la modélisation et la validation de systèmes temps-réel. Iulian Ober, Susanne Graf, Ileana Ober, David Lesens - Numéro spécial du journal Génie Logiciel consacré à la Journée NEPTUNE 05 : Ingénierie des Modèles - vérification de modèles - [bibtex]
  3. Formation en systèmes embarqués à l'INPG. Florence Maraninchi, Marc Renaudin - Revue des ingénieurs INPG - [bibtex]
  4. Translating Discrete-Time Simulink to Lustre. Paul Caspi, Adrian Curic, Aude Maignan, Christos Sofronis, Stavros Tripakis - ACM Trans. Embedded Computing Systems - [bibtex]
  5. Guidelines for a graduate curriculum on embedded software and systems.. Paul Caspi, Alberto L. Sangiovanni-Vincentelli, Luís Almeida, Albert Benveniste, Bruno Bouyssounouse, Giorgio C. Buttazzo, Ivica Crnkovic, Werner Damm, Jakob Engblom, Gerhard Fohler, Marisol García-Valls, Hermann Kopetz, Yassine Lakhnech, Francois Laroussinie, Lucia Lavagno, Giuseppe Lipari, Florence Maraninchi, Philipp Peti, Juan De la Puente, Norman Scaife, Joseph Sifakis, Robert De Simone, Martin Torngren, Paulo Veríssimo, Andrew J. Wellings, Reinhard Wilhelm, Tim Willemse, Wang Yi - ACM Trans. Embedded Comput. Syst. - [bibtex]
  6. Translating Java for Multiple Model Checkers: The Bandera Back-End. Radu Iosif, Matthew B. Dwyer, John Hatcliff - Formal Methods in System Design - [bibtex]
  7. Probabilistic Opacity for a Passive Adversary and its Application to Chaum's Voting Scheme. Yassine Lakhnech, Laurent Mazaré - IACR Cryptology ePrint Archive - [bibtex]

Book Chapters

  1. Roadmap: Component based design and Integration platforms. Bengt Jonsson, Ed Brinksma, Geoff Coulson, Susanne Graf, Ivica Crnkovic, Sébastien Gérard, Holger Hermanns, Jean-Marc Jezequel, Anders Ravn, Philippe Schnoebelen, François Terrier, Angelika Votintseva - Embedded Systems Design: The ARTIST Roadmap for Research and Development - [bibtex]
  2. From Control Loops to Real-Time Programs. Paul Caspi, Oded Maler - Handbook of Networked and Embedded Computing Systems - [bibtex]
  3. Chapter 5.9, Formal Verification. Matthieu Moy - Transaction-Level Modeling with SystemC. TLM Concepts and Applications for Embedded Systems - [bibtex]

Conference Articles

  1. Introduction au contrôle des systèmes temps-réel. Karine Altisen, Patricia Bouyer, Thierry Cachat, Franck Cassez, Guillaume Gardey - Modélisation des Systèmes Réactifs (MSR'05), session invitée de l'ACI CORTOS - [bibtex]
  2. Implémentabilité des automates temporisés. Karine Altisen, Nicolas Markey, Pierre-Alain Reynier, Stavros Tripakis - Modélisation des Systèmes Réactifs (MSR'05), session invitée de l'ACI CORTOS - [bibtex]
  3. Fine grain QoS control for multimedia application software. Jacques Combaz, Jean-Claude Fernandez, Thierry Lepley, Joseph Sifakis - Design, Automation and Test in Europe (DATE 2005), Munich, Germany - [bibtex]
  4. QoS Control for Optimality and Safety. Jacques Combaz, Jean-Claude Fernandez, Thierry Lepley, Joseph Sifakis - Proceedings of the 5th Conference on Embedded Software (EMSOFT 2005), Jersey City, New Jersey, USA - [bibtex]
  5. Eléments de modélisation pour le test de politiques de sécurité. Vianney Darmaillacq, Jean-Claude Fernandez, Roland Groz, Laurent Mounier, Jean-Luc Richier - Colloque sur les RIsques et la Sécurité d'Internet et des Systèmes, CRiSIS - [bibtex]
  6. Real Time Temporal Logic: Past, Present, Future. Oded Maler, Dejan Nickovic, Amir Pnueli - FORMATS 2005 - [bibtex]
  7. On temporal difference algorithms for continuous systems. Alexandre Donzé - ICINCO - [bibtex]
  8. Automatic Verification of Security Properties Based on Abstractions. Liana Bozga, Cristian Ene, Romain Janvier, Yassine Lakhnech, Laurent Mazaré, Michaël Périn - Proceedings of the NATO Advanced Research Workshop Verification of Infinite State Systems with Applications to Security VISS - [bibtex]
  9. Semantic-Preserving and Memory Efficient Implementation of Inter-Task Communication on Static-Priority or EDF Schedulers. Stavros Tripakis, Christos Sofronis, Norman Scaife, Paul Caspi - 5th International Conference on Embedded Software, EMSOFT05 - [bibtex]
  10. A model-based approach for robustness testing. Jean-Claude Fernandez, Laurent Mounier, Cyril Pachon - TestCom 2005 - [bibtex]
  11. Flush: a system development tool based on Scade/Lustre. Jan Mikác, Paul Caspi - Formal methods for industrial critical systems, FMICS05 - [bibtex]
  12. Implementation of Timed Automata: An Issue of Semantics or Modeling? Karine Altisen, Stavros Tripakis - FORMATS - [bibtex]
  13. Timing analysis and validation of the embedded MARS bus manager. Iulian Ober, Susanne Graf, Yuri Yushtein - Intl Workshop on Modeling and Analysis of Real Time Embedded Systems, MARTES 2005, associated with MoDELS 2005 - [bibtex]
  14. Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries. Romain Janvier, Yassine Lakhnech, Laurent Mazaré - The European Symposium on Programming (ESOP'05). Edinburgh (Scotland) - [bibtex]
  15. A synchronous language at work: the story of Lustre. Nicolas Halbwachs - Third ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE'2005 - [bibtex]
  16. Temporal Refinement for Lustre. Jan Mikác, Paul Caspi - Synchronous Languages Applications and Programming, SLAP'05 - [bibtex]
  17. LusSy: A Toolbox for the Analysis of Systems-on-a-Chip at the Transactional Level. Matthieu Moy, Florence Maraninchi, Laurent Maillet-Contoz - International Conference on Application of Concurrency to System Design - [bibtex]
  18. Pinapa: An Extraction Tool for SystemC descriptions of Systems-on-a-Chip. Matthieu Moy, Florence Maraninchi, Laurent Maillet-Contoz - EMSOFT - [bibtex]
  19. MARTES - Specification and Validation of Real-time and Embedded Systems, workshop overview. Susanne Graf, Sébastien Gérard, Oystein Haugen, Iulian Ober, Bran Selic - MoDELS 2005 International Workshops, Doctoral Symposium, Educators Symposium; Montenegro Bay, Jamaica, October 2005, Revised Selected Papers - [bibtex]
  20. COTS component-Based Embedded Systems - A Dream or Reality? Ivica Crnkovic, Jakob Axelsson, Susanne Graf, Magnus Larsson, Rob C. van Ommering, Kurt C. Wallnau - ICCBSS 2005, Bilbao, January 2005 - [bibtex]
  21. Time in Abstract State Machines. Susanne Graf, Andreas Prinz - Proceedings of the 12th International Workshop on Abstract State Machines, ASM 2005, March 8-11, 2005, Paris, France - [bibtex]
  22. On Decidability Within the Arithmetic of Addition and Divisibility. Marius Bozga, Radu Iosif - Foundations of Software Science and Computational Structures, 8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, - [bibtex]

PhD Thesis and HDR

  1. Implementing Lustre Programs on Distributed Platforms with Real-time Constraints. Adrian Curic - [bibtex]
  2. Réduction du nombre de variables en analyse de relations linéaires. David Merchat - [bibtex]
  3. Raffinements et preuves de systèmes Lustre. Jan Mikác - [bibtex]
  4. Exploitation des structures régulières et des spécifications locales pour le développement correct de systèmes réactifs de grande taille. Lionel Morel - [bibtex]
  5. Approche Fondée sur les Modèles pour Java Temps-Réel. Chaker Nakhli - [bibtex]
  6. Une approche basée sur les modèles pour le test de robustesse. Cyril Pachon - [bibtex]
  7. Techniques and Tools for the Verification of Systems-on-a-Chip at the Transaction Level. Matthieu Moy - [bibtex]

2004

Journal Articles

  1. Counter-example generation in symbolic abstract model-checking. Gordon Pace, Nicolas Halbwachs, Pascal Raymond - Software Tools for Technology Transfer - [bibtex]
  2. Symmetry reductions for model checking of concurrent dynamic software. Radu Iosif - STTT - [bibtex]

Conference Articles

  1. Arrays and Contracts for the Specification and Analysis of Regular Systems. Florence Maraninchi, Lionel Morel - Fourth International Conference on Application of Concurrency to System Design - [bibtex]
  2. On the Existence of an Effective and Complete Inference System for Cryptographic Protocols. Liana Bozga, Cristian Ene, Yassine Lakhnech - Foundations of Software Science and Computation Structures, 7th International Conference, FOSSACS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, B - [bibtex]
  3. A symbolic decision procedure for bounded security protocols with time stamps (Extended abstract). Liana Bozga, Cristian Ene, Yassine Lakhnech - CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings - [bibtex]
  4. IF Tutorial. Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober - 9th SPIN'04 Workshop on Model-Checking of Software, Barcelona, Spain - [bibtex]
  5. Monitoring Temporal Properties of Continuous Signals. Oded Maler, Dejan Nickovic - Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques i - [bibtex]
  6. A Symbolic Decision Procedure for Cryptographic Protocols with Time Stamps (Extended Abstract). Liana Bozga, Cristian Ene, Yassine Lakhnech - CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings - [bibtex]
  7. Verification of Analog and Mixed-Signal Circuits Using Hybrid System Techniques. Thao Dang, Alexandre Donzé, Oded Maler - FMCAD - [bibtex]
  8. Logical-Time Contracts for the Development of Reactive Embedded Software. Florence Maraninchi, Lionel Morel - 30th Euromicro Conference, Component-Based Software Engineering Track (ECBSE) - [bibtex]
  9. Integrating model-based design and preemptive scheduling in mixed time- and event-triggered systems. Norman Scaife, Paul Caspi - Euromicro Conference on Real-Time Systems, ECRTS04 - [bibtex]
  10. Heterogeneous Reactive Systems Modeling: capturing causality and the correctness of loosely time-triggered protocols. Albert Benveniste, Benoît Caillaud, Lucas Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli - Emsoft04 - [bibtex]
  11. Exploring Aspects in the Context of Reactive Systems. Karine Altisen, Florence Maraninchi, David Stauch - Workshop on the Foundations of Aspect-Oriented Languages (FOAL), affiliated with AOSD (International Conference on Aspect-Oriented Software Development) - [bibtex]
  12. Mixed delay and threshold voters in critical real-time systems. Chiheb Kossentini, Paul Caspi - Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT04 - [bibtex]
  13. How useful is the UML real-time profile SPT without Semantics? Susanne Graf, Ileana Ober - Int. workshop SIVOES 2004, associated with RTAS 2004, Toronto Canada - [bibtex]
  14. A Framework for Time in FDTs. Susanne Graf, Andreas Prinz - FORTE 2004, participants proceedings - [bibtex]
  15. Case Studies with Lurette V2. Erwan Jahier, Pascal Raymond, Philippe Baufreton - 1st International Symposium on Leveraging Applications of Formal Methods, ISoLA 2004 - [bibtex]
  16. Model Checking of UML Models via a Mapping to Communicating Extended Timed Automata. Iulian Ober, Susanne Graf, Ileana Ober - 11th International SPIN Workshop on Model Checking of Software, 2004 - [bibtex]
  17. From Discrete Duration Calculus to Symbolic Automata. Laure Gonnord, Nicolas Halbwachs, Pascal Raymond - 3rd International Workshop on Synchronous Languages, Applications, and Programs, SLAP'04, see also Electronic Notes in Theoretical Computer Science Volume 153, Issue 4, 27 June 2006, Pages 3-18 - [bibtex]
  18. Defining and translating a ``safe'' subset of Simulink/Stateflow into Lustre. Norman Scaife, Christos Sofronis, Paul Caspi, Stavros Tripakis, Florence Maraninchi - Fourth ACM International Conference on Embedded Software (EMSOFT) - [bibtex]
  19. SVERTS - Specification and Validation of Real-time and Embedded Systems, workshop overview. Susanne Graf, Oystein Haugen, Ileana Ober, Bran Selic - UML Modeling Languages and Applications, UML 2004 Satellite Activities, Lisbon, Portugal, October 11-15, 2004, Revised Selected Papers - [bibtex]
  20. The IF toolset. Marius Bozga, Susanne Graf, Iulian Ober, Ileana Ober, Joseph Sifakis - 4th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Real Time, SFM-04:RT, Bologna, Sept. 2004 - [bibtex]
  21. Correct Development of Embedded Systems. Susanne Graf, Jozef Hooman - European Workshop on Software Architecture: Languages, Styles, Models, Tools, and Applications (EWSA 2004), co-located with ICSE 2004, St Andrews, Scotland - [bibtex]
  22. Abstraction by projection and application to multi-affine systems. Eugène Asarin, Thao Dang - Hybrid Systems: Control and Computation HSCC'04 - [bibtex]
  23. On Logics of Aliasing. Marius Bozga, Radu Iosif, Yassine Lakhnech - Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings - [bibtex]

PhD Thesis and HDR

  1. Automatic verification of cryptographic protocols. Liana Bozga - [bibtex]
  2. Description et simulation de systèmes réactifs non-déterministes. Yvan Roux - [bibtex]
  3. Modélisation et Analyse de Systèmes Temps Réel avec Préemption, Incertitude et Dépendance. Marcelo Zanconi - [bibtex]

2003

Journal Articles

  1. The synchronous languages 12 years later. Albert Benveniste, Paul Caspi, Stefan A. Edwards, Nicolas Halbwachs, Paul Le Guernic, Robert De Simone - Proceedings of the IEEE - [bibtex]
  2. Mode-Automata: a new Domain-Specific Construct for the Development of Safe Critical Systems. Florence Maraninchi, Yann Rémond - Science of Computer Programming - [bibtex]
  3. Tools and Algorithms for the Construction and Analysis of Systems: An STTT special section. Susanne Graf - STTT, Software Tools for Technology Transfer - [bibtex]
  4. Temporal logic properties of Java objects. Radu Iosif, Riccardo Sisto - Journal of Systems and Software - [bibtex]

Conference Articles

  1. Automatic State Reaching for Debugging Reactive Programs. Erwan Jahier, Bertrand Jeannet, Fabien Gaucher, Florence Maraninchi - AADEBUG'2003 -- Fifth International Workshop on Automated Debugging - [bibtex]
  2. Abstract Interpretation for Secrecy using Patterns. Liana Bozga, Yassine Lakhnech, Michaël Périn - TACAS'03 - [bibtex]
  3. HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols. Liana Bozga, Yassine Lakhnech, Michaël Périn - 15th International Conference on Computer Aided Verification (CAV), - [bibtex]
  4. Validation of asynchronous circuit specifications using IF/CADP. Dominique Borrione, Menouer Boubekeur, Laurent Mounier, Marc Renaudin, Antoine Sirianni - IFIP Intl. Conference on VLSI, Darmstadt, Germany - [bibtex]
  5. Modelling CHP descriptions in Labelled Transition Systems for an efficient formal validations of asynchronous circuit specifications. Menouer Boubekeur, Dominique Borrione, Laurent Mounier, Marc Renaudin, Antoine Sirianni - Forum on Specification and Design Language (FDL'03), Frankfurt, Germany - [bibtex]
  6. Translating Discrete-Time Simulink to Lustre. Paul Caspi, Adrian Curic, Aude Maignan, Christos Sofronis, Stavros Tripakis - Embedded Software EMSOFT2003 - [bibtex]
  7. Heterogeneous Reactive Systems Modeling and Correct-by-Construction Deployment. Albert Benveniste, Lucas Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli - 3rd International Wokshop on Embedded Software, EMSOFT03 - [bibtex]
  8. Using Controller Synthesis to Build Property-Enforcing Layers. Karine Altisen, Aurélie Clodic, Florence Maraninchi, Eric Rutten - European Symposium on Programming (ESOP) - [bibtex]
  9. Property Oriented Test Case Generation. Jean-Claude Fernandez, Laurent Mounier, Cyril Pachon - Proceedings of FATES'03 (Satellite workshop of ASE'03), Montreal, Canada - [bibtex]
  10. Causality and Scheduling Constraints in Heterogeneous Reactive Systems Modeling. Albert Benveniste, Benoît Caillaud, Lucas Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli - FMCO 2003 - [bibtex]
  11. Timed annotations in UML. Susanne Graf, Ileana Ober, Iulian Ober - Workshop SVERTS on Specification and Validation of UML models for Real Time and Embedded Systems, a satellite event of UML 2003, San Francisco, October 2003 - [bibtex]
  12. Validating Timed UML models by simulation and verification. Iulian Ober, Susanne Graf, Ileana Ober - Workshop SVERTS on Specification and Validation of UML models for Real Time and Embedded Systems, a satellite event of UML 2003, San Francisco, October 2003 - [bibtex]
  13. Cartesian factoring of polyhedra in linear relation analysis. Nicolas Halbwachs, David Merchat, Catherine Parent-Vigouroux - Static Analysis Symposium, SAS'03 - [bibtex]
  14. From Simulink to SCADE/Lustre to TTA: A Layered Approach for Distributed Embedded Applications. Paul Caspi, Adrian Curic, Aude Maignan, Christos Sofronis, Stavros Tripakis, Peter Niebert - Languages, Compilers and Tools for Embedded Systems, LCTES 2003 - [bibtex]
  15. Finite state machines: composition, verification, minimization: a case study. Paul Amblard, Fabienne Lagnier, Michel Levy - 10th International Conference on Mixed Design (MIXDES03), Lodz, Poland - [bibtex]
  16. Automatique continue, automatique discrète, informatique industrielle : le triangle des Bermudes ? Paul Caspi - Actes du colloque Modélisation des systèmes réactifs, MSR03 - [bibtex]
  17. Abstraction as the Key for Invariant Verification. Saddek Bensalem, Susanne Graf, Yassine Lakhnech - Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday - [bibtex]
  18. A Real-time profile for UML and how to adapt it to SDL. Susanne Graf, Ileana Ober - SDL 2003: System Design, 11th International SDL Forum, Stuttgart, Germany, July 1-4, 2003. Proceedings - [bibtex]
  19. Counter-example Guided Predicate Abstraction of Hybrid Systems. Rajeev Alur, Thao Dang, Franjo Ivancic - Tools and Algorithms for the Construction and Analysis of Systems TACAS'03 - [bibtex]
  20. Progress on Reachability Analysis of Hybrid Systems using Predicate Abstraction. Rajeev Alur, Thao Dang, Franjo Ivancic - Hybrid Systems: Control and Computation HSCC'03 - [bibtex]
  21. Pattern-Based Abstraction for Verifying Secrecy in Protocols. Liana Bozga, Yassine Lakhnech, Michaël Périn - Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 20 - [bibtex]
  22. Storeless semantics and alias logic. Marius Bozga, Radu Iosif, Yassine Lakhnech - Proceedings of the 2003 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2003, San Diego, California, USA, June 7, 2003 - [bibtex]

PhD Thesis and HDR

  1. Modélisation et résolution de problèmes d'ordonnancement à l'aide d'automates temporisés. Yasmina Abdeddaïm - [bibtex]
  2. étude du débogage de systèmes réactifs et application au langage synchrone Lustre. Fabien Gaucher - [bibtex]
  3. Contribution à la validation de systèmes de processus communiquant par files d'attente : analyse statique pour la réduction de files. Manuel Aguilar - [bibtex]

2002

Journal Articles

  1. Testing Theories for Broadcasting Processes. Cristian Ene, Traian Muntean - Sci. Ann. Cuza Univ. - [bibtex]
  2. Iterating Transducers. Dennis Dams, Yassine Lakhnech, Martin Steffen - The Journal of Logic and Algebraic Programming - [bibtex]
  3. Scheduler modelling based on the controller synthesis paradigm. Karine Altisen, Gregor Göessler, Joseph Sifakis - Journal of Real-Time Systems - [bibtex]

Conference Articles

  1. Tools for Controller Synthesis of Timed Systems. Karine Altisen, Stavros Tripakis - 2nd Workshop on Real-Time Tools (RT-TOOLS'2002) - [bibtex]
  2. Using Formal Tools to Study Complex Circuits Behaviour. Paul Amblard, Fabienne Lagnier, Michel Levy - IEEE Symposium on Digital Systems Design (Euromicro DSD 2002) - [bibtex]
  3. Toward an Approximation Theory for Computerised Control. Paul Caspi, Albert Benveniste - 2nd International Workshop on Embedded Software, EMSOFT02 - [bibtex]
  4. A Protocol for Loosely Time-Triggered Architectures. Albert Benveniste, Paul Caspi, Paul Le Guernic, Hervé Marchand, Jean-Pierre Talpin, Stavros Tripakis - 2nd International Wokshop on Embedded Software, EMSOFT02 - [bibtex]
  5. Synchronous modeling of asynchronous systems. Nicolas Halbwachs, Siwar Baghdadi - ACM Conference on Embedded Systems Software, EMSOFT'02 - [bibtex]
  6. Describing Non-Deterministic Reactive Systems by Means of Regular Expressions. Pascal Raymond, Yvan Roux - First Workshop on Synchronous Languages, Applications and Programming, SLAP'02 - Electr. Notes Theor. Comput. Sci. - [bibtex]
  7. Expression of time and duration constraints in SDL. Susanne Graf - 3rd SAM Workshop on SDL and MSC, University of Wales Aberystwyth - [bibtex]
  8. IF-2.0: A Validation Environment for Component-Based Real-Time Systems. Marius Bozga, Susanne Graf, Laurent Mounier - Proceedings of Conference on Computer Aided Verification, CAV'02, Copenhagen - [bibtex]
  9. The d/dt Tool for Verification of Hybrid Systems. Eugène Asarin, Thao Dang, Oded Maler - Computer Aided Verification CAV'02 - [bibtex]
  10. Reachability Analysis Via Predicate Abstraction. Rajeev Alur, Thao Dang, Franjo Ivancic - Hybrid Systems: Computation and Control HSCC'02 - [bibtex]
  11. Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness. Kai Baukus, Yassine Lakhnech, Karsten Stahl - Verification, Model Checking, and Abstract Interpretation, Third International Workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002, Revised Papers - [bibtex]
  12. Symmetry Reduction Criteria for Software Model Checking. Radu Iosif - Model Checking of Software, 9th International SPIN Workshop, Grenoble, France, April 11-13, 2002, Proceedings - [bibtex]

PhD Thesis and HDR

  1. Génération automatique de tests de conformité pour les protocoles de télécommunications. Lucian Ghirvu - [bibtex]
  2. Analyse Algorithmique de Systèmes Hybrides Polygonaux. Gerardo Schneider - [bibtex]

2001

Journal Articles

  1. Argos: an Automaton-Based Synchronous Language. Florence Maraninchi, Yann Rémond - Computer Languages - [bibtex]
  2. Verification of Parameterized Protocols. Kai Baukus, Yassine Lakhnech, Karsten Stahl - Journal of Universal Computer Science - [bibtex]
  3. Verifying Untimed and Timed Aspects of the Experimental Batch Plant. Ralf Huuck, Ben Lukoschus, Yassine Lakhnech - European Journal of Control - [bibtex]
  4. Automatic Verification of Parameterized Networks of Processes. David Lesens, Nicolas Halbwachs, Pascal Raymond - Theoretical Computer Science - [bibtex]

Conference Articles

  1. Analyzing Fair Parametric Extended Automata. Aurore Annichini-Collomb, Ahmed Bouajjani, Yassine Lakhnech, Mihaela Sighireanu - Static Analysis Symposium 2001 - [bibtex]
  2. Model-Checking Ariane-5 Flight Program. Marius Bozga, David Lesens, Laurent Mounier - Proceedings of FMICS'01 (Paris, France) - [bibtex]
  3. Automated validation of distributed software using the IF environment. Marius Bozga, Susanne Graf, Laurent Mounier - Workshop on Software Model-checking, associated with CAV 2001, Paris - [bibtex]
  4. Timed Extensions for SDL. Marius Bozga, Alain Kerbrat, Susanne Graf, Laurent Mounier, Iulian Ober, Daniel Vincent - Proceedings of SDL FORUM'01 (Copenhagen, Denmark) - [bibtex]
  5. From Control System Design to Embedded Code: The Synchronous Data-Flow Approach. Paul Caspi, Pascal Raymond - IEEE-CDC - [bibtex]
  6. A Broadcast-based Calculus for Communicating Systems. Cristian Ene, Traian Muntean - Proceedings of the 15th International Parallel & Distributed Processing Symposium (IPDPS-01), San Francisco, CA, April 23-27, 2001 - [bibtex]
  7. Iterating Transducers. Dennis Dams, Yassine Lakhnech, Martin Steffen - Computer Aided Verification'01 - [bibtex]
  8. Embedded control: from asynchrony to synchrony and back. Paul Caspi - First International Workshop on Embedded Software - [bibtex]
  9. Counter-example generation in symbolic abstract model-checking. Gordon Pace, Nicolas Halbwachs, Pascal Raymond - 6th International Workshop on Formal Methods for Industrial Critical Systems, FMICS'2001 - [bibtex]
  10. Effective programming language support for discrete-continuous mode-switching control systems. Florence Maraninchi, Yann Rémond, Eric Rutten - 40th IEEE Conference on Decision and Control (CDC) - [bibtex]
  11. About the design of distributed control systems: the quasi-synchronous approach. Paul Caspi, Christine Mazuet, Natacha Reynaud-Paligot - Proc. Safecomp'01 - [bibtex]
  12. Automated validation of distributed software using the IF environment. Marius Bozga, Laurent Mounier, Susanne Graf - 2001 IEEE International Symposium on Network Computing and Applications (NCA 2001) - [bibtex]
  13. Verification Experiments on the Mascara Protocol. Susanne Graf, Guoping Jia - Model Checking Software, 8th International SPIN Workshop, Toronto, Canada, May 19-20, 2001, Proceedings - [bibtex]
  14. On Hybrid Control of Under-actuated Mechanical Systems. Eugène Asarin, Sorav Bansal, Thao Dang, Bernard Espiau, Oded Maler - Hybrid Systems: Computation and Control HSCC'01 - [bibtex]
  15. Stability and reachability analysis of a hybrid model of luminescence in the marine bacterium Vibrio Fisheri. Calin Belta, Jonathan Schug, Thao Dang, Vijay Kumar, George Pappas, Harvey Rubin, Paul Dunlap - CDC'01 - Conference on Decision and Control - [bibtex]
  16. d/dt: A Verification Tool for Hybrid Systems. Eugène Asarin, Thao Dang, Oded Maler - CDC'01 - Conference on Decision and Control - [bibtex]
  17. d/dt: a Tool for Reachability Analysis of Continuous and Hybrid systems. Eugène Asarin, Thao Dang, Oded Maler - 5th IFAC Symposium Nonlinear Control Systems NOLCOS - [bibtex]
  18. Exploiting Heap Symmetries in Explicit-State Model Checking of Software. Radu Iosif - 16th IEEE International Conference on Automated Software Engineering (ASE 2001), 26-29 November 2001, Coronado Island, San Diego, CA, USA - [bibtex]
  19. Incremental Verification by Abstraction. Yassine Lakhnech, Saddek Bensalem, Sergey Berezin, Sam Owre - Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 200 - [bibtex]
  20. Temporal Logic Properties of Java Objects. Radu Iosif, Riccardo Sisto - Proceedings of the Thirteenth International Conference on Software Engineering & Knowledge Engineering (SEKE'2001), Sheraton Buenos Aires Hotel, Buenos Aires, Argentina, June 13-15, 2001 - [bibtex]

PhD Thesis and HDR

  1. Vérification d'automates étendus : algorithmes d'analyse symbolique et mise en œuvre. Aurore Annichini-Collomb - [bibtex]
  2. Théorie algébrique des langages formels temps réel. Catalin Dima - [bibtex]
  3. Répartition de programmes synchrones temps-réel. Rym Salem-Habermehl - [bibtex]
  4. Application de la synthèse de contrôleur à l'ordonnancement de systèmes temps-réel. Karine Altisen - [bibtex]
  5. Un support langage pour les modes de fonctionnement des systèmes temps-réel : extension de Lustre par des automates de modes. Yann Rémond - [bibtex]
  6. Compositional Modelling of Real-Time Systems --- Theory and Practice. Gregor Göessler - [bibtex]

2000

Journal Articles

  1. Verification and test generation for the SSCOP protocol. Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Claude Jard, Thierry Jéron, Alain Kerbrat, Pierre Morel, Laurent Mounier - Sci. Comput. Program - [bibtex]
  2. Langages pour la conception de systèmes réactifs. Paul Caspi - Technique et science informatique - [bibtex]

Conference Articles

  1. Abstracting WS1S Systems to Verify Parameterized Networks. Kai Baukus, Saddek Bensalem, Yassine Lakhnech, Karsten Stahl - TACAS'00 - [bibtex]
  2. Utilizing Static Analysis for Programmable Logic Controllers. Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus - ADPM 2000 - The 4th International Conference Automation of Mixed Processes: Hybrid Dynamic Systems - [bibtex]
  3. An Abstract Model For Sequential Function ChartsVerification of Sequential Function Charts using SMV. Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus - WODES 2000 special session Formal Models of PLCs - [bibtex]
  4. Verification of Sequential Function Charts using SMV. Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus - PDPTA 2000 special session on Formal Validation - [bibtex]
  5. Approaches to the Formal Verification of Hybrid Systems. Stefan Kowalewski, Peter Herrmann, Sebastian Engell, Heiko Krumm, Heinz Treseler, Yassine Lakhnech, Ralf Huuck, Ben Lukoschus - Special issue of ``at-Automatisierungstechnik'' on the DFG research program KONDISK - [bibtex]
  6. Verifying Universal Properties of Parameterized Networks. Kai Baukus, Yassine Lakhnech, Karsten Stahl - Formal Techniques in Real-Time and Fault-Tolerant Systems - [bibtex]
  7. Using Static Analysis to Improve Automatic Test Generation. Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu - Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 20 - [bibtex]
  8. SDL for Real Time: What is missing? Marius Bozga, Susanne Graf, Alain Kerbrat, Laurent Mounier, Iulian Ober, Daniel Vincent - Proceedings of SAM'00: 2nd Workshop on SDL and MSC (Grenoble, France) - [bibtex]
  9. Threshold and Bounded-Delay Voting in Critical Control Systems. Paul Caspi, Rym Salem-Habermehl - Formal Techniques in Real-Time and Fault-Tolerant Systems - [bibtex]
  10. A methodology for the construction of scheduled systems. Karine Altisen, Gregor Göessler, Joseph Sifakis - Formal Techniques in Real-Time and Fault-Tolerant Systems 2000 (FTRTFT'00) - [bibtex]
  11. Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems. Jean-Pierre Krimm, Laurent Mounier - Proceedings of TACAS'00 - [bibtex]
  12. A PVS Proof Obligation Generator for Lustre Programs. Cécile Dumas, Paul Caspi - 7th International Conference on Logic for Programming and Automated Reasoning - [bibtex]
  13. Step-wise + Algorithmic debugging for Reactive Programs: LuDiC, a debugger for Lustre. Florence Maraninchi, Fabien Gaucher - AADEBUG'2000 -- Fourth International Workshop on Automated Debugging - [bibtex]
  14. MATOU: An Implementation of Mode-Automata. Florence Maraninchi, Yann Rémond, Yannick Raoul - International Conference on Compiler Construction (CC) - [bibtex]
  15. Running-Modes of Real-Time Systems: A Case-Study with Mode-Automata. Florence Maraninchi, Yann Rémond - 12th Euromicro Conference on Real-Time Systems - [bibtex]
  16. Applying Formal Methods to Industrial Cases: The Language Approach (The Production-Cell and Mode-Automata). Florence Maraninchi, Yann Rémond - 5th International Workshop on Formal Methods for Industrial Critical Systems (FMICS) - [bibtex]
  17. The Quasi-Synchronous Approach to Distributed Control Systems. Paul Caspi, Rym Salem-Habermehl - Proceedings of the Summer School "Modelling and Verification of Parallel Processes (MOVEP'2k), - [bibtex]
  18. Stability of discrete sampled systems. Nicolas Halbwachs, Jean-François Héry, Jen-Claude Laleuf, Xavier Nicollin - 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT'2000 - [bibtex]
  19. A Transformational Approach for Generating Non-linear Invariants. Saddek Bensalem, Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Yassine Lakhnech - Static Analysis, 7th International Symposium, SAS 2000, Santa Barbara, CA, USA, June 29 - July 1, 2000, Proceedings - [bibtex]
  20. IF: A Validation Environment for Timed Asynchronous Systems. Marius Bozga, Lucian Ghirvu, Susanne Graf, Laurent Mounier - Proceedings of Conference on Computer Aided Verification, CAV'00, Chicago - [bibtex]
  21. Approximate Reachability Analysis of Piecewise-Linear Dynamical Systems. Eugène Asarin, Oded Maler - Hybrid Systems: Computation and Control HSCC'00 - [bibtex]
  22. Formal verification applied to Java concurrent software. Radu Iosif - Proceedings of the 22nd International Conference on on Software Engineering, ICSE 2000, Limerick Ireland, June 4-11, 2000 - [bibtex]
  23. Abstracting WS1S Systems to Verify Parameterized Networks. Kai Baukus, Saddek Bensalem, Yassine Lakhnech, Karsten Stahl - Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 20 - [bibtex]
  24. Using Garbage Collection in Model Checking. Radu Iosif, Riccardo Sisto - SPIN Model Checking and Software Verification, 7th International SPIN Workshop, Stanford, CA, USA, August 30 - September 1, 2000, Proceedings - [bibtex]

PhD Thesis and HDR

  1. Méthodes déductives pour la preuve de programmes Lustre. Cécile Dumas Canovas - [bibtex]
  2. Partitionnement dynamique dans l'analyse de relations linéaires et application à la vérification de programmes synchrones. Bertrand Jeannet - [bibtex]
  3. Applications des ordres partiels à la génération compositionelle de systèmes asynchrones. Jean-Pierre Krimm - Thèse de doctorat - [bibtex]
  4. V'erification et synth`ese des syst`emes hybrides. Thao Dang - [bibtex]

1999

Journal Articles

  1. Automatic Distribution of Reactive Systems for Asynchronous Networks of Processors. Paul Caspi, Alain Girault, Daniel Pilaud - IEEE Transactions on Software Engineering - [bibtex]
  2. Automatic Generation of Invariants. Saddek Bensalem, Yassine Lakhnech - Formal Methods in System Design - [bibtex]
  3. Characterization of a sequentially consistent memory and verification of a cache memory by abstraction. Susanne Graf - Distributed Computing - [bibtex]
  4. A Deadlock Detection Tool for Concurrent Java Programs. Claudio Demartini, Radu Iosif, Riccardo Sisto - Softw., Pract. Exper. - [bibtex]

Conference Articles

  1. Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. Parosh Aziz Abdulla, Aurore Annichini-Collomb, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl, Yassine Lakhnech - Computer Aided Verification'99 - [bibtex]
  2. A Framework for Scheduler Synthesis. Karine Altisen, Gregor Göessler, Amir Pnueli, Joseph Sifakis, Stavros Tripakis, Sergio Yovine - RTSS'99 - [bibtex]
  3. Validation of Synchronous Reactive Systems: from Formal Verification to Automatic Testing. Nicolas Halbwachs, Pascal Raymond - ASIAN'99, Asian Computing Science Conference - [bibtex]
  4. A methodology for proving control systems with Lustre and PVS. Saddek Bensalem, Paul Caspi, Cécile Dumas, Catherine Parent-Vigouroux - Dependable Computing for Critical Applications (DCCA7) - [bibtex]
  5. State Space Reduction Based on Live Variables Analysis. Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu - SAS - [bibtex]
  6. Expressiveness of Point-to-Point versus Broadcast Communications. Cristian Ene, Traian Muntean - Fundamentals of Computation Theory, 12th International Symposium, FCT '99, Iasi, Romania, August 30 - September 3, 1999, Proceedings - [bibtex]
  7. On-the-fly controller synthesis for discrete and dense time systems. Stavros Tripakis, Karine Altisen - Formal Methods 1999 (FM'99) - [bibtex]
  8. Formal Design of Distributed Control Systems with Lustre. Paul Caspi, Christine Mazuet, Rym Salem-Habermehl, Daniel Weber - Proc. Safecomp'99 - [bibtex]
  9. Dynamic Partitioning in Analyses of Numerical Properties. Bertrand Jeannet, Nicolas Halbwachs, Pascal Raymond - Static Analysis Symposium, SAS'99 - [bibtex]
  10. Divide, abstract and model-check. Karsten Stahl, Kai Baukus, Yassine Lakhnech, Martin Steffen - Proceedings of the 5th International SPIN Workshop on Theoretical Aspects of Model Checking - [bibtex]
  11. IF: An Intermediate Representation for SDL and its Applications. Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier, Joseph Sifakis - Proceedings of SDL Forum 99, Montreal - [bibtex]
  12. IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems. Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier - Proceedings of Symposium on Formal Methods 99, Toulouse - [bibtex]
  13. Divide, Abstract, and Model-Check. Karsten Stahl, Kai Baukus, Yassine Lakhnech, Martin Steffen - Theoretical and Practical Aspects of SPIN Model Checking, 5th and 6th International SPIN Workshops, Trento, Italy, July 5, 1999, Toulouse, France, September 21 and 24 1999, Proceedings - [bibtex]
  14. dSPIN: A Dynamic Extension of SPIN. Claudio Demartini, Radu Iosif, Riccardo Sisto - Theoretical and Practical Aspects of SPIN Model Checking, 5th and 6th International SPIN Workshops, Trento, Italy, July 5, 1999, Toulouse, France, September 21 and 24 1999, Proceedings - [bibtex]

PhD Thesis and HDR

  1. Vérification symbolique pour les protocoles de communication. Marius Bozga - Thèse de doctorat - [bibtex]
  2. Contribution at the Definition and Implementation of E-LOTOS. Mihaela Sighireanu - [bibtex]
  3. Complexité Algorithmique des Systèmes Dynamiques Continus et Hybrides. Olivier Bournez - [bibtex]

1998

Journal Articles

  1. On Complexity of Reachability of Transition Restricted Petri Nets. Cristian Ene - Sci. Ann. Cuza Univ. - [bibtex]
  2. About synchronous programming and abstract interpretation. Nicolas Halbwachs - Science of Computer Programming, Special Issue on SAS'94 - [bibtex]
  3. Integrating Timed Condition/Event Systems and Timed Automata to the Verification of Hybrid Systems. Ralf Huuck, Yassine Lakhnech, Ben Lukoschus, Luis Urbina, Sebastian Engell, Stefan Kowalewski, Jorg Preußig - Journal of Parallel and Distributed Computing Practices - [bibtex]

Conference Articles

  1. A tool for proving Lustre programs in PVS. Saddek Bensalem, Paul Caspi, Cécile Dumas, Catherine Parent-Vigouroux - TOOLS'98 - [bibtex]
  2. Computing Abstractions of Infinite State Systems Automatically and Compositionally. Saddek Bensalem, Yassine Lakhnech, Sam Owre - Computer Aided Verification - [bibtex]
  3. InVeSt : A Tool for the Verification of Invariants. Saddek Bensalem, Yassine Lakhnech, Sam Owre - Computer Aided Verification - [bibtex]
  4. A Co-iterative Characterization of Synchronous Stream Functions. Paul Caspi, Marc Pouzet - Proceedings of the Workshop on Coalgebraic Methods in Computer Science, Lisbon - [bibtex]
  5. Synchronous programming of reactive systems, a tutorial and commented bibliography. Nicolas Halbwachs - Tenth International Conference on Computer-Aided Verification, CAV'98 - [bibtex]
  6. Verifying Statecharts with Spin. Gerard J. Holzmann, Erich Mikk, Yassine Lakhnech, Michael Siegel - Proc. Workshop on Industrial-strength Formal specification Techniques - [bibtex]
  7. On the Composition of Condition/Event Systems. Stefan Kowalewski, Yassine Lakhnech, Ben Lukoschus, Luis Urbina - WODES'98 - [bibtex]
  8. Test automatique de systèmes réactifs. Nicolas Halbwachs, Xavier Nicollin, Pascal Raymond, Daniel Weber - Ecole d'été ``MOdélisation et VÉrification des Processus parallèles - [bibtex]
  9. Automatic Testing of Reactive Systems. Pascal Raymond, Daniel Weber, Xavier Nicollin, Nicolas Halbwachs - 19th IEEE Real-Time Systems Symposium - [bibtex]
  10. Mode-Automata: About Modes and States for Reactive Systems. Florence Maraninchi, Yann Rémond - European Symposium On Programming (ESOP) - [bibtex]
  11. Implementing Statecharts in Promela/SPIN. Erich Mikk, Yassine Lakhnech, Michael Siegel, Gerard J. Holzmann - Proceedings of the 2nd IEEE Workshop on Industrial-Strength Formal Specification Techniques - [bibtex]
  12. Reachability Analysis via Face Lifting. Thao Dang, Oded Maler - Hybrid Systems: Computation and Control HSCC'98 - [bibtex]
  13. Implementing Statecharts in PROMELA/SPIN. Erich Mikk, Yassine Lakhnech, Michael Siegel, Gerard J. Holzmann - 2nd Workshop on Industrial-Strength Formal Specification Techniques (WIFT '98), October 20-23, 1998, Boca Raton, FL, USA - [bibtex]

PhD Thesis and HDR

  1. De la composition de systèmes temporisés. Sébastien Bornot - [bibtex]
  2. Méthodes d'analyse de systèmes temporisés : de la théorie à la pratique. Conrado Daws - [bibtex]
  3. Vérification des propriétés temporelles des programmes parallèles. Radu Mateescu - [bibtex]
  4. Sur la Vérification de Systèmes Infinis. Peter Habermehl - [bibtex]
  5. Combinaison de Méthodes Déductives et Arithméthiques pour la Vérification. Hassen Saidi - [bibtex]
  6. L'Analyse Formelle de Systèmes Temporisés en Pratique. Stavros Tripakis - [bibtex]

1997

Journal Articles

  1. Protocol Verification with the Aldebaran Toolset. Marius Bozga, Jean-Claude Fernandez, Alain Kerbrat, Laurent Mounier - Software Tools for Technology Transfer - [bibtex]
  2. Hierarchies of Petri Net Languages and a Super-Normal Form. Ferucio Laurentiu Tiplea, Cristian Ene - Journal of Automata, Languages and Combinatorics - [bibtex]
  3. An Experiment in Automatic Generation of Test Suites for Protocols with Verification Technology. Jean-Claude Fernandez, Claude Jard, Thierry Jéron, César Viho - Sci. Comput. Program. - [bibtex]
  4. Distributing Automata for Asynchronous Networks of Processors. Benoît Caillaud, Paul Caspi, Alain Girault, Claude Jard - Journal Européen des Systèmes Automatisés - [bibtex]
  5. Verifying programs in the Calculus of Inductive Constructions. Catherine Parent-Vigouroux - Formal Aspects of Computing - [bibtex]
  6. Verification of real-time systems using linear relation analysis. Nicolas Halbwachs, Yann-Eric Proy, Patrick Roumanoff - Formal Methods in System Design - [bibtex]

Book Chapters

  1. Aperçu du langage Lustre. Paul Caspi - Applications des Méthodes Formelles au Logiciel - [bibtex]

Conference Articles

  1. What can we learn from synchronous data-flow languages. Paul Caspi - Hybrid and Real-Time Systems - [bibtex]
  2. Combining a Computer Science and Control Theory Approach to the Verification of Hybrid Systems. Ralf Huuck, Yassine Lakhnech, Luis Urbina, Sebastian Engell, Stefan Kowalewski, Jorg Preußig - WPDRTS'97 - [bibtex]
  3. Comparing Timed Condition/Event Systems and Timed Automata. Ralf Huuck, Yassine Lakhnech, Luis Urbina, Sebastian Engell, Stefan Kowalewski, Jorg Preußig - HART'97 - [bibtex]
  4. Using Model--Checking for Timed Automata to Parameterize Logic Control Programs. Stefan Kowalewski, Sebastian Engell, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus, Luis Urbina - 8th European Symposium on Computer Aided Engineering - [bibtex]
  5. Compositional State Space Generation from Lotos Programs. Jean-Pierre Krimm, Laurent Mounier - Proceedings of TACAS'97 (Tools and Algorithms for the Construction and Analysis of Systems), Enschede, The Netherlands - [bibtex]
  6. Automatic Verification of Parameterized Linear Networks of Processes. David Lesens, Nicolas Halbwachs, Pascal Raymond - 24th ACM Symposium on Principles of Programming Languages, POPL'97 - [bibtex]
  7. A Kleene Theorem for Timed Automata. Eugène Asarin, Oded Maler, Paul Caspi - Proc. Logic in Computer Science, LICS'97 - [bibtex]
  8. Temporal Logic for Stabilizing Systems. Yassine Lakhnech, Michael Siegel - Second International Conference on Temporal Logic - ICTL'97 - [bibtex]
  9. On formal semantics of Statecharts as supported by STATEMATE. Erich Mikk, Yassine Lakhnech, Carsta Petersohn, Michael Siegel - 2nd BCS-FACS Northern Formal Methods Workshop - [bibtex]
  10. Towards Efficient Modelchecking Statecharts: A Statecharts to Promela Complier. Yassine Lakhnech, Erich Mikk, Michael Siegel - 3rd International SPIN Workshop - [bibtex]
  11. Towards Efficient Modelchecking Statecharts. Erich Mikk, Yassine Lakhnech, Michael Siegel - STATEMATE Anwenderforum 97 - [bibtex]
  12. On the Formal Semantics of Statecharts as Supported by STATEMATE. Yassine Lakhnech, Erich Mikk, Carsta Petersohn, Michael Siegel - Proc. of the BCS-FACS second Northern Formal Methods Workshop, Ilkley, 14-15th July - [bibtex]
  13. Hierarchical automata as model for statecharts. Yassine Lakhnech, Erich Mikk, Michael Siegel - Proc. of the Asian Computing Science Conference (ASIAN'97) - [bibtex]
  14. Compositionality Criteria for Defining Mixed-Styles Synchronous Languages (invited paper). Florence Maraninchi, Yann Rémond - International Symposium: Compositionality - The Significant Difference - [bibtex]
  15. Construction of abstract state graphs with PVS. Susanne Graf, Hassen Saidi - Conference on Computer Aided Verification CAV'97, Haifa - [bibtex]
  16. Deductive verification of stabilizing systems. Yassine Lakhnech, Michael Siegel - 3rd Workshop on Self-stabilizing Systems, Santa Barbara, California, August, 1997, Proceedings - [bibtex]

PhD Thesis and HDR

  1. HDR - Modélisation et validation des systèmes réactifs : un langage synchrone à base d'automates. Florence Maraninchi - Document d’Habilitation à Diriger des Recherches - [bibtex]
  2. Vérification et synthèse de systèmes réactifs. David Lesens - [bibtex]

1996

Journal Articles

  1. Specification and Verification of various Distributed Leader Election Algorithms for Unidirectional Ring Networks. Hubert Garavel, Laurent Mounier - Science of Computer Programming - [bibtex]
  2. Compositional Minimisation of Finite State Systems using Interface Specifications. Susanne Graf, Gerald Lüttgen, Bernhard Steffen - Formal Aspects of Computation - [bibtex]

Conference Articles

  1. Compiling ARGOS into Boolean equations. Florence Maraninchi, Nicolas Halbwachs - Formal Techniques for Real-Time and Fault Tolerance (FTRTFT) - [bibtex]
  2. Vérification de systèmes réactifs en Argos temporisé. Muriel Jourdan, Florence Maraninchi - Congrès AFCET : Modélisation des systèmes réactifs - [bibtex]
  3. Powerful Techniques for the Automatic Generation of Invariants. Saddek Bensalem, Yassine Lakhnech, Hassen Saidi - 8th International Conference on Computer Aided Verification - [bibtex]
  4. Model Checking for Extended Timed Temporal Logics. Ahmed Bouajjani, Yassine Lakhnech, Sergio Yovine - 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems FTRTFT'96 - [bibtex]
  5. Un modèle pour la distribution d'automates réactifs sur réseau asynchrone de processeurs. Benoît Caillaud, Paul Caspi, Alain Girault, Claude Jard - Conférence Afcet sur la Modélisation des systèmes réactifs, Brest - [bibtex]
  6. Specification and Verification of the PowerScale Bus Arbitration Protocol: An Industrial Experiment with LOTOS. Ghassan Chehaibar, Hubert Garavel, Laurent Mounier, Nadia Tawbi, Ferruccio Zulian - Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification FORTE/PST - [bibtex]
  7. Using On-The-Fly Verification Techniques for the Generation of test Suites. Jean-Claude Fernandez, Claude Jard, Thierry Jéron, César Viho - Computer Aided Verification, 8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings - [bibtex]
  8. Compositional Semantics of Non-deterministic Synchronous Languages. Florence Maraninchi, Nicolas Halbwachs - European Symposium On Programming (ESOP) - [bibtex]
  9. CADP - A Protocol Validation and Verification Toolbox. Jean-Claude Fernandez, Hubert Garavel, Alain Kerbrat, Laurent Mounier, Radu Mateescu, Mihaela Sighireanu - Computer Aided Verification, 8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings - [bibtex]
  10. Verifying invariants using theorem proving. Susanne Graf, Hassen Saidi - Conference on Computer Aided Verification CAV'96 - [bibtex]
  11. Synchronous Kahn networks. Paul Caspi, Marc Pouzet - Int. Conf. on Functional Programming - [bibtex]
  12. Réseaux de Kahn synchrones. Marc Pouzet, Paul Caspi - Journées Francophones des langages applicatifs, Val Morin, Quebec - [bibtex]
  13. Automatic Construction of Network Invariants. David Lesens, Nicolas Halbwachs, Pascal Raymond - International Workshop on Verification of Infinite State Systems (INFINITY) - [bibtex]
  14. Translating Statecharts to Promela/SPIN. Erich Mikk, Yassine Lakhnech, Michael Siegel - Dagstuhl-Seminar ``Synchronous Languages'' - [bibtex]
  15. Natural proofs and programs optimization in the Calculus of Inductive Constructions. Catherine Parent-Vigouroux - International Conference on Theorem Proving in Higher Order Logic - [bibtex]
  16. Recognizing Regular Expressions by Means of Dataflow Networks. Pascal Raymond - Automata, Languages and Programming, 23rd International Colloquium - [bibtex]
  17. Modular Completeness: Integrating the Reuse of Specified Software in Top-Down Program Development. Job Zwiers, Ulrich Hannemann, Yassine Lakhnech, Frank Stomp, Willem-Paul De Roever - Formal Methods Europe, FME'96 Symposium - [bibtex]
  18. Model-Checking for Extended Timed Temporal Logics. Ahmed Bouajjani, Yassine Lakhnech, Sergio Yovine - Formal Techniques in Real-Time and Fault-Tolerant Systems, 4th International Symposium, FTRTFT'96, Uppsala, Sweden, September 9-13, 1996, Proceedings - [bibtex]

1995

Journal Articles

  1. Metric temporal logic with durations. Yassine Lakhnech, Jozef Hooman - Theoretical Computer Science - [bibtex]
  2. The Algorithmic Analysis of Hybrid Systems. Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, Sergio Yovine - Theoretical Computer Science B - [bibtex]
  3. Property Preserving Abstractions for the Verification of Concurrent Systems. Claire Loiseaux, Susanne Graf, Joseph Sifakis, Ahmed Bouajjani, Saddek Bensalem - Formal Methods in System Design - [bibtex]

Conference Articles

  1. The railroad crossing problem, modeling with Hybrid Argos - Analysis with Polka. Nicolas Halbwachs, Florence Maraninchi, Yann-Eric Proy - Second European Workshop on Real-Time and Hybrid Systems - [bibtex]
  2. Static Timing Analysis of Real-Time Systems. Muriel Jourdan, Florence Maraninchi - ACM Sigplan Workshop on Language, compiler and tool support for real-time systems - [bibtex]
  3. Temporal logic + timed automata : expressiveness and decidability. Ahmed Bouajjani, Yassine Lakhnech - CONCUR'95: Concurrency Theory - [bibtex]
  4. From duration calculus to linear hybrid automata. Ahmed Bouajjani, Yassine Lakhnech, Riadh Robbana - Computer Aided Verification - [bibtex]
  5. An Algorithm for Reducing Binary Branchings. Paul Caspi, Jean-Claude Fernandez, Alain Girault - Foundations of Software Technology and Theoretical Computer Science, FSTTCS, 15th Conference, Bangalore, India, December 18-20, 1995, Proceedings - [bibtex]
  6. An algorithm for reducing binary branchings. Paul Caspi, Jean-Claude Fernandez, Alain Girault - Fifteenth Conference on the Foundations of Software Technology and Theoretical Computer Science, FST&TCS - [bibtex]
  7. Hierarchies of Petri Net Languages and a Super-Normal Form. Ferucio Laurentiu Tiplea, Cristian Ene - Developments in Language Theory - [bibtex]
  8. On the symbolic analysis of combinational loops in circuits and synchronous programs. Nicolas Halbwachs, Florence Maraninchi - Euromicro'95 - [bibtex]
  9. A functional extension to Lustre. Paul Caspi, Marc Pouzet - 8th Int. Symp. on Languages for Intensional Programming - [bibtex]
  10. Formal verification of a critical system written in Saga/Lustre. Fabienne Lagnier, Pascal Raymond, Christian Dubois - Workshop on Formal Methods, Modelling and Simulation for System Engineering - [bibtex]
  11. Vérification de propriétés de programmes écrits en Lustre. Christian Dubois, Paul Ghaleb, Fabienne Lagnier, Pascal Raymond - RTS'95 - [bibtex]
  12. Execution of reactive distributed systems. Paul Caspi, Alain Girault - EURO--PAR'95, Stockholm - [bibtex]
  13. Synthesizing different development paradigms: Combining top-down with bottom-up reasoning about distributed systems. Job Zwiers, Ulrich Hannemann, Yassine Lakhnech, Willem-Paul De Roever - FST & TCS Bangalore - [bibtex]
  14. Logics vs. Automata: The Hybrid Case. Ahmed Bouajjani, Yassine Lakhnech - Hybrid Systems III: Verification and Control, Proceedings of the DIMACS/SYCON Workshop, October 22-25, 1995, Ruttgers University, New Brunswick, NJ, USA - [bibtex]

PhD Thesis and HDR

  1. Spécification et Vérification de Systèmes Hybrides. Riadh Robbana - [bibtex]

1994

Journal Articles

  1. Some Decision Problems for Parallel Communicating Grammar Systems. Ferucio Laurentiu Tiplea, Cristian Ene, Cecilia Magdalena Ionescu, Octavian Procopiuc - Theor. Comput. Sci. - [bibtex]

Book Chapters

  1. Tolérance aux fautes logicielles. Paul Caspi, Jean-Claude Laprie - Informatique tolérante aux fautes - [bibtex]

Conference Articles

  1. A Modular State/Transition Approach for Programming Real-Time Systems. Muriel Jourdan, Florence Maraninchi - ACM Sigplan Workshop on Language, compiler and tool support for real-time systems - [bibtex]
  2. A Multiparadigm Language for Reactive Systems. Muriel Jourdan, Fabienne Lagnier, Pascal Raymond, Florence Maraninchi - In 5th IEEE International Conference on Computer Languages - [bibtex]
  3. Model-Based Verification Methods and Tools (Abstract). Jean-Claude Fernandez, Joseph Sifakis, Robert De Simone - CONCUR '94, Concurrency Theory, 5th International Conference, Uppsala, Sweden, August 22-25, 1994, Proceedings - [bibtex]
  4. Distributing Reactive Systems. Paul Caspi, Alain Girault, Daniel Pilaud - Seventh International Conference on Parallel and Distributed Computing Systems, PDCS'94 - [bibtex]
  5. Verification of linear hybrid systems by means of convex approximations. Nicolas Halbwachs, Yann-Eric Proy, Pascal Raymond - International Symposium on Static Analysis, SAS'94 - [bibtex]
  6. About synchronous programming and abstract interpretation. Nicolas Halbwachs - International Symposium on Static Analysis, SAS'94 - [bibtex]
  7. Studying Synchronous Communication Mechanisms by Abstractions. Muriel Jourdan, Florence Maraninchi - IFIP Working Conference on Programming Concepts, Methods and Calculi - [bibtex]
  8. Towards recursive block diagrams. Paul Caspi - Proc. 19th IFAC/IFIP Workshop on real-time programming, Isle of Reichenau - [bibtex]
  9. Verification of a distributed Cache memory by using abstractions. Susanne Graf - Conference on Computer Aided Verification CAV'94, Stanford - [bibtex]
  10. Reasoning about durations in metric temporal logic. Yassine Lakhnech, Jozef Hooman - Third International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems - [bibtex]

PhD Thesis and HDR

  1. Sur la répartition de programmes synchrones. Alain Girault - [bibtex]
  2. Méthodes symboliques pour la vérification de Processus Communicants : étude et mise en oeuvre. Alain Kerbrat - [bibtex]
  3. Vérification symbolique de programmes réactifs à l'aide d'abstractions. Claire Loiseaux - [bibtex]
  4. Etude d'un environnement de programmation et de vérification des systèmes réactifs, multi-langages et multi-outils. Muriel Jourdan - [bibtex]
  5. Modélisation et analyse de systèmes temporisés et hybrides. Alfredo Olivero - [bibtex]

1993

Journal Articles

  1. A Coverability Structure for Parallel Communicating Grammar Systems. Ferucio Laurentiu Tiplea, Cristian Ene - Elektronische Informationsverarbeitung und Kybernetik - [bibtex]

Conference Articles

  1. Embedding declarative subprograms into imperative constructs. Muriel Jourdan, Fabienne Lagnier, Florence Maraninchi, Pascal Raymond - Fifth International Symposium on Programming Language Implementation and Logic Programming, Tallin, Estonia - [bibtex]
  2. Data-flow synchronous languages. Albert Benveniste, Paul Caspi, Paul Le Guernic, Nicolas Halbwachs - Rex Symposium ``Ten Years of Concurrency, Reflections and Perspectives'' - [bibtex]
  3. Abstract Interpretation and Verification of Reactive Systems. Jean-Claude Fernandez - Static Analysis, Third International Workshop, WSA'93, Padova, Italy, September 22-24, 1993, Proceedings - [bibtex]
  4. Symbolic Equivalence Checking. Jean-Claude Fernandez, Alain Kerbrat, Laurent Mounier - Proceedings of the 5th Workshop on Computer-Aided Verification (Heraklion, Greece) - [bibtex]
  5. Program Verification using compositional Abstraction. Susanne Graf, Claire Loiseaux - TAPSOFT 93, joint conference CAAP/FASE - [bibtex]
  6. An executable temporal logic to express safety properties and its connection with the language Lustre. Nicolas Halbwachs, Jean-Claude Fernandez, Ahmed Bouajjani - Sixth International Symp. on Lucid and Intensional Programming, ISLIP'93 - [bibtex]
  7. Verifying quantitative real-time properties of synchronous programs. Muriel Jourdan, Florence Maraninchi, Alfredo Olivero - International Conference on Computer-Aided Verification (CAV) - [bibtex]
  8. Rôle de l'expression fonctionnelle dans l'enseignement de l'informatique en DEUG A. Florence Maraninchi, Pierre-Claude Scholl, Marie-Christine Fauvet, Fabienne Lagnier - 2èmes journées de travail : les langages applicatifs dans l'enseignement de l 'informatique - [bibtex]
  9. Lucid Synchrone. Paul Caspi - Actes du colloque INRIA OPOPAC, Lacanau - [bibtex]
  10. Delay analysis in synchronous programs. Nicolas Halbwachs - Fifth Conference on Computer-Aided Verification - [bibtex]
  11. A tool for symbolic program verification and abstraction. Susanne Graf, Claire Loiseaux - Conference on Computer Aided Verification CAV 93, Heraklion Crete - [bibtex]
  12. A tool implementing a method for symbolic program verification. Susanne Graf, Claire Loiseaux - Proceedings of "Formale Methoden zum Entwurf korrekter Systeme", Bad Herrenalb - [bibtex]
  13. Synchronous observers and the verification of reactive systems. Nicolas Halbwachs, Fabienne Lagnier, Pascal Raymond - Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93 - [bibtex]

PhD Thesis and HDR

  1. Méthodes et outils pour la vérification symbolique de systèmes temporisés. Sergio Yovine - [bibtex]

1992

Journal Articles

  1. An experience in proving regular networks of processes by modular model checking. Nicolas Halbwachs, Fabienne Lagnier, Christophe Ratel - Acta Informatica - [bibtex]
  2. Clocks in Dataflow languages. Paul Caspi - Theoretical Computer Science - [bibtex]
  3. Minimal State Graph Generation. Ahmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs, Pascal Raymond - Sci. Comput. Program. - [bibtex]
  4. On-the-Fly Verification of Finite Transition Systems. Jean-Claude Fernandez, Laurent Mounier, Claude Jard, Thierry Jéron - Formal Methods in System Design - [bibtex]
  5. Programming and verifying critical systems by means of the synchronous data-flow programming language Lustre. Nicolas Halbwachs, Fabienne Lagnier, Christophe Ratel - IEEE Transactions on Software Engineering, Special Issue on the Specification and Analysis of Real-Time Systems - [bibtex]

Conference Articles

  1. Operational and Compositional Semantics of Synchronous Automaton Compositions. Florence Maraninchi - International Conference on Concurrency Theory (CONCUR) - [bibtex]
  2. Minimization of timed transition systems (extended abstract). Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, David Dill, Howard Wong-Toi - CONCUR'92 - [bibtex]
  3. A Toolbox for the Verification of LOTOS Programs. Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodríguez, Joseph Sifakis - Proceedings of the 14th International Conference on Software Engineering ICSE'14 (Melbourne, Australia) - [bibtex]
  4. An Experience in compiling a mixed imperative/declarative language for reactive systems. Florence Maraninchi, Muriel Vachon - International Workshop on Compiler Construction (poster session) - [bibtex]
  5. Distributing a finite transition system on a shared/distributed memory system. Alain Girault, Paul Caspi - PARLE'92 Paris - [bibtex]
  6. An implementation of three algorithms for timing verification based on automata emptiness. Rajeev Alur, Costas Courcoubetis, David Dill, Nicolas Halbwachs, Howard Wong-Toi - 13th IEEE Real-Time Systems Symposium - [bibtex]
  7. Provably Correct Compiler Development and Implementation. Bettina Buth, Karl-Heinz Buth, Martin Fränzle, Burghard Karger, Yassine Lakhnech, Hans Langmaack, Markus Müller-Olm - Compiler Construction, 4th International Conference on Compiler Construction, CC'92, Paderborn, Germany, October 5-7, 1992, Proceedings - [bibtex]

PhD Thesis and HDR

  1. Vérification des systèmes matérieles numériques séquentiels synchrones : Application du langage Lustre et de l'outil de vérification Lesar. Bachir Berkane - [bibtex]
  2. Méthodes de Vérification de Spécifications Comportementales : étude et mise en oeuvre. Laurent Mounier - [bibtex]
  3. ATP: une algèbre pour la spécification et l'analyse des systèmes temps reel. Xavier Nicollin - [bibtex]
  4. Définition et réalisation d'un outil de vérification Formelle de Programmes Lustre : Le système LESAR. Christophe Ratel - [bibtex]
  5. Extension du langage Lustre et application à la conception de circuits : Le langage Lustre-V4 et le système POLLUX. Frédéric Rocheteau - [bibtex]

Contact | Site Map | Site created with SPIP 2.1.26 + AHUNTSIC [CC License]

Logged in visitors: 12 ; visits: 391163