Verimag

by years

2015

Journal Articles

  1. Knowledge-based Construction of Distributed Constrained Systems. Susanne Graf, Sophie Quinton - Journal on Software and Systems Modeling, SoSym - [bibtex]

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]
  3. Component-based verification using incremental design and invariants. Saddek Bensalem, Marius Bozga, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan - Software & Systems Modeling - [bibtex]
  4. Statitical Model-Checking QoS Properties of Systems with SBIP. Ayoub Nouri, Saddek Bensalem, Marius Bozga, Benoît Delahaye, Cyril Jegourel, Axel Legay - STTT - [bibtex]
  5. Synthesizing robust systems. Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Georg Hofferek, Barbara Jobstmann, Bettina Könighofer, Robert Könighofer - Acta Inf. - [bibtex]
  6. Distributed Implementation of Constrained Systems based on Knowledge. Susanne Graf, Sophie Quinton - Journal on Software and Systems Modeling, SoSym - [bibtex]
  7. Analyse de Code et Recherche de Vulnérabilités. Marie-Laure Potet, Josselin Feist, Laurent Mounier - Revue MISC - [bibtex]

Book Chapters

  1. Contract-Based Reasoning for Component Systems with Rich Interactions. Susanne Graf, Roberto Passerone, Sophie Quinton - Embedded Systems Development - [bibtex]

Conference Articles

  1. 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]
  2. 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]
  3. Architecture Internalisation in BIP. Simon Bliudze, Marius Bozga, Mohamad Jaber, Joseph Sifakis - Proceedings of CBSE'14 - The 7th International ACM Sigsoft Symposium on Component-Based Software Engineering - Lille, France - [bibtex]
  4. Model-driven Information Flow Security for Component-Based Systems. Najah Ben Said, Takoua Abdellatif, Saddek Bensalem, Marius Bozga - Proceedings of FPS'14 - From Programs to Systems - The Systems Perspective in Computing, ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis - [bibtex]
  5. Model-based validation of CANopen systems. Alexios Lekidis, Marius Bozga, Saddek Bensalem - Proceedings of WFCS'14 - 10th IEEE International Workshop on Factory Communication Systems, Toulouse, France - [bibtex]
  6. 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]
  7. Modular and lightweight certification of polyhedral abstract domains. Alexis Fouilhé, Sylvain Boulmé, Michaël Périn - Types for Proofs and Programs (TYPES 2014) -- Book of Abstracts - [bibtex]
  8. A certifying frontend for (sub)polyhedral abstract domains. Alexis Fouilhé, Sylvain Boulmé - Verified Software: Theories, Tools and Experiments (VSTTE 2014) - [bibtex]
  9. Distributed Implementation of Constrained Systems based on Knowledge. Susanne Graf - IEEE 13th International Symposium on Parallel and Distributed Computing, ISPDC 2013, Porquerolles Golden Island, France, June 24-27, 2014 - [bibtex]
  10. LiSTT: An Investigation into Unsound-incomplete Yet Practical Result Yielding Static Taintflow Analysis. Sanjay Rawat, Laurent Mounier, Marie-Laure Potet - Proceedings of SAW 2014 (ARES Workshop) - [bibtex]
  11. (In)Corruptibility of Routing Protocols. Raphaël Jamet, Pascal Lafourcade - Foundations and Practice of Security - 7th International Symposium, FPS 2014, Montréal, Canada, 2014 - [bibtex]
  12. Formal Verification of e-Reputation Protocols. Ali Kassem, Pascal Lafourcade, Yassine Lakhnech - Foundations and Practice of Security - 7th International Symposium, FPS 2014, Montréal, Canada - [bibtex]
  13. Formal Analysis of Electronic Exams. Jannik Dreier, Rosario Giustolisi, Ali Kassem, Pascal Lafourcade, Gabriele Lenzin, Peter Ryan - SECRYPT 2014 - [bibtex]

PhD Thesis and HDR

  1. Vérification et synthèse quantitative. Christian von Essen - [bibtex]

2013

Journal Articles

  1. Rigorous embedded design: challenges and perspectives. Saddek Bensalem, Axel Legay, Marius Bozga - STTT - [bibtex]
  2. Rigorous implementation of real-time systems - from theory to application. Tesnim Abdellatif, Jacques Combaz, Joseph Sifakis - Mathematical Structures in Computer Science - [bibtex]
  3. Automata-Based Termination Proofs. Radu Iosif, Adam Rogalewicz - Computing and Informatics - [bibtex]
  4. Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation. Ylies Falcone, Mohamad Jaber, Thanh-Hung Nguyen, Marius Bozga, Saddek Bensalem - Software & Systems Modeling - [bibtex]
  5. Algorithmic program synthesis: introduction. Rastislav Bodík, Barbara Jobstmann - STTT - [bibtex]
  6. BioScape: A Modeling and Simulation Language for Bacteria-Materials Interactions. Adriana B. Compagnoni, Vishakha Sharma, Yifei Bao, Matthew Libera, Svetlana Sukhishvili, Philippe Bidinger, Livio Bioglio, Eduardo Bonelli - Electr. Notes Theor. Comput. Sci. - [bibtex]

