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