16. CAV 2004: Boston, MA, USA

• John O'Leary, Marly Roncken:
  Rob Tristan Gerth: 1956?2003. 1-14
  
• Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm:
  Static Program Analysis via 3-Valued Logic. 15-30
  
• Sandip Ray, Warren A. Hunt Jr.:
  Deductive Verification of Pipelined Machines Using First-Order Quantification. 31-43
  
• Hui Gao, Wim H. Hesselink:
  A Formal Reduction for Lock-Free Parallel Algorithms. 44-56
  
• Kedar S. Namjoshi:
  An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking. 57-69
  
• Ashish Tiwari:
  Termination of Linear Programs. 70-82
  
• Martin Lange:
  Symbolic Model Checking of Non-regular Properties. 83-95
  
• Mohammad Awedh, Fabio Somenzi:
  Proving More Properties with Bounded Model Checking. 96-108
  
• Claus Schröter, Victor Khomenko:
  Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings. 109-121
  
• Jacob Chang, Sergey Berezin, David L. Dill:
  Using Interface Refinement to Integrate Formal Verification into the Design Cycle. 122-134
  
• Shuvendu K. Lahiri, Randal E. Bryant:
  Indexed Predicate Discovery for Unbounded System Verification. 135-147
  
• Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli:
  Range Allocation for Separation Logic. 148-161
  
• Leonardo Mendonça de Moura, Harald Rueß:
  An Experimental Evaluation of Ground Decision Procedures. 162-174
  
• Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
  DPLL( T): Fast Decision Procedures. 175-188
  
• Doron Bustan, Sasha Rubin, Moshe Y. Vardi:
  Verifying omega-Regular Properties of Markov Chains. 189-201
  
• Koushik Sen, Mahesh Viswanathan, Gul Agha:
  Statistical Model Checking of Black-Box Probabilistic Systems. 202-215
  
• Jin Yang, Carl-Johan H. Seger:
  Compositional Specification and Model Checking in GSTE. 216-228
  
• Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi:
  GSTE Is Partitioned Model Checking. 229-241
  
• Cédric Fournet, C. A. R. Hoare, Sriram K. Rajamani, Jakob Rehof:
  Stuck-Free Conformance. 242-254
  
• Amit Goel, Randal E. Bryant:
  Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors. 255-267
  
• Jie-Hong Roland Jiang, Robert K. Brayton:
  Functional Dependency for Verification Reduction. 268-280
  
• Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh:
  Verification via Structure Simulation. 281-294
  
• Farn Wang:
  Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures. 295-307
  
• Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman:
  Abstraction-Based Satisfiability Solving of Presburger Arithmetic. 308-320
  
• Constantinos Bartzis, Tevfik Bultan:
  Widening Arithmetic Automata. 321-333
  
• Alexander Metzner:
  Why Model Checking Can Improve WCET Analysis. 334-347
  
• Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Julien d'Orso, Mayank Saksena:
  Regular Model Checking for LTL(MSO). 348-360
  
• Alain Finkel, Jérôme Leroux:
  Image Computation in Infinite State Model Checking. 361-371
  
• Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar:
  Abstract Regular Model Checking. 372-386
  
• Nir Piterman, Moshe Y. Vardi:
  Global Model-Checking of Infinite-State Systems. 387-400
  
• Ganesh Gopalakrishnan, Yue Yang, Hemanthkumar Sivaraj:
  QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings. 401-413
  
• Tamarah Arons:
  Verification of an Advanced mips-Type Out-of-Order Execution Algorithm. 414-426
  
• Jesse D. Bingham, Anne Condon, Alan J. Hu, Shaz Qadeer, Zhichuan Zhang:
  Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values. 427-439
  
• Malay K. Ganai, Aarti Gupta, Pranav Ashar:
  Efficient Modeling of Embedded Memories in Bounded Model Checking. 440-452
  
• Alex Groce, Daniel Kroening, Flavio Lerda:
  Understanding Counterexamples with explain. 453-456
  
• Thomas Ball, Byron Cook, Shuvendu K. Lahiri, Lintao Zhang:
  Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. 457-461
  
• Cyrille Artho, Viktor Schuppan, Armin Biere, Pascal Eugster, Marcel Baur, Boris Zweimüller:
  JNuke: Efficient Dynamic Analysis for Java. 462-465
  
• Paula J. Pingree, Erich Mikk:
  The HiVy Tool Set. 466-469
  
• Víctor A. Braberman, Diego Garbervetsky, Alfredo Olivero:
  ObsSlice: A Timed Automata Slicer Based on Observers. 470-474
  
• Shuvendu K. Lahiri, Sanjit A. Seshia:
  The UCLID Decision Procedure. 475-478
  
• Peter Gammie, Ron van der Meyden:
  MCK: Model Checking the Logic of Knowledge. 479-483
  
• Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof, Yichen Xie:
  Zing: A Model Checker for Concurrent Software. 484-487
  
• Alain Griffault, Aymeric Vincent:
  The Mec 5 Model-Checker. 488-491
  
• Li Tan:
  PlayGame: A Platform for Diagnostic Games. 492-495
  
• Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari:
  SAL 2. 496-500
  
• Azadeh Farzan, Feng Chen, José Meseguer, Grigore Rosu:
  Formal Analysis of Java Programs in JavaFAN. 501-505
  
• S. Ramesh, Sampada Sonalkar, Vijay D'Silva, Naveen Chandra, B. Vijayalakshmi:
  A Toolset for Modelling and Verification of GALS Systems. 506-509
  
• Xiang Fu, Tevfik Bultan, Jianwen Su:
  WSAT: A Tool for Formal Analysis of Web Services. 510-514
  
• Clark W. Barrett, Sergey Berezin:
  CVC Lite: A New Implementation of the Cooperating Validity Checker Category B. 515-518
  
• HoonSang Jin, Mohammad Awedh, Fabio Somenzi:
  CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking. 519-522
  
• Warren A. Hunt Jr.:
  Mechanical Mathematical Methods for Microprocessor Verification. 523-533