Book Chapters (inbook)

  1. Smart Multicore Embedded Systems. Marius Bozga, Georgios Chasapis, Vassilios Dimakopoulos, Aggelis Aggelis - [bibtex]

Conference Articles

  1. Underapproximation of Procedure Summaries for Integer Programs. Pierre Ganty, Radu Iosif, Filip Kone\vcn\'y - TACAS - [bibtex]
  2. As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty. Jean-Francois Kempf, Marius Bozga, Oded Maler - TACAS - PDF - [bibtex]
  3. 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]
  4. 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]
  5. 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]
  6. Verifiability in E-Auction Protocols. Jannik Dreier, Hugo Jonker, Pascal Lafourcade - 1st Workshop on Hot Issues in Security Principles and Trust (HotSpot 2013) - [bibtex]
  7. 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]
  8. 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]
  9. 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]
  10. 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]
  11. 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]
  12. 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]
  13. 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]
  14. 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]
  15. 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]
  16. 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]
  17. 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]
  18. 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]
  19. Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra. Alexis Fouilhé, David Monniaux, Michaël Périn - Static analysis (SAS) - [bibtex]
  20. Incremental Generation of Linear Invariants for Component-Based Systems. Saddek Bensalem, Marius Bozga, Benoît Boyer, Axel Legay - 13th International Conference on Application of Concurrency to System Design, ACSD 2013, Barcelona, Spain, 8-10 July, 2013 - [bibtex]
  21. A model-based design flow for CAN-based systems. Alexios Lekidis, Marius Bozga, Didier Mauuary, Saddek Bensalem - Proceedings of the iCC CAN in Automation Conference, Paris, France - [bibtex]
  22. SBIP: A Statistical Model Checking Extension for the BIP Framework. Ayoub Nouri, Axel Legay, Saddek Bensalem, Marius Bozga - Statistical Model Checking Workshop, SMC - [bibtex]
  23. Modeling Mixed Critical Systems in Real-Time BIP. Dario Socci, Petro Poplavko, Saddek Bensalem, Marius Bozga - Proc. ReTiMiCs-2013, Workshop on Real-Time Mixed Criticality Systems - [bibtex]
  24. Time-Triggered Mixed-Critical Scheduler. Dario Socci, Petro Poplavko, Saddek Bensalem, Marius Bozga - 1st International Workshop on Mixed Criticality Systems (WMC) - [bibtex]
  25. Program Repair without Regret. Christian von Essen, Barbara Jobstmann - Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings - [bibtex]
  26. Preface. Barbara Jobstmann, Sandip Ray - Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013 - [bibtex]
  27. The Tree Width of Separation Logic with Recursive Definitions. Radu Iosif, Adam Rogalewicz, Jirí Simácek - Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings - [bibtex]
  28. 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]

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. Implantations distribuées de modèles à base de composants communicants par interactions multiparties avec priorités : application au langage BIP.. Jean Quilbeuf - [bibtex]

2012

Journal Articles

  1. 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]
  2. Achieving distributed control through model checking. Susanne Graf, Doron Peled, Sophie Quinton - Formal Methods in System Design - [bibtex]
  3. 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]
  4. Statistical abstraction and model-checking of large heterogeneous systems. Ananda Basu, Saddek Bensalem, Marius Bozga, Benoît Delahaye, Axel Legay - STTT - [bibtex]
  5. Synthesis of Reactive(1) designs. Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Yaniv Sa'ar - J. Comput. Syst. Sci. - [bibtex]
  6. Finding and fixing faults. Barbara Jobstmann, Stefan Staber, Andreas Griesmayer, Roderick Bloem - J. Comput. Syst. Sci. - [bibtex]
  7. A framework for automated distributed implementation of component-based models. Borzoo Bonakdarpour, Marius Bozga, Mohamad Jaber, Jean Quilbeuf, Joseph Sifakis - Distributed Computing - [bibtex]
  8. 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]
  9. Politiques de gestion de protections pour l'implémentation de sections critiques.. Sifakis Emmanuel, Mounier Laurent - Techniques et Sciences Informatiques - [bibtex]
  10. More testable properties. Ylies Falcone, Jean-Claude Fernandez, Thierry Jéron, Hervé Marchand, Laurent Mounier - STTT - [bibtex]
  11. Generating Invariant-based Certificates for Embedded Systems. Jan-Olaf Blech, Michaël Périn - ACM Transactions on Embedded Computing Systems (TECS) - [bibtex]
  12. Model-based implementation of distributed systems with priorities. Borzoo Bonakdarpour, Marius Bozga, Jean Quilbeuf - Design Automation for Embedded Systems - [bibtex]

Book Chapters (inbook)

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

