Parallel Saturation Based Model Checking. - András Vörös 001; Tamás Szabó; Attila Jámbor; Dániel Darvas; Ákos Horváth 001; Tamás Bartha (ISPDC, 2011)

K-Induction Based Verification of Real-Time Safety Critical Systems. - Tamás Tóth; András Vörös 001; István Majzik (DepCoS-RELCOMEX, 2013)

Formal Verification of Complex Properties on PLC Programs. - Dániel Darvas; Borja Fernandez Adiego; András Vörös 001; Tamás Bartha; Enrique Blanco Viñuela; Víctor M. González Suárez (FORTE, 2014)

On Open Source Tools for Behavioral Modeling and Analysis with fUML and Alf. - Zoltán Micskei; Raimund-Andreas Konnerth; Benedek Horváth; Oszkár Semeráth; András Vörös 001; Dániel Varró (OSS4MDE@MoDELS, 2014)

Verification of a Real-Time Safety-Critical Protocol Using a Modelling Language with Formal Data and Behaviour Semantics. - Tamás Tóth; András Vörös 001 (SAFECOMP Workshops, 2014)

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)

SEViz: A Tool for Visualizing Symbolic Execution. - David Honfi; András Vörös 001; Zoltán Micskei (ICST, 2015)

A Decomposition Method for the Verification of a Real-Time Safety-Critical Protocol. - Tamás Tóth; András Vörös 001; István Majzik (SERENE, 2015)

Saturation-Based Incremental LTL Model Checking with Inductive Proofs. - Vince Molnár; Dániel Darvas; András Vörös 001; Tamás Bartha (TACAS, 2015)

Efficient Decomposition Algorithm for Stationary Analysis of Complex Stochastic Petri Net Models. - Kristóf Marussy; Attila Klenik; Vince Molnár; András Vörös 001; István Majzik; Miklós Telek (Petri Nets, 2016)

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)

Iterative and Incremental Model Generation by Logic Solvers. - Oszkár Semeráth; András Vörös 001; Dániel Varró (FASE, 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)

Improving Saturation-based Bounded Model Checking. - Dániel Darvas; András Vörös 001; Tamás Bartha (Acta Cybern., 2016)

Component-wise incremental LTL model checking. - Vince Molnár; András Vörös 001; Dániel Darvas; Tamás Bartha; István Majzik (Formal Aspects Comput., 2016)

Getting the Priorities Right: Saturation for Prioritised Petri Nets. - Kristóf Marussy; Vince Molnár; András Vörös 001; István Majzik (Petri Nets, 2017)

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)

Distributed Graph Queries for Runtime Monitoring of Cyber-Physical Systems. - Márton Búr; Gábor S. Szilágyi; András Vörös 001; Dániel Varró (FASE, 2018)

The Gamma statechart composition framework: : design, verification and code generation for component-based reactive systems. - Vince Molnár; Bence Graics; András Vörös 001; István Majzik; Dániel Varró (ICSE (Companion Volume), 2018)

MoDeS3: Model-Based Demonstrator for Smart and Safe Cyber-Physical Systems. - András Vörös 001; Márton Búr; István Ráth; Ákos Horváth 001; Zoltán Micskei; László Balogh; Bálint Hegyi; Benedek Horváth; Zsolt Mázló; Dániel Varró (NFM, 2018)

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)

Symbolic Verification of Petri Net Based Models - András Vörös 001 (2018)

Towards System-Level Testing with Coverage Guarantees for Autonomous Vehicles. - István Majzik; Oszkár Semeráth; Csaba Hajdu; Kristóf Marussy; Zoltán Szatmári; Zoltán Micskei; András Vörös 001; Aren A. Babikian; Dániel Varró (MoDELS, 2019)

Will My Program Break on This Faulty Processor?: Formal Analysis of Hardware Fault Activations in Concurrent Embedded Software. - Levente Bajczi; András Vörös 001; Vince Molnár (ACM Trans. Embed. Comput. Syst., 2019)

Simulation-based Safety Assessment of High-level Reliability Models. - Simon József Nagy; Bence Graics; Kristóf Marussy; András Vörös 001 (MARS@ETAPS, 2020)

Mixed-semantics composition of statecharts for the component-based design of reactive systems. - Bence Graics; Vince Molnár; András Vörös 001; István Majzik; Dániel Varró (Softw. Syst. Model., 2020)

Distributed graph queries over models@run.time for runtime monitoring of cyber-physical systems. - Márton Búr; Gábor S. Szilágyi; András Vörös 001; Dániel Varró (Int. J. Softw. Tools Technol. Transf., 2020)

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

Demonstrator for dependable edge-based cyber-physical systems. - Simon József Nagy; Richárd Szabó; Máté Levente Vajda; András Vörös 001 (LADC, 2021)

Towards formally analyzed Cyber-Physical Systems. - Richárd Szabó; András Vörös 001 (CoRR, 2021)

Evaluation of SMT solvers in abstraction-based software model checking. - Mihály Dobos-Kovács; András Vörös 001 (LADC, 2022)

Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification. - Márk Somorjai; Mihály Dobos-Kovács; Zsófia Ádám; Levente Bajczi; András Vörös 001 (LSFA/HCVS, 2023)

Towards the Formal Verification of SysML v2 Models. - Vince Molnár; Bence Graics; András Vörös 001; Stefano Tonetta; Luca Cristoforetti; Greg Kimberly; Pamela Dyer; Kristin Giammarco; Manfred Köthe; John Hester; Jamie Smith; Christoph Grimm 001 (MoDELS (Companion), 2024)

Reasoning with Happens-Before Relations About Concurrent Programs in the THETA Framework. - Csanád Telbisz; Levente Bajczi; Dániel Szekeres; András Vörös 001; István Majzik (DSN-W, 2025)

On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study). - Levente Bajczi; Csanád Telbisz; Dániel Szekeres; András Vörös 001 (TACAS (1), 2025)

Theta: Various Approaches for Concurrent Program Verification (Competition Contribution). - Csanád Telbisz; Levente Bajczi; Dániel Szekeres; András Vörös 001 (TACAS (3), 2025)