| The exact schedule is to be announced. Registration will be
opened together with registration for main conference.
Tutorial 1
Monday, Sep. 5th, all day
Building, Combining, and Integrating
Decision Procedures for Software Verification
Tutorial 2
Monday, Sep. 5th, all day
Unified Modeling Language 2.0 - Concepts and Semantics
Tutorial 3
Tuesday, Sep. 6th, morning
An Introduction to CSP || B
Tutorial 4
Tuesday, Sep. 6th, afternoon
QoS Modelling and Verification with UML Statecharts
|
TUTORIAL 1 |
Title:
Building, Combining, and Integrating
Decision Procedures for Software Verification
Speaker:
David Déharbe, University of Rio Grande do Norte
Silvio Ranise, INRIA
Christophe Ringeissen, INRIA
Abstract:
Decision procedures, their combination, and their integration with other
reasoning activities (such as Boolean solving or quantifier handling) have
recently attracted a lot of attention because of their importance for many
verification techniques (such as bounded model checking, software model checking,
and deductive verification to name but a few). In this tutorial, we will describe
some of the techniques which allow us to build, combine, and integrate decision
procedures.
Short CV:
David Déharbe has been professor at Federal University of
Rio Grande do Norte (Natal, Brazil) since 1997. He got his PhD from
University of Grenoble I in 1996, on the subject of "Temporal Logic
Model Checking: Study and Application to the VHDL Language." He was
visiting researcher at Carnegie Mellon University (Pittsburgh, U.S.A.)
from 1995 to 1997. In 2002, he spent a year on sabbatical at LORIA
(Nancy, France). His research interest focus on the development of
automated formal verification techniques (theorem proving and model
checking) and their application to the design of hardware and software
designs. He was the author and principal developer of the CV VHDL model
checker and is now involved in the construction of the theorem prover
haRVey. He has also been the Principal Investigator of several projects
funded by Brazilian funding agencies. He is a member of the Brazilian
Computer Society and is in the Program Committee of several national and
international events (SEFM, SBMF, SBCCI, SBES). He has been involved in
the realization of several scientific events and has held several
administrative positions at his University. He is the co-author of 6
journal papers and 13 publications in international events.
Silvio Ranise has a permanent research position at INRIA from September
2002, in the LORIA laboratory common to CNRS, INRIA and the Universities of
Nancy. He got his PhD in January 2002 from the University of Genova (Italy) and
the University of Nancy 1 (France) under a joint PhD program. The subject of his
PhD was "On the Integration of Decision Procedures in Automated Deduction." His
research interests are program verification, automated deduction, constraint
solving, decision procedures, their combination and integration with Boolean
solvers and other reasoning activities. He is one of the principal designer of
the theorem prover haRVey. He has initiated and co-organized the first two
workshops (in 2003 and 2004) of the series "Pragmatics of Decision Procedures
in Automated Deduction (PDPAR)" and he serves in the Program Committee of this
edition. He is co-ordinator of the "Satisfiability Modulo Theory Library
(SMT-LIB)," an initiative whose major goal is to establish a library of
benchmarks for satisfiability of formulas so to facilitate the evaluation and the
comparison of systems, and advance the state of the art in the eld, in the same
way as, for instance, the SATLIB library has done for propositional
satisfiability. He also serves in the Program Committees of the second workshop on
Empirically Successful Classical Automated Reasoning co-located with CADE'05 and
the 12th Symposium on the Integration of Symbolic Computation and Mechanized
Reasoning (Calculemus 2005) co-located with FME'05. He is the co-author of 6
journal papers and 14 publications in international conferences.
Christophe Ringeissen has a permanent research position at INRIA from October
1995, in the LORIA laboratory common to CNRS, INRIA and Universities of Nancy.
He got his PhD in 1993 at the University of Nancy 1. The subject of his PhD was
on the "Combinations of constraint solving techniques". He works in the Protheo
group aimed at designing and implementing tools for program specification and
verification.
His research interests are automated deduction, constraint solving, semantics of
declarative programming languages (algebraic and logic programming, constraint
programming), and combination of constraint solvers. He was involved in the
design of ELAN, a programming environment based on rewriting, which is developed
in the Protheo group. He was co-organizer of a tutorial on ELAN at ETAPS'2001.
He was co-organizer of FroCoS'2000 (Frontiers of Combining Systems) and
RULE'2004 (Rule-based Programming, workshop of RDP'2004). He was Program
Committee co-chairs of FroCoS'2000, AMAST'2002 and RULE'2004. He was/is in the
Program Committees of the following events: FroCoS'98, Strategies'01, FroCoS'02,
CoSolv'01, CoSolv'03, and FroCoS'05. He was co-editors of three proceedings
(LNAI, LNCS, ENTCS) and he is co-editor of a special issue of the journal
Information and Computation on "Combining Logical Systems". He published 6
articles in international journals, 22 publications in international
conferences, and various publications in international workshops.
|
TUTORIAL 2 |
Title:
Unified Modeling Language 2.0 - Concepts and Semantics
Speaker:
Alexander Knapp, University of Munich
Harald Störrle, University of Munich
Abstract:
The upcoming new version 2.0 of the UML introduces many new concepts and a
substantial reengineering of the metamodel. One of the persistent shortcomings
of the UML, however, is its lack of semantic foundations, which has inspired a
lot of research in the formal methods community. In this tutorial, we would like
introduce the new version of the UML, with a particular emphasis on its semantic
foundations.
The proposed tutorial would present a unique opportunity for participants of
SEFM2005 to get acquainted with the new version of the standard and the state of
the art concerning the relationship between the UML and formal methods.
Short CV:
Dr. Alexander Knapp is a research and teaching assistant at the
department of computer science of the Ludwig-Maximilians-Universität
München at the chair of Prof. Dr. M. Wirsing. In the winter term 1998/99
he spent a research visit to SRI, Menlo Park, California with Prof. J.
Meseguer, PhD. He obtained his PhD in 2000, his dissertation is titled "A
Formal Approach to Object-Oriented Software Engineering". His main
research interests are the integration of formal and semi-formal software
engineering methods and the semantics of programming and modelling
languages.
Dr. Harald Störrle completed his PhD on software architecture in 2000 at
the University of Munich (Prof. Dr. M. Wirsing). Till October last year he
worked as a software architect in the Competence Center Informatics of FJH AG in
Munich, one of the biggest standard software manufacturers in Germany. Since
January, he works as a senior consultant for MGM EDVBeratung GmbH in Munich. In
his industrial work he has been working on some of the largest software projects
in Germany over the last years, Additionally, he is lecturing Software
Engineering at the University of Munich.
|
TUTORIAL 3 |
Title:
An Introduction to CSP || B
Speaker:
Neil Evans, University of Southampton
Steve Schneider, University of Surrey
Helen Treharne, University of Surrey
Abstract:
The tutorial starts with an overview
of the B-Method, the process algebra CSP, and their respective tool
support. A discussion of how they can be combined will be illustrated.
The theoretical foundations underpinning the CSP || B approach will be
presented with particular focus on compositional verification. The
running examples will demonstrate how the industrial-strength tools can
be applied to the verification of a CSP || B specification. The tutorial
concludes by outlining application domains which would benefit from
using CSP || B.
Short CV:
Dr Evans is a Research Fellow within the Department of Electronics and
Computer Science at the University of Southampton. He is currently
working on the RODIN project investigating open source tool support for
verification of B developments. He has extensive experience of using the
theorem prover PVS for verifying security properties and worked on
developing the foundations of CSP || B.
Professor Schneider is Head of Computing at the University of Surrey. He
has been working in the area of formal methods and security for over 10
years. He has published several books including ones on the B-Method
and on the CSP approach to real-time and concurrent systems. He has made
a significant contribution to research in process algebra, its timed
extensions, and its application.
Dr Treharne is a lecturer at the University of Surrey. She was behind the
development of the theoretical foundations for CSP || B, and has recently
completed an EPSRC project which extended the theory of CSP || B and
investigated the animation of CSP || B descriptions. She has previous industrial
experience of using the B-Method to develop embedded software.
|
TUTORIAL 4 |
Title:
QoS Modelling and Verification with UML Statecharts
Speaker:
Holger Hermanns, Saarland University
David N. Jansen, University of Twente
Joost-Pieter Katoen, RWTH Aachen
Abstract:
The UML is an influential and widespread notation for high-level modelling
of information processing system. UML statechart diagrams are a graphical
language to describe system behaviour. They constitute one of the most intensively
used formalisms comprised by the UML. However, statechart diagrams
are lacking concepts for describing real-time, performance, dependability and
QoS characteristics at a behavioural level.
In this tutorial, we present a QoS-oriented extension of UML statechart
diagrams, called StoCharts. StoCharts enhance the basic statechart formalism
with two distinguished features, both being simple and easy to understand,
yet powerful enough to model a sufficiently rich class of stochastic
decision processes. This is illustrated by a selection of case studies performed
using StoCharts. We review the main ingredients of StoCharts and explain
different approaches to evaluate QoS requirements satisfied by a collection of
StoCharts. In particular we emphasize how a rigid formal semantics makes
it possible to employ stochastic model checking to verify QoS requirements.
Short CV:
Holger Hermanns is a professor for dependable systems and software
at Saarland University, where he works on computer assisted modelling and
verification of embedded and distributed systems. Before, he held positions
at the University of Twente, and the University of Erlangen-Nürnberg. In
2001, the Netherlands Organisation for Scientific Research (NWO) awarded
him the "Verniewingsimpuls" prize for innovative research.
David N. Jansen is a postdoc researcher for formal methods and tools
at the University of Twente. Prior to this, he was a postdoc researcher at
Max-Planck Institute for Computer Science, Saarbrücken. finished his Ph.D.
thesis on extensions of statecharts at the information systems group of University
of Twente in 2003.
Joost-Pieter Katoen is a professor for programming languages and
software validation at the RWTH Aachen. Research interests include formal
methods and supporting software tools, in particular formal methods
for performance and dependability evaluation. Before, he held positions at
Philips Research, and the universities in Eindhoven, Erlangen-Nürnberg, and
Twente.
|
|