Conference Articles

  1. 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]
  2. 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]
  3. 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]
  4. 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]
  5. 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]
  6. 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]
  7. 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]
  8. 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]
  9. 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]
  10. Accelerating Interpolants. Hossein Hojjat, Radu Iosif, Filip Kone\vcn\'y, Viktor Kuncak, Philipp Rümmer - ATVA - [bibtex]
  11. 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]
  12. 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]
  13. 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]
  14. 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]
  15. 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]
  16. 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]
  17. 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]
  18. 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]
  19. 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]
  20. A Taint Based Approach for Smart Fuzzing. Sofia Bekrar, Chaouki Bekrar, Roland Groz, Laurent Mounier - Proceedings of SecTest - [bibtex]
  21. Dynamic Information-Flow Analysis for Multi-threaded Applications. Laurent Mounier, Emmanuel Sifakis - Proceedings of ISoLA - [bibtex]
  22. Finding Buffer Overflow Inducing Loops in Binary Executables. Sanjay Rawat, Laurent Mounier - Proceedings of Sixth International Conference on Software Security and Reliability (SERE) - [bibtex]
  23. 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]
  24. System Level Modeling, Analysis and Code Generation: Object Recognition Case Study. Aannda Basu, Saddek Bensalem, Marius Bozga, Julien Mottin, Francois Pacull, Athanasios Poulakidas, Aggelis Aggelis - Proceedings of Embedded World'12 Conference, Nurnberg, Germany - [bibtex]
  25. Knowledge Based Transactional Behavior. Saddek Bensalem, Marius Bozga, Doron Peled, Jean Quilbeuf - Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers - [bibtex]
  26. Modeling and Validation of a Data Process Unit Control for Space Applications. Hai Wan, Chongdi Huang, Yuhui Wang, Fei He, Ming Gu, Rui Chen, Marius Bozga - Proceedings of ERTS'2012 - Embedded Real-Time Software and Systems, Toulouse, France - [bibtex]
  27. 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]

PhD Thesis and HDR

  1. A Formal Framework for Specifying and Analyzing Liabilities Using Log as Digital Evidence. Eduardo Sampaio Elesbao Mazza - [bibtex]
  2. Computer-Aider Security for: Cryptographic Primitives, Voting Protocols and Wireless Sensor Networks. Pascal Lafourcade - Habilitation à diriger des recherches - [bibtex]
  3. Rigorous Implementation of Real-Time Systems. Tesnim Abdellatif - [bibtex]
  4. Tirex : a textual target-level intermediate representation. Artur Pietrek - [bibtex]
  5. Formal Methods For Concrete Security Proofs. Marion Daubignard - [bibtex]
  6. 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. A vision for computer science - the system perspective. Joseph Sifakis - Central Europ. J. Computer Science - [bibtex]
  4. 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]
  5. Automated Proofs for Asymmetric Encryption. Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech - J. Autom. Reasoning - [bibtex]
  6. Building Distributed Controllers for Systems with Priorities. Imene Ben Hafaiedh, Susanne Graf, Sophie Quinton - J. Log. Algebr. Program. - [bibtex]
  7. Priority scheduling of distributed systems based on model checking. Ananda Basu, Saddek Bensalem, Doron Peled, Joseph Sifakis - Formal Methods in System Design - [bibtex]
  8. Formalisms for Specifying Markovian Population Models. Thomas A. Henzinger, Barbara Jobstmann, Verena Wolf - Int. J. Found. Comput. Sci. - [bibtex]
  9. 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]
  10. 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]

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. Information Flow Control of Component-based Distributed Systems. Takoua Abdellatif, Lilia Sfaxi, Riadh Robbana, Yassine Lakhnech - Concurrency and Computation, Practice and Experience - [bibtex]
  3. 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]
  4. A refinement methodology for object-oriented programs. Asma Tafat, Sylvain Boulmé, Claude Marché - Formal Verification of Object-Oriented Software - [bibtex]
  5. Synthesizing Systems with Optimal Average-Case Behavior for Ratio Objectives. Christian von Essen, Barbara Jobstmann - International Workshop on Interactions, Games and Protocols - [bibtex]
  6. 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]
  7. Contract-Based Reasoning for Component Systems with Complex Interactions. Susanne Graf, Roberto Passerone, Sophie Quinton - TIMOBD'11 - [bibtex]
  8. 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]
  9. 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]
  10. 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]
  11. 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]
  12. 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]
  13. On the Generation of Positivstellensatz Witnesses in Degenerate Cases. David Monniaux, Pierre Corbineau - Interactive Theorem Proving (ITP) - PDF - [bibtex]
  14. 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]
  15. 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]
  16. Performance Evaluation of Schedulers in a Probabilistic Setting. Jean-Francois Kempf, Marius Bozga, Oded Maler - FORMATS - [bibtex]
  17. 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]
  18. 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]
  19. 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]
  20. 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]
  21. 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]
  22. 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]
  23. 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]
  24. 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]
  25. 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]
  26. 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]
  27. 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]
  28. 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]
  29. 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]
  30. 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]
  31. 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]
  32. 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]
  33. A Computational Indistinguishability Logic for the Bounded Storage Model. Gilles Barthe, Mathilde Duclos, Yassine Lakhnech - Foundations and Practice of Security - [bibtex]
  34. 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]
  35. 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]
  36. 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]
  37. 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]
  38. Politiques de gestion de protections pour l'implémentation de sections critiques.. Sifakis Emmanuel, Mounier Laurent - Actes des Rencontres du Parallélisme (RenPar) - [bibtex]
  39. 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]
  40. Routage par marche aléatoire à listes tabous. Karine Altisen, Stéphane Devismes, Pascal Lafourcade, Clément Ponsonnet - Algotel - [bibtex]
  41. 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]

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. Modélisation des systèmes synchrones en BIP. Vassiliki Sfyrla - [bibtex]

2010

Journal Articles

  1. Controle de flux d?Information des systemes distribues a base de composants. Takoua Abdellatif, Lilia Sfaxi, Yassine Lakhnech - NOTERE IEEE - [bibtex]
  2. Compositional verification for component-based systems and application. Saddek Bensalem, Marius Bozga, Thanh-Hung Nguyen, Joseph Sifakis - IET Software - [bibtex]
  3. Causal semantics for the algebra of connectors. Simon Bliudze, Joseph Sifakis - Formal Methods in System Design - [bibtex]
  4. 2009 CAV award announcement. Randal E. Bryant, Orna Grumberg, Joseph Sifakis, Moshe Y. Vardi - Formal Methods in System Design - [bibtex]
  5. Source-to-Source Architecture Transformation for Performance Optimization in BIP. Marius Bozga, Mohamad Jaber, Joseph Sifakis - IEEE Trans. Industrial Informatics - [bibtex]
  6. 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]
  7. Automata-based verification of programs with tree updates. Peter Habermehl, Radu Iosif, Tomás Vojnar - Acta Inf. - [bibtex]
  8. Quantitative Separation Logic and Programs with Lists. Marius Bozga, Radu Iosif, Swann Perarnau - J. Autom. Reasoning - [bibtex]

Conference Articles

  1. 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]
  2. 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]
  3. Designing Log Architecture For Legal Evidence. Daniel Le Métayer, Eduardo Mazza, Marie-Laure Potet - Software Engineering And Formal Methods (SEFM) - [bibtex]
  4. 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]
  5. 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]
  6. 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]
  7. 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]
  8. 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]
  9. 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]
  10. Contract-Based Reasoning about Progress: Application to Resource Sharing in a Network. Imene Ben-Hafaiedh, Susanne Graf, Sophie Quinton - Proc. of FLACOS'10 - [bibtex]
  11. 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]
  12. 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]
  13. 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]
  14. Computational indistinguishability logic. Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech - ACM Conference on Computer and Communications Security - [bibtex]
  15. 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]
  16. Proof Trick: Small Inversions. Jean-François Monin - Second Coq Workshop - [bibtex]
  17. 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]
  18. 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]
  19. Knowledge Based Scheduling of Distributed Systems. Saddek Bensalem, Doron Peled, Joseph Sifakis - Time for Verification, Essays in Memory of Amir Pnueli - [bibtex]
  20. 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]
  21. 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]
  22. 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]
  23. Component-based Construction of Heterogeneous Real-time Systems in BIP. Joseph Sifakis - The Future of Software Engineering - [bibtex]
  24. 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]
  25. 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]
  26. 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]
  27. 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]
  28. 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]
  29. 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]
  30. 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]
  31. 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]
  32. 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]
  33. Verification of an AFDX Infrastructure Using Simulations and Probabilities. Ananda Basu, Saddek Bensalem, Marius Bozga, Benoît Delahaye, Axel Legay, Emmanuel Sifakis - Runtime Verification - First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings - [bibtex]
  34. Robustness with Respect to Error Specifications. Barbara Jobstmann - Proceedings of the 2010 Forum on specification & Design Languages, FDL 2010, September 14-16, 2010, Southampton, UK - [bibtex]
  35. Message from the chairs. Klaus Schneider, Barbara Jobstmann, Luca P. Carloni, Jens Brandt - 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), Grenoble, France, 26-28 July 2010 - [bibtex]

PhD Thesis and HDR

  1. Constructive Verification for Component-based Systems. Thanh-Hung Nguyen - [bibtex]
  2. Automatisation de la Certification Formelle de Systèmes Critiques par Instrumentation d'Interpréteurs Abstraits. Manuel Garnacho - [bibtex]
  3. Implémentations Centralisée et Répartie de Systèmes Corrects par construction \'a base des Composants par Transformations Source-\'a-source dans BIP. Mohamad Jaber - [bibtex]
  4. Component-Based Design of Real-Time Systems (HDR). Marius Bozga - [bibtex]
  5. Modélisation des systèmes temps-réel embarqués en utilisant AADL pour la génération automatique d'applications formellement vérifiées. Mohamad Chkouri - [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. 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]
  3. Model checking: algorithmic verification and debugging. Edmund M. Clarke, Allen Emerson, Joseph Sifakis - Commun. ACM - [bibtex]
  4. Flat Parametric Counter Automata. Marius Bozga, Radu Iosif, Yassine Lakhnech - Fundam. Inform. - [bibtex]
  5. Convincing Proofs for Program Certification. Manuel Garnacho, Michaël Périn - Electronic Notes in Theoretical Computer Science - [bibtex]
  6. Les résultats du projet OpenEmbeDD. Charles Andre, Mariano Belaunde, Bernard Berthomieu, Christian Brunette, Agusti Canals, Hubert Garavel, Susanne Graf, Frederic Lang, Vincent Mahe, Michel Nakhle, others - Génie logiciel - [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]

