Skip to main content
main-content

Über dieses Buch

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.

Inhaltsverzeichnis

Frontmatter

Model Checking and the State Explosion Problem

Abstract
Model checking is an automatic verification technique for hardware and software systems that are finite state or have finite state abstractions. It has been used successfully to verify computer hardware, and it is beginning to be used to verify computer software as well. As the number of state variables in the system increases, the size of the system state space grows exponentially. This is called the “state explosion problem”. Much of the research in model checking over the past 30 years has involved developing techniques for dealing with this problem. In these lecture notes, we will explain how the basic model checking algorithms work and describe some recent approaches to the state explosion problem, with an emphasis on Bounded Model Checking.
Edmund M. Clarke, William Klieber, Miloš Nováček, Paolo Zuliani

From Program to Logic: An Introduction

Abstract
We review, compare and discuss several approaches for representing programs by logic formulas, such as symbolic model checking, bounded model checking, verification-condition generation, and symbolic-execution-based test generation.
Patrice Godefroid, Shuvendu K. Lahiri

Introduction to the Coq Proof-Assistant for Practical Software Verification

Abstract
This paper is a tutorial on using the Coq proof-assistant for reasoning on software correctness. It illustrates features of Coq like inductive definitions and proof automation on a few examples including arithmetic, algorithms on functional and imperative lists and cryptographic protocols.
Coq is not a tool dedicated to software verification but a general purpose environment for developing mathematical proofs. However, it is based on a powerful language including basic functional programming and high-level specifications. As such it offers modern ways to literally program proofs in a structured way with advanced data-types, proofs by computation, and general purpose libraries of definitions and lemmas.
Coq is well suited for software verification of programs involving advanced specifications like language semantics and real numbers. The Coq architecture is also based on a small trusted kernel, making possible to use third-party libraries while being sure that proofs are not compromised.
Christine Paulin-Mohring

Advanced Theorem Proving Techniques in PVS and Applications

Abstract
The Prototype Verification System (PVS) is an interactive verification environment that combines a strongly typed specification language with a classical higher-order logic theorem prover. The PVS type system supports: predicate subtypes, dependent types, abstract data types, compound types such as records, unions, and tuples, and basic types such as numbers, Boolean values, and strings. The PVS theorem prover includes decision procedures for a variety of theories such as linear arithmetic, propositional logic, and temporal logic. This paper surveys advanced PVS features, including: types for specifications, implicit induction, iterations, rapid prototyping, strategy writing, and computational reflection. These features are illustrated with simple examples taken from NASA PVS developments.
César A. Muñoz, Ramiro A. Demasi

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

Abstract
Static program verifiers such as Spec#, Dafny, jStar, and VeriFast define the state of the art in automated functional verification techniques. The next open challenges are to make verification tools usable even by programmers not fluent in formal techniques. This paper discusses some techniques used in AutoProof, a verification tool that translates Eiffel programs to Boogie and uses the Boogie verifier to prove them. In an effort to be usable with real programs, AutoProof fully supports several advanced object-oriented features including polymorphism, inheritance, and function objects. AutoProof also adopts simple strategies to reduce the amount of annotations needed when verifying programs (e.g., frame conditions). The paper illustrates the main features of AutoProof’s translation, including some whose implementation is underway, and demonstrates them with examples and a case study.
Julian Tschannen, Carlo Alberto Furia, Martin Nordio, Bertrand Meyer

Using Dafny, an Automatic Program Verifier

Abstract
These lecture notes present Dafny, an automated program verification system that is based on the concept of dynamic frames and is capable of producing .NET executables. These notes overview the basic design, Dafny’s history, and summarizes the environment configuration. The key language constructs, and various system limits, are illustrated through the development of a simple Dafny program. Further examples, linked to online demonstrations, illustrate Dafny’s approach to loop invariants, termination, data abstraction, and heap-related specifications.
Luke Herbert, K. Rustan M. Leino, Jose Quaresma

Backmatter

Weitere Informationen

Premium Partner

    Bildnachweise