Publications

Bruno Ferres, Oussama Oulkaid, Ludovic Henrio, Mehdi Khosravian, Matthieu Moy, Gabriel Radanne, and Pascal Raymond. Electrical Rule Checking of Integrated Circuits using Satisfiability Modulo Theory. In DATE 2023 - Design, Automation and Test in Europe Conference, Anvers (Antwerpen), Belgium, Apr 2023. [ http | .pdf ]

Keywords: Electrical Rule Checking ; Integrated Circuits ; SMT Solving

BibTex

Stéphane Devismes, Anissa Lamani, Franck Petit, Pascal Raymond, and Sébastien Tixeuil. Terminating exploration of a grid by an optimal number of asynchronous oblivious robots. The Computer Journal, 64(1):132–154, 01 2021. [ DOI | http ]

BibTex

Matheus Schuh, Claire Maiza, Joël Goossens, Pascal Raymond, and Benoît Dupont De Dinechin. A study of predictable execution models implementation for industrial data-flow applications on a multi-core platform with shared banked memory. In 2020 IEEE Real-Time Systems Symposium (RTSS), Houston, TX, United States, Dec 2020. [ http | .pdf ]

BibTex

Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Erwan Jahier, Nicolas Halbwachs, Fabienne Carrier, Mihail Asavoae, and Rémy Boutonnet. Improving WCET evaluation using linear relation analysis. Leibniz Transactions on Embedded Systems, 6(1):02–1–02:28, 2019. [ DOI | http ]

Keywords: Worst Case Execution Time estimation; Infeasible Execution Paths; Abstract Interpretation

BibTex

Amaury Graillat, Matthieu Moy, Pascal Raymond, and Benoît Dupont De Dinechin. Parallel code generation of synchronous programs for a many-core architecture. In Design, Automation and Test in Europe, Dresden, Germany, Mar 2018. [ .pdf ]

BibTex

Moustapha Lo, Nicolas Valot, Florence Maraninchi, and Pascal Raymond. Real-time on-board manycore implementation of a health monitoring system: Lessons learnt. In 9th European Congress Embedded Real Time Software and Systems (ERTS2 2018), Toulouse, France, february 2018. [ .pdf ]

BibTex

Claire Maiza, Pascal Raymond, Catherine Parent-Vigouroux, Armelle Bonenfant, Fabienne Carrier, Hugues Cassé, Philippe Cuenot, Denis Claraz, Nicolas Halbwachs, Erwan Jahier, Hanbing Li, Marianne de Michiel, Vincent Mussot, Isabelle Puaut, Christine Rochange, Erven Rohou, Jordy Ruiz, Pascal Sotin, and Wei-Tsun Sun. The w-sept project: Towards semantic-aware wcet estimation. In Jan Reineke, editor, 17th International Workshop on Worst-Case Execution Time Analysis (WCET 2017), volume 57 of OpenAccess Series in Informatics (OASIcs), pages 1–13, Dagstuhl, Germany, 2017. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. [ DOI | http ]

BibTex

Armelle Bonenfant, Fabienne Carrier, Hugues Cassé, Philippe Cuenot, Denis Claraz, Nicolas Halbwachs, Hanbing Li, Claire Maiza, Marianne De Michiel, Vincent Mussot, Catherine Parent-Vigouroux, Isabelle Puaut, Pascal Raymond, Erven Rohou, and Pascal Sotin. When the worst-case execution time estimation gains from the application semantics. In 8th European Congress on Embedded Real-Time Software and Systems, Toulouse, France, Jan 2016. [ http ]

BibTex

Moustapha Lo, Nicolas Valot, Florence Maraninchi, and Pascal Raymond. Implementing a real-time avionic application on a many-core processor. In 42nd European Rotorcraft Forum (ERF), Lille, France, Sep 2016. [ .pdf | .pdf ]

Keywords: many-core ; avionics ; health monitoring

BibTex

Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Fabienne Carrier, and Mihail Asavoae. Timing analysis enhancement for synchronous program. Real-Time Systems, pages 1–29, 2015. [ DOI | http ]

BibTex

Hugues Cassé, Claire Maiza, , Catherine Parent-Vigouroux, and Pascal Raymond. Schedulability and modular analysis: how to fit timing model? In OPRTC, 2014. [ .pdf ]

BibTex

Claire Maiza, Christine Rochange, and Pascal Raymond. Estimation de temps d’exécution et délais. In Maryline Chetto, editor, Ordonnancement dans les systèmes temps réel, chapter 13, pages 365–392. ISTE editions, 2014.

BibTex

Claire Maiza, Christine Rochange, and Pascal Raymond. Estimation of execution time and delays. In Maryline Chetto, editor, Real-time Systems Scheduling 1, chapter 5, pages 193–230. ISTE editions, august 2014. [ http ]

BibTex

Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Fabienne Carrier, and Mihail Asavoae. Timing analysis enhancement for synchronous program. In Workshop on Reconciling Performance and Predictability (REPP), 2014. [ .pdf ]

BibTex

Pascal Raymond. A general approach for expressing infeasibility in implicit path enumeration technique. In International Conference on Embedded Software (EMSOFT 2014), New Dehli, India, October 2014. [ DOI | .pdf ]

BibTex

Mihail Asavoae, Claire Maiza, and Pascal Raymond. Program semantics in model-based wcet analysis: A state of the art perspective. In Claire Maiza, editor, 13th International Workshop on Worst-Case Execution Time Analysis, WCET 2013, July 9, 2013, Paris, France, volume 30 of OASICS, pages 32–41. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. [ .pdf ]

BibTex

Florence Maraninchi, Nicolas Halbwachs, Pascal Raymond, Catherine Parent, and Rudrapatna K. Shyamasundar. Specification and validation of embedded systems: A case study of a fault-tolerant data acquisition system with lustre programming environment. CSI Journal of Computing, 1(4), September 2013.

BibTex

Franck Petit, Anissa Lamani, Stéphane Devismes, Sébastien Tixeuil, and Pascal Raymond. Explorer une grille avec un minimum de robots amnésiques. In Nicolas Nisse, Franck Rousseau, and Yann Busnel, editors, 15èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications (AlgoTel), pages 1–4, Pornic, France, May 2013. [ http ]

BibTex

Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, and Fabienne Carrier. Timing analysis enhancement for synchronous program. In RTNS, pages 141–150, 2013. [ .pdf ]

BibTex

Erwan Jahier, Nicolas Halbwachs, and Pascal Raymond. Engineering functional requirements of reactive systems using synchronous languages. In International Symposium on Industrial Embedded Systems, 2013. SIES'13., Porto, Portugal, 06 2013. [ .pdf ]

BibTex

Stéphane Devismes, Anissa Lamani, Franck Petit, Pascal Raymond, and Sébastien Tixeuil. Optimal grid exploration by asynchronous oblivious robots. In Sukumar Ghosh and Christian Scheideler, editors, 14th International Symposium on Stabilization, Safety, and Security of Distributed Systems, SSS, pages 64–76, Toronto, Canada, October 2012. LNCS.

BibTex

Marc Pouzet and Pascal Raymond. Modular static scheduling of synchronous data-flow networks. Design Automation for Embedded Systems, 14(3):165–192, 2010. [ DOI | http ]

Keywords: Real-time systems; Synchronous languages; Block-diagrams; Compilation; NP-completeness; Partial orders; Preorders

BibTex

Mouaiad Alras, Paul Caspi, Alain Girault, and Pascal Raymond. Model-based design of embeded control systems with a synchronous intermediate model. In 6th IEEE International Conference on Embedded Systems and Software (ICESS-09), Hangzhou, China, May 2009.

BibTex

Erwan Jahier, Nicolas Halbwachs, and Pascal Raymond. Synchronous modeling and validation of priority inheritance schedulers. In Fundamental Approaches to Software Engineering, FASE'09, York, U.K., March 2009. [ http ]

BibTex

Marc Pouzet and Pascal Raymond. Modular static scheduling of synchronous data-flow networks – an efficient symbolic representation. In International Conference on Embedded Software (EMSOFT'09), Grenoble, France, October 2009. [ .pdf ]

BibTex

Paul Caspi, Jean-louis Colao̧, Léonard Gérard, Marc Pouzet, and Pascal Raymond. Synchronous objects with scheduling policies, introducing safe shared memory in lustre. In ACM SIGPLAN/SIGBED 2009 Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2009), Dublin, Ireland, june 2009.

BibTex

Pascal Raymond. Synchronous program verification with lustre/lesar. In Stefan Mertz and Nicolas Navet, editors, Modeling and Verification of Real-Time Systems, chapter 6. ISTE/Wiley, 2008.

BibTex

Pascal Raymond, Yvan Roux, and Erwan Jahier. Lutin: a language for specifying and executing reactive scenarios. EURASIP Journal on Embedded Systems, 2008, 2008.

https://jes-eurasipjournals.springeropen.com/articles/10.1155/2008/753821. [ .pdf ]

BibTex

Erwan Jahier and Pascal Raymond. Generating random values using binary decision diagrams and convex polyhedra. In Barry O’Sullivan Frédéric Benhamou, editor, Trends in Constraint Programming, pages 349–356. ISTE, London, UK, May 2007. http://www.iste.co.uk/index.php?isbn=9781905209972. [ .pdf ]

BibTex

Paul Caspi, Pascal Raymond, and Stavros Tripakis. Synchronous languages. In Sang H. Son and Insup Lee, editors, Handbook of Real-Time And Embedded Systems. Chapman & Hall, 2007.

BibTex

Erwan Jahier, Nicolas Halbwachs, Pascal Raymond, Xavier Nicollin, and David Lesens. Virtual execution of aadl models via a translation into synchronous programs. In Christoph Kirsch and Reinhard Wilhelm, editors, Proceedings of the 7th ACM & IEEE International conference on Embedded software, EMSOFT 2007, September 30 - October 3, 2007, Salzburg, Austria, pages 134–143. ACM, 2007. [ http ]

BibTex

Pascal Raymond, Yvan Roux, and Erwan Jahier. Specifying and executing reactive scenarios with lutin. In SLA++P'07, ETAPS'07 Satellite Workshop on Model-driven High-level Programming of Embedded Systems, Braga, Portugal, March 2007. [ .pdf ]

BibTex

Paul Caspi, Pascal Raymond, and Stavros Tripakis. Synchronous programming. In Insup Lee, Joseph Y.-T. Leung, and Sang H. Son, editors, Handbook of Real-Time amd Embedded Systems, chapter 14. Chapman and Hall/CRC, 2007.

BibTex

Ludovic Samper, Florence Maraninchi, Laurent Mounier, Erwan Jahier, and Pascal Raymond. On the importance of modeling the environment when analyzing sensor networks. In 3rd International Workshop on Wireless Ad-hoc and Sensor Networks (IWWAN'06), New York, USA, June 2006.

BibTex

Erwan Jahier and Pascal Raymond. Generating random values using binary decision diagrams and convex polyhedra. In Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA'06), Nantes, France, 09 2006. http://www.irisa.fr/manifestations/2006/CSTVA06/. [ .pdf ]

BibTex

Pascal Raymond. Vérification de programmes synchrones avec lustre/lesar. In Nicolas Navet, editor, Systèmes temps réel 1 – techniques de description et de vérification, chapter 6. Hermes science – Lavoisier, 2006.

BibTex

Pascal Raymond, Erwan Jahier, and Yvan Roux. Describing and executing random reactive systems. In SEFM 2006, 4th IEEE International Conference on Software Engineering and Formal Methods, Pune, India, September 2006. [ .pdf ]

BibTex

Erwan Jahier, Pascal Raymond, and Philippe Baufreton. Case studies with lurette v2. Software Tools for Technology Transfer, 8(6):517–530, November 2006. [ .pdf ]

BibTex

Gordon Pace, Nicolas Halbwachs, and Pascal Raymond. Counter-example generation in symbolic abstract model-checking. Software Tools for Technology Transfer, 5(2), March 2004. [ http ]

BibTex

Erwan Jahier, Pascal Raymond, and Philippe Baufreton. Case studies with lurette v2. In 1st International Symposium on Leveraging Applications of Formal Methods, ISoLA 2004, Paphos, Cyprus, October 2004. [ .html ]

BibTex

Laure Gonnord, Nicolas Halbwachs, and Pascal Raymond. From discrete duration calculus to symbolic automata. In 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, Barcelona, Spain, March 2004. [ http ]

BibTex

Pascal Raymond and Yvan Roux. Describing non-deterministic reactive systems by means of regular expressions. In First Workshop on Synchronous Languages, Applications and Programming, SLAP'02, volume 65, Grenoble, April 2002. [ http ]

BibTex

Paul Caspi and Pascal Raymond. From control system design to embedded code: The synchronous data-flow approach. In IEEE-CDC, 2001.

BibTex

Gordon Pace, Nicolas Halbwachs, and Pascal Raymond. Counter-example generation in symbolic abstract model-checking. In 6th International Workshop on Formal Methods for Industrial Critical Systems, FMICS'2001, Paris, July 2001. Inria. [ .html ]

BibTex

David Lesens, Nicolas Halbwachs, and Pascal Raymond. Automatic verification of parameterized networks of processes. Theoretical Computer Science, 256(1):113–144, 2001. [ http ]

BibTex

Nicolas Halbwachs and Pascal Raymond. Validation of synchronous reactive systems: from formal verification to automatic testing. In ASIAN'99, Asian Computing Science Conference, Phuket (Thailand), December 1999. LNCS 1742, Springer Verlag. [ .html ]

BibTex

Bertrand Jeannet, Nicolas Halbwachs, and Pascal Raymond. Dynamic partitioning in analyses of numerical properties. In Static Analysis Symposium, SAS'99, Venezia (Italy), September 1999. LNCS 1694, Springer Verlag. [ .html ]

BibTex

Nicolas Halbwachs, Xavier Nicollin, Pascal Raymond, and Daniel Weber. Test automatique de systèmes réactifs. In Ecole d’été “MOdélisation et VÉrification des Processus parallèles, Nantes, July 1998.

BibTex

Pascal Raymond, Daniel Weber, Xavier Nicollin, and Nicolas Halbwachs. Automatic testing of reactive systems. In 19th IEEE Real-Time Systems Symposium, Madrid, Spain, December 1998. [ .html ]

BibTex

David Lesens, Nicolas Halbwachs, and Pascal Raymond. Automatic verification of parameterized linear networks of processes. In 24th ACM Symposium on Principles of Programming Languages, POPL'97, Paris, January 1997. [ .html ]

BibTex

David Lesens, Nicolas Halbwachs, and Pascal Raymond. Automatic construction of network invariants. In International Workshop on Verification of Infinite State Systems (INFINITY), Pisa, August 1996.

BibTex

Pascal Raymond. Recognizing regular expressions by means of dataflow networks. In Automata, Languages and Programming, 23rd International Colloquium, volume 1099 of Lecture Notes in Computer Science, pages 336–347, Paderborn, Germany, July 1996. Springer-Verlag.

BibTex

Fabienne Lagnier, Pascal Raymond, and Christian Dubois. Formal verification of a critical system written in saga/lustre. In Workshop on Formal Methods, Modelling and Simulation for System Engineering, St Quentin en Yvelines (France), february 1995.

BibTex

Christian Dubois, Paul Ghaleb, Fabienne Lagnier, and Pascal Raymond. Vérification de propriétés de programmes écrits en Lustre. In RTS'95, Paris, january 1995.

BibTex

Muriel Jourdan, Fabienne Lagnier, Pascal Raymond, and Florence Maraninchi. A multiparadigm language for reactive systems. In In 5th IEEE International Conference on Computer Languages, Toulouse, mai 1994. IEEE Computer Society Press.

BibTex

Nicolas Halbwachs, Yann-Eric Proy, and Pascal Raymond. Verification of linear hybrid systems by means of convex approximations. In Baudouin Le Charlier, editor, International Symposium on Static Analysis, SAS'94, Namur (Belgium), September 1994. LNCS 864, Springer Verlag. [ .html ]

BibTex

Nicolas Halbwachs, Fabienne Lagnier, and Pascal Raymond. Synchronous observers and the verification of reactive systems. In Maurice Nivat, C. Rattray, Teodor Rus, and Giuseppe Scollo, editors, Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93, Twente, June 1993. Workshops in Computing, Springer Verlag. [ .html ]

BibTex

Muriel Jourdan, Fabienne Lagnier, Florence Maraninchi, and Pascal Raymond. Embedding declarative subprograms into imperative constructs. In Fifth International Symposium on Programming Language Implementation and Logic Programming, Tallin, Estonia. Springer Verlag, LNCS 714, aout 1993.

BibTex

Ahmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs, and Pascal Raymond. Minimal state graph generation. Sci. Comput. Program., 18(3):247–269, 1992.

BibTex

Christophe Ratel, Nicolas Halbwachs, and Pascal Raymond. Programming and verifying critical systems by means of the synchronous data-flow programming language lustre. In ACM-SIGSOFT'91 Conference on Software for Critical Systems, New Orleans, December 1991.

BibTex

Nicolas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud. The synchronous data-flow programming language Lustre (extended abstract). In 1st European Control Conference, pages 1661–1665, Grenoble, July 1991.

BibTex

Nicolas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud. Programmation et vérification des systèmes réactifs: Le langage . Technique et Science Informatique, 10(2):139–158, 1991.

BibTex

Nicolas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud. The synchronous dataflow programming language . Proceedings of the IEEE, 79(9):1305–1320, September 1991. [ .html ]

BibTex

Nicolas Halbwachs, Pascal Raymond, and Christophe Ratel. Generating efficient code from data-flow programs. In Third International Symposium on Programming Language Implementation and Logic Programming, pages 207–218, Passau, August 1991. LNCS 528, Springer Verlag. [ .html ]

BibTex

Pascal Raymond. Compilation efficace d’un langage déclaratif synchrone : Le générateur de code Lustre-V3. Thèse, INPG, Grenoble, France, november 1991. [ http ]

BibTex

Pascal Raymond. Compilation séparée de programmes lustre. Technical report, Projet SPECTRE, IMAG, july 1988. [ .pdf ]

BibTex