by years

• Synchrone by years ; by kinds
• Tempo by years ; by kinds
• Pacss by years ; by kinds
• RSD by years ; by kinds
• Verimag by years ; by kinds

2019

Journal Articles

1. Gradual stabilization. Karine Altisen, Stéphane Devismes, Anaïs Durand, Franck Petit - J. Parallel Distrib. Comput. - [bibtex]
2. A silent self-stabilizing algorithm for the generalized minimal \emphk-dominating set problem. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore - Theor. Comput. Sci. - [bibtex]

Conference Articles

3. Silent Self-Stabilizing Scheme for Spanning-Tree-like Constructions. Stéphane Devismes, David Ilcinkas, Colette Johnen - 20th International Conference on Distributed Computing and Networking (ICDCN 2019) - [bibtex]

2018

Journal Articles

4. Optimal Torus Exploration by Oblivious Robots. Stéphane Devismes, Anissa Lamani, Franck Petit, Sébastien Tixeuil - Computing - [bibtex]
5. Global and Local Deadlock Freedom in BIP. Paul C. Attie, Saddek Bensalem, Marius Bozga, Mohamad Jaber, Joseph Sifakis, Fadi A. Zaraket - ACM Trans. Softw. Eng. Methodol. - [bibtex]
6. DOL-BIP-Critical: a tool chain for rigorous design and implementation of mixed-criticality multi-core systems. Georgia Giannopoulou, Peter Poplavko, Dario Socci, Pengcheng Huang, Nikolay Stoimenov, Paraskevas Bourgos, Lothar Thiele, Marius Bozga, Saddek Bensalem, Sylvain Girbal, Madeleine Faugère, Romain Soulat, Beno\^ Dupont de Dinechin - Design Autom. for Emb. Sys. - [bibtex]
7. Model-based design of IoT systems with the BIP component framework. Alexios Lekidis, Emmanouela Stachtiari, Panagiotis Katsaros, Marius Bozga, Christos K. Georgiadis - Softw., Pract. Exper. - [bibtex]
8. Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra. Sylvain Boulmé, Alexandre Maréchal - Journal of Automated Reasoning - [bibtex]
9. Maximal software execution time: a regression-based approach. Ayoub Nouri, Peter Poplavko, Lefteris Angelis, Alexandros Zerzelidis, Saddek Bensalem, Panagiotis Katsaros - ISSE - [bibtex]
10. TT-BIP: using correct-by-design BIP approach for modelling real-time system with time-triggered paradigm. Hela Guesmi, Belgacem Ben Hedia, Simon Bliudze, Saddek Bensalem, Briag Le Nabec - ISSE - [bibtex]
11. Improving the results of program analysis by abstract interpretation beyond the decreasing sequence. Remy Boutonnet, Nicolas Halbwachs - Formal Methods in System Design - [bibtex]

Book Chapters

12. Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications. Ezio Bartocci, Jyotirmoy V. Deshmukh, Alexandre Donzé, Georgios E. Fainekos, Oded Maler, Dejan Nickovic, Sriram Sankaranarayanan - Lectures on Runtime Verification - Introductory and Advanced Topics - [bibtex]

Conference Articles

