Publications

2023

Journal articles

titre

Real-Time Fixed Priority Scheduling Synthesis using Affine DataFlow Graphs: from Theory to Practice

auteur

Alexandre Honorat, Hai Nam Tran, Thierry Gautier, Loïc Besnard, Shuvra S. Bhattacharyya, Jean-Pierre Talpin

article

ACM Transactions on Embedded Computing Systems (TECS), 2023, pp.1-30. ⟨10.1145/3615586⟩

Accès au texte intégral et bibtex

titre

The Polychronous Model of Computation and Kahn Process Networks

auteur

Thierry Gautier, Paul Le Guernic, Loïc Besnard, Jean-Pierre Talpin

article

Science of Computer Programming, 2023, pp.1-49. ⟨10.1016/j.scico.2023.102958⟩

Accès au texte intégral et bibtex

titre

A denotational semantics of Simulink with higher-order UTP

auteur

Xiong Xu, Bohua Zhan, Shuling Wang, Jean-Pierre Talpin, Naijun Zhan

article

Journal of Logical and Algebraic Methods in Programming, 2023, 130, pp.100809. ⟨10.1016/j.jlamp.2022.100809⟩

Accès au texte intégral et bibtex

Conference papers

titre

Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof Simplification

auteur

Shenghao Yuan, Benjamin Lion, Frédéric Besson, Jean-Pierre Talpin

article

SETTA 2023 – 9th International Symposium Dependable Software Engineering. Theories, Tools, and Applications, Nov 2023, Nanjing (Chine), China. pp.385-401, ⟨10.1007/978-981-99-8664-4_22⟩

Accès au texte intégral et bibtex

Theses

titre

Verified programming and secure integration of operating system libraries in Coq

auteur

Shenghao Yuan

article

Systems and Control [cs.SY]. Université de Rennes, 2023. English. ⟨NNT : 2023URENS060⟩

Accès au texte intégral et bibtex

2022

Journal articles

titre

Semantics Foundation for Cyber-Physical Systems Using Higher-Order UTP

auteur

Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Bohua Zhan, Naijun Zhan

article

ACM Transactions on Software Engineering and Methodology, 2022, pp.1-47. ⟨10.1145/3517192⟩

Accès au texte intégral et bibtex

titre

Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow

auteur

Xiong Xu, Shuling Wang, Bohua Zhan, Xiangyu Jin, Jean-Pierre Talpin, Naijun Zhan

article

Theoretical Computer Science, 2022, 903, pp.1-25. ⟨10.1016/j.tcs.2021.11.008⟩

Accès au bibtex

Conference papers

titre

Femto-Containers: Lightweight Virtualization and Fault Isolation For Small Software Functions on Low-Power IoT Microcontrollers

auteur

Koen Zandberg, Emmanuel Baccelli, Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin

article

Middleware 2022 – 23rd ACM/IFIP International Conference Middleware, Nov 2022, Quebec, Canada. pp.1-12, ⟨10.1145/3528535.3565242⟩

Accès au texte intégral et bibtex

titre

End-to-end Mechanized Proof of an eBPF Virtual Machine for Micro-controllers

auteur

Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg, Emmanuel Baccelli

article

CAV 2022 – 34th International Conference on Computer Aided Verification, Aug 2022, Haifa, Israel. pp.1-23

Accès au texte intégral et bibtex

2021

Journal articles

titre

Verification of concurrent code from synchronous specifications

auteur

Kai Hu, Teng Zhang, Yi Ding, Jian Zhu, Jean-Pierre Talpin

article

Science of Computer Programming, 2021, 206, pp.1-19. ⟨10.1016/j.scico.2021.102625⟩

Accès au bibtex

Conference papers

titre

Verified functional programming of an IoT operating system’s bootloader

auteur

Shenghao Yuan, Jean-Pierre Talpin

article

MEMOCODE 2021 – 19th ACM-IEEE International Conference on Formal Methods and Models for System Design, Nov 2021, Beijing, China. pp.1-16

Accès au texte intégral et bibtex

titre

Verified Functional Programming of an Abstract Interpreter

auteur

Lucas Franceschino, Jean-Pierre Talpin, David Pichardie

article

SAS 2021 – 28th Static Analysis Symposium, Oct 2021, Chicago, United States. pp.1-20

Accès au texte intégral et bibtex

titre

A Mechanically Verified Theory of Contracts

auteur

Stéphane Kastenbaum, Benoît Boyer, Jean-Pierre Talpin

article

ICTAC 2021 – 18th International Colloquium on Theoretical Aspects of Computing, Sep 2021, Nur-Sultan, Kazakhstan. pp.134-151, ⟨10.1007/978-3-030-85315-0_9⟩

Accès au texte intégral et bibtex

titre

A Framework for Fixed Priority Periodic Scheduling Synthesis from Synchronous Data-flow Graphs

auteur

Hai Nam Tran, Alexandre Honorat, Shuvra S Bhattacharyya, Jean-Pierre Talpin, Thierry Gautier, Loïc Besnard

article

SAMOS XXI 2021 – 21st International Conference on embedded computer Systems: Architectures, MOdeling and Simulation, Jul 2021, Virtual, France. pp.1-12

Accès au texte intégral et bibtex

Theses

titre

Verified Programming at the Intersection of Dependent Types and Static Analysis

auteur

Lucas Franceschino

article

Autre [cs.OH]. École normale supérieure de Rennes, 2021. Français. ⟨NNT : 2021ENSR0030⟩

Accès au texte intégral et bibtex

2020

Journal articles

titre

TRAP: trace runtime analysis of properties

auteur

Daian Yue, Vania Joloboff, Frédéric Mallet

article

Frontiers of Computer Science, 2020, 14 (3), pp.1-15. ⟨10.1007/s11704-018-7217-7⟩

Accès au texte intégral et bibtex

Other publications

titre

SIGNAL V4 – INRIA version: Reference Manual (revised working version)

auteur

Loïc Besnard, Thierry Gautier, Paul Le Guernic

article

2020

Accès au texte intégral et bibtex

titre

LIO*: Low Level Information Flow Control in F*

auteur

Jean-Joseph Marty, Lucas Franceschino, Jean-Pierre Talpin, Niki Vazou

article

2020

Accès au texte intégral et bibtex

2019

Journal articles

titre

Polychronous automata and their use for formal validation of AADL models

auteur

Thierry Gautier, Clément Guy, Alexandre Honorat, Paul Le Guernic, Jean-Pierre Talpin, Loïc Besnard

article

Frontiers of Computer Science, 2019, 13 (4), pp.677-697. ⟨10.1007/s11704-017-6134-5⟩

Accès au texte intégral et bibtex

Conference papers

titre

Efficient Contention-Aware Scheduling of SDF Graphs on Shared Multi-bank Memory

auteur

Hai Nam Tran, Alexandre Honorat, Jean-Pierre Talpin, Thierry Gautier, Loïc Besnard

article

ICECCS 2019 – 24th International Conference on Engineering of Complex Computer Systems, Nov 2019, Hong Kong, China. pp.114-123, ⟨10.1109/ICECCS.2019.00020⟩

Accès au texte intégral et bibtex

titre

Unified Graphical Co-Modelling of Cyber-Physical Systems using AADL and Simulink/Stateflow

auteur

Haolan Zhan, Qianqian Lin, Shuling Wang, Jean-Pierre Talpin, Xiong Xu, Naijun Zhan

article

UTP 2019 – 7th International Symposium on Unifying Theories of Programming, Oct 2019, Porto, Portugal. pp.1-20, ⟨10.1007/978-3-030-31038-7_6⟩

Accès au texte intégral et bibtex

titre

Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic

auteur

Simon Lunel, Stefan Mitsch, Benoît Boyer, Jean-Pierre Talpin

article

FM 2019 – 23rd International Symposium on Formal Methods, Oct 2019, Porto, Portugal. pp.1-22

Accès au bibtex

titre

Towards verified programming of embedded devices

auteur

Jean-Pierre Talpin, Jean-Joseph Marty, Shravan Narayan, Deian Stefan, Rajesh Gupta

article

DATE 2019 – 22nd IEEE/ACM Design, Automation and Test in Europe, Mar 2019, Florence, Italy. pp.1445-1450, ⟨10.23919/DATE.2019.8715067⟩

Accès au texte intégral et bibtex

Theses

titre

Parallelism and modular proof in differential dynamic logic

auteur

Simon Lunel

article

Artificial Intelligence [cs.AI]. Université de Rennes, 2019. English. ⟨NNT : 2019REN1S005⟩

Accès au texte intégral et bibtex

2018

Journal articles

titre

Guest Editorial: Special Issue of ACM TECS on the ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2017)

auteur

Patricia Derler, Klaus Schneider, Jean-Pierre Talpin

article

ACM Transactions on Embedded Computing Systems (TECS), 2018, pp.1-2

Accès au texte intégral et bibtex

Conference papers

titre

Refinement types for system design (abstract)

auteur

Jean-Pierre Talpin

article

FDL 2018 – Forum on specification and Design Languages, Sep 2018, Munich, Germany

Accès au bibtex

titre

Toward Efficient Many-core Scheduling of Partial Expansion Graphs

auteur

Hai Nam Tran, Shuvra S Bhattacharyya, Jean-Pierre Talpin, Thierry Gautier

article

SCOPES 2018 – 21st International Workshop on Software and Compilers for Embedded Systems, May 2018, Saint Goar, Germany. pp.1-4, ⟨10.1145/3207719.3207734⟩

Accès au texte intégral et bibtex

titre

Formal Modeling and Verification of Blockchain System

auteur

Zhangbo Duan, Hongliang Mao, Zhidong Chen, Xiaomin Bai, Kai Hu, Jean-Pierre Talpin

article

the 10th International Conference, Jan 2018, Sydney, France. pp.231-235

Accès au bibtex

Lectures

titre

The Signal synchronous language: the principles beyond the language and how to exploit and extend them

auteur

Albert Benveniste, Thierry Gautier

article

École thématique. France. 2018, pp.1-68

Accès au texte intégral et bibtex

2017

Journal articles

titre

Parallel Code Generation from Synchronous Specifications

auteur

Kai Hu, Teng Zhang, Lihong Shang, Zhibing Yang, Jean-Pierre Talpin

article

Journal of Software, 2017, 28, pp.1-15. ⟨10.13328/j.cnki.jos.005056⟩

Accès au texte intégral et bibtex

Conference papers

titre

Compositional methods for CPS design (keynote abstract)

auteur

Jean-Pierre Talpin

article

3rd Symposium on Dependable Software Engineering: Theories, Tools and Applications, Oct 2017, Changsha, China

Accès au bibtex

titre

ADFG: a scheduling synthesis tool for dataflow graphs in real-time systems

auteur

Alexandre Honorat, Hai Nam Tran, Loïc Besnard, Thierry Gautier, Jean-Pierre Talpin, Adnan Bouakaz

article

International Conference on Real-Time Networks and Systems , Oct 2017, Grenoble, France. pp.1-10, ⟨10.1145/3139258.3139267⟩

Accès au texte intégral et bibtex

titre

Compositional proofs in differential dynamic logic dL

auteur

Simon Lunel, Benoît Boyer, Jean-Pierre Talpin

article

17th International Conference on Application of Concurrency to System Design, Jun 2017, Zaragoza, Spain

Accès au texte intégral et bibtex

titre

An Abstraction Technique For Parameterized Model Checking of Leader Election Protocols: Application to FTSP

auteur

Ocan Sankur, Jean-Pierre Talpin

article

23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Apr 2017, Uppsala, Sweden. pp.23-40

Accès au texte intégral et bibtex

Book sections

titre

Formal Semantics of Behavior Specifications in the Architecture Analysis and Design Language Standard

auteur

Loic Besnard, Thierry Gautier, Paul Le Guernic, Clément Guy, Jean-Pierre Talpin, Brian Larson, Etienne Borde

article

Cyber-Physical System Design from an Architecture Analysis Viewpoint, Springer, 2017, Cyber-Physical System Design from an Architecture Analysis Viewpoint, ⟨10.1007/978-981-10-4436-6_3⟩

Accès au bibtex

Books

titre

Cyber-Physical System Design from an Architecture Analysis Viewpoint

auteur

Shin Nakajima, Jean-Pierre Talpin, Masumo Toyoshima, Huafeng Yu

article

Springer, 2017, Communications of NII Shonan Meetings, 978-981-10-4435-9. ⟨10.1007/978-981-10-4436-6⟩

Accès au bibtex

2016

Journal articles

titre

Using Runtime Systems Tools to Implement Efficient Preconditioners for Heterogeneous Architectures

auteur

Adrien Roussel, Jean-Marc Gratien, Thierry Gautier

article

Oil & Gas Science and Technology – Revue d’IFP Energies nouvelles, 2016, 71 (6), pp.65:1-13. ⟨10.2516/ogst/2016020⟩

Accès au texte intégral et bibtex

Conference papers

titre

Formal semantics of behavior specifications in the architecture analysis and design language standard

auteur

Loïc Besnard, Thierry Gautier, Clément Guy, Paul Le Guernic, Jean-Pierre Talpin, Brian R Larson, Etienne Borde

article

HLDVT 2016 – 18th IEEE International High-Level Design Validation and Test Workshop, Oct 2016, Santa Cruz, United States. pp.30-39, ⟨10.1109/HLDVT.2016.7748252⟩

Accès au texte intégral et bibtex

titre

Flexible Runtime Verification Based On Logical Clock Constraints

auteur

Daian Yue, Vania Joloboff, Frédéric Mallet

article

FDL 2016 – Forum on specification & Design Languages, ECSI, Sep 2016, Bremen, Germany

Accès au texte intégral et bibtex

titre

A Sequent Calculus for a Modal Logic on Finite Data Trees

auteur

David Baelde, Simon Lunel, Sylvain Schmitz

article

CSL 2016, Sep 2016, Marseille, France. pp.1–16, ⟨10.4230/LIPIcs.CSL.2016.32⟩

Accès au texte intégral et bibtex

titre

PSCV: A Runtime Verification Tool for Probabilistic SystemC Models

auteur

Van Chan Ngo, Axel Legay, Vania Joloboff

article

CAV 2016 – 28th International Conference on Computer Aided Verification, Jul 2016, Toronto, Canada. pp.84 – 91, ⟨10.1007/978-3-319-41528-4_5⟩

Accès au texte intégral et bibtex

titre

A Stencil DSEL for Single Code Accelerated Computing with SYCL

auteur

Olivier Aumage, Denis Barthou, Alexandre Honorat

article

SYCL 2016 1st SYCL Programming Workshop during the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Mar 2016, Barcelone, Spain

Accès au texte intégral et bibtex

titre

Integration of polychrony and QGen model compiler

auteur

Christophe Junke, Thierry Gautier, Jean-Pierre Talpin, Loic Besnard

article

ERTS’16 – European Congress on Embeddd Real-Rime Software and Systems, Jan 2016, Toulouse, France

Accès au texte intégral et bibtex

Reports

titre

TRAP: A Platform For Flexible Runtime Verification of Temporal Properties

auteur

Daian Yue

article

[Research Report] RR-9006, INRIA. 2016, pp.46

Accès au texte intégral et bibtex

titre

Formal semantics of behavior specifications in the architecture analysis and design language standard

auteur

Loïc Besnard, Thierry Gautier, Paul Le Guernic, Clément Guy, Jean-Pierre Talpin, Brian Larson, Etienne Borde

article

[Research Report] RR-8950, INRIA. 2016, pp.30 – 39

Accès au texte intégral et bibtex

2015

Journal articles

titre

Fast approximately timed simulation

auteur

Vania Joloboff, Shenpeng Wang, Yangdong Deng

article

WIT Transactions on Information and Communication Technologies, 2015, WIT Transactions on Information and Communication Technologies, 978-1-78466-054-3 (68), pp.756

Accès au texte intégral et bibtex

Conference papers

titre

Towards Verified Faithful Simulation

auteur

Vania Joloboff, Jean-François Monin, Xiaomu Shi

article

Dependable Software Engineering: Theories, Tools, and Applications, Nov 2015, Nanjing, China

Accès au bibtex

titre

Towards refinement types for time-dependent data-flow networks

auteur

Jean-Pierre Talpin, Pierre Jouvelot, Sandeep Kumar Shukla

article

ACM-IEEE Conference on Methods and Models for System Design, Sep 2015, Austin, United States

Accès au bibtex

titre

Polychronous Automata

auteur

Paul Le Guernic, Thierry Gautier, Jean-Pierre Talpin, Loïc Besnard

article

TASE 2015, 9th International Symposium on Theoretical Aspects of Software Engineering, Sep 2015, Nanjing, China. pp.95-102, ⟨10.1109/TASE.2015.21⟩

Accès au texte intégral et bibtex

titre

Model-Based Integration for Automotive Control Software

auteur

Huafeng Yu, Joshi Prashi, Jean-Pierre Talpin, Sandeep Kumar Shukla, Shin’Ichi Shiraishi

article

Digital Automation Conference, ACM, Jun 2015, San Francisco, United States

Accès au bibtex

titre

Translation Validation for Synchronous Data-Flow Specification in the SIGNAL Compiler

auteur

Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier

article

35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2015, Grenoble, France. pp.66-80, ⟨10.1007/978-3-319-19195-9_5⟩

Accès au texte intégral et bibtex

titre

Modular translation validation of a full-sized synchronous compiler using off-the-shelf verification tools (abstract)

auteur

van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier, Loic Besnard, Paul Le Guernic

article

International Workshop on Software and Compilers for Embedded Systems, ACM, Jun 2015, St Goar, Germany

Accès au texte intégral et bibtex

titre

Mapping Functional Behavior onto Architectural Model in a Model Driven Embedded System Design

auteur

Joshi Prashi, Sandeep Kumar Shukla, Jean-Pierre Talpin, Huafeng Yu

article

Symposium On Applied Computing, Apr 2015, Salamanca, Spain

Accès au bibtex

titre

Translation Validation for Clock Transformations in a Synchronous Compiler

auteur

van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier, Paul Le Guernic

article

FASE – ETAPS 2015, Apr 2015, London, United Kingdom

Accès au texte intégral et bibtex

Reports

titre

Liquid Clocks – Refinement Types for Time-Dependent Stream Functions

auteur

Jean-Pierre Talpin, Pierre Jouvelot, Sandeep Kumar Shukla

article

[Research Report] RR-8747, INRIA Rennes – Bretagne Atlantique; INRIA. 2015

Accès au texte intégral et bibtex

2014

Journal articles

titre

Constructive Polychronous Systems

auteur

Jean-Pierre Talpin, Jens Brandt, Mike Gemünde, Klaus Schneider, Sandeep Shukla

article

Science of Computer Programming, 2014, Science of Computer Programming, pp.20

Accès au bibtex

titre

Timed behavioural modelling and affine scheduling of embedded software architectures in the AADL using Polychrony

auteur

Loïc Besnard, Adnan Bouakaz, Thierry Gautier, Paul Le Guernic, Yue Ma, Jean-Pierre Talpin, Huafeng Yu

article

Science of Computer Programming, 2014, Science of Computer Programming, pp.20

Accès au bibtex

titre

From AADL to timed abstract state machine: a certified model transformation

auteur

Zhibin Yang, Kai Hu, Dianfu Ma, Jean-Paul Bodeveix, Lei Pi, Jean-Pierre Talpin

article

Journal of Systems and Software, 2014, Journal of Systems and Software, pp.20

Accès au bibtex

titre

From AADL to Timed Abstract State Machines: A Verified Model Transformation

auteur

Zhibin Yang, Kai Hu, Dianfu Ma, Jean-Paul Bodeveix, Lei Pi, Jean-Pierre Talpin

article

Journal of Systems and Software, 2014, vol. 93, pp. 42-68. ⟨10.1016/j.jss.2014.02.058⟩

Accès au texte intégral et bibtex

Conference papers

titre

Earliest-Deadline First Scheduling of Multiple Independent Dataflow Graphs

auteur

Adnan Bouakaz, Thierry Gautier, Jean-Pierre Talpin

article

2014 IEEE Workshop on Signal Processing Systems (SiPS), Oct 2014, Belfast, United Kingdom

Accès au bibtex

titre

Optimized Distribution of Synchronous Programs via a Polychronous Model

auteur

Ke Sun, Loïc Besnard, Thierry Gautier

article

Formal Methods and Models for System Design (MEMOCODE’14), Oct 2014, Lausanne, Switzerland. pp.42 – 51, ⟨10.1109/MEMCOD.2014.6961842⟩

Accès au texte intégral et bibtex

titre

An abstraction-refinement framework for priority-driven scheduling of static dataflow graphs

auteur

Adnan Bouakaz, Thierry Gautier

article

International Conference on Formal Methods and Models for System Design, Oct 2014, Lausanne, Switzerland. ⟨10.1109/MEMCOD.2014.6961838⟩

Accès au bibtex

titre

Towards an architecture-centric approach dedicated to model-based virtual integration for embedded software systems

auteur

Huafeng Yu, Jean-Pierre Talpin, Sandeep Shukla, Prachi Joshi, Shin’Ichi Shiraishi

article

Workshop on Architecture Centric Virtual Integration, MODELS 2014, Sep 2014, Valencia, Spain

Accès au bibtex

titre

A constraint-solving approach to Faust program type checking

auteur

Imré Frotier de La Messelière, Pierre Jouvelot, Jean-Pierre Talpin

article

Constraint Programming meets Verification, The 20th International Conference on Principles and Practice of Constraint Programming, Sep 2014, Lyon, France

Accès au bibtex

titre

Precise deadlock detection for polychronous data-flow specifications

auteur

van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier

article

ESLsyn – DAC 2014, May 2014, San Francisco, United States. ⟨10.1109/ESLsyn.2014.6850379⟩

Accès au texte intégral et bibtex

Reports

titre

Logically timed specifications in the AADL : a synchronous model of computation and communication (recommendations to the SAE committee on AADL)

auteur

Loïc Besnard, Etienne Borde, Pierre Dissaux, Thierry Gautier, Paul Le Guernic, Jean-Pierre Talpin

article

[Technical Report] RT-0446, INRIA. 2014, pp.27

Accès au texte intégral et bibtex

Theses

titre

Formal verification of a synchronous data-flow compiler : from Signal to C

auteur

van Chan Ngô

article

Software Engineering [cs.SE]. Université de Rennes, 2014. English. ⟨NNT : 2014REN1S034⟩

Accès au texte intégral et bibtex

Preprints, Working Papers, …

titre

Translation Validation for Synchronous Data-flow Specification in the SIGNAL Compiler

auteur

van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier

article

2014

Accès au texte intégral et bibtex

2013

Conference papers

titre

Simultaneous information and power transfer in wireless cooperative networks

auteur

Zhiguo Ding, Samir M. Perlaza, Iñaki Esnaola, H. Vincent Poor

article

8th International ICST Conference on Communications and Networking in China (CHINACOM), Aug 2013, Guilin, China. ⟨10.1109/ChinaCom.2013.6694600⟩

Accès au texte intégral et bibtex

2005

Conference papers

titre

MARTE: a new OMG profile RFP for the Modeling and Analysis of Real-Time Embedded Systems

auteur

Charles André, Arnaud Cuccuru, Jean-Luc Dekeyser, Robert de Simone, Cédric Dumoulin, Julien Forget, Thierry Gautier, Sébastien Gérard, Frédéric Mallet, Ansgar Radermacher, Laurent Rioux, Thierry Saunier, Yves Sorel

article

DAC 2005 Workshop – UML for SoC Design, Jun 2005, Anaheim California, United States

Accès au bibtex