ClawZ: Cost-Effective Formal Verification for Control Systems, 7th Int. Conf. on Formal Methods and Software Engineering (ICFEM 2005) (LNCS), vol.3785, pp.465-479, 2005. ,
Symbolic Analysis for Improving Simulation Coverage of Simulink/Stateflow Models, Proc. 8th ACM Int. Conf. on Embedded Software, pp.89-98, 2008. ,
ClawZ: control laws in Z, 2nd Int. Conf. on Formal Methods and Software Engineering, pp.169-176, 2000. ,
Compilation certifiée de SCADE/LUSTRE, Ph.D. Dissertation. Univ. Paris Sud, vol.11, 2013. ,
A Formalization and Proof of a Modular Lustre Code Generator, 2014. ,
Real Time Programming: Special Purpose or General Purpose Languages, Proc. 11th Int. Federation for Information Processing, pp.11-17, 1989. ,
URL : https://hal.archives-ouvertes.fr/inria-00075494
Preemption in Concurrent Systems, Foundations of Software Technology and Theoretical Computer Science (LNCS), vol.761, pp.72-93, 1993. ,
, The Esterel v5 Language Primer (5.91 ed.). Ecole des Mines and INRIA, 2000.
The Constructive Semantics of Pure Esterel (draft version 3 ed.), 2002. ,
Clock-directed modular code generation for synchronous data-flow languages, Proc. 9th ACM SIGPLAN Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES 2008), pp.121-130, 2008. ,
Mechanized Semantics for the Clight Subset of the C Language, J. Automated Reasoning, vol.43, pp.263-288, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00352524
An operational semantics for Simulink's simulation engine, Proc. 13th ACM SIGPLAN Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES 2012, pp.129-138, 2012. ,
A Formally Verified Compiler for Lustre, Proc. 2017 ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01512286
, , pp.586-601
Towards a verified Lustre compiler with modular reset, Proc. 21st Int. Workshop on Software and Compilers for Embedded Systems (SCOPES'18), pp.14-17, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01817949
Arguments cadencés dans un compilateur Lustre vérifié, 30 ièmes Journées Francophones des Langages Applicatifs, pp.109-124, 2019. ,
Clocks in dataflow languages, Theoretical Computer Science, vol.94, issue.1, pp.125-140, 1992. ,
Towards recursive block diagrams, Annual Review in Automatic Programming, vol.18, pp.90015-90024, 1994. ,
LUSTRE: A declarative language for programming synchronous systems, Proc. 14th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp.178-188, 1987. ,
A Co-iterative Characterization of Synchronous Stream Functions, 1997. ,
URL : https://hal.archives-ouvertes.fr/hal-01622305
A Co-iterative Characterization of Synchronous Stream Functions, First Workshop on Coalgebraic Methods in Computer Science (CMCS'98) (ENTCS), vol.11, pp.50-57, 1998. ,
URL : https://hal.archives-ouvertes.fr/hal-01622305
From control law diagrams to Ada via Circus, Formal Aspects of Computing, vol.23, pp.465-512, 2011. ,
Abstract Simulation: A Static Analysis of Simulink Models, Proc. Int. Conf. on Embedded Software and Systems, pp.83-92, 2009. ,
URL : https://hal.archives-ouvertes.fr/hal-00332447
A formal framework for modeling and validating Simulink diagrams, Formal Aspects of Computing, vol.21, pp.451-483, 2009. ,
MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems, Provably Correct Systems (NASA Monographs in Systems and Software Engineering, pp.39-58, 2017. ,
Programming Parallelism with Futures in Lustre, Proc. 12th ACM Int. Conf. on Embedded Software (EMSOFT 2012, pp.197-206, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00786682
A Conservative Extension of Synchronous Data-flow with State Machines, Proc. 5th ACM Int. Conf. on Embedded Software (EMSOFT 2005), pp.173-182, 2005. ,
Scade 6: A Formal Language for Embedded Critical Software Development, Proc. 11th Int. Symp. Theoretical Aspects of Software Engineering, pp.4-15, 2017. ,
Clocks as First Class Abstract Types, Proc. 3rd Int. Conf. on Embedded Software (EMSOFT 2003) (LNCS), vol.2855, pp.134-155, 2003. ,
Type-based initialization analysis of a synchronous dataflow language, Int. J. Software Tools for Technology Transfer, vol.6, pp.245-255, 2004. ,
, The Coq proof assistant reference manual, 2019.
A modular memory optimization for synchronous data-flow languages: application to arrays in a Lustre compiler, Proc. 13th ACM SIGPLAN Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES 2012, pp.51-60, 2012. ,
A Denotational Semantics for Stateflow, Proc. 5th ACM Int. Conf. on Embedded Software (EMSOFT 2005), pp.164-172, 2005. ,
Modular Resetting of Synchronous Data-Flow Programs, Proc. 2nd ACM SIGPLAN Int. Conf. on Principles and Practice of Declarative Programming, pp.289-300, 2000. ,
URL : https://hal.archives-ouvertes.fr/hal-01573195
An Operational Semantics for Stateflow, Proc. 7th Int. Conf. on Fundamental Approaches to Software Engineering (FASE'04), vol.2984, pp.229-243, 2004. ,
Statecharts: A Visual Formalism for Complex Systems, Science of Computer Programming, vol.8, issue.3, pp.90035-90044, 1987. ,
, The STATEMATE Semantics of Statecharts. ACM Trans. Software Engineering and Methodology (TOSEM), vol.5, pp.293-333, 1996.
The Lustre V6 Reference Manual, 2019. ,
Validating LR(1) parsers, 21st European Symposium on Programming (ESOP 2012), held as part of European Joint Conferences on Theory and Practice of Software (ETAPS 2012) (LNCS), Helmut Seidl, vol.7211, pp.397-416, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-01077321
The Semantics of a Simple Language for Parallel Programming, Proc. Int. Federation for Information Processing, pp.471-475, 1974. ,
CakeML: A Verified Implementation of ML, Proc. 41st ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp.179-191, 2014. ,
Formal verification of a realistic compiler, Comms. ACM, vol.52, pp.107-115, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00415861
Compiling Argos into Boolean equations, Proc. 4th Int. Symp. Formal Techniques for Real-Time and Fault-Tolerance (FTRTFT '96) (LNCS), vol.1135, pp.72-89, 1996. ,
Argos: an automaton-based synchronous language, Computer Languages, vol.27, pp.61-92, 2001. ,
URL : https://hal.archives-ouvertes.fr/hal-00273055
Mode-Automata: a new Domain-Specific Construct for the Development of Safe Critical Systems, Proc. 35th IFIP WG 6.1 Int. Conf. on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2015) (LNCS), vol.46, pp.66-80, 2003. ,
URL : https://hal.archives-ouvertes.fr/hal-01876521
A constructive denotational semantics for Kahn networks in Coq, From Semantics to Computer Science: Essays in Honour of Gilles Kahn, pp.383-413, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00431806
, Haskell 98 Language and Libraries: The Revised Report, CUP, 2003.
Compiling Esterel, 2007. ,
Lucid Synchrone, v. 3. Tutorial and reference manual, 2006. ,
Translation Validation: From Simulink to C, Proc. 21st Int. Conf. on Computer Aided Verification (CAV 2009) (LNCS), vol.5643, pp.696-701, 2009. ,
A Formally Verified Sequentializer for Lustre-Like Concurrent Synchronous Data-Flow Programs, Proc. 39th Int. Conf. on Software Engineering Companion (ICSE-C'17), pp.109-111, 2017. ,
A formally verified transformation to unify multiple nested clocks for a Lustre-like language, Science China Information Sciences, vol.62, issue.1, p.12801, 2019. ,
A New Verified Compiler Backend for CakeML, Proc. 21st ACM SIGPLAN Int. Conf. on Functional Programming, pp.60-73, 2016. ,
Translating Discrete-Time Simulink to Lustre, ACM Trans. Embedded Computing Systems, vol.4, pp.779-818, 2005. ,
Semantic Translation of Simulink Diagrams to Input/Output Extended Finite Automata, Discrete Event Dynamic Systems, vol.22, pp.223-247, 2012. ,
Formal Verification of Simulink/Stateflow Diagrams, Proc. 13th Int. Symp. Automated Technology for Verification and Analysis (ATVA 2015) (LNCS), Bernd Finkbeiner, vol.9364, pp.464-481, 2015. ,
Verifying Simulink Diagrams via a Hybrid Hoare Logic Prover, Proc. 13th ACM Int. Conf. on Embedded Software (EMSOFT 2013, vol.9, pp.1-9, 2013. ,