hajduakos / hajduakos.github.io Goto Github PK

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, where the latest research results come to life in real-world solutions.

• 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

• 2021 - present: Meta/WhatsApp, London, UK, Software engineer
  Working on static and dynamic program analysis for WhatsApp server (Erlang) and clients (Android/iOS).
• 2019 - 2021: Budapest University of Technology and Economics, Assistant lecturer
  Involved in research, projects and education at the Critical Systems Research Group.

• 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.

• 2022 - present: Sapienz
  Automated UI testing for clients.
• 2021 - present: Infer
  Static analysis platform by Meta.
• 2021 - present: FAUSTA
  Automated testing for WhatsApp with traffic generation.
• 2015 - 2021: Theta
  Generic, modular and configurable model checking framework.

• 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
• ESOP'20 SMT-Friendly Formalization of the Solidity Memory Model
  With D. Jovanović   paper   slides   talk
• JAR'19 Efficient Strategies for CEGAR-Based Model Checking
  With Z. Micskei   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

• PC chair: 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