Verified Software: Theorie, Tools, Experiments

5th International Conference, VSTTE 2013, Menlo Park, CA, USA, May 17-19, 2013, Revised Selected Papers

AvErnie Cohen,Andrey Rybalchenko

Häftad, Engelska, 2014

Del i serien Lecture Notes in Computer Science

560 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt över 249 kr.

Beskrivning

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.

Produktinformation

Utgivningsdatum:2014-01-23
Mått:155 x 235 x 20 mm
Vikt:552 g
Format:Häftad
Språk:Engelska
Serie:Lecture Notes in Computer Science
Antal sidor:345
Upplaga:2014
Förlag:Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
ISBN:9783642541070

Utforska kategorier

Innehållsförteckning

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.