Computer scientist located in London, UK, working on code analysis at Facebook.
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.
- Formal methods, model checking, static analysis, SAT/SMT, compilers
- Verification and analysis of software, smart contracts and system models
- Tool and framework development
- Experimental evaluation and data analysis
Education and Degrees
- 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: Facebook, London, UK, Software engineer
Working on developer infrastructure, including dynamic and static analysis of code.
- 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, Internship (12 weeks)
Formalizing and verifying advanced data structures in Solidity.
- 2018: SRI International, New York, USA, Internship (12 weeks)
Developing solc-verify, a formal verification tool for Solidity smart contracts.
- 2017: McGill University, Montréal, Canada, Research visit (8 weeks)
Working on functional verification for cyber-physical systems.
- 2015: CERN, Geneva, Switzerland, Internship (10 weeks)
Developing code generation in ROOT, a data analysis framework for the experiments.
- 2013: evopro, Budapest, Hungary, Internship (6 weeks)
Modeling and analyzing public transportation networks using Petri nets.
- 2021 - present: Infer
Static analysis tool by Facebook.
- 2018 - present: solc-verify
Automated formal verification for Solidity smart contracts.
- 2016 - present: Theta
Generic, modular and configurable verification framework.
- 2018 - present: Gazer
LLVM-based C program analysis frontend for Theta.
- 2017 - 2018: PLCVerif
PLC verification framework, supporting Theta as a backend.
- 2012 - 2016: PetriDotNet
Petri net modeling and analysis framework.
- 2015 - 2015: ROOT
Data analysis framework of CERN for high energy physics.
- 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
- SCP’18 Industrial Applications of the PetriDotNet Modelling and Analysis Tool
With A. Vörös, D. Darvas, A. Klenik, K. Marussy, V. Molnár, T. Bartha, I. Majzik paper
- 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
- ICATPN’15 New search strategies for the Petri net CEGAR approach
With A. Vörös, T. Bartha paper slides
Full list of publications / Google Scholar / dblp
- 2019 - 2021: MCaaS (with IncQuery Labs and NASA JPL)
Model Checking as a Service: cloud-based, push-button model checking for SysML statecharts.
- 2016 - 2020: MTA-BME Lendület
Functional verification for cyber-physical systems.
- 2017 - 2018: CERN-BME Collaboration
Application of formal methods to verify industrial control code.
- PC member: FORTE’22, OMBEE’21, FMICS’21, MSR’21-shadow, SV-COMP’21, OMBEE’20
- AE PC member: TAP’21, PLDI’21, TAP’20, VMCAI’20
- Subreviewer: VMCAI’22, POPL’22, FASE’21, IEEE Access’20, MODELS’20, VSTTE’19, HASE’19, LADC’18, SRDS’17
- Volunteer: DISC’19, AVM’17, SRDS’16, ICACON’15, DSN’13