| 751 | -- | 752 | Jim Woodcock, Cliff B. Jones. Editorial |
| 753 | -- | 788 | Artem Polyvyanyy, Marcello La Rosa, Chun Ouyang, Arthur H. M. ter Hofstede. Untanglings: a novel approach to analyzing concurrent systems |
| 789 | -- | 804 | Maryam Dabaghchian, Mohammad Abdollahi Azgomi. Model checking the observational determinism security property using PROMELA and SPIN |
| 805 | -- | 829 | Rachid Rebiha, Arnaldo Vieira Moura, Nadir Matringe. Generating invariants for non-linear loops by linear algebraic methods |
| 831 | -- | 865 | Pablo F. Castro, Nazareno Aguirre, Carlos López Pombo, T. S. E. Maibaum. Categorical foundations for structured specifications in Z |
| 867 | -- | 884 | Domenico Rosaci. Finding semantic associations in hierarchically structured groups of Web data |
| 885 | -- | 916 | Douglas Pereira Pasqualin, Juliana Kaizer Vizzotto, Eduardo Kessler Piveta. Typed context awareness Ambient Calculus for pervasive applications |
| 917 | -- | 949 | Omar I. Al-Bataineh, Mark Reynolds, Tim French. Accelerating worst case execution time analysis of timed automata models with cyclic behaviour |
| 951 | -- | 973 | Messaouda Bouneb, Djamel-Eddine Saïdouni, Jean-Michel Ilié. A reduced maximality labeled transition system generation for recursive Petri nets |
| 975 | -- | 1001 | Alexandre Mota, Adalberto Farias, Jim Woodcock, Peter Gorm Larsen. Model checking CML: tool development and industrial applications |