Skip to main content
  • Conference proceedings
  • © 2014

Verified Software: Theorie, Tools, Experiments

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

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 8164)

Part of the book sub series: Programming and Software Engineering (LNPSE)

Conference series link(s): VSTTE: Working Conference on Verified Software: Theories, Tools, and Experiments

Conference proceedings info: VSTTE 2013.

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

This is a preview of subscription content, log in via an institution to check for access.

Table of contents (17 papers)

  1. Front Matter

  2. Classifying and Solving Horn Clauses for Verification

    • Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
    Pages 1-21
  3. Static Analysis of Programs with Imprecise Probabilistic Inputs

    • Assale Adje, Olivier Bouissou, Jean Goubault-Larrecq, Eric Goubault, Sylvie Putot
    Pages 22-47
  4. Effect Analysis for Programs with Callbacks

    • Etienne Kneuss, Viktor Kuncak, Philippe Suter
    Pages 48-67
  5. Compositional Network Mobility

    • Pamela Zave, Jennifer Rexford
    Pages 68-87
  6. Parallel Bounded Verification of Alloy Models by TranScoping

    • Nicolás Rosner, Carlos Gustavo López Pombo, Nazareno Aguirre, Ali Jaoua, Ali Mili, Marcelo F. Frias
    Pages 88-107
  7. Extending the Theory of Arrays: memset , memcpy , and Beyond

    • Stephan Falke, Florian Merz, Carsten Sinz
    Pages 108-128
  8. An Improved Unrolling-Based Decision Procedure for Algebraic Data Types

    • Tuan-Hung Pham, Michael W. Whalen
    Pages 129-148
  9. Program Checking with Less Hassle

    • Julian Tschannen, Carlo A. Furia, Martin Nordio, Bertrand Meyer
    Pages 149-169
  10. Verified Calculations

    • K. Rustan M. Leino, Nadia Polikarpova
    Pages 170-190
  11. Preserving User Proofs across Specification Changes

    • François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
    Pages 191-201
  12. An Automatic Encoding from VeriFast Predicates into Implicit Dynamic Frames

    • Daniel Jost, Alexander J. Summers
    Pages 202-221
  13. Automated Code Proofs on a Formal Model of the X86

    • Shilpi Goel, Warren A. Hunt Jr.
    Pages 222-241
  14. Verification of a Virtual Filesystem Switch

    • Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, Wolfgang Reif
    Pages 242-261
  15. Verifying Chinese Train Control System under a Combined Scenario by Theorem Proving

    • Liang Zou, Jidong Lv, Shuling Wang, Naijun Zhan, Tao Tang, Lei Yuan et al.
    Pages 262-280
  16. Formal Verification of Loop Bound Estimation for WCET Analysis

    • Sandrine Blazy, André Maroneze, David Pichardie
    Pages 281-303
  17. Result Certification of Static Program Analysers with Automated Theorem Provers

    • Frédéric Besson, Pierre-Emmanuel Cornilleau, Thomas Jensen
    Pages 304-325
  18. A Formally Verified Generic Branching Algorithm for Global Optimization

    • Anthony Narkawicz, César Muñoz
    Pages 326-343
  19. Back Matter

Other Volumes

  1. Verified Software: Theories, Tools, Experiments

About this book

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.

Editors and Affiliations

  • 107 Hewett Road, Wyncote, USA

    Ernie Cohen

  • Technische Universität, München, Germany

    Andrey Rybalchenko

Bibliographic Information

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access