Conference Articles

  1. Prototyping of Distributed Embedded Systems Using AADL. Mohamed Yassin Chkouri, Marius Bozga - Model Based Architecting and Construction of Embedded Systems ACES-MB - [bibtex]
  2. 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]
  3. 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]
  4. Using Checker Predicates in Certifying Code Generation. Jan Olaf Blech, Benjamin Grégoire - Workshop on Compiler Optimization meets Compiler Verification (COCV) - [bibtex]
  5. Invariants and Robustness of BIP Models. Jan Olaf Blech, Thanh-Hung Nguyen, Michaël Périn - Workshop on Invariant Generation (WING) - [bibtex]
  6. Certifying Deadlock-freedom for BIP Models. Jan Olaf Blech, Michaël Périn - Software and Compilers for Embedded Systems (SCOPES) - [bibtex]
  7. Comparing State Spaces in Automatic Protocol Analysis. Cas J. F. Cremers, Pascal Lafourcade, Philippe Nadeau - Formal to Practical Security - [bibtex]
  8. Runtime Verification of Safety Progress Properties. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier - Runtime Verification 2009 - [bibtex]
  9. 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]
  10. Automated Proofs for Encryption Modes. Martin Gagne, Pascal Lafourcade, Yassine Lakhnech, Reihaneh Safavi - Workshop on Formal and Computational Cryptography, (FCC'09) - [bibtex]
  11. Deterministic data flow communication in AADL. Mohamed Yassin Chkouri, Marius Bozga - ICESS '09: Proceedings of the 2009 International Conference on Embedded Software and Systems - [bibtex]
  12. 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]
  13. Prudent engineering practices to prevent type-flaw attacks under algebraic properties. Sreekanth Malladi, Pascal Lafourcade - Workshop on Security and Rewriting Techniques, (SecReT'09) - [bibtex]
  14. 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]
  15. From Orchestration to Choreography: Memoryless and Distributed Orchestrators. Sophie Quinton, Imene Ben-Hafaiedh, Susanne Graf - Proc. of FLACOS'09 - [bibtex]
  16. 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]
  17. 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]
  18. 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]
  19. 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]
  20. 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]
  21. 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]
  22. 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]
  23. 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]
  24. 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]
  25. 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]
  26. Compositional Timing Analysis. Ramzi Ben Salah, Marius Bozga, Oded Maler - EMSOFT - [bibtex]
  27. 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]
  28. 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]
  29. "Certfication of Smart-Card Applications in Common Criteria: Proving Representation Correspondences". Iman Narasamdya, Michaël Périn - Fundamental Approaches to Software Engineering - [bibtex]
  30. "Certfication of Smart-Card Applications in Common Criteria". Iman Narasamdya, Michaël Périn - ACM Symposium on Applied Computing - [bibtex]
  31. 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]
  32. 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]
  33. 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]
  34. Instantaneous Soundness Checking of Industrial Business Process Models. Dirk Fahland, Cédric Favre, Barbara Jobstmann, Jana Koehler, Niels Lohmann, Hagen Völzer, Karsten Wolf - Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009. Proceedings - [bibtex]
  35. Better Quality in Synthesis through Quantitative Objectives. Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann - Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings - [bibtex]
  36. Formalisms for Specifying Markovian Population Models. Thomas A. Henzinger, Barbara Jobstmann, Verena Wolf - Reachability Problems, 3rd International Workshop, RP 2009, Palaiseau, France, September 23-25, 2009. Proceedings - [bibtex]

PhD Thesis and HDR

  1. Study and Implementation of Runtime Validation Techniques. Ylies Falcone - [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. OMEGA -- Correct development of Real Time Embedded Systems. Susanne Graf - SoSyM, int. Journal on Software & Systems Modelling - [bibtex]
  3. 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]
  4. Symbolic quality control for multimedia applications. Jacques Combaz, Jean-Claude Fernandez, Joseph Sifakis, Loïc Strus - Real-Time Systems - [bibtex]
  5. The Algebra of Connectors - Structuring Interaction in BIP. Simon Bliudze, Joseph Sifakis - IEEE Trans. Computers - [bibtex]

Book Chapters

  1. 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. 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]
  4. 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]
  5. 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]
  6. A Model Transformation Tool for Performance Simulation of Complex UML Models. Olivier Constant, Wei Monin, Susanne Graf - ICSE 2008, tool track - [bibtex]
  7. 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]
  8. 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]
  9. Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier - International Conference of Information System Security - [bibtex]
  10. 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]
  11. 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]
  12. 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]
  13. 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]
  14. 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]
  15. 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]
  16. 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]
  17. 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]
  18. 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]
  19. 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]
  20. Specification and Verification of Conurrent Systems in Cesar. Jean-Pierre Queille, Joseph Sifakis - 25 Years of Model Checking - History, Achievements, Perspectives - [bibtex]
  21. 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]
  22. 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]
  23. 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]
  24. 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]
  25. A New Elimination Rule for the Calculus of Inductive Constructions. Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini - Types for Proofs and Programs (International Conference TYPES 2008, Revised Selected Papers) - [bibtex]
  26. Environment Assumptions for Synthesis. Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann - CONCUR 2008 - Concurrency Theory, 19th International Conference, CONCUR 2008, Toronto, Canada, August 19-22, 2008. Proceedings - [bibtex]
  27. Interface theories with component reuse. Laurent Doyen, Thomas A. Henzinger, Barbara Jobstmann, Tatjana Petrov - Proceedings of the 8th ACM & IEEE International conference on Embedded software, EMSOFT 2008, Atlanta, GA, USA, October 19-24, 2008 - [bibtex]
  28. Open Implication. Karin Greimel, Roderick Bloem, Barbara Jobstmann, Moshe Y. Vardi - Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II - Track B: Logic, Semantics, and Theory of Programming & - [bibtex]
  29. Model checking transactional memories. Rachid Guerraoui, Thomas A. Henzinger, Barbara Jobstmann, Vasu Singh - Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008 - [bibtex]

PhD Thesis and HDR

  1. Component-based modeling of heterogeneous real time systems in BIP. Ananda Basu - [bibtex]
  2. Models and Methods for the Construction and Verification of Complex Reactive Systems. Susanne Graf - Habilitation à diriger des recherches - [bibtex]
  3. Modélisations et analyses de réseaux de capteurs. Ludovic Samper - [bibtex]
  4. Contrôle de qualité de service optimal d'application multimédia. Loïc Strus - [bibtex]
  5. Le débogage de code optimisé dans le contexte des systèmes embarqués. Hugo Venturini - [bibtex]

2007

Journal Articles

  1. Software and architecture modelling with Omega-UML and validation with IF. Susanne Graf, Iulian Ober - Génie Logiciel - [bibtex]
  2. Intruder Deduction for the Equational Theory of Abelian Groups with Distributive Encryption. Pascal Lafourcade, Denis Lugiez, Ralf Treinen - Information and Computation - [bibtex]
  3. Time in Abstract State Machines. Susanne Graf, Andreas Prinz - Fundamentae Informaticae, Special issue on ASM 2005 - [bibtex]
  4. The Discipline of Embedded Systems Design. Thomas A. Henzinger, Joseph Sifakis - IEEE Computer - [bibtex]
  5. Specify, Compile, Run: Hardware from PSL. Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer - Electr. Notes Theor. Comput. Sci. - [bibtex]

Conference Articles

  1. 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]
  2. 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]
  3. 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]
  4. 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]
  5. A Compositional Testing Framework Driven by Partial Specifications. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier, Jean-Luc Richier - TESTCOM/FATES - [bibtex]
  6. Contracts for BIP: hierarchical interaction models for compositional verification. Susanne Graf, Sophie Quinton - FORTE 2007, Talinn - [bibtex]
  7. Test Generation from Security Policies Specified in Or-BAC. Keqin Li, Laurent Mounier, Roland Groz - IEEE COMPSAC'07 - [bibtex]
  8. 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]
  9. 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]
  10. 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]
  11. 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]
  12. 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]
  13. Intuitionistic Refinement Calculus.. Sylvain Boulmé - Typed Lambda Calculi and Applications - PDF - [bibtex]
  14. 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]
  15. 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]
  16. 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]
  17. 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]
  18. 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]
  19. 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]
  20. Anzu: A Tool for Property Synthesis. Barbara Jobstmann, Stefan J. Galler, Martin Weiglhofer, Roderick Bloem - Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings - [bibtex]
  21. Interactive presentation: Automatic hardware synthesis from specifications: a case study. Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer - 2007 Design, Automation and Test in Europe Conference and Exposition (DATE 2007), April 16-20, 2007, Nice, France - [bibtex]

PhD Thesis and HDR

  1. Model Based Testing for Real-Time Systems. Moez Krichen - [bibtex]
  2. On Timing Analysis of Large Systems. Ramzi Ben Salah - [bibtex]

2006

Journal Articles

  1. 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]
  2. 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]
  3. A real-time profile for UML. Susanne Graf, Ileana Ober, Iulian Ober - STTT, Software Tools for Technology Transfer - [bibtex]
  4. Validating Timed UML models by simulation and verification. Susanne Graf, Ileana Ober, Iulian Ober - STTT, Software Tools for Technology Transfer - [bibtex]
  5. 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]

Conference Articles

  1. Qualification d'architectures fontionnelles. Marius Bozga, Pierre Combes, Susanne Graf, Wei Monin, Nicolas Moteau - Notere'06 - [bibtex]
  2. Test Generation for Network Security Rules. Vianney Darmaillacq, Jean-Claude Fernandez, Roland Groz, Laurent Mounier, Jean-Luc Richier - TestCom'06 - [bibtex]
  3. A Test Calculus Framework Applied to Network Security Policies. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier, Jean-Luc Richier - FATES/RV'06 - [bibtex]
  4. 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]
  5. 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]
  6. 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 - [bibtex]
  7. 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]
  8. 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]
  9. 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]
  10. 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]
  11. 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]
  12. 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]
  13. 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]
  14. 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]
  15. 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]
  16. 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]
  17. 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]
  18. 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]
  19. 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]
  20. Optimizations for LTL Synthesis. Barbara Jobstmann, Roderick Bloem - Formal Methods in Computer-Aided Design, 6th International Conference, FMCAD 2006, San Jose, California, USA, November 12-16, 2006, Proceedings - [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. 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]
  4. Translating Java for Multiple Model Checkers: The Bandera Back-End. Radu Iosif, Matthew B. Dwyer, John Hatcliff - Formal Methods in System Design - [bibtex]
  5. 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]

