Verified Software: Theorie, Tools, Experiments

5th International Conference, VSTTE 2013, Menlo Park, CA, USA, May 17-19, 2013, Revised Selected Papers
Herausgegeben:Cohen, Ernie; Rybalchenko, Andrey

• Broschiertes Buch

Produktbeschreibung

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.

Produktdetails

• Lecture Notes in Computer Science 8164
• Verlag: Springer / Springer Berlin Heidelberg / Springer, Berlin
• Artikelnr. des Verlages: 978-3-642-54107-0
• 2014
• Seitenzahl: 364
• Erscheinungstermin: 23. Januar 2014
• Englisch
• Abmessung: 235mm x 155mm x 20mm
• Gewicht: 557g
• ISBN-13: 9783642541070
• ISBN-10: 3642541070
• Artikelnr.: 40181349

Inhaltsangabe

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.