Contact: Jochen Pfalzgraf (jochen.pfalzgraf [AT] sbg.ac.at)
URL: http://www.cosy.sbg.ac.at/~jpfalz/ETAPS-/2008
This satellite event has been cancelled.
AVIS is a forum for researchers, students, and practitioners interested in the application of formal methods and tools for the automatic verification of large practical systems. Formal methods, in particular model checking, is increasingly being used in industry to automatically
establish the correctness of (and to find flaws in) finite-state systems, such as descriptions of hardware and protocols. However, model checking is limited in scope due to the state explosion problem. Most practical system descriptions, notably that of software, are therefore not directly amenable to finite-state verification methods since they have very large or infinite state spaces. For such systems, theorem proving - a process that requires manual effort and mathematical sophistication to use - has so far been the only viable alternative.
Contact: Ramesh Bharadwaj (avis08 [AT] chacs.nrl.navy.mil)
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 (smartcards, phones, etc.), where security is a major issue. Moreover, bytecode is device-independent and allows dynamic loading of classes, which provides an extra challenge for the application of formal methods. In addition, the unstructuredness of the code and the pervasive presence of the operand stack also provide extra challenges for the analysis of bytecode. This workshop will focus on the latest developments in the semantics, verification, analysis, and transformation of bytecode. Both new theoretical results and tool demonstrations are welcome.
Contact: Francesco Logozzo (logozzo [AT] microsoft.com )
URL: http://research.microsoft.com/~logozzo/Bytecode%202008/Bytecode08.htm
During the last few years, it has become increasingly clear that a great variety of state-based dynamical systems, like transition systems, automata, process calculi and class-based systems, can be captured uniformly as coalgebras. Coalgebra is developing into a field of its own interest presenting a deep mathematical foundation, a growing field of applications, and interactions with various other fields such as reactive and interactive system theory, object oriented and concurrent programming, formal system specification, modal logic, dynamical systems, control systems, category theory, algebra, analysis, etc. The aim of the workshop is to bring together researchers with a common interest in the theory of coalgebras and its applications.
Contact: Jan Rutten (cmcs08 [AT] cwi.nl)
URL: http://www.cwi.nl/projects/cmcs08/
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)
URL: http://www.complang.tuwien.ac.at/cocv2008/cocv/2008
In recent years, formal methods have been used increasingly in the verification of large-scale circuit designs, particularly in the microprocessor industry. Great progress has been made in adapting and scaling up methods developed in academia, and in developing new methods to solve real verification problems. The DCC workshop aims to bring together academic and industrial researchers in formal methods for hardware design and verification. It will allow participants to learn about the current state of the art and provide a venue for debate about how more effective methods can be developed for the real problems facing microprocessor designers and those developing System on a Chip solutions. A major aim of the workshop is to open these necessary communication channels.
Contact: Gordon Pace (gordon.pace [AT] um.edu.mt)
URL: http://www.cs.um.edu.mt/DCC08
The aim of this 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 embedded software and component-based software engineering. Component-based software design has received considerable attention in industry and academia since object-oriented software development approaches became popular. Recent years has seen the emergence of formal and informal techniques and technologies for the specification and implementation of component-based software architectures. With the increased uptake of component-based safety-critical embedded software, such as the use of the PECOS methodology and OPC, this trend has been amplified. Formal methods have sometimes not kept up with the increasing complexity of software. FESCA aims to address the open question of how formal methods can be applied effectively to these new contexts.
Contact: Iman Poernomo (iman.poernomo [AT] kcl.ac.uk)
URL: http://palab.dcs.kcl.ac.uk/fesca/index.html
Component-based design is widely considered as a major approach to develop systems in a time and cost effective way. Central in this approach is the notion of an interface. Interfaces summarize the externally visible properties of a component and are seen as a key to achieve component interoperability and to predict global system behavior based on the component behavior. To capture the intricacy of complex software products, rich interfaces have been proposed. These interfaces do not only specify syntactic properties, such as the signatures of methods and operations, but also take into account behavioral and extra-functional properties, such as quality of service, security and dependability. Rich interfaces have been proposed for describing, e.g., the legal sequences of messages or method calls accepted by components, or the resource and timing constraints in embedded software. The development of a rigorous framework for the specification and analysis of rich interfaces is challenging. The aim of this workshop is to bring together researchers who are interested in the formal underpinnings of interface technologies.
Contact: Andrzej Wasowski (wasowski [AT] itu.dk), Kim G. Larsen (kgl [AT] cs.aau.dk)()
URL: http://fit2008.cs.aau.dk/
Nowadays, formal methods have an important role in the curricula of higher education. Teaching formal methods is a challenge for both the students and the teachers. As the student's motivation and knowledge background varies, it is difficult to choose the adequate formal method, opportune place in the curriculum. One must decide about the formal method and software tool, the specification language, the relations between the formal and semi-formal methods. Learning and teaching programming languages seems to be an easier task, however, developing rigorous and high level abstraction skills is also crucial and imperative. We would like to provide a forum for the lecturers, teachers, industrial partners to discuss, and present their experiences, their pedagogical methodology, and best practices.
Contact: Zoltan Istenes (istenes [AT] inf.elte.hu)
URL: http://formed2008.inf.elte.hu
In the past decade game semantics has emerged as a new and successful paradigm in the field of semantics of logics and programming languages. Game semantics made its breakthrough in computer science in the early 90s, providing an innovative set of methods and techniques for the analysis of logical systems. Subsequently, game- semantic techniques led to the development of the first syntax- independent fully-abstract models for a variety of programming languages, ranging from the purely functional to languages with non- functional features such as control, references or concurrency. There are also emerging connections between game semantics and other semantic theories, notably theories of concurrency such as the pi- calculus, and traditional tree-based semantics of lambda calculi. In addition to semantic analysis, an algorithmic approach to game semantics has recently been developed, with a view to applications in computer assisted verification and program analysis. The aim of the workshop is to provide opportunity for interaction with other ETAPS '08 events and to become a major meeting point in the research area of Game Semantics and its applications.
Contact: Dan Ghica (d.r.ghica [AT] cs.bham.ac.uk) Russ Harmer (russ.harmer [AT] pps.jussieu.fr)
URL: http://www.cs.bham.ac.uk/galop
GT-VMT 2008 is the seventh workshop of a series serving as a forum for researchers and practitioners interested in graph-based notation, techniques and tools for modeling, validation, manipulation and verification of complex systems. Popular visual modeling formalisms are e.g. UML, Petri nets, graph transformation, and business process/workflow models. Due to the variety of languages and methods used in different domains, the aim of GT-VMT is to promote engineering approaches that starting from high-level specifications and robust formalizations allow for the design and the implementation of such visual modeling techniques. This year's workshop will have a special focus on visualisation, simulation, and animation of models as means of providing an intuitive representation of static semantics and for model behaviour validation.
Contact: Claudia Ermel (lieske [AT] cs.tu-berlin.de)
URL: http://tfs.cs.tu-berlin.de/gtvmt08
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)
URL: http://ldta2008.inf.elte.hu/
MBT 2008 is devoted to model-based testing of both software and hardware. Model-based testing uses models that describe the behaviour 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. Techniques to support model-based testing are drawn from diverse areas, like formal verification, model checking, control and data flow analysis, grammar analysis, and Markov decision processes. The intent of this workshop is to discuss the state of the art in theory, application, tools, and industrialization of model-based testing.
Contact: Bernd Finkbeiner (finkbeiner [AT] cs.uni-sb.de)
URL: http://react.cs.uni-sb.de/mbt2008
Model Based Development (MBD) comprises approaches to software development which heaviliy rely on modeling and the systematic transition from models to executable code. One of these approaches is the OMG's Model Driven Architecture (MDA), which is based on the separation between the specification of a system and its implementation using specific platforms. This workshop focuses on the scientific and practical aspects related with the adoption of MDA and other MBD methodologies (notation, process, methods, and tools) for supporting the construction of computerbased systems, and more specifically, pervasive and embedded software.
Contact: Joa~o M. Fernandes (jmf [AT] di.uminho.pt)
URL: http://www.di.uminho.pt/mompes
The growing importance of automated formal verification in industry is driving a growing interest in those aspects that directly impact the applicability to real-world problems. One of the main technical challenges lies in devising tools that allow the handling of large state spaces using parallel architectures. The aim of the PDMC workshop series is to cover all aspects of parallel and distributed methods and techniques for verification. Theoretical results, algorithms and case studies are equally welcome. Contributions from the domains of model checking, theorem proving, performance evaluation and equivalence checking are anticipated. The PDMC workshop aims to provide a working forum for presenting, sharing and discussing recent achievements in the field of parallel and distributed verification.
Contact: Gerald Luettgen
(gerald.luettgen [AT] cs.york.ac.uk)
Contact: Givana Cerna
(cerna [AT] fi.muni.cz)
URL: http://pdmc.informatik.tu-muenchen.de/PDMC08/
Quantitative aspects of computation involve 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 either directly in the model or as a tool for the analysis of systems.
Contact: Alessandro Aldini (aldini [AT] sti.uniurb.it) Christel Baier (baier [AT] tcs.inf.tu-dresden.de)
URL: http://wwwtcs.inf.tu-dresden.de/ALGI/qapl08/
The objective of RV'08 is to bring together scientists from both academia and industry to debate on how to monitor and analyze the execution of programs, for example by checking conformance with a formal specification written in temporal logic or some other form of history tracking logic. The purpose might be testing a piece of software before deployment, detecting errors after deployment in the field and potentially triggering subsequent diagnosis and fault protection actions, or the purpose can be to augment the software with new capabilities in an aspect oriented style. The longer term goal is to investigate whether the use of lightweight formal methods applied during the execution of programs is a viable complement to the current heavyweight methods proving programs correct always before their execution, such as model checking and theorem proving.
Contact: Martin Leucker (leucker [AT] in.tum.de)
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 shows 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)
URL: http://safecert08.offis.de/
The goal of SC 2008 is to advance the research in component-based software development. Challenges are the composition of components, their development, and verification. Another challenge is the scalability of any component based software development approach to computing devices that provide a wide range of different computing capabilities such as cell phones, PDAs, desktops, or server farms. SC 2008 will be the 7th symposium on software composition. The goal of the SC series is to bring together the research and industrial communities in order to develop a better understanding of how software components may be used to build and maintain large software systems. Therefore papers relating theory and practice are particularly welcome.
Contact: Cesare Pautasso - Éric Tanter (sc2008 [AT] software-composition.org)
URL: http://www.2008.software-composition.org/
SLA++P is dedicated to the model-driven high-level programming of reactive and embedded systems, e.g. synchronous languages. Grounded in formal semantics, they have a growing industrial impact since the 80s. Lustre, Esterel, Signal are now widely and successfully used for real-time and safety critical applications, from nuclear power plant management to Airbus air flight control systems. At the same time, model-based programming is making its way in other fields of software engineering, often involving cycle-based synchronous paradigms. We welcome researchers and practitioners in languages and tools for the model-driven development of embedded applications, in hardware and software. The workshop is open to synchronous and also other engineering design approaches with strong semantical foundations, going from high-level description to provable executable code.
Contact: Eric Rutten (eric.rutten [AT] inria.fr)
URL: http://www.inrialpes.fr/sla++p08/
Generative programming is a recently emerged programming paradigm assisting the creation of flexible libraries, software development automation, and compile-time code transformation. The programming paradigm consists of numerous styles, including aspect-orientation, template metaprogramming, intentional programming, generic programming, and others. These programming styles are becoming everyday tools for today's programmers designing and implementing software ever growing in size and complexity. The purpose of the workshop is to provide a forum for researchers working in this area to discuss the state-of-the-art generative technologies and tools, and also exchange ideas about the future of the generative paradigm. Papers describing practical applications of generative styles, and new possible directions of the paradigm are expected.
Contact: Zoltan Porkolab (gsd [AT] elte.hu)
Rewriting logic (RL) is a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication and interaction. It can be used for specifying a wide range of systems and languages in various application fields. It also has good properties as a metalogical framework for representing logics. In recent years, several languages based on RL (ASF+SDF, CafeOBJ, ELAN, Maude) have been designed and implemented. The aim of the workshop is to bring together researchers with a common interest in RL and its applications, and to give them the opportunity to present their recent works, discuss future research directions, and exchange ideas.
Contact: Grigore Rosu (grosu [AT] cs.uiuc.edu)
URL: http://wrla08.cs.uiuc.edu/
For further information and enquires do not hesitate to contact:
Zoltán Horváth
Tihamér Levendovszky