3. VSTTE 2010: Edinburgh, UK

Invited Talk

• Thomas Ball, Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer, Julien Vanegue:
  Towards Scalable Modular Checking of User-Defined Properties. 1-24
  

Verification Techniques

• Ali Sezgin, Serdar Tasiran, Shaz Qadeer:
  Tressa: Claiming the Future. 25-39
  
• Eyad Alkassar, Mark A. Hillebrand, Wolfgang J. Paul, Elena Petrova:
  Automated Verification of a Small Hypervisor. 40-54
  

Verification of Low-Level Code

• Tom Ridge:
  A Rely-Guarantee Proof System for x86-TSO. 55-70
  
• Eyad Alkassar, Wolfgang J. Paul, Artem Starostin, Alexandra Tsyban:
  Pervasive Verification of an OS Microkernel - Inline Assembly, Memory Consumption, Concurrent Devices. 71-85
  

Invited Talk

• Gerwin Klein:
  The L4.verified Project - Next Steps. 86-96
  

Requirements and Speci?cations

• Michael Jastram, Stefan Hallerstede, Michael Leuschel, Aryldo G. Russo:
  An Approach of Requirements Tracing in Formal Refinement. 97-111
  
• K. Rustan M. Leino, Rosemary Monahan:
  Dafny Meets the Verification Benchmarks Challenge. 112-126
  
• Nadia Polikarpova, Carlo A. Furia, Bertrand Meyer:
  Specifying Reusable Components. 127-141
  

Verification Techniques

• Magnus O. Myreen:
  Reusable Verification of a Copying Collector. 142-156
  
• Michael Barnett, K. Rustan M. Leino:
  To Goto Where No Statement Has Gone Before. 157-168
  

Invited Talk

• Matthew J. Parkinson:
  The Next 700 Separation Logics - (Invited Paper). 169-182
  

Locality in Reasoning

• Stan Rosenberg, Anindya Banerjee, David A. Naumann:
  Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients. 183-198
  
• Thomas Dinsdale-Young, Philippa Gardner, Mark J. Wheelhouse:
  Abstraction and Refinement for Local Reasoning. 199-215
  

Last update Fri May 25 08:46:35 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page