Program Logics for Certified Compilers, 2014. ,
DOI : 10.1017/CBO9781107256552
Compilation certifiée de SCADE/LUSTRE, 2013. ,
A formalization and proof of a modular Lustre code generator. Draft, 2013. ,
OTAWA: An Open Toolbox for Adaptive WCET Analysis, 8th IFIP WG 10.2 International Workshop on Software Technologies for Embedded and Ubiquitous Systems, pp.35-46, 2010. ,
DOI : 10.1007/978-3-642-16256-5_6
URL : https://hal.archives-ouvertes.fr/hal-01055378
Loosely Time-Triggered Architectures, ACM Transactions on Embedded Computing Systems, vol.15, issue.4, 2016. ,
DOI : 10.1145/2932189
URL : https://hal.archives-ouvertes.fr/hal-01408224
A hybrid synchronous language with hierarchical automata, Proceedings of the ninth ACM international conference on Embedded software, EMSOFT '11, pp.137-147, 2011. ,
DOI : 10.1145/2038642.2038664
URL : https://hal.archives-ouvertes.fr/hal-00654113
Divide and recycle: Types and compilation for a hybrid synchronous language, Proceedings of the 12th ACM SIGPLAN Conference on Languages, Compilers, and Tools for Embedded Systems, pp.61-70, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00654112
Clockdirected modular code generation for synchronous data-flow languages, Proceedings of the 9th ACM SIGPLAN Conference on Languages, Compilers, and Tools for Embedded Systems, pp.121-130, 2008. ,
DOI : 10.1145/1379023.1375674
Mechanized Semantics for the Clight Subset of the C Language, Journal of Automated Reasoning, vol.29, issue.6, pp.263-288, 2009. ,
DOI : 10.1007/s10817-009-9148-3
URL : https://hal.archives-ouvertes.fr/inria-00352524
Formal Verification of a C Compiler Front-End, Proceedings of the 14th International Symposium on Formal Methods, pp.460-475, 2006. ,
DOI : 10.1007/11813040_31
URL : https://hal.archives-ouvertes.fr/inria-00106401
The Landing Gear System Case Study, ABZ 2014: The Landing Gear Case Study?Proceedings of the Case Study Track at the 4th International Conference on Abstract State Machines, 2014. ,
DOI : 10.1007/978-3-319-07512-9_1
Certifying Synchrony for Free, Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, pp.495-506, 2001. ,
DOI : 10.1007/3-540-45653-8_34
LUSTRE: A declarative language for programming synchronous systems, Proceedings of the 14th ACM SIGPLAN-SIGACT Symposium on Principles Of Programming Languages, pp.178-188, 1987. ,
DOI : 10.1145/41625.41641
About the Design of Distributed Control Systems: The Quasi-Synchronous Approach, Proceedings of the International Conference on Computer Safety, Reliability and Security (SAFECOMP'01), number 2187 in Lecture Notes in Computer Science, pp.215-226, 2001. ,
DOI : 10.1007/3-540-45416-0_21
From Simulink to SCADE/Lustre to TTA: a layered approach for distributed embedded applications, Proceedings of the 4th ACM SIGPLAN Conference on Languages, Compilers, and Tools for Embedded Systems, pp.153-162, 2003. ,
DOI : 10.1145/780753.780754
CoCoSpec: A Mode-Aware Contract Language for Reactive Systems, Proceedings of the 14th International Conference on Software Engineering and Formal Methods, pp.347-366, 2016. ,
DOI : 10.1007/978-3-319-41591-8_24
The Kind 2 Model Checker, Proceedings of the 28th International Conference on Computer Aided Verification Part II, pp.510-517, 2016. ,
DOI : 10.1007/978-3-319-41540-6_29
Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant, 2013. ,
Clocks as First Class Abstract Types, Proceedings of the 3rd International Conference on Embedded Software (EMSOFT 2003), pp.134-155, 2003. ,
DOI : 10.1007/978-3-540-45212-6_10
A conservative extension of synchronous data-flow with state machines, Proceedings of the 5th ACM international conference on Embedded software , EMSOFT '05, pp.173-182, 2005. ,
DOI : 10.1145/1086228.1086261
Hardware Verification Using Co-induction in COQ, Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, pp.91-108, 1999. ,
DOI : 10.1007/3-540-48256-3_7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.6015
Compilation of synchronous observers as code contracts, Proceedings of the 30th Annual ACM Symposium on Applied Computing, SAC '15, pp.1933-1939, 2015. ,
DOI : 10.1145/2695664.2695819
A modular memory optimization for synchronous data-flow languages, Proceedings of the 13th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, Tools and Theory for Embedded Systems, LCTES '12, pp.51-60, 2012. ,
DOI : 10.1145/2248418.2248426
Certification de SCADE V3, 2000. ,
Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques, 2008 Formal Methods in Computer-Aided Design, pp.1-15, 2008. ,
DOI : 10.1109/FMCAD.2008.ECP.19
Synchronous Programming of Reactive Systems, 1993. ,
Simulation and verification of aysnchronous systems by means of a synchronous model, Proceedings of the 6th International Conference on Application of Concurrency to System Design, pp.3-14, 2006. ,
The synchronous data flow programming language LUSTRE, Proceedings of the IEEE, vol.79, issue.9, pp.1305-1320, 1991. ,
DOI : 10.1109/5.97300
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.5059
Generating efficient code from data-flow programs, Proceedings of the 3rd International Symposium on Programming Language Implementation and Logic Programming (PLILP'91), pp.207-218, 1991. ,
DOI : 10.1007/3-540-54444-5_100
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.6974
Programming and verifying real-time systems by means of the synchronous data-flow language LUSTRE, IEEE Transactions on Software Engineering, vol.18, issue.9, pp.785-793, 1992. ,
DOI : 10.1109/32.159839
An executable temporal logic to express safety properties and its connection with the language Lustre, Proceedings of the 6th International Symposium on Lucid and Intensional Programming (ISLIP'93), 1993. ,
Lustre, Lecture Notes in Computer Science, vol.891, issue.6, pp.101-112, 1995. ,
DOI : 10.1007/3-540-58867-1_50
BI as an assertion language for mutable data structures, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.14-26, 2001. ,
DOI : 10.1145/1988042.1988050
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.4925
Certifying an automated code generator using formal tools: Preliminary experiments in the GeneAuto project, Proceedings of the 4th European Congress on Embedded Real-Time Software Société des Ingénieurs de l'Automobile. [35] E. Jahier, P. Raymond, and N. Halbwachs. The Lustre V6 Reference Manual. Verimag, 2008. ,
Validating LR(1) Parsers, 21st European Symposium on Programming held as part of European Joint Conferences on Theory and Practice of Software, pp.397-416, 2012. ,
DOI : 10.1007/978-3-642-28869-2_20
URL : https://hal.archives-ouvertes.fr/hal-01077321
The semantics of a simple language for parallel programming, Proceedings of the International Federation for Information Processing (IFIP) Congress 1974, pp.471-475, 1974. ,
PKind: A parallel k-induction based model checker, Proceedings of the 10th International Workshop on 2011, number 72 in Electronic Proceedings in Theoretical Computer Science, pp.55-62, 2011. ,
DOI : 10.4204/EPTCS.72.6
URL : http://arxiv.org/abs/1111.0372
Mechanised Separation Algebra, Proceedings of the 3rd International Conference on Interactive Theorem Proving, pp.332-337, 2012. ,
DOI : 10.1007/978-3-642-32347-8_22
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.400.9382
Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009. ,
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861
Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations, Journal of Automated Reasoning, vol.17, issue.5???6, pp.1-31, 2008. ,
DOI : 10.1007/s10817-008-9099-0
URL : https://hal.archives-ouvertes.fr/inria-00289542
The OCaml system: Documentation and user's manual. Inria, 4.03 edition, 2016. ,
Modular code generation from synchronous block diagrams: Modularity vs. code size, Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles Of Programming Languages, pp.78-89, 2009. ,
DOI : 10.1145/1594834.1480893
Compiling Argos into Boolean equations, Proceedings of the 4th International Symposium on Formal Techniques for Real-Time and Fault-Tolerance (FTRTFT '96), pp.72-89, 1996. ,
DOI : 10.1007/3-540-61648-9_35
Mode-Automata: a new domain-specific construct for the development of safe critical systems, Science of Computer Programming, vol.46, issue.3, pp.219-254, 2003. ,
DOI : 10.1016/S0167-6423(02)00093-X
Translation validation for synchronous data-flow specification in the SIGNAL compiler, Proceedings of the 35th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, pp.66-80, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01087801
Modular translation validation of a full-sized synchronous compiler using off-the-shelf verification tools, Proceedings of the 18th International Workshop on Software and Compilers for Embedded Systems, SCOPES '15, pp.109-112, 2015. ,
DOI : 10.1145/2764967.2775291
URL : https://hal.archives-ouvertes.fr/hal-01148919
Certified Development Tools Implementation in Objective Caml, Proceedings of the 10th International Symposium on Practical Aspects of Declarative Languages number 4902 in Lecture Notes in Computer Science, pp.2-17, 2008. ,
DOI : 10.1007/978-3-540-77442-6_2
URL : https://hal.archives-ouvertes.fr/hal-00319700
A constructive denotational semantics for Kahn networks in Coq, From Semantics to Computer Science: Essays in Honour of Gilles Kahn, pp.383-413, 2009. ,
DOI : 10.1017/CBO9780511770524.018
URL : https://hal.archives-ouvertes.fr/inria-00431806
Translation validation for synchronous languages, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, pp.235-246, 1998. ,
DOI : 10.1007/BFb0055057
Lucid Synchrone, version 3. Tutorial and reference manual, 2006. ,
Modular static scheduling of synchronous data-flow networks: An efficient symbolic representation, Proceedings of the 9th ACM International Conference on Embedded Software, pp.215-224, 2009. ,
Compilation efficace d'un langage déclaratif synchrone: le générateur de code Lustre-V3, 1991. ,
The Lustre V4 distribution. http://wwwverimag .imag.fr/The-Lustre-Toolbox.html, 1992. ,
Recognizing regular expressions by means of dataflow networks, Proceedings of the 23rd International Colloquium on Automata, Languages and Programming, number 1099 in Lecture Notes in Computer Science, pp.336-347, 1996. ,
DOI : 10.1007/3-540-61440-0_140
URL : https://hal.archives-ouvertes.fr/hal-00384443
Separation logic: a logic for shared mutable data structures, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp.55-74, 2002. ,
DOI : 10.1109/LICS.2002.1029817
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.5322
Translation Validation: From Simulink to C, Proceedings of the 21st International Conference on Computer Aided Verification Proceedings of the 4th ACM International Conference on Embedded Software, pp.696-701, 2004. ,
DOI : 10.1007/978-3-642-02658-4_57
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.172.9992
Embedding imperative synchronous languages in interactive theorem provers, Proceedings Second International Conference on Application of Concurrency to System Design, pp.143-154, 2001. ,
DOI : 10.1109/CSD.2001.981772
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.559.7027
LUCID, the dataflow programming language, 1985. ,