Verified Software: Theories, Tools, Experiments 5th International Conference, VSTTE 2013, Menlo Park, CA, USA, May 17-19, 2013, Revised Selected Papers /

• Corporate Author: SpringerLink (Online service)
• Other Authors: Cohen, Ernie (Editor), Rybalchenko, Andrey (Editor)
• Format: Electronic eBook
• Language: English
• Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2014.
• Series: Lecture Notes in Computer Science, 8164
• Subjects: Computer science.; Computer programming.; Software engineering.; Programming languages (Electronic computers).; Computer logic.; Mathematical logic.; Artificial intelligence.; Computer Science.; Software Engineering.; Logics and Meanings of Programs.; Programming Languages, Compilers, Interpreters.; Programming Techniques.; Mathematical Logic and Formal Languages.; Artificial Intelligence (incl. Robotics).

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...

Table of Contents:

• Classifying and Solving Horn Clauses for Verification
• Static Analysis of Programs with Imprecise Probabilistic Inputs
• Effect Analysis for Programs with Callbacks
• Compositional Network Mobility
• Parallel Bounded Verification of Alloy Models by TranScoping
• Extending the Theory of Arrays: memset, memcpy, and Beyond
• An Improved Unrolling-Based Decision Procedure for Algebraic Data Types
• Program Checking with Less Hassle
• Verified Calculations.
• Preserving User Proofs across Specification Changes
• An Automatic Encoding from VeriFast Predicates into Implicit Dynamic Frames
• Automated Code Proofs on a Formal Model of the X86
• Verification of a Virtual Filesystem Switch
• Verifying Chinese Train Control System under a Combined Scenario by Theorem Proving
• Formal Verification of Loop Bound Estimation for WCET Analysis
• Result Certification of Static Program Analysers with Automated Theorem Provers
• A Formally Verified Generic Branching Algorithm for Global Optimization.