T. Karvi, M. Tienari and R. Kaivola: Stepwise Development of Process-Algebraic Specifications in Decorated Trace Semantics, accepted for publication in Formal Methods in System Design.

M.Luukkainen, V.K.Shanbhag, K.Gopinath: Verifying a UMTS protocol using Spin and EASN, Electronic Notes in Theoretical Computer Science, Volume 118, Proceedings of International Workshop on Software Verification and Validation, December 2003
T.Malinen, M.Luukkainen: Fairness in automata theoretic model checking, Proceedings of Estonian Academy of Sciences - Physics and Mathematics, Special issue on programming theory, 52 4 (2003), 394-412
M.Luukkainen: A process algebraic reduction strategy for automata theoretic verification of untimed and timed concurrent systems , Ph.D. thesis, Report A-2003-7, Department of Computer Science, University of Helsinki.

V.K.Shanbhag, K.Gopinath, M.Turunen, A.Ahtiainen, M.Luukkainen: EASN: Integrating ASN.1 and model checking, Proceedings of 13th Conference on Computer Aided Verification (CAV'01), 2001
M.Luukkainen: Verification of dense time properties using theories of untimed process algebra, Proceedings of 20th Conference on Formal Description Techniques for Networked Systems (FORTE'01),2001
M.Luukkainen:Verification of Bounded retransmission protocol with a process algebra based method for dense time, Proceedings of the 1st workshop on Real Time Tools (RT-TOOLS'01), 2001

T.Karvi: Partially Lotos defined specifications and their refinement relations, Ph.D. thesis, Report A-2000-5, Department of Computer Science, University of Helsinki.
M.Luukkainen: Timed semantics of concurrent systems, Ph.Lic. Thesis, Report C-2000-4, Department of Computer Science, University of Helsinki.
S.Leppänen, M.Luukkainen:Compositional verification of a Third generation mobile communication protocol. Proceedings of the 1st Workshop on Distributed System Validation and Verification (DSVV'00), 2000

M.Luukkainen, A.Ahtiainen:Compositional verification of SDL descriptions, Proceedings of the 1st Workshop of the SDL Forum Society on SDL and MSC (SAM'98), 1998
R. Kaivola: Axiomatising extended computation tree logic. Theoretical Computer Science 190, 1 (1998), 41-60.

J. Eloranta, M. Tienari and A. Valmari: Essential transitions to bisimulation equivalences. Theoretical Computer Science 179, 1/2 (1997), 397-419.
R. Kaivola: Using compositional preorders in the verification of sliding window protocol. In: Proc. CAV '97, 9th International Conference on Computer-Aided Verification (ed. O. Grumberg), Lecture Notes in Computer Science 1254, Springer, 1997, 48-59.
R. Kaivola: Using Automata to Characterise Fixed Point Temporal Logics. Ph.D. Thesis, Report CST-135-97 (ECS-LFCS-97-356), Department of Computer Science, University of Edinburgh, 1997.

R. Kaivola: Axiomatising extended computation tree logic. In: Proc. CAAP '96, Colloquium on Trees in Algebra and Programming, Lecture Notes in Computer Science 1059, Springer, Berlin, 1996, pp. 87-101.
R. Kaivola: Fixpoints for Rabin tree automata make complementation easy. In: Proc. ICALP '96, 23rd International Colloquium on Automata, Languages and Programming (eds. F. Meyer auf der Heide and B. Monien), Lecture Notes in Computer Science 1099, Springer, 1996, 312-323.
R. Kaivola: Equivalences, preorders and compositional verification for linear time temporal logic and concurrent systems. Ph.D. Thesis, Report A-1996-1, Department of Computer Science, University of Helsinki, 1996.

R. Kaivola: Axiomatising linear time mu-calculus. In: Proc. CONCUR '95, Concurrency theory, 6th International Conference (ed. I. Lee and S. Smolka), Lecture Notes in Computer Science 962, Springer-Verlag, Berlin, 1995, 423-437.
R. Kaivola: On modal mu-calculus and Büchi tree automata. Information Processing Letters 54 (1995), 17-22.
R. Kaivola: A simple decision method for the linear time mu-calculus Proc. International Workshop on Structures in Concurrency Theory (STRICT) (ed. J. Desel), Springer-Verlag, Berlin 1995, 190-204.
A. Valmari and M. Tienari: Compositional Failure-Based Semantic Models for Basic LOTOS. Formal Aspects of Computing 7 (1995), 440-468.

J.Eloranta: Minimal transition systems with respect to divergence preserving behavioural equivalences, Ph.D. Thesis, Report A-1994-1, Department of Computer Science, University of Helsinki.

R. Kaivola: Compositional model checking for linear-time temporal logic. In: Proc. CAV '92, Computer Aided Verification, Fourth International Workshop, Lecture Notes in Computer Science 663, Springer-Verlag, Berlin, 1993, 248-259.

R. Kaivola and A. Valmari: The weakest compositional semantic equivalence preserving nexttime-less linear temporal logic. In: Proc. CONCUR '92, 3rd International Conference on Concurrency Theory (ed. W. Cleaveland), Lecture Notes in Computer Science 630, Springer-Verlag, Berlin, 1992, 207-221.

A. Valmari and M. Tienari: An improved failures equivalence for finite-state systems with a reduction algorithm. In: Protocol Specification, Testing, and Verification, XI. Proc. IFIP WG 6.1 11th International Symposium (ed. B. Jonsson et al.), North-Holland, Amsterdam, 1991, 1-18.
R. Kaivola and A. Valmari: Using truth-preserving reductions to improve the clarity of Kripke-models. In: Proc. CONCUR '91, 2nd International Conference on Concurrency Theory (ed. J. Baeten et al.), Lecture Notes in Computer Science 527, Springer-Verlag, Berlin, 1991, 361-375.
J.Eloranta: Equivalence concepts and algorithms for CCS-like languages, Ph.Lic. Thesis, Report C-1991-2, Department of Computer Science, University of Helsinki.
J.Eloranta: Minimizing the number of transitions with respect to observation equivalence , BIT 31(1991), 576-590.

M.Tienari, K.Aaltonen, J.Eloranta, J.Keskinen, K.Lehtinen, L.Summanen, K.Tarpila, and I.Turunen: PROTAN88 - A software tool for verifying communication protocols specified with an extended state transition model. Report A-1988-5, Department of Computer Science, University of Helsinki, 1988.