Verified Software: Theories, Tools, and Experiments : 7th International Conference, VSTTE 2015, San Francisco, CA, USA, July 18-19, 2015. Revised Selected Papers

This volume constitutes the thoroughly refereed post-conference proceedings of the 7th International Conference on Verified Software: Theories, Tools and Experiments, VSTTE 2015, held in July 2015 in San Francisco, CA, USA. The 12 revised full papers presented were carefully revised and selected from 25 submissions. The goal of this conference is to advance the state of the art in the science and technology of software verification, through the interaction of theory development, tool evolution, and experimental validation and large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge. Front Matter....Pages I-IX A Proof-Sensitive Approach for Small Propositional Interpolants....Pages 1-18 Recursive Games for Compositional Program Synthesis....Pages 19-39 Testing the IPC Protocol for a Real-Time Operating System....Pages 40-60 Pseudo-Random Number Generator Verification: A Case Study....Pages 61-72 Inside a Verified Flash File System: Transactions and Garbage Collection....Pages 73-93 How to Avoid Proving the Absence of Integer Overflows....Pages 94-109 Machine-Checked Proofs for Realizability Checking Algorithms....Pages 110-123 Dynamic Frames Based Verification Method for Concurrent Java Programs....Pages 124-141 A Simpler Reduction Theorem for x86-TSO....Pages 142-164 Moving Around: Lipton’s Reduction for TSO....Pages 165-182 Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover....Pages 183-201 AUSPICE: Automatic Safety Property Verification for Unmodified Executables....Pages 202-222 Back Matter....Pages 223-223