Publications by the Verification Algorithm Research Group 1993-

How to get these publications electronically:

At the end of some entries there is a link to an electronic copy at the publisher's website. In that case the paper can be downloaded from there.

If the code for a publication is a link, then the publication can be downloaded by clicking the link. Small differences between the electronic and published version are possible, in particular in the layout. If you have problems in downloading, please contact Valmari.

Other publications can be asked from the authors.

We try our best to conform to copyright regulations. Publications have been made electronically available according to the conditions stated by the publishers or other copyright holders (Springer-Verlag LNCS, IEEE Computer Society, Elsevier).

List of publications

[06-9] Hansen, H. & Valmari, A.: Operational Determinism and Fast Algorithms. Concurrency Theory, Proceedings of the 17th International Conference, CONCUR 2006, Bonn, Germany, August 27--30, 2006. Volume 4137 of Lecture Notes in Computer Science, Springer Verlag, pp. 188--202.

[06-8] Hansen, H. & Kervinen, A.: Minimal Counterexamples in O(n log n) Memory and O(n^2) Time. Proceedings of ACSD 2006, Sixth International Conference on Application of Concurrency to System Design, Turku, Finland. IEEE Computer Society Presss, pp. 133--142.

[06-7] Geldenhuys, J. & Hansen, H.: Larger Automata and Less Work for LTL Model Checking. Proceedings of the 13th SPIN Workshop on Model Checking Software, Vienna, Austria, March 30--April 1, 2006. Volume 3925 of Lecture Notes in Computer Science, Springer Verlag, pp. 53--70.

[06-6] Place holder for Antero's Doctoral Consortium paper. ???

[06-5] Geldenhuys, J.: Improvements in State Space Representation and Model Checking Algorithms. Dr. Tech. Thesis, Tampere University of Technology Publication 591, Tampere 2006, 114 p.

