Zobrazeno 1 - 10
of 10
pro vyhledávání: '"Florian Faissole"'
Autor:
Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, Hiroaki Inoue
Publikováno v:
International Journal on Software Tools for Technology Transfer
International Journal on Software Tools for Technology Transfer, 2022, 24 (6), pp.977-997. ⟨10.1007/s10009-022-00680-0⟩
International Journal on Software Tools for Technology Transfer, 2022, 24 (6), pp.977-997. ⟨10.1007/s10009-022-00680-0⟩
International audience; Programmable Logic Controllers are industrial digital computers used as automation controllers in manufacturing processes. The Ladder language is a programming language used to develop software for such controllers. In this wo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7e33021b1b500f86b72d06a08ea446a3
https://inria.hal.science/hal-03737869/document
https://inria.hal.science/hal-03737869/document
Publikováno v:
Journal of Automated Reasoning
Journal of Automated Reasoning, 2022, 66, pp.175-213. ⟨10.1007/s10817-021-09612-0⟩
Journal of Automated Reasoning, Springer Verlag, In press, ⟨10.1007/s10817-021-09612-0⟩
Journal of Automated Reasoning, 2022, 66, pp.175-213. ⟨10.1007/s10817-021-09612-0⟩
Journal of Automated Reasoning, Springer Verlag, In press, ⟨10.1007/s10817-021-09612-0⟩
Integration, just as much as differentiation, is a fundamental calculus tool that is widely used in many scientific domains. Formalizing the mathematical concept of integration and the associated results in a formal proof assistant helps in providing
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7e54d99a7408ac53b21d014b24149571
https://inria.hal.science/hal-03471095/file/article.pdf
https://inria.hal.science/hal-03471095/file/article.pdf
Autor:
Claude Marché, Denis Cousineau, David Mentré, Hiroaki Inoue, Cláudio Belo Lourenço, Florian Faissole
Publikováno v:
FMICS 2021-Formal Methods for Industrial Critical Systems
FMICS 2021-Formal Methods for Industrial Critical Systems, Aug 2021, Paris, France. ⟨10.1007/978-3-030-85248-1_2⟩
Formal Methods for Industrial Critical Systems ISBN: 9783030852474
FMICS
FMICS 2021-Formal Methods for Industrial Critical Systems, Aug 2021, Paris, France. ⟨10.1007/978-3-030-85248-1_2⟩
Formal Methods for Industrial Critical Systems ISBN: 9783030852474
FMICS
International audience; Programmable Logic Controllers (PLCs) are industrial digital computers used as automation controllers in manufacturing processes. The Ladder language is a programming language used to develop PLC software. Our aim is to prove
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::072e97f0f42eeea56dc5be6b3610ca34
https://inria.hal.science/hal-03281580
https://inria.hal.science/hal-03281580
Publikováno v:
FCCM
High-level synthesis (HLS) tools such as VivadoHLS interpret C/C++ code supplemented by proprietary optimization directives called pragmas. In order to perform loop pipelining, HLS compilers have to deal with non-trivial loop-carried data dependencie
Publikováno v:
IEEE Transactions on Computers
IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, In press, ⟨10.1109/TC.2019.2917902⟩
IEEE Transactions on Computers, 2019, ⟨10.1109/TC.2019.2917902⟩
IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, In press, ⟨10.1109/TC.2019.2917902⟩
IEEE Transactions on Computers, 2019, ⟨10.1109/TC.2019.2917902⟩
International audience; Numerical integration schemes are mandatory to understand complex behaviors of dynamical systems described by ordinary differential equations. Implementation of these numerical methods involve floating-point computations and p
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::24d1662f1175c6ce458e594640facc8c
https://hal.archives-ouvertes.fr/hal-01883843v3/document
https://hal.archives-ouvertes.fr/hal-01883843v3/document
Publikováno v:
25th IEEE Symposium on Computer Arithmetic
25th IEEE Symposium on Computer Arithmetic, Jun 2018, Amherst, MA, United States
ARITH
25th IEEE Symposium on Computer Arithmetic, Jun 2018, Amherst, MA, United States
ARITH
International audience; Some modern processors include decimal floating-point units, with a conforming implementation of the IEEE-754 2008 standard. Unfortunately, many algorithms from the computer arithmetic literature are not correct anymore when c
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4b31b2dbbc0263040dd934a66f3cc087
https://hal.inria.fr/hal-01772272
https://hal.inria.fr/hal-01772272
Autor:
Florian Faissole, Bas Spitters
Publikováno v:
JFLA 2018-Journées Francophones des Langages Applicatifs
JFLA 2018-Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France
Aarhus University
Faissole, F & Spitters, B 2018, Preuves constructives de programmes probabilistes . i Journées Francophones des Langages Applicatifs . Journées Francophones des Langages Applicatifs (JFLA), nr. 2018, Journées Francophones des Langages Applicatifs, Banyuls-sur-Mer, Frankrig, 24/01/2018 .
JFLA 2018-Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France
Aarhus University
Faissole, F & Spitters, B 2018, Preuves constructives de programmes probabilistes . i Journées Francophones des Langages Applicatifs . Journées Francophones des Langages Applicatifs (JFLA), nr. 2018, Journées Francophones des Langages Applicatifs, Banyuls-sur-Mer, Frankrig, 24/01/2018 .
National audience
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::33bc00e6a9cdb419d1db8eafcce14ba1
https://hal.inria.fr/hal-01654459
https://hal.inria.fr/hal-01654459
Autor:
Florian Faissole, Bas Spitters
Publikováno v:
Faissole, F & Spitters, B 2018, ' Un cadre pour la preuve de programmes probabilistes ', Paper fremlagt ved Vingt-neuviemes Journees Francophones des Langages Applicatifs, JFLA 2018-29th French-Speaking Conference on Applicative Languages, JFLA 2018, Banyuls-sur-Mer, Frankrig, 24/01/2018-27/01/2018 s. 137-150 .
Aarhus University
Aarhus University
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::0fc465f95c61f4415e1ce8892f91199b
https://pure.au.dk/portal/da/publications/un-cadre-pour-la-preuve-de-programmes-probabilistes(ae2e2ada-9376-4f0b-ac53-bd17a069e48d).html
https://pure.au.dk/portal/da/publications/un-cadre-pour-la-preuve-de-programmes-probabilistes(ae2e2ada-9376-4f0b-ac53-bd17a069e48d).html
Autor:
Florian Faissole
Publikováno v:
SYNASC 2017-19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
SYNASC 2017-19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2017, Timișoara, Romania. pp.1-7
SYNASC
SYNASC 2017-19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2017, Timișoara, Romania. pp.1-7
SYNASC
International audience; This article presents a Coq formalization of finite dimensional subspaces of Hilbert spaces: we prove that such subspaces are closed submodules. This result is one of the basic blocks to prove the correctness of the finite ele
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::cb14563286e0391fd7f6c8c70b9f68a3
https://hal.inria.fr/hal-01630411/file/synasc_hal.pdf
https://hal.inria.fr/hal-01630411/file/synasc_hal.pdf
Publikováno v:
6th ACM SIGPLAN Conference on Certified Programs and Proofs
6th ACM SIGPLAN Conference on Certified Programs and Proofs, Jan 2017, Paris, France. ⟨10.1145/3018610.3018625⟩
CPP
6th ACM SIGPLAN Conference on Certified Programs and Proofs, Jan 2017, Paris, France. ⟨10.1145/3018610.3018625⟩
CPP
International audience; The Finite Element Method is a widely-used method to solve numerical problems coming for instance from physics or biology. To obtain the highest confidence on the correction of numerical simulation programs implementing the Fi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0ec64beda8a953c5bb5838dc0d1410a2
https://inria.hal.science/hal-01391578
https://inria.hal.science/hal-01391578