Conference Articles

  1. 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]
  2. 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]
  3. 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]
  4. 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]
  5. A model-based approach for robustness testing. Jean-Claude Fernandez, Laurent Mounier, Cyril Pachon - TestCom 2005 - [bibtex]
  6. 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]
  7. 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]
  8. 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]
  9. 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]
  10. 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]
  11. 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]
  12. Program Repair as a Game. Barbara Jobstmann, Andreas Griesmayer, Roderick Bloem - Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings - [bibtex]
  13. Finding and Fixing Faults. Stefan Staber, Barbara Jobstmann, Roderick Bloem - Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005, Proceedings - [bibtex]

PhD Thesis and HDR

  1. Approche Fondée sur les Modèles pour Java Temps-Réel. Chaker Nakhli - [bibtex]
  2. Une approche basée sur les modèles pour le test de robustesse. Cyril Pachon - [bibtex]

2004

Journal Articles

  1. Symmetry reductions for model checking of concurrent dynamic software. Radu Iosif - STTT - [bibtex]

Conference Articles

  1. 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]
  2. 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]
  3. IF Tutorial. Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober - 9th SPIN'04 Workshop on Model-Checking of Software, Barcelona, Spain - [bibtex]
  4. 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]
  5. 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]
  6. A Framework for Time in FDTs. Susanne Graf, Andreas Prinz - FORTE 2004, participants proceedings - [bibtex]
  7. 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]
  8. 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]
  9. 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]
  10. 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]
  11. 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]

2003

Journal Articles

  1. Tools and Algorithms for the Construction and Analysis of Systems: An STTT special section. Susanne Graf - STTT, Software Tools for Technology Transfer - [bibtex]
  2. Temporal logic properties of Java objects. Radu Iosif, Riccardo Sisto - Journal of Systems and Software - [bibtex]

Conference Articles

  1. Abstract Interpretation for Secrecy using Patterns. Liana Bozga, Yassine Lakhnech, Michaël Périn - TACAS'03 - [bibtex]
  2. 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]
  3. 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]
  4. 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]
  5. Property Oriented Test Case Generation. Jean-Claude Fernandez, Laurent Mounier, Cyril Pachon - Proceedings of FATES'03 (Satellite workshop of ASE'03), Montreal, Canada - [bibtex]
  6. 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]
  7. 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]
  8. 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]
  9. 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]
  10. 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]
  11. 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. 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]

Conference Articles

  1. Expression of time and duration constraints in SDL. Susanne Graf - 3rd SAM Workshop on SDL and MSC, University of Wales Aberystwyth - [bibtex]
  2. 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]
  3. 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]
  4. 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]

2001

Journal Articles

  1. Verification of Parameterized Protocols. Kai Baukus, Yassine Lakhnech, Karsten Stahl - Journal of Universal Computer Science - [bibtex]
  2. Verifying Untimed and Timed Aspects of the Experimental Batch Plant. Ralf Huuck, Ben Lukoschus, Yassine Lakhnech - European Journal of Control - [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. 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]
  6. Iterating Transducers. Dennis Dams, Yassine Lakhnech, Martin Steffen - Computer Aided Verification'01 - [bibtex]
  7. 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]
  8. 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]
  9. 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]
  10. 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]
  11. 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. 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]

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. Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems. Jean-Pierre Krimm, Laurent Mounier - Proceedings of TACAS'00 - [bibtex]
  10. 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]
  11. 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]
  12. 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]
  13. 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]
  14. 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. Applications des ordres partiels à la génération compositionelle de systèmes asynchrones. Jean-Pierre Krimm - Thèse de doctorat - [bibtex]

1999

Journal Articles

  1. Automatic Generation of Invariants. Saddek Bensalem, Yassine Lakhnech - Formal Methods in System Design - [bibtex]
  2. Characterization of a sequentially consistent memory and verification of a cache memory by abstraction. Susanne Graf - Distributed Computing - [bibtex]
  3. 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. State Space Reduction Based on Live Variables Analysis. Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu - SAS - [bibtex]
  3. 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]
  4. 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]
  5. 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]
  6. 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]
  7. 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]
  8. 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]

1998

Journal Articles

  1. On Complexity of Reachability of Transition Restricted Petri Nets. Cristian Ene - Sci. Ann. Cuza Univ. - [bibtex]
  2. 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. Computing Abstractions of Infinite State Systems Automatically and Compositionally. Saddek Bensalem, Yassine Lakhnech, Sam Owre - Computer Aided Verification - [bibtex]
  2. InVeSt : A Tool for the Verification of Invariants. Saddek Bensalem, Yassine Lakhnech, Sam Owre - Computer Aided Verification - [bibtex]
  3. Verifying Statecharts with Spin. Gerard J. Holzmann, Erich Mikk, Yassine Lakhnech, Michael Siegel - Proc. Workshop on Industrial-strength Formal specification Techniques - [bibtex]
  4. On the Composition of Condition/Event Systems. Stefan Kowalewski, Yassine Lakhnech, Ben Lukoschus, Luis Urbina - WODES'98 - [bibtex]
  5. 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]
  6. 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. Vérification des propriétés temporelles des programmes parallèles. Radu Mateescu - [bibtex]
  2. Sur la Vérification de Systèmes Infinis. Peter Habermehl - [bibtex]
  3. Combinaison de Méthodes Déductives et Arithméthiques pour la Vérification. Hassen Saidi - [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]

