Verified software : theories, tools, experiments : 5th International Conference, VSTTE 2013, Menlo Park, CA, USA, May 17-19, 2013 : revised selected papers

This volume constitutes the thoroughly refereed post-conference proceedings of the 5th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2013, held in Menlo Park, CA, USA, in May 2013. The 17 revised full papers presented were carefully revised and selected from 35 submissions. The papers address a wide range of topics including education, requirements modeling, specification languages, specification/verification case-studies, formal calculi, software design methods, automatic code generation, refinement methodologies, compositional analysis, verification tools, tool integration, benchmarks, challenge problems, and integrated verification environments. Front Matter....Pages - Classifying and Solving Horn Clauses for Verification....Pages 1-21 Static Analysis of Programs with Imprecise Probabilistic Inputs....Pages 22-47 Effect Analysis for Programs with Callbacks....Pages 48-67 Compositional Network Mobility....Pages 68-87 Parallel Bounded Verification of Alloy Models by TranScoping....Pages 88-107 Extending the Theory of Arrays: memset , memcpy , and Beyond....Pages 108-128 An Improved Unrolling-Based Decision Procedure for Algebraic Data Types....Pages 129-148 Program Checking with Less Hassle....Pages 149-169 Verified Calculations....Pages 170-190 Preserving User Proofs across Specification Changes....Pages 191-201 An Automatic Encoding from VeriFast Predicates into Implicit Dynamic Frames....Pages 202-221 Automated Code Proofs on a Formal Model of the X86....Pages 222-241 Verification of a Virtual Filesystem Switch....Pages 242-261 Verifying Chinese Train Control System under a Combined Scenario by Theorem Proving....Pages 262-280 Formal Verification of Loop Bound Estimation for WCET Analysis....Pages 281-303 Result Certification of Static Program Analysers with Automated Theorem Provers....Pages 304-325 A Formally Verified Generic Branching Algorithm for Global Optimization....Pages 326-343 Back Matter....Pages -