Extensions to the CEGAR Approach on Petri Nets. - Ákos Hajdu; András Vörös 001; Tamás Bartha; Zoltán Mártonka (Acta Cybern., 2014)

New Search Strategies for the Petri Net CEGAR Approach. - Ákos Hajdu; András Vörös 001; Tamás Bartha (Petri Nets, 2015)

PetriDotNet 1.5: Extensible Petri Net Editor and Analyser for Education and Research. - András Vörös 001; Dániel Darvas; Vince Molnár; Attila Klenik; Ákos Hajdu; Attila Jámbor; Tamás Bartha; István Majzik (Petri Nets, 2016)

A Configurable CEGAR Framework with Interpolation-Based Refinements. - Ákos Hajdu; Tamás Tóth; András Vörös 001; István Majzik (FORTE, 2016)

Theta: A framework for abstraction refinement-based model checking. - Tamás Tóth; Ákos Hajdu; András Vörös 001; Zoltán Micskei; István Majzik (FMCAD, 2017)

Exploiting Hierarchy in the Abstraction-Based Verification of Statecharts Using SMT Solvers. - Bence Czipó; Ákos Hajdu; Tamás Tóth; István Majzik (FESCA@ETAPS, 2017)

Towards Evaluating Size Reduction Techniques for Software Model Checking. - Gyula Sallai; Ákos Hajdu; Tamás Tóth; Zoltán Micskei (VPT@ETAPS, 2017)

Backward Reachability Analysis for Timed Automata with Data Variables. - Rebeka Farkas; Tamás Tóth; Ákos Hajdu; András Vörös 001 (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2018)

Industrial applications of the PetriDotNet modelling and analysis tool. - András Vörös 001; Dániel Darvas; Ákos Hajdu; Attila Klenik; Kristóf Marussy; Vince Molnár; Tamás Bartha; István Majzik (Sci. Comput. Program., 2018)

solc-verify: A Modular Verifier for Solidity Smart Contracts. - Ákos Hajdu; Dejan Jovanovic (VSTTE, 2019)

Formal Specification and Verification of Solidity Contracts with Events (Short Paper). - Ákos Hajdu; Dejan Jovanovic; Gabriela F. Ciocarlie (FMBC@CAV, 2020)

SMT-Friendly Formalization of the Solidity Memory Model. - Ákos Hajdu; Dejan Jovanovic (ESOP, 2020)

Model checking as a service: towards pragmatic hidden formal methods. - Benedek Horváth; Bence Graics; Ákos Hajdu; Zoltán Micskei; Vince Molnár; István Ráth; Luigi Andolfato; Ivan Gomes; Robert Karban (MoDELS (Companion), 2020)

Abstract: SMT-Friendly Formalization of the Solidity Memory Model. - Ákos Hajdu; Dejan Jovanovic (SMT, 2020)

Using Fault Injection to Assess Blockchain Systems in Presence of Faulty Smart Contracts. - Ákos Hajdu; Naghmeh Ramezani Ivaki; Imre Kocsis; Attila Klenik; László Gönczy; Nuno Laranjeiro; Henrique Madeira; András Pataricza (IEEE Access, 2020)

Formal Specification and Verification of Solidity Contracts with Events. - Ákos Hajdu; Dejan Jovanovic; Gabriela F. Ciocarlie (CoRR, 2020)

Efficient Strategies for CEGAR-Based Model Checking. - Ákos Hajdu; Zoltán Micskei (J. Autom. Reason., 2020)

Effective Domain-Specific Formal Verification Techniques - Ákos Hajdu (2020)

Bitvector Support in the Theta Formal Verification Framework. - Mihály Dobos-Kovács; Ákos Hajdu; András Vörös 001 (LADC, 2021)

Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution). - Zsófia Ádám; Gyula Sallai; Ákos Hajdu (TACAS (2), 2021)

InfERL: scalable and extensible Erlang static analysis. - Ákos Hajdu; Matteo Marescotti; Thibault Suzanne; Ke Mao; Radu Grigore; Per Gustafsson; Dino Distefano (Erlang Workshop, 2022)

FAUSTA: Scaling Dynamic Analysis with Traffic Generation at WhatsApp. - Ke Mao; Timotej Kapus; Lambros Petrou; Ákos Hajdu; Matteo Marescotti; Andreas Löscher; Mark Harman; Dino Distefano (ICST, 2022)

Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution). - Zsófia Ádám; Levente Bajczi; Mihály Dobos-Kovács; Ákos Hajdu; Vince Molnár (TACAS (2), 2022)

Pragmatic verification and validation of industrial executable SysML models. - Benedek Horváth; Vince Molnár; Bence Graics; Ákos Hajdu; István Ráth; Ákos Horváth 001; Robert Karban; Gelys Trancho; Zoltán Micskei (Syst. Eng., 2023)

PrivacyCAT: Privacy-Aware Code Analysis at Scale. - Ke Mao; Cons Åhs; Sopot Cela; Dino Distefano; Nick Gardner; Radu Grigore; Per Gustafsson; Ákos Hajdu; Timotej Kapus; Matteo Marescotti; Gabriela Cunha Sampaio; Thibault Suzanne (ICSE-SEIP, 2024)

Enhancing Compositional Static Analysis with Dynamic Analysis. - Dino Distefano; Matteo Marescotti; Cons Åhs; Sopot Cela; Gabriela Cunha Sampaio; Radu Grigore; Ákos Hajdu; Timotej Kapus; Ke Mao; Thibault Suzanne (ASE, 2024)

Automated End-to-End Dynamic Taint Analysis for WhatsApp. - Sopot Cela; Andrea Ciancone; Per Gustafsson; Ákos Hajdu; Yue Jia 001; Timotej Kapus; Maksym Koshtenko; Will Lewis; Ke Mao; Dragos Martac (SIGSOFT FSE Companion, 2024)

Compositional Static Callgraph Reachability Analysis for WhatsApp Android App Health. - Ákos Hajdu; Roman Lee; Gavin Weng; Nilesh Agrawal; Jérémy Dubreil (SOAP@PLDI, 2025)