Conference Articles

  1. 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]
  2. Comparing Timed Condition/Event Systems and Timed Automata. Ralf Huuck, Yassine Lakhnech, Luis Urbina, Sebastian Engell, Stefan Kowalewski, Jorg Preußig - HART'97 - [bibtex]
  3. 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]
  4. 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]
  5. Temporal Logic for Stabilizing Systems. Yassine Lakhnech, Michael Siegel - Second International Conference on Temporal Logic - ICTL'97 - [bibtex]
  6. 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]
  7. Towards Efficient Modelchecking Statecharts: A Statecharts to Promela Complier. Yassine Lakhnech, Erich Mikk, Michael Siegel - 3rd International SPIN Workshop - [bibtex]
  8. Towards Efficient Modelchecking Statecharts. Erich Mikk, Yassine Lakhnech, Michael Siegel - STATEMATE Anwenderforum 97 - [bibtex]
  9. 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]
  10. Hierarchical automata as model for statecharts. Yassine Lakhnech, Erich Mikk, Michael Siegel - Proc. of the Asian Computing Science Conference (ASIAN'97) - [bibtex]
  11. Construction of abstract state graphs with PVS. Susanne Graf, Hassen Saidi - Conference on Computer Aided Verification CAV'97, Haifa - [bibtex]
  12. Deductive verification of stabilizing systems. Yassine Lakhnech, Michael Siegel - 3rd Workshop on Self-stabilizing Systems, Santa Barbara, California, August, 1997, Proceedings - [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. Powerful Techniques for the Automatic Generation of Invariants. Saddek Bensalem, Yassine Lakhnech, Hassen Saidi - 8th International Conference on Computer Aided Verification - [bibtex]
  2. 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]
  3. 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]
  4. 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]
  5. 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]
  6. Verifying invariants using theorem proving. Susanne Graf, Hassen Saidi - Conference on Computer Aided Verification CAV'96 - [bibtex]
  7. Translating Statecharts to Promela/SPIN. Erich Mikk, Yassine Lakhnech, Michael Siegel - Dagstuhl-Seminar ``Synchronous Languages'' - [bibtex]
  8. 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]
  9. 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. Temporal logic + timed automata : expressiveness and decidability. Ahmed Bouajjani, Yassine Lakhnech - CONCUR'95: Concurrency Theory - [bibtex]
  2. From duration calculus to linear hybrid automata. Ahmed Bouajjani, Yassine Lakhnech, Riadh Robbana - Computer Aided Verification - [bibtex]
  3. 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]
  4. Hierarchies of Petri Net Languages and a Super-Normal Form. Ferucio Laurentiu Tiplea, Cristian Ene - Developments in Language Theory - [bibtex]
  5. 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]
  6. 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]

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]

Conference Articles

  1. 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]
  2. Verification of a distributed Cache memory by using abstractions. Susanne Graf - Conference on Computer Aided Verification CAV'94, Stanford - [bibtex]
  3. 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. Méthodes symboliques pour la vérification de Processus Communicants : étude et mise en oeuvre. Alain Kerbrat - [bibtex]
  2. Vérification symbolique de programmes réactifs à l'aide d'abstractions. Claire Loiseaux - [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. 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]
  2. Symbolic Equivalence Checking. Jean-Claude Fernandez, Alain Kerbrat, Laurent Mounier - Proceedings of the 5th Workshop on Computer-Aided Verification (Heraklion, Greece) - [bibtex]
  3. Program Verification using compositional Abstraction. Susanne Graf, Claire Loiseaux - TAPSOFT 93, joint conference CAAP/FASE - [bibtex]
  4. A tool for symbolic program verification and abstraction. Susanne Graf, Claire Loiseaux - Conference on Computer Aided Verification CAV 93, Heraklion Crete - [bibtex]
  5. A tool implementing a method for symbolic program verification. Susanne Graf, Claire Loiseaux - Proceedings of "Formale Methoden zum Entwurf korrekter Systeme", Bad Herrenalb - [bibtex]

1992

Journal Articles

  1. Minimal State Graph Generation. Ahmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs, Pascal Raymond - Sci. Comput. Program. - [bibtex]
  2. On-the-Fly Verification of Finite Transition Systems. Jean-Claude Fernandez, Laurent Mounier, Claude Jard, Thierry Jéron - Formal Methods in System Design - [bibtex]

Conference Articles

  1. 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]
  2. 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. Méthodes de Vérification de Spécifications Comportementales : étude et mise en oeuvre. Laurent Mounier - [bibtex]

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

Logged in visitors: 20 ; visits: 452002