Rehan MALAK
blog : System Performance&Safety
Employment
2022-Today
Intrinsic ID, Eindhoven : Senior Software Engineer
Zign C development and integration of the SRAM-PUF Zign library in MCUBoot / MbedTLS
2018-2021
INRIA, Paris & Saclay & Lille : Software Engineer
Whisper C Linux kernel
Deducteam Ocaml Lambdapi
Toccata C C++ Why3
Fun C Contiki-NG
2017
MILIBOO, New York City : Software Engineer
Ekko C C++ Java U-boot, Linux kernel, Android app
Education
2012-2016
CEA, Saclay PhD High-Performance Computing
C C++ Python DynQCD, data analysis
2009-2011
Paris-Saclay University MSc Mathematics
2007-2009
Paris-Sorbonne University BSc Mathematics
2006
ENSIIE, Evry BSc Software Engineering
Languages
- C
- C++
- Ocaml
- Python
- Java
Software
Formal methods and Proof assistant
- Frama-C
- Why3
- Dedukti3
Embedded/IoT OS internals
- Contiki-NG
- Zephyr
- FreeRTOS
Binaries and compilation
- GCC
- GNU binutils
- LLVM
Cryptography and Trusted Execution Environment
- WolfSSL/OpenSSL
- MbedTLS/PSA
- TF-M/TF-A
Debugging
- GDB
- JLink
- OpenOCD
Linux
- Scheduler/RT
- FTrace
- DeviceTree
Virtualization
- Qemu/KVM
- Docker
Architecture
- ARM Cortex-M
- ARM Cortex-A
- Risc-V
Talks
Linux
Realtime linux scheduling latency (after S.Rostedt and B.De Oliveira)
CFS/RT mixed policies problematic use cases (after P. Sangappa, D. Giani and S. Turlapati, S. Bhat)
CPU topology exposed to Linux and Qemu topology/NUMA interesting examples
Formal methods
SMT solvers, CDCL and Tableaux-method and the Alt-Ergo core solvers (after the work of the Alt-Ergo team)
Runtime verification of Contiki-NG IoT OS with Frama-C + E-ACSL
Dedukti3 new features : proof mode with LSP server
The F* programming language and application to Wireguard (after B.Beurdouche, J-K. Zinzindohoue)
Lattice QCD
Leading-order HVP contribution to the anomalous magnetic moment of the muon in LQCD (PhD slides)
Publications, Conferences
Formal methods
R.M. , Digicosme
Dedukti 3 proof-mode with unification goals
B. Barras, R.M. , Types2020
A Semi-simplicial Model of System F in Dependent Type Theory Modulo Rewriting
A. Blanchard, A. Puccetti, G. Eberhardt, N. Mitton, R.M. , Vessedia
Verification engineering of safety and security critical dynamic industrial applications : report
Lattice QCD
S. Borsanyi et. al., Phys. Rev. Lett. 121 , no. 2 022002
HVP contribution to the anomalous magnetic moments of leptons from first principles
S. Borsanyi et. al., Phys. Rev., D96, no. 7 074507
Slope and curvature of the hadron vacuum polarization at vanishing virtuality from lattice QCD
R.M. , Z. Fodor, C. Hoelbling, L. Lellouch, A. Sastre, K. Szabo, PoS, LATTICE2014 161
Finite-volume corrections to the leading-order hadronic contribution to gμ-2
E. B. Gregory, Z. Fodor, C. Hoelbling, S. Krieg, L. Lellouch, R.M. , C. McNeile, K. Szabo, PoS, LATTICE2013 302
Leading-order hadronic contributions to gμ−2
S. Dürr et al. Phys.Rev., D90, no. 11 114504
Lattice QCD at the physical point meets SU(2) chiral perturbation theory