LZI - Schloss Dagstuhl - Talks + Materials of Seminar 06281

Collector buttons:

Seminar 06281
The Challenge of Software Verification

M. Broy (TU München, DE), P. Cousot (ENS - Paris, FR), J. Misra (Univ. of Austin, US), P. O'Hearn (Queen Mary College - London, GB)

Seminar Wide Materials

Dagstuhl Seminar Proceedings - an Introduction

Abstracts:

Slides:

	Upload or overwrite a document file and/or change title of talk


	Due to caching problems of microsofts internet explorer concerning dynamic webpages, sometimes newly uploaded files are not shown. By pressing [CTRL]+[F5], the page is completely reloaded.

Jean-Raymond Abrial , ETH Zürich

Anindya Banerjee , Kansas State University

Gilles Barthe , INRIA - Sophia Antipolis

Bernhard Beckert , Univ. Koblenz-Landau

Must Program Verification Systems and Calculi Be Verified?

Abstracts:

Slides:

Paper:

Joshua Berdine , Microsoft Research UK

Yves Bertot , INRIA - Sophia Antipolis

Richard Bornat , Middlesex University

Manfred Broy , TU München

Michael Butler , University of Southampton

Verified system design and its link to software verification

Abstracts:

Other:

Egon Börger , Università di Pisa

The Role of Ground Models for Software System Development and Analysis

Abstracts:

Cristiano Calcagno , Imperial College London

Rod Chapman , Praxis High Integrity Systems Ltd. - Bath

Byron Cook , Microsoft Research UK

Patrick Cousot , ENS - Paris

Stefan Hallerstede , ETH Zürich

Moritz Hammer , Universität München

Tony Hoare , Microsoft Research UK

Marieke Huisman , INRIA - Sophia Antipolis

Dieter Hutter , DFKI Saarbrücken

Evolutionary Formal Software Development

Abstracts:

Reiner Hähnle , Chalmers UT - Göteborg

Verification-Based Test Generation

Abstracts:

Slides:

Bart Jacobs , Radboud University of Nijmegen

Cliff Jones , University of Newcastle

Joseph R. Kiniry , University College - Dublin

Where the Rubber Hits the Road: ESC/Java State-of-the-Art Update; Current Challenges, Desires, Directions & GC6-inspired Activities at UCD

Abstracts:

Slides:

Daniel Kröning , ETH Zürich

Gary T. Leavens , Iowa State University

Roadmap for Enhanced Languages and Methods to Aid Verification

Abstracts:

Slides:

DROPS-Submission:

K. Rustan M. Leino , Microsoft Research

Etienne Lozes , ENS - Cachan

Tiziana Margaria , Universität Potsdam

Bertrand Meyer , ETH Zürich

Bringing concurrent programming to the same level of quality as sequential programming

Abstracts:

Tests and proofs of contracted components

Abstracts:

Jayadev Misra , Univ. of Texas at Austin

C. Carroll Morgan , Univ. of New South Wales

David Naumann , Stevens Institute of Technology

Theory Panel Report

Abstracts:

Slides:

Tobias Nipkow , TU München

Verified Enumeration of Tame Plane Graphs

Abstracts:

Slides:

Peter O'Hearn , Queen Mary College - London

Lawrence Paulson , Cambridge University

Integrating Interactive and Automatic Theorem Provers

Abstracts:

Slides:

Wolfgang J. Paul , Universität des Saarlandes

Andreas Podelski , MPI für Informatik - Saarbrücken

Erik Poll , Radboud University of Nijmegen

Wolfgang Reif , Universität Augsburg

Tamara Rezk , INRIA - Sophia Antipolis

Peter H. Schmitt , Universität Karlsruhe

A Case Study in Specification and Software Verification

Abstracts:

Kaisa Sere , Aabo Akademi University - Turku

Natarajan Shankar , SRI - Menlo Park

Verified Software Roadmap

Abstracts:

Paper:

The Verified Software Roadmap: An Overview

Abstracts:

Slides:

Bernhard Steffen , Universität Dortmund

Andrzej Tarlecki , University of Warsaw

Pawel Urzyczyn , University of Warsaw

Tarmo Uustalu , Tallinn Technical University

Natural semantics and logics/type systems for low-level languages and program optimizations

Abstracts:

Slides:

Helmut Veith , TU München

Reinhard Wilhelm , Universität des Saarlandes

Timing Analysis and Timing Predictability

Abstracts:

Jim C. P. Woodcock , University of York

Kwangkeun Yi , Seoul Nat. University

Classification Methods for the Alarms from a Sound Bug-Finding C Analyzer: Our Airac5 Experience

Abstracts:

Slides:

Copyright

This webpage and the material that is made available on this webpage is licensed under a
Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 Unported License.

The CC by-nc-nd license allows you to copy, distribute and transmit the work under the following conditions:

Attribution: You must attribute the work in the manner specified by the author or licensor (but not in any way that suggests that they endorse you or your use of the work).
Noncommercial: You may not use this work for commercial purposes.
No Derivative Works: You may not alter, transform, or build upon this work.

Seminar 06281 The Challenge of Software Verification

Copyright

Seminar 06281
The Challenge of Software Verification