Electronic Notes in Theoretical Computer Science, Volume 217

Volume 217, July 2008

• Ralf Huuck, Gerwin Klein, Bastian Schlich:
  Preface. 1-3
  
• Pär Emanuelsson, Ulf Nilsson:
  A Comparative Study of Industrial Static Analysis Tools. 5-21
  
• Dirk Leinenbach, Elena Petrova:
  Pervasive Compiler Verification - From Verified Programs to Verified Systems. 23-40
  
• Harvey Tuch:
  Structured Types and Separation Logic. 41-59
  
• Rafal Kolanski:
  A Logic for Virtual Memory. 61-77
  
• Hendrik Tews, Tjark Weber, Marcus Völp:
  A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code. 79-96
  
• Christof Efkemann, Tobias Hartmann:
  Specification of Conditions for Error Diagnostics. 97-112
  
• Helge Löding, Jan Peleska:
  Symbolic and Abstract Interpretation for C/C++ Programs. 113-131
  
• Gerlind Herberich, Bastian Schlich, Carsten Weise, Thomas Noll:
  Proving Correctness of an Efficient Abstraction for Interrupt Handling. 133-150
  
• Thomas In der Rieden, Alexandra Tsyban:
  CVM - A Verified Framework for Microkernel Programmers. 151-168
  
• Artem Starostin, Alexandra Tsyban:
  Correct Microkernel Primitives. 169-185
  
• Paul T. Graunke:
  Verified Safety and Information Flow of a Block Device. 187-202
  
• Kirsten Berkenkötter:
  Reliable UML Models and Profiles. 203-220
  
• Tony Cant, Ben Long, Jim McCarthy, Brendan P. Mahony, Kylie Williams:
  The HiVe Writer. 221-234