Volume 144, Number 1, January 2006

Proceedings of the Third International Workshop on Bounded Model Checking (BMC 2005)

• 
  Armin Biere, Ofer Strichman: Preface. 1-
• 
  Markus Jehle, Jan Johannsen, Martin Lange, Nicolas Rachinsky: Bounded Model Checking for All Regular Properties. 3-18
• 
  Anders Franzén: Using Satisfiability Modulo Theories for Inductive Verification of Lustre Programs. 19-33
• 
  Ohad Shacham, Karen Yorav: Adaptive Application of SAT Solving Techniques. 35-50
• 
  Mohammad Awedh, Fabio Somenzi: Termination Criteria for Bounded Model Checking: Extensions and Comparison. 51-66
• 
  Daniel Geist, Mark Ginzburg, Yoad Lustig, Ishai Rabinovitz, Ohad Shacham, Rachel Tzoref: Supporting SAT based BMC on Finite Path Models. 67-77
• 
  Daniel Kroening: Computing Over-Approximations with Bounded Model Checking. 79-92

Volume 144, Number 2, January 2006

Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005)

• 
  Alessandro Armando, Alessandro Cimatti: Preface. 1-2
• 
  Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, Roberto Sebastiani: Encoding RTL Constructs for MathSAT: a Preliminary Report. 3-14
• 
  Jim Grundy, Thomas F. Melham, Sava Krstic, Sean McLaughlin: Tool Building Requirements for an API to First-Order Solvers. 15-26
• 
  Shuvendu K. Lahiri, Madanlal Musuvathi: An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals. 27-41
• 
  Sean McLaughlin, Clark Barrett, Yeting Ge: Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. 43-51
• 
  Amir Pnueli, Ofer Strichman: Reduced Functional Consistency of Uninterpreted Functions. 53-65
• 
  Tjark Weber: Integrating a SAT Solver with an LCF-style Theorem Prover. 67-78
• 
  Ian Wehrman, Aaron Stump: Mining Propositional Simplification Proofs for Small Validating Clauses. 79-91

Volume 144, Number 3, February 2006

Proceedings of the Workshop on Software Model Checking (SoftMC 2005)

• 
  Byron Cook, Scott D. Stoller, Willem Visser: Preface. 1-2
• 
  Wolfgang Grieskamp, Nikolai Tillmann, Wolfram Schulte: XRT- Exploring Runtime for .NET Architecture and Applications. 3-26
• 
  Radu Grosu, Xiaowan Huang, Sumit Jain, Scott A. Smolka: Open-Source Model Checking. 27-44
• 
  Graham Hughes, Sreeranga P. Rajan, Tom Sidle, Keith Swenson: Error Detection in Concurrent Java Programs. 45-58
• 
  Morgan Magnin, Didier Lime, Olivier H. Roux: An Efficient Method for Computing Exact State Space of Petri Nets With Stopwatches. 59-77
• 
  Alessandro Armando, Massimo Benerecetti, Jacopo Mantovani: Model Checking Linear Programs with Arrays. 79-94
• 
  Robert Palmer, Steve Barrus, Yu Yang, Ganesh Gopalakrishnan, Robert M. Kirby: Gauss: A Framework for Verifying Scientific Computing Software. 95-106
• 
  Steven P. Reiss: Checking Event-Based Specifications in Java Systems. 107-132
• 
  Bernd Westphal: LSC Verification for UML Models with Unbounded Creation and Destruction. 133-145

Volume 144, Number 4, May 2006

Proceedings of the Fifth Workshop on Runtime Verification (RV 2005)

• 
  Howard Barringer, Bernd Finkbeiner, Yuri Gurevich, Henny B. Sipma: Preface. 1
• 
  Feng Chen, Marcelo d'Amorim, Grigore Rosu: Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP. 3-20
• 
  Arvind Easwaran, Sampath Kannan, Oleg Sokolsky: Steering of Discrete Event Systems: Control Theory Approach. 21-39
• 
  Tayfun Elmas, Serdar Tasiran: VyrdMC: Driving Runtime Refinement Checking with Model Checkers. 41-56
• 
  Yaniv Eytani: Concurrent Java Test Generation as a Search Problem. 57-72
• 
  Amir Pnueli, Aleksandr Zaks, Lenore D. Zuck: Monitoring Interfaces for Faults. 73-89
• 
  Oleg Sokolsky, Usa Sammapun, Insup Lee, Jesung Kim: Run-Time Checking of Dynamic Properties. 91-108
• 
  Volker Stolz, Eric Bodden: Temporal Assertions using AspectJ. 109-124
• 
  Yuhong Zhao, Simon Oberthür, Martin Kardos, Franz-Josef Rammig: Model-based Runtime Verification Framework for Self-optimizing Systems. 125-145