12. CAV 2000: Chicago, IL, USA

E. Allen Emerson, A. Prasad Sistla (Eds.): Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings. Lecture Notes in Computer Science 1855 Springer 2000, ISBN 3-540-67770-4 BibTeX

@proceedings{DBLP:conf/cav/2000,
  editor    = {E. Allen Emerson and
               A. Prasad Sistla},
  title     = {Computer Aided Verification, 12th International Conference, CAV
               2000, Chicago, IL, USA, July 15-19, 2000, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1855},
  year      = {2000},
  isbn      = {3-540-67770-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Invited Talks and Tutorials

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

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

Tool Papers

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