Tutorials
Saturday morning, 09:00-13:00, March 29
The Spec# Programming System provides language and tool support
for assertion checking in object oriented programs. This system consists of the
Spec# programming language which is an extension of C#, the Spec# compiler
which is integrated into the Microsoft Visual Studio development environment
and the Spec# static program verifier which translates Spec# programs into logical
verification conditions. The result is an automatic verification environment
which establishes the correctness of a program before allowing it to be executed.
A unique feature of the Spec# programming system is its guarantee of maintaining
invariants in object-oriented programs in the presence of callbacks, threads
and inter-object relationships. In addition, the Spec# programming system has
been recently extended so that programs that involve the mathematical domains
that are so familiar to textbook examples (such as sum, count , product ,
min, and max) may be verified by the system.
In this half-day tutorial, we give an overview of the Spec# programming system,
providing hands-on experience of the verification of object oriented programs.
Our target audience includes educators who are considering using Spec#
for teaching and programmers who wish to learn about the Spec# methodology.
The verification of several challenging programming examples drawn from a textbook
by Dijkstra and Feijen will be used as illustrative examples.
Important
Installing Spec# before the tutorial, please visit the following URLs:
Speakers:
This tutorial event has been cancelled by the organizers.
Saturday morning, 09:00-13:00, March 29
Many testing techniques vitally depend on symbolic
computation and constraint-solving techniques. Their limits therefore represent
limits for testing as whole. The HOL-TestGen (http://www.brucker.ch/projects/hol-testgen/)
system is designed as plug-in into the state-of-the-art
theorem proving environment Isabelle/HOL. Thus, powerful modeling languages
as well as powerful automated and interactive proof methods for constraint resolution
are available. HOL-TestGen has been applied in unit, sequence, and reactive
sequence black-box test scenarios in substantial case studies. Conceptually, it offers
a unique combined view on these areas traditionally considered separately.
Moreover, it bridges the gap to traditional program verification by concepts such
as “explicit test hypothesis.” The tutorial will be a guided tour through theory,
pragmatics, and case-studies.
Speakers:
This tutorial event has been cancelled by the organizers due to Martin's illness. For further information contact us at the registration desk
Saturday afternoon, 14:30-18:30, March 29
Recently, several applications of learning techniques for solving verification problems
have been proposed. Most often, variations of Angluin's L* algorithm or Biermann's
constraint satisfaction approach, or combinations thereof have been used, for example
to infer invariants to be used in verification. In this tutorial, the learning algorithms as
well as their applications in the verification domain are explained in detail.
Speaker:
This tutorial event has been cancelled by the organizers.
Sunday, April 6
Tutorial is dedicated to Web Services concept and practical development with Java.
In the tutorial will be covered:
- Introduction to Web Services.
- Web Services Standards (SOAP, WSDL, UDDI).
- Developing Web Services with Java EE 5 (JAX-WS 2.0, JAXB 2.0, SAAJ 1.3, XML APIs).
- Web Services Security.
- Service Oriented Architecture (SOA) and Web Services.
Speaker:
Practical Phoenix - A Hands-On Workshop
This tutorial event has been cancelled by the organizers.
Sunday, April 6
We propose to hold a hands-on lab where participants will use Phoenix to solve a practical, relevant, carefully scoped analysis/optimization problem. The emphasis of the lab will be on (1) producing a working software component for an optimizing compiler; (2) application of that component to the optimization of a realistic program; and (3) performing a meaningful evaluation of the component versus competitive components. Participants can work individually or in teams as they see fit. Members of the Phoenix team will be on hand to provide technical assistance.
Speakers:
Sunday, march 30
This tutorial introduces ESC/Java2 and the JML annotation language via their integrated and interactive use within the Eclipse IDE.
The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules. It combines the Design by Contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus. JML has a Java-based syntax and semantics, thus is easy to learn for Java programmers.
ESC/Java2 is a tool that checks that a program is consistent with its annotation. It also detects, at compile time, common programming errors that ordinarily are not detected until run time, and sometimes not even then; for example, null dereference errors, array bounds errors, type cast errors, and race conditions. While ESC/Java uses a theorem prover, it feels to a programmer more like a powerful type checker.
Because JML is familiar to Java programmers, and ESC/Java2 just feels like a typechecker, we believe that they are an excellent way to gently introduce programmers to formal methods.
ESC/Java2 and JML have been deeply integrated into the Eclipse development environment, under the auspices of the European Union Framework 6 research program "Mobius". Within this large research project, many tools and technologies have been integrated to construct the Mobius Program Verification Environment (PVE), a customized version of Eclipse. The PVE looks and feels like Eclipse, but has numerous capabilities that helps one focus on program analysis, design, development, testing, verification, and maintenance using hidden, powerful static checkers, theorem provers, and more.
Speaker:
Model-based vs. Code-based Verification for Secure Systems
This tutorial event has been cancelled by the organizers.
Saturday morning, 9:00-13:00, April 5
With respect to crypto-based software (such as crypto-protocols or
software somehow making use of cryptographic algorithms), a lot of
very successful work has been done to formally analyze abstract
specifications of these protocols for security design weaknesses.
What is still largely missing is an approach which analyzes
pre-existing implementations of crypto-based systems for security
weaknesses. This is necessitated by the fact that so far,
crypto-based software is usually not generated automatically from
formal specifications. Thus, even where the corresponding
specifications are formally verified, the implementations may still
contains vulnerabilities related to the insecure use of cryptographic
algorithms.
An important missing link in the construction of secure systems is
thus finding a practical way to establish correspondence between a
software design and its implementation. This tutorial presents work
towards a solution to this problem for the case of crypto-based
implementations in Java (such as crypto protocols). Given a textual
specification of a crypto-based system and its implementation, we show
how one can construct a formal specification using the security
extension UMLsec of the Unified Modeling Language (UML), which
is based on a formal semantics defined using Abstract State Machines
(ASMs). This formal model can then be automatically and formally
verified against the security goals using automated theorem provers
for first-order logic. In a second step, one can then make sure
that the implementation correctly implements the specification by
making use of techniques such as model-checking, run-time
verification, and security testing. Our approach is supported by a
tool available as open-source. As a running example for
the tutorial, we use the open-source Java implementation Jessie
of the SSL protocol. We will also explain how to apply the
approach to the Java Secure Sockets Extension library recently
made open-source by Sun.
Speaker:
Saturday afternoon, 14:30-18:30, April 5
Data flow analysis is a technique for discovering useful information
from programs. The applications of this technique range from compiler
optimization to software engineering to software verification. The
traditional literature on data flow analysis seems to begin and end with
very simple applications of data flow analysis which creates a very
narrow view of the possibilities of this technique.
This tutorial presents the frontiers of data flow analysis which go much
beyond the common perception. The analysis of heap allocated data is
chosen as a vehicle to bring out the strengths of data flow analysis.
This is interesting because heap data is allocated dynamically and seems
to have arbitrary and unbounded spatial and temporal structures. This is
quite unlike stack and static data whose spatial and temporal structures
are well understood. As a consequence, despite significant progress in
the theory and practice of program analysis, analysing properties of
heap data statically has not reached the same level of maturity as the
static analysis of static and stack data. This tutorial will show how
the advances in data flow analysis can change this situation.
Speaker:
For further information and enquires do not hesitate to contact:
ETAPS 2008 Satellite Events Co-chairs (etaps08-satellites [AT] mit.bme.hu):
Zoltán Horváth
Tihamér Levendovszky
