8. CAV 1996: New Brunswick, NJ, USA

• Bernard Boigelot, Patrice Godefroid:
  Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs (Extended Abstract). 1-12
  
• Kenneth L. McMillan:
  A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking. 13-25
  
• George S. Avrunin:
  Symbolic Model Checking Using Algebraic Geometry. 26-37
  
• Marco Pistore, Davide Sangiorgi:
  A Partition Refinement Algorithm for the pi-Calculus (Extended Abstract). 38-49
  
• Christel Baier:
  Polynomial Time Algorithms for Testing Probabilistic Bisimulation and Simulation. 50-61
  
• Igor Walukiewicz:
  Pushdown Processes: Games and Model Checking. 62-74
  
• Orna Kupferman, Moshe Y. Vardi:
  Module Checking. 75-86
  
• E. Allen Emerson, Kedar S. Namjoshi:
  Automatic Verification of Parameterized Synchronous Systems (Extended Abstract). 87-98
  
• Sandeep K. Shukla, Harry B. Hunt III, Daniel J. Rosenkrantz:
  HORNSAT, Model Checking, Verification and games (Extended Abstract). 99-110
  
• Edmund M. Clarke, Steven M. German, Xudong Zhao:
  Verifying the SRT Division Algorithm Using Theorem Proving Techniques. 111-122
  
• Harald Rueß, Natarajan Shankar, Mandayam K. Srivas:
  Modular Verification of SRT Division. 123-134
  
• Deepak Kapur, Mahadevan Subramaniam:
  Mechanically Verifying a Family of Multiplier Circuits. 135-146
  
• C. Norris Ip, David L. Dill:
  Verifying Systems with Replicated Components in Murphi. 147-158
  
• Masahiro Fujita:
  Verification of Arithmetic Circuits by Comparing Two Similar Circuits. 159-168
  
• John M. Rushby:
  Automated Deduction and Formal Methods. 169-183
  
• Amir Pnueli, Elad Shahar:
  A Platform for Combining Deductive with Algorithmic Verification. 184-195
  
• Susanne Graf, Hassen Saïdi:
  Verifying Invariants Using theorem Proving. 196-207
  
• Henny Sipma, Tomás E. Uribe, Zohar Manna:
  Deductive Model Checking. 208-219
  
• Narjes Berregeb, Adel Bouhoula, Michaël Rusinowitch:
  Automated Verification by Induction with Associative-Commutative Operators. 220-231
  
• Stavros Tripakis, Sergio Yovine:
  Analysis of Timed Systems Based on Time-Abstracting Bisimulation. 232-243
  
• Johan Bengtsson, W. O. David Griffioen, Kåre J. Kristoffersen, Kim Guldstrand Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi:
  Verification of an Audio Protocol with Bus Collision Using UPPAAL. 244-256
  
• Sérgio Vale Aguiar Campos, Orna Grumberg:
  Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System. 257-268
  
• Adnan Aziz, Kumud Sanwal, Vigyan Singhal, Robert K. Brayton:
  Verifying Continuous Time Markov Chains. 269-276
  
• Mark R. Greenstreet:
  Verifying Safety Properties of Differential Equations. 277-287
  
• Luca de Alfaro, Zohar Manna:
  Temporal Verification by Diagram Transformations. 288-299
  
• Seungjoon Park, David L. Dill:
  Protocol Verification by Aggregation of Distributed Transactions. 300-310
  
• E. Pascal Gribomont:
  Atomicity Refinement and Trace Reduction Theorems. 311-322
  
• Saddek Bensalem, Yassine Lakhnech, Hassen Saïdi:
  Powerful Techniques for the Automatic Generation of Invariants. 323-335
  
• Hillel Miller, Shmuel Katz:
  Saving Space by Fully Exploiting Invisible Transitions. 336-347
  
• Jean-Claude Fernandez, Claude Jard, Thierry Jéron, César Viho:
  Using On-The-Fly Verification Techniques for the Generation of test Suites. 348-359
  
