Zobrazeno 1 - 10
of 40
pro vyhledávání: '"Delphine Demange"'
Publikováno v:
CPP 2023-12th ACM SIGPLAN International Conference on Certified Programs and Proofs
CPP 2023-12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2023, Boston, United States. ⟨10.1145/3573105.3575681⟩
CPP 2023-12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2023, Boston, United States. ⟨10.1145/3573105.3575681⟩
International audience
Autor:
Pierre Sesques, Lionel Karlin, Emmanuel Massy, Alizée Maarek, Guillaume Aussedat, Anne Lazareth, Camille Golfier, Fadhela Bouafia-Sauvy, Helene Lequeu, Dana Ghergus, Violaine Safar, Emmanuelle Ferrant, Emmanuel Bachy, Hervé Ghesquières, Cyrille B. Confavreux, Delphine Demangel, Emeline Perrial, Charles Dumontet
Publikováno v:
Frontiers in Oncology, Vol 14 (2024)
BackgroundIn spite of spectacular advances in the treatment of multiple myeloma, a majority of patients will die from this disease or related complications. While a great amount of focus has been dedicated to the development of novel therapies, littl
Externí odkaz:
https://doaj.org/article/4a125c6c53de4fb0b5064a8ef7afa57d
Publikováno v:
LCTES
LCTES '20: 21st ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems Proceedings
LCTES '20-21st ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems
LCTES '20-21st ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, Jun 2020, London / Virtual, United Kingdom. pp.85-96, ⟨10.1145/3372799.3394365⟩
LCTES '20: 21st ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems Proceedings
LCTES '20-21st ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems
LCTES '20-21st ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, Jun 2020, London / Virtual, United Kingdom. pp.85-96, ⟨10.1145/3372799.3394365⟩
International audience; Transiently-powered systems featuring non-volatile memory as well as external peripherals enable the development of new low-power sensor applications. However, as programmers, we are ill-equipped to reason about systems where
Autor:
Jan Vitek, Gustavo Petri, Yannick Zakowski, Delphine Demange, David Cachera, Suresh Jagannathan, David Pichardie
Publikováno v:
Journal of Automated Reasoning
Journal of Automated Reasoning, 2018, ⟨10.1007/s10817-018-9489-x⟩
Journal of Automated Reasoning, Springer Verlag, 2018, ⟨10.1007/s10817-018-9489-x⟩
Journal of Automated Reasoning, 2018, ⟨10.1007/s10817-018-9489-x⟩
Journal of Automated Reasoning, Springer Verlag, 2018, ⟨10.1007/s10817-018-9489-x⟩
International audience; Concurrent garbage collection algorithms are a challenge for program verification. In this paper, we address this problem by proposing a mechanized proof methodology based on the Rely-Guarantee proof technique. We design a com
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::385df8e2609d466368827576019acb7a
https://hal.science/hal-01897251/file/jar18.pdf
https://hal.science/hal-01897251/file/jar18.pdf
Publikováno v:
SAC 2018-The 33rd ACM/SIGAPP Symposium On Applied Computing
SAC 2018-The 33rd ACM/SIGAPP Symposium On Applied Computing, Apr 2018, Pau, France. pp.1881-1890, ⟨10.1145/3167132.3167333⟩
SAC
SAC 2018-The 33rd ACM/SIGAPP Symposium On Applied Computing, Apr 2018, Pau, France. pp.1881-1890, ⟨10.1145/3167132.3167333⟩
SAC
International audience; Compiling concurrent and managed languages involves implementing sophisticated interactions between client code and the runtime system. An emblematic runtime service, whose implementation is particularly error-prone, is concur
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2ac74991dbb04af29a214e3a1925f0e6
https://hal.archives-ouvertes.fr/hal-01653620/file/SimuLin.pdf
https://hal.archives-ouvertes.fr/hal-01653620/file/SimuLin.pdf
Publikováno v:
CC 2018-27th International Conference on Compiler Construction
CC 2018-27th International Conference on Compiler Construction, Feb 2018, Vienna, Austria. pp.163-173, ⟨10.1145/3178372.3179503⟩
CC
CC 2018-27th International Conference on Compiler Construction, Feb 2018, Vienna, Austria. pp.163-173, ⟨10.1145/3178372.3179503⟩
CC
International audience; The Sea of Nodes intermediate representation was introduced by Cliff Click in the mid 90s as an enhanced Static Single Assignment (SSA) form. It improves on the initial SSA form by relaxing the total order on instructions in b
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b6adfcafa5264c8e3cf3a2bd62496465
https://inria.hal.science/hal-01723236/document
https://inria.hal.science/hal-01723236/document
Autor:
Gustavo Petri, David Cachera, Delphine Demange, Jan Vitek, David Pichardie, Yannick Zakowski, Suresh Jagannathan
Publikováno v:
ITP 2017-8th International Conference on Interactive Theorem Proving
ITP 2017-8th International Conference on Interactive Theorem Proving, Sep 2017, Brasília, Brazil. pp.496-513, ⟨10.1007/978-3-319-66107-0_31⟩
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Interactive Theorem Proving
Interactive Theorem Proving ISBN: 9783319661063
ITP
J. Autom. Reasoning
ITP 2017-8th International Conference on Interactive Theorem Proving, Sep 2017, Brasília, Brazil. pp.496-513, ⟨10.1007/978-3-319-66107-0_31⟩
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Interactive Theorem Proving
Interactive Theorem Proving ISBN: 9783319661063
ITP
J. Autom. Reasoning
International audience; Concurrent garbage collection algorithms are an emblematic challenge in the area of concurrent program verification. In this paper, we address this problem by proposing a mechanized proof methodology based on the popular Rely-
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5548be8beb952f52abdbda285872812d
https://hal.inria.fr/hal-01613389
https://hal.inria.fr/hal-01613389
Publikováno v:
Proceedings of the 25th International Conference on Compiler Construction
25th International Conference on Compiler Construction
25th International Conference on Compiler Construction, Mar 2016, Barcelona, Spain
CC
25th International Conference on Compiler Construction
25th International Conference on Compiler Construction, Mar 2016, Barcelona, Spain
CC
International audience; Modern optimizing compilers rely on the Static Single Assignment (SSA) form to make optimizations fast and simpler to implement. From a semantic perspective, the SSA form is nowadays fairly well understood, as witnessed by rec
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b170bf90b1d42488c2fa4927dd41c0f4
https://hal.archives-ouvertes.fr/hal-01378393
https://hal.archives-ouvertes.fr/hal-01378393
Publikováno v:
24th International Conference on Compiler Construction, CC 2015
24th International Conference on Compiler Construction, CC 2015, 2015, London, United Kingdom
Lecture Notes in Computer Science ISBN: 9783662466629
CC
24th International Conference on Compiler Construction, CC 2015, 2015, London, United Kingdom
Lecture Notes in Computer Science ISBN: 9783662466629
CC
The Static Single Assignment (SSA) form is a predominant technology in modern compilers, enabling powerful and fast program optimizations. Despite its great success in the implementation of production compilers, it is only very recently that this tec
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8cb0ef16f070ddcb063420ee8a59e0e1
https://inria.hal.science/hal-01110779
https://inria.hal.science/hal-01110779
Publikováno v:
Interactive Theorem Proving ISBN: 9783319221014
ITP
Interactive Theorem Proving
Interactive Theorem Proving, Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_6⟩
ITP
Interactive Theorem Proving
Interactive Theorem Proving, Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_6⟩
International audience; The problem of computing dominators in a control flow graph is central to numerous modern compiler optimizations. Many efficient algorithms have been proposed in the litterature, but mechanizing the correctness of the most sop
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9135835a07e64a4631d11c0a24b657f7
https://doi.org/10.1007/978-3-319-22102-1_6
https://doi.org/10.1007/978-3-319-22102-1_6