Skip to Main content Skip to Navigation


...
hal-01653283v1  Conference papers
Thibaut GirkaDavid MentréYann Régis-Gianas. Verifiable Semantic Difference Languages
International Symposium on Principles and Practice of Declarative Programming, Oct 2017, Namur, Belgium. ⟨10.1145/3131851.3131870⟩
...
hal-01419860v1  Reports
Thibaut GirkaDavid MentréYann Régis-Gianas. Oracle-based Differential Operational Semantics (long version)
[Research Report] Université Paris Diderot / Sorbonne Paris Cité. 2016
...
hal-01615140v1  Conference papers
Simon LunelBenoît BoyerJean-Pierre Talpin. Compositional proofs in differential dynamic logic dL
17th International Conference on Application of Concurrency to System Design, Jun 2017, Zaragoza, Spain
hal-02894772v1  Conference papers
Thierry JéronNicolas MarkeyDavid MentréReiya NoguchiOcan Sankur. Incremental methods for checking real-time consistency
FORMATS 2020 - 18th International Conference on Formal Modeling and Analysis of Timed Systems, Sep 2020, Vienne, Austria. pp.1-18
hal-02193642v1  Conference papers
Simon LunelStefan MitschBenoît BoyerJean-Pierre Talpin. Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic
FM 2019 - 23rd International Symposium on Formal Methods, Oct 2019, Porto, Portugal. pp.1-22
hal-02895344v1  Conference papers
Emily ClementThierry JéronNicolas MarkeyDavid Mentré. Computing maximally-permissive strategies in acyclic timed automata
FORMATS 2020 - 18th International Conference on Formal Modeling and Analysis of Timed Systems, Sep 2020, Vienna, Austria. pp.1-33
...
hal-03329311v1  Conference papers
Stéphane KastenbaumBenoît BoyerJean-Pierre Talpin. A Mechanically Verified Theory of Contracts
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⟩
...
tel-01890508v1  Theses
Thibaut Girka. Differential program semantics
Programming Languages [cs.PL]. Université Paris Diderot, 2018. English
...
hal-03281580v1  Conference papers
Cláudio LourençoDenis CousineauFlorian FaissoleClaude MarchéDavid Mentré et al.  Automated Verification of Temporal Properties of Ladder Programs
FMICS 2021 - Formal Methods for Industrial Critical Systems, Aug 2021, Paris, France. ⟨10.1007/978-3-030-85248-1_2⟩
...
hal-00741134v1  Conference papers
Erwan BousseDavid MentréBenoit CombemaleBenoit BaudryKatsuragi Takaya. Aligning SysML with the B Method to Provide V&V for Systems Engineering
Model-Driven Engineering, Verification, and Validation 2012 (MoDeVVa 2012), Sep 2012, Innsbruck, Austria
...
hal-00998092v1  Conference papers
David DelahayeCatherine DuboisClaude MarchéDavid Mentré. The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations
Abstract State Machines, Alloy, B, VDM, and Z, Jun 2014, Toulouse, France. pp.290-293
...
hal-00998094v1  Conference papers
David DelahayeClaude MarchéDavid Mentré. Le projet BWare : une plate-forme pour la vérification automatique d'obligations de preuve B
Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2014, Paris, France
...
hal-00681781v1  Conference papers
David MentréClaude MarchéJean-Christophe FilliâtreMasashi Asuka. Discharging Proof Obligations from Atelier B using Multiple Automated Provers
ABZ - 3rd International Conference on Abstract State Machines, Alloy, B and Z, Jun 2012, Pisa, Italy