Electronic Notes in Theoretical Computer Science, Volume 254

Volume 254, October 2009

• Ralf Huuck, Gerwin Klein, Bastian Schlich:
  Preface. 1-3
  
• Matko Botincan, Matthew Parkinson, Wolfram Schulte:
  Separation Logic Verification of C Programs with an SMT Solver. 5-23
  
• Andrew Boyton:
  A Verified Shared Capability Model. 25-44
  
• Jörg Brauer, Bastian Schlich, Stefan Kowalewski:
  Parallel and Distributed Invariant Checking of Microcontroller Software. 45-63
  
• Jörg Brauer, Ralf Huuck, Bastian Schlich:
  Interprocedural Pointer Analysis in Goanna. 65-83
  
• Ernie Cohen, Michal Moskal, Stephan Tobies, Wolfram Schulte:
  A Precise Yet Efficient Memory Model For C. 85-103
  
• Yuusuke Hashimoto, Shin Nakajima:
  Modular Checking with Model Checking. 105-122
  
• Mark A. Hillebrand, Dirk Leinenbach:
  Formal Verification of a Reader-Writer Lock Implementation in C. 123-141
  
• Vitor Lima, Chamseddine Talhi, Djedjiga Mouheb, Mourad Debbabi, Lingyu Wang, Makan Pourzandi:
  Formal Verification and Validation of UML 2.0 Sequence Diagrams using Source and Destination of Messages. 143-160
  
• Norbert Schirmer, Makarius Wenzel:
  State Spaces - The Locale Way. 161-179
  
• Michael Vistein, Frank Ortmeier, Wolfgang Reif, Ralf Huuck, Ansgar Fehnker:
  An Abstract Specification Language for Static Program Analysis. 181-197