13. Parallel Code Generation of Synchronous Programs for a Many-core Architecture. Amaury Graillat, Matthieu Moy, Pascal Raymond, Benoît Dupont De Dinechin - Design, Automation and Test in Europe - [bibtex]
14. Real-time on-Board Manycore Implementation of a Health Monitoring System: Lessons Learnt. Moustapha Lo, Nicolas Valot, Florence Maraninchi, Pascal Raymond - 9th European Congress Embedded Real Time Software and Systems (ERTS2 2018) - [bibtex]
15. L-Exclusion autostabilisante revisitée. Fabienne Carrier, Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore - ALGOTEL 2018 - 20èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications - [bibtex]
16. Schéma général auto-stabilisant et silencieux de constructions de type arbres couvrants. Stéphane Devismes, David Ilcinkas, Colette Johnen - ALGOTEL 2018 - 20èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications - [bibtex]
17. Stabilisation progressive. Karine Altisen, Stéphane Devismes, Anaïs Durand, Franck Petit - ALGOTEL 2018 - 20èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications - [bibtex]
18. Eviter les collisions dans les réseaux 6TiSCH. Ali Fahs, Rodolphe Bertolini, Olivier Alphand, Franck Rousseau, Karine Altisen, Stéphane Devismes - CoRes - Rencontres Francophones sur la Conception de Protocoles, lévaluation de Performance et l'Expérimentation des Réseaux de Communication - [bibtex]
19. Efficient Parametric Identification for STL. Alexey Bakhirkin, Thomas Ferrére, Oded Maler - Hybrid Systems: Computation and Control (HSCC) - [bibtex]
20. Specifying Timed Patterns using Temporal Logic. Dogan Ulus, Oded Maler - Hybrid Systems: Computation and Control (HSCC) - [bibtex]
21. AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic. Dejan Nickovic, Olivier Lebeltel, Oded Maler, Thomas Ferrére, Dogan Ulus - Tools and Algorithms for the Construction and Analysis (TACAS) - [bibtex]
22. Binary Deobfuscation and Dynamic Symbolic Execution. Jonthan Salwan, Sebastien Bardin, Marie-Laure Potet - DIMVA'18, 15th Conference on Detection of Intrusions and Malware & Vulnerability Assessment - [bibtex]
23. Model Generation for Quantified Formulas: A Taint-Based Approach. Benjamin Farinier, Sebastien Bardin, Richard Bonichon, Marie-Laure Potet - CAV'18, 30th International Conference on Computer Aided Verification - [bibtex]
24. A Model-based Approach to Certification of Adaptive MILS. Dorien Koelemeijer, Rasma Araby, Ayoub Nouri, Marius Bozga, Rance DeLong - International Workshop on MILS: Architecture and Assurance for Secure Systems, MILS@HiPEAC 2018, Luxembourg, June 25, 2018. - [bibtex]
25. Distance on Timed Words and Applications. Eugene Asarin, Nicolas Basset, Aldric Degorre - Formal Modeling and Analysis of Timed Systems - 16th International Conference, FORMATS 2018, Beijing, China, September 4-6, 2018, Proceedings - [bibtex]
26. A Generalized Digraph Model for Expressing Dependencies. Pascal Fradet, Xiaojie Guo, Jean-François Monin, Sophie Quinton - 26th International Conference on Real-Time Networks and Systems (RTNS '18) - [bibtex]
27. \emphS BIP 2.0: Statistical Model Checking Stochastic Real-Time Systems. Braham Lotfi Mediouni, Ayoub Nouri, Marius Bozga, Mahieddine Dellabani, Axel Legay, Saddek Bensalem - Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings - [bibtex]
28. Programming Dynamic Reconfigurable Systems. Rim El Ballouli, Saddek Bensalem, Marius Bozga, Joseph Sifakis - Formal Aspects of Component Software - 15th International Conference, FACS 2018, Pohang, South Korea, October 10-12, 2018, Proceedings - [bibtex]
29. Four Exercises in Programming Dynamic Reconfigurable Systems: Methodology and Solution in DR-BIP. Rim El Ballouli, Saddek Bensalem, Marius Bozga, Joseph Sifakis - Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III - [bibtex]
30. Designing Systems with Detection and Reconfiguration Capabilities: A Formal Approach. Iulia Dragomir, Simon Iosti, Marius Bozga, Saddek Bensalem - Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III - [bibtex]
31. Mitigating Security Risks Through Attack Strategies Exploration. Braham Lotfi Mediouni, Ayoub Nouri, Marius Bozga, Axel Legay, Saddek Bensalem - Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part II - [bibtex]
32. A Process Network Model for Reactive Streaming Software with Deterministic Task Parallelism. Fotios Gioulekas, Peter Poplavko, Panagiotis Katsaros, Saddek Bensalem, Pedro Palomo - Fundamental Approaches to Software Engineering, 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessalonik - [bibtex]
33. Left-Eigenvectors Are Certificates of the Orbit Problem. Steven de Oliveira, Virgile Prevosto, Peter Habermehl, Saddek Bensalem - Reachability Problems - 12th International Conference, RP 2018, Marseille, France, September 24-26, 2018, Proceedings - [bibtex]
34. Algorithmic Complexity of Correctness Testing in MC-Scheduling. Rany Kahil, Dario Socci, Peter Poplavko, Saddek Bensalem - Proceedings of the 26th International Conference on Real-Time Networks and Systems, RTNS 2018, Chasseneuil-du-Poitou, France, October 10-12, 2018 - [bibtex]
35. Acyclic Strategy for Silent Self-stabilization in Spanning Forests. Karine Altisen, Stéphane Devismes, Anaïs Durand - Stabilization, Safety, and Security of Distributed Systems - 20th International Symposium, SSS 2018, Tokyo, Japan, November 4-7, 2018, Proceedings - [bibtex]
36. Building Correct Cyber-Physical Systems: Why We Need a Multiview Contract Theory. Susanne Graf, Sophie Quinton, Alain Girault, Gregor Gößler - Formal Methods for Industrial Critical Systems - 23rd International Conference, FMICS 2018, Maynooth, Ireland, September 3-4, 2018, Proceedings - [bibtex]
37. A Coq Tactic for Equality Learning in Linear Arithmetic. Sylvain Boulmé, Alexandre Maréchal - Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings - [bibtex]

PhD Thesis and HDR

38. Formal Methods for Distributed Real-Time Systems. Mahieddine Dellabani - [bibtex]
39. Finding constancy in linear routines. Steven De Oliveira - [bibtex]

2017

Journal Articles

40. Self-stabilizing silent disjunction in an anonymous network. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore - Theor. Comput. Sci. - [bibtex]
41. Concurrency in snap-stabilizing local resource allocation. Karine Altisen, Stéphane Devismes, Anaïs Durand - J. Parallel Distrib. Comput. - [bibtex]
42. Self-Stabilizing Leader Election in Polynomial Steps. Karine Altisen, Alain Cournier, Stéphane Devismes, Anaïs Durand, Franck Petit - Information and Computation - [bibtex]
43. Self-Stabilizing Weak Leader Election in Anonymous Trees Using Constant Memory per Edge. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore, Vincent Villain - Parallel Processing Letters - [bibtex]
44. On probabilistic snap-stabilization. Karine Altisen, Stéphane Devismes - Theoretical Computer Science - [bibtex]
45. Online and offline scheduling with cache-related preemption delays. Guillaume Phavorin, Pascal Richard, Joël Goossens, Claire Maiza, Laurent George, Thomas Chapeaux - Real-Time Systems - [bibtex]
46. An extensible framework for multicore response time analysis. Robert I. Davis, Sebastian Altmeyer, Leandro Indrusiak, Claire Maiza, Vincent Nelis, Jan Reineke - Real-Time Systems - [bibtex]
47. SR3: secure resilient reputation-based routing. Karine Altisen, Stéphane Devismes, Raphaël Jamet, Pascal Lafourcade - Wireless Networks - [bibtex]
48. Reachability computation for polynomial dynamical systems. Tommaso Dreossi, Thao Dang, Carla Piazza - Formal Methods in System Design - [bibtex]
49. Certified Roundoff Error Bounds Using Semidefinite Programming. Victor Magron, George A. Constantinides, Alastair F. Donaldson - ACM Trans. Math. Softw. - [bibtex]
50. Self-Stabilizing Disconnected Components Detection and Rooted Shortest-Path Tree Maintenance in Polynomial Steps. Stéphane Devismes, David Ilcinkas, Colette Johnen - Discrete Mathematics & Theoretical Computer Science - [bibtex]
51. A Framework for Certified Self-Stabilization. Karine Altisen, Pierre Corbineau, Stéphane Devismes - Logical Methods in Computer Science (special issue of FORTE 2016) - [bibtex]
52. Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation. Hosein Nazarpour, Ylies Falcone, Saddek Bensalem, Marius Bozga - Formal Asp. Comput. - [bibtex]

Book Chapters

53. SimSoC: A Fast, Proven Faithful, Full System Virtual Prototyping Framework. Vania Joloboff, Jean-François Monin, Xiaomu Shi - Model-Implementation Fidelity in Cyber Physical System Design - [bibtex]

Conference Articles

54. Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic. Andrew Reynolds, Radu Iosif, Cristina Serban - Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings - [bibtex]
55. scat: Learning from a Single Execution of a Binary. Franck de Goer, Christopher Ferreira, Laurent Mounier - Proceedings of SANER 2017 - [bibtex]
56. Modeling the Wind Turbine Benchmark with PWA Hybrid Automata. Nikolaos Kekatos, Marcelo Forets, Goran Frehse - ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems - [bibtex]
57. Leader Election in Asymmetric Labeled Unidirectional Rings. Karine Altisen, Ajoy Kumar Datta, Stéphane Devismes, Anaïs Durand, Lawrence L. Larmore - 2017 IEEE International Parallel and Distributed Processing Symposium, IPDPS 2017, Orlando, FL, USA, May 29 - June 2, 2017 - [bibtex]
58. Metrics for runtime detection of allocators in binaries. Franck de Goer, Roland Groz, Laurent Mounier - 10th USENIX Workshop on Cyber Security Experimentation and Test, CSET - [bibtex]
59. Certified Roundoff Error Bounds Using Bernstein Expansions and Sparse Krivine-Stengle Representations. Alexandre Rocca, Victor Magron, Thao Dang - 24th IEEE Symposium on Computer Arithmetic, ARITH 2017, London, United Kingdom, July 24-26, 2017 - [bibtex]
60. Derivatives of Quantitative Regular Expressions. Rajeev Alur, Konstantinos Mamouras, Dogan Ulus - Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday - [bibtex]
61. Classification and Coverage-Based Falsification for Embedded Control Systems. Arvind S. Adimoolam, Thao Dang, Alexandre Donzé, James Patrick Kapinski, Xiaoqing Jin - Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I - [bibtex]
62. Montre: A Tool for Monitoring Timed Regular Expressions. Dogan Ulus - Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I - [bibtex]
63. Combining the Temporal and Epistemic Dimensions for MTL Monitoring. Eugene Asarin, Oded Maler, Dejan Nickovic, Dogan Ulus - Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, Berlin, Germany, September 5-7, 2017, Proceedings - [bibtex]
64. On the Quantitative Semantics of Regular Expressions over Real-Valued Signals. Alexey Bakhirkin, Thomas Ferrére, Oded Maler, Dogan Ulus - Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, Berlin, Germany, September 5-7, 2017, Proceedings - [bibtex]
65. Template complex zonotopes for stability and invariant verification. Arvind S. Adimoolam, Thao Dang - 2017 American Control Conference, ACC 2017, Seattle, WA, USA, May 24-26, 2017 - [bibtex]
66. A Generic Algorithm for Learning Symbolic Automata from Membership Queries. Oded Maler, Irini-Eleftheria Mens - Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday - [bibtex]
67. ARCH-COMP17 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics. Matthias Althoff, Stanley Bak, Dario Cattaruzza, Xin Chen, Goran Frehse, Rajarshi Ray, Stefan Schupp - ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems, collocated with Cyber-Physical Systems Week (CPSWeek) on April 17, 2017 in Pittsburgh, PA, USA - [bibtex]
68. ARCH-COMP17 Category Report: Hybrid Systems with Piecewise Constant Dynamics. Goran Frehse, Alessandro Abate, Dieky Adzkiya, Lei Bu, Mirco Giacobbe - ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems, collocated with Cyber-Physical Systems Week (CPSWeek) on April 17, 2017 in Pittsburgh, PA, USA - [bibtex]
69. Modeling the Wind Turbine Benchmark with PWA Hybrid Automata. Nikolaos Kekatos, Marcelo Forets, Goran Frehse - ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems, collocated with Cyber-Physical Systems Week (CPSWeek) on April 17, 2017 in Pittsburgh, PA, USA - [bibtex]
70. Scheduling of Embedded Controllers Under Timing Contracts. Mohammad Al Khatib, Antoine Girard, Thao Dang - Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017, Pittsburgh, PA, USA, April 18-20, 2017 - [bibtex]
71. Counterexample-Guided Refinement of Template Polyhedra. Sergiy Bogomolov, Goran Frehse, Mirco Giacobbe, Thomas A. Henzinger - Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETA - [bibtex]
72. Election et anneaux unidirectionnels en présence d'homonymes. Anaïs Durand - Algotel'2017 - [bibtex]
73. Composition certifié d'algorithmes autostabilisants silencieux. Karine Altisen, Pierre Corbineau - Algotel'2017 - [bibtex]
74. Collision Prevention in Distributed 6TiSCH Networks. Karine Altisen, Olivier Alphand, Rodolphe Bertolini, Stéphane Devismes, Ali Fahs, Franck Rousseau - WiMob 2017, The 13th IEEE International Conference on Wireless and Mobile Computing, Networking and Communications - [bibtex]
75. Deobfuscation of VM based software protection. Jonathan Salwan, Sebastien Bardin, Marie-Laure Potet - Symposium sur la sécurité des technologies de l'information et des communications, SSTIC, France, Rennes, June 7-9 2017 - [bibtex]
76. Generation of Applicative Attacks Scenarios Against Industrial Systems. Maxime Puys, Marie-Laure Potet, Abdelaziz Khaled - Foundations and Practice of Security - 10th International Symposium, FPS 2017, Nancy, France, October 23-25, 2017, Revised Selected Papers - [bibtex]
77. Formally Verifying Flow Properties in Industrial Systems. Jannik Dreier, Maxime Puys, Marie-Laure Potet, Pascal Lafourcade, Jean-Louis Roch - Proceedings of the 14th International Joint Conference on e-Business and Telecommunications (ICETE 2017) - Volume 4: SECRYPT, Madrid, Spain, July 24-26, 2017. - [bibtex]
78. Collision Prevention in Distributed 6TiSCH Networks. Ali Fahs, Rodolphe Bertolini, Olivier Alphand, Franck Rousseau, Karine Altisen, Stéphane Devismes - IEEE International Conference on Wireless and Mobile Computing, Networking and Communications (WiMob) - [bibtex]
79. Constructing verification models of nonlinear Simulink systems via syntactic hybridization. Nikolaos Kekatos, Marcelo Forets, Goran Frehse - Conference on Decision and Control (CDC) - [bibtex]
80. First order temporal logic monitoring with BDDs. Klaus Havelund, Doron Peled, Dogan Ulus - Formal Methods in Computer Aided Design (FMCAD) - [bibtex]
81. Knowledge Based Optimization for Distributed Real-Time Systems. Mahieddine Dellabani, Jacques Combaz, Saddek Bensalem, Marius Bozga - 24th Asia-Pacific Software Engineering Conference, APSEC 2017, Nanjing, China, December 4-8, 2017 - [bibtex]
82. An End-to-End Security Model for Adaptive Service-Oriented Applications. Takoua Abdellatif, Marius Bozga - Service-Oriented Computing - ICSOC 2017 Workshops - ASOCA, ISyCC, WESOACS, and Satellite Events, Málaga, Spain, November 13-16, 2017, Revised Selected Papers - [bibtex]
83. Improved Learning for Stochastic Timed Models by State-Merging Algorithms. Braham Lotfi Mediouni, Ayoub Nouri, Marius Bozga, Saddek Bensalem - NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings - [bibtex]
84. Design of Embedded Systems with Complex Task Dependencies and Shared Resource Interference (Short Paper). Fotios Gioulekas, Peter Poplavko, Rany Kahil, Panagiotis Katsaros, Marius Bozga, Saddek Bensalem, Pedro Palomo - Software Engineering and Formal Methods - 15th International Conference, SEFM 2017, Trento, Italy, September 4-8, 2017, Proceedings - [bibtex]
85. Work In Progress: Toward a Coq-certified Tool for the Schedulability Analysis of Tasks with Offsets. Xiaojie Guo, Sophie Quinton, Pascal Fradet, Jean-François Monin - RTSS 2017 - IEEE Real-Time Systems Symposium - [bibtex]
86. Synthesizing Invariants by Solving Solvable Loops. Steven de Oliveira, Saddek Bensalem, Virgile Prevosto - Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings - [bibtex]
87. TT-BIP: Using Correct-by-Design BIP Approach for Modelling Real-Time System with Time-Triggered Paradigm. Hela Guesmi, Belgacem Ben Hedia, Simon Bliudze, Saddek Bensalem, Briag Le Nabec - Verification and Evaluation of Computer and Communication Systems - 11th International Conference, VECoS 2017, Montreal, QC, Canada, August 24-25, 2017, Proceedings - [bibtex]
88. Regression-Based Statistical Bounds on Software Execution Time. Peter Poplavko, Ayoub Nouri, Lefteris Angelis, Alexandros Zerzelidis, Saddek Bensalem, Panagiotis Katsaros - Verification and Evaluation of Computer and Communication Systems - 11th International Conference, VECoS 2017, Montreal, QC, Canada, August 24-25, 2017, Proceedings - [bibtex]
89. A Framework for Evaluating Schedulability Analysis Tools. Lijun Shan, Susanne Graf, Sophie Quinton, Lo\ic Fejoz - Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday - [bibtex]
90. Ascertaining Uncertainty for Efficient Exact Cache Analysis. Valentin Touzeau, Claire Maiza, David Monniaux, Jan Reineke - Computer Aided Verification - 29th International Conference - [bibtex]
91. The W-SEPT Project: Towards Semantic-Aware WCET Estimation. Claire Maiza, Pascal Raymond, Catherine Parent-Vigouroux, Armelle Bonenfant, Fabienne Carrier, Hugues Cass'e, Philippe Cuenot, Denis Claraz, Nicolas Halbwachs, Erwan Jahier - OASIcs-OpenAccess Series in Informatics - [bibtex]

PhD Thesis and HDR

92. Many-Core timing Analysis of Real-Time Systems. Hamza Rihani - [bibtex]
93. From Timed Component-Based Systems to Time-Triggered Implementations: A Correct-by-Design Approach. Hela Guesmi - [bibtex]

2016

Journal Articles

94. Distinguishing extended finite state machine configurations using predicate abstraction. Khaled El-Fakih, Nina Yevtushenko, Marius Bozga, Saddek Bensalem - J. Software Eng. R&D - [bibtex]
95. Component-based verification using incremental design and invariants. Saddek Bensalem, Marius Bozga, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan - Software and System Modeling - [bibtex]
96. ASTROLABE: A Rigorous Approach for System-Level Performance Modeling and Analysis. Ayoub Nouri, Marius Bozga, Anca Molnos, Axel Legay, Saddek Bensalem - ACM Trans. Embedded Comput. Syst. - [bibtex]
97. Knowledge-based construction of distributed constrained systems. Susanne Graf, Sophie Quinton - Software and System Modeling - [bibtex]
98. Snap-Stabilizing Committee Coordination. Borzoo Bonakdarpour, Stéphane Devismes, Franck Petit - Journal of Parallel and Distributed Computing (JPDC) - [bibtex]
99. The Expressive Power of Snap-Stabilization. Alain Cournier, Ajoy Kumar Datta, Stéphane Devismes, Franck Petit, Vincent Villain - Theoretical Computer Science (TCS) - [bibtex]
100. Competitive Self-Stabilizing k-Clustering. Ajoy Kumar Datta, Stéphane Devismes, Karel Heurtefeux, Lawrence L. Larmore, Yvan Rivierre - Theoretical Computer Science (TCS) - [bibtex]
101. Parallel Simulation of Loosely Timed SystemC/TLM Programs: Challenges Raised by an Industrial Case Study. Denis Becker, Matthieu Moy, Jérôme Cornet - MDPI Electronics - [bibtex]
102. Modeling Power Consumption and Temperature in TLM Models. Matthieu Moy, Claude Helmstetter, Tayeb Bouhadiba, Florence Maraninchi - Leibniz Transactions on Embedded Systems - [bibtex]
103. Causality Problem in Real-Time Calculus. Karine Altisen, Matthieu Moy - Formal Methods in System Design - [bibtex]
104. Silent Self-stabilizing BFS Tree Algorithms Revisited. Stéphane Devismes, Colette Johnen - Journal of Parallel and Distributed Computing (JPDC) - [bibtex]
105. On the existence and decidability of unique decompositions of processes in the applied (pi)-calculus. Jannik Dreier, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech - Theor. Comput. Sci. - [bibtex]
106. Guided search for hybrid systems based on coarse-grained space abstractions. Sergiy Bogomolov, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor T Johnson, Hamed Ladan, Andreas Podelski, Martin Wehrle - STTT - [bibtex]
107. De la surveillance secrète à la prédiction des risques : les dérives du fichage dans le champ de la lutte contre le terrorisme. Virginie Gautron, David Monniaux - Archives de politique criminelle - [bibtex]

Conference Articles

108. Finding Recurrent Sets with Backward Analysis and Trace Partitioning. Alexey Bakhirkin, Nir Piterman - Tools and Algorithms for the Construction and Analysis of System (TACAS) - [bibtex]
109. Polynomial Invariants by Linear Algebra. Steven de Oliveira, Saddek Bensalem, Virgile Prevosto - Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings - [bibtex]
110. A Compositional Approach to the Verification of Hybrid Systems. Lacramioara Astefanoaei, Saddek Bensalem, Marius Bozga - Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday - [bibtex]
111. Compositional Parameter Synthesis. Lacramioara Astefanoaei, Saddek Bensalem, Marius Bozga, Chih-Hong Cheng, Harald Ruess - FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings - [bibtex]
112. Local Planning of Multiparty Interactions with Bounded Horizons. Mahieddine Dellabani, Jacques Combaz, Marius Bozga, Saddek Bensalem - FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings - [bibtex]
113. Monitoring Multi-threaded Component-Based Systems. Hosein Nazarpour, Ylies Falcone, Saddek Bensalem, Marius Bozga, Jacques Combaz - Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings - [bibtex]
114. Mixed-Critical Systems Design with Coarse-Grained Multi-core Interference. Peter Poplavko, Rany Kahil, Dario Socci, Saddek Bensalem, Marius Bozga - Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Pa - [bibtex]
115. A Model-Based Approach to Secure Multiparty Distributed Systems. Najah Ben Said, Takoua Abdellatif, Saddek Bensalem, Marius Bozga - Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Pa - [bibtex]
116. Poster Abstract: Towards Correct Transformation: From High-Level Models to Time-Triggered Implementations. Hela Guesmi, Belgacem Ben Hedia, Mathieu Jan, Simon Bliudze, Saddek Bensalem - 2016 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, April 11-14, 2016 - [bibtex]
117. Performance Evaluation of Complex Systems Using the SBIP Framework. Ayoub Nouri, Marius Bozga, Axel Legay, Saddek Bensalem - Proceedings of the 10th Workshop on Verification and Evaluation of Computer and Communication System, VECoS 2016, Tunis, Tunisia, October 6-7, 2016. - [bibtex]
118. BINSEC/SE: A Dynamic Symbolic Execution Toolkit for Binary-level Analysis. Robin David, Sebastien Bardin, Josselin Feist, Jean-Yves Marion, Laurent Mounier, Marie-Laure Potet, Thanh Dinh Ta - Proceedings of SANER 2016 - [bibtex]
119. Efficient Monitoring of Loose-Ordering Properties for SystemC TLM. Yuliia Romenska, Florence Maraninchi - Design, Automation, and Test in Europe (DATE) - [bibtex]
120. Program Analysis with Local Policy Iteration. Egor George Karpenkov, David Monniaux, Philipp Wendler - Verification, Model Checking, and Abstract Interpretation (VMCAI) - [bibtex]
121. Toward large-scale vulnerability discovery using Machine Learning. Gustavo Grieco, Guillermo Luis Grinblat, Lucas Uzal, Sanjay Rawat, Josselin Feist, Laurent Mounier - Proceedings of CODASPY 2016 publisher = ACM - [bibtex]
122. RDBG: a Reactive Programs Extensible Debugger. Erwan Jahier - 19th International Workshop on Software and Compilers for Embedded Systems (SCOPES'16), May 23th to 25th, 2016, Sankt Goar, Germany - [bibtex]
123. Environment-Model Based Testing with Differential Evolution in an Industrial Setting. Annamária Szenkovits, Noémi Gask\'o, Erwan Jahier - Applications of Evolutionary Computation - 19th European Conference, EvoApplications 2016, Porto, Portugal, March 30 - April 1, 2016, Proceedings, Part I - [bibtex]
124. SycView: Visualize and Profile SystemC Simulations. Denis Becker, Matthieu Moy, Jérôme Cornet - Workshop on Design Automation for Understanding Hardware Designs (DUHDe) - [bibtex]
125. A Framework for Certified Self-Stabilization. Karine Altisen, Corbineau Pierre, Stéphane Devismes - FORTE'2016, the 36th IFIP International Conference on Formal Techniques for Distributed Objects, Components and System - [bibtex]
126. Gradual Stabilization under T-Dynamics. Karine Altisen, Stéphane Devismes, Anaïs Durand, Franck Petit - Euro-Par 2016, 22nd International European Conference on Parallel and Distributed Computing - [bibtex]
127. Efficient Execution of Dependent Tasks on Many-Core Processors. Hamza Rihani, Claire Maiza, Matthieu Moy - RTSOPS 2016 - [bibtex]
128. Response Time Analysis of Synchronous Data Flow Programs on a Many-Core Processor. Hamza Rihani, Matthieu Moy, Claire Maiza, Robert I. Davis, Sebastian Altmeyer - RTNS 2016 - [bibtex]
129. Application of the Reachability Analysis for the Iron Homeostasis Study. Alexandre Rocca, Thao Dang, Eric Fanchon, Jean Marc Moulis - Hybrid Systems Biology - 5th International Workshop, HSB 2016, Grenoble, France, October 20-21, 2016, Proceedings - [bibtex]
130. Parallelotope Bundles for Polynomial Reachability. Tommaso Dreossi, Thao Dang, Carla Piazza - Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, April 12-14, 2016 - [bibtex]
131. Verification and Synthesis of Timing Contracts for Embedded Controllers. Mohammad Al Khatib, Antoine Girard, Thao Dang - Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, April 12-14, 2016 - [bibtex]
132. SL2SX Translator: From Simulink to SpaceEx Models. Stefano Minopoli, Goran Frehse - Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, April 12-14, 2016 - [bibtex]
133. From Simulation Models to Hybrid Automata Using Urgency and Relaxation. Stefano Minopoli, Goran Frehse - Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, April 12-14, 2016 - [bibtex]
134. Some Thoughts on Runtime Verification. Oded Maler - Runtime Verification - 16th International Conference, RV 2016, Madrid, Spain, September 23-30, 2016, Proceedings - [bibtex]
135. Online Timed Pattern Matching Using Derivatives. Dogan Ulus, Thomas Ferrére, Eugene Asarin, Oded Maler - Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETA - [bibtex]
136. A Survey of Satisfiability Modulo Theory. David Monniaux - Computer Algebra in Scientific Computing - [bibtex]
137. Cell Morphing: From Array Programs to Array-Free Horn Clauses. David Monniaux, Laure Gonnord - Static analysis - [bibtex]
138. Formula Slicing: Inductive Invariants from Preconditions. Egor George Karpenkov, David Monniaux - Hardware and Software: Verification and Testing (Haifa Verification Conference) - [bibtex]
139. Model Checking of Cache for WCET Analysis Refinement. Valentin Touzeau, Claire Maiza, David Monniaux - 10th Junior Researcher Workshop on Real-Time Computing - [bibtex]
140. Polyhedral Approximation of Multivariate Polynomials Using Handelman's Theorem. Alexandre Maréchal, Alexis Fouilhé, Tim King, David Monniaux, Michaël Périn - Verification, Model Checking, and Abstract Interpretation (VMCAI) - [bibtex]
141. Specification of concretization and symbolization policies in symbolic execution. Robin David, Sebastien Bardin, Josselin Feist, Laurent Mounier, Marie-Laure Potet, Thanh Dinh Ta, Jean-Yves Marion - Proceedings of the 25th International Symposium on Software Testing and Analysis, ISSTA 2016, Saarbrucken, Germany, July 18-20, 2016 - [bibtex]
142. FISSC: A Fault Injection and Simulation Secure Collection. Louis Dureuil, Guillaume Petiot, Marie-Laure Potet, Thanh-Ha Lee, Aude Crohen, Philippe De Choudens - Computer Safety, Reliability, and Security - 35th International Conference, SAFECOMP 2016, Trondheim, Norway, September 21-23, 2016, Proceedings - [bibtex]
143. Finding the Needle in the Heap: Combining Static Analysis and Dynamic Symbolic Execution to Trigger Use-After-Free. Feist Josselin, Mounier Laurent, Marie-Laure Potet, Sebastien Bardin, David Robin - Proceedings of the 6th Software Security, Protection, and Reverse Engineering Workshop, SSPREW 2016, Los Angeles, USA, December 5-6, 2016 - [bibtex]
144. When the worst-case execution time estimation gains from the application semantics. Armelle Bonenfant, Fabienne Carrier, Hugues Cass'e, Philippe Cuenot, Denis Claraz, Nicolas Halbwachs, Hanbing Li, Claire Maiza, Marianne De Michiel, Vincent Mussot, Catherine Parent-Vigouroux, Isabelle Puaut, Pascal Raymond, Erven Rohou, Pascal Sotin - 8th European Congress on Embedded Real-Time Software and Systems - PDF - [bibtex]
145. Leader Election in Rings with Bounded Multiplicity (Short Paper). Karine Altisen, Ajoy Kumar Datta, Stéphane Devismes, Anaïs Durand, Lawrence L. Larmore - Stabilization, Safety, and Security of Distributed Systems - 18th International Symposium, SSS 2016, Lyon, France, November 7-10, 2016, Proceedings - [bibtex]
146. Domain Specific Stateful Filtering with Worst-Case Bandwidth. Maxime Puys, Jean-Louis Roch, Marie-Laure Potet - 11th International Conference on Critical Information Infrastructures Security (CRITIS 2016) - [bibtex]
147. Private Multi-party Matrix Multiplication and Trust Computations. Jean-Guillaume Dumas, Pascal Lafourcade, Jean-Baptiste Orfila, Maxime Puys - SECRYPT 2016 : 13th International Conference on Security and Cryptography - [bibtex]
148. Formal Analysis of Security Properties on the OPC-UA SCADA Protocol. Maxime Puys, Marie-Laure Potet, Pascal Lafourcade - International Conference on Computer Safety, Reliability, and Security (SAFECOMP'16) - [bibtex]
149. How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property? Radu Iosif, Arnaud Sangnier - Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings - [bibtex]
150. A Decision Procedure for Separation Logic in SMT. Andrew Reynolds, Radu Iosif, Cristina Serban, Tim King - Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings - [bibtex]
151. RTD-Finder: A Tool for Compositional Verification of Real-Time Component-Based Systems. Souha Ben-Rayana, Marius Bozga, Saddek Bensalem, Jacques Combaz - Proceedings of the 22Nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9636 - [bibtex]
152. Concurrence en allocation de ressources locales instantanément stabilisante. Karine Altisen, Stéphane Devismes, Anaïs Durand - Algotel'2016 - [bibtex]
153. Self-Stabilizing Disconnected Components Detection and Rooted Shortest-Path Tree Maintenance in Polynomial Steps. Stéphane Devismes, David Ilcinkas, Colette Johnen - OPODIS 2016, the 20th International Conference on Principles of Distributed Systems - [bibtex]
154. Implementing a Real-time Avionic Application on a Many-core Processor. Moustapha Lo, Nicolas Valot, Florence Maraninchi, Pascal Raymond - 42nd European Rotorcraft Forum (ERF) - [bibtex]

PhD Thesis and HDR

155. Analyse de code et processus d'évaluation des composants sécurisé contre l'injection de faute. Louis Dureuil - Theses - [bibtex]
156. Methods for cryptographic protocols verification in the computational model. Mathilde Duclos - [bibtex]
157. Scheduling of Certifiable Mixed-Criticality Systems. Dario Socci - Theses - [bibtex]
158. Compositional Verification of Component-based Real-time Systems and Applications. Souha Ben Rayana - Tekaya - Theses - [bibtex]
159. Model-based Information Flow Security. Najah Ben Said - Theses - [bibtex]

2015

Journal Articles

160. Self-Stabilizing (f,g)-Alliances with Safe Convergence. Fabienne Carrier, Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore, Yvan Rivierre - Journal of Parallel and Distributed Computing (JPDC) - [bibtex]
161. Weak vs. Self vs. Probabilistic Stabilization. Stéphane Devismes, Sébastien Tixeuil, Masafumi Yamashita - International Journal of Foundations of Computer Science - [bibtex]
162. Optimized distributed implementation of multiparty interactions with Restriction. Saddek Bensalem, Marius Bozga, Jean Quilbeuf, Joseph Sifakis - Sci. Comput. Program. - [bibtex]
163. 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 and System Modeling - [bibtex]
164. Statistical model checking QoS properties of systems with SBIP. Ayoub Nouri, Saddek Bensalem, Marius Bozga, Benoît Delahaye, Cyrille J'egourel, Axel Legay - STTT - [bibtex]
165. Timing analysis enhancement for synchronous program. Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Fabienne Carrier, Mihail Asavoae - Real-Time Systems - PDF - [bibtex]
166. Learning Regular Languages over Large Ordered Alphabets. Irini-Eleftheria Mens, Oded Maler - Logical Methods in Computer Science - [bibtex]
167. Compositional Verification for Timed Systems Based on Automatic Invariant Generation. Souha Ben Rayana, Lacramioara Astefanoaei, Saddek Bensalem, Marius Bozga, Jacques Combaz - Logical Methods in Computer Science - [bibtex]

Book Chapters

168. Correctness of Service Components and Service Component Ensembles. Jacques Combaz, Saddek Bensalem, Francesco Tiezzi, Andrea Margheri, Rosario Pugliese, Jan Kofron - Software Engineering for Collective Autonomic Systems - The ASCENS Approach - [bibtex]

Conference Articles

169. A Forward Analysis for Recurrent Sets. Alexey Bakhirkin, Josh Berdine, Nir Piterman - Static Analysis Symposium (SAS) - [bibtex]
170. Education and training challenges in the era of Cyber-Physical Systems: beyond traditional engineering. Martin Torngren, Saddek Bensalem, John A. McDermid, Roberto Passerone, Alberto L. Sangiovanni-Vincentelli, Bernhard Schatz - Proceedings of the Workshop on Embedded and Cyber-Physical Systems Education, WESE 2015, Amsterdam, The Netherlands, October 4-9, 2015 - [bibtex]
171. A Robust Framework for Securing Composed Web Services. Najah Ben Said, Takoua Abdellatif, Saddek Bensalem, Marius Bozga - Formal Aspects of Component Software - 12th International Conference, FACS 2015, Niteroi, Brazil, October 14-16, 2015, Revised Selected Papers - [bibtex]
172. Time-Triggered Mixed-Critical Scheduler on Single and Multi-processor Platforms. Dario Socci, Peter Poplavko, Saddek Bensalem, Marius Bozga - 17th IEEE International Conference on High Performance Computing and Communications, HPCC 2015, 7th IEEE International Symposium on Cyberspace Safety and Security, CSS 2015, and 12th IEEE In - [bibtex]
173. A Verifiable and Correct-by-Construction Controller for Robots in Human Environments. Lavindra de Silva, Rongjie Yan, Felix Ingrand, Rachid Alami, Saddek Bensalem - Proceedings of the Tenth Annual ACM/IEEE International Conference on Human-Robot Interaction, HRI 2015 Extended Abstracts, Portland, OR, USA, March 02 - 05, 2015 - [bibtex]
174. Optimized distributed implementation of timed component-based systems. Ahlem Triki, Jacques Combaz, Saddek Bensalem - 13. ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015, Austin, TX, USA, September 21-23, 2015 - [bibtex]
175. Automated Conflict-Free Concurrent Implementation of Timed Component-Based Models. Ahlem Triki, Borzoo Bonakdarpour, Jacques Combaz, Saddek Bensalem - NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings - [bibtex]
176. Introduction to ACES-MB 2015. Iulia Dragomir, Susanne Graf, Gabor Karsai, Florian Noyrit, Iulian Ober - Joint Proceedings of the 8th International Workshop on Model-based Architecting of Cyber-physical and Embedded Systems and 1st International Workshop on UML Consistency Rules (ACES-MB 2015 & - [bibtex]
177. Towards Verified Faithful Simulation. Vania Joloboff, Jean-François Monin, Xiaomu Shi - Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings - [bibtex]
178. Election autostabilisante en un nombre polynomial de pas de calcul. Karine Altisen, Stéphane Devismes, Anaïs Durand - 17èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications (AlgoTel) - [bibtex]
179. Self-Stabilizing L-Exclusion Revisited. Fabienne Carrier, Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore - ICDCN'2015, 16th International Conference on Distributed Computing and Networking - [bibtex]
180. A Theory Agenda for Component-Based Design. Joseph Sifakis, Saddek Bensalem, Simon Bliudze, Marius Bozga - Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering - [bibtex]
181. Compositional Verification of Parameterised Timed Systems. Lacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, Jacques Combaz - NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings - [bibtex]
182. Using BIP to reinforce correctness of resource-constrained IoT applications. Alexios Lekidis, Emmanouela Stachtiari, Panagiotis Katsaros, Marius Bozga, Christos K. Georgiadis - 10th IEEE International Symposium on Industrial Embedded Systems, SIES 2015, Siegen, Germany, June 8-10, 2015 - [bibtex]
183. Models for deterministic execution of real-time multiprocessor applications. Peter Poplavko, Dario Socci, Paraskevas Bourgos, Saddek Bensalem, Marius Bozga - Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, DATE 2015, Grenoble, France, March 9-13, 2015 - [bibtex]
184. Multiprocessor Scheduling of Precedence-constrained Mixed-Critical Jobs. Dario Socci, Peter Poplavko, Saddek Bensalem, Marius Bozga - IEEE 18th International Symposium on Real-Time Distributed Computing, ISORC 2015, Auckland, New Zealand, 13-17 April, 2015 - [bibtex]
185. A Timed-Automata Based Middleware for Time-Critical Multicore Applications. Dario Socci, Peter Poplavko, Saddek Bensalem, Marius Bozga - 2015 IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops, ISORC Workshops 2015, Auckland, New Zealand, April 13-17, 2015 - [bibtex]
186. Building Distributed Sensor Network Applications using BIP. Alexios Lekidis, Paraskevas Bourgos, Simplice Djoko-Djoko, Marius Bozga, Saddek Bensalem - Proceedings of 2015 IEEE Sensors Applications Symposium, Zadar, Croatia - [bibtex]
187. Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra. Sylvain Boulmé, Alexandre Maréchal - Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings - [bibtex]
188. From Code Review to Fault Injection Attacks: Filling the Gap using Fault Model Inference). Louis Dureuil, Marie-Laure Potet, Philippe de Choudens, Cécile Dumas, Jessy Clediére - 14th Smart Card Research and Advanced Application Conference) - [bibtex]
189. WCET analysis in shared resources real-time systems with TDMA buses. Hamza Rihani, Matthieu Moy, Claire Maiza, Sebastian Altmeyer - RTNS 2015 - [bibtex]
190. Lightweight Heuristics to Retrieve Parameter Associations from Binaries. Franck de Goer, Roland Groz, Laurent Mounier - Proceedings of the 5th Program Protection and Reverse Engineering Workshop - [bibtex]
191. Scheduling with Preemption Delays: Anomalies and Issues. Guillaume Phavorin, Pascal Richard, Joël Goossens, Thomas Chapeaux, Claire Maiza - Proceedings of the 23rd International Conference on Real Time and Networks Systems - [bibtex]
192. Complexity of scheduling real-time tasks subjected to cache-related preemption delays. Guillaume Phavorin, Pascal Richard, Claire Maiza - Emerging Technologies Factory Automation (ETFA), 2015 IEEE 20th Conference on - [bibtex]
193. A Generic and Compositional Framework for Multicore Response Time Analysis. Sebastian Altmeyer, Robert I. Davis, Leandro Indrusiak, Claire Maiza, Vincent Nelis, Jan Reineke - Proceedings of the 23rd International Conference on Real-Time Networks and Systems (RTNS 2015) - [bibtex]
194. WCET and Mixed-Criticality: What does Confidence in WCET Estimations Depend Upon? Sebastian Altmeyer, Bjorn Lisper, Claire Maiza, Jan Reineke, Christine Rochange - 15th International Workshop on Worst-Case Execution Time Analysis, WCET 2015, July 7, 2015, Lund, Sweden - [bibtex]
195. Polyhedra to the rescue of array interpolants. Francesco Alberti, David Monniaux - ACM Symposium on Applied Computing, software verification and testing track - [bibtex]
196. Synthesis of ranking functions using extremal counterexamples. Laure Gonnord, David Monniaux, Gabriel Radanne - Programming Language Design and Implementation (PLDI) - [bibtex]
197. A simple abstraction of arrays and maps by program translation. David Monniaux, Francesco Alberti - Static analysis (SAS) - [bibtex]
198. Concurrency in Snap-Stabilizing Local Resource Allocation. Karine Altisen, Stéphane Devismes, Anaïs Durand - NETYS'2015, The International Conference on NETworked sYStems - [bibtex]
199. Optimal Torus Exploration by Oblivious Robots. Stéphane Devismes, Anissa Lamani, Franck Petit, Sébastien Tixeuil - NETYS'2015, The International Conference on NETworked sYStems - [bibtex]
200. Runtime-behavior based malware classification using online machine learning. Abdurrahman Pektas, Tankut Acarman, Ylies Falcone, Jean-Claude Fernandez - 2015 World Congress on Internet Security, WorldCIS 2015, Dublin, Ireland, October 19-21, 2015 - [bibtex]
201. Challenges for the Parallelization of Loosely Timed SystemC Programs. Denis Becker, Matthieu Moy, Jérôme Cornet - IEEE International Symposium on Rapid System Prototyping (RSP) - [bibtex]
202. Performance Evaluations of Cryptographic Protocols. Verification Tools Dealing with Algebraic Properties. Pascal Lafourcade, Maxime Puys - To appear in FPS 2015 - [bibtex]
203. Efficient Guiding Strategies for Testing of Temporal Properties of Hybrid Systems. Tommaso Dreossi, Thao Dang, Alexandre Donz\' e, James Patrick Kapinski, Xiaoqing Jin, Jyotirmoy V. Deshmukh - NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings - [bibtex]
204. Computing maximizer trajectories of affine dynamics for reachability. Goran Frehse - 54th IEEE Conference on Decision and Control, CDC 2015, Osaka, Japan, December 15-18, 2015 - [bibtex]
205. Running SpaceEx on the ARCH14 Benchmarks. Stefano Minopoli, Goran Frehse - 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems, ARCH at CPSWeek 2014, Berlin, Germany, April 14, 2014 / ARCH at CPSWeek 2015, Seattle, WA, USA, April 13, - [bibtex]
206. Parameter Synthesis Through Temporal Logic Specifications. Thao Dang, Tommaso Dreossi, Carla Piazza - FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings - [bibtex]
207. Eliminating spurious transitions in reachability with support functions. Goran Frehse, Sergiy Bogomolov, Marius Greitschus, Thomas Strump, Andreas Podelski - Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC'15, Seattle, WA, USA, April 14-16, 2015 - [bibtex]
208. An Introduction to Hybrid Automata, Numerical Simulation and Reachability Analysis. Goran Frehse - Formal Modeling and Verification of Cyber-Physical Systems, 1st International Summer School on Methods and Tools for the Design of Digital Systems, Bremen, Germany, September 2015 - [bibtex]
209. Measuring with Timed Patterns. Thomas Ferrére, Oded Maler, Dejan Nickovic, Dogan Ulus - Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II - [bibtex]
210. Stochastic Local Search for Falsification of Hybrid Systems. Jyotirmoy V. Deshmukh, Xiaoqing Jin, James Patrick Kapinski, Oded Maler - Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings - [bibtex]
211. On Switching Aware Synthesis for Combinational Circuits. Jan Láník, Oded Maler - Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings - [bibtex]
212. Reducing power with activity trigger analysis. Jan Láník, Julien Legriel, Erwan Piriou, Emmanuel Viaud, Fahim Rahim, Oded Maler, Solaiman Rahim - 13. ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015, Austin, TX, USA, September 21-23, 2015 - [bibtex]
213. Current Challenges in the Verification of Hybrid Systems. Stefan Schupp, Erika Abraham, Xin Chen, Ibtissem Ben Makhlouf, Goran Frehse, Sriram Sankaranarayanan, Stefan Kowalewski - Cyber Physical Systems. Design, Modeling, and Evaluation - 5th International Workshop, CyPhy 2015, Amsterdam, The Netherlands, October 8, 2015, Proceedings - [bibtex]
214. A Benchmark Suite for Hybrid Systems Reachability Analysis. Xin Chen, Stefan Schupp, Ibtissem Ben Makhlouf, Erika Abraham, Goran Frehse, Stefan Kowalewski - NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings - [bibtex]

PhD Thesis and HDR

215. Le domaine abstrait des polyèdres revisité : représentation par contraintes et preuve formelle. Alexis Fouilhé - [bibtex]
216. Rigorous System-level Modeling and Performance Evaluation for Embedded System Design. Ayoub Nouri - Theses - [bibtex]
217. Distributed Implementations of Timed Component-based Systems. Ahlem Triki - Theses - [bibtex]
218. Design flow for the rigorous development of networked embedded systems. Alexios Lekidis - Theses - [bibtex]

2014

Journal Articles

219. Verification and validation meet planning and scheduling. Saddek Bensalem, Klaus Havelund, Andrea Orlandini - STTT - [bibtex]
220. Statically detecting Use-After-Free on Binary Code. Josselin Feist, Laurent Mounier, Marie-Laure Potet - Journal of Computer Virology and Hacking Techniques - [bibtex]
221. Compte-rendu d'habilitation : Modélisation à haut niveau d'abstraction pour les systèmes embarqués. Matthieu Moy - Technique et Science Informatiques - [bibtex]
222. Synthesizing robust systems. Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Georg Hofferek, Barbara Jobstmann, Bettina Konighofer, Robert Konighofer - Acta Inf. - [bibtex]
223. Analyse de Code et Recherche de Vulnérabilités. Marie-Laure Potet, Josselin Feist, Laurent Mounier - Revue MISC - [bibtex]
224. 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]
225. Deciding Conditional Termination. Marius Bozga, Radu Iosif, Filip Konecn\'y - Logical Methods in Computer Science - [bibtex]
226. Implementing and Reasoning About Hash-consed Data Structures in Coq. Thomas Braibant, Jacques-Henri Jourdan, David Monniaux - Journal of Automated Reasoning - [bibtex]
227. Apport des méthodes formelles pour l'exploitation des logs informatiques dans un contexte contractuel. Gregor Goessler, Daniel Le Métayer, Eduardo Mazza, Marie-Laure Potet, Lacramioara Astefanoaei - TSI, Technique et Science Informatiques - [bibtex]
228. Comparison of Mean Hitting Times for a Degree-Biased Random Walk. Karine Altisen, Stéphane Devismes, Antoine Gerbaud, Pascal Lafourcade - Discrete Applied Mathematics - [bibtex]

Book Chapters

229. Estimation de temps d'exécution et délais. Claire Maiza, Christine Rochange, Pascal Raymond - Ordonnancement dans les systèmes temps réel - [bibtex]
230. Estimation of Execution Time and Delays. Claire Maiza, Christine Rochange, Pascal Raymond - Real-time Systems Scheduling 1 - [bibtex]
231. The Unmet Challenge of Timed Systems. Oded Maler - From Programs to Systems - [bibtex]
232. Cellular iron regulation in animals: need and use of suitable models. Emmanuel Pourcelot, Nicolas Mobilia, Alexandre Donzé, Oded Maler, Pascal Mossuz, Eric Fanchon - Nutzen-Risiko-Bewertung von Mineralstoffen und Spurenelementen: Biochemische, physiologische und toxikologische Aspekte - [bibtex]
233. Contract-Based Reasoning for Component Systems with Rich Interactions. Susanne Graf, Roberto Passerone, Sophie Quinton - Embedded Systems Development - [bibtex]

Conference Articles

234. Backward Analysis via over-Approximate Abstraction and under-Approximate Subtraction. Alexey Bakhirkin, Josh Berdine, Nir Piterman - Static Analysis Symposium (SAS) - [bibtex]
235. On Probabilistic Snap-Stabilization. Karine Altisen, Stéphane Devismes - ICDCN'2014, 15th International Conference on Distributed Computing and Networking - [bibtex]
236. Environment-Model Based Testing of Control Systems: Case Studies. Erwan Jahier, Simplice Djoko-Djoko, Chaouki Maiza, Eric Lafont - International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014), Held as Part of ETAPS 2014. - [bibtex]
237. Learning Regular Languages over Large Alphabets. Oded Maler, Irini Eleftheria Mens - International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014 - [bibtex]
238. 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]
239. Stabilisation Instantanée Probabiliste. Karine Altisen, Stéphane Devismes - 16èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications (AlgoTel) - [bibtex]
240. 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]
241. 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]
242. A certifying frontend for (sub)polyhedral abstract domains. Alexis Fouilhé, Sylvain Boulmé - Verified Software: Theories, Tools and Experiments (VSTTE 2014) - [bibtex]
243. 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]
244. Schedulability and modular analysis: how to fit timing model? Hugues Cass'e, Claire Maiza, Catherine and Parent-Vigouroux, Pascal Raymond - OPRTC - PDF - [bibtex]
245. Timing analysis enhancement for synchronous program. Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Fabienne Carrier, Mihail Asavoae - Workshop on Reconciling Performance and Predictability (REPP) - PDF - [bibtex]
246. Selfish-LRU: Preemption-Aware Caching for Predictability and Performance. Jan Reineke, Sebastian Altmeyer, Daniel Grund, Sebastian Hahn, Claire Maiza - Proceedings of the 20th Real-Time and Embedded Technology and Applications Symposium (RTAS'14) - PDF - [bibtex]
247. (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]
248. 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]
249. Formal Analysis of Electronic Exams. Jannik Dreier, Rosario Giustolisi, Ali Kassem, Pascal Lafourcade, Gabriele Lenzin, Peter Ryan - SECRYPT 2014 - [bibtex]
250. Self-Stabilizing Leader Election in Polynomial Steps. Karine Altisen, Alain Cournier, Stéphane Devismes, Anaïs Durand, Franck Petit - SSS'2014, 16th International Symposium on Stabilization, Safety, and Security of Distributed Systems - [bibtex]
251. A General Approach for Expressing Infeasibility in Implicit Path Enumeration Technique. Pascal Raymond - International Conference on Embedded Software (EMSOFT 2014) - PDF - [bibtex]
252. The WCET Analysis using Counters - A Preliminary Assessment. Remy Boutonnet, Mihail Asavoae - In Proceedings of 8th JRWRTC, in conjunction with RTNS14 - PDF - [bibtex]
253. 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]
254. Architecture internalisation in BIP. Simon Bliudze, Joseph Sifakis, Marius Bozga, Mohamad Jaber - CBSE'14, Proceedings of the 17th International ACM SIGSOFT Symposium on Component-Based Software Engineering (part of CompArch 2014), Marcq-en-Baroeul, Lille, France, June 30 - July 4, 2014 - [bibtex]
255. 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]
256. 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]
257. How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. Julien Henry, Mihail Asavoae, David Monniaux, Claire Maiza - SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2014, LCTES '14 - [bibtex]
258. Rigorous System Design Flow for Autonomous Systems. Saddek Bensalem, Marius Bozga, Jacques Combaz, Ahlem Triki - Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change - 6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Procee - [bibtex]
259. Building faithful high-level models and performance evaluation of manycore embedded systems. Ayoub Nouri, Marius Bozga, Anca Molnos, Axel Legay, Saddek Bensalem - Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2014, Lausanne, Switzerland, October 19-21, 2014 - [bibtex]
260. Faster Statistical Model Checking by Means of Abstraction and Learning. Ayoub Nouri, Balaji Raman, Marius Bozga, Axel Legay, Saddek Bensalem - Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings - [bibtex]
261. Combining High-Level and Low-Level Approaches to Evaluate Software Implementations Robustness Against Multiple Fault Injection Attacks. Lionel Rivi`ere, Marie-Laure Potet, Thanh-Ha Le, Julien Bringer, Herve Chabanne, Maxime Puys - Foundations and Practice of Security - 7th International Symposium, FPS 2014, Montreal, QC, Canada, November 3-5, 2014. Revised Selected Papers - [bibtex]
262. Speeding Up Logico-Numerical Strategy Iteration. David Monniaux, Peter Schrammel - Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings - [bibtex]
263. Efficient and Generalized Decentralized Monitoring of Regular Languages. Ylies Falcone, Tom Cornebize, Jean-Claude Fernandez - Formal Techniques for Distributed Objects, Components, and Systems - 34th IFIP WG 6.1 International Conference, FORTE 2014, Held as Part of the 9th International Federated Conference on Distribu - [bibtex]
264. On the Expressiveness of some Runtime Validation Techniques. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier - HOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday - [bibtex]
265. High-Level Simulation for Multiple Fault Injection Evaluation. Maxime Puys, Lionel Rivi`ere, Julien Bringer, Thanh-Ha Le - Data Privacy Management, Autonomous Spontaneous Security, and Security Assurance - 9th International Workshop, DPM 2014, 7th International Workshop, SETOP 2014, and 3rd International Workshop, QA - [bibtex]
266. Many-Core Scheduling of Data Parallel Applications Using SMT Solvers. Pranav Tendulkar, Peter Poplavko, Ioannis Galanommatis, Oded Maler - 17th Euromicro Conference on Digital System Design, DSD 2014, Verona, Italy, August 27-29, 2014 - [bibtex]
267. Test Coverage Estimation Using Threshold Accepting. Thao Dang, Noa Shalev - Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings - [bibtex]
268. Non-convex Invariants and Urgency Conditions on Linear Hybrid Automata. Stefano Minopoli, Goran Frehse - Formal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Florence, Italy, September 8-10, 2014. Proceedings - [bibtex]
269. Parameter Synthesis Using Parallelotopic Enclosure and Applications to Epidemic Models. Thao Dang, Tommaso Dreossi, Carla Piazza - Hybrid Systems Biology - Second International Workshop, HSB 2013, Taormina, Italy, September 2, 2013 and Third International Workshop, HSB 2014, Vienna, Austria, July 23-24, 2014, Revised Selected - [bibtex]
270. Exploiting the Eigenstructure of Linear Systems to Speed up Reachability Computations. Alexandre Rocca, Thao Dang, Eric Fanchon - Hybrid Systems Biology - Second International Workshop, HSB 2013, Taormina, Italy, September 2, 2013 and Third International Workshop, HSB 2014, Vienna, Austria, July 23-24, 2014, Revised Selected - [bibtex]
271. Assume-Guarantee Abstraction Refinement Meets Hybrid Systems. Sergiy Bogomolov, Goran Frehse, Marius Greitschus, Radu Grosu, Corina S. Pasareanu, Andreas Podelski, Thomas Strump - Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014. Proceedings - [bibtex]
272. Parameter synthesis for polynomial biological models. Tommaso Dreossi, Thao Dang - 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'14, Berlin, Germany, April 15-17, 2014 - [bibtex]
273. Formal Analysis of Timing Effects on Closed-Loop Properties of Control Software. Goran Frehse, Arne Hamann, Sophie Quinton, Matthias Woehrle - Proceedings of the IEEE 35th IEEE Real-Time Systems Symposium, RTSS 2014, Rome, Italy, December 2-5, 2014 - [bibtex]
274. Timed Pattern Matching. Dogan Ulus, Thomas Ferrére, Eugene Asarin, Oded Maler - Formal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Florence, Italy, September 8-10, 2014. Proceedings - [bibtex]
275. Formal and Informal Methods for Multi-Core Design Space Exploration. Jean-Francois Kempf, Olivier Lebeltel, Oded Maler - QAPL - [bibtex]
276. Compositional Verification of Timed Systems. Saddek Bensalem - Proceedings of the 8th International Workshop on Verification and Evaluation of Computer and Communication Systems, VECoS 2014, Beja"ia, Algeria, September 29-30, 2014. - [bibtex]
277. 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]

PhD Thesis and HDR

278. Automated Verification of Termination Certificates. Kim Quyen Ly - [bibtex]
279. High-level Models for Embedded Systems. Matthieu Moy - Habilitation à Diriger des Recherches (HDR) - [bibtex]
280. Static Analysis by Abstract Interpretation and Decision Procedures. Julien Henry - PDF - [bibtex]
281. Protocols and Models for the Security of Wireless Ad-Hoc Networks. Raphael Jamet - [bibtex]
282. Vérification et synthèse quantitative. Christian von Essen - [bibtex]

2013

Journal Articles

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

Book Chapters (inbook)

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

Book Chapters

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

Conference Articles

297. Handcrafted Inversions Made Operational on Operational Semantics. Jean-François Monin, Xiaomu Shi - ITP 2013 - [bibtex]
298. Flowpipe Approximation and Clustering in Space-Time. Goran Frehse, Colas Le Guernic, Rajat Kateja - HSCC - [bibtex]
299. Underapproximation of Procedure Summaries for Integer Programs. Pierre Ganty, Radu Iosif, Filip Konecn\'y - TACAS - [bibtex]
300. Fast and Accurate TLM Simulations using Temporal Decoupling for FIFO-based Communications. Claude Helmstetter, Jérôme Cornet, Bruno Galilée, Matthieu Moy, Pascal VIVET - Design, Automation and Test in Europe (DATE) - [bibtex]
301. Co-Simulation of Functional SystemC TLM Models with Power/Thermal Solvers. Tayeb Bouhadiba, Matthieu Moy, Florence Maraninchi, Jérôme Cornet, Laurent Maillet-Contoz, Ilija Materic - Virtual Prototyping of Parallel and Embedded Systems (VIPES) - [bibtex]
302. As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty. Jean-Francois Kempf, Marius Bozga, Oded Maler - TACAS - PDF - [bibtex]
303. Explorer une grille avec un minimum de robots amnésiques. Franck Petit, Anissa Lamani, Stéphane Devismes, Sébastien Tixeuil, Pascal Raymond - 15èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications (AlgoTel) - [bibtex]
304. 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]
305. 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]
306. 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]
307. Verifiability in E-Auction Protocols. Jannik Dreier, Hugo Jonker, Pascal Lafourcade - 1st Workshop on Hot Issues in Security Principles and Trust (HotSpot 2013) - [bibtex]
308. Multiple Independent Lazy Intruders. Ali Kassem, Pascal Lafourcade, Yassine Lakhnech, Sebastian M odersheim - 1st Workshop on Hot Issues in Security Principles and Trust (HotSpot 2013) - [bibtex]
309. Engineering Functional Requirements of Reactive Systems using Synchronous Languages. Erwan Jahier, Nicolas Halbwachs, Pascal Raymond - International Symposium on Industrial Embedded Systems, 2013. SIES'13. - [bibtex]
310. Efficient Robust Monitoring for STL. Alexandre Donzé, Thomas Ferrére, Oded Maler - CAV - [bibtex]
311. Verification of embedded control programs. Thao Dang, Bertrand Jeannet, Romain Testylier - Proceedings of European Conrol Conference ECC - [bibtex]
312. 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]
313. Integrating cache related pre-emption delay analysis into EDF scheduling. Will Lunniss, Sebastian Altmeyer, Claire Maiza, Robert I. Davis - 19th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2013, Philadelphia, PA, USA, April 9-11, 2013 - [bibtex]
314. 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]
315. Exploring the Dynamics of Mass Action Systems. Oded Maler, Adam M. Halasz, Olivier Lebeltel, Ouri Maler - Hybrid Systems Biology - PDF - [bibtex]
316. Falsifying Oscillation Properties of Parametric Biological Models. Thao Dang, Tommaso Dreossi - Proceedings Second International Workshop on Hybrid Systems and Biology, HSB 2013, Taormina, Italy, 2nd September 2013 - [bibtex]
317. NLTOOLBOX: A Library for Reachability Computation of Nonlinear Dynamical Systems. Romain Testylier, Thao Dang - Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings - [bibtex]
318. Algorithmic Analysis of Continuous and Hybrid Systems. Oded Maler - Infinity - [bibtex]
319. 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]
320. 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]
321. 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]
322. 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]
323. Implementing hash-consed data structures in Coq. Thomas Braibant, Jacques-Henri Jourdan, David Monniaux - Interactive theorem proving (ITP) - [bibtex]
324. Modular, hierarchical models of control systems in SpaceEx. Alexandre Donzé, Goran Frehse - Control Conference (ECC), 2013 European - [bibtex]
325. Self-Stabilizing (f,g)-Alliances with Safe Convergence. Fabienne Carrier, Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore, Yvan Rivierre - SSS'2013, 15th International Symposium on Stabilization, Safety, and Security of Distributed Systems - [bibtex]
326. Self-stabilizing Silent Disjunction in an Anonymous Network. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore - ICDCN: 14th International Conference on Distributed Computing and Networking - [bibtex]
327. Fast Leader (Full) Recovery despite Dynamic Faults. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore, Sébastien Tixeuil - ICDCN: 14th International Conference on Distributed Computing and Networking - [bibtex]
328. 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]
329. Preface. Barbara Jobstmann, Sandip Ray - Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013 - [bibtex]
330. 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]
331. Symmetry Breaking for Multi-criteria Mapping and Scheduling on Multicores. Pranav Tendulkar, Peter Poplavko, Oded Maler - FORMATS - [bibtex]
332. 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]
333. Algorithme autostabilisant avec convergence sûre construisant une $(f,g)$-alliance. Fabienne Carrier, Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore, Yvan Rivierre - Algotel : 15èmes Rencontres Francophones pour les Aspects Algorithmiques des Télécommunications - [bibtex]
334. Program Semantics in Model-Based WCET Analysis: A State of the Art Perspective. Mihail Asavoae, Claire Maiza, Pascal Raymond - 13th International Workshop on Worst-Case Execution Time Analysis, WCET 2013, July 9, 2013, Paris, France - PDF - [bibtex]
335. Timing analysis enhancement for synchronous program. Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Fabienne Carrier - RTNS - PDF - [bibtex]
336. System-Level Modeling of Energy in TLM for Early Validation of Power and Thermal Management. Tayeb Bouhadiba, Matthieu Moy, Florence Maraninchi - Design Automation and Test Europe (DATE) - PDF - [bibtex]
337. Parallel Programming with SystemC for Loosely Timed Models: A Non-Intrusive Approach. Matthieu Moy - The Design, Automation, and Test in Europe (DATE) - [bibtex]
338. Incremental Generation of Linear Invariants for Component-Based Systems. Saddek Bensalem, Marius Bozga, Beno^it Boyer, Axel Legay - 13th International Conference on Application of Concurrency to System Design, ACSD 2013, Barcelona, Spain, 8-10 July, 2013 - [bibtex]
339. 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]
340. 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]
341. 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]
342. 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]
343. 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]
344. SBIP: A Statistical Model Checking Extension for the BIP Framework. Ayoub Nouri, Axel Legay, Saddek Bensalem, Marius Bozga - Statistical Model Checking Workshop, SMC - [bibtex]
345. 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]
346. Time-Triggered Mixed-Critical Scheduler. Dario Socci, Petro Poplavko, Saddek Bensalem, Marius Bozga - 1st International Workshop on Mixed Criticality Systems (WMC) - [bibtex]
347. 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]
348. Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra. Alexis Fouilhé, David Monniaux, Michaël Périn - Static analysis (SAS) - [bibtex]
349. Analysis of Probabilistic Cache Related Pre-emption Delays. Robert I. Davis, Luca Santinelli, Sebastian Altmeyer, Claire Maiza, Liliana Cucu-Grosjean - 25th Euromicro Conference on Real-Time Systems (ECRTS 2013) - [bibtex]
350. Flowpipe approximation and clustering in space-time. Goran Frehse, Rajat Kateja, Colas Le Guernic - Proceedings of the 16th international conference on Hybrid systems: computation and control, HSCC 2013, April 8-11, 2013, Philadelphia, PA, USA - [bibtex]
351. Synthesizing distributed scheduling implementation for probabilistic component-based systems. Saddek Bensalem, Axel Legay, Ayoub Nouri, Doron Peled - 11th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMCODE 2013, Portland, OR, USA, October 18-20, 2013 - [bibtex]

