15. CAV 2003: Boulder, Colorado, USA

Extending Bounded Model Checking

• Kenneth L. McMillan:
  Interpolation and SAT-Based Model Checking. 1-13
  
• Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea:
  Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A). 14-26
  

Symbolic Model Checking

• Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac, David Van Campenhout:
  Reasoning with Temporal Logic on Truncated Paths. 27-39
  
• Gianfranco Ciardo, Radu Siminiceanu:
  Structural Symbolic CTL Model Checking of Asynchronous Systems. 40-53
  
• Orna Grumberg, Tamir Heyman, Assaf Schuster:
  A Work-Efficient Distributed Algorithm for Reachability Analysis. 54-66
  

Games, Trees, and Counters

• Rajeev Alur, Salvatore La Torre, P. Madhusudan:
  Modular Strategies for Infinite Games on Recursive Graphs. 67-79
  
• Jan Obdrzálek:
  Fast Mu-Calculus Model Checking when Tree-Width Is Bounded. 80-92
  
• Gaoyan Xie, Zhe Dang, Oscar H. Ibarra, Pierluigi San Pietro:
  Dense Counter Machines and Verification Problems. 93-105
  

Tool Presentations I

• Bikram Sengupta, Rance Cleaveland:
  TRIM: A Tool for Triggered Message Sequence Charts. 106-109
  
• Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Willem Visser, Michael Wooldridge:
  Model Checking Multi-Agent Programs with CASP. 110-113
  
• Doron Drusinsky:
  Monitoring Temporal Rules Combined with Time Series. 114-117
  
• Sébastien Bardin, Alain Finkel, Jérôme Leroux, Laure Petrucci:
  FAST: Fast Acceleration of Symbolikc Transition Systems. 118-121
  
• Dirk Beyer, Claus Lewerentz, Andreas Noack:
  Rabbit: A Tool for BDD-Based Verification of Real-Time Systems. 122-125
  

Abstraction I

• Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang:
  Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates. 126-140
  
• Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook:
  A Symbolic Approach to Predicate Abstraction. 141-153
  
• Sanjit A. Seshia, Randal E. Bryant:
  Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. 154-166
  

Dense Time

• Gaurav Chakravorty, Paritosh K. Pandya:
  Digitizing Interval Duration Logic. 167-179
  
• Patricia Bouyer, Deepak D'Souza, P. Madhusudan, Antoine Petit:
  Timed Control with Partial Observability. 180-192
  
• Bernard Boigelot, Frédéric Herbreteau, Sébastien Jodogne:
  Hybrid Acceleration Using Real Vector Automata (Extended Abstract). 193-205
  

Tool Presentations (II)

• Aarti Gupta, Malay K. Ganai, Chao Wang, Zijiang Yang, Pranav Ashar:
  Abstraction and BDDs Complement SAT-Based BMC in DiVer. 206-209
  
• Marsha Chechik, Arie Gurfinkel:
  TLQSolver: A Temporal Logic Query Checker. 210-214
  
• Yifei Dong, C. R. Ramakrishnan, Scott A. Smolka:
  Evidence Explorer: A Tool for Exploring Model-Checking Proofs. 215-218
  
• Liana Bozga, Yassine Lakhnech, Michaël Périn:
  HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols. 219-222
  

Infinite State Systems

• Bernard Boigelot, Axel Legay, Pierre Wolper:
  Iterating Transducers in the Large (Extended Abstract). 223-235
  
• Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Julien d'Orso:
  Algorithmic Improvements in Regular Model Checking. 236-248
  
• Constantinos Bartzis, Tevfik Bultan:
  Efficient Image Computation in Infinite State Model Checking. 249-261
  

Abstraction II

• Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer:
  Thread-Modular Abstraction Refinement. 262-274
  
• Sharon Shoham, Orna Grumberg:
  A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement. 275-287
  
• Kedar S. Namjoshi:
  Abstraction for Branching Time Properties. 288-300
  

Applications

• Grigore Rosu, Ram Prasad Venkatesan, Jon Whittle, Laurentiu Leustean:
  Certifying Optimality of State Estimation Programs. 301-314
  
• Hardi Hungar, Oliver Niese, Bernhard Steffen:
  Domain-Specific Optimization in Automata Learning. 315-327
  
• Marcelo Glusman, Shmuel Katz:
  Model Checking Conformance with Scenario-Based Specifications. 328-340
  

Theorem Proving

• Shuvendu K. Lahiri, Randal E. Bryant:
  Deductive Verification of Advanced Out-of-Order Microprocessors. 341-353
  
• Cormac Flanagan, Rajeev Joshi, Xinming Ou, James B. Saxe:
  Theorem Proving Using Lazy Proof Explication. 355-367
  

Automata-Based Verification

• Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer, Moshe Y. Vardi:
  Enhanced Vacuity Detection in Linear Temporal Logic. 368-380
  
• Yonit Kesten, Nir Piterman, Amir Pnueli:
  Bridging the Gap between Fair Simulation and Trace Inclusion. 381-393
  
• Marc Geilen:
  An Improved On-The-Fly Tableau Construction for a Real-Time Temporal Logic. 394-406
  

Invariants

• Husam Abu-Haimed, Sergey Berezin, David L. Dill:
  Strengthening Invariants by Symbolic Consistency Testing. 407-419
  
• Michael Colón, Sriram Sankaranarayanan, Henny Sipma:
  Linear Invariant Generation Using Non-linear Constraint Solving. 420-432
  

Explicit Model Checking

• Gerd Behrmann, Kim Guldstrand Larsen, Radek Pelánek:
  To Store or Not to Store. 433-445
  
• Gordon J. Pace, Frédéric Lang, Radu Mateescu:
  Calculating-Confluence Compositionally. 446-459