Jean-Pierre Talpin, INRIA

I am a senior INRIA researcher in Rennes, Brittany. Past twenty-two years serving as INRIA project-team leader since the early 2000s, on synchronous programming (project-team ESPRESSO) and real-time architecture and scheduling analysis (project-team TEA), my scientific interest now focus on exciting theoretical challenges on the semantics, analysis and verification of programs and cyber-physical systems, concurrency theory and process algebras, dependent-types theory and mechanized proofs of programs.
My most recent and all collaborative works comprise the mechanized formalization of an extension of the Unified Theory of Programming (UTP) to model Hybrid Communicating Sequential Processes (HCSP), the end-to-end verified programming of a virtual machine and JIT compiler for Berkeley Packet Filters (BPF), the definition of a hybrid π-calculus (HpC) and its dependently-typed session calculus (type system), and a mechanically verified theory of contracts.

Publications

"Modeling and Analysis of Cyber-Physical Systems in the Hybrid π-Calculus Using Extended Sequence Diagrams". Xiong Xu, Jixiang Miao, Shuling Wang, Jean-Pierre Talpin. International Conference on Formal Engineering Methods, 2025.
"A calculus of hybrid and mobile processes". Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Hao Wu, Bohua Zhan, Xinxin Liu, Naijun Zhan. Proceedings of the ACM on Programming Languages' issue on Object-Oriented Programming, Systems, Languages and Applications (SPLASH/OOPSLA), 2025. A complete version with proofs, case studies and link to artifacts is available on Arxiv (January 2025).

"End-to-end mechanized proof of a JIT-accelerated eBPF virtual machine for IoT". Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin. International Conference on Computer-Aided Verification, 2024.
"Theories of contracts and their applications". Jean-Pierre Talpin. 6th. Spring School on Engineering Trustworthy Software, 2024.

"Real-time fixed-priority scheduling synthesis using affine dataflow graphs: from theory to practice". Alexandre Honorat, Hai Nam Tran, Thierry Gautier, Loïc Besnard, Shuvra S. Bhattachaya, Jean-Pierre Talpin. ACM Transactions on Embedded Computing Systems, 2023. Artifact available on Gitlab, ADFG.
"Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof Simplification". Shenghao Yuan, Benjamin Lion, Frédéric Besson, Jean-Pierre Talpin. Symposium on Dependable Software Engineering: Theories, Tools and Applications, 2023.
"The polychronous model and Kahn process networks". Thierry Gautier, Paul Le Guernic, Loic Besnard, Jean-Pierre Talpin. Science of Computer Programming, 2023.
"Semantics Foundation for Cyber-Physical Systems Using Higher-Order UTP". Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Bohua Zhan, Naijun Zhan. ACM Transaction on Software Engineering and Methodology, 2023.

"Femto-Containers Runtime: Ultra-Lightweight Virtualization andf Fault Isolation For Small Software Functions on Low-Power IoT Microcontrollers". Koen Zandberg, Emmanuel Baccelli, Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin. 23rd ACM/IFIP International Middleware Conference. Usenix, 2022. Artifact available on Github, Femto-Containers.
"A denotational semantics of Simulink with higher-order UTP". Xiong Xu, Bohua Zhan, Shuling Wang, Jean-Pierre Talpin, Naijun Zhan. Journal of Logical and Algebraic Methods in Programming, 2022.
"End-to-end Mechanized Proof of an eBPF Virtual Machine for Micro-controllers". Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg, Emmanuel Baccelli. International Conference on Computer-Aided Verification, 2022. Artifact available on Gitlab, CertFC.

"Unified Graphical Co-modeling, Analysis and Verification of Cyber-Physical Systems by Combining AADL and Simulink/Stateflow". Xiong Xu, Shuling Wang, Bohua Zhan, Xiangyu Jin, Jean-Pierre Talpin, Naijun Zhan. Theoretical Computer Science, 2021.
"Verified Functional Programming of an Abstract Interpreter". Lucas Franceschino, David Pichardie, Jean-Pierre Talpin. Static Analysis Symposium. ACM, 2021. With artifact "AbIntFStar" on Gitlab.
"Verified Functional Programming of an IoT operating system’s bootloader". Shenghao Yuan, Jean-Pierre Talpin. International Conference on Formal Methods and Models for System Design. ACM, 2021.
"A Mechanically Verified Theory of Contracts". Stéphane Kastenbaum, Benoît Boyer, Jean-Pierre Talpin. International Colloquium on Theoretical Aspects of Computing. Springer, 2021. Artifact available on Gitlab, Differential contracts.

"Formal Simulation and Verification of Solidity contracts in Event-B". Jian Zhu, Kai Hu, Mamoun Filali, Jean-Paul Bodeveix, Jean-Pierre Talpin and Haitao Cao. Conference on Computers, Software and Applications. IEEE, 2021.
"A Framework for Periodic Scheduling Synthesis of Synchronous Data-Flow Graphs". Hai Nam Tran, Alexandre Honorat, Shuvra S. Bhattacharyya, Jean-Pierre Talpin, Thierry Gautier, and Loïc Besnard. International Conference on embedded computer Systems: Architectures, Modeling and Simulation. Springer, 2021.
"Verification of Concurrent Code from Synchronous Specifications". Kai Hu, Teng Zhang, Yi Ding, Jian Zhu, Jean-Pierre Talpin. Science of Computer Programming. Elsevier, 2021.

"Efficient Contention-Aware Scheduling of Synchronous Data Flow Graphs on Shared Multi-bank Memory". Hai Nam Tran, Alexandre Honorat, Jean-Pierre Talpin, Thierry Gautier and Loic Besnard. 24th International Conference on Engineering of Complex Computer Systems (ICECCS'19). IEEE, 2019.
"Parallel Composition and Modular Verification of Computer-Controlled Systems in Differential Dynamic Logic". Simon Lunel, Stefan Mitsch, Benoit Boyer, and Jean-Pierre Talpin. 23rd International Symposium on Formal Methods (FM'19). Springer, 2019.
"Unified Graphical Co-Modelling of Cyber-Physical Systems using AADL and Simulink/Stateflow". Haolan Zhan, Qianqian Lin, Shulin Wang, Jean-Pierre Talpin, Xiong Xu, and Naijun Zhan. 7th International Symposium on Unifying Theories of Programming (UTP'19). Springer, 2019.
"Towards verified programming of embedded devices". J.-P. Talpin, J.-J. Marty, S. Narayan, D. Stefan, R. Gupta. Invited Speaker at the 23rd Design, Automation and Test in Europe (DATE'19). IEEE, 2019.

"Formal Modeling and Verification of Blockchain Systems". Z. Duan, H. Mao, Z. Chen, X. Bai, K. Hu, J.-P. Talpin. 10th International Conference on Computer Modeling and Simulation. ACM, 2018.
"Polychronous automata and their use for formal validation of AADL models". T. Gautier, C; Guy, A. Honorat, P. Le Guernic, J.-P. Talpin, L. Besnard. Frontiers of Computer Science. Springer, 2018.
"Toward efficient many-core scheduling of partial expansion graphs". H. N. Tran, S. S. Bhattacharyya, J.-P. Talpin, T. Gautier. 21st International Workshop on Software and Compilers for Embedded Systems (SCOPES'18). ACM, 2018.
"Refinement types for system design". J.-P. Talpin. Keynote at the 21st Forum on Specification and Design Languages (FDL'18). IEEE, 2018.

"Compositional methods for CPS design". J.-P. Talpin. Keynote at the Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA'17). Springer, 2017.
"ADFG: a scheduling synthesis tool for dataflow graphs in real-time system". A. Honorat, H. N. Tran, L. Besnard, T. Gautier, J.-P. Talpin, A. Bouakaz. International Conference on Real-Time Networks and Systems (RNTS'17). ACM, 2017.
"Compositional proofs in dynamic differential logic". S. Lunel, B. Boyer, J.-P. Talpin. International Conference on Applications of Concurrency to System Design (ACSD'17). Springer, 2017.
"An Abstraction Technique For Parameterized Model Checking of Leader Election Protocols: Application to FTSP". O. Sankur, J.-P. Talpin. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17). Springer, 2017.
"Formal Semantics of Behavior Specifications in the Architecture Analysis and Design Language Standard". L. Besnard, T. Gautier, P. Le Guernic, C. Guy, J.-P. Talpin, B. R. Larson, E. Borde. Chapter in Cyber-Physical System Design from an Architecture Analysis Viewpoint, Communications of the NII Shonan Meetings. Springer, 2017.
"Parallel Code Generation from Synchronous Specifications". K. Hu, T. Zhang, L.-H. Shang, Z.-B. Yang, J.-P. Talpin. Journal of Software. ISCAS, 2017.

"Bottom-up approach for integrating models for software components using contracts". P. Joshi, H. Yu, S. K. Shukla, J.-P. Talpin. Patent US9477446B1. US Patents Office, 2016.
"Timing-oriented and architecture-centric system design using contracts". H. Yu, S. K. Shukla, J.-P. Talpin. Patent US9459840B1. US Patents Office, 2016.
"Formal Semantics of Behavior Speciﬁcations in the Architecture Analysis and Design Language Standard (extended abstract)". L. Besnard, T. Gautier, P. Le Guernic, C. Guy, J.-P. Talpin, B. R. Larson, E. Borde. High-Level Design, Verification and Test (HLDVT'16). IEEE, 2016.
"Integration of polychrony in the QGen model compiler". C. Junke, T. Gautier, J.-P. Talpin, L. Besnard. European Congress on Embeddd Real-Rime Software and Systems (ERTS'16), 2016.

"Polychronous automata". T. Gautier, P. Le Guernic, J.-P. Talpin, L. Besnard. Theoretical Aspects of Software Engineering (TASE'15), Awarded best paper. IEEE, 2015.
"Modular translation validation of a full-sized synchronous compiler using off-the-shelf verification tools (abstract)". V. C. Ngo, J.-P. Talpin, T. Gautier, L. Besnard, P. Le Guernic. International Workshop on Software and Compilers for Embedded Systems (SCOPES'15), invited presentation. ACM, 2015.
"Translation Validation for Synchronous Data-flow Specification in the SIGNAL Compiler". V. C. Ngo, J.-P. Talpin, T. Gautier. International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE'15). IFIP, 2015.
"Model-Based Integration for Automotive Control Software". H. Yu, P. Joshi, J.-P. Talpin, S. Shukla, S. Shiraishi. Digital Automation Conference (DAC'15), Automotive Special Session. ACM, 2015.
"Translation validation for clock transformations in a synchronous compiler". V. C. Ngo, J.-P. Talpin, T. Gautier. International Conference on Fundamental Approaches to Software Engineering (ETAPS/FASE'15). Springer, 2015.
"Mapping Functional Behavior onto Architectural Model in a Model Driven Embedded System Design". P. Joshi, S. K. Shukla, J.-P. Talpin, H. Yu. Symposium On Applied Computing (SAC'15). ACM, 2015.
"Towards refinement types for time-dependent data-flow networks". J.-P. Talpin, P. Jouvelot, S. K. Shukla. 13th ACM-IEEE International Conference on Formal Methods and Models for System Design. ACM, 2015.

"Earliest-Deadline First Scheduling of Multiple Independent Dataflow". A. Bouakaz, T. Gautier, J.-P. Talpin. IEEE International Workshop on Signal Processing Systems (SIPS'14). IEEE, 2014.
"Towards an architecture-centric approach dedicated to model-based virtual integration for embedded software systems (position paper)". H. Yu, J.-P. Talpin, S. Shukla, P. Joshi, S. Shiraishi. Workshop on Architecture Centric Virtual Integration (ACVI'14), 2014.
"A constraint-solving approach to Faust program type checking". I. Frotier de la Messelière, P. Jouvelot, and J.-P. Talpin. Constraint Programming meets Verification (CP/CAV'14), 2014.
"Efficient deadlock detection for polychronous data-flow specifications". C. Ngo, J.-P. Talpin, T. Gautier. Electronic System Level Synthesis Conference (ESLSYN'14). IEEE, 2014.
"Logically timed specifications in the AADL : a synchronous model of computation and communication (recommendations to the SAE committee on AADL)". L. Besnard, E. Borde, P. Dissaux, T. Gautier, P. Le Guernic, J.-P. Talpin. INRIA Technical Report n.446, 2014.
"Timed behavioural modelling and affine scheduling of embedded software architectures in the AADL using Polychrony". L. Besnard, A. Bouakaz, T. Gautier, P. Le Guernic, Y. Ma, J.-P. Talpin, H. Yu. In Science of Computer Programming (SCP). Elsevier, 2014.
"From AADL to timed abstract state machine: a certified model transformation". Z. Yang, K. Hu, D. Ma, J.-P. Bodeveix, L. Pi, J.-P. Talpin. In Journal of System and Software (JSS). Elsevier, 2014.
"Constructive Polychronous Systems". J.-P. Talpin, J. Brandt, M. Gemünde, K. Schneider, and S. Shukla. In Science of Computer Programming (SCP). Elsevier, 2014.

"Polychronous modeling, analysis, verification and simulation for timed software architectures". H. Yu, Y. Ma, T. Gautier, L. Besnard, P. Le Guernic, J.-P. Talpin. In Journal of Systems Architecture (JSA). Elsevier, 2013.
"Formal verification of synchronous data-flow program transformations toward certified compilation". V.-C. Ngo, J.-P. Talpin, Gautier, P. Le Guernic, L. Besnard. In Frontiers of Computer Systems (FCS). Special issue on synchronous programming. Springer, 2013.
"Exploring software architectures with Polychrony and Syndex". H. Yu, Y. Ma, T. Gautier, L. Besnard, J.-P. Talpin, P. Le Guernic, Y. Sorel (FCS). In Frontiers of Computer Systems. Special issue on synchronous programming. Springer, 2013.
"Design of Safety-Critical Java Level 1 Applications Using Affine Abstract Clocks". A. Bouakaz and J.-P. Talpin. International Workshop on Software and Compilers for Embedded Systems (M-SCOPES'13). ACM, June 2013.
"Buffer minimization in earliest-deadline first scheduling of dataflow graphs". A. Bouakaz and J.-P. Talpin. Conference on Languages, Compilers and Tools for Embedded Systems (LCTES'13). ACM, June 2013.
"Toward polychronous analysis and validation for timed software architectures in AADL". Y. Ma, H. Yu, T. Gautier, L. Besnard, P. Le Guernic, J.-P. Talpin and Maurice Heitz.Design Analysis and Test in Europe (DATE'13). IEEE, April 2013.

"Embedding polychrony into synchrony". J. Brandt, M. Gemünde, K. Schneider, S. Shukla, and J.-P. Talpin. In Transactions on Software Engineering (TSE). IEEE, 2012.
"Representation of synchronous, asynchronous, and polychronous components by clocked guarded Actions". J. Brandt, M. Gemünde, K. Schneider, S. Shukla, and J.-P. Talpin. In Design Automation for Embedded Systems (DAES), Special Issue on Languages, Models and Model Based Design for Embedded Systems. Springer, 2012.
"Constructive polychronous systems". J.-P. Talpin, J. Brandt, M. Gemünde, K. Schneider, and S. Shukla. Logical Foundations in Computer Science (LFCS'12). Springer, December 2012.
"Affine data-flow graphs for the synthesis of hard real-time applications". A. Bouakaz, J.-P. Talpin, and J. Vitek. Application of Concurrency to System Design (ACSD'12). IEEE Press, June 2012.
"Formal verification on compiler transformations on polychronous equations". V. C. Ngo, J.-P. Talpin, T. Gautier, P. Le Guernic, and L. Besnard. International Congerence on Integrated Formal Methods (IFM'11). Springer, June 2012.

"From concurrent multi-clock programs to deterministic asynchronous implementations". Potop-Butucaru D., Sorel, Y., de Simone, R., Talpin, J.-P. In Fundamenta Informaticae (FI). IOS Press, 2011.
"Integrating system descriptions by clocked guarded actions". J. Brandt, M. Gemünde, K. Schneider, S. Shukla, and J.-P. Talpin. Forum on Design Languages (FDL'11). IEEE, September 2011.
"System synthesis from AADL using Polychrony". Y. Ma, H. Yu, T. Gautier, J.-P. Talpin, L. Besnard and P. Le Guernic. Electronic System Level Synthesis Conference (ESLSYN'11). IEEE, June 2011.
"From concurrent multi-clock programs to concurrent multi-threaded implementations". V. Papailiopoulou, D. Potop-Butucaru, Y. Sorel, R. de Simone, L. Besnard and J.-P. Talpin. Electronic System Level Synthesis Conference (ESLSYN'11). IEEE, June 2011.
"Polychronous controller synthesis from MARTE's CCSL constraints". Yu, H., Talpin, J.-P., Besnard, L., Gautier, T., Marchand, H., Le Guernic, P. ACM-IEEE Conference on Methods and Models for Codesign (MEMOCODE'11). IEEE, July 2011.
"Two formal semantics for a subset of the AADL". Yang, Z., Hu, K., Bodeveix, J.-P., Pi, L., Ma, D., Talpin, J.-P. UML&AADL workshop at the IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'11) . IEEE, 2011.
"System-level co-simulation of integrated avionics using polychrony". Yu, H., Ma, Y., Glouche, Y., Talpin, J.-P., Besnard, L., Gautier, T., Le Guernic, P., Toom, A., and Laurent, O. ACM Symposium on Applied Computing (SAC'11). ACM, 2011.

"Compositional design of isochronous systems". Talpin, J.-P., Ouy, J., Gautier,T., Besnard, L., Le Guernic, P. In Science of Computer Programming (SCP), Special Issue on APGES. Elsevier, 2011.
"Synoptic : a domain-specific modeling language for space on-board application software". Cortier, A., Besnard, L., Bodeveix, J.-P., Buisson, J., Dagnat, F., Filali, M., Garcia, G., Ouy, J., Pantel, M., Rugina, A., Strecker, M., Talpin, J.-P. . Chapter in Synthesis of embedded software. Springer, 2010.
"Compilation of polychronous data flow equations". Besnard, L., Gautier, T., Le Guernic, P., Talpin, J.-P. Chapter in Synthesis of embedded software. Springer, 2010.
"A module language for typing Signal programs by contracts". Glouche, Y., Gautier, T. Le Guernic, P., Talpin, J.-P. Chapter in Synthesis of embedded software. Springer, 2010.
"Interpretation of the AADL Behavior Annex into a Synchronous Formalism Using SSA". Ma, Y., Talpin, J.-P, Gautier, T. International Conference on Computer and Information Technology (ICCIT'10). IEEE Press, 2010.
"A synchronous approach to threaded program verification". Johnson, K., Besnard, L., Gautier, T., Talpin, J.-P. Automated Verification of Critical Systems (AVOCS'10). EASST, 2010.
"A higher-order extension for imperative synchronous languages". Vecchie, E., Talpin, J.-P, Boisgérault, S. Software and Compilers for Embedded Systems (SCOPES'10). ACM Press, 2010.
"Synoptic: a domain-specific modeling language for onboard real-time software design". A . Cortier, J.P. Bodeveix, M. Filali, G. Garcia, E. Morand , M. Pantel, A. Rugina, M. Strecker, J.P. Talpin. Embedde Real-Time Software and Systems, Neptune Workshop (NEPTUNE'10). Génie Logiciel , 2010.
"Modular interpretation of heterogeneous modeling diagrams into synchronous equations using static single assignment". Talpin, J.-P, Ouy, J., Gautier, T., Besnard, L., Cortier, A. Application of Concurrency to System Design (ACSD'10). IEEE Press, 2010.
"Polychronous analysis of timing constraints in UML MARTE". Yue, H., Talpin, J.-P.,Besnard, L., Gautier, T., Mallet, F., André, C., de Simone, R. International Workshop on Model-Based Engineering for Real-Time Embedded Systems Design (MOBE-RTES'10). IEEE Press, 2010.

"The synchronous hypothesis and polychronous languages". Potop-Butucaru D., De Simone, R., Talpin, J.-P. Chapter in Networked Embedded Systems. CRC Press, 2009.
"Programming models for multi-core embedded systems". Jose, B., Xue, B., Shukla, S., Talpin, J.-P. Chapter in Multi-core Embedded Systems. Taylor and Francis, 2009.
"Clock-driven distributed real-time implementation of endochronous synchronous programs". Potop-Butucaru D., De Simone, R., Sorel, Y., Talpin, J.-P.Embedded Software Conference (EMSOFT'09). ACM Press, 2009.
"Automatic translation of C/C++ parallel code into synchronous formalism using an SSA intermediate form". Besnard, L., Gautier, T, Moy, M., Talpin, J.-P., Johnson, K., Maraninchi, F. Automated Verification of Cirtical Systems (AVOCS'09). EASST, 2009.
"Synoptic: a domain-specific modeling language for embedded flight-software". A. Cortier, L. Besnard, J.-P. Bodeveix, J. Buisson, F. Dagnat, M. Filali, G. Garcia, T. Gautier, J. Ouy, M. Pantel, A. Rugina, M. Strecker, J.-P. Talpin. FM'09 Workshop on Formal Methods for Aerospace (FMA'09). Elsevier, 2009.
"A boolean algebra of contracts for assume-guarantee reasoning". Glouche, Y., Le Guernic, P., Talpin, J.-P., Gautier, T. Formal Aspects of Component Software (FACS'09). Elsevier, 2009.
"A module language for typing by contracts". Glouche, Y., Talpin, J.-P., Le Guernic, P., Gautier, T. NASA Formal Methods Symposium (NFM'09). Springer, 2009.
"From concurrent multiclock programs to deterministic asynchronous implementations". Potop-Butucaru D., De Simone, R., Sorel, Y., Talpin, J.-P. Application of Concurrency to System Design (ACSD'09). IEEE Press, 2009.
"Distributed simulation of AADL specifications in a polychronous model of computation". Ma, Y., Talpin, J.-P.,Shukla, S., Gautier, T. International Conference on Embedded Software and Systems (ICESS'09). IEEE Press, 2009.
"Separate compilation and execution of imperative synchronous modules". Vecchie, E., Talpin, J.-P., Schneider, K. Design Analysis and Test in Europe (DATE'09). IEEE, April 2009.

"A metamodel for the design of polychronous systems". Brunette, C., Talpin, J.-P., Gamatié, A., Gautier, T. Journal of Logic and Algebraic Programming (JLAP), Special Issue on Applying Concurrency Research to Industry. Elsevier, 2008.
"On the automatic inference of synchronization logic for multi-threaded software synthesis from polychronous specifications". Jose, B., Shukla, S., Patel, H., Talpin, J.-P. ACM-IEEE Conference on Methods and Models for Codesign (MEMOCODE'08). IEEE, June 2008.
"Virtual prototyping AADL architectures in a polychronous model of computation". Ma, Y., Talpin, J.-P.,Gautier, T. ACM-IEEE Conference on Methods and Models for Codesign (MEMOCODE'08). IEEE, June 2008.
"Analysis of periodic clock relations in polychronous systems". Talpin, J.-P., Métivier, H., Gautier, T., Le Guernic, P. IFIP Working Conference on Distributed and Parallel Embedded Systems (DIPES'08). Springer, September 2008.
"Compositional design of isochronous systems". Talpin, J.-P., Ouy, J., Besnard, L., Le Guernic, P. Design Analysis and Test in Europe (DATE'08). IEEE Press, March 2008.
"Generating multi-threaded code from polychronous specifications". Jose, B., Patel, H., Shukla, S., Talpin, J.-P. Synchronous Languages, Applications, and Programming (SLAP'08). Elsevier, March 2008.

"On the polychronous approach to embedded software design". Shukla, S. K., Suhaib, S. M., Mathaikutty, D. A., Talpin, J.-P. Next generation design and verification methodologies for distributed embedded systems (GM R&D WORKSHOP'07). Springer Verlag, 2007.
"Separate compilation of polychronous specifications". Ouy, J., Talpin, J.-P., Besnard, L., Le Guernic, P. Formal Methods for Globally Asynchronous Locally Synchronous Design (FMGALS'07). Electronic Notes in Theoretical Computer Science, Elsevier, 2007.

"Polychronous design of embedded real-time systems"Gamatié, A., Gautier, T., Le Guernic, P., Talpin, J.-P. ACM Transactions on Software Engineering and Methodology (TOSEM). ACM Press, 2006.
"An algebraic theory for behavioral modeling and protocol synthesis in system design". Talpin, J.-P, Le Guernic, P. In Formal Methods in System Design (FMSD), Special Issue on formal methods for GALS design. Springer Verlag, 2006.
"Polychronous mode automata". Talpin, J.-P., Brunette, C.,Gautier, T., Gamatié, A. Embedded Software Conference (EMSOFT'06). ACM Press, 2006.
"Polychronous methodology for system design, a true concurrency approach". S. Suhaib, D. Mathaikutty, S. Shukla, J.-P. Talpin. High-level design, validation and test workshop (HLDVT'06). IEEE Press, November 2006.
"A modeling paradigm for integrated modular avionics design". Brunette, C., Delamare, R., Gamatié, A., Gautier, T., Talpin, J.-P. Software Engineering and Advanced Application (SEAA'06). IEEE Press, 2006.
"The Topcased project - a toolkit in open-source for critical application and system development". Vernadat, F., Percebois, C., Farail, P., Vingerhoeds, R., Rossignol, A., Talpin, J.-P., Chemouil,D. International Space System Engineering Conference - Data Systems in Aerospace (DASIA'06). Eurospace, May 2006.
"Modeling multi-clocked data-flow programs using the Generic Modeling Environment". Brunette, C., Talpin, J.-P., Besnard, L., Gauthier, T. Synchronous Languages, Applications, and Programming (SLAP'06). Elsevier, March 2006.
"Automated translation of C/C++ programs into a synchronous formalism". Kalla, H.,Talpin, J.-P., Berner, D., Besnard, L. International Conference on the Engineering of Computer Based Systems (ECBS'06). IEEE, March 2006.
"A verification approach for GALS integration of synchronous components". F. Doucet, M. Menarini, I.H. Krueger, R. Gupta, and J.- P. Talpin. Electronic Notes in Theoretical Computer Science (ENTCS), v. 146(2). Elsevier, 2006.

"Compositional behavioral modeling of embedded systems and conformance checking". Talpin, J.-P, Le Guernic, P., Shukla, S., Gupta, R. In International Journal on Parallel Processing (IJPP), special issue on testing of embedded systems. Springer, 2005.
"The synchronous hypothesis and synchronous languages". Potop-Butucaru D., De Simone, R., Talpin, J.-P. Chapter in Embedded Systems Handbook. CRC Press, 2005.
"Automated clock inference for stream function-based system level specifications". Talpin, J.-P., Shukla, S.High-level design, validation and test workshop (HLDVT'05). IEEE Press, November 2005.
"From multi-clocked synchronous specifications to latency-insensitive systems". Talpin, J.-P., Potop-Butucaru, D., Ouy, J., Caillaud, B. Embedded Software Conference (EMSOFT'05). ACM Press, September 2005.
"SystemCXML: an open-source extensible SystemC front-end using XML". Berner, D., Patel, H., Mathaikutty, D., Shukla, S., Talpin, J.-P. Forum on Specification and Design Languages (FDL'05). ECSI, September 2005.
"A verification approach for GALS integration of synchronous components". Doucet, F., Menarini, M., Krueger, I.,Talpin, J.-P., Gupta, R. International Workshop on Formal Methods for Globally Asynchronous locally Synchronous Design (FMGALS'05). Electronic Notes in Computer Science. Elsevier, June 2005.
"A functional programming framework for latency insensitive protocol validation"Suhaib, S.,Mathaikutty, D., Shukla, S., Berner, D.,Talpin, J.-P. International Workshop on Formal Methods for Globally Asynchronous locally Synchronous Design (FMGALS'05). Electronic Notes in Computer Science. Elsevier, June 2005.

"Behavioral type inference for compositional system design". Talpin, J.-P., Berner, D., Shukla, S., Le Guernic, P., Gamatié, A., Gupta, R. Chapter in Formal Methods and Models for System Design. Kluwer Academic Publishers, 2004.
"Algebraic theory for behavioral type inference". Talpin, J.-P., Le Guernic. Chapter in Formal Methods and Models for System Design. Kluwer Academic Publishers, 2004.
"Capturing formal specifications into abstract models". Berner, D., Suhaib, S., Shukla, S., Talpin, J.-P. Chapter in Formal Methods and Models for System Design. Kluwer Academic Publishers, 2004.
"Formal refinement checking in a system-level design methodology". Talpin, J.-P., Le Guernic, P., Shukla, S. K., Gupta, R., Doucet, F. Fundamenta Informaticae (FI), Special Issue on Applications of Concurrency to System Design. IOS Press, 2004.
"Encapsulation and behavioural inheritance in a synchronous model of computation for embedded system services adaptation". Kerboeuf, M., Talpin, J.-P. Journal of Logics and Algebraic Programming (JLAP), special issue on process algebra and system architectures. Elsevier, 2004.
"Modular design through component abstraction". Berner, D., Talpin, J.-P., Le Guernic, P., Shukla, S. K. International conference on compilers, architectures and synthesis for embedded systems (CASES'04). ACM Press, September 2004.
"A behavioral type inference system for compositional system-on-chip design". Talpin, J.-P., Berner, D., Shukla, S. K., Gamatié, A., Le Guernic, P., Gupta, R. Application of Concurrency to System Design (ACSD'04). IEEE Press, June 2004.
"Modeling and validation of asynchronous systems in synchronous frameworks". Mousavi, M., R., Le Guernic, P., Talpin, J.-P., Shukla, S., Basten, T. Design Analysis and Test Europe (DATE'04). IEEE Press, March 2004. Available as INRIA Research Report 4935.

"Méthodes formelles pour la modélisation et l'analyse de systèmes". Talpin, J.-P. Thèse d'Habilitation à Diriger les Recherches (HDR). Université de Rennes, November 2003.
"Polychrony for system design". Le Guernic, P., Talpin, J.-P., Le Lann, J.-C. Journal for Circuits, Systems and Computers (JCSC). Special Issue on Application Specific Hardware Design. World Scientific, August 2003.
"Formal proof of a polychronous protocol for loosely time-triggered architectures". Kerboeuf, M., Nowak, D., Talpin, J.-P. International conference on formal engineering methods (ICFEM'03). Lectures Notes in Computer Science. Springer Verlag, November 2003.
"Hard real-time implementation of embedded systems in JAVA". Talpin, J.-P., Gamatié, A., Berner, D., Le Dez, B., Le Guernic, P. International Workshop on Scientific Engineering of Distributed JAVA Applications (FIDJI'2003). Lectures Notes in Computer Science. Springer Verlag, November 2003.
"Polychrony for formal refinement-checking in a system-level design methodology". Talpin, J.-P., Le Guernic, P., Shukla, S. K., Gupta, R., Doucet, F. Application of Concurrency to System Design (ACSD'03). IEEE Press, June 2003.
"A polychronous model for high-level component-based system design". Talpin, J.-P., Le Guernic, P., Shukla, S. K., Gupta, R., Doucet, F. Design Analysis and Test Europe (DATE'03). IEEE Press, March 2003.

"A protocol for loosely time-triggered architectures". Benveniste, A., Caspi, P., Le Guernic, P., Marchand, H., Talpin, J.-P., Tripakis, S. Embedded Software Conference (EMSOFT'02). Lectures Notes in Computer Science. Springer Verlag, October 2002.
"Model checking robustness to desynchronization". Talpin, J.-P. Distributed and parallel embedded systems, IFIP World Computer Congress (DIPES'2002). Kluwer Academic Publishers, August 2002.

"Specification and verification of a steam-boiler with Signal-Coq". Kerboeuf, M., Nowak, D., Talpin, J.-P. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'00). Springer Verlag, October 2000.
"A new methodology for real-time distributed systems". Wang, Y., Talpin, J.-P., Benveniste, A., Le Guernic, P. IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS'00). Kluwer Academic Publishers, September 2000.
"A semantics of UML state-machines using synchronous pre-order transition systems". Wang, Y., Talpin, J.-P., Benveniste, A., Le Guernic, P. In International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC'00). IEEE Press, March 2000.

"Timed polyhedra analysis for synchronous languages". Besson, F., Jensen, T., Talpin, J.-P. Static Analysis Symposium (SAS'99). Springer Verlag, September 1999.
"Synchronous structures". Nowak, D., Talpin, J.-P., Le Guernic, P. International Conference on Concurrency Theory (CONCUR'99). Springer Verlag, August 1999.

"A synchronous semantics of higher-order processes for modeling reconfigurable reactive systems". Talpin, J.-P., Nowak, D. International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'98). Springer Verlag, December 1998.
"Co-inductive axiomatization of a synchronous language". Nowak, D., Beauvais, J.-R., Talpin, J.-P. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'98). Springer Verlag, October 1998.
"BDL, a language of distributed reactive objects". Talpin, J.-P., Benveniste, A., Caillaud, B., Jard, C., Bouziane, Z., Canon, H. International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC'98). IEEE Press, April 1998.

"Region-based memory management". Tofte, M., Talpin, J.-P. Information and Computation (I&C), Vol. 132, pages 109-176. Academic Press, 1997.
"An ML-like module system for the synchronous language SIGNAL". Nowak, D., Talpin, J.-P., Gautier, T., Le Guernic, P. European Conference on Parallel Processing (EUROPAR'97). Springer Verlag, August 1997.
"Reactive types". Talpin, J.-P. International Joint Conference on the Theory and Practice of Software Development (TAPSOFT'97). Springer Verlag, April 1997.

"Benchmarking implementations of functional languages with Pseudoknot, a float-intensive benchmark". Hartel, P., & al. Journal of Functional Programming, Vol. 6. Cambridge University Press, 1996.

"The type and effect discipline". Talpin, J.-P., Jouvelot, P. Information and Computation (I&C), vol. 111, pages 245-296. Academic Press, 1994.
"Implementation of the typed lambda calculus using a stack of regions". Tofte, M., Talpin, J.-P. Symposium on Principles of Programming Languages (POPL'94). ACM Press, January 1994. Received the 2004 ACM SIGPLAN Award for the most influential POPL paper.

"Aspects théoriques et pratiques de l'inférence de types et d'effets". Talpin, J.-P. Thèse de Doctorat en Informatique de l'Université Paris VI. Ecole des Mines de Paris, May 1993.
"Compiling FX on the CM-2". Talpin, J.-P., Jouvelot, P. Workshop on Semantics Analysis (WSA'93). Springer Verlag, September 1993.

"The type and effect discipline". Talpin, J.-P., Jouvelot, P. Conference on Logic in Computer Science (LICS'92). IEEE Press, June 1992. Received the 2012 ACM-IEEE LICS Test-of-Time Award.
"Polymorphic type, region and effect inference". Talpin, J.-P., Jouvelot, P. Journal of Functional Programming (JFP), Vol. Cambridge University Press, 1992.

Books

TECS

"Formal methods and models for system design". Gupta, R., Le Guernic, P., Shukla, S., Talpin, J.-P., Editors. ISBN 978-1-4020-8051-7, Springer, 2004.

"Synthesis of embedded systems". Shukla, S., Talpin, J.-P., Editors. ISBN 978-1-4419-6399-4, Springer, 2010.

"Cyber-Physical System Design from an Architecture Analysis Viewpoint". S. Nakajima, Talpin, J.-P., M. Toyoshima, H. Yu, Editors. Communications of the NII Shonan Meetings, Springer, 2017.

Conferences

Rajesh Gupta, UCSD, and Sandeep Shukla, IIT Kanpur, and I co-founded the ACM-IEEE Conference Series on Methods and Models for System Design, MEMOCODE. I co-chaired MEMOCODE in 200-04, 2013-14, 2016-17. I participated to the program committee of the following conferences.

International Conference on Formal Engineering Methods (ICFEM), 2025
Symposium on Dependable Software Engineering (SETTA), 2022 (Cochair), 2023
Conference on Embedded Computer Systems: Architectures, Modeling and Simulation (SAMOS), 2020-23
ACM Symposium on Applied Computing (SAC), Embedded Systems Track (EMBS), 2006-20
ACM conference on languages, compilers and tools for embedded systems (LCTES), 2014-20
International Workshop on Software and Compilers for Embedded Systems (SCOPES), 2014-20
Application of Concurrency to System Design (ACSD), 2007-12, 2017
ACM/IEEE Conference on Formal Methods and Models for System Design (MEMOCODE), 2003 to 2016, 2024-25
International Symposium on Theoretical Aspects of Software Engineering (TASE), 2015-16
International Conference on Formal Aspects of Component Software (FACS), 2015
ACM Embedded Systems Conference (EMSOFT), 2008, 2013-14
International Conference on Language and Automata Theory and Applications (LATA), 2014
IEEE International Symposium on Industrial Embedded Systems (SIES), 2005-12
European Symposium on Programming (ESOP), 2009
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), 2008
IEEE International Conference on Embedded Software and Systems (ICESS), 2005, 2015
IEEE Design, Automation and Test in Europe (DATE), 2003-05

Collaborative projects

Natural Science Foundation of China, International Collaborative Project Design and Validation of Hybrid and Mobile Systems (2026-30)
Chinese Academy of Science, International Fellowship (PIFI) Validation Methods for Safety-Critical Systems (2024-26)
MSCA Post-Doctoral Grant Cert-T with Benjamin Lion (2024-26)

INRIA project-team TEA (2013-23, team leader)
INRIA Challenge Future-proof IoT with Shenghao Yuan (2019-23)
INRIA associate team Convex with ISCAS (2018-22)
Mitsubishi Electric R&D doctoral grant with Stéphane Kastenbaum (2019-22)
Doctoral grant co-funded by MSR-Inria and ERC Vesta with Lucas Franceschino (2018-21)
Inria - Mitsubishi Electric R&D Europe collaboration framework program (2018)
INRIA associate team Composite with UC San Diego (2017-19)
Mitsubishi Electric R&D doctoral grant with Simon Lunel (2015-18)
ASTRI consulting grant (2016-17)
ANR project FEEVER (2013-17)
USAF OSR grant FA8655-13-1-3049 (2013-16) with VTRL
Toyota ITC grant (2014-16)
FUI project CORAIL (2012-15)
FUI project P (2011-14)
INRIA project-team ESPRESSO (2002-13, team leader)
ANR project Verisync with Van Chan Ngo (2010-2013)
INRIA associate project POLYCORE with VTRL (2011-13)
ITEA2 project OPEES (2010-12, work-package leader)
Artemisia project CESAR (2009-11)
ANR project SPACIFY (2007-10)
ANR project FotoVP (2008-10)
DGE project TOPCASED (2005-10)
EADS Foundation grant (2006-09)
Networks of excellence Artist, Artist 2, Artist Design (2000-09)
NSF-INRIA project BALBOA with UCSD (2002-09)
ANR project OPENEMBEDD (2006-08, coordinator)

Short bio

I have a Master Degree in Theoretical Computer Science from University Paris VI. I did my PhD Thesis at Ecole des Mines de Paris under the advisory of Pierre Jouvelot. I worked three years as Research Associate at the European Computer-Industry Research Centre in Munich. I joined INRIA in 1995, in the EPART project-team of Paul Le Guernic. I lead INRIA project-team ESPRESSO from 2000 to 2012 and project-team TEA until 2023.
I am deeply honored to be recipient of both the ACM SIGPLAN Award for the most influential POPL paper, with Mads Tofte, 2004, and of the ACM-IEEE LICS "Test of Time" Award, with my Ph.D. advisor Pierre Jouvelot, 2012.

Jean-Pierre Talpin