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.

News

2020/07/20 Gave a talk at FMBC@CAV 2020 on Solidity events.
2020/07/19 Gave an invited talk at WoSCA@ISSTA 2020 on the Solidity memory model.
2020/07/05 Gave a talk at SMT@IJCAR 2020 on formalizing the Solidity memory model.
2020/06/24 Paper on Solidity event verification accepted for presentation at FMBC@CAV 2020.
2020/06/20 Preprint on Solidity smart contract fault injection.
2020/04/29 Gave a talk at the Solidity Summit, on formal verification.
2020/04/18 Our ESOP paper on formalizing the Solidity memory model is published.

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
Dissertation (under review): 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

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

Tools

2018 - present: solc-verify
Automated formal verification for Solidity smart contracts.
GitHub paper talk
2016 - present: Theta
Generic, modular and configurable verification framework.
GitHub paper talk
2012 - 2016: PetriDotNet
Petri net modeling and analysis framework.
Website paper
2015 - 2015: ROOT
Data analysis framework of CERN for high energy physics.
GitHub report

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 - present: ADVANCE
Addressing Verification and Validation Challenges in Future Cyber-Physical Systems.
2019 - present: Arrowhead Tools
Automated tool chain for verication and validation of systems under development.
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.

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

Service

PC member: TAP’20-AE, VMCAI’20-AE
Subreviewer: MODELS’20, VSTTE’19, HASE’19, LADC’18, SRDS’17
Volunteer: DISC’19, AVM’17, SRDS’16, ICACON’15, DSN’13
Webmaster: DISC’19

Ákos Hajdu