Verifying networks of processes that communicate via shared variables. - Tatjana Kapus; Bogomir Horvat (Microprocess. Microprogramming, 1992)

A true concurrency semantics for parallel programs. - Tatjana Kapus; Bogomir Horvat; Marjeta Pucko (Microprocess. Microprogramming, 1993)

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)

Specification of synchronous sequential circuits using SDL and ObjectGEODE. - Tatjana Kapus (Comput. Stand. Interfaces, 2002)

Mobile Agent System Specification using the Temporal Logic of Actions. - Tatjana Kapus (IASTED Conf. on Software Engineering, 2005)

Checking Connectivity in Mobile System Ambients with the Temporal Logic of Actions. - Tatjana Kapus (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2006)

Specification and Verification of a Parametric Handover Procedure Using TLA. - Tatjana Kapus (J. Circuits Syst. Comput., 2006)

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)

Using Mobile TLA as a Logic for Dynamic I/O Automata. - Tatjana Kapus (IEICE Trans. Inf. Syst., 2009)

Closing a System in the Dynamic Input/Output Automata Model. - Tatjana Kapus (Comput. J., 2011)

Modelling medium access control in IEEE 802.15.4 nonbeacon-enabled networks with probabilistic timed automata. - Tatjana Kapus (Mob. Inf. Syst., 2013)

Specifying and Verifying External Behaviour of Fair Input/Output Automata by Using the Temporal Logic of Actions. - Tatjana Kapus (Informatica, 2015)

Using PRISM model checker as a validation tool for an analytical model of IEEE 802.15.4 networks. - Tatjana Kapus (Simul. Model. Pract. Theory, 2017)

Specifying reversibility with TLA+. - Tatjana Kapus (J. Log. Algebraic Methods Program., 2020)

Generating and Employing Witness Automata for ACTLW Formulae. - Rok Vogrin; Robert Meolic; Tatjana Kapus (IEEE Access, 2022)

Improved Formal Verification of SDN-Based Firewalls by Using TLA+. - Tatjana Kapus (IEEE Access, 2023)