Electronic Notes in Theoretical Computer Science, Volume 145

Volume 145, January 2006

Proceedings of the 5th International Workshop on Automated Verification of Critical Systems (AVoCS 2005)

• 
  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