Computer scientist, PhD
Software Engineer at Meta
akoshajdu@meta.com
Publications
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.
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.
Education
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.
- 2021 - present: Infer
Infer is a general purpose static analysis platform developed at Meta. I am working on the integrations of Infer on WhatsApp codebases (server/Android/iOS), including the Erlang frontend and some customized analyses.
- 2022 - 2024: Sapienz
I worked on integrating Sapienz – an automated UI testing engine – with the WhatsApp iOS client to perform taint analysis for privacy properties.
- 2021 - 2022: FAUSTA
FAUSTA is a traffic generation-based automated testing tool for WhatsApp server. 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
- SOAP’25 Compositional Static Callgraph Reachability Analysis for WhatsApp Android App Health paper slides
- FSE’24 Automated End-to-End Dynamic Taint Analysis for WhatsApp paper slides
- ICSE’24 PrivacyCAT: Privacy-Aware Code Analysis at Scale paper
- ICST’22 FAUSTA: Scaling Dynamic Analysis with Traffic Generation at WhatsApp paper
- VSTTE’19 solc-verify: A Modular Verifier for Solidity Smart Contracts paper slides
- FMCAD’17 Theta: a Framework for Abstraction Refinement-Based Model Checking 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