12. CAV 2000: Chicago, IL, USA

Invited Talks and Tutorials

• Amir Pnueli:
  Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion. 1
  
• Catherine Meadows:
  Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis. 2
  
• João P. Marques Silva, Karem A. Sakallah:
  Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation. 3
  
• Parosh Aziz Abdulla, Bengt Jonsson:
  Invited Tutorial: Verification of Infinite-State and Parameterized Systems. 4
  

Regular Papers

• Jason Baumgartner, Anson Tripp, Adnan Aziz, Vigyan Singhal, Flemming Andersen:
  An Abstraction Algorithm for the Verification of Generalized C-Slow Designs. 5-19
  
• Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster:
  Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. 20-35
  
• Orna Kupferman, Moshe Y. Vardi:
  An Automata-Theoretic Approach to Reasoning about Infinite-State Systems. 36-52
  
• Giorgio Delzanno:
  Automatic Verification of Parameterized Cache Coherence Protocols. 53-68
  
• Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard A. Kemmerer, Jianwen Su:
  Binary Reachability Analysis of Discrete Pushdown Timed Automata. 69-84
  
• Randal E. Bryant, Miroslav N. Velev:
  Boolean Satisfiability with Transitivity Constraints. 85-98
  
• Abdelwaheb Ayari, David A. Basin:
  Bounded Model Construction for Monadic Second-Order Logics. 99-112
  
• James H. Kukula, Thomas R. Shiple:
  Building Circuits from Relations. 113-123
  
• Poul Frederick Williams, Armin Biere, Edmund M. Clarke, Anubhav Gupta:
  Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. 124-138
  
• Kedar S. Namjoshi, Richard J. Trefler:
  On the Competeness of Compositional Reasoning. 139-153
  
• Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith:
  Counterexample-Guided Abstraction Refinement. 154-169
  
• Abdelwaheb Ayari, David A. Basin, Felix Klaedtke:
  Decision Procedures for Inductive Boolean Functions Based on Alternating Automata. 170-185
  
• Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang:
  Detecting Errors Before Reaching Them. 186-201
  
• Jens Vöge, Marcin Jurdzinski:
  A Discrete Strategy Improvement Algorithm for Solving Parity Games. 202-215
  
• Gerd Behrmann, Thomas Hune, Frits W. Vaandrager:
  Distributing Timed Model Checking - How the Search Order Matters. 216-231
  
• Javier Esparza, David Hansel, Peter Rossmanith, Stefan Schwoon:
  Efficient Algorithms for Model Checking Pushdown Systems. 232-247
  
• Fabio Somenzi, Roderick Bloem:
  Efficient Büchi Automata from LTL Formulae. 248-263
  
• Scott D. Stoller, Leena Unnikrishnan, Yanhong A. Liu:
  Efficient Detection of Global Properties in Distributed Systems Using Partial-Order Methods. 264-279
  
• Rajeev Alur, Radu Grosu, Michael McDougall:
  Efficient Reachability Analysis of Hierarchical Reactive Machines. 280-295
  
• Miroslav N. Velev:
  Formal Verification of VLIW Microprocessors with Speculative Execution. 296-311
  
• Kenneth L. McMillan, Shaz Qadeer, James B. Saxe:
  Induction in Compositional Model Checking. 312-327
  
• Amir Pnueli, Elad Shahar:
  Liveness and Acceleration in Parameterized Verification. 328-343
  
• Michaël Rusinowitch, Sorin Stratulat, Francis Klay:
  Mechanical Verification of an Ideal Incremental ABR Conformance. 344-357
  
• Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen:
  Model Checking Continuous-Time Markov Chains by Transient Analysis. 358-372
  
• Franck Cassez, François Laroussinie:
  Model-Checking for Hybrid Systems by Quotienting and Constraints Solving. 373-388
  
• Ranan Fraer, Gila Kamhi, Barukh Ziv, Moshe Y. Vardi, Limor Fix:
  Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification. 389-402
  
• Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, Tayssir Touili:
  Regular Model Checking. 403-418
  
• Aurore Annichini, Eugene Asarin, Ahmed Bouajjani:
  Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. 419-434
  
• Kedar S. Namjoshi, Robert P. Kurshan:
  Syntactic Program Transformations for Automatic Abstraction. 435-449
  
• William Chan:
  Temporal-Locig Queries. 450-463
  
• Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, Antoine Petit:
  Are Timed Automata Updatable? 464-479
  
• Ofer Strichman:
  Tuning SAT Checkers for Bounded Model Checking. 480-494
  
• Parosh Aziz Abdulla, S. Purushothaman Iyer, Aletta Nylén:
  Unfoldings of Unbounded Petri Nets. 495-507
  
• John M. Rushby:
  Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification. 508-520
  
• Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas:
  Verifying Advanced Microarchitectures that Support Speculation and Exceptions. 521-537
  

Tool Papers

• Yael Abarbanel, Ilan Beer, Leonid Gluhovsky, Sharon Keidar, Yaron Wolfsthal:
  FoCs: Automatic Generation of Simulation Checkers from Formal Specifications. 538-542
  
• Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier:
  IF: A Validation Environment for Timed Asynchronous Systems. 543-547
  
• Sam Owre, Harald Rueß:
  Integrating WS1S with PVS. 548-551
  
• Elsa L. Gunter, Robert P. Kurshan, Doron Peled:
  PET: An Interactive Software Testing Tool. 552-556
  
• Christopher Colby, Peter Lee, George C. Necula:
  A Proof-Carrying Code Architecture for Java. 557-560
  
• Tom Bienmüller, Werner Damm, Hartmut Wittke:
  The STATEMATE Verification Environment - Making It Real. 561-567
  
• Ernie Cohen:
  TAPS: A First-Order Verifier for Cryptographic Protocols. 568-571
  
• Tomohiro Yoneda:
  VINAS-P: A Tool for Trace Theoretic Verification of Timed Asynchronous Circuits. 572-575
  
• C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Yifei Dong, Xiaoqun Du, Abhik Roychoudhury, V. N. Venkatakrishnan:
  XMC: A Logic-Programming-Based Verification Toolset. 576-580
  

Last update Sat May 18 18:12:32 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page