Rehan MALAK

(GPG)

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

Software

Formal methods and Proof assistant

Embedded/IoT OS internals

Binaries and compilation

Cryptography and Trusted Execution Environment

Debugging

Linux

Virtualization

Architecture

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