CAV 2000

48 papers

1. A Discrete Strategy Improvement Algorithm for Solving Parity Games · Jens Vöge, Marcin Jurdzinski
2. A Proof-Carrying Code Architecture for Java · Christopher Colby, Peter Lee, George C. Necula
3. Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits · Tamir Heyman, Daniel Geist, Orna Grumberg, Assaf Schuster
4. An Abstraction Algorithm for the Verification of Generalized C-Slow Designs · Jason Baumgartner, Anson Tripp, Adnan Aziz, Vigyan Singhal, Flemming Andersen
5. An Automata-Theoretic Approach to Reasoning about Infinite-State Systems · Orna Kupferman, Moshe Y. Vardi
6. Are Timed Automata Updatable? · Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, Antoine Petit
7. Automatic Verification of Parameterized Cache Coherence Protocols · Giorgio Delzanno
8. Binary Reachability Analysis of Discrete Pushdown Timed Automata · Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard A. Kemmerer, Jianwen Su
9. Boolean Satisfiability with Transitivity Constraints · Randal E. Bryant, Miroslav N. Velev
10. Bounded Model Construction for Monadic Second-Order Logics · Abdelwaheb Ayari, David A. Basin
11. Building Circuits from Relations · James H. Kukula, Thomas R. Shiple
12. Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking · Poul Frederick Williams, Armin Biere, Edmund M. Clarke, Anubhav Gupta
13. Counterexample-Guided Abstraction Refinement · Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith
14. Decision Procedures for Inductive Boolean Functions Based on Alternating Automata · Abdelwaheb Ayari, David A. Basin, Felix Klaedtke
15. Detecting Errors Before Reaching Them · Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang
16. Distributing Timed Model Checking - How the Search Order Matters · Gerd Behrmann, Thomas Hune, Frits W. Vaandrager
17. Efficient Algorithms for Model Checking Pushdown Systems · Javier Esparza, David Hansel, Peter Rossmanith, Stefan Schwoon
18. Efficient Büchi Automata from LTL Formulae · Fabio Somenzi, Roderick Bloem
19. Efficient Detection of Global Properties in Distributed Systems Using Partial-Order Methods · Scott D. Stoller, Leena Unnikrishnan, Yanhong A. Liu
20. Efficient Reachability Analysis of Hierarchical Reactive Machines · Rajeev Alur, Radu Grosu, Michael McDougall
21. FoCs: Automatic Generation of Simulation Checkers from Formal Specifications · Yael Abarbanel, Ilan Beer, Leonid Gluhovsky, Sharon Keidar, Yaron Wolfsthal
22. Formal Verification of VLIW Microprocessors with Speculative Execution · Miroslav N. Velev
23. IF: A Validation Environment for Timed Asynchronous Systems · Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier
24. Induction in Compositional Model Checking · Kenneth L. McMillan, Shaz Qadeer, James B. Saxe
25. Integrating WS1S with PVS · Sam Owre, Harald Rueß
26. Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis · Catherine Meadows
27. Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation · João Marques-Silva, Karem A. Sakallah
28. Invited Tutorial: Verification of Infinite-State and Parameterized Systems · Parosh Aziz Abdulla, Bengt Jonsson
29. Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion · Amir Pnueli
30. Liveness and Acceleration in Parameterized Verification · Amir Pnueli, Elad Shahar
31. Mechanical Verification of an Ideal Incremental ABR Conformance · Michaël Rusinowitch, Sorin Stratulat, Francis Klay
32. Model Checking Continuous-Time Markov Chains by Transient Analysis · Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen
33. Model-Checking for Hybrid Systems by Quotienting and Constraints Solving · Franck Cassez, François Laroussinie
34. On the Competeness of Compositional Reasoning · Kedar S. Namjoshi, Richard J. Trefler
35. PET: An Interactive Software Testing Tool · Elsa L. Gunter, Robert P. Kurshan, Doron A. Peled
36. Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification · Ranan Fraer, Gila Kamhi, Barukh Ziv, Moshe Y. Vardi, Limor Fix
37. Regular Model Checking · Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, Tayssir Touili
38. Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems · Aurore Annichini, Eugene Asarin, Ahmed Bouajjani
39. Syntactic Program Transformations for Automatic Abstraction · Kedar S. Namjoshi, Robert P. Kurshan
40. TAPS: A First-Order Verifier for Cryptographic Protocols · Ernie Cohen
41. Temporal-Locig Queries · William Chan
42. The STATEMATE Verification Environment - Making It Real · Tom Bienmüller, Werner Damm, Hartmut Wittke
43. Tuning SAT Checkers for Bounded Model Checking · Ofer Strichman
44. Unfoldings of Unbounded Petri Nets · Parosh Aziz Abdulla, S. Purushothaman Iyer, Aletta Nylén
45. VINAS-P: A Tool for Trace Theoretic Verification of Timed Asynchronous Circuits · Tomohiro Yoneda
46. Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification · John M. Rushby
47. Verifying Advanced Microarchitectures that Support Speculation and Exceptions · Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas
48. XMC: A Logic-Programming-Based Verification Toolset · C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Yifei Dong, Xiaoqun Du, Abhik Roychoudhury + 1 more