About Me

Computer scientist located in London, UK, working on static 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.

News

• 2021/04/01 Gave a talk at ESOP’21 on formalizing the Solidity memory model.
• 2021/03/08 I’m happy to join the group of Dino Distefano at Facebook to work on static analysis.
• 2021/01/22 Competition contribution paper accepted to TACAS 2021.
• 2020/12/16 Our gazer-theta toolchain qualified to SV-COMP’21.
• 2020/11/27 I defended my thesis and officially got my PhD.
• 2020/10/27 Paper on cloud-based model checking with IncQuery Labs and NASA JPL published.

Research Interests

• 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

Employment

• 2021 - present: Facebook, London, UK, Software engineer
  Working on static analysis for source 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.

Tools

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

Selected Publications

• 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

Research Projects

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

Service

• PC member: OMBEE’21, FMICS’21, MSR’21-shadow, SV-COMP’21, OMBEE’20
• AE PC member: TAP’21, PLDI’21, TAP’20, VMCAI’20
• Subreviewer: 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