default search action
12th CAV 2000: Chicago, IL, USA
- E. Allen Emerson, A. Prasad Sistla:
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
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 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
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
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
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 A. 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-01-02 18:24 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: