Formal Models in Industry Standard Tools: an Argos Block within Simulink. - Timothy Bourke; Arcot Sowmya (Int. J. Softw. Eng. Knowl. Eng., 2005)

A timing model for synchronous language implementations in simulink. - Timothy Bourke; Arcot Sowmya (EMSOFT, 2006)

Automatically transforming and relating Uppaal models of embedded systems. - Timothy Bourke; Arcot Sowmya (EMSOFT, 2008)

Modelling and programming embedded controllers with timed automata and synchronous languages. - Timothy Bourke (2009)

New Results on Timed Specifications. - Timothy Bourke; Alexandre David; Kim G. Larsen; Axel Legay; Didier Lime; Ulrik Nyman; Andrzej Wasowski (WADT, 2010)

A hybrid synchronous language with hierarchical automata: static typing and translation to synchronous code. - Albert Benveniste; Timothy Bourke; Benoît Caillaud; Marc Pouzet (EMSOFT, 2011)

Divide and recycle: types and compilation for a hybrid synchronous language. - Albert Benveniste; Timothy Bourke; Benoît Caillaud; Marc Pouzet (LCTES, 2011)

Challenges and Experiences in Managing Large-Scale Proofs. - Timothy Bourke; Matthias Daum 001; Gerwin Klein; Rafal Kolanski (AISC/MKM/Calculemus, 2012)

Non-standard semantics of hybrid systems modelers. - Albert Benveniste; Timothy Bourke; Benoît Caillaud; Marc Pouzet (J. Comput. Syst. Sci., 2012)

Zélus: a synchronous language with ODEs. - Timothy Bourke; Marc Pouzet (HSCC, 2013)

seL4: From General Purpose to a Proof of Information Flow Enforcement. - Toby C. Murray; Daniel Matichuk; Matthew Brassil; Peter Gammie; Timothy Bourke; Sean Seefried; Corey Lewis; Xin Gao; Gerwin Klein (IEEE Symposium on Security and Privacy, 2013)

Analyzing an embedded sensor with timed automata in uppaal. - Timothy Bourke; Arcot Sowmya (ACM Trans. Embed. Comput. Syst., 2013)

A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol. - Timothy Bourke; Rob J. van Glabbeek; Peter Höfner (ATVA, 2014)

A type-based analysis of causality loops in hybrid systems modelers. - Albert Benveniste; Timothy Bourke; Benoît Caillaud; Bruno Pagano; Marc Pouzet (HSCC, 2014)

Showing Invariance Compositionally for a Process Algebra for Network Protocols. - Timothy Bourke; Rob J. van Glabbeek; Peter Höfner (ITP, 2014)

Mechanization of the Algebra for Wireless Networks (AWN). - Timothy Bourke (Arch. Formal Proofs, 2014)

Loop freedom of the (untimed) AODV routing protocol. - Timothy Bourke; Peter Höfner (Arch. Formal Proofs, 2014)

A Synchronous-Based Code Generator for Explicit Hybrid Systems Languages. - Timothy Bourke; Jean-Louis Colaço; Bruno Pagano; Cédric Pasteur; Marc Pouzet (CC, 2015)

Soundness of the quasi-synchronous abstraction. - Guillaume Baudart; Timothy Bourke; Marc Pouzet (FMCAD, 2016)

Sundials/ML: Connecting OCaml to the Sundials Numeric Solvers. - Timothy Bourke; Jun Inoue 001; Marc Pouzet (ML/OCAML, 2016)

Mechanizing a Process Algebra for Network Protocols. - Timothy Bourke; Rob J. van Glabbeek; Peter Höfner (J. Autom. Reason., 2016)

Loosely Time-Triggered Architectures: Improvements and Comparisons. - Guillaume Baudart; Albert Benveniste; Timothy Bourke (ACM Trans. Embed. Comput. Syst., 2016)

Symbolic simulation of dataflow synchronous programs with timers. - Guillaume Baudart; Timothy Bourke; Marc Pouzet (FDL, 2017)

Real-time ticks for synchronous programming. - Reinhard von Hanxleden; Timothy Bourke; Alain Girault (FDL, 2017)

A formally verified compiler for Lustre. - Timothy Bourke; Lélio Brun; Pierre-Évariste Dagand; Xavier Leroy; Marc Pouzet; Lionel Rieg (PLDI, 2017)

A Synchronous Look at the Simulink Standard Library. - Timothy Bourke; Francois Carcenac; Jean-Louis Colaço; Bruno Pagano; Cédric Pasteur; Marc Pouzet (ACM Trans. Embed. Comput. Syst., 2017)

Towards a verified Lustre compiler with modular reset. - Timothy Bourke; Lélio Brun; Marc Pouzet (SCOPES, 2018)

Building a Hybrid Systems Modeler on Synchronous Languages Principles. - Albert Benveniste; Timothy Bourke; Benoît Caillaud; Jean-Louis Colaço; Cédric Pasteur; Marc Pouzet (Proc. IEEE, 2018)

Mechanized semantics and verified compilation for a dataflow synchronous language with reset. - Timothy Bourke; Lélio Brun; Marc Pouzet (Proc. ACM Program. Lang., 2020)

Specification and end-to-end proof of a reactive language and its compiler (invited talk). - Timothy Bourke (REBLS@SPLASH, 2021)

Verified Lustre Normalization with Node Subsampling. - Timothy Bourke; Paul Jeanmaire; Basile Pesin; Marc Pouzet (ACM Trans. Embed. Comput. Syst., 2021)

Scheduling and Compiling Rate-Synchronous Programs with End-To-End Latency Constraints. - Timothy Bourke; Vincent Bregeon; Marc Pouzet (ECRTS, 2023)

Verified Compilation of Synchronous Dataflow with State Machines. - Timothy Bourke; Basile Pesin; Marc Pouzet (ACM Trans. Embed. Comput. Syst., 2023)

Lustre, Fast First, and Fresh. - Timothy Bourke; Marc Pouzet (IEEE Embed. Syst. Lett., 2025)