CAV 1999

43 papers

1. A Complete Finite Prefix for Process Algebra · Rom Langerak, Ed Brinksma
2. A Theory of Restrictions for Logics and Automata · Nils Klarlund
3. A Toolbox for the Analysis of Discrete Event Dynamic Systems · Peter Buchholz, Peter Kemper
4. Abstract and Model Check While You Prove · Hassen Saïdi, Natarajan Shankar
5. Alternative Approaches to Hardware Verification (abstract) · David L. Dill
6. Assume-Guarantee Refinement Between Different Time Scales · Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani
7. Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol · Béatrice Bérard, Laurent Fribourg
8. Automatic Verification of Abstract State Machines · Marc Spielmann
9. Automatic Verification of Combinatorial and Pipelined FFT · Per Bjesse
10. Deciding Equality Formulas by Small Domains Instantiations · Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel
11. Efficient Analysis of Cyclic Definitions · Kedar S. Namjoshi, Robert P. Kurshan
12. Efficient Decision Procedures for Model Checking of Linear Time Logic Properties · Roderick Bloem, Kavita Ravi, Fabio Somenzi
13. Efficient Timed Reachability Analysis Using Clock Difference Diagrams · Gerd Behrmann, Kim Guldstrand Larsen, Justin Pearson, Carsten Weise, Wang Yi
14. Elementary Microarchitecture Algebra · John Matthews, John Launchbury
15. Experience with Predicate Abstraction · Satyaki Das, David L. Dill, Seungjoon Park
16. Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions · Randal E. Bryant, Steven M. German, Miroslav N. Velev
17. Formal Methods for Conformance Testing: Theory Can Be Practical · Ed Brinksma
18. Handling Global Conditions in Parameterized System Verification · Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson
19. Improved Automata Generation for Linear Temporal Logic · Marco Daniele, Fausto Giunchiglia, Moshe Y. Vardi
20. Java Bytecode Verification by Model Checking · David A. Basin, Stefan Friedrich, Joachim Posegga, Harald Vogt
21. Latency Insensitive Protocols · Luca P. Carloni, Kenneth L. McMillan, Alberto L. Sangiovanni-Vincentelli
22. Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation · Panagiotis Manolios, Kedar S. Namjoshi, Robert Summers
23. Mechanizing Proofs of Computation Equivalence · Marcelo Glusman, Shmuel Katz
24. Model Checking Based on Sequential ATPG · Vamsi Boppana, Sreeranga P. Rajan, Koichiro Takayama, Masahiro Fujita
25. Model Checking Partial State Spaces with 3-Valued Temporal Logics · Glenn Bruns, Patrice Godefroid
26. Model Checking of Safety Properties · Orna Kupferman, Moshe Y. Vardi
27. Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists · Jason Baumgartner, Tamir Heyman, Vigyan Singhal, Adnan Aziz
28. NUSMV: A New Symbolic Model Verifier · Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri
29. On the Representation of Probabilities over Structured Domains · Marius Bozga, Oded Maler
30. Optimizing Symbolic Model Checking for Constraint-Rich Models · Bwolen Yang, Reid G. Simmons, Randal E. Bryant, David R. O'Hallaron
31. PIL/SETHEO: A Tool for the Automatic Analysis of Authentication Protocols · Johann Schumann
32. Stepwise CTL Model Checking of State/Event Systems · Jørn Lind-Nielsen, Henrik Reif Andersen
33. Stutter-Invariant Languages, omega-Automata, and Temporal Logic · Kousha Etessami
34. TIPPtool: Compositional Specification and Analysis of Markovian Performance Models · Holger Hermanns, Vassilis Mertsiotakis, Markus Siegle
35. Test Generation Derived from Model-Checking · Thierry Jéron, Pierre Morel
36. The Compositional Specification of Timed Systems - A Tutorial · Joseph Sifakis
37. The Mathematical Foundation fo Symbolic Trajectory Evaluation · Ching-Tsun Chou
38. Timed Automata · Rajeev Alur
39. Validation of Pipelined Processor Designs Using Esterel Tools: A Case Study · S. Ramesh, Purandar Bhaduri
40. Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis · Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl, Yassine Lakhnech
41. Verification of Parameterized Systems by Dynamic Induction on Diagrams · Zohar Manna, Henny Sipma
42. Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs · Armin Biere, Edmund M. Clarke, Richard Raimi, Yunshan Zhu
43. Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems · Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani