Abstract is missing.
- Towards Scalable Modular Checking of User-Defined PropertiesThomas Ball, Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer, Julien Vanegue. 1-24 [doi]
- Tressa: Claiming the FutureAli Sezgin, Serdar Tasiran, Shaz Qadeer. 25-39 [doi]
- Automated Verification of a Small HypervisorEyad Alkassar, Mark A. Hillebrand, Wolfgang J. Paul, Elena Petrova. 40-54 [doi]
- A Rely-Guarantee Proof System for x86-TSOTom Ridge. 55-70 [doi]
- Pervasive Verification of an OS Microkernel - Inline Assembly, Memory Consumption, Concurrent DevicesEyad Alkassar, Wolfgang J. Paul, Artem Starostin, Alexandra Tsyban. 71-85 [doi]
- The L4.verified Project - Next StepsGerwin Klein. 86-96 [doi]
- An Approach of Requirements Tracing in Formal RefinementMichael Jastram, Stefan Hallerstede, Michael Leuschel, Aryldo G. Russo. 97-111 [doi]
- Dafny Meets the Verification Benchmarks ChallengeK. Rustan M. Leino, Rosemary Monahan. 112-126 [doi]
- Specifying Reusable ComponentsNadia Polikarpova, Carlo A. Furia, Bertrand Meyer. 127-141 [doi]
- Reusable Verification of a Copying CollectorMagnus O. Myreen. 142-156 [doi]
- To Goto Where No Statement Has Gone BeforeMichael Barnett, K. Rustan M. Leino. 157-168 [doi]
- The Next 700 Separation Logics - (Invited Paper)Matthew J. Parkinson. 169-182 [doi]
- Local Reasoning and Dynamic Framing for the Composite Pattern and Its ClientsStan Rosenberg, Anindya Banerjee, David A. Naumann. 183-198 [doi]
- Abstraction and Refinement for Local ReasoningThomas Dinsdale-Young, Philippa Gardner, Mark J. Wheelhouse. 199-215 [doi]