Computer scientist mainly located in Budapest, Hungary, currently pursuing PhD studies in formal methods and verification techniques. 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, SMT, abstraction, CEGAR
- Verification of software, smart contracts and Petri nets
- Tool and framework development
- Experimental evaluation and analysis
Education and Degrees
- 2016 - present: Budapest University of Technology and Economics
Advised by Dr. Zoltán Micskei
- 2014 - 2016: Budapest University of Technology and Economics
Computer Engineering MSc thesis
- 2010 - 2014: Budapest University of Technology and Economics
Computer Engineering BSc thesis
Research Visits, Internships
- 2019: SRI International, New York, USA, Internship (12 weeks)
Formalizing and verifying advanced data structures in Solidity. tool paper
- 2018: SRI International, New York, USA, Internship (12 weeks)
Developing solc-verify, a formal verification tool for Solidity smart contracts. tool paper
- 2017: McGill University, Montréal, Canada, Research visit (8 weeks)
Working on functional verification for cyber-physical systems. talk
- 2015: CERN, Geneva, Switzerland, Internship (10 weeks)
Developing code generation in ROOT, a data analysis framework for the experiments. tool report
- 2013: evopro, Budapest, Hungary, Internship (6 weeks)
Modeling and analyzing public transportation networks using Petri nets. paper
- 2018 - present: solc-verify
Automated formal verification for Solidity smart contracts.
- 2016 - present: Theta
Generic, modular and configurable verification framework.
- 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
- 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 talk
- 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 talk
- ICATPN’15 New search strategies for the Petri net CEGAR approach
With A. Vörös, T. Bartha paper talk
Full list of publications / Google Scholar / dblp
- 2019 - present: ADVANCE
Addressing Verification and Validation Challenges in Future Cyber-Physical Systems.
- 2017 - 2018: CERN-BME Collaboration
Application of formal methods to verify industrial control code.
- 2016 - present: MTA-BME Lendület
Functional verification for cyber-physical systems.
- Current: Formal Methods (MSc), Integration and Verification Techniques (BSc), Software and Systems Verification (MSc), Software Verification and Validation (PhD), Systems Engineering Laboratory 1-2 (BSc)
- Former: Basics of Programming 1-2 (BSc), Databases (BSc), Intelligent Systems Supervision (BSc), IT Engineering Laboratory 2 (BSc), Software Laboratory 1-2 (BSc)
Summer Schools, Seminars