9. CAV 1997: Haifa, Israel

• F. Erich Marschner:
  Practical Challenges for Industrial Formal Verification Tools. 1-2
  
• Roger B. Hughes:
  Formal Verification of Digital Systems, from ASICs to HW/SW Codesign - a Pragmatic Approach. 3-6
  
• Arne Borälv:
  The Industrial Success of Verification Tools Based on Stålmarck's Method. 7-10
  
• Martin Rowe:
  Formal Verification - Applications & Case Studies. 11
  
• Abelardo Pardo, Gary D. Hachtel:
  Automatic Abstraction Techniques for Propositional µ-calculus Model Checking. 12-23
  
• Kenneth L. McMillan:
  A Compositional Rule for Hardware Design Refinement. 24-35
  
• Orna Kupferman, Moshe Y. Vardi:
  Model Checking Revisited. 36-47
  
• Roope Kaivola:
  Using Compositional Preorders in the Verification of Sliding Window Protocal. 48-59
  
• David Cyrluk, M. Oliver Möller, Harald Rueß:
  An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors. 60-71
  
• Susanne Graf, Hassen Saïdi:
  Construction of Abstract State Graphs with PVS. 72-83
  
• Adam L. Turk, Scott T. Probst, Gary J. Powers:
  Verification of a Chemical Process Leak Test Procedure. 84-94
  
• Gila Kamhi, Osnat Weissberg, Limor Fix:
  Automatic Datapath Extraction for Efficient Usage of HDD. 95-106
  
• Nils Klarlund:
  An n log n Algorithm for Online BDD Refinement. 107-118
  
• Christel Baier, Holger Hermanns:
  Weak Bisimulation for Fully Probabilistic Processes. 119-130
  
• Dominique Bolignano:
  Towards a Mechanization of Cryptographic Protocal Verification. 131-142
  
• Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Terrance Swift, David Scott Warren:
  Efficient Model Checking Using Tabled Resolution. 143-154
  
• Kathi Fisler:
  Containing of Regular Languages in Non-Regular Timing Diagram Languages is Decidable. 155-166
  
• Bernard Boigelot, Louis Bronne, Stéphane Rassart:
  An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems (Extended Abstract). 167-178
  
• Marius Bozga, Oded Maler, Amir Pnueli, Sergio Yovine:
  Some Progress in the Symbolic Verification of Timed Automata. 179-190
  
• Serdar Tasiran, Robert K. Brayton:
  STARI: A Case Study in Compositional and Hierarchical Timing Verification. 191-201
  
• Alessandro Cimatti, Fausto Giunchiglia, Paolo Pecchiari, Bruno Pietra, Joe Profeta, Dario Romano, Paolo Traverso, Bing Yu:
  A Provably Correct Embedded Verifier for the Certification of Safety Critical Software. 202-213
  
• Geoff Barrett, Anthony McIsaac:
  Model Checking in a Microprocessor Design Project. 214-225
  
• David Harel:
  Some Thoughts on Statecharts, 13 Years Later. 226-231
  
• Viktor Gyuris, A. Prasad Sistla:
  On-the-Fly Model Checking Under Fairness That Exploits Symmetry. 232-243
  
• Manish Pandey, Randal E. Bryant:
  Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation. 244-255
  
• Ulrich Stern, David L. Dill:
  Parallelizing the Murphi Verifier. 256-278
  
• Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh:
  Efficient Detection of Vacuity in ACTL Formulaas. 279-290
  
• Neil Immerman, Moshe Y. Vardi:
  Model Checking and Transitive-Closure Logic. 291-302
  
• Gérard Berry:
  Boolean and 2-adic Numbers Based Techniques for Verifying Synchronous Design. 303
  
• Gérard Cécé, Alain Finkel:
  Programs with Quasi-Stable Channels are Effectively Recognizable (Extended Abstract). 304-315
  
• William Chan, Richard J. Anderson, Paul Beame, David Notkin:
  Combining Constraint Solving and Symbolic Model Checking for a Class of a Systems with Non-linear Constraints. 316-327
  
• Ilkka Kokkarinen, Doron Peled, Antti Valmari:
  Relaxed Visibility Enhances Partial Order Reduction. 328-339
  
• Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani:
  Partial-Order Reduction in Symbolic State Space Exploration. 340-351
  
• Stephan Melzer, Stefan Römer:
  Deadlock Checking Using Net Unfoldings. 352-363
  
• Jun Sawada, Warren A. Hunt Jr.:
  Trace Table Based Approach for Pipeline Microprocessor Verification. 364-375
  
• Jun Yuan, Jian Shen, Jacob A. Abraham, Adnan Aziz:
  On Combining Formal and Informal Verification. 376-387
  
• Miroslav N. Velev, Randal E. Bryant, Alok Jain:
  Efficient Modeling of Memory Arrays in Symbolic Simulation. 388-399
  
• Tevfik Bultan, Richard Gerber, William Pugh:
  Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic. 400-411
  
• A. Prasad Sistla:
  Parametrized Verification of Linear Networks Using Automata as Invariants. 412-423
  
• Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar:
  Symbolic Model Checking with Rich ssertional Languages. 424-435
  

Tool Papers

• Hassen Saïdi:
  The Invariant Checker: Automated Deductive Verification of Reactive Systems. 436-439
  
• Bernd Grahlmann:
  The PEP Tool. 440-443
  
• Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik:
  TermiLog: A System for Checking Termination of Queries to Logic Programs. 444-447
  
• Peter Kelb, Tiziana Margaria, Michael Mendler, Claudia Gsottberger:
  MOSEL: A Sound and Efficient Tool for M2L(Str). 448-451
  
• Sérgio Vale Aguiar Campos, Edmund M. Clarke, Marius Minea:
  The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems. 452-455
  
• Kim Guldstrand Larsen, Paul Pettersson, Wang Yi:
  UPPAAL: Status & Developments. 456-459
  
• Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi:
  HYTECH: A Model Checker for Hybrid Systems. 460-463
  
• A. Prasad Sistla, L. Miliades, Viktor Gyuris:
  SMC: A Symmetry Based Model Checker for Verification of Liveness Properties. 464-467
  
• Armin Biere:
  µcke - Efficient µ-Calculus Model Checking. 468-471
  
• Kimmo Varpaaniemi, Keijo Heljanko, Johan Lilius:
  prod 3.2: An Advanced Tool for Efficient Reachability Analysis. 472-475
  
• Patrice Godefroid:
  VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software. 476-479
  
• Ilan Beer, Shoham Ben-David, Cindy Eisner, Daniel Geist, Leonid Gluhovsky, Tamir Heyman, Avner Landver, P. Paanah, Yoav Rodeh, G. Ronin, Yaron Wolfsthal:
  RuleBase: Model Checking at IBM. 480-483