Contact: Jochen Pfalzgraf (jochen.pfalzgraf [AT] sbg.ac.at) and Julia Padberg
URL: http://www.cosy.sbg.ac.at/~jpfalz/ETAPS-/2009
WITS2009 is the ninth workshop of the IFIP WG 1.7 on ``Theoretical Foundations of Security Analysis and Design'', that promotes the investigation on theoretical foundations of security, discovering and promoting new applications of theoretical techniques and supporting the systematic use of formal techniques.
ARSPA2009 is the sixth workshop on ``Automated Reasoning for Security Protocol Analysis'', for researchers and practitioners from the security and the formal methods communities, from academia and industry, who are working on automated reasoning techniques and tools for the specification and analysis of security protocols. This year the two workhops join forces and invite researchers working on security issues to participate and present their recent results in theory, as well as in automated reasoning techniques and tools.
Contact: Pierpaolo Degano (degano [AT] di.unipi.it) and Luca Vigano
URL: http://www.avantssar.eu/arspa-wits09/
Bytecode, such as produced by e.g. Java and .NET compilers, has become an important topic of interest, both for industry and academia. The industrial interest stems from the fact that bytecode is typically used for the Internet and mobile devices (smart-cards, phones, etc.) applications, where security is a major issue. This workshop will focus on theoretical and practical aspects of semantics, verification, analysis, certification and transformation of bytecode.
Contact: Samir Genaim (samir [AT] clip.dia.fi.upm.es)
URL: http://www.clip.dia.fi.upm.es/Conferences/BYTECODE09
COCV provides a forum for researchers and practitioners working on optimizing and verifying compilation, and on related fields such as translation validation, certifying compilation and embedded systems with a special emphasis on hardware verification, formal synthesis methods, correctness aspects in HW/SW co-design, formal verification of hardware/software systems, and practical and industrial applications of formal techniques for exchanging their latest findings, and for plumbing the mutual impact of these fields on each other. By encouraging discussions and co-operations across different, yet related fields, the workshop strives for bridging the gap between the communities, and for stimulating synergies and cross-fertilizations among them.
Contact: Jens Knoop (knoop [AT] complang.tuwien.ac.at and Wolf Zimmermann
URL: http://www.complang.tuwien.ac.at/cocv2009/cocv/2009
Aerospace systems such as Spacecraft, Unmanned Aerial Vehicles (UAVs), Air Traffic Control are critical systems for which errors in either software or hardware can be catastrophic. Correctness notions are in fact mostly tightly connected to performance issues. What is the probability of a space mission success? Safety and dependability analysis in nominal as well as in the degraded modes of operation are prominent examples thereof. This calls for combining correctness, safety, dependability, and performance aspects in an integrated approach. This workshop aims to bring together researchers and practitioners that apply or develop (semi-)formal techniques for the modeling, verification, performance, and safety analysis of aerospace (or any critical) systems. Approaches that attempt to combine some of these different aspects are of particular interest.
Contact: Joost-Pieter Katoen (katoen [AT] cs.rwth-aachen.de)
URL: http://moves.rwth-aachen.de/Events/COMPASS09/
The aim of the FESCA workshop is to bring together researchers from academia and industry interested in formal modeling approaches as well as associated analysis and reasoning techniques with practical benefits for component-based software engineering.
Component-based software design has received considerable attention in industry and academia since object-oriented development became popular. In recent years, the growing need for safety-critical software and the increased relevance of systems reliability and scalability have stimulated the emergence of formal techniques for the specification and implementation of component-based software architectures.
Formal methods have not entirely kept up with the increasing complexity of software. Engineers often prefer semi-formal notations and techniques to model and organize components. In common semi-formal techniques, important component-specific attributes (like quality of service, correct service coordination, or resource consumption) are rarely considered. FESCA aims to address the open question of how formal methods can be applied effectively to these new contexts and challenges.
Contact: Barbora Zimmerova and Jens Happe (fesca09 [AT] ipd.uka.de)
URL: http://sdq.ipd.uka.de/conferences_and_events/fesca09
GaLoP is the annual international workshop on game-semantic models for logics and programming languages and their applications. This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tutorials as well as contributed papers and invited talks.
Contact: Guy McCusker (G.A.McCusker [AT] bath.ac.uk) and Andrzej Murawski (Andrzej.Murawski [A] comlab.ox.ac.uk)
URL:http://www.comlab.ox.ac.uk/galop09/
GT-VMT 2009 is the eighth workshop of a series that serves as a forum for all researchers and practitioners interested in the use of graph-based notation, techniques and tools for the specification, modeling, validation, manipulation and verification of complex systems. The aim of the workshop is to promote engineering approaches that provide effective sound tool support for visual modeling languages, enhancing formal reasoning at the semantic level (e.g., for model analysis, transformation, and consistency management) in different domains, such as UML, Petri nets, Graph Transformation or Business Process/Workflow Models.
This year's workshop will have a special focus on visualisation, simulation, and verification of domain-specific languages (DSLs) to improve the automation and quality in model-driven and/or service-oriented processes.
Contact: Reiko Heckel (reiko [AT] mcs.le.ac.uk) and Artur Boronat
URL: http://www.cs.le.ac.uk/events/gtvmt09/
Hardware designs today are more than three orders of magnitude larger than the designs of the 1980s, yet the abstraction level of design descriptions has not changed. To compound the problem, some of our traditional simplifying assumptions -for example, that wire delay can be neglected in early stages of the design cycle- are no longer valid. An abstraction breakthrough is sorely needed.
The HFL workshops focus on using modern programming language techniques -in particular, techniques derived from the field of functional programming- to describe hardware abstractly yet precisely. A major aim of HFL is to facilitate communication and debate among academic and industrial researchers in programming languages, hardware description, high-level modeling, verification, and formal design environments.
Contact: Andy Martin (akmartin [AT] us.ibm.com and John O'Leary)
URL: http://www.hflworkshop.org/hfl09/
The LDTA workshops bring together researchers interested in the field of formal language definitions and language technologies, with an emphasis on tools developed for or with these language definitions. Several specification formalisms like attribute grammars, action semantics, operational semantics, term rewriting, and algebraic approaches have been developed over the years. Of specific interest are the formal analysis of language specifications, and the automatic generation of language processing tools from such specifications. These tools typically perform some sort of program analysis, transformation, or generation. Also of interest are applications of such tools in domains including, but not limited to, modeling languages, re-engineering and re-factoring, aspect-oriented and domain-specific languages, XML processing, visualization and graph transformation.
Contact: Eric Van Wyk (evw [AT] cs.umn.edu), Mark van den Brand, and Gorel Hedin
URL: http://www.ldta.info
MBT 2009 is devoted to model-based testing of both software and hardware. Model-based testing uses models that describe the behavior of the system under consideration to guide such efforts as test selection and test results evaluation. Model-based testing has gained attention with the popularization of models in software/hardware design and development. Of particular importance are formal models with precise semantics, such as state-based formalisms. Testing with such models allows one to measure the degree of the product's conformance with the model. The intent of this workshop is to bring together researchers and users using different kinds of models for testing and to discuss the state of the art in theory, applications, tools, and industrialization of model-based testing.
Contact: Bernd Finkbeiner (finkbeiner [AT] cs.uni-sb.de)
URL: http://react.cs.uni-sb.de/mbt2009
This is a call for participation in a Kick-Off meeting in conjunction with ETAPS 2009 with the aim of establishing an ERCIM Working Group called MLQA on Models and Logics for Quantitative Analysis.
Models and Logics for Quantitative Analysis are seen as comprising process models analysed using logics for quantitative properties. More specifically, we will (1) consider process models formally described by transition systems, automata or process calculi, (2) we will consider logics for expressing stochastic and continuous (control theory) properties as well as discrete ones, (3) we will focus on algorithms, theory and tools, and (4) we will study applications within embedded systems and service oriented systems but will aim at treating also IT guided workflow systems.
Contact: Flemming Nielson (Nielson [AT] imm.dtu.dk)
URL: http://www.mt-lab.dk/MLQA.htm
The aim of this workshop is to bring together researchers from academia and industry who are interested in developing techniques for the quality assessment of Open Source Software (OSS), leading to the definition of a complete certification process.
The workshop will focus on formal methods and model-based techniques, emphasising on those aspects which are specific to OSS, such as unconventional development, rapid evolution of the code, and huge amount of legacy code.
Contributions to the workshop are expected to present foundations, methods, tools and case studies that integrate techniques from different areas such as certification, security, reverse engineering, and formal modelling and verification, in order to overcome the challenges in the quality assessment of OSS.
Contact: Antonio Cerone (antonio [AT] iist.unu.edu)
URL: http://opencert.iist.unu.edu/
This workshop aims to offer a forum for researchers from different fields to exchange new ideas on one of the central challenges in programming in the near future: the development of programming methodologies and infrastructures where concurrency and communication are the norm rather than a marginal concern, be it for web services, sensor networks, multicore CPUs, business integration or high-performance computing. The development of effective programming methodologies for this new area demands exploration and understanding of a wide range of ideas and methodologies, from language primitives to concurrent data structures to types for linearity and communication to static analysis to runtime architectures. The workshop is dedicated to the focused exchange of new ideas on these topics in the quest for a unifying picture in this new area of programming methodologies.
Contact: Alastair Beresford (arb33 [AT] cam.ac.uk) and Simon Gay (simon [AT] dcs.gla.ac.uk)
URL: http://places09.di.fc.ul.pt/
Quantitative aspects of computation refer to the use of physical quantities (time, bandwidth, etc.) as well as mathematical quantities (e.g. probabilities) for the characterisation of the behaviour and for determining the properties of systems. Such quantities play a central role in defining both the model of systems (architecture, language design, semantics) and the methodologies and tools for the analysis and verification of system properties. The aim of the QAPL workshop series is to discuss the explicit use of time and probability and general quantities either directly in the model or as a tool for the analysis of systems.
Contact: Alessandra Di Pierro (alessandra.dipierro [AT] univr.it) and Herbert Wiklicky et al.
URL: http://wwwtcs.inf.tu-dresden.de/ALGI/qapl09/
Reversible computation has a growing number of promising application areas such as the modelling of biochemical systems, program debugging and testing, database recovery, discrete event simulation and even programming languages for quantum computing. This workshop aims at being a forum for researchers and students interested in new developments, and directions for future investigation, in the field of reversible computation. One of the specific goals of the workshop is to establish cooperation among experts from a variety of fields of computer science who are interested in reversibility. The workshop aims also at widening the knowledge of reversible computation among postgraduate students and young researchers from the U.K. and abroad.
Contact: Irek Ulidowski ( iu3 [AT] mcs.le.ac.uk )
URL: http://www.cs.le.ac.uk/events/RC2009/
Certification of Safety-Critical Software Controlled Systems In many domains like transportation, power generation, medical technology, manufacturing and space exploration, statutory obligations traditionally require a formalized certification for the development of high assurance products. Formal methods are part of the standard recommendations, in particular for the higher safety integrity levels. However, experience and recent work show that certifiable development of high-assurance software needs a lot more than pure application of formal techniques and tools that are founded on a formal semantics and support in parts automated code generation, formal analysis, verification or error detection. The major question to be addressed in the workshop is how to embed formal methods and tools in a seamless design process which covers several development phases and which includes an efficient construction of a safety case for the product.
Contact: Michaela Huhn (M.Huhn [AT] tu-bs.de), Hardi Hungar
URL: http://safecert09.offis.de
Mathematical treatments of concrete syntax (using strings, trees, etc.) have always been a central concern in programming language implementation and computer-aided reasoning. It has proved much harder to find theories of abstract syntax addressing the structural properties common to all high-level semantics of formal languages, especially those properties that have to do with substitution, delimiting the scope of names, and sharing common substructures. The purpose of the workshop is to bring together researchers who are applying logic, category theory and set theory to the study of abstract syntax in computer languages, as well as researchers who are building computer systems based on those theories; applications in computational logic, program language design, and mechanised theorem proving are particularly welcome.
Contact: Maribel Fernandez (Maribel.Fernandez [AT] kcl.ac.uk)
URL: http://www.dcs.kcl.ac.uk/staff/maribel/TAASN.html
The advantage of computing with graphs rather than terms is that common subexpressions can be shared, improving the efficiency of computations in space and time. Sharing is ubiquitous in implementations of programming languages: many functional, logic, object-oriented and concurrent calculi are implemented using term graphs. Research in term and graph rewriting ranges from theoretical questions to practical implementation issues. Different research areas include: the modelling of first- and higher-order term rewriting by (acyclic or cyclic) graph rewriting, the use of graphical frameworks such as interaction nets and sharing graphs (optimal reduction), rewrite calculi for the semantics and analysis of functional programs, graph reduction implementations of programming languages, graphical calculi modelling concurrent and mobile computations, object-oriented systems, graphs as models of biological or chemical abstract machines, and automated reasoning and symbolic computation systems working on shared structures.
Contact: Andrea Corradini (andrea [AT] di.unipi.it)
URL: http://www.di.unipi.it/~andrea/Workshops/TG09/
WING 2009 will be an interdisciplinary workshop bringing together researchers from fields like formal methods, symbolic computation, or automated reasoning, to discuss novel approaches to reasoning about loops in programs. Techinques of interest involve abstract interpretation, algebra, rippling, theorem proving, model checking, static analysis, and many more. If you are interested in more sophisticated approaches to the verification of loops than ``the programmer has to specify a sufficiently strong invariant'' --- this is the event for you!
Contact: air [AT] macs.hw.ac.uk
URL: http://mtc.epfl.ch/events/WING09/
We present a practical synthesis of formal methods, theoretical computer science, and practical testing techniques. This is an ambitious agenda, so to avoid overloading participants we will split the tutorial into two complementary sessions. The tutorial is suitable for levels of ability.
Part 1 presents the theoretical and practical background to the state-based "X-machine testing methodology". First described in the late 90s, this had developed into a comprehensive design and `complete testing' approach that can exploit hardware-inspired design-for-test conditions to ensure `correctness-via-testing'.
Part 2 offers a hands-on opportunity to investigate techniques for testing OO systems using the JWalk system. This is a lazy systematic unit testing tool that supports exhaustive class testing, and has been shown to test up to two orders of magnitude more paths than manual tests created for JUnit by an expert tester.
Contact: Mike Stannett (m.stannett [AT] dcs.shef.ac.uk) and Tony Simons
URL: http://www.dcs.shef.ac.uk/~mps/etaps09/
This tutorial gives an introduction into formal foundations for verifying security-critical software. It explains a formal framework based on predicate logic for formalizing important security properties such as secrey, integrity, and authenticity. It can be used to formally, automatically verifiy software specifications against security properties using automated theorem provers for first-order logic. It shows how Java or C implementations can be verified against these specifications using software model-checkers (with an enphasis on crypto-protocols). The approach is explained at the hand of an implementation of the SSL protocol within the Java Secure Sockets Extension (JSSE) recently made open-source by Sun. The tutorial includes hands-on tool demos in small groups (if sufficient computers or participants laptops with verification software installed are present).
Contact: Jan Jurjens (http://mcs.open.ac.uk/jj2924)
URL: TBA
Formal model based refinement has enjoyed considerable success in projects where it has been used. However refinement is very demanding as regards the precise relationship between abstract and concrete models, which can undermine its connection to system requirements. Retrenchment modifies the main proof obligations of refinement in order to increase expressiveness and applicability (at the price of a weaker general theory).
The tutorial firstly introduces retrenchment and presents the main theoretical features (compositions, interworking with refinement and the Tower Pattern). Secondly, it considers a case study: the Mondex Purse, a critical application in which the exigencies of refinement prevented the formal modelling from fully addressing a number of issues. These can be incorporated using retrenchment.
Contact: Richard Banach (banach [AT] cs.man.ac.uk)
URL: http://www.cs.man.ac.uk/~banach/EVENTS/ETAPS.2009.Tutorial.html
This tutorial introduces a verification-centric style to developing reliable, dependable Java software systems. In this process, the JML annotation language is used to specify the behavior of modules via a model-based and DBC-centric approach. Moreover, powerful tools are available that compile and reason about JML-annotated Java for runtime checking, unit testing, static analysis, specification generation, etc. This process and these tools have been deeply integrated into the Eclipse platform. The resulting IDE is called the Mobius Program Verification Environment (PVE). 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.
Contact: Joe Kiniry (kiniry [AT] acm.org), Dan Zimmerman, Erik Poll
URL: TBA
Dr Jeremy Jacob and Dr Simon O'Keefe, University of York
The satellite organisers can be contacted by sending e-mail
to <etaps-satellites@cs.york.ac.uk>.