11. CAV 1999: Trento, Italy

Tutorials and Invited Papers

• David L. Dill:
  Alternative Approaches to Hardware Verification (abstract). 1
  
• Joseph Sifakis:
  The Compositional Specification of Timed Systems - A Tutorial. 2-7
  
• Rajeev Alur:
  Timed Automata. 8-22
  
• Zohar Manna, Henny Sipma:
  Verification of Parameterized Systems by Dynamic Induction on Diagrams. 25-41
  
• Ed Brinksma:
  Formal Methods for Conformance Testing: Theory Can Be Practical. 44-45
  

Processor Verification

• Armin Biere, Edmund M. Clarke, Richard Raimi, Yunshan Zhu:
  Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs. 60-71
  
• Jason Baumgartner, Tamir Heyman, Vigyan Singhal, Adnan Aziz:
  Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists. 72-83
  
• S. Ramesh, Purandar Bhaduri:
  Validation of Pipelined Processor Designs Using Esterel Tools: A Case Study. 84-95
  

Protocol Verification and Testing

• Béatrice Bérard, Laurent Fribourg:
  Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol. 96-107
  
• Thierry Jéron, Pierre Morel:
  Test Generation Derived from Model-Checking. 108-121
  
• Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli:
  Latency Insensitive Protocols. 123-133
  

Infinite State Space

• Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson:
  Handling Global Conditions in Parameterized System Verification. 134-145
  
• Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl, Yassine Lakhnech:
  Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. 146-159
  
• Satyaki Das, David L. Dill, Seungjoon Park:
  Experience with Predicate Abstraction. 160-171
  

Theory of Verification

• Orna Kupferman, Moshe Y. Vardi:
  Model Checking of Safety Properties. 172-183
  
• Rom Langerak, Ed Brinksma:
  A Complete Finite Prefix for Process Algebra. 184-195
  
• Ching-Tsun Chou:
  The Mathematical Foundation fo Symbolic Trajectory Evaluation. 196-207
  
• Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani:
  Assume-Guarantee Refinement Between Different Time Scales. 208-221
  

Linear Temporal Logic

• Roderick Bloem, Kavita Ravi, Fabio Somenzi:
  Efficient Decision Procedures for Model Checking of Linear Time Logic Properties. 222-235
  
• Kousha Etessami:
  Stutter-Invariant Languages, omega-Automata, and Temporal Logic. 236-248
  
• Marco Daniele, Fausto Giunchiglia, Moshe Y. Vardi:
  Improved Automata Generation for Linear Temporal Logic. 249-260
  

Modeling of Systems

• Marius Bozga, Oded Maler:
  On the Representation of Probabilities over Structured Domains. 261-273
  
• Glenn Bruns, Patrice Godefroid:
  Model Checking Partial State Spaces with 3-Valued Temporal Logics. 274-287
  
• John Matthews, John Launchbury:
  Elementary Microarchitecture Algebra. 288-300
  
• Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani:
  Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems. 301-315
  

Symbolic Model-Checking

• Jørn Lind-Nielsen, Henrik Reif Andersen:
  Stepwise CTL Model Checking of State/Event Systems. 316-327
  
• Bwolen Yang, Reid G. Simmons, Randal E. Bryant, David R. O'Hallaron:
  Optimizing Symbolic Model Checking for Constraint-Rich Models. 328-340
  
• Gerd Behrmann, Kim Guldstrand Larsen, Justin Pearson, Carsten Weise, Wang Yi:
  Efficient Timed Reachability Analysis Using Clock Difference Diagrams. 341-353
  

Theorem Proving

• Marcelo Glusman, Shmuel Katz:
  Mechanizing Proofs of Computation Equivalence. 354-367
  
• Panagiotis Manolios, Kedar S. Namjoshi, Robert Summers:
  Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation. 369-379
  
• Per Bjesse:
  Automatic Verification of Combinatorial and Pipelined FFT. 380-393
  

Automata-Theoretic Methods

• Kedar S. Namjoshi, Robert P. Kurshan:
  Efficient Analysis of Cyclic Definitions. 394-405
  
• Nils Klarlund:
  A Theory of Restrictions for Logics and Automata. 406-417
  
• Vamsi Boppana, Sreeranga P. Rajan, Koichiro Takayama, Masahiro Fujita:
  Model Checking Based on Sequential ATPG. 418-430
  
• Marc Spielmann:
  Automatic Verification of Abstract State Machines. 431-442
  

Abstraction

• Hassen Saïdi, Natarajan Shankar:
  Abstract and Model Check While You Prove. 443-454
  
• Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel:
  Deciding Equality Formulas by Small Domains Instantiations. 455-469
  
• Randal E. Bryant, Steven M. German, Miroslav N. Velev:
  Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. 470-482
  

Tool Presentations

• Peter Buchholz, Peter Kemper:
  A Toolbox for the Analysis of Discrete Event Dynamic Systems. 483-486
  
• Holger Hermanns, Vassilis Mertsiotakis, Markus Siegle:
  TIPPtool: Compositional Specification and Analysis of Markovian Performance Models. 487-490
  
• David A. Basin, Stefan Friedrich, Joachim Posegga, Harald Vogt:
  Java Bytecode Verification by Model Checking. 491-494
  
• Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri:
  NUSMV: A New Symbolic Model Verifier. 495-499
  
• Johann Schumann:
  PIL/SETHEO: A Tool for the Automatic Analysis of Authentication Protocols. 500-504