Hello !

Welcome to my personal page. Currently, I am working as a senior verification engineer at Arteris IP. I develop innovative verification methodologies for highly parametric Network-on-Chips (NoCs).

Previously, I have completed my PhD thesis at Institut Polytechnique de Paris under the supervision of Florian Brandner, Mihail Asavoae, and Lirida Naviner.

I am quite enthusiastic about learning and staying in touch with many different areas. Nevertheless, my main research interest (and expertise) is on using formal methods to design correct-by-construction hardware.

Alternative resources

You can download my CV here. You can also visit my Google Scholar page or my Linkedin page.

Education

PhD at Institut Polytechnique de Paris, Paris, France (2020-2024). Thesis: Secure Dynamic Memory Hierarchy.
MsC at Télécom Paris & Université Paris-Saclay, Paris, France (2018-2020). Thesis: Implementation of a biometric library in a multi-core Trusted Execution Environment (TEE). GPA: 16.2/20.
BsC in Electrical Engineering at Universidade Federal de Minas Gerais (UFMG), Belo Horizonte, Brazil (2015-2020). Focus on electronics and computer micro-architecture.
Technical Degree in Industrial Automation at Instituto Federal de Minas Gerais (IFMG), Ouro Preto, Brazil (2012-2014).

Professional Experience

Senior Verification Engineer at Arteris IP (Jul 2024 - present).
Graduate Research Intern at Collins Aerospace (Jan 2023 - Jun 2023) . I have been applying formal methods to verify the correctness of customised RISC-V microarchitectures -- with a strong focus on security and crypto-accelerators.
Intern at Trustonic (Mar 2020 - Sep 2020) . I implemented a biometric library and provided sample-code for fingerprint and face-recognitionin applications in a resource-limited Trusted Execution Environment (TEE). I've also contributed to the TEE by enabling C++ support on the kernel.

Teaching

Teaching assistant at Télécom Paris (2020 - present). I've been in charge of lab assignments for the following courses: SE201, about Computer Architecture; INF103, about Java and GUIs; INF104, about C programming; and INF106, about Operational Systems and Concurrency.

Publications (from most to least recent)

(Accepted) Lisboa Malaquias, F. , Asavoae, M. & Brandner, F. Leveraging Reusable Code and Proofs to Design Complex DRAM Controllers – A Case Study. 27th Euromicro Conference Series on Digital System Design (DSD), 2024.
Lisboa Malaquias, F. , Asavoae, M. & Brandner, F. A formal framework to design and prove trustworthy memory controllers. Real-Time Syst (2023). DOI
Lisboa Malaquias, F., Giantamidis, G., Basagiannis, S., Fulvio Rollini, S., & Amundson, I. (2023). Towards a Methodology to Design Provably Secure Cyber-physical Systems. ACM SIGAda Ada Letters, 43(1), 94-99. DOI
Malaquias, Felipe Lisboa, Mihail Asavoae, and Florian Brandner. "From the Standards to Silicon: Formally Proved Memory Controllers." NASA Formal Methods: 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings. Cham: Springer Nature Switzerland, 2023. DOI, AAM
(Best Paper Award) Felipe Lisboa Malaquias, Mihail Asavoae, and Florian Brandner. 2022. A Coq Framework for More Trustworthy DRAM Controllers. In Proceedings of the 30th International Conference on Real-Time Networks and Systems (RTNS ’22), June 7–8, 2022, Paris, France. ACM, New York, NY, USA, 11 pages.

Awards and Honors

Best Paper Award (RTNS, 2022).
1st place at the 1st National RISC-V student contest (Paris, France, 2021). Organised by Thales, CNFM, and the GdR SOC2.
CAPES BRAFITEC Excellence Double Degree Fellowship (Belo Horizonte, Brazil, 2018). Granted by CAPES.
1st place at CoRA, the Autonomous Robot Competition (Belo Horizonte, Brazil, 2016). Organised by PETEE, School of Enginering, UFMG. Along with two teamates, I’ve designed a high speed line follower robot. Our robot’s performance granted us first place in the competition. You can check out the video from the championship round here. The software running on it is here.

Other Research Projects

Superscalar Processor Timing Anomalies Detector. A software written in C to detect timing anomalies in super-scalar processor trace executions.
RISC-V National Competition. My changes on the Ariane processor that awarded my first place on the 1st National RISC-V student contest.

Skills

Proficiency: C, and the Coq Theorem Prover.
Working level: SystemVerilog/Verilog, C++, Python, Java.
Basic knownledge:
- Functional programming languages: Haskell, OCaml, Scala.
- Formal verification languages/tools: F*, UPPALL, TLA+.
- Other: Matlab, HTML, CSS, SQL.

Trivia

I am passionate about languages. I can currently speak six languages: Portuguese, English, French, Spanish, Italian, and German.