PhD Thesis and HDR

352. Certification of an Instruction Set Simulator. Xiaomu Shi - [bibtex]
353. Rigorous Design Flow for Programming Manycore Platforms. Paraskevas Bourgos - [bibtex]
354. Towards efficient and secure shared memory applications. Emmanuel Sifakis - [bibtex]
355. Self-Stabilizing Algorithms for Constructing Distributed Spanning Structures. Yvan Rivierre - [bibtex]
356. Analyse statique de programmes manipulant des tableaux. Valentin Perrelle - Thesis - [bibtex]
357. Implantations distribuées de modèles à base de composants communicants par interactions multiparties avec priorités : application au langage BIP.. Jean Quilbeuf - [bibtex]
358. Rigorous Design Flow for Programming Manycore Platforms. Paraskevas Bourgos - Theses - [bibtex]
359. Distributed Implementations of Component-based Systems with Prioritized Multiparty Interactions : Application to the BIP Framework.. Jean Quilbeuf - Theses - [bibtex]

2012

Journal Articles

360. Optimizing Explicit Data Transfers for Data Parallel Applications on the Cell Architecture. Selma Saidi, Pranav Tendulkar, Thierry Lepley, Oded Maler - ACM Transactions on Architecture and Code Optimization, Vol. V, - PDF - [bibtex]
361. 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]
362. Achieving distributed control through model checking. Susanne Graf, Doron Peled, Sophie Quinton - Formal Methods in System Design - [bibtex]
363. 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]
364. Synthesis of Reactive(1) designs. Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Yaniv Sa'ar - J. Comput. Syst. Sci. - [bibtex]
365. Finding and fixing faults. Barbara Jobstmann, Stefan Staber, Andreas Griesmayer, Roderick Bloem - J. Comput. Syst. Sci. - [bibtex]
366. Monitoring Properties of Analog and Mixed-Signal Designs,. Oded Maler, Dejan Nickovic - Software Tools for Technology Transfer - [bibtex]
367. Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs. Thomas Gawlitza, David Monniaux - Logical Methods in Computer Science - [bibtex]
368. Improved cache related pre-emption delay aware response time analysis for fixed priority pre-emptive systems. Sebastian Altmeyer, Robert I. Davis, Claire Maiza - Real-Time Systems - [bibtex]
369. Reachability analysis for polynomial dynamical systems using the Bernstein expansion. Thao Dang, Romain Testylier - Reliable Computing Journal - [bibtex]
370. Introduction à la calculabilité. David Monniaux - Quadrature - [bibtex]
371. Algorithme autostabilisant construisant un petit ensemble k-dominant. Ajoy Kumar Datta, Stéphane Devismes, Karel Heurtefeux, Lawrence L. Larmore, Yvan Rivierre - Technique et Science Informatiques - [bibtex]
372. Politiques de gestion de protections pour l'implémentation de sections critiques.. Sifakis Emmanuel, Mounier Laurent - Techniques et Sciences Informatiques - [bibtex]
373. More testable properties. Ylies Falcone, Jean-Claude Fernandez, Thierry Jéron, Hervé Marchand, Laurent Mounier - STTT - [bibtex]
374. Generating Invariant-based Certificates for Embedded Systems. Jan-Olaf Blech, Michaël Périn - ACM Transactions on Embedded Computing Systems (TECS) - [bibtex]
375. Model-based implementation of distributed systems with priorities. Borzoo Bonakdarpour, Marius Bozga, Jean Quilbeuf - Design Automation for Embedded Systems - [bibtex]
376. A framework for automated distributed implementation of component-based models. Borzoo Bonakdarpour, Marius Bozga, Mohamad Jaber, Jean Quilbeuf, Joseph Sifakis - Distributed Computing - [bibtex]
377. Statistical abstraction and model-checking of large heterogeneous systems. Ananda Basu, Saddek Bensalem, Marius Bozga, Benoît Delahaye, Axel Legay - STTT - [bibtex]
378. 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]

Book Chapters (inbook)

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

Conference Articles

380. Is RSSI a good choice for localization in Wireless Sensor Network? Karel Heurtefeux, Fabrice Valois - IEEE International Conference on Advanced Information Networking and Applications - [bibtex]
381. 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]
382. 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]
383. Deciding Conditional Termination. Marius Bozga, Radu Iosif, Filip Konecn\'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]
384. Experiments on the feasibility of using a floating-point simplex in an SMT solver. Diego Caminha Barbosa de Oliveira, David Monniaux - Workshop on Practical Aspects of Automated Reasoning (PAAR) - [bibtex]
385. Anatomy of Alternating Quantifier Satisfiability (Work in progress). Anh-Dung Phan, Nikolaj Bj\orner, David Monniaux - 10th International Workshop on Satisfiability Modulo Theories (SMT) - [bibtex]
386. Algorithme de k-partitionnement auto-stabilisant et compétitif. Kumar Ajoy Datta, Stéphane Devismes, Karel Heurtefeux, Lawrence L. Larmore, Yvan Rivierre - 14èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications (AlgoTel) - [bibtex]
387. Optimal 2D Data Partitioning for DMA Transfers on MPSoCs. Selma Saidi, Pranav Tendulkar, Thierry Lepley, Oded Maler - Proceedings of the 15th EUROMICRO Conference on Digital System Design - [bibtex]
388. Co-Simulation of a SystemC TLM Virtual Platform with a Power Simulator at the Architectural Level: Case of a Set-Top Box. Jérôme Cornet, Laurent Maillet-Contoz, Ilija Materic, Sylvian Kaiser, Hela Boussetta, Tayeb Bouhadiba, Matthieu Moy, Florence Maraninchi - Design Automation Conference - [bibtex]
389. PAGAI: a path sensitive static analyzer. Julien Henry, David Monniaux, Matthieu Moy - Tools for Automatic Program Analysis (TAPAS) - [bibtex]
390. 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]
391. Competitive Self-Stabilizing k-Clustering. Ajoy Kumar Datta, Stéphane Devismes, Karel Heurtefeux, Lawrence L. Larmore, Yvan Rivierre - ICDCS - [bibtex]
392. Succinct Representations for Abstract Interpretation. Julien Henry, David Monniaux, Matthieu Moy - Static analysis (SAS) - [bibtex]
393. When the decreasing sequence fails. Nicolas Halbwachs, Julien Henry - 19th International Static Analysis Symposium, SAS'12 - PDF - [bibtex]
394. Brief Announcement: Self-stabilizing Silent Disjunction in an Anonymous Network. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore - Stabilization, Safety, and Security of Distributed Systems - 14th International Symposium, SSS 2012, Toronto, Canada, October 1-4, 2012. Proceedings - [bibtex]
395. On efficiency of unison. Stéphane Devismes, Franck Petit - 4th Workshop on Theoretical Aspects of Dynamic Distributed Systems, TADDS - [bibtex]
396. 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]
397. 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]
398. 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]
399. 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]
400. Flowpipe-Guard Intersection for Reachability Computations with Support Functions. Goran Frehse, Rajarshi Ray - IFAC Conf. Analysis and Design of Hybrid Systems (ADHS) - [bibtex]
401. Analysis of parametric biological models with non-linear dynamics. Romain Testylier, Thao Dang - HSB - [bibtex]
402. Investigation of Scratchpad Memory for Preemptive Multitasking. Jack Whitham, Robert I. Davis, Neil C. Audsley, Sebastian Altmeyer, Claire Maiza - RTSS - [bibtex]
403. Accelerating Interpolants. Hossein Hojjat, Radu Iosif, Filip Konecn\'y, Viktor Kuncak, Philipp Rümmer - ATVA - [bibtex]
404. A Verification Toolkit for Numerical Transition Systems - Tool Paper. Hossein Hojjat, Filip Konecn\'y, Florent Garnier, Radu Iosif, Viktor Kuncak, Philipp Rümmer - FM - [bibtex]
405. On Temporal Logic and Signal Processing. Alexandre Donzé, Oded Maler, Ezio Bartocci, Dejan Nickovic, Radu Grosu, Scott Smolka - ATVA - PDF - [bibtex]
406. A Taint Based Approach for Smart Fuzzing. Sofia Bekrar, Chaouki Bekrar, Roland Groz, Laurent Mounier - Proceedings of SecTest - [bibtex]
407. Dynamic Information-Flow Analysis for Multi-threaded Applications. Laurent Mounier, Emmanuel Sifakis - Proceedings of ISoLA - [bibtex]
408. Finding Buffer Overflow Inducing Loops in Binary Executables. Sanjay Rawat, Laurent Mounier - Proceedings of Sixth International Conference on Software Security and Reliability (SERE) - [bibtex]
409. Formal Model Driven Engineering for Space Onboard Software. Eric Conquet,Dormoy, Franç,ois-Xavier, Iulia Dragomir, Susanne Graf, David Lesens, Piotr Nienaltowski, Iulian Ober - International Congress on Embedded Real Time Software and Systems (ERTS2), Toulouse, February 2012 - [bibtex]
410. Reachability Analysis of Polynomial Systems Using Linear Programming Relaxations. Mohamed Amin Ben Sassi, Romain Testylier, Thao Dang, Antoine Girard - Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings - [bibtex]
411. State Estimation and Property-Guided Exploration for Hybrid Systems Testing. Thao Dang, Noa Shalev - ICTSS - [bibtex]
412. 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]
413. 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]
414. 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]
415. 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]
416. 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]
417. 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]
418. 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]
419. Statistical Model Checking QoS Properties of Systems with SBIP. Saddek Bensalem, Marius Bozga, Benoît Delahaye, Cyrille J'egourel, 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]
420. 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]
421. 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]
422. 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]
423. 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]
424. A Theory of Fault Recovery for Component-Based Models. Borzoo Bonakdarpour, Marius Bozga, Gregor Goessler - Stabilization, Safety, and Security of Distributed Systems - 14th International Symposium, SSS 2012, Toronto, Canada, October 1-4, 2012. Proceedings - [bibtex]
425. A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx. Sergiy Bogomolov, Goran Frehse, Radu Grosu, Hamed Ladan, Andreas Podelski, Martin Wehrle - Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings - [bibtex]
426. Optimal Grid Exploration by Asynchronous Oblivious Robots. Stéphane Devismes, Anissa Lamani, Franck Petit, Pascal Raymond, Sébastien Tixeuil - 14th International Symposium on Stabilization, Safety, and Security of Distributed Systems, SSS - [bibtex]

PhD Thesis and HDR

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

2011

Journal Articles

438. What can you Verify and Enforce at Runtime ? Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier - Software Tool in Tecnology Transfer (STTT) - [bibtex]
439. Runtime Enforcement Monitors: composition, synthesis, and enforcement abilities. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier, Jean-Luc Richier - Formal Methods in System Design - [bibtex]
440. Self-Stabilizing k-out-of-l exclusion on tree networks. Ajoy Kumar Datta, Stéphane Devismes, Florian Horn, Lawrence L. Larmore - International Journal of Foundations of Computer Science - [bibtex]
441. Computing reachable states for nonlinear biological models. Thao Dang, Colas Le Guernic, Oded Maler - Theoretical Computer Science - [bibtex]
442. Asymptotically Optimal Deterministic Rendezvous. Fabienne Carrier, Stéphane Devismes, Franck Petit, Yvan Rivierre - International Journal of Foundations of Computer Science (IJFCS) - [bibtex]
443. Automated Proofs for Asymmetric Encryption. Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech - J. Autom. Reasoning - [bibtex]
444. Autour de l'Auto-stabilisation. Partie I : Techniques généralisant l'approche. Stéphane Devismes, Franck Petit, Vincent Villain - Technique et science informatiques (TSI) - [bibtex]
445. Autour de l'Auto-Stabilisation. Partie II : Techniques spécialisant l'approche. Stéphane Devismes, Franck Petit, Vincent Villain - Technique et science informatiques (TSI) - [bibtex]
446. Robustness Analysis and Behavior Discrimination in Enzymatic Reaction Networks. Alexandre Donzé, Eric Fanchon, Lucie Martine Gattepaille, Oded Maler, Philippe Tracqui - PLOS One - [bibtex]
447. Building Distributed Controllers for Systems with Priorities. Imene Ben Hafaiedh, Susanne Graf, Sophie Quinton - J. Log. Algebr. Program. - [bibtex]
448. Formalisms for Specifying Markovian Population Models. Thomas A. Henzinger, Barbara Jobstmann, Verena Wolf - Int. J. Found. Comput. Sci. - [bibtex]
449. 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]
450. 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]
451. 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]
452. Priority scheduling of distributed systems based on model checking. Ananda Basu, Saddek Bensalem, Doron Peled, Joseph Sifakis - Formal Methods in System Design - [bibtex]
453. A vision for computer science - the system perspective. Joseph Sifakis - Central Europ. J. Computer Science - [bibtex]

Book Chapters (inbook)

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

Book Chapters

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

Conference Articles

457. First Steps towards the Certification of an ARM Simulator Using Compcert. Xiaomu Shi, Jean-François Monin, Frédéric Tuong, Frédéric Blanqui - Certified Proofs and Programs - First International Conference - [bibtex]
458. A Framework for Verifying Data-Centric Protocols. Yuxin Deng, Stéphane Grumbach, Jean-François Monin - FMOODS/FORTE 2011 - [bibtex]
459. 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]
460. Improving Strategies via SMT Solving. Thomas Gawlitza, David Monniaux - ESOP - PDF - [bibtex]
461. Faithfulness Considerations for Virtual Prototyping of Systems-on-Chip. Giovanni Funchal, Matthieu Moy, Laurent Maillet-Contoz, Florence Maraninchi - 3rd Workshop on: Rapid Simulation and Performance Evaluation: Methods and Tools (RAPIDO) - PDF - [bibtex]
462. Hybridization Domain Construction using Curvature Estimation. Thao Dang, Romain Testylier - Proceedings HSCC 2011 - PDF - [bibtex]
463. jTLM: an Experimentation Framework for the Simulation of Transaction-Level Models of Systems-on-Chip. Giovanni Funchal, Matthieu Moy - Design, Automation and Test in Europe (DATE) - PDF - [bibtex]
464. Efficient and Playful Tools to Teach Unix to New Students. Matthieu Moy - 16th Annual Conference on Innovation and Technology in Computer Science Education ITiCSE - [bibtex]
465. Information Flow Control of Component-based Distributed Systems. Takoua Abdellatif, Lilia Sfaxi, Riadh Robbana, Yassine Lakhnech - Concurrency and Computation, Practice and Experience - [bibtex]
466. 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]
467. A refinement methodology for object-oriented programs. Asma Tafat, Sylvain Boulmé, Claude Marché - Formal Verification of Object-Oriented Software - [bibtex]
468. Synthesizing Systems with Optimal Average-Case Behavior for Ratio Objectives. Christian von Essen, Barbara Jobstmann - International Workshop on Interactions, Games and Protocols - [bibtex]
469. 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]
470. On Universal Search Strategies for Multi-criteria Optimization Using Weighted Sums. Julien Legriel, Scott Cotton, Oded Maler - CEC - PDF - [bibtex]
471. Meeting Deadlines Cheaply. Julien Legriel, Oded Maler - ECRTS - PDF - [bibtex]
472. SpaceEx: Scalable Verification of Hybrid Systems. Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, Oded Maler - Proc. 23rd International Conference on Computer Aided Verification (CAV) - PDF - [bibtex]
473. Modeling of Time in Discrete-Event Simulation of Systems-on-Chip. Giovanni Funchal, Matthieu Moy - ACM/IEEE Ninth International Conference on Formal Methods and Models for Codesign MEMOCODE - [bibtex]
474. AreaCast : une communication par zone dans les réseaux de capteurs sans fil. Karel Heurtefeux, Florence Maraninchi, Fabrice Valois - 13 èmes Rencontres Francophones sur les Aspects Algorithmiques de Télécommunications (AlgoTel) - PDF - [bibtex]
475. Using bounded model checking to focus fixpoint iterations. David Monniaux, Laure Gonnord - Static analysis (SAS) - PDF - [bibtex]
476. AreaCast: a Cross-Layer Approach for a Communication by Area in Wireless Sensor Networks. Karel Heurtefeux, Florence Maraninchi, Fabrice Valois - 17th IEEE International Conference on networks - [bibtex]
477. Cache related pre-emption delay aware response time analysis for fixed priority pre-emptive systems. Sebastian Altmeyer, Robert I. Davis, Claire Maiza - Proceedings of the 32nd IEEE Real-Time Systems Symposium (RTSS) - [bibtex]
478. A framework for the timing analysis of dynamic branch predictors. Claire Maiza, Christine Rochange - Proceedings of the 19th International Conference on Real-Time and Network Systems (RTNS2011) - PDF - [bibtex]
479. Contract-Based Reasoning for Component Systems with Complex Interactions. Susanne Graf, Roberto Passerone, Sophie Quinton - TIMOBD'11 - [bibtex]
480. 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]
481. 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]
482. Stratified Static Analysis Based on Variable Dependencies. David Monniaux, Julien Le Guen - Third International Workshop on Numerical and Symbolic Abstract Domains - PDF - [bibtex]
483. Modular Abstractions of Reactive Nodes using Disjunctive Invariants. David Monniaux, Martin Bodin - Programming Languages and Systems (APLAS) - PDF - [bibtex]
484. On the Generation of Positivstellensatz Witnesses in Degenerate Cases. David Monniaux, Pierre Corbineau - Interactive Theorem Proving (ITP) - PDF - [bibtex]
485. 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]
486. On Under-Determined Dynamical Systems. Oded Maler - EMSOFT - PDF - [bibtex]
487. Causality closure for a new class of curves in real-time calculus. Karine Altisen, Matthieu Moy - Proceedings of the 1st International Workshop on Worst-Case Traversal Time - [bibtex]
488. Self-Stabilizing Small k-Dominating Sets. Ajoy Kumar Datta, Stéphane Devismes, Karel Heurtefeux, Lawrence L. Larmore, Yvan Rivierre - The Second International Conference on Networking and Computing (ICNC'11) - [bibtex]
489. Sorting on Skip Chains. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore - Proceedings of PDAA'2011, 3rd International Workshop on Parallel and Distributed Algorithms and Applications - [bibtex]
490. Multi-resource Allocation with Unknown Participants.. Ajoy Kumar Datta, Stéphane Devismes, Maria Gradinariu Potop-Butucaru, François Kawala, Lawrence L. Larmore - PDAA'2011, 3rd International Workshop on Parallel and Distributed Algorithms and Applications - [bibtex]
491. Performance Evaluation of Schedulers in a Probabilistic Setting. Jean-Francois Kempf, Marius Bozga, Oded Maler - FORMATS - [bibtex]
492. Efficient Encoding of SystemC/TLM in Promela. Kevin Marquet, Matthieu Moy, Bertrand Jeannet - DATICS-IMECS - [bibtex]
493. 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]
494. 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]
495. 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]
496. 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]
497. 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]
498. 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]
499. 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]
500. 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]
501. A Computational Indistinguishability Logic for the Bounded Storage Model. Gilles Barthe, Mathilde Duclos, Yassine Lakhnech - Foundations and Practice of Security - [bibtex]
502. 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]
503. Monitoring Dynamical Signals While Testing Timed Aspects of a System. Goran Frehse, Kim Guldstrand Larsen, Marius Mikucionis, Brian Nielsen - ICTSS - [bibtex]
504. Snap-Stabilizing Committee Coordination. Borzoo Bonakdarpour, Stéphane Devismes, Franck Petit - IPDPS'2011, 25th IEEE International Parallel and Distributed Processing Symposium - [bibtex]
505. Self-Stabilizing Labeling and Ranking in Ordered Trees. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore, Yvan Rivierre - SSS'2011, 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems - [bibtex]
506. Brief Announcement: Sorting on Skip Chains. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore - SSS'2011, 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems - [bibtex]
507. Algorithme auto-stabilisant construisant un ensemble k-dominant minimal borné. Ajoy Kumar Datta, Stéphane Devismes, Karel Heurtefeux, Lawrence L. Larmore, Yvan Rivierre - 20èmes Rencontres francophones du Parallélisme - PDF - [bibtex]
508. 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]
509. 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]
510. Politiques de gestion de protections pour l'implémentation de sections critiques.. Sifakis Emmanuel, Mounier Laurent - Actes des Rencontres du Parallélisme (RenPar) - [bibtex]
511. 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]
512. Routage par marche aléatoire à listes tabous. Karine Altisen, Stéphane Devismes, Pascal Lafourcade, Clément Ponsonnet - Algotel - [bibtex]
513. Template-Based Unbounded Time Verification of Affine Hybrid Automata. Thao Dang, Thomas Gawlitza - Programming Languages and Systems - 9th Asian Symposium, APLAS 2011, Kenting, Taiwan, December 5-7, 2011. Proceedings - [bibtex]
514. Discretizing Affine Hybrid Automata with Uncertainty. Thao Dang, Thomas Gawlitza - Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings - [bibtex]
515. A Theory of Fault Recovery for Component-Based Models. Borzoo Bonakdarpour, Marius Bozga, Gregor Goessler - 30th IEEE Symposium on Reliable Distributed Systems (SRDS 2011), Madrid, Spain, October 4-7, 2011 - [bibtex]
516. Multi-criteria optimization for mapping programs to multi-processors. Scott Cotton, Oded Maler, Julien Legriel, Selma Saidi - SIES - [bibtex]
517. Coordination de Comités Instantanément Stabilisante. Borzoo Bonakdarpour, Stéphane Devismes, Franck Petit - Algotel - [bibtex]
518. 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]
519. 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]
520. 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]
521. 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]
522. 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]
523. 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]
524. 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]
525. 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]
526. 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]
527. 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]
528. 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]
529. 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]
530. 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]

PhD Thesis and HDR

531. Design, Verification and Implementation of Systems of Components. Sophie Quinton - [bibtex]
532. Component-based Systems: from Design to Implementation. Imene Ben-Hafaiedh - [bibtex]
533. Multi-Criteria Optimization and its Application to Multi-Processor Embedded Systems. Julien Legriel - [bibtex]
534. Contributions to the Transaction-Level Modeling of Systems-on-a-Chip. Giovanni Funchal - [bibtex]
535. Modélisation des systèmes synchrones en BIP. Vassiliki Sfyrla - [bibtex]
536. Modeling Synchronous Systems in BIP. Vasiliki Sfyrla Sfyrla - Theses - [bibtex]

2010

Journal Articles

