Electronic Notes in Theoretical Computer Science, Volume 144

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 W. 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 D. 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