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. Springer 2000 Lecture Notes in Computer Science ISBN 3-540-67770-4
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
- Abdelwaheb Ayari, David A. Basin: Bounded Model Construction for Monadic Second-Order Logics. 99-112
- Poul Frederick Williams, Armin Biere, Edmund M. Clarke, Anubhav Gupta: Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. 124-138
- 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
- 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
- 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
- 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
- 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
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-17T203403 by the dblp team