| 1997 | A Brief Introduction to Coloured Petri Nets. Kurt Jensen |
| 1997 | A Tableau System for Linear-TIME Temporal Logic. Peter H. Schmitt, Jean Goubault-Larrecq |
| 1997 | A Tool to Support Formal Reasoning about Computer Languages. Richard J. Boulton |
| 1997 | An Automated Based Verification Environment for Mobile Processes. Gian-Luigi Ferrari, Gianluigi Ferro, Stefania Gnesi, Ugo Montanari, Marco Pistore, Gioia Ristori |
| 1997 | Automatic Synthesis of Specifications from the Dynamic Observation of Reactive Programs. Bernard Boigelot, Patrice Godefroid |
| 1997 | Combining Partial Order and Symmetry Reductions. E. Allen Emerson, Somesh Jha, Doron A. Peled |
| 1997 | Compositional Performance Analysis. Chris M. N. Tofts |
| 1997 | Compositional State Space Generation from Lotos Programs. Jean-Pierre Krimm, Laurent Mounier |
| 1997 | Design/CPN - A Computer Tool for Coloured Petri Nets. Søren Christensen, Jens Bæk Jørgensen, Lars Michael Kristensen |
| 1997 | Formal Verification of Statecharts with Instantaneous Chain Reaction. Jan Philipps, Peter Scholz |
| 1997 | Graphs in METAFrame: The Unifying Power of Polymorphism. Michael von der Beeck, Volker Braun, Andreas Claßen, Achim Dannecker, Carsten Friedrich, Dirk Koschützki, Tiziana Margaria, Falk Schreiber, Bernhard Steffen |
| 1997 | Hardware and Software Synthesis, Optimization, and Verification from Esterel Programs. Gérard Berry |
| 1997 | Incremental Development of Deadlock-Free Communicating Systems. Stephan Kleuker |
| 1997 | Integration in PVS: Tables, Types, and Model Checking. Sam Owre, John M. Rushby, Natarajan Shankar |
| 1997 | MOSEL: A FLexible Toolset for Monadic Second-Order Logic. Peter Kelb, Tiziana Margaria, Michael Mendler, Claudia Gsottberger |
| 1997 | Manipulation Algorithms for K*BMDs. Rolf Drechsler, Bernd Becker, Stefan Ruppertz |
| 1997 | Mechanically Verified Self-Stabilizing Hierarchical Algorithms. I. S. W. B. Prasetya |
| 1997 | Model-Checking for a Subclass of Event Structures. Wojciech Penczek |
| 1997 | Partial Model Checking with ROBDDs. Henrik Reif Andersen, Jørgen Staunstrup, Niels Maretti |
| 1997 | Real-Time Logics: Fictitious Clock as an Abstraction of Dense Time. Jean-François Raskin, Pierre-Yves Schobbens |
| 1997 | Space Efficient Reachability Analysis Through Use of Pseudo-Root States. Atanas N. Parashkevov, Jay Yantchev |
| 1997 | Syntactic Detection of Process Divergence and Non-local Choice inMessage Sequence Charts. Hanêne Ben-Abdallah, Stefan Leue |
| 1997 | Test Generation for Intelligent Networks Using Model Checking. André Engels, Loe M. G. Feijs, Sjouke Mauw |
| 1997 | The Bounded Retransmission Protocol Must Be on Time! Pedro R. D'Argenio, Joost-Pieter Katoen, Theo C. Ruys, Jan Tretmans |
| 1997 | The Reference Component of PEP. Bernd Grahlmann |
| 1997 | The Term Processor Generator Peter van Eijk, Axel Belinfante, Henk Eertink, Henk Alblas |
| 1997 | Theorem Prover Support for the Refinement of Stream Processing Functions. Robert Sandner, Olaf Müller |
| 1997 | Tools and Algorithms for Construction and Analysis of Systems, Third International Workshop, TACAS '97, Enschede, The Netherlands, April 2-4, 1997, Proceedings Ed Brinksma |
| 1997 | Visual Verification of Reactive Systems. Luca de Alfaro, Zohar Manna, Henny B. Sipma, Tomás E. Uribe |