Electronic Notes in Theoretical Computer Science, Volume 145

Volume 145, January 2006

• Ranko Lazic, Rajagopal Nagarajan:
  Preface. 1-2
  
• Cliff B. Jones:
  Reasoning About Partial Functions in the Formal Development of Programs. 3-25
  
• Mike Gordon, Juliano Iyoda, Scott Owens, Konrad Slind:
  Automatic Formal Synthesis of Hardware from Higher Order Logic. 27-43
  
• Hasan Amjad:
  Verification of AMBA Using a Combination of Model Checking and Theorem Proving. 45-61
  
• Damián Barsotti, Leonor Prensa Nieto, Alwen Fernanto Tiu:
  Verification of Clock Synchronization Algorithms: Experiments on a Combination of Deductive Tools. 63-78
  
• Dimitar P. Guelev, Mark Dermot Ryan, Pierre-Yves Schobbens:
  Synthesising Features by Games. 79-93
  
• Tobe Toben, Bernd Westphal:
  Concurrent LSC Verification: On Decomposition Properties of Partially Ordered Symbolic Automata. 95-111
  
• Milan Ceska, Pavel Erlebach, Tomás Vojnar:
  Pattern-Based Verification of Programs with Extended Linear Linked Data Structures. 113-130
  
• Nathaniel Charlton:
  Verification of Java Programs with Interacting Analysis Plugins. 131-150
  
• Eun-Young Kang, Stephan Merz:
  Predicate Diagrams for the Verification of Real-Time Systems. 151-165
  
• Hosung Song, Kevin J. Compton, William C. Rounds:
  SPHIN: A model checker for reconfigurable hybrid systems based on SPIN. 167-183
  
• Joy N. Reed, A. W. Roscoe, Jane Sinclair:
  Machine-Verifiable Responsiveness. 185-200
  
• Neil Evans, Helen Treharne:
  Linking Semantic Models to Support CSP || B Consistency Checking. 201-217