Jean-Christophe Léchenet

Tiago Oliveira

Peter Schwabe

IACR Trans. Cryptogr. Hardw. Embed. Syst., 2024

2023

Efficient computation of arbitrary control dependencies.

[BibT_eX]

[DOI]

Theor. Comput. Sci., August, 2023

Formally verifying Kyber Episode IV: Implementation correctness.

[BibT_eX]

[DOI]

IACR Trans. Cryptogr. Hardw. Embed. Syst., 2023

Formally verifying Kyber Part I: Implementation Correctness.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2023

Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi.

[BibT_eX]

[DOI]

Benjamin Grégoire

Enrico Tassi

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

2020

A Fast Verified Liveness Analysis in SSA Form.

[BibT_eX]

[DOI]

Sandrine Blazy

David Pichardie

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2018

Certified algorithms for program slicing. (Algorithmes certifiés pour la simplification syntaxique de programmes).

[BibT_eX]

[DOI]

PhD thesis, 2018

Cut branches before looking for bugs: certifiably sound verification on relaxed slices.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2018

Fast Computation of Arbitrary Control Dependencies.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2018

2016

Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2016

2014

Power Consumption Analysis of Parallel Algorithms on GPUs.

[BibT_eX]

[DOI]

Frédéric Magoulès

Abal-Kassim Cheik Ahamed

Alban Desmaison