[06-4] Valmari, A.: Teaching Concepts of Compositional Concurrency with State Machines. Proceedings of the Workshop on Teaching Concurrency (TeaConc '2006), Turku, Finland, June 27, 2006. Åbo Akademi and TUCS, pp.41-55.

[06-3] Valmari, A.: Teaching mathematically demanding computer science topics to software engineering students: Is there any reason? Is there any hope? Invited talk. Proceedings of the Workshop on Teaching Concurrency (TeaConc '2006), Turku, Finland, June 27, 2006. Åbo Akademi and TUCS, pp. 1-8.

[06-2] Valmari, A. (editor): Model Checking Software, 13th International SPIN Workshop, Vienna, Austria, March/April 2006, Proceedings. Lecture Notes in Computer Science 3925, Springer-Verlag 2006. X+307 p.

[06-1] Valmari, A.: What the Small Rubik's Cube Taught Me about Data Structures, Information Theory and Randomisation. International Journal on Software Tools for Technology Transfer (STTT) (2006) 8(3): 180-194. Published online 16 February, 2006. Journal version of an invited talk in TACAS 2004, Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, Barcelona, Spain, March 29-April 2.

[05-5] Puhakka, A.: Using Fairness Constraints in Process-Algebraic Verification. Proceedings of ICTAC'2005, Second International Colloquium on Theoretical Aspects of Computing, October 17--21, Hanoi, Vietnam, Lecture Notes in Computer Science 3722, Springer-Verlag 2005, pp. 546--561.

[05-4] Valmari, A.: A Modern Mathematical Theory of Co-operating State Machines. Proceedings of the Algorithmic Information Theory Conference, Vaasa, Finland, May 16-18 2005, Proceedings of the University of Vaasa, Reports 124, ss. 201-214.

[05-3] Geldenhuys, J. & Valmari, A.: More Efficient On-the-fly LTL Verification with Tarjan's Algorithm. Theoretical Computer Science Vol. 345 1 (2005) pp. 60-82. An Elsevier web page near the article

[05-2] Kellomäki, T. Historialaajennus mallipohjaisessa testauksessa. Tietojenkäsittelytieteen päivät 2005, University of Oulu, Department of Information Processing Science, Working Papers Series B 67, pp. 131-135. (Proceedings of an event in Oulu, Finland, June 12 - 13.) In Finnish.

[05-1] Kellomäki, T. & Valmari, A.: A Method for Analysing the Performance of Certain Testing Techniques for Concurrent Systems. Proceedings of ACSD 2005, Fifth International Conference on Application of Concurrency to System Design, St. Malo, France, June 7-9, IEEE Computer Society Press, pp. 154--163. An improved version of [04-7].

[04-9] Erkkilä, T.: LSTS-tiedostojenkäsittelykirjasto (The LSTS File Processing Library). M. Sc. (Eng.) Thesis, Tampere University of Technology, January 2004, in Finnish, 70 p.

[04-8] Kervinen, A. & Virolainen, P.: Konferenssiprotokollan automaattinen testaus (Automatic Testing of a Conference Protocol). Tietojenkäsittelytiede 22, Tietojenkäsittelytieteen Seura 2004, pp. 35-46. In Finnish.

[04-7] Kellomäki, T. & Valmari, A.: A Method for Analysing the Performance of Testing Techniques for Concurrent Systems. Tampere University of Technology, Institute of Software Systems Report 37, 2004, 12 p. ISBN 952-15-1273-3, ISSN 1459-417X. (More recent version: [05-1].)

[04-6] Puhakka, A.: Weakest Congruences, Fairness and Compositional Process-Algebraic Verification. Dr. Tech. Thesis, Tampere University of Technology Publications 468, Tampere 2004, 176 p.

[04-5] Kervinen, A. & Virolainen, P.: Konferenssiprotokollan automaattinen testaus (Automatic Testing of a Conference Protocol). Proceedings of Tietojenkäsittelytieteen päivät 2004, Joensuu, Finland, May 2004, pp. 44-48. In Finnish. See [04-8].

[04-4] Geldenhuys, J.: State Caching Reconsidered. Proceedings of Model Checking Software: 11th International SPIN Workshop, Barcelona, Spain, April 1-3, 2004, Lecture Notes in Computer Science 2989, Springer-Verlag 2004, pp. 23-38. LNCS #2989

[04-3] Virtanen, H., Hansen, H., Valmari, A., Nieminen, J. & Erkkilä, T.: Tampere Verification Tool. Proceedings of TACAS 2004, Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, Barcelona, Spain, March 29-April 2, Lecture Notes in Computer Science 2988, Springer-Verlag 2004, pp. 153-157. LNCS #2988

[04-2] Geldenhuys, J. & Valmari, A.: Tarjan's Algorithm Makes On-the-Fly LTL Verification More Efficient. Proceedings of TACAS 2004, Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, Barcelona, Spain, March 29-April 2, Lecture Notes in Computer Science 2988, Springer-Verlag 2004, pp. 205-219. LNCS #2988

[04-1] Kervinen, A. & Virolainen, P.: Heuristics for Faster Error Detection with Automated Black Box Testing. Proceedings of International workshop on Model Based Testing (MBT'04), Barcelona, Spain, March 27-28, 2004, Electronic Notes in Theoretical Computer Science 111, Elsevier 2005, pp. 53-71. Earlier version [03-8].

[03-8] Kervinen, A. & Virolainen, P.: Heuristics for Faster Error Detection with Automated Black Box Testing. Tampere University of Technology, Institute of Software Systems, Report 35, 2003. (More recent version: [04-1])

[03-7] Kivelä, T.: Muuttujallisten tilakoneiden kääntäjä verifiointitarkoituksiin (A Verification-Oriented Compiler for State Machines with Variables). M. Sc. (Eng.) Thesis, Tampere University of Technology, January 2003. In Finnish. 52 p.

[03-6] Puhakka, A.: Using Fairness in Process-Algebraic Verification. Tampere University of Technology, Institute of Software Systems Report 24, 2003, 39 p. Available in PDF.

[03-5] Hansen, H., Virtanen, H. & Valmari, A.: Merging State-based and Action-based Verification. Proceedings of ACSD 03, Third International Conference on Application of Concurrency to System Design, Guimaraes, Portugal, June 18-20, 2003, IEEE, pp 150-156.

[03-4] Kangas, A. & Valmari, A.: Verification with the Undefined: A New Look. Proc. Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS'03), Røros, Norway, June 5-7, 2003, ERCIM, pp. 122-137. Ed. Thomas Arts and Wan Fokkink. Also Electronic Notes in Theoretical Computer Science Volume 80, Elsevier Science, August 2003. PDF file at ENTCS website

[03-3] Kangas, A.: "Määrittelemätön" verifioinnissa: uusi näkökulma ("Undefined" in Verification: A New Point of View). Proc. Tietojenkäsittelytieteen päivät 2003, Espoo, Finland, May 2003, Ed. Ari Korhonen and Jorma Tarhio, Helsinki University of Technology TKO-A39/03, pp. 41-43. In Finnish.

[03-2] Geldenhuys, J. & Valmari, A.: A Nearly Memory-optimal Data Structure for Sets and Mappings. In Proceedings of the 10th International SPIN Workshop on Model Checking of Software, Lecture Notes in Computer Science #2648, pages 136-150. Springer-Verlag, May 2003. LNCS #2648

[03-1] Karsisto, K.: A New Parallel Composition Operator for Verification Tools. Dr.Tech. Thesis, Tampere University of Technology Publications 420, Tampere 2003, 114 p.

[02-5] Valmari, A. & Kervinen, A.: Alphabet-Based Synchronisation is Exponentially Cheaper. Proc. CONCUR 2002 -- Concurrency Theory, 13th International Conference, Brno, Czech Republic, 20-23 August 2002, Lecture Notes in Computer Science 2421, Springer-Verlag 2002, pp. 161-176.

[02-4] Valmari, A., Virtanen, H. & Puhakka, A.: Context-Sensitive Visibility. FMICS'02, 7th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, University of Malaga, Spain, 12-13 July 2002, pp. 201-217. Ed. Rance Cleaveland and Hubert Garavel, Electronic Notes in Theoretical Computer Science Volume 66 Issue 2, Elsevier Science, December 2002. PDF, PS ENTCS website.

[02-3] Hansen, H., Penczek, W. & Valmari, A: Stuttering-Insensitive Automata for On-the-fly Detection of Livelock Properties. FMICS'02 7th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, University of Malaga, Spain, 12-13 July 2002, pp. 185-200. Ed. Rance Cleaveland and Hubert Garavel, Electronic Notes in Theoretical Computer Science Volume 66 Issue 2, Elsevier Science, December 2002. ENTCS website

[02-2] Kilamo, T.: Vahva bisimulaatiominimointi (Strong Bisimulation Minimization). M. Sc. (Eng.) Thesis, Tampere University of Technology May 2002. In Finnish. 45 p.

[02-1] Nieminen, J.: Rinnankytkentäohjelman toteutustekniikoita (Implementation Techniques of a Parallel Composition Program). M. Sc. (Eng.) Thesis, Tampere University of Technology January 2002. In Finnish. 47 p.

[01-10] Peled, D., Valmari, A. & Kokkarinen, I.: Relaxed Visibility Enhances Partial Order Reduction. Formal Methods in System Design, 19, 275-289, 2001.

[01-9] Kervinen, A.: Erään tietoliikenneprotokollan verifiointi (Verification of a Communication Protocol). M. Sc. (Eng.) Thesis, Tampere University of Technology March 2001. In Finnish. 45 p.

[01-8] Puhakka, A: Weakest Congruence Results Concerning ``Any-Lock''. Proc. TACS'2001, Fourth International Symposium on Theoretical Aspects of Computer Software, October 29-31 2001, Sendai, Japan, Lecture Notes in Computer Science 2215, Springer-Verlag 2001, pp. 400-419.

[01-7] Puhakka, A. & Valmari, A.: Liveness and Fairness in Process-Algebraic Verification. CONCUR 2001 -- Concurrency Theory, 12th International Conference, Aalborg, Denmark, 21-24 August 2001, Lecture Notes in Computer Science 2154, Springer-Verlag 2001, pp. 202-217.

[01-6] Geldenhuys, J. & Valmari, A.: Techniques for Smaller Intermediary BDDs. CONCUR 2001 -- Concurrency Theory, 12th International Conference, Aalborg, Denmark, 21-24 August 2001, Lecture Notes in Computer Science 2154, Springer-Verlag 2001, pp. 233-247.

[01-5] Kervinen, A., Valmari, A. & Järnström, R.: Debugging a Real-life Protocol with CFFD-Based Verification Tools. FMICS 2001, 6th International Workshop on Formal Methods for Industrial Critical Systems, Paris, 16-17 July 2001, INRIA, pp. 13-27.

[01-4] Valmari, A.: Composition and Abstraction. Cassez, F., Jard., C., Rozoy, B. & Ryan, M. (eds.): Modelling and Verification of Parallel Processes. LNCS Tutorials, Lecture Notes in Computer Science 2067, Springer-Verlag 2001, pp. 58-99. Earlier version [00-4]. (Invited tutorial.)

[01-3] Puhakka, A.: Compositional Construction of Protocol Behaviours with Arbitrary Channel Capacities. Proc. ICECCS 2001, Seventh IEEE International Conference on Engineering of Complex Computer Systems, June 11-13, Skövde, Sweden, IEEE Computer Society Press, pp. 80-89.

[01-2] Valmari, A. & Yakovlev, A.: Message from the Programme Chairs. ICACSD 2001, 2nd IEEE International Conference on Application of Concurrency to System Design, Newcastle upon Tyne, U.K., 25-29 June, IEEE Computer Society 2001, pp. vii-viii. PDF file at IEEE Computer Society

[01-1] Helovuo, J. & Leppänen, S: Exploration Testing, ICACSD 2001, 2nd IEEE International Conference on Application of Concurrency to System Design, Newcastle upon Tyne, U.K., 25-29 June, IEEE Computer Society 2001, pp. 201-210.

[00-6] Valmari, A.: A Chaos-Free Failures Divergences Semantics with Applications to Verification. Millennial Perspectives in Computer Science: Proceedings of the 1999 Oxford--Microsoft Symposium in honour of Sir Tony Hoare, Palgrave "Cornerstones of Computing" series, 2000, pp. 365-382. (There were 36 talks, all of them invited by the organisers.)

[00-5] Virtanen, H.: Visual Verification Techniques. Movep '2k, Modelling and Verification of Parallel Processes, Proceedings of the Summer School, Nantes, France 19-23 June 2000, pp. 244-248.

[00-4] Valmari, A.: Composition and Abstraction. Movep '2k, Modelling and Verification of Parallel Processes, Proceedings of the Summer School, Nantes, France 19-23 June 2000, pp. 3-32. (More recent version: [01-4])

[00-3] Puhakka, A. & Valmari, A.: Livelocks, Fairness and Protocol Verification. Proceedings of Conference on Software: Theory and Practice, ICS2000, IFIP 16th World Computer Congress 2000, Beijing, China, August 21-25, 2000, pp. 471-479.

[00-2] Kristensen, L. M. & Valmari, A: Improved Question-Guided Stubborn Set Methods for State Properties. Application and Theory of Petri Nets 2000, 21st International Conference, Aarhus, Denmark, June 26-30, 2000, Proceedings, Lecture Notes in Computer Science 1825, Springer-Verlag 2000, pp. 282-302. Also Department of Computer Science, University of Aarhus, DAIMI PB-543, January 2000, 21 p.

[00-1] Helovuo, J. & Valmari, A: Checking for CFFD-Preorder with Tester Processes. Tools and Algorithms for the Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Berlin, March 27-31 2000, Proceedings, Lecture Notes in Computer Science 1785, Springer-Verlag 2000, pp. 283-298.

[99-2] Helovuo, J.: Automatic Testing Concepts for Reactive Systems. M. Sc. (Eng.) Thesis, Tampere University of Technology September 1999. 67 p.

[99-1] Puhakka, A. & Valmari, A.: Weakest-Congruence Results for Livelock-Preserving Equivalences. Proceedings of CONCUR '99 (Concurrency Theory), Lecture Notes in Computer Science 1664, Springer-Verlag 1999, pp. 510-524.

[98-4] Valmari, A.: The State Explosion Problem. Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science 1491, Springer-Verlag 1998, pp. 429-528.

[98-3] Kokkarinen, I: A Verification-Oriented Theory of Data in Labelled Transition Systems. Dr.Tech. Thesis, Tampere University of Technology Publications 234, Tampere 1998, 105 p.

[98-2] Kristensen, L. M. & Valmari, A.: Finding Stubborn Sets of Coloured Petri Nets Without Unfolding. Application and Theory of Petri Nets 1998, 19th International Conference, Lisbon, Portugal, June 1998, Proceedings, Lecture Notes in Computer Science 1420, Springer-Verlag 1998, pp. 104-123.

[98-1] Valmari, A. & Kokkarinen, I.: Unbounded Verification Results by Finite-State Compositional Techniques: 10^any States and Beyond. 1998 International Conference on Application of Concurrency to System Design, Proceedings, Aizu-Wakamatsu, Fukushima, Japan, March 1998, IEEE Computer Society, 75-85. (This paper, presented by AV, won the "Best Paper Award" of the conference. The winner was elected by the conference participants from 23 papers.)

[97-6] Kokkarinen, I: Symbolic Data in Labelled Transition Systems. Lic.Tech. Thesis, 1997, 52 pp.

[97-5] Eloranta, J., Tienari, M. & Valmari, A.: Essential Transitions to Bisimulation Equivalences. Theoretical Computer Science 179 (1997) 397-419.

[97-4] Kokkarinen, I., Peled, D. & Valmari, A.: Relaxed Visibility Enhances Partial Order Reduction. Computer Aided Verification, 9th International Conference, CAV'97, Haifa, Israel, June 1997, Proceedings, Lecture Notes in Computer Science 1254, Springer-Verlag 1997, pp. 328-339.

[97-3] Kokkarinen, I.: $\Omega$-Algebraic Data in Labelled Transition Systems. Proceedings of the Fifth Symposium on Programming Languages and Software Tools, Jyväskylä, Finland, June 1997, University of Helsinki, Department of Computer Science, Series of Publications C, Report C-1997-37, pp. 155-166.

[97-2] Puhakka, A. & Valmari, A.: Verification of Self-Synchronizing Alternating Bit Protocols with ARA. Proceedings of the Fifth Symposium on Programming Languages and Software Tools, Jyväskylä, Finland, June 1997, University of Helsinki, Department of Computer Science, Series of Publications C, Report C-1997-37, pp. 167-178.

[97-1] Karsisto, K.: A More Flexible Parallel Composition Operator. Proceedings of the Fifth Symposium on Programming Languages and Software Tools, Jyväskylä, Finland, June 1997, University of Helsinki, Department of Computer Science, Series of Publications C, Report C-1997-37, pp. 13-23.

[96-8] Karsisto, K.: Verification-Driven Development of Two Collision-Free Protocols for the Ethernet. M. Sc. (Eng.) Thesis, Tampere University of Technology 1996. 63 p.

[96-7] Valmari, A.: Stubborn Set Methods for Process Algebras. Proceedings of POMIV'96, Workshop on Partial Order Methods in Verification, Princeton, NJ, USA, July 24-26, 1996, DIMACS Series in Discrete Mathematics and Theoretical Computer Science Vol. 29, American Mathematical Society 1997, pp. 213-231. (Preliminary proceedings 1996, pp. 192-210.) (There were 25 talks, all of them invited by the organisers.)

[96-6] Karsisto, K. & Valmari, A.: Verification-Driven Development of a Collision-Avoidance Protocol for the Ethernet. Formal Techniques in Real-Time and Fault Tolerant Systems, 4th International Symposium, Uppsala, Sweden, Sept. 11-13, 1996, Proceedings, Lecture Notes in Computer Science 1135, Springer-Verlag 1996, pp. 228-245.

[96-5] Valmari, A.: Verification Algorithm Research Group at Tampere University of Technology. Tietojenkäsittelytiede, nr. 8, August 1996, pp. 25-38.

[96-4] Valmari, A.: Compositionality in State Space Verification Methods. Invited talk, Application and Theory of Petri Nets 1996, 17th International Conference, Osaka, Japan, June 1996, Proceedings, Lecture Notes in Computer Science 1091, Springer-Verlag 1996, pp. 29-56. (This was one of three one-hour invited talks during the conference. The conference had also 26 ordinary talks.)

[96-3] Valmari, A. & Setälä, M.: Visual Verification of Safety and Liveness. Proceedings of Formal Methods Europe '96: Industrial Benefit and Advances in Formal Methods, Lecture Notes in Computer Science 1051, Springer-Verlag 1996, pp. 228-247. Also Tampere University of Technology, Software Systems Laboratory, Report 17, Tampere, Finland, September 1995, 20 p.

[96-2] Valmari, A., Karsisto, K. & Setälä, M.: Visualisation of Reduced Abstracted Behaviour as a Design Tool. Proceedings of PDP'96, the Fourth Euromicro Workshop on Parallel and Distributed Processing, Braga, Portugal, January 24-26 1996, IEEE Computer Society Press, pp. 187-194.

[96-1] Valmari, A. & Savola, R.: Verification of the Behaviour of Reactive Software with CFFD-semantics and Ara Tools. Proceedings of an International Symposium on On-board Real-time Software, ESTEC, Noordwijk, The Netherlands, November 13-15 1995, ESA SP-375, January 1996, pp. 173-180. HTML version here.

[95-5] Valmari, A. & Tienari, M.: Compositional Failure-Based Semantic Models for Basic LOTOS. Formal Aspects of Computing (1995) 7: 440-468. Also Tampere University of Technology, Software Systems Laboratory, Report 16, Tampere, Finland, July 1993, 25 p.

[95-4] Kokkarinen, I.: Rinnankytketyn siirtymäsysteemin kutistaminen itsepäisillä joukoilla (Reduction of Parallel Labelled Transition Systems with Stubborn Sets). M. Sc. (Eng.) Thesis. In Finnish. 49 p.

[95-3] Savola, R.: A State Space Generation Tool for LOTOS Specifications. VTT Publications 241, Technical Research Centre of Finland (VTT), Espoo, Finland 1995, 107 p.

[95-2] Valmari, A.: Failure-based Equivalences Are Faster Than Many Believe. Structures in Concurrency Theory, Proceedings, Berlin, Germany, May 1995, Springer-Verlag "Workshops in Computing" series 1995, pp. 326-340.

[95-1] Valmari, A.: The Weakest Deadlock-Preserving Congruence. Information Processing Letters 53 (1995) 341-346.

[94-3] Setälä, M. & Valmari, A.: Validation and Verification with Weak Process Semantics. Proceedings of Nordic Seminar on Dependable Computing Systems 1994, Lyngby, Denmark, August 1994, pp. 15-26.

[94-2] Valmari, A.: Compositional Analysis with Place-Bordered Subnets. Application and Theory of Petri Nets 1994, 15th International Conference, Zaragoza, Spain, June 1994, Proceedings, Lecture Notes in Computer Science 815, Springer-Verlag 1994, pp. 531-547.

[94-1] Valmari, A.: State of the Art Report: Stubborn Sets. Invited article, Petri Net Newsletter 46, April 1994, pp. 6-14.

[93-3] Valmari, A.: On-the-fly Verification with Stubborn Sets. Proceedings of CAV '93, 5th International Conference on Computer-Aided Verification, Elounda, Greece, Lecture Notes in Computer Science 697, Springer-Verlag 1993, pp. 397-408.

[93-2] Valmari, A.: Compositional State Space Generation. Advances in Petri Nets 1993, Lecture Notes in Computer Science 674, Springer-Verlag 1993, pp. 427-457. (Also: Department of Computer Science, University of Helsinki, Report A-1991-5, Helsinki, Finland 1992, 30 p., and earlier version: Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris, France 1990, pp. 43-62.)

[93-1] Valmari, A., Kemppainen, J., Clegg, M. & Levanto, M.: Putting Advanced Reachability Analysis Techniques Together: the "ARA" Tool. Proceedings of Formal Methods Europe '93: Industrial-Strength Formal Methods, Lecture Notes in Computer Science 670, Springer-Verlag 1993, pp. 597-616. An improved version of [KL+92].


Antti Valmari, ava@cs.tut.fi, 2001-09-10