537. Stabilizing leader election in partial synchronous systems with crash failures. Carole Delporte-Gallet, Stéphane Devismes, Hugues Fauconnier - J. Parallel Distrib. Comput. - [bibtex]
538. Automatic Modular Abstractions for Template Numerical Constraints. David Monniaux - Logical Methods in Computer Science - PDF - [bibtex]
539. Snap-Stabilization in Message-Passing Systems. Sylvie Delaët, Stéphane Devismes, Mikhail Nesterenko, Sébastien Tixeuil - Journal of Parallel and Distributed Computing (JPDC) - [bibtex]
540. Controle de flux d?Information des systemes distribues a base de composants. Takoua Abdellatif, Lilia Sfaxi, Yassine Lakhnech - NOTERE IEEE - [bibtex]
541. On Simulation-Based Probabilistic Model-Checking of Mixed-Analog Circuits. Edmund M. Clarke, Alexandre Donzé, Axel Legay - Formal Methods in System Design - [bibtex]
542. Parameter Synthesis in Nonlinear Dynamical Systems: Application to Systems Biology. Alexandre Donzé, Gilles Clermont, Christopher James Langmead - Journal of Computational Biology - [bibtex]
543. Cache-related Preemption Delay via Useful Cache Blocks: Survey and Redefinition. Sebastian Altmeyer, Claire Maiza - Journal of Systems Architecture - [bibtex]
544. A Self-Stabilizing 3-Approximation for the Maximum Leaf Spanning Tree Problem in Arbitrary Networks. Stéphane Devismes, Hirotsugu Kakugawa, Sayaka Kamei, Sébastien Tixeuil - Journal of Combinatorial Optimization (Special Issue) - [bibtex]
545. Automata-based verification of programs with tree updates. Peter Habermehl, Radu Iosif, Tomás Vojnar - Acta Inf. - [bibtex]
546. Quantitative Separation Logic and Programs with Lists. Marius Bozga, Radu Iosif, Swann Perarnau - J. Autom. Reasoning - [bibtex]
547. Modular static scheduling of synchronous data-flow networks. Marc Pouzet, Pascal Raymond - Design Automation for Embedded Systems - [bibtex]
548. Compositional verification for component-based systems and application. Saddek Bensalem, Marius Bozga, Thanh-Hung Nguyen, Joseph Sifakis - IET Software - [bibtex]
549. Source-to-Source Architecture Transformation for Performance Optimization in BIP. Marius Bozga, Mohamad Jaber, Joseph Sifakis - IEEE Trans. Industrial Informatics - [bibtex]
550. 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]
551. Causal semantics for the algebra of connectors. Simon Bliudze, Joseph Sifakis - Formal Methods in System Design - [bibtex]
552. 2009 CAV award announcement. Randal E. Bryant, Orna Grumberg, Joseph Sifakis, Moshe Y. Vardi - Formal Methods in System Design - [bibtex]

Conference Articles

553. An analysis of permutations in arrays. Valentin Perrelle, Nicolas Halbwachs - 11th International Conference on Verification, Model-checking, and Abstract Interpretation, VMCAI 2010 - [bibtex]
554. 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]
555. Performance Evaluation of Components Using a Granularity-based Interface Between Real-Time Calculus and Timed Automata. Karine Altisen, Yanhong Liu, Matthieu Moy - Eighth Workshop on Quantitative Aspects of Programming Languages (QAPL) - [bibtex]
556. Algorithms For Extracting Timeliness Graphs. Stéphane Devismes, Carole Delporte-Gallet, Hugues Fauconnier, Mikel Larrea - 17th International Colloquium on Structural Information and Communication Complexity (SIROCCO 2010) - [bibtex]
557. A Theoretical and Experimental Review of SystemC Front-ends. Kevin Marquet, Matthieu Moy, Bageshri Karkare - Forum for Design Languages (FDL) - [bibtex]
558. A Self-Stabilizing 3-Approximation for the Maximum Leaf Spanning Tree Problem in Arbitrary Networks. Stéphane Devismes, Hirotsugu Kakugawa, Sayaka Kamei, Sébastien Tixeuil - COCOON 2010, The 16th Annual International Computing and Combinatorics Conference - [bibtex]
559. 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]
560. Designing Log Architecture For Legal Evidence. Daniel Le Métayer, Eduardo Mazza, Marie-Laure Potet - Software Engineering And Formal Methods (SEFM) - [bibtex]
561. 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]
562. 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]
563. 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]
564. 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]
565. A Unifying View Of Loosely Time-Triggered Architectures. Albert Benveniste, Anne Bouillard, Paul Caspi - International Conference on Embedded Software International Conference on Embedded Software - [bibtex]
566. Approximation of $\delta$-timeliness. Carole Delporte-Gallet, Stéphane Devismes, Hugues Fauconnier - 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2010) - [bibtex]
567. Communications Efficaces et Auto-Stabilisation. Stéphane Devismes, Toshimitsu Masuzawa, Sébastien Tixeuil - 12èmes Rencontres Francophones sur les Aspects Algorithmiques de Télécommunications (Algotel 2010) - [bibtex]
568. 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]
569. 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]
570. Contract-Based Reasoning about Progress: Application to Resource Sharing in a Network. Imene Ben-Hafaiedh, Susanne Graf, Sophie Quinton - Proc. of FLACOS'10 - [bibtex]
571. 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]
572. 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]
573. 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]
574. ac2lus: Bringing SMT-solving and Abstract Interpretation Techniques to Real-Time Calculus through the Synchronous Language Lustre. Karine Altisen, Matthieu Moy - 22nd Euromicro Conference on Real-Time Systems (ECRTS) - PDF - [bibtex]
575. Property-Based Monitoring of Analog and Mixed-Signal Systems. John Havlicek, Scott Little, Oded Maler, Dejan Nickovic - Formal Modeling and Analysis of Timed Systems - 8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings - [bibtex]
576. On the Krohn-Rhodes Cascaded Decomposition Theorem. Oded Maler - Time for Verification, Essays in Memory of Amir Pnueli - PDF - [bibtex]
577. Robust Satisfaction of Temporal Logic over Real-Valued Signals. Alexandre Donzé, Oded Maler - Formal Modeling and Analysis of Timed Systems - 8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings - PDF - [bibtex]
578. Amir Pnueli and the dawn of hybrid systems. Oded Maler - Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010 - PDF - [bibtex]
579. On Zone-Based Analysis of Duration Probabilistic Automata. Oded Maler, Kim Guldstrand Larsen, Bruce H. Krogh - Proceedings 12th International Workshop on Verification of Infinite-State Systems - PDF - [bibtex]
580. Using Redundant Constraints for Refinement. Eugene Asarin, Thao Dang, Oded Maler, Romain Testylier - Automated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings - [bibtex]
581. Computational indistinguishability logic. Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech - ACM Conference on Computer and Communications Security - [bibtex]
582. Approximating the Pareto Front of Multi-criteria Optimization Problems. Julien Legriel, Colas Le Guernic, Scott Cotton, Oded Maler - Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2 - PDF - [bibtex]
583. 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]
584. Probabilistic Self-Stabilizing Vertex Coloring in Unidirectional Anonymous Networks. Samuel Bernard, Stéphane Devismes, Maria Gradinariu Potop-Butucaru, Katy Paroux, Sébastien Tixeuil - ICDCN'2010, 11th International Conference on Distributed Computing and Networking - [bibtex]
585. Accurate hybridization of nonlinear systems. Thao Dang, Oded Maler, Romain Testylier - Proceedings of HSCC 2010 - PDF - [bibtex]
586. Proof Trick: Small Inversions. Jean-François Monin - Second Coq Workshop - [bibtex]
587. Quantifier elimination by lazy model enumeration. David Monniaux - Computer-aided verification (CAV) - PDF - [bibtex]
588. Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems. Alexandre Donzé - CAV - [bibtex]
589. Resilience Analysis: Tightening the CRPD Bound for Set-Associative Caches. Sebastian Altmeyer, Claire Maiza, Jan Reineke - LCTES '10: Proceedings of the ACM SIGPLAN/SIGBED 2010 conference on Languages, compilers, and tools for embedded systems - [bibtex]
590. Static Timing Analysis for Hard Real-Time Systems. Reinhard Wilhelm, Sebastian Altmeyer, Claire Maiza-Burguière, Daniel Grund, Joerg Herter, Jan Reineke, Bjoern Wachter, Stephan Wilhelm - VMCAI - [bibtex]
591. Influence of the Task Model on the Precision of Scheduling Analysis for Preemptive Systems. Sebastian Altmeyer, Claire Maiza-Burguière - Proceedings of the 1st International Real-Time Scheduling Open Problems Seminar - [bibtex]
592. Optimal Exploration of Small Rings. Stéphane Devismes - WRAS'2010, Third International ACM SIGOPS/SIGACT Workshop on Reliability, Availability, and Security - [bibtex]
593. 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]
594. 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]
595. 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]
596. PinaVM: a SystemC Front-End Based on an Executable Intermediate Representation. Kevin Marquet, Matthieu Moy - International Conference on Embedded Software - [bibtex]
597. 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]
598. Fast Acceleration of Ultimately Periodic Relations. Marius Bozga, Radu Iosif, Filip Konecn\'y - Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings - [bibtex]
599. 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]
600. 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]
601. Rendez-vous d'agents amnésiques. Fabienne Carrier, Stéphane Devismes, Franck Petit, Yvan Rivierre - 12èmes Rencontres Francophones sur les Aspects Algorithmiques de Télécommunications (Algotel 2010) - [bibtex]
602. 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]
603. Methods for Knowledge Based Controlling of Distributed Systems. Saddek Bensalem, Marius Bozga, Susanne Graf, Doron Peled, Sophie Quinton - Automated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings - [bibtex]
604. 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]
605. Statistical Abstraction and Model-Checking of Large Heterogeneous Systems. Ananda Basu, Saddek Bensalem, Marius Bozga, Benoît Caillaud, Benoît Delahaye, Axel Legay - Formal Techniques for Distributed Systems, Joint 12th IFIP WG 6.1 International Conference, FMOODS 2010 and 30th IFIP WG 6.1 International Conference, FORTE 2010, Amsterdam, The Netherlands, June 7-9, - [bibtex]
606. 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]
607. 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]
608. 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]
609. 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]
610. 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]
611. Knowledge Based Scheduling of Distributed Systems. Saddek Bensalem, Doron Peled, Joseph Sifakis - Time for Verification, Essays in Memory of Amir Pnueli - [bibtex]
612. 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]
613. Component-based Construction of Heterogeneous Real-time Systems in BIP. Joseph Sifakis - The Future of Software Engineering - [bibtex]
614. 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]
615. 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]
616. Arrival Curves for Real-Time Calculus: the Causality Problem and its Solutions. Karine Altisen, Matthieu Moy - TACAS - [bibtex]

PhD Thesis and HDR

617. 42, A Component-Based Approach to Virtual Prototyping of Heterogeneous Embedded Systems. Tayeb Bouhadiba - PDF - [bibtex]
618. Contributions à l'analyse statique de programmes manipulant des tableaux. Mathias Péron - PDF - [bibtex]
619. Constructive Verification for Component-based Systems. Thanh-Hung Nguyen - [bibtex]
620. Automatisation de la Certification Formelle de Systèmes Critiques par Instrumentation d'Interpréteurs Abstraits. Manuel Garnacho - [bibtex]
621. 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]
622. 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]
623. Component-Based Design of Real-Time Systems (HDR). Marius Bozga - [bibtex]
624. Modelling real-time embedded systems using AADL for the automatic generation of applications formally verified. Mohamed Yassin Chkouri - Theses - [bibtex]
625. Centralized and Distributed Implementations of Correct-by-construction Component-based Systems by using Source-to-source Transformations in BIP. Mohamad Jaber - Theses - [bibtex]
626. Constructive Verification for Component-based Systems. Thanh-Hung Nguyen - Theses - [bibtex]
627. Design and Implementation of Component Based Systems. Towards a Unification of the Software Engineering and the System Paradigms.. Marc Poulhiès - Theses - [bibtex]

2009

Journal Articles

628. Full Simulation Coverage for SystemC Transaction-Level Models of Systems-on-a-Chip. Claude Helmstetter, Florence Maraninchi, Laurent Maillet-Contoz - Formal Methods in System Design - [bibtex]
629. Coverage-Guided Test Generation for Continuous and Hybrid Systems. Thao Dang, Tarik Nahhal - Formal Methods in System Design - [bibtex]
630. Flush: an example of development by refinements in SCADE/Lustre. Jan Mikác, Paul Caspi - International Journal on Software Tools for Technology Transfer (STTT) - [bibtex]
631. 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]
632. A minimalistic look at widening operators. David Monniaux - Higher order and symbolic computation - PDF - [bibtex]
633. Flat Parametric Counter Automata. Marius Bozga, Radu Iosif, Yassine Lakhnech - Fundam. Inform. - [bibtex]
634. Convincing Proofs for Program Certification. Manuel Garnacho, Michaël Périn - Electronic Notes in Theoretical Computer Science - [bibtex]
635. Light enabling snap-stabilization of fundamental protocols. Alain Cournier, Stéphane Devismes, Vincent Villain - TAAS, ACM Transactions on Autonomous and Adaptive Systems - [bibtex]
636. 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]
637. Model checking: algorithmic verification and debugging. Edmund M. Clarke, Allen Emerson, Joseph Sifakis - Commun. ACM - [bibtex]
638. 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 - Génie logiciel - [bibtex]

Book Chapters (inbook)

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

Book Chapters

640. 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]
641. Tools for the verification of linear hybrid automata models. Goran Frehse - Handbook of Hybrid Systems Control, Theory -- Tools -- Applications - [bibtex]

Conference Articles

642. 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]
643. 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]
644. Automatic Verification of Integer Array Programs. Marius Bozga, Peter Habermehl, Radu Iosif, Filip Konecn\'y, Tomás Vojnar - Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings - [bibtex]
645. Verifying self-stabilizing population protocols with Coq. Yuxin Deng, Jean-François Monin - 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering - [bibtex]
646. 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]
647. Contract-Based Coordination of Hardware Components for the Development of Embedded Software. Tayeb Bouhadiba, Florence Maraninchi - COORDINATION'09, the 11th international conference on Coordination Models and Languages - [bibtex]
648. Formal and Executable Contracts for Transaction-Level Modeling in SystemC. Tayeb Bouhadiba, Florence Maraninchi, Giovanni Funchal - ACM International Conference on Embedded Sofware (EMSOFT 09) - [bibtex]
649. 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]
650. Model-Based Design of Embeded Control Systems with a Synchronous Intermediate Model. Mouaiad Alras, Paul Caspi, Alain Girault, Pascal Raymond - 6th IEEE International Conference on Embedded Systems and Software (ICESS-09) - [bibtex]
651. Volume and Entropy of Regular Timed Languages: Discretization Approach. Eugene Asarin, Aldric Degorre - CONCUR - [bibtex]
652. Sur le Coloriage Auto-stabilisant dans les Réseaux Unidirectionnels Anonymes. Samuel Bernard, Stéphane Devismes, Katy Paroux, Maria Gradinariu Potop-Butucaru, Sébastien Tixeuil - AlgoTel'09 - [bibtex]
653. 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]
654. Using Checker Predicates in Certifying Code Generation. Jan Olaf Blech, Benjamin Grégoire - Workshop on Compiler Optimization meets Compiler Verification (COCV) - [bibtex]
655. Invariants and Robustness of BIP Models. Jan Olaf Blech, Thanh-Hung Nguyen, Michaël Périn - Workshop on Invariant Generation (WING) - [bibtex]
656. Certifying Deadlock-freedom for BIP Models. Jan Olaf Blech, Michaël Périn - Software and Compilers for Embedded Systems (SCOPES) - [bibtex]
657. Evaluating Design Trade-offs in Customizable Processors. Unmesh D. Bordoloi, Huynh Phung Huynh, Samarjit Chakraborty, Tulika Mitra - 46th Annual ACM IEEE Design Automation Conference - [bibtex]
658. Designing Heterogeneous ECU Networks via Compact Architecture Encoding and Hybrid Timing Analysis. Michael Glaß, Martin Lukasiewycz, Jürgen Teich, Unmesh D. Bordoloi, Samarjit Chakraborty - 46th Annual ACM IEEE Design Automation Conference - [bibtex]
659. A DECOMSYS Based Tool-Chain for Analyzing FlexRay based Automotive Control Applications. Dip Goswami, Pradeep Seshadri, Unmesh D. Bordoloi, Samarjit Chakraborty - IEEE Conference on Automation Science and Engineering -(CASE) - [bibtex]
660. Space-Optimal Deterministic Rendezvous. Fabienne Carrier, Stéphane Devismes, Franck Petit, Yvan Rivierre - WRAS'09, Second International Workshop on Reliability, Availability, and Security (associated with PDCAT'09) - [bibtex]
661. Comparing State Spaces in Automatic Protocol Analysis. Cas J. F. Cremers, Pascal Lafourcade, Philippe Nadeau - Formal to Practical Security - [bibtex]
662. Image computation for polynomial dynamical systems using the Bernstein expansion. Thao Dang, David Salinas - Computer Aided Verification CAV'09 - [bibtex]
663. Quand le consensus est plus simple que la diffusion fiable. Carole Delporte-Gallet, Stéphane Devismes, Hugues Fauconnier, Franck Petit, Sam Toueg - AlgoTel'09 - [bibtex]
664. Self-Stabilizing k-out-of-l exclusion on tree networks. Ajoy Kumar Datta, Stéphane Devismes, Florian Horn, Lawrence L. Larmore - IPDPS'09, International Conference on Parallel and Distributed Processing Symposium - [bibtex]
665. A Self-Stabilizing O(n)-Round k-Clustering Algorithm. Ajoy Kumar Datta, Stéphane Devismes, Lawrence L. Larmore - SRDS'09, 28th International Symposium on Reliable Distributed Systems - [bibtex]
666. Snap-Stabilization in Message-Passing Systems. Sylvie Delaët, Stéphane Devismes, Mikhail Nesterenko, Sébastien Tixeuil - ICDCN, 10th International Conference on Distributed Computing and Networking - [bibtex]
667. Stabilisation instantanée dans les systèmes à passage de messages. Sylvie Delaët, Stéphane Devismes, Mikhail Nesterenko, Sébastien Tixeuil - AlgoTel'09 - [bibtex]
668. Communication Efficiency in Self-Stabilizing Silent Protocols. Stéphane Devismes, Toshimitsu Masuzawa, Sébastien Tixeuil - ICDCS'09, International Conference on Distributed Computing Systems - [bibtex]
669. Parameter synthesis for hybrid systems with an application to simulink models. Alexandre Donzé, Bruce H. Krogh, Akshay Rajhans - Proceedings of the 12th International Conference on Hybrid Systems: Computation and Control (HSCC'09) - [bibtex]
670. Parameter Synthesis in Nonlinear Dynamical Systems: Application to Systems Biology. Alexandre Donzé, Gilles Clermont, Christopher James Langmead, Axel Legay - Proceedings of the 13th Annual International Conference on Research in Computational Molecular Biology RECOMB'09 - [bibtex]
671. Optimal Probabilistic Ring Exploration by Semi-synchronous Oblivious Robots. Stéphane Devismes, Franck Petit, Sébastien Tixeuil - Structural Information and Communication Complexity, 16th International Colloquium, SIROCCO 2009 - [bibtex]
672. Exploration Optimale Probabiliste d'un Anneau par des Robots Semi-Synchrones et Amnésiques. Stéphane Devismes, Franck Petit, Sébastien Tixeuil - AlgoTel'09 - [bibtex]
673. Synchronous Modeling and Validation of Priority Inheritance Schedulers. Erwan Jahier, Nicolas Halbwachs, Pascal Raymond - Fundamental Approaches to Software Engineering, FASE'09 - [bibtex]
674. Modular Static Scheduling of Synchronous Data-flow Networks -- An efficient symbolic representation. Marc Pouzet, Pascal Raymond - International Conference on Embedded Software (EMSOFT'09) - [bibtex]
675. Runtime Verification of Safety Progress Properties. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier - Runtime Verification 2009 - [bibtex]
676. 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]
677. Automated Proofs for Encryption Modes. Martin Gagne, Pascal Lafourcade, Yassine Lakhnech, Reihaneh Safavi - Workshop on Formal and Computational Cryptography, (FCC'09) - [bibtex]
678. Actors without directors: A Kahnian view of heterogeneous systems. Paul Caspi, Albert Benveniste, Roberto Lublinerman, Stavros Tripakis - Hybrid Systems Computation and Control, HSCC09 - [bibtex]
679. Reachability Analysis of Hybrid Systems using Support Functions. Colas Le Guernic, Antoine Girard - CAV - [bibtex]
680. 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]
681. Polyhedral Domains and Widening for Verification of Numerical Programs. Hitashyam Maka, Goran Frehse, Bruce H. Krogh - NSV-II: Second International Workshop on Numerical Software Verification - [bibtex]
682. Prudent engineering practices to prevent type-flaw attacks under algebraic properties. Sreekanth Malladi, Pascal Lafourcade - Workshop on Security and Rewriting Techniques, (SecReT'09) - [bibtex]
683. Synchronous Objects with Scheduling Policies, Introducing safe shared memory in Lustre. Paul Caspi, Jean-louis Colaço, Léonard Gérard, Marc Pouzet, Pascal Raymond - ACM SIGPLAN/SIGBED 2009 Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2009) - [bibtex]
684. 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]
685. Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form. Loïc Besnard, Thierry Gautier, Matthieu Moy, Jean-Pierre Talpin, Kenneth Johnson, Florence Maraninchi - Ninth International Workshop on Automated Verification of Critical Systems (AVOCS'09) - [bibtex]
686. From Orchestration to Choreography: Memoryless and Distributed Orchestrators. Sophie Quinton, Imene Ben-Hafaiedh, Susanne Graf - Proc. of FLACOS'09 - [bibtex]
687. 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]
688. Reachability for Continuous and Hybrid Systems. Oded Maler - Reachability Problems, 3rd International Workshop, RP 2009, Palaiseau, France, September 23-25, 2009. Proceedings - [bibtex]
689. On Omega-Languages Defined by Mean-Payoff Conditions. Rajeev Alur, Aldric Degorre, Oded Maler, Gera Weiss - FOSSACS - PDF - [bibtex]
690. Computing Reachable States for Nonlinear Biological Models. Thao Dang, Colas Le Guernic, Oded Maler - Computational Methods in Systems Biology, 7th International Conference, CMSB 2009, Bologna, Italy, August 31-September 1, 2009. Proceedings - [bibtex]
691. Design Principles for an Extendable Verification Tool for Hybrid Systems. Goran Frehse, Rajarshi Ray - Proceedings of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2009) - [bibtex]
692. 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]
693. A New Notion of Useful Cache Block to Improve the Bounds of Cache-Related Preemption Delay. Sebastian Altmeyer, Claire Maiza-Burguière - Proceedings of the 21st Euromicro Conference on Real-Time Systems (ECRTS '09) - [bibtex]
694. Cache-Related Preemption Delay Computation for Set-Associative Caches---Pitfalls and Solutions. Claire Maiza-Burguière, Jan Reineke, Sebastian Altmeyer - Proceedings of 9th International Workshop on Worst-Case Execution Time (WCET) Analysis - [bibtex]
695. Computing the Maximum Blocking Time for Scheduling with Deferred Preemption. Sebastian Altmeyer, Claire Maiza-Burguière, Reinhard Wilhelm - Workshop on Software Technologies for Future Dependable Distributed Systems - [bibtex]
696. Optimal deterministic self-stabilizing vertex coloring in unidirectional anonymous networks. Samuel Bernard, Stéphane Devismes, Maria Gradinariu Potop-Butucaru, Sébastien Tixeuil - IPDPS '09: Proceedings of the 2009 IEEE International Symposium on Parallel&Distributed Processing - [bibtex]
697. On using floating-point computations to help an exact linear arithmetic decision procedure. David Monniaux - Computer-aided verification (CAV) - PDF - [bibtex]
698. Automatic Modular Abstractions for Linear Constraints. David Monniaux - POPL (Principles of programming languages) - PDF - [bibtex]
699. Compositional Timing Analysis. Ramzi Ben Salah, Marius Bozga, Oded Maler - EMSOFT - [bibtex]
700. 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]
701. "Certfication of Smart-Card Applications in Common Criteria: Proving Representation Correspondences". Iman Narasamdya, Michaël Périn - Fundamental Approaches to Software Engineering - [bibtex]
702. "Certfication of Smart-Card Applications in Common Criteria". Iman Narasamdya, Michaël Périn - ACM Symposium on Applied Computing - [bibtex]
703. 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]
704. 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]
705. Instantaneous Soundness Checking of Industrial Business Process Models. Dirk Fahland, Cédric Favre, Barbara Jobstmann, Jana Koehler, Niels Lohmann, Hagen Volzer, Karsten Wolf - Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8-10, 2009. Proceedings - [bibtex]
706. 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]
707. Volume and Entropy of Regular Timed Languages: Analytic Approach. Eugene Asarin, Aldric Degorre - FORMATS - [bibtex]
708. 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]
709. 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]
710. 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]
711. 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]
712. Prototyping of Distributed Embedded Systems Using AADL. Mohamed Yassin Chkouri, Marius Bozga - Model Based Architecting and Construction of Embedded Systems ACES-MB - [bibtex]
713. 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]
714. 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]
715. 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]
716. 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]

