Skip to main content
SpringerLink
Log in

Tools for Practical Software Verification

International Summer School, LASER 2011, Elba Island, Italy, Revised Tutorial Lectures

  • Textbook
  • © 2012

Overview

Editors:
  1. Bertrand Meyer

    1. ETH Zurich, Zurich, Switzerland

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Martin Nordio

    1. ETH Zurich, Zurich, Switzerland

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

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

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

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

Included in the following conference series:

Conference proceedings info: LASER 2011.

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 49.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 (6 chapters)

  1. Front Matter

    Download chapter PDF

  2. Model Checking and the State Explosion Problem

    • Edmund M. Clarke, William Klieber, Miloš Nováček, Paolo Zuliani
    Pages 1-30

  3. From Program to Logic: An Introduction

    • Patrice Godefroid, Shuvendu K. Lahiri
    Pages 31-44

  4. Introduction to the Coq Proof-Assistant for Practical Software Verification

    • Christine Paulin-Mohring
    Pages 45-95

  5. Advanced Theorem Proving Techniques in PVS and Applications

    • César A. Muñoz, Ramiro A. Demasi
    Pages 96-132

  6. Automatic Verification of Advanced Object-Oriented Features: The AutoProof Approach

    • Julian Tschannen, Carlo Alberto Furia, Martin Nordio, Bertrand Meyer
    Pages 133-155

  7. Using Dafny, an Automatic Program Verifier

    • Luke Herbert, K. Rustan M. Leino, Jose Quaresma
    Pages 156-181

  8. Back Matter

    Download chapter PDF
Back to top

Keywords

About this book

The LASER school is intended for professionals from the industry (engineers and managers) as well as university researchers, including PhD students. Participants learn about the most important software technology advances from the pioneers in the field. The school's focus is applied, although theory is welcome to establish solid foundations. The format of the school favors extensive interaction between participants and speakers. LASER 2011 is devoted to software verification tools. There have been great advances in the field of software verification in recent years. Today verification tools are being increasingly used not only by researchers, but by programming practitioners. The summer school will focus on several of the most prominent and practical of such tools from different areas of software verification (such as formal proofs, testing and model checking). During the school the participants will not only learn the principles behind the tools, but also get hands-on experience, trying the tools on real programs.

Editors and Affiliations

  • ETH Zurich, Zurich, Switzerland

    Bertrand Meyer, Martin Nordio

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation