@inproceedings{oulkaid:hal-04527225,
   title = {{A Transistor Level Relational Semantics for Electrical Rule Checking by SMT Solving}},
   author = {Oulkaid, Oussama and Ferres, Bruno and Moy, Matthieu and Raymond, Pascal and Khosravian, Mehdi and Henrio, Ludovic and Radanne, Gabriel},
   booktitle = {{Design, Automation and Test in Europe Conference}},
   address = {Valencia, Spain},
   month = {Mar},
   url = {https://hal.science/hal-04527225},
   team = {SYNC, axe_SharedResources},
   year = {2024},
   pdf = {https://hal.science/hal-04527225/file/date2024.pdf},
   hal_id = {hal-04527225},
   hal_version = {v1},
   keywords = {Formal Verification ; Integrated Circuits ; Electrical Rule Checking ; SMT Solving}
}

@inproceedings{ferres:hal-04007446,
   title = {{Electrical Rule Checking of Integrated Circuits using Satisfiability Modulo Theory}},
   author = {Ferres, Bruno and Oulkaid, Oussama and Henrio, Ludovic and Khosravian, Mehdi and Moy, Matthieu and Radanne, Gabriel and Raymond, Pascal},
   booktitle = {{DATE 2023 - Design, Automation and Test in Europe Conference}},
   address = {Anvers (Antwerpen), Belgium},
   month = {Apr},
   url = {https://hal.science/hal-04007446},
   team = {SYNC, axe_SharedResources},
   year = {2023},
   pdf = {https://hal.science/hal-04007446/file/date2023.pdf},
   hal_id = {hal-04007446},
   hal_version = {v1},
   keywords = {Electrical Rule Checking ; Integrated Circuits ; SMT Solving}
}

@article{DLPRT12j,
   title = {Terminating Exploration of a Grid by an Optimal Number of Asynchronous Oblivious Robots},
   author = {Devismes, St\'ephane and Lamani, Anissa and Petit, Franck and Raymond, Pascal and Tixeuil, S\'ebastien},
   journal = {The Computer Journal},
   month = {01},
   number = {1},
   pages = {132-154},
   url = {https://doi.org/10.1093/comjnl/bxz166},
   volume = {64},
   team = {SYNC, axe_SharedResources},
   year = {2021},
   doi = {10.1093/comjnl/bxz166},
   issn = {0010-4620}
}

@inproceedings{schuh:hal-03185800,
   title = {A study of predictable execution models implementation for industrial data-flow applications on a multi-core platform with shared banked memory},
   author = {Schuh, Matheus and Maiza, Claire and Goossens, Jo\"el and Raymond, Pascal and Dupont De Dinechin, Beno{\^i}t},
   booktitle = {2020 IEEE Real-Time Systems Symposium (RTSS)},
   address = {Houston, TX, United States},
   month = {Dec},
   url = {https://hal.archives-ouvertes.fr/hal-03185800},
   team = {SYNC},
   year = {2020},
   pdf = {https://hal.archives-ouvertes.fr/hal-03185800/file/schuh2020study.pdf},
   hal_id = {hal-03185800},
   hal_version = {v1}
}

@article{LITESLITES-v006-i001-a002,
   title = {Improving {WCET} Evaluation using Linear Relation Analysis},
   author = {Raymond, Pascal and Maiza, Claire and Parent-Vigouroux, Catherine and Jahier, Erwan and Halbwachs, Nicolas and Carrier, Fabienne and Asavoae, Mihail and Boutonnet, R\'emy},
   journal = {Leibniz Transactions on Embedded Systems},
   number = {1},
   pages = {02--1-02:28},
   url = {https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v006-i001-a002},
   volume = {6},
   team = {SYNC, PACSS, axe_SharedResources},
   year = {2019},
   doi = {10.4230/LITES-v006-i001-a002},
   issn = {2199-2002},
   keywords = {Worst Case Execution Time estimation; Infeasible Execution Paths; Abstract Interpretation},
   abstract = {The precision of a worst case execution time (WCET) evaluation tool on a given program is highly dependent on how the tool is able to detect and discard semantically infeasible executions of the program. In this paper, we propose to use the classical abstract interpretation-based method of linear relation analysis to discover and exploit relations between execution paths. For this purpose, we add auxiliary variables (counters) to the program to trace its execution paths. The results are easily incorporated in the classical workflow of a WCET evaluator, when the evaluator is based on the popular implicit path enumeration technique. We use existing tools - a WCET evaluator and a linear relation analyzer - to build and experiment a prototype implementation of this idea.}
}

@inproceedings{graillat:date18,
   title = {Parallel Code Generation of Synchronous Programs for a Many-core Architecture},
   author = {Graillat, Amaury and Moy, Matthieu and Raymond, Pascal and Dupont De Dinechin, Beno{\^i}t},
   booktitle = {{Design, Automation and Test in Europe}},
   address = {Dresden, Germany},
   month = {Mar},
   url = {https://hal.inria.fr/hal-01667594/file/date2018.pdf},
   team = {SYNC, axe_SharedResources},
   year = {2018}
}

@inproceedings{lo:erts2018,
   title = {Real-time on-Board Manycore Implementation of a Health Monitoring System: Lessons Learnt},
   author = {Lo, Moustapha and Valot, Nicolas and Maraninchi, Florence and Raymond, Pascal},
   booktitle = {9th European Congress Embedded Real Time Software and Systems (ERTS2 2018)},
   address = {Toulouse, France},
   month = {february},
   url = {https://www.erts2018.org/uploads/program/ERTS_2018_paper_7.pdf},
   team = {SYNC},
   year = {2018},
   select = {yes}
}

@inproceedings{maiza2017wcet,
   title = {The W-SEPT Project: Towards Semantic-Aware WCET Estimation},
   author = {Maiza, Claire and Raymond, Pascal and Parent-Vigouroux, Catherine and Bonenfant, Armelle and Carrier, Fabienne and Cass\'e, Hugues and Cuenot, Philippe and Claraz, Denis and Halbwachs, Nicolas and Jahier, Erwan and Li, Hanbing and Michiel, Marianne de and Mussot, Vincent and Puaut, Isabelle and Rochange, Christine and Rohou, Erven and Ruiz, Jordy and Sotin, Pascal and Sun, Wei-Tsun},
   editor = {Reineke, Jan},
   booktitle = {17th International Workshop on Worst-Case Execution Time Analysis (WCET 2017)},
   address = {Dagstuhl, Germany},
   annote = {Keywords: Worst-case execution time analysis, Static analysis, Program analysis},
   pages = {1--13},
   publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
   series = {OpenAccess Series in Informatics (OASIcs)},
   url = {http://drops.dagstuhl.de/opus/volltexte/2017/7309},
   volume = {57},
   team = {SYNC},
   year = {2017},
   doi = {10.4230/OASIcs.WCET.2017.9},
   isbn = {978-3-95977-057-6},
   issn = {2190-6807}
}

@inproceedings{bonenfant:hal-01235781,
   title = {When the worst-case execution time estimation gains from the application semantics},
   author = {Bonenfant, Armelle and Carrier, Fabienne and Cass\'e, Hugues and Cuenot, Philippe and Claraz, Denis and Halbwachs, Nicolas and Li, Hanbing and Maiza, Claire and De Michiel, Marianne and Mussot, Vincent and Parent-Vigouroux, Catherine and Puaut, Isabelle and Raymond, Pascal and Rohou, Erven and Sotin, Pascal},
   booktitle = {{8th European Congress on Embedded Real-Time Software and Systems}},
   address = {Toulouse, France},
   month = {Jan},
   url = {https://hal.inria.fr/hal-01235781},
   team = {SYNC, PACSS},
   year = {2016}
}

@inproceedings{lo:hal-01718139,
   title = {Implementing a Real-time Avionic Application on a Many-core Processor},
   author = {Lo, Moustapha and Valot, Nicolas and Maraninchi, Florence and Raymond, Pascal},
   booktitle = {{42nd European Rotorcraft Forum (ERF)}},
   address = {Lille, France},
   month = {Sep},
   url = {https://hal.archives-ouvertes.fr/hal-01718139/file/ERF2016_063.pdf},
   team = {SYNC},
   year = {2016},
   pdf = {https://hal.archives-ouvertes.fr/hal-01718139/file/ERF2016_063.pdf},
   hal_id = {hal-01718139},
   hal_version = {v1},
   keywords = {many-core ; avionics ; health monitoring}
}

@article{RMPCA-RTS15,
   title = {Timing analysis enhancement for synchronous program},
   author = {Raymond, Pascal and Maiza, Claire and Parent-Vigouroux, Catherine and Carrier, Fabienne and Asavoae, Mihail},
   journal = {Real-Time Systems},
   pages = {1-29},
   publisher = {Springer US},
   url = {http://dx.doi.org/10.1007/s11241-015-9219-y},
   team = {SYNC},
   year = {2015},
   doi = {10.1007/s11241-015-9219-y},
   issn = {0922-6443},
   select = {yes},
   abstract = {Real-time critical systems can be considered as correct if they compute both right and fast enough. Functionality aspects (computing right) can be addressed using high level design methods, such as the synchronous approach that provides languages, compilers and verification tools. Real-time aspects (computing fast enough) can be addressed with static timing analysis, that aims at discovering safe bounds on the Worst-Case Execution Time (WCET) of the binary code. In this paper, we aim at improving the estimated WCET in the case where the binary code comes from a high-level synchronous design. The key idea is that some high-level functional properties may imply that some execution paths of the binary code are actually infeasible, and thus, can be removed from the worst-case candidates. In order to automatize the method, we show (1) how to trace semantic information between the high-level design and the executable code, (2) how to use a model-checker to prove infeasibility of some execution paths, and (3) how to integrate such infeasibility information into an existing timing analysis framework. Based on a realistic example, we show that there is a large possible improvement for a reasonable computation time overhead.}
}

@inproceedings{Maiza_OPRTC2014,
   title = {Schedulability and modular analysis: how to fit timing model?},
   author = {Cass\'e, Hugues and Maiza, Claire and and Parent-Vigouroux, Catherine and Raymond, Pascal},
   booktitle = {OPRTC},
   url = {http://www-verimag.imag.fr/PUBLIS/uploads/elvyt3392.pdf},
   team = {SYNC},
   year = {2014}
}

@incollection{MRR-ISTE14,
   title = {Estimation de temps d'ex\'ecution et d\'elais},
   author = {Maiza, Claire and Rochange, Christine and Raymond, Pascal},
   editor = {Chetto, Maryline},
   booktitle = {Ordonnancement dans les syst\`emes temps r\'eel},
   chapter = {13},
   pages = {365-392},
   publisher = {ISTE editions},
   team = {SYNC},
   year = {2014}
}

@incollection{MRR-ISTE14-ENG,
   title = {Estimation of Execution Time and Delays},
   author = {Maiza, Claire and Rochange, Christine and Raymond, Pascal},
   editor = {Chetto, Maryline},
   booktitle = {Real-time Systems Scheduling 1},
   chapter = {5},
   month = {august},
   pages = {193-230},
   publisher = {ISTE editions},
   url = {http://www.iste.co.uk/index.php?p=a&ACTION=View&id=744},
   team = {SYNC},
   year = {2014},
   isbn = {9781848216655}
}

@inproceedings{Raymond_REPP2014,
   title = {Timing analysis enhancement for synchronous program},
   author = {Raymond, Pascal and Maiza, Claire and Parent-Vigouroux, Catherine and Carrier, Fabienne and Asavoae, Mihail},
   booktitle = {Workshop on Reconciling Performance and Predictability (REPP)},
   url = {http://www-verimag.imag.fr/PUBLIS/uploads/kihec5769.pdf},
   team = {SYNC},
   year = {2014}
}

@inproceedings{raymond-emsoft14,
   title = {A General Approach for Expressing Infeasibility in Implicit Path Enumeration Technique},
   author = {Raymond, Pascal},
   booktitle = {International Conference on Embedded Software (EMSOFT 2014)},
   address = {New Dehli, India},
   month = oct,
   url = {https://hal.science/hal-04680351},
   team = {SYNC, axe_SharedResources},
   year = {2014},
   doi = {10.1145/2656045.2656046},
   select = {yes},
   abstract = {Static timing analysis aims at computing a guaranteed upper bound to the Worst-Case Execution Time (WCET) of a program. It requires both an accurate modeling of the hardware, and a precise analysis of the program in order to reject infeasible executions (in particular, all infinite ones). For the actual computation of the worst-case execution, most of the existing tools and methods are based on the Implicit Path Enumeration Technique (IPET), which consist in encoding this search into a numerical optimization problem (Integer Linear Programming, ILP). An interest of this approach is that it naturally integrates the loop bounds. It also allows to implicitly prune infeasible paths, as far as they can be expressed using linear constraints. Several works on the subject are using this ability in order to enhance the WCET estimation: they identify specific property patterns (e.g., implications, exclusions) and propose ad hoc translation into numerical constraints. The goal of this paper is to go further than ad hoc reasoning by proposing a general method for translating infeasibility in terms of numerical constraints. It does not address the problem of finding infeasible paths, only the one of characterizing them as precisely as possible. Moreover the paper aims at exploring the limits of the method, and thus, it does not try to enhance the result using additional methods (e.g., graph transformation).}
}

@inproceedings{Asavoae-wcet2013,
   title = {Program Semantics in Model-Based WCET Analysis: A State of the Art Perspective},
   author = {Asavoae, Mihail and Maiza, Claire and Raymond, Pascal},
   editor = {Maiza, Claire},
   booktitle = {13th International Workshop on Worst-Case Execution Time Analysis, WCET 2013, July 9, 2013, Paris, France},
   pages = {32-41},
   publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
   series = {OASICS},
   url = {http://www-verimag.imag.fr/PUBLIS/uploads/rhdhu7986.pdf},
   volume = {30},
   team = {SYNC},
   year = {2013},
   isbn = {978-3-939897-54-5}
}

@article{GYRO-journal13,
   title = {Specification and Validation of Embedded Systems: A Case Study of a Fault-Tolerant Data Acquisition System with Lustre Programming environment},
   author = {Maraninchi, Florence and Halbwachs, Nicolas and Raymond, Pascal and Parent, Catherine and Shyamasundar, Rudrapatna K.},
   journal = {CSI Journal of Computing},
   month = sep,
   number = {4},
   publisher = {The computer Society of India},
   volume = {1},
   team = {SYNC},
   year = {2013}
}

@inproceedings{petit:hal-00817123,
   title = {{Explorer une grille avec un minimum de robots amn{\'e}siques}},
   author = {Petit, Franck and Lamani, Anissa and Devismes, St\'ephane and Tixeuil, S\'ebastien and Raymond, Pascal},
   editor = {Nisse, Nicolas and Rousseau, Franck and Busnel, Yann},
   booktitle = {{15{\`e}mes Rencontres Francophones sur les Aspects Algorithmiques des T{\'e}l{\'e}communications (AlgoTel)}},
   address = {Pornic, France},
   month = {May},
   pages = {1-4},
   url = {http://hal.archives-ouvertes.fr/hal-00817123},
   team = {SYNC},
   year = {2013}
}

@inproceedings{raymond_rtns2013,
   title = {Timing analysis enhancement for synchronous program},
   author = {Raymond, Pascal and Maiza, Claire and Parent-Vigouroux, Catherine and Carrier, Fabienne},
   booktitle = {RTNS},
   pages = {141-150},
   url = {http://www-verimag.imag.fr/PUBLIS/uploads/ovcuf5189.pdf},
   team = {SYNC},
   year = {2013}
}

@inproceedings{sies2013,
   title = {Engineering Functional Requirements of Reactive Systems using Synchronous Languages},
   author = {Jahier, Erwan and Halbwachs, Nicolas and Raymond, Pascal},
   booktitle = {International Symposium on Industrial Embedded Systems, 2013. SIES'13.},
   address = {Porto, Portugal},
   month = {06},
   url = {http://www-verimag.imag.fr/~jahier/publis/sies2013-jhr.pdf},
   team = {SYNC},
   year = {2013}
}

@inproceedings{DLPRT12c,
   title = {Optimal Grid Exploration by Asynchronous Oblivious Robots},
   author = {Devismes, St\'ephane and Lamani, Anissa and Petit, Franck and Raymond, Pascal and Tixeuil, S\'ebastien},
   editor = {Ghosh, Sukumar and Scheideler, Christian},
   booktitle = {14th International Symposium on Stabilization, Safety, and Security of Distributed Systems, SSS},
   address = {Toronto, Canada},
   month = {October},
   pages = {64-76},
   publisher = {LNCS},
   team = {SYNC},
   year = {2012}
}

@article{staticsched10,
   title = {Modular static scheduling of synchronous data-flow networks},
   author = {Pouzet, Marc and Raymond, Pascal},
   journal = {Design Automation for Embedded Systems},
   month = {Jun},
   number = {3},
   pages = {165-192},
   publisher = {{Springer Verlag}},
   url = {https://hal.science/hal-04679268},
   volume = {14},
   team = {SYNC},
   year = {2010},
   doi = {10.1007/s10617-010-9053-3},
   pdf = {https://hal.science/hal-04679268/file/pouzet-raymond-09.pdf},
   hal_id = {hal-04679268},
   hal_version = {v1},
   keywords = {Algorithms ; Languages ; Theory Real-time systems ; Synchronous languages ; Block-diagrams ; Compilation ; NP-completeness ; Partial orders ; Preorders}
}

@inproceedings{alras-icess09,
   title = {Model-Based Design of Embeded Control Systems with a Synchronous Intermediate Model},
   author = {Alras, Mouaiad and Caspi, Paul and Girault, Alain and Raymond, Pascal},
   booktitle = {6th IEEE International Conference on Embedded Systems and Software (ICESS-09)},
   address = {Hangzhou, China},
   month = may,
   team = {SYNC},
   year = {2009}
}

@inproceedings{ejnhpr-fase09,
   title = {Synchronous Modeling and Validation of Priority Inheritance Schedulers},
   author = {Jahier, Erwan and Halbwachs, Nicolas and Raymond, Pascal},
   booktitle = {Fundamental Approaches to Software Engineering, FASE'09},
   address = {York, U.K.},
   month = mar,
   url = {http://hal.archives-ouvertes.fr/hal-00384389/fr/},
   team = {SYNC},
   year = {2009}
}

@inproceedings{emsoft09,
   title = {Modular Static Scheduling of Synchronous Data-flow Networks -- An efficient symbolic representation},
   author = {Pouzet, Marc and Raymond, Pascal},
   booktitle = {International Conference on Embedded Software (EMSOFT'09)},
   address = {Grenoble, France},
   month = oct,
   url = {http://www-verimag.imag.fr/~raymond/publis/emsoft09.pdf},
   team = {SYNC},
   year = {2009}
}

@inproceedings{pouzet-lctess09,
   title = {Synchronous Objects with Scheduling Policies, Introducing safe shared memory in Lustre},
   author = {Caspi, Paul and Cola\c{o}, Jean-louis and G\'erard, L\'eonard and Pouzet, Marc and Raymond, Pascal},
   booktitle = {ACM SIGPLAN/SIGBED 2009 Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2009)},
   address = {Dublin, Ireland},
   month = {june},
   team = {SYNC},
   year = {2009}
}

@incollection{lesar-wiley,
   title = {Synchronous Program Verification with Lustre/Lesar},
   author = {Raymond, Pascal},
   editor = {Mertz, Stefan and Navet, Nicolas},
   booktitle = {Modeling and Verification of Real-Time Systems},
   chapter = {6},
   publisher = {ISTE/Wiley},
   team = {SYNC},
   year = {2008}
}

@article{lutin,
   title = {Lutin: a language for specifying and executing reactive scenarios},
   author = {Raymond, Pascal and Roux, Yvan and Jahier, Erwan},
   journal = {EURASIP Journal on Embedded Systems},
   note = {https://jes-eurasipjournals.springeropen.com/articles/10.1155/2008/753821},
   url = {https://jes-eurasipjournals.springeropen.com/track/pdf/10.1155/2008/753821.pdf},
   volume = {2008},
   team = {SYNC},
   year = {2008}
}

@incollection{cstva-book-jr07,
   title = {Generating Random Values Using Binary Decision Diagrams and Convex Polyhedra},
   author = {Jahier, Erwan and Raymond, Pascal},
   editor = {Benhamou, Barry O'Sullivan Fr\'ed\'eric},
   booktitle = {Trends in Constraint Programming},
   address = {London, UK},
   month = may,
   note = {http://www.iste.co.uk/index.php?isbn=9781905209972},
   pages = {349--356},
   publisher = {ISTE},
   url = {http://www-verimag.imag.fr/~jahier/cstva06-jahier-raymond.pdf},
   team = {SYNC},
   year = {2007},
   isbn = {9781905209972}
}

@incollection{hdbk2,
   title = {Synchronous languages},
   author = {Caspi, Paul and Raymond, Pascal and Tripakis, Stavros},
   editor = {Son, Sang H. and Lee, Insup},
   booktitle = {Handbook of Real-Time And Embedded Systems},
   publisher = {Chapman {\&} Hall},
   team = {SYNC},
   year = {2007}
}

@inproceedings{JahierHRNL07,
   title = {Virtual execution of AADL models via a translation into synchronous programs},
   author = {Jahier, Erwan and Halbwachs, Nicolas and Raymond, Pascal and Nicollin, Xavier and Lesens, David},
   editor = {Kirsch, Christoph and Wilhelm, Reinhard},
   booktitle = {Proceedings of the 7th ACM {\&} IEEE International conference on Embedded software, EMSOFT 2007, September 30 - October 3, 2007, Salzburg, Austria},
   pages = {134-143},
   publisher = {ACM},
   url = {http://hal.archives-ouvertes.fr/hal-00189563/en/},
   team = {SYNC},
   year = {2007},
   isbn = {978-1-59593-825-1}
}

@inproceedings{slap07,
   title = {Specifying and executing reactive scenarios with Lutin},
   author = {Raymond, Pascal and Roux, Yvan and Jahier, Erwan},
   booktitle = {SLA++P'07, ETAPS'07 Satellite Workshop on Model-driven High-level Programming of Embedded Systems},
   address = {Braga, Portugal},
   month = mar,
   url = {http://www-verimag.imag.fr/~jahier/slap-2007.pdf},
   team = {SYNC},
   year = {2007}
}

@incollection{synch-handbook,
   title = {Synchronous Programming},
   author = {Caspi, Paul and Raymond, Pascal and Tripakis, Stavros},
   editor = {Lee, Insup and Leung, Joseph Y.-T. and Son, Sang H.},
   booktitle = {Handbook of Real-Time amd Embedded Systems},
   chapter = {14},
   publisher = {Chapman and Hall/CRC},
   team = {SYNC},
   year = {2007}
}

@inproceedings{IWWAN06,
   title = {On the Importance of Modeling the Environment when Analyzing Sensor Networks},
   author = {Samper, Ludovic and Maraninchi, Florence and Mounier, Laurent and Jahier, Erwan and Raymond, Pascal},
   booktitle = {3rd International Workshop on Wireless Ad-hoc and Sensor Networks (IWWAN'06)},
   address = {New York, USA},
   month = jun,
   team = {SYNC,PACSS},
   year = {2006}
}

@inproceedings{jahier-cstva06,
   title = {Generating Random Values Using Binary Decision Diagrams and Convex Polyhedra},
   author = {Jahier, Erwan and Raymond, Pascal},
   booktitle = {Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA'06)},
   address = {{N}antes, {F}rance},
   month = {09},
   note = {http://www.irisa.fr/manifestations/2006/CSTVA06/},
   url = {http://www-verimag.imag.fr/~jahier/cstva06-jahier-raymond.pdf},
   team = {SYNC},
   year = {2006}
}

@incollection{lesar-hermes,
   title = {V\'erification de programmes synchrones avec Lustre/Lesar},
   author = {Raymond, Pascal},
   editor = {Navet, Nicolas},
   booktitle = {Syst\`emes temps r\'eel 1 -- techniques de description et de v\'erification},
   chapter = {6},
   publisher = {Hermes science -- Lavoisier},
   team = {SYNC},
   year = {2006}
}

@inproceedings{lucky-sefm06,
   title = {Describing and executing random reactive systems},
   author = {Raymond, Pascal and Jahier, Erwan and Roux, Yvan},
   booktitle = {SEFM 2006, 4th IEEE International Conference on Software Engineering and Formal Methods},
   address = {Pune, India},
   month = sep,
   url = {http://www-verimag.imag.fr/~jahier/sefm06.pdf},
   team = {SYNC},
   year = {2006}
}

@article{sttt06,
   title = {Case Studies with Lurette V2},
   author = {Jahier, Erwan and Raymond, Pascal and Baufreton, Philippe},
   journal = {Software Tools for Technology Transfer},
   month = nov,
   number = {6},
   pages = {517--530},
   url = {http://www.springerlink.com/content/u02131123x856227/fulltext.pdf},
   volume = {8},
   team = {SYNC},
   year = {2006}
}

@article{fmics-sttt,
   title = {Counter-example generation in symbolic abstract model-checking},
   author = {Pace, Gordon and Halbwachs, Nicolas and Raymond, Pascal},
   journal = {Software Tools for Technology Transfer},
   month = mar,
   number = {2},
   url = {http://hal.archives-ouvertes.fr/hal-00199168/en/},
   volume = {5},
   team = {SYNC},
   year = {2004}
}

@inproceedings{isola04,
   title = {Case Studies with Lurette V2},
   author = {Jahier, Erwan and Raymond, Pascal and Baufreton, Philippe},
   booktitle = {1st International Symposium on Leveraging Applications of Formal Methods, ISoLA 2004},
   address = {Paphos, Cyprus},
   month = oct,
   url = {http://www-verimag.imag.fr/~jahier/publis/isola04.html},
   team = {SYNC},
   year = {2004}
}

@inproceedings{slap04,
   title = {From Discrete Duration Calculus to Symbolic Automata},
   author = {Gonnord, Laure and Halbwachs, Nicolas and Raymond, Pascal},
   booktitle = {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},
   address = {Barcelona, Spain},
   month = mar,
   url = {http://hal.archives-ouvertes.fr/hal-00198433/en/},
   team = {SYNC},
   year = {2004}
}

@inproceedings{lutin-slap,
   title = {Describing Non-Deterministic Reactive Systems by Means of Regular Expressions},
   author = {Raymond, Pascal and Roux, Yvan},
   booktitle = {First Workshop on Synchronous Languages, Applications and Programming, SLAP'02},
   address = {Grenoble},
   journal = {Electr. Notes Theor. Comput. Sci.},
   month = apr,
   number = {5},
   url = {http://www.elsevier.com/gej-ng/31/29/23/117/53/show/Products/notes/index.htt\#005},
   volume = {65},
   team = {SYNC},
   year = {2002}
}

@inproceedings{cdc2001,
   title = {From Control System Design to Embedded Code: The Synchronous Data-Flow Approach},
   author = {Caspi, Paul and Raymond, Pascal},
   booktitle = {IEEE-CDC},
   team = {SYNC},
   year = {2001}
}

@inproceedings{fmics01,
   title = {Counter-example generation in symbolic abstract model-checking},
   author = {Pace, Gordon and Halbwachs, Nicolas and Raymond, Pascal},
   booktitle = {6th International Workshop on Formal Methods for Industrial Critical Systems, FMICS'2001},
   address = {Paris},
   month = jul,
   publisher = {Inria},
   url = {http://www-verimag.imag.fr/PEOPLE/Nicolas.Halbwachs/fmics01.html},
   team = {SYNC},
   year = {2001}
}

@article{tcs01,
   title = {Automatic Verification of Parameterized Networks of Processes},
   author = {Lesens, David and Halbwachs, Nicolas and Raymond, Pascal},
   journal = {Theoretical Computer Science},
   number = {1},
   pages = {113--144},
   url = {http://hal.archives-ouvertes.fr/hal-00198649/en/},
   volume = {256},
   team = {SYNC},
   year = {2001}
}

@inproceedings{asian99,
   title = {Validation of Synchronous Reactive Systems: from Formal Verification to Automatic Testing},
   author = {Halbwachs, Nicolas and Raymond, Pascal},
   booktitle = {ASIAN'99, Asian Computing Science Conference},
   address = {Phuket (Thailand)},
   month = dec,
   publisher = {LNCS 1742, Springer Verlag},
   url = {http://www-verimag.imag.fr/PEOPLE/Nicolas.Halbwachs/asian99.html},
   team = {SYNC},
   year = {1999}
}

@inproceedings{sas99,
   title = {Dynamic Partitioning in Analyses of Numerical Properties},
   author = {Jeannet, Bertrand and Halbwachs, Nicolas and Raymond, Pascal},
   booktitle = {Static Analysis Symposium, SAS'99},
   address = {Venezia (Italy)},
   month = sep,
   publisher = {LNCS 1694, Springer Verlag},
   url = {http://www-verimag.imag.fr/PEOPLE/Nicolas.Halbwachs/sas99.html},
   team = {SYNC},
   year = {1999}
}

@inproceedings{lurette-movep,
   title = {Test automatique de syst\`emes r\'eactifs},
   author = {Halbwachs, Nicolas and Nicollin, Xavier and Raymond, Pascal and Weber, Daniel},
   booktitle = {Ecole d'\'et\'e ``MOd\'elisation et V\'Erification des Processus parall\`eles},
   address = {Nantes},
   month = jul,
   team = {SYNC},
   year = {1998}
}

@inproceedings{lurette:rtss,
   title = {Automatic Testing of Reactive Systems},
   author = {Raymond, Pascal and Weber, Daniel and Nicollin, Xavier and Halbwachs, Nicolas},
   booktitle = {19th IEEE Real-Time Systems Symposium},
   address = {Madrid, Spain},
   month = dec,
   url = {http://www-verimag.imag.fr/PEOPLE/Nicolas.Halbwachs/rtss98.html},
   team = {SYNC},
   year = {1998}
}

@inproceedings{lesens:popl,
   title = {Automatic Verification of Parameterized Linear Networks of Processes},
   author = {Lesens, David and Halbwachs, Nicolas and Raymond, Pascal},
   booktitle = {24th ACM Symposium on Principles of Programming Languages, POPL'97},
   address = {Paris},
   month = jan,
   url = {http://www-verimag.imag.fr/PEOPLE/Nicolas.Halbwachs/popl97.html},
   team = {SYNC},
   year = {1997}
}

@inproceedings{lesens96,
   title = {Automatic Construction of Network Invariants},
   author = {Lesens, David and Halbwachs, Nicolas and Raymond, Pascal},
   booktitle = {International Workshop on Verification of Infinite State Systems (INFINITY)},
   address = {Pisa},
   month = aug,
   team = {SYNC},
   year = {1996}
}

@inproceedings{reglo:icalp96,
   title = {Recognizing Regular Expressions by Means of Dataflow Networks},
   author = {Raymond, Pascal},
   booktitle = {Automata, Languages and Programming, 23rd International Colloquium},
   address = {Paderborn, Germany},
   month = jul,
   pages = {336--347},
   publisher = {Springer-Verlag},
   series = {Lecture Notes in Computer Science},
   volume = {1099},
   team = {SYNC},
   year = {1996}
}

@inproceedings{lagnier95,
   title = {Formal verification of a critical system written in {\sc Saga/Lustre}},
   author = {Lagnier, Fabienne and Raymond, Pascal and Dubois, Christian},
   booktitle = {Workshop on Formal Methods, Modelling and Simulation for System Engineering},
   address = {St Quentin en Yvelines (France)},
   month = {february},
   team = {SYNC},
   year = {1995}
}

@inproceedings{lesar:rts95,
   title = {V\'erification de propri\'et\'es de programmes \'ecrits en {Lustre}},
   author = {Dubois, Christian and Ghaleb, Paul and Lagnier, Fabienne and Raymond, Pascal},
   booktitle = {RTS'95},
   address = {Paris},
   month = {january},
   team = {SYNC},
   year = {1995}
}

@inproceedings{Argos-Lustre-ICCL94,
   title = {A Multiparadigm Language for Reactive Systems},
   author = {Jourdan, Muriel and Lagnier, Fabienne and Raymond, Pascal and Maraninchi, Florence},
   booktitle = {In 5th IEEE International Conference on Computer Languages},
   address = {Toulouse},
   month = {mai},
   publisher = {IEEE Computer Society Press},
   team = {SYNC},
   year = {1994}
}

@inproceedings{halbwachs94b,
   title = {Verification of linear hybrid systems by means of convex approximations},
   author = {Halbwachs, Nicolas and Proy, Yann-Eric and Raymond, Pascal},
   editor = {Le Charlier, Baudouin},
   booktitle = {International Symposium on Static Analysis, SAS'94},
   address = {Namur (Belgium)},
   month = sep,
   publisher = {LNCS 864, Springer Verlag},
   url = {http://www-verimag.imag.fr/PEOPLE/Nicolas.Halbwachs/hybrid.html},
   team = {SYNC},
   year = {1994}
}

@inproceedings{Argos-Lustre-PLILP93,
   title = {Embedding declarative subprograms into imperative constructs},
   author = {Jourdan, Muriel and Lagnier, Fabienne and Maraninchi, Florence and Raymond, Pascal},
   booktitle = {Fifth International Symposium on Programming Language Implementation and Logic Programming, {\em Tallin, Estonia}},
   month = {aout},
   publisher = {Springer Verlag, LNCS 714},
   team = {SYNC},
   year = {1993}
}

@inproceedings{observers-amast93,
   title = {{Synchronous Observers and the Verification of Reactive Systems}},
   author = {Halbwachs, Nicolas and Lagnier, Fabienne and Raymond, Pascal},
   editor = {Nivat, M. and Rattray, C. and Rus, T. and Scollo, G.},
   booktitle = {{Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93}},
   address = {Twente, Netherlands},
   month = {Jun},
   pages = {83-96},
   publisher = {{Springer London}},
   series = {Workshops in Computing},
   url = {https://hal.science/hal-04683965},
   team = {SYNC, PACSS},
   year = {1993},
   doi = {10.1007/978-1-4471-3227-1_8},
   pdf = {https://hal.science/hal-04683965/file/amast93-pp.pdf},
   hal_id = {hal-04683965},
   hal_version = {v1}
}

@article{DBLP:journals/scp/BouajjaniFHR92,
   title = {Minimal State Graph Generation},
   author = {Bouajjani, Ahmed and Fernandez, Jean-Claude and Halbwachs, Nicolas and Raymond, Pascal},
   journal = {Sci. Comput. Program.},
   number = {3},
   pages = {247-269},
   volume = {18},
   team = {DCS, SYNC},
   year = {1992}
}

@inproceedings{lesar-sigsoft,
   title = {Programming and verifying critical systems by means of the synchronous data-flow programming language {\sc Lustre}},
   author = {Ratel, Christophe and Halbwachs, Nicolas and Raymond, Pascal},
   booktitle = {ACM-SIGSOFT'91 Conference on Software for Critical Systems},
   address = {New Orleans},
   month = dec,
   team = {SYNC},
   year = {1991}
}

@inproceedings{lustre-ecc,
   title = {The synchronous data-flow programming language {Lustre} (extended abstract)},
   author = {Halbwachs, Nicolas and Caspi, Paul and Raymond, Pascal and Pilaud, Daniel},
   booktitle = {1st European Control Conference},
   address = {Grenoble},
   month = jul,
   pages = {1661--1665},
   team = {SYNC},
   year = {1991}
}

@article{lustre-tsi,
   title = {Programmation et V\'erification des syst\`emes r\'eactifs: Le langage \lustre},
   author = {Halbwachs, Nicolas and Caspi, Paul and Raymond, Pascal and Pilaud, Daniel},
   journal = {Technique et Science Informatique},
   number = {2},
   pages = {139--158},
   volume = {10},
   team = {SYNC},
   year = {1991}
}

@article{lustre:ieee,
   title = {The synchronous dataflow programming language \lustre},
   author = {Halbwachs, Nicolas and Caspi, Paul and Raymond, Pascal and Pilaud, Daniel},
   journal = {Proceedings of the IEEE},
   month = sep,
   number = {9},
   pages = {1305-1320},
   url = {http://www-verimag.imag.fr/PEOPLE/Nicolas.Halbwachs/lustre-ieee.html},
   volume = {79},
   team = {SYNC},
   year = {1991}
}

@inproceedings{lustre:plilp,
   title = {Generating Efficient Code From Data-Flow Programs},
   author = {Halbwachs, Nicolas and Raymond, Pascal and Ratel, Christophe},
   booktitle = {Third International Symposium on Programming Language Implementation and Logic Programming},
   address = {Passau},
   month = aug,
   pages = {207--218},
   publisher = {LNCS 528, Springer Verlag},
   url = {http://www-verimag.imag.fr/PEOPLE/Nicolas.Halbwachs/lustre-plilp.html},
   team = {SYNC},
   year = {1991}
}

@phdthesis{raymond91,
   title = {Compilation efficace d'un langage d\'eclaratif synchrone~: Le g\'en\'erateur de code Lustre-V3},
   author = {Raymond, Pascal},
   address = {Grenoble, France},
   institution = {Institut National Polytechnique de Grenoble},
   type = {Th\`ese},
   month = {november},
   school = {INPG},
   url = {https://hal.archives-ouvertes.fr/tel-00198546},
   team = {SYNC},
   year = {1991}
}

@techreport{spectre-L5,
   title = {Compilation s\'epar\'ee de programmes Lustre},
   author = {Raymond, Pascal},
   institution = {Projet SPECTRE, IMAG},
   month = {july},
   url = {http://www-verimag.imag.fr/~raymond/publis/spectre-L5.pdf},
   team = {SYNC},
   year = {1988}
}