Zobrazeno 1 - 4
of 4
pro vyhledávání: '"Cyril Six"'
Autor:
David Monniaux, Cyril Six
Publikováno v:
ACM Transactions on Embedded Computing Systems. 22:1-27
We present an approach for implementing a formally certified loop-invariant code motion optimization by composing an unrolling pass and a formally certified yet efficient global subexpression elimination. This approach is lightweight: each pass comes
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e43bea453d2e8e816b7ad7589aed0b08
https://doi.org/10.1145/3529507
https://doi.org/10.1145/3529507
Publikováno v:
Certified Programs and Proofs (CPP ’22)
Certified Programs and Proofs (CPP ’22), Jan 2022, Philadelphia, United States. ⟨10.1145/3497775.3503679⟩
CPP 2022: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs
Certified Programs and Proofs (CPP ’22), Jan 2022, Philadelphia, United States. pp.40-54, ⟨10.1145/3497775.3503679⟩
Certified Programs and Proofs (CPP ’22), Jan 2022, Philadelphia, United States. ⟨10.1145/3497775.3503679⟩
CPP 2022: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs
Certified Programs and Proofs (CPP ’22), Jan 2022, Philadelphia, United States. pp.40-54, ⟨10.1145/3497775.3503679⟩
International audience; Necula [2000] and Tristan et al. [2011] established that symbolic execution combined with rewriting is effective in validating the code produced by state-of-the-art compilers applying various optimizations. In the meantime, Tr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::dfa50dfc6287c390b68863a7bc40188c
https://hal.archives-ouvertes.fr/hal-03200774
https://hal.archives-ouvertes.fr/hal-03200774
Autor:
David Monniaux, Cyril Six
Publikováno v:
Languages, Compilers, Tools and Theory of Embedded Systems (LCTES)
Languages, Compilers, Tools and Theory of Embedded Systems (LCTES), ACM, Jun 2021, online, Canada. pp.85-96, ⟨10.1145/3461648.3463850⟩
LCTES
HAL
Languages, Compilers, Tools and Theory of Embedded Systems (LCTES), ACM, Jun 2021, online, Canada. pp.85-96, ⟨10.1145/3461648.3463850⟩
LCTES
HAL
International audience; We present an approach for implementing a formally certified loop-invariant code motion optimization by composing an unrolling pass and a formally certified yet efficient global subexpression elimination.This approach is light
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b272ed483e9cd8a87329c15aae52d9ce
https://hal.archives-ouvertes.fr/hal-03212087/file/CSE3_LCTES2021_HAL.pdf
https://hal.archives-ouvertes.fr/hal-03212087/file/CSE3_LCTES2021_HAL.pdf
Publikováno v:
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2020, OOPSLA 2020, pp.129. ⟨10.1145/3428197⟩
Proceedings of the ACM on Programming Languages, ACM, In press, OOPSLA 2020
Proceedings of the ACM on Programming Languages, ACM, 2020, OOPSLA 2020, 4, pp.129. ⟨10.1145/3428197⟩
Proceedings of the ACM on Programming Languages, ACM, 2020, OOPSLA 2020, pp.129. ⟨10.1145/3428197⟩
Proceedings of the ACM on Programming Languages, ACM, In press, OOPSLA 2020
Proceedings of the ACM on Programming Languages, ACM, 2020, OOPSLA 2020, 4, pp.129. ⟨10.1145/3428197⟩
CompCert is a moderately optimizing C compiler with a formal, machine-checked, proof of correctness: after successful compilation, the assembly code has a behavior faithful to the source code. Previously, it only supported target instruction sets wit
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::de52293d0b590074d22e7c603e3c9a65
https://hal.archives-ouvertes.fr/hal-02185883v3/document
https://hal.archives-ouvertes.fr/hal-02185883v3/document