About Me

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.

Research Interests

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
PhD student/candidate
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

2018-19: SRI International, New York, USA, Internship (2x3 months)
Formal verification of Solidity smart contracts on the Ethereum blockchain. [tool] [paper]
2017: McGill University, Montréal, Canada, Research visit (8 weeks)
Development of functional verification for cyber-physical systems. [talk]
2015: CERN, Geneva, Switzerland, Internship (10 weeks)
Development of code generation in the ROOT data analysis framework. [tool] [report]
2013: evopro, Budapest, Hungary, Internship (6 weeks)
Modeling and analysis of public transportation networks using Petri nets. [paper]

Tools

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.

Participation in Research Projects

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.

Selected Publications

VSTTE’19 solc-verify: A Modular Verifier for Solidity Smart Contracts [paper] [talk]
With D. Jovanović
SCP’18 Industrial Applications of the PetriDotNet Modelling and Analysis Tool [paper]
With A. Vörös, D. Darvas, A. Klenik, K. Marussy, V. Molnár, T. Bartha, I. Majzik
FMCAD’17 Theta: a Framework for Abstraction Refinement-Based Model Checking [paper] [talk]
With T. Tóth, A. Vörös, Z. Micskei, I. Majzik
FORTE’16 A Configurable CEGAR Framework with Interpolation-based Refinements [paper] [talk]
With _T. Tóth, A. Vörös, I. Majzik
ICATPN’15 New search strategies for the Petri net CEGAR approach [paper] [talk]
With A. Vörös, T. Bartha

Full list of publications / Google Scholar / dblp

Teaching

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 Surveillance (BSc), IT Engineering Laboratory 2 (BSc), Software Laboratory 1-2 (BSc)

Professional Activities and Services

Subreviewer: VSTTE’19, HASE’19, LADC’18, SRDS’17
Local organization: DISC’19, AVM’17, SRDS’16, ICACON’15, DSN’13
Webmaster: DISC’19

Akos Hajdu