| 1996 | Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs (Extended Abstract). | Bernard Boigelot, Patrice Godefroid |
| 1996 | STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems. | Nikolaj S. Bjrner, Anca Browne, Edward Y. Chang, Michael Coln, Arjun Kapur, Zohar Manna, Henny Sipma, Toms E. Uribe |
| 1996 | Automated Verification by Induction with Associative-Commutative Operators. | Narjes Berregeb, Adel Bouhoula, Michal Rusinowitch |
| 1996 | Powerful Techniques for the Automatic Generation of Invariants. | Saddek Bensalem, Yassine Lakhnech, Hassen Sadi |
| 1996 | Verification of an Audio Protocol with Bus Collision Using UPPAAL. | Johan Bengtsson, W. O. David Griffioen, Kre J. Kristoffersen, Kim Guldstrand Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi |
| 1996 | Polynomial Time Algorithms for Testing Probabilistic Bisimulation and Simulation. | Christel Baier |
| 1996 | Verifying Continuous Time Markov Chains. | Adnan Aziz, Kumud Sanwal, Vigyan Singhal, Robert K. Brayton |
| 1996 | Symbolic Model Checking Using Algebraic Geometry. | George S. Avrunin |
| 1996 | MDG Tools for the Verification of RTL Designs. | K. D. Anon, N. Boulerice, Eduard Cerny, Francisco Corella, Michel Langevin, Xiaoyu Song, Sofine Tahar, Ying Xu, Zijian Zhou |
| 1996 | Marella: A Tool for Simulation and Verification. | Dominique Ambroise, Brigitte Rozoy |
| 1996 | Temporal Verification by Diagram Transformations. | Luca de Alfaro, Zohar Manna |
| 1995 | An Automata-Theoretic Approach to Fair Realizability and Synthesis. | Moshe Y. Vardi |
| 1995 | Local Model Checking for Real-Time Systems (Extended Abstract). | Oleg Sokolsky, Scott A. Smolka |
| 1995 | Toupie = µ-Calculus + Constraints. | Antoine Rauzy |
| 1995 | An Integration of Model Checking with Automated Proof Checking. | S. Rajan, Natarajan Shankar, Mandayam K. Srivas |
| 1995 | Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings. | Kenneth L. McMillan |
| 1995 | On Polynomial-Size Programs Winning Finite-State Games. | Helmut Lescow |
| 1995 | Modelling Asynchrony with a Synchronous Model. | Robert P. Kurshan, Michael Merritt, Ariel Orda, Sonia R. Sachs |
| 1995 | Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions. | Orna Kupferman |
| 1995 | The Rabin Index and Chain Automata, with Applications to Automatas and Games. | Sriram C. Krishnan, Anuj Puri, Robert K. Brayton, Pravin Varaiya |
| 1995 | Verifying Safety Properties of a Class of Infinite-State Distributed Algorithms. | Bengt Jonsson, Lars Kempe |
| 1995 | Safety Property Verification of ESTEREL Programs and Applications to Telecommunications Software. | Lalita Jategaonkar Jagadeesan, Carlos Puchol, James Von Olnhausen |
| 1995 | Efficient Timing Analysis of a Class of Petri Nets. | Henrik Hulgaard, Steven M. Burns |
| 1995 | Automated Analysis of an Audio Control Protocol. | Pei-Hsin Ho, Howard Wong-Toi |
| 1995 | Automatic Datapath Abstraction In Hardware Systems. | Ramin Hojati, Robert K. Brayton |