Automatic Formal Verification of Digital Systems using Prolog. - Zmago Brezocnik; Bogomir Horvat (ACM SIGCHI Bull., 1988)

Formal hardware specification and verification using prolog. - Zmago Brezocnik; Bogomir Horvat (Microprocessing and Microprogramming, 1989)

Exploiting Partitioned Transition Relations for Efficient Symbolic Model Checking in CTL. - Ales Casar; Zmago Brezocnik; Tatjana Kapus (ED&TC, 1996)

TLA-style Specification of a Mobile Network. - Tatjana Kapus; Zmago Brezocnik (EUROMICRO, 1997)

Microcomputer unit for control of distributed devices over computer networks. - Gregor Vrecko; Zmago Brezocnik; Tatjana Kapus; Bogomir Horvat; Andrej Duh (J. Syst. Archit., 1997)

Verification of XTP Context Management Closing Procedure in Style of TLA. - Tatjana Kapus; Zmago Brezocnik (Sci. Comput. Program., 1997)

Specifying and Verifying Dataflow Networks in TLA. - Tatjana Kapus; Zmago Brezocnik (Applied Informatics, 1999)

Automated generation of Promela model from SDL specification. - Bostjan Vlaovic; Aleksander Vreze; Zmago Brezocnik; Tatjana Kapus (Comput. Stand. Interfaces, 2007)

ACTLW - An action-based computation tree logic with unless operator. - Robert Meolic; Tatjana Kapus; Zmago Brezocnik (Inf. Sci., 2008)

Eclipse Plug-In for Spin and st2msc Tools-Tool Presentation. - Tim Kovse; Bostjan Vlaovic; Aleksander Vreze; Zmago Brezocnik (SPIN, 2009)

Sdl2pml - Tool for automated generation of Promela model from SDL specification. - Aleksander Vreze; Bostjan Vlaovic; Zmago Brezocnik (Comput. Stand. Interfaces, 2009)

SpinRCP: the eclipse rich client platform integrated development environment for the spin model checker. - Zmago Brezocnik; Bostjan Vlaovic; Aleksander Vreze (SPIN, 2014)

Applying Automated Model Extraction for Simulation and Verification of Real-Life SDL Specification With Spin. - Bostjan Vlaovic; Aleksander Vreze; Zmago Brezocnik (IEEE Access, 2017)

Accelerating Deep Learning Inference in Constrained Embedded Devices Using Hardware Loops and a Dot Product Unit. - Jure Vreca; Karl J. X. Sturm; Ernest Gungl; Farhad Merchant; Paolo Bientinesi; Rainer Leupers; Zmago Brezocnik (IEEE Access, 2020)