• Rani Nelken, Nissim Francez:
  Automatic Translation of Natural Language System Specifications. 360-371
  
• Orna Kupferman, Moshe Y. Vardi:
  Verification of Fair Transisiton Systems. 372-382
  

Tools and Case Studies

• Gerard J. Holzmann, Doron Peled:
  The State of SPIN. 385-389
  
• David L. Dill:
  The Murphi Verification System. 390-393
  
• Rance Cleaveland, Steve Sims:
  The NCSU Concurrency Workbench. 394-397
  
• Rance Cleaveland, Philip M. Lewis, Scott A. Smolka, Oleg Sokolsky:
  The Concurrency Factory: A Development Environment for Concurrent Systems. 398-401
  
• Duncan Clarke, Hanêne Ben-Abdallah, Insup Lee, Hong-liang Xie, Oleg Sokolsky:
  XVERSA: An Integrated Graphical and Textual Toolset for the Specification and Analysis of Resource-Bound Real-Time Sytems. 402-405
  
• Pedro Merino, José M. Troya:
  EVP: Integration of FDTs for the Analysis and Verification of Communication Protocols. 406-410
  
• Sam Owre, S. Rajan, John M. Rushby, Natarajan Shankar, Mandayam K. Srivas:
  PVS: Combining Specification, Proof Checking, and Model Checking. 411-414
  
• Nikolaj Bjørner, Anca Browne, Edward Y. Chang, Michael Colón, Arjun Kapur, Zohar Manna, Henny Sipma, Tomás E. Uribe:
  STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems. 415-418
  
• Edmund M. Clarke, Kenneth L. McMillan, Sérgio Vale Aguiar Campos, Vassili Hartonas-Garmhausen:
  Symbolic Model Checking. 419-427
  
• Robert K. Brayton, Gary D. Hachtel, Alberto L. Sangiovanni-Vincentelli, Fabio Somenzi, Adnan Aziz, Szu-Tsung Cheng, Stephen A. Edwards, Sunil P. Khatri, Yuji Kukimoto, Abelardo Pardo, Shaz Qadeer, Rajeev K. Ranjan, Shaker Sarwary, Thomas R. Shiple, Gitanjali Swamy, Tiziano Villa:
  VIS: A System for Verification and Synthesis. 428-432
  
• K. D. Anon, N. Boulerice, Eduard Cerny, Francisco Corella, Michel Langevin, Xiaoyu Song, Sofiène Tahar, Ying Xu, Zijian Zhou:
  MDG Tools for the Verification of RTL Designs. 433-436
  
• Jean-Claude Fernandez, Hubert Garavel, Alain Kerbrat, Laurent Mounier, Radu Mateescu, Mihaela Sighireanu:
  CADP - A Protocol Validation and Verification Toolbox. 437-440
  
• Amar Bouali, Annie Ressouche, Valérie Roy, Robert de Simone:
  The FC2TOOLS Set. 441-445
  
• Louise E. Moser, P. M. Melliar-Smith, Y. S. Ramakrishna, G. Kutty, Laura K. Dillon:
  The Real-Time Graphical Interval Logic Toolset. 446-449
  
• Bernhard Steffen, Tiziana Margaria, Andreas Claßen, Volker Braun:
  The METAFrame'95 Environment. 450-453
  
• Frank A. Koch, Markus Ullmann, Stefan Wittmann:
  Verification Support Environment. 454-457
  
• Dominique Ambroise, Brigitte Rozoy:
  Marella: A Tool for Simulation and Verification. 458-461
  
• Georges Gonthier:
  Verifying the Safety of a Practical Concurrent Garbage Collector. 462-465
  
• Carla Capellmann, Ralph Demant, Farhad Fatahi-Vanani, Rafael Galvez-Estrada, Ulrich Nitsche, Peter Ochsenschläger:
  Verification by Behaviour Abstraction - A Case Study of Service Interaction Detection in Intelligent Telephone Networks. 466-469