CAV 2003

41 papers

1. A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement · Sharon Shoham, Orna Grumberg
2. A Symbolic Approach to Predicate Abstraction · Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook
3. A Work-Efficient Distributed Algorithm for Reachability Analysis · Orna Grumberg, Tamir Heyman, Assaf Schuster
4. Abstraction and BDDs Complement SAT-Based BMC in DiVer · Aarti Gupta, Malay K. Ganai, Chao Wang, Zijiang Yang, Pranav Ashar
5. Abstraction for Branching Time Properties · Kedar S. Namjoshi
6. Algorithmic Improvements in Regular Model Checking · Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Julien d'Orso
7. An Improved On-The-Fly Tableau Construction for a Real-Time Temporal Logic · Marc Geilen
8. Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A) · Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea
9. Bridging the Gap between Fair Simulation and Trace Inclusion · Yonit Kesten, Nir Piterman, Amir Pnueli
10. Calculating-Confluence Compositionally · Gordon J. Pace, Frédéric Lang, Radu Mateescu
11. Certifying Optimality of State Estimation Programs · Grigore Rosu, Ram Prasad Venkatesan, Jon Whittle, Laurentiu Leustean
12. Deductive Verification of Advanced Out-of-Order Microprocessors · Shuvendu K. Lahiri, Randal E. Bryant
13. Dense Counter Machines and Verification Problems · Gaoyan Xie, Zhe Dang, Oscar H. Ibarra, Pierluigi San Pietro
14. Digitizing Interval Duration Logic · Gaurav Chakravorty, Paritosh K. Pandya
15. Domain-Specific Optimization in Automata Learning · Hardi Hungar, Oliver Niese, Bernhard Steffen
16. Efficient Image Computation in Infinite State Model Checking · Constantinos Bartzis, Tevfik Bultan
17. Enhanced Vacuity Detection in Linear Temporal Logic · Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer + 1 more
18. Evidence Explorer: A Tool for Exploring Model-Checking Proofs · Yifei Dong, C. R. Ramakrishnan, Scott A. Smolka
19. FAST: Fast Acceleration of Symbolikc Transition Systems · Sébastien Bardin, Alain Finkel, Jérôme Leroux, Laure Petrucci
20. Fast Mu-Calculus Model Checking when Tree-Width Is Bounded · Jan Obdrzálek
21. HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols · Liana Bozga, Yassine Lakhnech, Michaël Périn
22. Hybrid Acceleration Using Real Vector Automata (Extended Abstract) · Bernard Boigelot, Frédéric Herbreteau, Sébastien Jodogne
23. Interpolation and SAT-Based Model Checking · Kenneth L. McMillan
24. Iterating Transducers in the Large (Extended Abstract) · Bernard Boigelot, Axel Legay, Pierre Wolper
25. Linear Invariant Generation Using Non-linear Constraint Solving · Michael Colón, Sriram Sankaranarayanan, Henny Sipma
26. Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates · Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang
27. Model Checking Conformance with Scenario-Based Specifications · Marcelo Glusman, Shmuel Katz
28. Model Checking Multi-Agent Programs with CASP · Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Willem Visser, Michael J. Wooldridge
29. Modular Strategies for Infinite Games on Recursive Graphs · Rajeev Alur, Salvatore La Torre, P. Madhusudan
30. Monitoring Temporal Rules Combined with Time Series · Doron Drusinsky
31. Rabbit: A Tool for BDD-Based Verification of Real-Time Systems · Dirk Beyer, Claus Lewerentz, Andreas Noack
32. Reasoning with Temporal Logic on Truncated Paths · Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac, David Van Campenhout
33. Strengthening Invariants by Symbolic Consistency Testing · Husam Abu-Haimed, Sergey Berezin, David L. Dill
34. Structural Symbolic CTL Model Checking of Asynchronous Systems · Gianfranco Ciardo, Radu Siminiceanu
35. TLQSolver: A Temporal Logic Query Checker · Marsha Chechik, Arie Gurfinkel
36. TRIM: A Tool for Triggered Message Sequence Charts · Bikram Sengupta, Rance Cleaveland
37. Theorem Proving Using Lazy Proof Explication · Cormac Flanagan, Rajeev Joshi, Xinming Ou, James B. Saxe
38. Thread-Modular Abstraction Refinement · Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer
39. Timed Control with Partial Observability · Patricia Bouyer, Deepak D'Souza, P. Madhusudan, Antoine Petit
40. To Store or Not to Store · Gerd Behrmann, Kim Guldstrand Larsen, Radek Pelánek
41. Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods · Sanjit A. Seshia, Randal E. Bryant