Skip to main content
SpringerLink
Log in

Verified Software: Theories, Tools, Experiments

4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012 Proceedings

  • Conference proceedings
  • © 2012

Overview

Editors:
  1. Rajeev Joshi

    1. MS 301-285, Pasadena, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Peter Müller

    1. ETH Zürich, Zürich, Switzerland

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Andreas Podelski

    1. Department of Computer Science, University of Freiburg, Freiburg, Germany

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  • Up-to-date results
  • Fast track conference proceedings
  • State-of-the-art report

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

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

Included in the following conference series:

Conference proceedings info: VSTTE 2012.

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

Access this book

Log in via an institution
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

Licence this eBook for your library

Institutional subscriptions

Table of contents (24 papers)

  1. Front Matter

    Download chapter PDF

  2. Cyber War, Formal Verification and Certified Infrastructure

    • Wolfgang Paul
    Pages 1-1

  3. A Certified Multi-prover Verification Condition Generator

    • Paolo Herms, Claude Marché, Benjamin Monate
    Pages 2-17

  4. Integrated Semantics of Intermediate-Language C and Macro-Assembler for Pervasive Formal Verification of Operating Systems and Hypervisors from VerisoftXT

    • Sabine Schmaltz, Andrey Shadrin
    Pages 18-33

  5. The Location Linking Concept: A Basis for Verification of Code Using Pointers

    • Gregory Kulczycki, Hampton Smith, Heather Harton, Murali Sitaraman, William F. Ogden, Joseph E. Hollingsworth
    Pages 34-49

  6. Verifying Implementations of Security Protocols by Refinement

    • Nadia Polikarpova, Michał Moskal
    Pages 50-65

  7. Deciding Functional Lists with Sublist Sets

    • Thomas Wies, Marco Muñiz, Viktor Kuncak
    Pages 66-81

  8. Developing Verified Programs with Dafny

    • K. Rustan, M. Leino
    Pages 82-82

  9. Verifying Two Lines of C with Why3: An Exercise in Program Verification

    • Jean-Christophe Filliâtre
    Pages 83-97

  10. Development and Evaluation of LAV: An SMT-Based Error Finding Platform

    • Milena Vujošević-Janičić, Viktor Kuncak
    Pages 98-113

  11. A Lightweight Technique for Distributed and Incremental Program Verification

    • Martin Brain, Florian Schanda
    Pages 114-129

  12. A Comparison of Intermediate Verification Languages: Boogie and Sireum/Pilar

    • Loren Segal, Patrice Chalin
    Pages 130-145

  13. LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR

    • Florian Merz, Stephan Falke, Carsten Sinz
    Pages 146-161

  14. The Marriage of Exploration and Deduction

    • Rupak Majumdar
    Pages 162-162

  15. Modeling and Validating the Train Fare Calculation and Adjustment System Using VDM++

    • Nguyen Van Tang, Daisuke Souma, Goro Hatayama, Hitoshi Ohsaki
    Pages 163-178

  16. Formalized Verification of Snapshotable Trees: Separation and Sharing

    • Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, Peter Sestoft
    Pages 179-195

  17. Comparing Verification Condition Generation with Symbolic Execution: An Experience Report

    • Ioannis T. Kassios, Peter Müller, Malte Schwerhoff
    Pages 196-208

  18. Verification of TLB Virtualization Implemented in C

    • Eyad Alkassar, Ernie Cohen, Mikhail Kovalev, Wolfgang J. Paul
    Pages 209-224

  19. Formalization and Analysis of Real-Time Requirements: A Feasibility Study at BOSCH

    • Amalinda Post, Jochen Hoenicke
    Pages 225-240

  20. Our Experience with the CodeContracts Static Checker

    • Francesco Logozzo
    Pages 241-242
Back to top

Other volumes

  1. Verified Software: Theories, Tools, Experiments

Keywords

About this book

This volume contains the proceedings of the 4th International Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2012, held in Philadelphia, PA, USA, in January 2012. The 20 revised full papers presented together with 2 invited talks and 2 tutorials were carefully revised and selected from 54 initial submissions for inclusion in the book. The goal of the VSTTE conference is to advance the state of the art through the interaction of theory development, tool evolution, and experimental validation. The papers address topics such as: specification and verification techniques, tool support for specification languages, tool for various design methodologies, tool integration and plug-ins, automation in formal verification, tool comparisons and benchmark repositories, combination of tools and techniques, customizing tools for particular applications, challenge problems, refinement methodologies, requirements modeling, specification languages, specification/verification case-studies, software design methods, and program logic.

Editors and Affiliations

  • MS 301-285, Pasadena, USA

    Rajeev Joshi

  • ETH Zürich, Zürich, Switzerland

    Peter Müller

  • Department of Computer Science, University of Freiburg, Freiburg, Germany

    Andreas Podelski

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation