About Me

Computer scientist located in London, UK, working on static/dynamic program analysis at Meta/WhatsApp. PhD in formal methods from BME, Hungary. Former intern at CERN and SRI International. Feeling the most comfortable at the intersection of theory and practice, adopting research results in real-world applications.

Education

2016 - 2020: Budapest University of Technology and Economics
Computer science PhD, advised by Dr. Zoltán Micskei
Dissertation: Effective Domain-Specific Formal Verification Techniques
2014 - 2016: Budapest University of Technology and Economics
Computer Engineering MSc thesis
2010 - 2014: Budapest University of Technology and Economics
Computer Engineering BSc thesis

Employment

2021 - present: Meta/WhatsApp, London, UK, Software engineer
Working on automated static and dynamic program analysis tools for WhatsApp server (Erlang) and clients (Android/iOS), mostly concerning reliability, performance and privacy properties.
2019 - 2021: Budapest University of Technology and Economics, Assistant lecturer
Involved in research, projects and education at the Critical Systems Research Group, related to software model checking and other verification techniques.

Internships

2019: SRI International, New York, USA (12 weeks)
Formalizing and verifying advanced data structures in Solidity.
2018: SRI International, New York, USA (12 weeks)
Developing solc-verify, a formal verification tool for Solidity smart contracts.
2017: McGill University, Montréal, Canada (8 weeks)
Working on functional verification for cyber-physical systems.
2015: CERN, Geneva, Switzerland (10 weeks)
Developing code generation in ROOT, a data analysis framework for the experiments.
2013: evopro, Budapest, Hungary (6 weeks)
Modeling and analyzing public transportation networks using Petri nets.

Tools and Projects

2021 - present: Infer
Infer is a general purpose static analysis platform developed at Meta. I am working on the Erlang frontend, a callgraph reachability analysis and the integrations with WhatsApp server and client codebases.
2022 - 2024: Sapienz
I worked on integrating Sapienz – an automated UI testing engine – with WhatsApp iOS client to perform taint analysis of privacy properties.
2021 - 2022: FAUSTA
FAUSTA is an automated testing for WhatsApp server with traffic generation. I worked on more precise fault localization.
2015 - 2021: Theta
Theta is a generic, modular and configurable model checking framework. I was one of the original founders and main developers, focusing on the abstraction-based algorithms for transition systems and programs.

Selected Publications

FSE’24 Automated End-to-End Dynamic Taint Analysis for WhatsApp
With S. Cela, A. Ciancone, P. Gustafsson, Y. Jia, T. Kapus, M. Koshtenko, W. Lewis, K. Mao, D. Martac paper
ICSE’24 PrivacyCAT: Privacy-Aware Code Analysis at Scale
With K. Mao, C. Ahs, S. Cela, D. Distefao, N. Gardner, R. Grigore, P. Gustafsson, T. Kapus, M. Marescotti, G. Cunha Sampaio, T. Suzanne paper
ICST’22 FAUSTA: Scaling Dynamic Analysis with Traffic Generation at WhatsApp
With K. Mao, T. Kapus, L. Petrou, M. Marescotti, A. Löscher, M. Harman, D. Distefano paper
VSTTE’19 solc-verify: A Modular Verifier for Solidity Smart Contracts
With D. Jovanović paper slides
FMCAD’17 Theta: a Framework for Abstraction Refinement-Based Model Checking
With T. Tóth, A. Vörös, Z. Micskei, I. Majzik paper slides talk

Full list of publications / Google Scholar / dblp

Service

PC chair: Erlang’25, FormaliSE’25-AE, Infer’23
PC member: Infer’24, FormaliSE’23, VMCAI’23, WoSoCer’22, FORTE’22, OMBEE’21, FMICS’21, MSR’21-shadow, SV-COMP’21, OMBEE’20
AE PC member: CAV’22, TAP’21, PLDI’21, TAP’20, VMCAI’20
Journal reviewer: SCP’24, FAC’24, SCP’23, SQJ’22, STTT’22, IEEE Access’20
Subreviewer: VMCAI’22, POPL’22, FASE’21, MODELS’20, VSTTE’19, HASE’19, LADC’18, SRDS’17
Volunteer: DISC’19, AVM’17, SRDS’16, ICACON’15, DSN’13