PhD Thesis and HDR

717. On Some Problems in Satisfiability Solving. Scott Cotton - [bibtex]
718. Study and Implementation of Runtime Validation Techniques. Ylies Falcone - [bibtex]
719. Analyse statique : de la théorie à la pratique. David Monniaux - Habilitation to direct research - [bibtex]
720. Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics. Colas Le Guernic - [bibtex]
721. On some Quantitative Aspects of Formal Languages. Aldric Degorre - [bibtex]

2008

Journal Articles

722. Secure Neighborhood Discovery: A Fundamental Element for Mobile Ad Hoc Networking. Panos Papadimitratos, Marcin Poturalski, Patrick Schaller, Pascal Lafourcade, David Basin, Srdjan \vCapkun, Jean-Pierre Hubaux - IEEE Communications Magazine - [bibtex]
723. Symbolic protocol analysis for monoidal equational theories. Stéphanie Delaune, Pascal Lafourcade, Denis Lugiez, Ralf Treinen - Information and Computation - [bibtex]
724. PHAVer: Algorithmic Verification of Hybrid Systems past HyTech. Goran Frehse - International Journal on Software Tools for Technology Transfer - [bibtex]
725. Implementing synchronous models on Loosely Time-Triggered Architectures. Stavros Tripakis, Claudio Pinello, Albert Benveniste, Alberto L. Sangiovanni-Vincentelli, Paul Caspi, Marco Di Natale - IEEE trans. on Computers - [bibtex]
726. The pitfalls of verifying floating-point computations. David Monniaux - TOPLAS - [bibtex]
727. Formal Analysis Tools for the Synchronous Aspect Language Larissa. David Stauch - EURASIP Journal on Embedded Systems - [bibtex]
728. Semantic-preserving multitask implementation of synchronous programs. Paul Caspi, Norman Scaife, Christos Sofronis, Stavros Tripakis - ACM Trans. Embedded Computing Systems - [bibtex]
729. OMEGA -- Correct development of Real Time Embedded Systems. Susanne Graf - SoSyM, int. Journal on Software & Systems Modelling - [bibtex]
730. 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]
731. Lutin: a language for specifying and executing reactive scenarios. Pascal Raymond, Yvan Roux, Erwan Jahier - EURASIP Journal on Embedded Systems - [bibtex]
732. Automatic generation of path conditions for concurrent timed systems. Saddek Bensalem, Doron Peled, Hongyang Qu, Stavros Tripakis - Theor. Comput. Sci. - [bibtex]
733. Symbolic quality control for multimedia applications. Jacques Combaz, Jean-Claude Fernandez, Joseph Sifakis, Loïc Strus - Real-Time Systems - [bibtex]
734. The Algebra of Connectors - Structuring Interaction in BIP. Simon Bliudze, Joseph Sifakis - IEEE Trans. Computers - [bibtex]

Book Chapters

735. Programmation. Jean-François Monin - [bibtex]
736. Synchronous Program Verification with Lustre/Lesar. Pascal Raymond - Modeling and Verification of Real-Time Systems - [bibtex]
737. 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

738. 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]
739. Time-robust discrete control over networked Loosely Time-Triggered Architectures. Paul Caspi, Albert Benveniste - IEEE Decision and Control Conference, Cancun, December - [bibtex]
740. 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]
741. 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]
742. 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]
743. A Model Transformation Tool for Performance Simulation of Complex UML Models. Olivier Constant, Wei Monin, Susanne Graf - ICSE 2008, tool track - [bibtex]
744. Sensitive State Space Exploration. Thao Dang, Alexandre Donzé, Oded Maler, Noa Shalev - IEEE Conference on Decision and Control (CDC) - [bibtex]
745. Outils pour l'analyse des modèles hybrides. Thao Dang, Goran Frehse, Antoine Girard, Colas Le Guernic - Approches formelles des systèmes embarqué communicants - [bibtex]
746. Using Disparity to Enhance Test Generation for Hybrid Systems. Thao Dang, Tarik Nahhal - TestCom/FATES 2008 - [bibtex]
747. Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Delta-Sigma Modulator. Edmund M. Clarke, Alexandre Donzé, Axel Legay - Haifa Verification Conference - [bibtex]
748. 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]
749. Election Robuste, Auto-Stabilisante et Efficace. Carole Delporte-Gallet, Stéphane Devismes, Hugues Fauconnier - Algotel'08 - [bibtex]
750. With Finite Memory Consensus Is Easier Than Reliable Broadcast. Carole Delporte-Gallet, Stéphane Devismes, Hugues Fauconnier, Franck Petit, Sam Toueg - OPODIS'09, 12th International Conference On Principles of DIstributed Systems - [bibtex]
751. K-parmi-L exclusion auto-stabilisante. Ajoy Kumar Datta, Stéphane Devismes, Florian Horn, Lawrence L. Larmore - Algotel'08 - [bibtex]
752. Snap-stabilization in message-passing systems. Sylvie Delaët, Stéphane Devismes, Mikhail Nesterenko, Sébastien Tixeuil - PODC'08, the Twenty-Seventh Annual ACM Symposium on Principles of Distributed Computing - [bibtex]
753. On Scheduling Policies for Streams of Structured Jobs. Aldric Degorre, Oded Maler - FORMATS - [bibtex]
754. Weak vs. Self vs. Probabilistic Stabilization. Stéphane Devismes, Sébastien Tixeuil, Masafumi Yamashita - ICDCS'08, 28th IEEE International Conference on Distributed Computing Systems - [bibtex]
755. 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]
756. Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier - International Conference of Information System Security - [bibtex]
757. A Counterexample-Guided Approach to Parameter Synthesis for Linear Hybrid Automata. Goran Frehse, Sumit Kumar Jha, Bruce H. Krogh - HSCC - [bibtex]
758. Zonotope/Hyperplane Intersection for Hybrid Systems Reachability Analysis. Antoine Girard, Colas Le Guernic - HSCC - [bibtex]
759. Efficient Reachability Analysis for Linear Systems Using Support Functions. Antoine Girard, Colas Le Guernic - IFAC World Congress - [bibtex]
760. On the timed automata-based verification of Ravenscar systems. Ileana Ober, Nicolas Halbwachs - 13th International Conference on Reliable Software Technologies - Ada-Europe 2008 - [bibtex]
761. Control software model checking using bisimulation functions for nonlinear systems. James Patrick Kapinski, Flavio Lerda, Alexandre Donzé, Bruce H. Krogh, Hitashyam Maka, Silke Wagner - Proceedings of the 47th IEEE Conference on Decision and Control (CDC'08) - [bibtex]
762. 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]
763. Approximating Continuous Systems by Timed Automata. Oded Maler, Grégory Batt - FMSB - [bibtex]
764. Combination of Abstractions in the ASTRÉE Static Analyzer. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival - Advances in Computer Science --- ASIAN 2006. Secure Software and Related Issues - [bibtex]
765. Discovering Properties about Arrays in Simple Programs. Nicolas Halbwachs, Mathias Péron - ACM Conference on Programming Language Design and Implementation, PLDI 2008 - [bibtex]
766. A Method for the Efficient Development of Timed and Untimed Transaction-Level Models of Systems-on-Chip. Jérôme Cornet, Florence Maraninchi, Laurent Maillet-Contoz - Design Automation and Test in Europe (DATE) - [bibtex]
767. 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]
768. 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]
769. 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]
770. A Policy Iteration Technique for Time Elapse over Template Polyhedra. Sriram Sankaranarayanan, Thao Dang, Franjo Ivancic - Hybrid Systems: Computation and Control HSCC'08 - [bibtex]
771. Symbolic Model Checking of Hybrid Systems Using Template Polyhedra. Sriram Sankaranarayanan, Thao Dang, Franjo Ivancic - TACAS'08 - [bibtex]
772. SystemC/TLM Semantics for Heterogeneous System-on-Chip Validation. Florence Maraninchi, Matthieu Moy, Jérôme Cornet, Laurent Maillet-Contoz, Claude Helmstetter, Claus Traulsen - 2008 Joint IEEE-NEWCAS and TAISA Conference - [bibtex]
773. Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. Oded Maler, Dejan Nickovic, Amir Pnueli - Pillars of Computer Science - PDF - [bibtex]
774. A Quantifier Elimination Algorithm for Linear Real Arithmetic. David Monniaux - LPAR (Logic for Programming Artificial Intelligence and Reasoning) - PDF - [bibtex]
775. 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]
776. 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]
777. 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]
778. 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]
779. 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]
780. 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]
781. 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]
782. 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]
783. 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]
784. 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]
785. 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]
786. 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]
787. 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]
788. 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]
789. 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]
790. 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]
791. Specification and Verification of Conurrent Systems in Cesar. Jean-Pierre Queille, Joseph Sifakis - 25 Years of Model Checking - History, Achievements, Perspectives - [bibtex]

PhD Thesis and HDR

792. Component-based modeling of heterogeneous real time systems in BIP. Ananda Basu - [bibtex]
793. Separation of Functional and Non-Functional Aspects in Transactional Level Models of Systems-on-Chip. Jérôme Cornet - [bibtex]
794. Models and Methods for the Construction and Verification of Complex Reactive Systems. Susanne Graf - Habilitation à diriger des recherches - [bibtex]
795. Checking Timed and Hybrid Properties: Theory and Applications. Dejan Nickovic - [bibtex]
796. Synthèse de gestionnaires mémoire pour applications Java temps-réel embarquées. Guillaume Salagnac - [bibtex]
797. Modélisations et analyses de réseaux de capteurs. Ludovic Samper - [bibtex]
798. Contrôle de qualité de service optimal d'application multimédia. Loïc Strus - [bibtex]
799. Le débogage de code optimisé dans le contexte des systèmes embarqués. Hugo Venturini - [bibtex]
800. Modeliser la prediction de branchement pour le calcul de temps d'execution pire-cas. Claire Maiza-Burguière - [bibtex]
801. Component-based Modeling of Heterogeneous Real-time Systems in BIP. Ananda Basu - Theses - [bibtex]

2007

Journal Articles

802. Hybridization methods for the analysis of nonlinear systems. Eugene Asarin, Thao Dang, Antoine Girard - Acta Inf. - [bibtex]
803. Software and architecture modelling with Omega-UML and validation with IF. Susanne Graf, Iulian Ober - Génie Logiciel - [bibtex]
804. Intruder Deduction for the Equational Theory of Exclusive-or with Commutative and Distributive Encryption. Pascal Lafourcade - Proceedings of the 1st International Workshop on Security and Rewriting Techniques (SecReT'06) - Electronic Notes in Theoretical Computer Science - [bibtex]
805. Intruder Deduction for the Equational Theory of Abelian Groups with Distributive Encryption. Pascal Lafourcade, Denis Lugiez, Ralf Treinen - Information and Computation - [bibtex]
806. On optimal and reasonable control in the presence of adversaries. Oded Maler - Annual Reviews in Control - [bibtex]
807. Time in Abstract State Machines. Susanne Graf, Andreas Prinz - Fundamentae Informaticae, Special issue on ASM 2005 - [bibtex]
808. 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]
809. The Discipline of Embedded Systems Design. Thomas A. Henzinger, Joseph Sifakis - IEEE Computer - [bibtex]

Book Chapters

810. Proving Termination Using Dependent Types: the Case of Xor-Terms. Jean-François Monin, Judicaël Courant - Trends in Functional Programming 7 - [bibtex]
811. Synchronous languages. Paul Caspi, Pascal Raymond, Stavros Tripakis - Handbook of Real-Time And Embedded Systems - [bibtex]
812. Lucid synchrone: un langage pour la programmation des systèmes réactifs. Paul Caspi, Grégoire Hamon, Marc Pouzet - Systèmes temps réel - [bibtex]
813. Synchronous Programming. Paul Caspi, Pascal Raymond, Stavros Tripakis - Handbook of Real-Time amd Embedded Systems - [bibtex]
814. Generating Random Values Using Binary Decision Diagrams and Convex Polyhedra. Erwan Jahier, Pascal Raymond - Trends in Constraint Programming - [bibtex]

Conference Articles

815. 42: Programmable Models of Computation for a Component-Based Approach to Heterogeneous Embedded Systems. Florence Maraninchi, Tayeb Bouhadiba - Sixth ACM International Conference on Generative Programming and Component Engineering (GPCE'07) - [bibtex]
816. Sensor Minimization Problems with Static or Dynamic Observers for Fault Diagnosis. Franck Cassez, Stavros Tripakis, Karine Altisen - ACSD '07: Proceedings of the Seventh International Conference on Application of Concurrency to System Design - [bibtex]
817. 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]
818. 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]
819. On Synthesizing Controllers from Bounded-Response Properties. Oded Maler, Dejan Nickovic, Amir Pnueli - CAV - [bibtex]
820. Test Coverage for Continuous and Hybrid Systems. Tarik Nahhal, Thao Dang - CAV - [bibtex]
821. On Timed Models of Gene Networks. Grégory Batt, Ramzi Ben Salah, Oded Maler - FORMATS - [bibtex]
822. AMT: A Property-Based Monitoring Tool for Analog Systems. Dejan Nickovic, Oded Maler - FORMATS - [bibtex]
823. 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]
824. Reachability Analysis of a Switched Buffer Network. Goran Frehse, Oded Maler - HSCC - [bibtex]
825. Guided Randomized Simulation. Tarik Nahhal, Thao Dang - HSCC - [bibtex]
826. Robust Stabilizing Leader Election. Carole Delporte-Gallet, Stéphane Devismes, Hugues Fauconnier - SSS'07, 9th International Symposium on Stabilization, Safety, and Security of Distributed Systems - [bibtex]
827. Systematic Simulation Using Sensitivity Analysis. Alexandre Donzé, Oded Maler - HSCC - [bibtex]
828. Loosely Time-Triggered Architectures based on Communication by Sampling. Albert Benveniste, Paul Caspi, Marco Di Natale, Claudio Pinello, Alberto L. Sangiovanni-Vincentelli, Stavros Tripakis - 7th Intl. Conf. on Embedded Software (EMSOFT'06) - [bibtex]
829. A Compositional Testing Framework Driven by Partial Specifications. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier, Jean-Luc Richier - TESTCOM/FATES - [bibtex]
830. Contracts for BIP: hierarchical interaction models for compositional verification. Susanne Graf, Sophie Quinton - FORTE 2007, Talinn - [bibtex]
831. Larissa, un langage d'aspects pour le développement des systèmes réactifs sûrs. David Stauch, Karine Altisen, Florence Maraninchi - 3èmes Journées Francophones sur le Développement de Logiciels par Aspects - [bibtex]
832. Test Generation from Security Policies Specified in Or-BAC. Keqin Li, Laurent Mounier, Roland Groz - IEEE COMPSAC'07 - [bibtex]
833. 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]
834. 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]
835. Verification of Device Drivers and Intelligent Controllers: a Case Study. David Monniaux - EMSOFT - [bibtex]
836. An abstract domain extending Difference-Bound Matrices with disequality constraints. Mathias Péron, Nicolas Halbwachs - 8th International Conference on Verification, Model-checking, and Abstract Intepretation, VMCAI'07 - [bibtex]
837. 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]
838. Lustre as a System Modeling Language: Lussensor, a Case-Study with Sensor Networks. Florence Maraninchi, Ludovic Samper, Kevin Baradon, Antoine Vasseur - SLA++P'07, ETAPS'07 Satellite Workshop on Model-driven High-level Programming of Embedded Systems - [bibtex]
839. Semi-Automatic Region-Based Memory Management for Real-Time Java Embedded Systems. Guillaume Salagnac, Christophe Rippert, Sergio Yovine - Proceedings of the 13th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications - [bibtex]
840. Synthesis Of Optimal-Cost Dynamic Observers for Fault Diagnosis of Discrete-Event Systems. Franck Cassez, Stavros Tripakis, Karine Altisen - TASE '07: Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering - [bibtex]
841. A SystemC/TLM semantics in Promela and its possible applications. Claus Traulsen, Jérôme Cornet, Matthieu Moy, Florence Maraninchi - 14th Workshop on Model Checking Software SPIN - [bibtex]
842. Virtual execution of AADL models via a translation into synchronous programs. Erwan Jahier, Nicolas Halbwachs, Pascal Raymond, Xavier Nicollin, David Lesens - Proceedings of the 7th ACM & IEEE International conference on Embedded software, EMSOFT 2007, September 30 - October 3, 2007, Salzburg, Austria - [bibtex]
843. 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]
844. Intuitionistic Refinement Calculus.. Sylvain Boulmé - Typed Lambda Calculi and Applications - PDF - [bibtex]
845. On the Complexity of Modeling Dynamic Branch Predictors when Computing Worst-Case Execution Time. Claire Maiza-Burguière, Christine Rochange - Proceedings of the ERCIM/DECOS Workshop On Dependable Embedded Systems - [bibtex]
846. 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]
847. 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]
848. 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]
849. 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]
850. Specifying and executing reactive scenarios with Lutin. Pascal Raymond, Yvan Roux, Erwan Jahier - SLA++P'07, ETAPS'07 Satellite Workshop on Model-driven High-level Programming of Embedded Systems - [bibtex]
851. On timed components and their abstraction. Ramzi Ben Salah, Marius Bozga, Oded Maler - SAVCBS '07: Proceedings of the 2007 conference on Specification and verification of component-based systems - [bibtex]
852. 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]
853. 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]
854. 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]
855. 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]
856. 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]
857. An Approach to Modeling and Verification of Component Based Systems. Gregor Goessler, Susanne Graf, Mila Majster-Cederbaum, Moritz Martens, Joseph Sifakis - Current Trends in Theory and Practice of Computer Science, SOFSEM'07 - [bibtex]

Master Thesis

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

PhD Thesis and HDR

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

2006

Journal Articles

866. Counter-example Guided Predicate Abstraction of Hybrid Systems. Rajeev Alur, Thao Dang, Franjo Ivancic - Theoretical Computer Science (TCS) - [bibtex]
867. Reachability Analysis of Hybrid Systems via Predicate Abstraction. Rajeev Alur, Thao Dang, Franjo Ivancic - ACM transactions on embedded computing systems (TECS) - [bibtex]
868. Aspect-Oriented Programming for Reactive Systems: a Proposal in the Synchronous Framework. Karine Altisen, Florence Maraninchi, David Stauch - Science of Computer Programming - [bibtex]
869. 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]
870. A Survey of Algebraic Properties Used in Cryptographic Protocols. Véronique Cortier, Stéphanie Delaune, Pascal Lafourcade - Journal of Computer Security - [bibtex]
871. Snap-Stabilizing Depth-First Search on Arbitrary Networks. Alain Cournier, Stéphane Devismes, Franck Petit, Vincent Villain - Computer Journal - [bibtex]
872. Scheduling with timed automata. Yasmina Abdeddaïm, Eugene Asarin, Oded Maler - Theor. Comput. Sci. - [bibtex]
873. LusSy: an open Tool for the Analysis of Systems-on-a-Chip at the Transaction Level. Matthieu Moy, Florence Maraninchi, Laurent Maillet-Contoz - Design Automation for Embedded Systems - [bibtex]
874. Some ways to reduce the space dimension in polyhedra computations. Nicolas Halbwachs, David Merchat, Laure Gonnord - Formal Methods in System Design - [bibtex]
875. 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]
876. Automatic rate desynchronization of embedded reactive programs. Alain Girault, Xavier Nicollin, Marc Pouzet - ACM TECS - PDF - [bibtex]
877. A real-time profile for UML. Susanne Graf, Ileana Ober, Iulian Ober - STTT, Software Tools for Technology Transfer - [bibtex]
878. Validating Timed UML models by simulation and verification. Susanne Graf, Ileana Ober, Iulian Ober - STTT, Software Tools for Technology Transfer - [bibtex]
879. 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]
880. Case Studies with Lurette V2. Erwan Jahier, Pascal Raymond, Philippe Baufreton - Software Tools for Technology Transfer - [bibtex]

Book Chapters

881. Coq. Jean-François Monin, Philippe Chavin - Software Specification Methods, An Overview Using a Case Study - [bibtex]
882. 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]
883. Vérification de programmes synchrones avec Lustre/Lesar. Pascal Raymond - Systèmes temps réel 1 -- techniques de description et de vérification - [bibtex]

Conference Articles

884. Defending the bank with a proof assistant. Judicaël Courant, Jean-François Monin - WITS 2006 - [bibtex]
885. Monitoring and Fault Diagnosis with Digital Clocks. Karine Altisen, Franck Cassez, Stavros Tripakis - Application of Concurrency to System Design (ACSD'06) - [bibtex]
886. Qualification d'architectures fontionnelles. Marius Bozga, Pierre Combes, Susanne Graf, Wei Monin, Nicolas Moteau - Notere'06 - [bibtex]
887. From Self- to Snap- Stabilization. Alain Cournier, Stéphane Devismes, Vincent Villain - SSS'06, 8th International Symposium on Stabilization, Safety, and Security of Distributed Systems - [bibtex]
888. Snap-Stabilizing PIF and Useless Computations. Alain Cournier, Stéphane Devismes, Vincent Villain - ICPADS'06, 12th International Conference on Parallel and Distributed Systems - [bibtex]
889. Recent Progress in Continuous and Hybrid Reachability Analysis. Eugene Asarin, Thao Dang, Goran Frehse, Antoine Girard, Colas Le Guernic, Oded Maler - CACSD 2006 - [bibtex]
890. Approximate Reachability Computation for Polynomial Systems. Thao Dang - HSCC 2006 - [bibtex]
891. Scheduling for multi-threaded real-time programs via path planning. Thao Dang, Philippe Gerner - Proceedings of the 6th ACM & IEEE International conference on Embedded software, EMSOFT 2006 - [bibtex]
892. Simulation of Hybrid Systems For Circuit Validation. Thao Dang, Tarik Nahhal - FDL 2006 - [bibtex]
893. Test Generation for Network Security Rules. Vianney Darmaillacq, Jean-Claude Fernandez, Roland Groz, Laurent Mounier, Jean-Luc Richier - TestCom'06 - [bibtex]
894. On Timed Simulation Relations for Hybrid Systems and Compositionality. Goran Frehse - FORMATS 2006 - [bibtex]
895. From MITL to Timed Automata. Oded Maler, Dejan Nickovic, Amir Pnueli - FORMATS 2006 - [bibtex]
896. Efficient Computation of Reachable Sets of Linear Time-Invariant Systems with Inputs. Antoine Girard, Colas Le Guernic, Oded Maler - HSCC 2006 - [bibtex]
897. Fast and Flexible Difference Constraint Propagation for DPLL(T). Scott Cotton, Oded Maler - SAT 2006 - [bibtex]
898. Symbolic Protocol Analysis in Presence of a Homomorphism Operator and Exclusive-Or. Stéphanie Delaune, Pascal Lafourcade, Denis Lugiez, Ralf Treinen - Proceedings of the 33rd International Colloquium on Automata, Languages and Programming - [bibtex]
899. A Memory-Optimal Buffering Protocol for Preservation of Synchronous Semantics under Preemptive Scheduling. Christos Sofronis, Stavros Tripakis, Paul Caspi - 6th Intl. Conf. on Embedded Software (EMSOFT'06) - [bibtex]
900. Communication by Sampling in Time-Sensitive Distributed Systems. Albert Benveniste, Benoît Caillaud, Lucas Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli, Stavros Tripakis - 6th Intl. Conf. on Embedded Software (EMSOFT'06) - [bibtex]
901. A Test Calculus Framework Applied to Network Security Policies. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier, Jean-Luc Richier - FATES/RV'06 - [bibtex]
902. Interference of Larissa Aspects. David Stauch, Karine Altisen, Florence Maraninchi - FOAL : Foundations of Aspect-Oriented Languages workshop (an AOSD'06 satellite event) - [bibtex]
903. 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]
904. Combining widening and acceleration in linear relation analysis. Laure Gonnord, Nicolas Halbwachs - 13th International Static Analysis Symposium, SAS'06 - [bibtex]
905. Simulation and verification of asynchronous systems by means of a synchronous model. Nicolas Halbwachs, Louis Mandel - Sixth International Conference on Application of Concurrency to System Design, ACSD 2006 - [bibtex]
906. Test Coverage for Loose Timing Annotations. Claude Helmstetter, Florence Maraninchi, Laurent Maillet-Contoz - 11th International Workshop on Formal Methods for Industrial Critical Systems - [bibtex]
907. Approximation, Sampling and Voting in Hybrid Computing Systems. Chiheb Kossentini, Paul Caspi - Hybrid Systems Computation and Control, HSCC06 - [bibtex]
908. 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]
909. 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]
910. On the Importance of Modeling the Environment when Analyzing Sensor Networks. Ludovic Samper, Florence Maraninchi, Laurent Mounier, Erwan Jahier, Pascal Raymond - 3rd International Workshop on Wireless Ad-hoc and Sensor Networks (IWWAN'06) - [bibtex]
911. 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]
912. ACUNh: Unification and Disunification Using Automata Theory. Pascal Lafourcade, Denis Lugiez, Ralf Treinen - Proceedings of the 20th International Workshop on Unification (UNIF'06) - [bibtex]
913. 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]
914. 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]
915. Larissa: Modular Design of Man-Machine Interfaces with Aspects. Karine Altisen, Florence Maraninchi, David Stauch - Fifth International Symposium on Software Composition (an ETAPS satellite event) - [bibtex]
916. Efficient Region-Based Memory Management for Resource-limited Real-Time Embedded Systems. Guillaume Salagnac, Chaker Nakhli, Christophe Rippert, Sergio Yovine - In proceedings of the workshop on Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems - [bibtex]
917. Automatic Generation of Schedulings for Improving the Test Coverage of Systems-on-a-Chip. Claude Helmstetter, Florence Maraninchi, Laurent Maillet-Contoz, Matthieu Moy - Formal Methods in Computer Aided Design (FMCAD) - [bibtex]
918. 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]
919. Randomized simulation of hybrid systems for circuit validation. Thao Dang, Tarik Nahhal - Proceedings of FDL06 - Forum on specification and Design Languages - [bibtex]
920. History-Based Schemes and Implicit Path Enumeration. Claire Maiza-Burguière, Christine Rochange - Proceedings of the 6th International Workshop On Worst-Case Execution Time (WCET) Analysis - [bibtex]
921. 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]
922. 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]
923. 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]
924. Time Domain Verification of Oscillator Circuit Properties. Goran Frehse, Bruce H. Krogh, Rob A. Rutenbar, Oded Maler - Proc. Workshop on Formal Verification of Analog Circuits - [bibtex]
925. 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]
926. 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]
927. Describing and executing random reactive systems. Pascal Raymond, Erwan Jahier, Yvan Roux - SEFM 2006, 4th IEEE International Conference on Software Engineering and Formal Methods - [bibtex]
928. Generating Random Values Using Binary Decision Diagrams and Convex Polyhedra. Erwan Jahier, Pascal Raymond - Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA'06) - [bibtex]
929. 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]
930. On Interleaving in Timed Automata. Ramzi Ben Salah, Marius Bozga, Oded Maler - CONCUR 2006 - [bibtex]
931. 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]
932. 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]
933. Ensuring Properties of Interaction Systems by Construction. Gregor Goessler, Susanne Graf, Mila Majster-Cederbaum, Moritz Martens, Joseph Sifakis - Program Analysis and Compilation, Theory and Practice - [bibtex]
934. 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]

PhD Thesis and HDR

935. A Scalable Framework for Modelling and Performance Analysis of Multiprocessor Embedded Systems. Ismail Assayad - [bibtex]
936. Conception de Systèmes Adaptatifs Surs et Optimaux. Jacques Combaz - [bibtex]
937. Liens entre modèles symboliques et computationnels pour les protocoles cryptographiques utilisant des hachages. Romain Janvier - [bibtex]
938. Conditional Scheduling Strategies using Timed Automata. Abdelkarim Kerbaa - [bibtex]
939. Computational Soundness of Symbolic Models for Cryptographic Protocols. Laurent Mazaré - [bibtex]
940. Embedded Code Generation from High-level Heterogeneous Components. Christos Sofronis - [bibtex]
941. Vérification des protocoles cryptographiques en présence de théories équationnelles. Pascal Lafourcade - Thèse de doctorat - [bibtex]

2005

Journal Articles

942. A symbolic decision procedure for cryptographic protocols with time stamps. Liana Bozga, Cristian Ene, Yassine Lakhnech - J. Log. Algebr. Program. - [bibtex]
943. A Silent Self-stabilizing Algorithm for Finding Cut-nodes and Bridges. Stéphane Devismes - Parallel Processing Letters - [bibtex]
944. 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]
945. Formation en systèmes embarqués à l'INPG. Florence Maraninchi, Marc Renaudin - Revue des ingénieurs INPG - [bibtex]
946. Translating Discrete-Time Simulink to Lustre. Paul Caspi, Adrian Curic, Aude Maignan, Christos Sofronis, Stavros Tripakis - ACM Trans. Embedded Computing Systems - [bibtex]
947. 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]
948. Translating Java for Multiple Model Checkers: The Bandera Back-End. Radu Iosif, Matthew B. Dwyer, John Hatcliff - Formal Methods in System Design - [bibtex]
949. 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

950. 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]
951. From Control Loops to Real-Time Programs. Paul Caspi, Oded Maler - Handbook of Networked and Embedded Computing Systems - [bibtex]
952. Chapter 5.9, Formal Verification. Matthieu Moy - Transaction-Level Modeling with SystemC. TLM Concepts and Applications for Embedded Systems - [bibtex]

Conference Articles

953. Introduction au contrôle des systèmes temps-réel. Karine Altisen, Patricia Bouyer, Thierry Cachat, Franck Cassez, Guillaume Gardey - Modélisation des Systèmes Réactifs (MSR'05), session invitée de l'ACI CORTOS - [bibtex]
954. Implémentabilité des automates temporisés. Karine Altisen, Nicolas Markey, Pierre-Alain Reynier, Stavros Tripakis - Modélisation des Systèmes Réactifs (MSR'05), session invitée de l'ACI CORTOS - [bibtex]
955. A Snap-Stabilizing DFS with a Lower Space Requirement. Alain Cournier, Stéphane Devismes, Vincent Villain - SSS'05, 7th International Symposium on Self-Stabilizing Systems - [bibtex]
956. Snap-Stabilizing Detection of Cutsets. Alain Cournier, Stéphane Devismes, Vincent Villain - HiPC'05, 12th International Conference on High Performance Computing - [bibtex]
957. 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]
958. Real Time Temporal Logic: Past, Present, Future. Oded Maler, Dejan Nickovic, Amir Pnueli - FORMATS 2005 - [bibtex]
959. On temporal difference algorithms for continuous systems. Alexandre Donzé - ICINCO - [bibtex]
960. 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]
961. Semantic-Preserving and Memory Efficient Implementation of Inter-Task Communication on Static-Priority or EDF Schedulers. Stavros Tripakis, Christos Sofronis, Norman Scaife, Paul Caspi - 5th International Conference on Embedded Software, EMSOFT05 - [bibtex]
962. A model-based approach for robustness testing. Jean-Claude Fernandez, Laurent Mounier, Cyril Pachon - TestCom 2005 - [bibtex]
963. Flush: a system development tool based on Scade/Lustre. Jan Mikác, Paul Caspi - Formal methods for industrial critical systems, FMICS05 - [bibtex]
964. Implementation of Timed Automata: An Issue of Semantics or Modeling? Karine Altisen, Stavros Tripakis - FORMATS - [bibtex]
965. 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]
966. 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]
967. Intruder Deduction for AC-like Equational Theories with Homomorphisms. Pascal Lafourcade, Denis Lugiez, Ralf Treinen - Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA'05) - [bibtex]
968. A synchronous language at work: the story of Lustre. Nicolas Halbwachs - Third ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE'2005 - [bibtex]
969. Temporal Refinement for Lustre. Jan Mikác, Paul Caspi - Synchronous Languages Applications and Programming, SLAP'05 - [bibtex]
970. LusSy: A Toolbox for the Analysis of Systems-on-a-Chip at the Transactional Level. Matthieu Moy, Florence Maraninchi, Laurent Maillet-Contoz - International Conference on Application of Concurrency to System Design - [bibtex]
971. Pinapa: An Extraction Tool for SystemC descriptions of Systems-on-a-Chip. Matthieu Moy, Florence Maraninchi, Laurent Maillet-Contoz - EMSOFT - [bibtex]
972. 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]
973. 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]
974. 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]
975. A Contribution to Branch Prediction Modeling in WCET Analysis. Claire Maiza-Burguière, Christine Rochange - Proceedings of the Conference on Design, Automation and Test in Europe (DATE'05) - [bibtex]
976. A Case for Static Branch Prediction Modeling in Real-Time Systems. Claire Maiza-Burguière, Christine Rochange, Sainrat Pascal - Proceedings of the 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA'05) - [bibtex]
977. Modelisation d'un predicteur de branchement bimodal dans le calcul du WCET par la methode IPET. Claire Maiza-Burguière, Christine Rochange - Proceedings of the Conference on Real-Time Systems (RTS'05) - [bibtex]
978. 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]
979. 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]
980. 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]
981. 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]
982. 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]

PhD Thesis and HDR

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

2004

Journal Articles

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

Conference Articles

992. Formalisation of the Join-Calculus in Type Theory. Jean-François Monin - International Worshop on Formal Methods and Security - [bibtex]
993. Proof pearl: From concrete to functional unparsing. Jean-François Monin - Theorem Proving in Higher Order Logics (17th International Conference on TPHOLs 2004) - [bibtex]
994. Arrays and Contracts for the Specification and Analysis of Regular Systems. Florence Maraninchi, Lionel Morel - Fourth International Conference on Application of Concurrency to System Design - [bibtex]
995. 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]
996. 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]
997. IF Tutorial. Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober - 9th SPIN'04 Workshop on Model-Checking of Software, Barcelona, Spain - [bibtex]
998. Snap-Stabilizing Depth-First Search on Arbitrary Networks. Alain Cournier, Stéphane Devismes, Franck Petit, Vincent Villain - OPODIS'04, 8th International Conference On Principles Of DIstributed Systems - [bibtex]
999. Monitoring Temporal Properties of Continuous Signals. Oded Maler, Dejan Nickovic - Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques i - [bibtex]
1000. 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]
1001. Verification of Analog and Mixed-Signal Circuits Using Hybrid System Techniques. Thao Dang, Alexandre Donzé, Oded Maler - FMCAD - [bibtex]
1002. Logical-Time Contracts for the Development of Reactive Embedded Software. Florence Maraninchi, Lionel Morel - 30th Euromicro Conference, Component-Based Software Engineering Track (ECBSE) - [bibtex]
1003. Integrating model-based design and preemptive scheduling in mixed time- and event-triggered systems. Norman Scaife, Paul Caspi - Euromicro Conference on Real-Time Systems, ECRTS04 - [bibtex]
1004. Heterogeneous Reactive Systems Modeling: capturing causality and the correctness of loosely time-triggered protocols. Albert Benveniste, Benoît Caillaud, Lucas Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli - Emsoft04 - [bibtex]
1005. Exploring Aspects in the Context of Reactive Systems. Karine Altisen, Florence Maraninchi, David Stauch - Workshop on the Foundations of Aspect-Oriented Languages (FOAL), affiliated with AOSD (International Conference on Aspect-Oriented Software Development) - [bibtex]
1006. Mixed delay and threshold voters in critical real-time systems. Chiheb Kossentini, Paul Caspi - Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT04 - [bibtex]
1007. 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]
1008. A Framework for Time in FDTs. Susanne Graf, Andreas Prinz - FORTE 2004, participants proceedings - [bibtex]
1009. 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]
1010. From Discrete Duration Calculus to Symbolic Automata. Laure Gonnord, Nicolas Halbwachs, Pascal Raymond - 3rd International Workshop on Synchronous Languages, Applications, and Programs, SLAP'04, see also Electronic Notes in Theoretical Computer Science Volume 153, Issue 4, 27 June 2006, Pages 3-18 - [bibtex]
1011. Defining and translating a ``safe'' subset of Simulink/Stateflow into Lustre. Norman Scaife, Christos Sofronis, Paul Caspi, Stavros Tripakis, Florence Maraninchi - Fourth ACM International Conference on Embedded Software (EMSOFT) - [bibtex]
1012. 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]
1013. 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]
1014. 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]
1015. Abstraction by projection and application to multi-affine systems. Eugene Asarin, Thao Dang - Hybrid Systems: Control and Computation HSCC'04 - [bibtex]
1016. 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]
1017. Case Studies with Lurette V2. Erwan Jahier, Pascal Raymond, Philippe Baufreton - 1st International Symposium on Leveraging Applications of Formal Methods, ISoLA 2004 - [bibtex]

PhD Thesis and HDR

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

2003

Journal Articles

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

Conference Articles

1025. Abstract Interpretation for Secrecy using Patterns. Liana Bozga, Yassine Lakhnech, Michaël Périn - TACAS'03 - [bibtex]
1026. 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]
1027. 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]
1028. 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]
1029. Translating Discrete-Time Simulink to Lustre. Paul Caspi, Adrian Curic, Aude Maignan, Christos Sofronis, Stavros Tripakis - Embedded Software EMSOFT2003 - [bibtex]
1030. Heterogeneous Reactive Systems Modeling and Correct-by-Construction Deployment. Albert Benveniste, Lucas Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli - 3rd International Wokshop on Embedded Software, EMSOFT03 - [bibtex]
1031. Using Controller Synthesis to Build Property-Enforcing Layers. Karine Altisen, Aurélie Clodic, Florence Maraninchi, Eric Rutten - European Symposium on Programming (ESOP) - [bibtex]
1032. Property Oriented Test Case Generation. Jean-Claude Fernandez, Laurent Mounier, Cyril Pachon - Proceedings of FATES'03 (Satellite workshop of ASE'03), Montreal, Canada - [bibtex]
1033. Causality and Scheduling Constraints in Heterogeneous Reactive Systems Modeling. Albert Benveniste, Benoît Caillaud, Lucas Carloni, Paul Caspi, Alberto L. Sangiovanni-Vincentelli - FMCO 2003 - [bibtex]
1034. 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]
1035. 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]
1036. Cartesian factoring of polyhedra in linear relation analysis. Nicolas Halbwachs, David Merchat, Catherine Parent-Vigouroux - Static Analysis Symposium, SAS'03 - [bibtex]
1037. From Simulink to SCADE/Lustre to TTA: A Layered Approach for Distributed Embedded Applications. Paul Caspi, Adrian Curic, Aude Maignan, Christos Sofronis, Stavros Tripakis, Peter Niebert - Languages, Compilers and Tools for Embedded Systems, LCTES 2003 - [bibtex]
1038. Finite state machines: composition, verification, minimization: a case study. Paul Amblard, Fabienne Lagnier, Michel Levy - 10th International Conference on Mixed Design (MIXDES03), Lodz, Poland - [bibtex]
1039. Automatique continue, automatique discrète, informatique industrielle : le triangle des Bermudes ? Paul Caspi - Actes du colloque Modélisation des systèmes réactifs, MSR03 - [bibtex]
1040. 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]
1041. 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]
1042. Counter-example Guided Predicate Abstraction of Hybrid Systems. Rajeev Alur, Thao Dang, Franjo Ivancic - Tools and Algorithms for the Construction and Analysis of Systems TACAS'03 - [bibtex]
1043. Progress on Reachability Analysis of Hybrid Systems using Predicate Abstraction. Rajeev Alur, Thao Dang, Franjo Ivancic - Hybrid Systems: Control and Computation HSCC'03 - [bibtex]
1044. 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]
1045. 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]
1046. Automatic State Reaching for Debugging Reactive Programs. Erwan Jahier, Bertrand Jeannet, Fabien Gaucher, Florence Maraninchi - AADEBUG'2003 -- Fifth International Workshop on Automated Debugging - [bibtex]

Master Thesis

1047. Application de la résolution de conflits << logiques >>, à l'aide à la décision pour la résolution de conflits des problèmes d'ordonnancement. Pascal Lafourcade - Rapport de DEA - [bibtex]

PhD Thesis and HDR

1048. Modélisation et résolution de problèmes d'ordonnancement à l'aide d'automates temporisés. Yasmina Abdeddaïm - [bibtex]
1049. étude du débogage de systèmes réactifs et application au langage synchrone Lustre. Fabien Gaucher - [bibtex]
1050. 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

1051. Testing Theories for Broadcasting Processes. Cristian Ene, Traian Muntean - Sci. Ann. Cuza Univ. - [bibtex]
1052. Iterating Transducers. Dennis Dams, Yassine Lakhnech, Martin Steffen - The Journal of Logic and Algebraic Programming - [bibtex]
1053. Scheduler modelling based on the controller synthesis paradigm. Karine Altisen, Gregor Goessler, Joseph Sifakis - Journal of Real-Time Systems - [bibtex]
1054. Generic program monitoring by trace analysis. Erwan Jahier, Mireille Ducassé - TPLP - PDF - [bibtex]

Conference Articles

1055. Tools for Controller Synthesis of Timed Systems. Karine Altisen, Stavros Tripakis - 2nd Workshop on Real-Time Tools (RT-TOOLS'2002) - [bibtex]
1056. Using Formal Tools to Study Complex Circuits Behaviour. Paul Amblard, Fabienne Lagnier, Michel Levy - IEEE Symposium on Digital Systems Design (Euromicro DSD 2002) - [bibtex]
1057. Toward an Approximation Theory for Computerised Control. Paul Caspi, Albert Benveniste - 2nd International Workshop on Embedded Software, EMSOFT02 - [bibtex]
1058. A Protocol for Loosely Time-Triggered Architectures. Albert Benveniste, Paul Caspi, Paul Le Guernic, Hervé Marchand, Jean-Pierre Talpin, Stavros Tripakis - 2nd International Wokshop on Embedded Software, EMSOFT02 - [bibtex]
1059. Synchronous modeling of asynchronous systems. Nicolas Halbwachs, Siwar Baghdadi - ACM Conference on Embedded Systems Software, EMSOFT'02 - [bibtex]
1060. Describing Non-Deterministic Reactive Systems by Means of Regular Expressions. Pascal Raymond, Yvan Roux - First Workshop on Synchronous Languages, Applications and Programming, SLAP'02 - Electr. Notes Theor. Comput. Sci. - [bibtex]
1061. Expression of time and duration constraints in SDL. Susanne Graf - 3rd SAM Workshop on SDL and MSC, University of Wales Aberystwyth - [bibtex]
1062. 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]
1063. The d/dt Tool for Verification of Hybrid Systems. Eugene Asarin, Thao Dang, Oded Maler - Computer Aided Verification CAV'02 - [bibtex]
1064. Reachability Analysis Via Predicate Abstraction. Rajeev Alur, Thao Dang, Franjo Ivancic - Hybrid Systems: Computation and Control HSCC'02 - [bibtex]
1065. 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]
1066. 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

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

2001

Journal Articles

1069. Argos: an Automaton-Based Synchronous Language. Florence Maraninchi, Yann Rémond - Computer Languages - [bibtex]
1070. Verification of Parameterized Protocols. Kai Baukus, Yassine Lakhnech, Karsten Stahl - Journal of Universal Computer Science - [bibtex]
1071. Verifying Untimed and Timed Aspects of the Experimental Batch Plant. Ralf Huuck, Ben Lukoschus, Yassine Lakhnech - European Journal of Control - [bibtex]
1072. Automatic Verification of Parameterized Networks of Processes. David Lesens, Nicolas Halbwachs, Pascal Raymond - Theoretical Computer Science - [bibtex]
1073. Efficient Automated Trace Analysis: Examples with Morphine. Mireille Ducassé, Erwan Jahier - Electr. Notes Theor. Comput. Sci. - [bibtex]

Conference Articles

1074. Analyzing Fair Parametric Extended Automata. Aurore Annichini-Collomb, Ahmed Bouajjani, Yassine Lakhnech, Mihaela Sighireanu - Static Analysis Symposium 2001 - [bibtex]
1075. Model-Checking Ariane-5 Flight Program. Marius Bozga, David Lesens, Laurent Mounier - Proceedings of FMICS'01 (Paris, France) - [bibtex]
1076. 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]
1077. Timed Extensions for SDL. Marius Bozga, Alain Kerbrat, Susanne Graf, Laurent Mounier, Iulian Ober, Daniel Vincent - Proceedings of SDL FORUM'01 (Copenhagen, Denmark) - [bibtex]
1078. From Control System Design to Embedded Code: The Synchronous Data-Flow Approach. Paul Caspi, Pascal Raymond - IEEE-CDC - [bibtex]
1079. 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]
1080. Iterating Transducers. Dennis Dams, Yassine Lakhnech, Martin Steffen - Computer Aided Verification'01 - [bibtex]
1081. Embedded control: from asynchrony to synchrony and back. Paul Caspi - First International Workshop on Embedded Software - [bibtex]
1082. Counter-example generation in symbolic abstract model-checking. Gordon Pace, Nicolas Halbwachs, Pascal Raymond - 6th International Workshop on Formal Methods for Industrial Critical Systems, FMICS'2001 - [bibtex]
1083. Effective programming language support for discrete-continuous mode-switching control systems. Florence Maraninchi, Yann Rémond, Eric Rutten - 40th IEEE Conference on Decision and Control (CDC) - [bibtex]
1084. About the design of distributed control systems: the quasi-synchronous approach. Paul Caspi, Christine Mazuet, Natacha Reynaud-Paligot - Proc. Safecomp'01 - [bibtex]
1085. 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]
1086. 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]
1087. On Hybrid Control of Under-actuated Mechanical Systems. Eugene Asarin, Sorav Bansal, Thao Dang, Bernard Espiau, Oded Maler - Hybrid Systems: Computation and Control HSCC'01 - [bibtex]
1088. Stability and reachability analysis of a hybrid model of luminescence in the marine bacterium Vibrio Fisheri. Calin Belta, Jonathan Schug, Thao Dang, Vijay Kumar, George Pappas, Harvey Rubin, Paul Dunlap - CDC'01 - Conference on Decision and Control - [bibtex]
1089. d/dt: A Verification Tool for Hybrid Systems. Eugene Asarin, Thao Dang, Oded Maler - CDC'01 - Conference on Decision and Control - [bibtex]
1090. d/dt: a Tool for Reachability Analysis of Continuous and Hybrid systems. Eugene Asarin, Thao Dang, Oded Maler - 5th IFAC Symposium Nonlinear Control Systems NOLCOS - [bibtex]
1091. 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]
1092. 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]
1093. 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]
1094. Prototyping CLP(FD) tracers: a trace model and an experimental validation environment. Ludovic Langevine, Pierre Deransart, Mireille Ducassé, Erwan Jahier - WLPE - [bibtex]

PhD Thesis and HDR

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

2000

Journal Articles

1101. 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]
1102. Langages pour la conception de systèmes réactifs. Paul Caspi - Technique et science informatique - [bibtex]

Conference Articles

1103. Abstracting WS1S Systems to Verify Parameterized Networks. Kai Baukus, Saddek Bensalem, Yassine Lakhnech, Karsten Stahl - TACAS'00 - [bibtex]
1104. 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]
1105. 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]
1106. Verification of Sequential Function Charts using SMV. Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus - PDPTA 2000 special session on Formal Validation - [bibtex]
1107. 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]
1108. Verifying Universal Properties of Parameterized Networks. Kai Baukus, Yassine Lakhnech, Karsten Stahl - Formal Techniques in Real-Time and Fault-Tolerant Systems - [bibtex]
1109. 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]
1110. 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]
1111. Threshold and Bounded-Delay Voting in Critical Control Systems. Paul Caspi, Rym Salem-Habermehl - Formal Techniques in Real-Time and Fault-Tolerant Systems - [bibtex]
1112. A methodology for the construction of scheduled systems. Karine Altisen, Gregor Goessler, Joseph Sifakis - Formal Techniques in Real-Time and Fault-Tolerant Systems 2000 (FTRTFT'00) - [bibtex]
1113. Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems. Jean-Pierre Krimm, Laurent Mounier - Proceedings of TACAS'00 - [bibtex]
1114. A PVS Proof Obligation Generator for Lustre Programs. Cécile Dumas, Paul Caspi - 7th International Conference on Logic for Programming and Automated Reasoning - [bibtex]
1115. Step-wise + Algorithmic debugging for Reactive Programs: LuDiC, a debugger for Lustre. Florence Maraninchi, Fabien Gaucher - AADEBUG'2000 -- Fourth International Workshop on Automated Debugging - [bibtex]
1116. MATOU: An Implementation of Mode-Automata. Florence Maraninchi, Yann Rémond, Yannick Raoul - International Conference on Compiler Construction (CC) - [bibtex]
1117. Running-Modes of Real-Time Systems: A Case-Study with Mode-Automata. Florence Maraninchi, Yann Rémond - 12th Euromicro Conference on Real-Time Systems - [bibtex]
1118. Applying Formal Methods to Industrial Cases: The Language Approach (The Production-Cell and Mode-Automata). Florence Maraninchi, Yann Rémond - 5th International Workshop on Formal Methods for Industrial Critical Systems (FMICS) - [bibtex]
1119. The Quasi-Synchronous Approach to Distributed Control Systems. Paul Caspi, Rym Salem-Habermehl - Proceedings of the Summer School "Modelling and Verification of Parallel Processes (MOVEP'2k), - [bibtex]
1120. Stability of discrete sampled systems. Nicolas Halbwachs, Jean-François Héry, Jen-Claude Laleuf, Xavier Nicollin - 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT'2000 - [bibtex]
1121. Collecting Graphical Abstract Views of Mercury Program Executions. Erwan Jahier - AADEBUG - [bibtex]
1122. 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]
1123. 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]
1124. Approximate Reachability Analysis of Piecewise-Linear Dynamical Systems. Eugene Asarin, Oded Maler - Hybrid Systems: Computation and Control HSCC'00 - [bibtex]
1125. 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]
1126. 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]
1127. 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]
1128. Specifying Prolog Trace Models with a Continuation Semantics. Erwan Jahier, Mireille Ducassé, Olivier Ridoux - Logic Based Program Synthesis and Transformation, 10th International Workshop, LOPSTR 2000 London, UK, July 24-28, 2000, Selected Papers - [bibtex]
1129. Spécification de modèles de traces à l'aide d'une sémantique par continuations. Erwan Jahier, Mireille Ducassé, Olivier Ridoux - Programmation en logique avec contraintes, JFPLC 2000, 28-30 Juin 2000, Marseille, France - [bibtex]

PhD Thesis and HDR

1130. Méthodes déductives pour la preuve de programmes Lustre. Cécile Dumas Canovas - [bibtex]
1131. Partitionnement dynamique dans l'analyse de relations linéaires et application à la vérification de programmes synchrones. Bertrand Jeannet - [bibtex]
1132. Applications des ordres partiels à la génération compositionelle de systèmes asynchrones. Jean-Pierre Krimm - Thèse de doctorat - [bibtex]
1133. Analyse dynamique de programmes : mise en oeuvre automatisée d'analyseurs performants et spécifications de modèle d'exécution. Erwan Jahier - [bibtex]
1134. V'erification et synth`ese des syst`emes hybrides. Thao Dang - [bibtex]

1999

Journal Articles

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

Conference Articles

1139. 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]
1140. A Framework for Scheduler Synthesis. Karine Altisen, Gregor Goessler, Amir Pnueli, Joseph Sifakis, Stavros Tripakis, Sergio Yovine - RTSS'99 - [bibtex]
1141. Validation of Synchronous Reactive Systems: from Formal Verification to Automatic Testing. Nicolas Halbwachs, Pascal Raymond - ASIAN'99, Asian Computing Science Conference - [bibtex]
1142. A methodology for proving control systems with Lustre and PVS. Saddek Bensalem, Paul Caspi, Cécile Dumas, Catherine Parent-Vigouroux - Dependable Computing for Critical Applications (DCCA7) - [bibtex]
1143. State Space Reduction Based on Live Variables Analysis. Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu - SAS - [bibtex]
1144. 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]
1145. On-the-fly controller synthesis for discrete and dense time systems. Stavros Tripakis, Karine Altisen - Formal Methods 1999 (FM'99) - [bibtex]
1146. Formal Design of Distributed Control Systems with Lustre. Paul Caspi, Christine Mazuet, Rym Salem-Habermehl, Daniel Weber - Proc. Safecomp'99 - [bibtex]
1147. Dynamic Partitioning in Analyses of Numerical Properties. Bertrand Jeannet, Nicolas Halbwachs, Pascal Raymond - Static Analysis Symposium, SAS'99 - [bibtex]
1148. 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]
1149. 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]
1150. Un traceur d'exécution de programme ne sert pas qu'au débogage. Erwan Jahier, Mireille Ducassé - JFPLC'99, Huitièmes Journées Francophones de Programmation Logique et programmation par Contraintes, 2-4 juin 199, Lyon, France - [bibtex]
1151. A Generic Approach to Monitor Program Executions. Erwan Jahier, Mireille Ducassé - ICLP - [bibtex]
1152. 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]
1153. 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]
1154. 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

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

1998

Journal Articles

1158. On Complexity of Reachability of Transition Restricted Petri Nets. Cristian Ene - Sci. Ann. Cuza Univ. - [bibtex]
1159. About synchronous programming and abstract interpretation. Nicolas Halbwachs - Science of Computer Programming, Special Issue on SAS'94 - [bibtex]
1160. 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

1161. A tool for proving Lustre programs in PVS. Saddek Bensalem, Paul Caspi, Cécile Dumas, Catherine Parent-Vigouroux - TOOLS'98 - [bibtex]
1162. Computing Abstractions of Infinite State Systems Automatically and Compositionally. Saddek Bensalem, Yassine Lakhnech, Sam Owre - Computer Aided Verification - [bibtex]
1163. InVeSt : A Tool for the Verification of Invariants. Saddek Bensalem, Yassine Lakhnech, Sam Owre - Computer Aided Verification - [bibtex]
1164. A Co-iterative Characterization of Synchronous Stream Functions. Paul Caspi, Marc Pouzet - Proceedings of the Workshop on Coalgebraic Methods in Computer Science, Lisbon - [bibtex]
1165. Synchronous programming of reactive systems, a tutorial and commented bibliography. Nicolas Halbwachs - Tenth International Conference on Computer-Aided Verification, CAV'98 - [bibtex]
1166. Verifying Statecharts with Spin. Gerard J. Holzmann, Erich Mikk, Yassine Lakhnech, Michael Siegel - Proc. Workshop on Industrial-strength Formal specification Techniques - [bibtex]
1167. On the Composition of Condition/Event Systems. Stefan Kowalewski, Yassine Lakhnech, Ben Lukoschus, Luis Urbina - WODES'98 - [bibtex]
1168. Test automatique de systèmes réactifs. Nicolas Halbwachs, Xavier Nicollin, Pascal Raymond, Daniel Weber - Ecole d'été ``MOdélisation et VÉrification des Processus parallèles - [bibtex]
1169. Automatic Testing of Reactive Systems. Pascal Raymond, Daniel Weber, Xavier Nicollin, Nicolas Halbwachs - 19th IEEE Real-Time Systems Symposium - [bibtex]
1170. Mode-Automata: About Modes and States for Reactive Systems. Florence Maraninchi, Yann Rémond - European Symposium On Programming (ESOP) - [bibtex]
1171. 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]
1172. Reachability Analysis via Face Lifting. Thao Dang, Oded Maler - Hybrid Systems: Computation and Control HSCC'98 - [bibtex]
1173. 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

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

1997

Journal Articles

1180. Protocol Verification with the Aldebaran Toolset. Marius Bozga, Jean-Claude Fernandez, Alain Kerbrat, Laurent Mounier - Software Tools for Technology Transfer - [bibtex]
1181. Hierarchies of Petri Net Languages and a Super-Normal Form. Ferucio Laurentiu Tiplea, Cristian Ene - Journal of Automata, Languages and Combinatorics - [bibtex]
1182. 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]
1183. Distributing Automata for Asynchronous Networks of Processors. Benoît Caillaud, Paul Caspi, Alain Girault, Claude Jard - Journal Européen des Systèmes Automatisés - [bibtex]
1184. Verifying programs in the Calculus of Inductive Constructions. Catherine Parent-Vigouroux - Formal Aspects of Computing - [bibtex]
1185. Verification of real-time systems using linear relation analysis. Nicolas Halbwachs, Yann-Eric Proy, Patrick Roumanoff - Formal Methods in System Design - [bibtex]

Book Chapters

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

Conference Articles

1187. What can we learn from synchronous data-flow languages. Paul Caspi - Hybrid and Real-Time Systems - [bibtex]
1188. 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]
1189. Comparing Timed Condition/Event Systems and Timed Automata. Ralf Huuck, Yassine Lakhnech, Luis Urbina, Sebastian Engell, Stefan Kowalewski, Jorg Preußig - HART'97 - [bibtex]
1190. 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]
1191. 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]
1192. Automatic Verification of Parameterized Linear Networks of Processes. David Lesens, Nicolas Halbwachs, Pascal Raymond - 24th ACM Symposium on Principles of Programming Languages, POPL'97 - [bibtex]
1193. A Kleene Theorem for Timed Automata. Eugene Asarin, Oded Maler, Paul Caspi - Proc. Logic in Computer Science, LICS'97 - [bibtex]
1194. Temporal Logic for Stabilizing Systems. Yassine Lakhnech, Michael Siegel - Second International Conference on Temporal Logic - ICTL'97 - [bibtex]
1195. 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]
1196. Towards Efficient Modelchecking Statecharts: A Statecharts to Promela Complier. Yassine Lakhnech, Erich Mikk, Michael Siegel - 3rd International SPIN Workshop - [bibtex]
1197. Towards Efficient Modelchecking Statecharts. Erich Mikk, Yassine Lakhnech, Michael Siegel - STATEMATE Anwenderforum 97 - [bibtex]
1198. 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]
1199. Hierarchical automata as model for statecharts. Yassine Lakhnech, Erich Mikk, Michael Siegel - Proc. of the Asian Computing Science Conference (ASIAN'97) - [bibtex]
1200. Compositionality Criteria for Defining Mixed-Styles Synchronous Languages (invited paper). Florence Maraninchi, Yann Rémond - International Symposium: Compositionality - The Significant Difference - [bibtex]
1201. Construction of abstract state graphs with PVS. Susanne Graf, Hassen Saidi - Conference on Computer Aided Verification CAV'97, Haifa - [bibtex]
1202. Deductive verification of stabilizing systems. Yassine Lakhnech, Michael Siegel - 3rd Workshop on Self-stabilizing Systems, Santa Barbara, California, August, 1997, Proceedings - [bibtex]

PhD Thesis and HDR

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

1996

Journal Articles

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

Conference Articles

1207. Compiling ARGOS into Boolean equations. Florence Maraninchi, Nicolas Halbwachs - Formal Techniques for Real-Time and Fault Tolerance (FTRTFT) - [bibtex]
1208. Vérification de systèmes réactifs en Argos temporisé. Muriel Jourdan, Florence Maraninchi - Congrès AFCET : Modélisation des systèmes réactifs - [bibtex]
1209. Powerful Techniques for the Automatic Generation of Invariants. Saddek Bensalem, Yassine Lakhnech, Hassen Saidi - 8th International Conference on Computer Aided Verification - [bibtex]
1210. 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]
1211. Un modèle pour la distribution d'automates réactifs sur réseau asynchrone de processeurs. Benoît Caillaud, Paul Caspi, Alain Girault, Claude Jard - Conférence Afcet sur la Modélisation des systèmes réactifs, Brest - [bibtex]
1212. 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]
1213. 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]
1214. Compositional Semantics of Non-deterministic Synchronous Languages. Florence Maraninchi, Nicolas Halbwachs - European Symposium On Programming (ESOP) - [bibtex]
1215. 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]
1216. Verifying invariants using theorem proving. Susanne Graf, Hassen Saidi - Conference on Computer Aided Verification CAV'96 - [bibtex]
1217. Synchronous Kahn networks. Paul Caspi, Marc Pouzet - Int. Conf. on Functional Programming - [bibtex]
1218. Réseaux de Kahn synchrones. Marc Pouzet, Paul Caspi - Journées Francophones des langages applicatifs, Val Morin, Quebec - [bibtex]
1219. Automatic Construction of Network Invariants. David Lesens, Nicolas Halbwachs, Pascal Raymond - International Workshop on Verification of Infinite State Systems (INFINITY) - [bibtex]
1220. Translating Statecharts to Promela/SPIN. Erich Mikk, Yassine Lakhnech, Michael Siegel - Dagstuhl-Seminar ``Synchronous Languages'' - [bibtex]
1221. Natural proofs and programs optimization in the Calculus of Inductive Constructions. Catherine Parent-Vigouroux - International Conference on Theorem Proving in Higher Order Logic - [bibtex]
1222. Recognizing Regular Expressions by Means of Dataflow Networks. Pascal Raymond - Automata, Languages and Programming, 23rd International Colloquium - [bibtex]
1223. 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]
1224. 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

1225. Metric temporal logic with durations. Yassine Lakhnech, Jozef Hooman - Theoretical Computer Science - [bibtex]
1226. 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]
1227. 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

1228. The railroad crossing problem, modeling with Hybrid Argos - Analysis with Polka. Nicolas Halbwachs, Florence Maraninchi, Yann-Eric Proy - Second European Workshop on Real-Time and Hybrid Systems - [bibtex]
1229. Static Timing Analysis of Real-Time Systems. Muriel Jourdan, Florence Maraninchi - ACM Sigplan Workshop on Language, compiler and tool support for real-time systems - [bibtex]
1230. Temporal logic + timed automata : expressiveness and decidability. Ahmed Bouajjani, Yassine Lakhnech - CONCUR'95: Concurrency Theory - [bibtex]
1231. From duration calculus to linear hybrid automata. Ahmed Bouajjani, Yassine Lakhnech, Riadh Robbana - Computer Aided Verification - [bibtex]
1232. 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]
1233. An algorithm for reducing binary branchings. Paul Caspi, Jean-Claude Fernandez, Alain Girault - Fifteenth Conference on the Foundations of Software Technology and Theoretical Computer Science, FST&TCS - [bibtex]
1234. Hierarchies of Petri Net Languages and a Super-Normal Form. Ferucio Laurentiu Tiplea, Cristian Ene - Developments in Language Theory - [bibtex]
1235. On the symbolic analysis of combinational loops in circuits and synchronous programs. Nicolas Halbwachs, Florence Maraninchi - Euromicro'95 - [bibtex]
1236. A functional extension to Lustre. Paul Caspi, Marc Pouzet - 8th Int. Symp. on Languages for Intensional Programming - [bibtex]
1237. Formal verification of a critical system written in Saga/Lustre. Fabienne Lagnier, Pascal Raymond, Christian Dubois - Workshop on Formal Methods, Modelling and Simulation for System Engineering - [bibtex]
1238. Vérification de propriétés de programmes écrits en Lustre. Christian Dubois, Paul Ghaleb, Fabienne Lagnier, Pascal Raymond - RTS'95 - [bibtex]
1239. Execution of reactive distributed systems. Paul Caspi, Alain Girault - EURO--PAR'95, Stockholm - [bibtex]
1240. 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]
1241. Logics vs. Automata: The Hybrid Case. Ahmed Bouajjani, Yassine Lakhnech - Hybrid Systems III: Verification and Control, Proceedings of the DIMACS/SYCON Workshop, October 22-25, 1995, Ruttgers University, New Brunswick, NJ, USA - [bibtex]

PhD Thesis and HDR

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

1994

Journal Articles

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

Book Chapters

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

Conference Articles

1245. A Modular State/Transition Approach for Programming Real-Time Systems. Muriel Jourdan, Florence Maraninchi - ACM Sigplan Workshop on Language, compiler and tool support for real-time systems - [bibtex]
1246. A Multiparadigm Language for Reactive Systems. Muriel Jourdan, Fabienne Lagnier, Pascal Raymond, Florence Maraninchi - In 5th IEEE International Conference on Computer Languages - [bibtex]
1247. 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]
1248. Distributing Reactive Systems. Paul Caspi, Alain Girault, Daniel Pilaud - Seventh International Conference on Parallel and Distributed Computing Systems, PDCS'94 - [bibtex]
1249. Verification of linear hybrid systems by means of convex approximations. Nicolas Halbwachs, Yann-Eric Proy, Pascal Raymond - International Symposium on Static Analysis, SAS'94 - [bibtex]
1250. About synchronous programming and abstract interpretation. Nicolas Halbwachs - International Symposium on Static Analysis, SAS'94 - [bibtex]
1251. Studying Synchronous Communication Mechanisms by Abstractions. Muriel Jourdan, Florence Maraninchi - IFIP Working Conference on Programming Concepts, Methods and Calculi - [bibtex]
1252. Towards recursive block diagrams. Paul Caspi - Proc. 19th IFAC/IFIP Workshop on real-time programming, Isle of Reichenau - [bibtex]
1253. Verification of a distributed Cache memory by using abstractions. Susanne Graf - Conference on Computer Aided Verification CAV'94, Stanford - [bibtex]
1254. 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

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

1993

Journal Articles

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

Conference Articles

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

PhD Thesis and HDR

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

1992

Journal Articles

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

Conference Articles

1280. Operational and Compositional Semantics of Synchronous Automaton Compositions. Florence Maraninchi - International Conference on Concurrency Theory (CONCUR) - [bibtex]
1281. Minimization of timed transition systems (extended abstract). Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, David Dill, Howard Wong-Toi - CONCUR'92 - [bibtex]
1282. 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]
1283. An Experience in compiling a mixed imperative/declarative language for reactive systems. Florence Maraninchi, Muriel Vachon - International Workshop on Compiler Construction (poster session) - [bibtex]
1284. Distributing a finite transition system on a shared/distributed memory system. Alain Girault, Paul Caspi - PARLE'92 Paris - [bibtex]
1285. An implementation of three algorithms for timing verification based on automata emptiness. Rajeev Alur, Costas Courcoubetis, David Dill, Nicolas Halbwachs, Howard Wong-Toi - 13th IEEE Real-Time Systems Symposium - [bibtex]
1286. Provably Correct Compiler Development and Implementation. Bettina Buth, Karl-Heinz Buth, Martin Franzle, 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

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