10. CAV 1998: Vancouver, BC, Canada

Invited Papers

• Nicolas Halbwachs:
  Synchronous Programming of Reactive Systems. 1-16
  
• Doron Peled:
  Ten Years of Partial Order Reduction. 17-28
  
• J. Strother Moore:
  An ACL2 Proof of Write Invalidate Cache Coherence. 29-38
  
• David Hardin, Matthew Wilding, David A. Greve:
  Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle. 39-44
  
• Albert John Camilleri:
  A Role for Theorem Proving in Multi-Processor Design. 45-48
  
• John Hoffman, Charlie Payne:
  A Formal Method Experience at Secure Computing Corporation. 49-56
  
• Jorge Cuéllar:
  Formal Methods in an Industrial Environment. 57-60
  
• Gerard J. Holzmann:
  On Checking Model Checkers. 61-70
  
• John C. Mitchell:
  Finite-State Analysis of Security Protocols. 71-76
  
• Dominique Bolignano:
  Integrating Proof-Based and Model-Checking Techniques for the Formal Verification of Cryptographic Protocols. 77-87
  
• Pierre Wolper, Bernard Boigelot:
  Verifying Systems with Infinite but Regular State Spaces. 88-97
  

Regular Papers

• Jens U. Skakkebæk, Robert B. Jones, David L. Dill:
  Formal Verification of Out-of-Order Execution Using Incremental Flushing. 98-109
  
• Kenneth L. McMillan:
  Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. 110-121
  
• Ravi Hosabettu, Mandayam K. Srivas, Ganesh Gopalakrishnan:
  Decomposing the Proof of Correctness of pipelined Microprocessors. 122-134
  
• Jun Sawada, Warren A. Hunt Jr.:
  Processor Verification with Precise Exeptions and Speculative Execution. 135-146
  
• Edmund M. Clarke, E. Allen Emerson, Somesh Jha, A. Prasad Sistla:
  Symmetry Reductions inModel Checking. 147-158
  
• Gurmeet Singh Manku, Ramin Hojati, Robert K. Brayton:
  Structural Symmetry and Model Checking. 159-171
  
• Ulrich Stern, David L. Dill:
  Using Magnatic Disk Instead of Main Memory in the Murphi Verifier. 172-183
  
• Ilan Beer, Shoham Ben-David, Avner Landver:
  On-the-Fly Model Checking of RCTL Formulas. 184-194
  
• Thomas A. Henzinger, Orna Kupferman, Shaz Qadeer:
  From Pre-historic to Post-modern Symbolic Model Checking. 195-206
  
• Frank Wallner:
  Model Checking LTL Using Net Unforldings. 207-218
  
• Ying Xu, Eduard Cerny, Xiaoyu Song, Francisco Corella, Otmane Aït Mohamed:
  Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs. 219-231
  
• Jayram S. Thathachar:
  On the Limitations of Ordered Representations of Functions. 232-243
  
• Anuj Goel, Khurram Sajid, Hai Zhou, Adnan Aziz, Vigyan Singhal:
  BDD Based Procedures for a Theory of Equality with Uninterpreted Functions. 244-255
  
• Adrian J. Isles, Ramin Hojati, Robert K. Brayton:
  Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory. 256-267
  
• Hubert Comon, Yan Jurski:
  Multiple Counters Automata, Safety Analysis and Presburger Arithmetic. 268-279
  
• Thomas R. Shiple, James H. Kukula, Rajeev K. Ranjan:
  A Comparison of Presburger Engines for EFSM Reachability. 280-292
  
• Michael Colón, Tomás E. Uribe:
  Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures. 293-304
  
• Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson:
  On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels. 305-318
  
• Saddek Bensalem, Yassine Lakhnech, Sam Owre:
  Computing Abstractions of Infinite State Systems Compositionally and Automatically. 319-331
  
• W. O. David Griffioen, Frits W. Vaandrager:
  Normed Simulations. 332-344
  
• Raphaël Couturier, Dominique Méry:
  An Experiment in Parallelizing an Application Using Formal Methods. 345-356
  
• Scott D. Stoller, Yanhong A. Liu:
  Efficient Symbolic Detection of Global Properties in Distributed Systems. 357-368
  
• Matthew Wilding:
  A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy. 369-378
  
• Parosh Aziz Abdulla, Bengt Jonsson, Mats Kindahl, Doron Peled:
  A General Approach to Partial Order Reductions in Symbolic Verification (Extended Abstract). 379-390
  
• Felice Balarin:
  Correctness of the Concurrent Approach to Symbolic Verification of Interleaved Models. 391-402
  
• Wendy Belluomini, Chris J. Myers:
  Verification of Timed Systems Using POSETs. 403-415
  
• Giampaolo Bella, Lawrence C. Paulson:
  Mechanising BAN Kerberos by the Inductive Method. 416-427
  
• Amy P. Felty, Douglas J. Howe, Frank A. Stomp:
  Protocol Verification in Nuprl. 428-439
  
• Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani:
  You Assume, We Guarantee: Methodology and Case Studies. 440-451
  
• E. Allen Emerson, Kedar S. Namjoshi:
  Verification of Parameterized Bus Arbitration Protocol. 452-463
  
• Ratan Nalumasu, Rajnish Ghughal, Abdelillah Mokkedem, Ganesh Gopalakrishnan:
  The 'Test Model-Checking' Approach to the Verification of Formal Memory Models of Multiprocessors. 464-476
  
• Matt Kaufmann, Andrew Martin, Carl Pixley:
  Design Constraints in Symbolic Model Checking. 477-487
  
• Yirng-An Chen, Randal E. Bryant:
  Verification of Floating-Point Adders. 488-499
  

Tool Papers

• Amar Bouali:
  XEVE, an ESTEREL Verification Environment. 500-504
  
• Saddek Bensalem, Yassine Lakhnech, Sam Owre:
  InVeST: A Tool for the Verification of Invariants. 505-510
  
• Gian Luigi Ferrari, Stefania Gnesi, Ugo Montanari, Marco Pistore, Gioia Ristori:
  Verifying Mobile Processes in the HAL Environment. 511-515
  
• Jacob Elgaard, Nils Klarlund, Anders Møller:
  MONA 1.x: New Techniques for WS1S and WS2S. 516-520
  
• Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran:
  MOCHA: Modularity in Model Checking. 521-525
  
• Constance L. Heitmeyer, James Kirby, Bruce G. Labaw, Ramesh Bharadwaj:
  SCR*: A Toolset for Specifying and Analyzing Software Requirements. 526-531
  
• Doron Peled:
  A Toolset for Message Sequence Charts. 532-536
  
• Udo Brockmeyer, Gunnar Wittich:
  Real-Time Verification of Statemate Designs. 537-541
  
• Conrado Daws:
  Optikron: A Tool Suite for Enhancing Model-Checking of Real-Time Systems. 542-545
  
• Marius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis, Sergio Yovine:
  Kronos: A Model-Checking Tool for Real-Time Systems. 546-550