This workshop builds upon the success of AVIS'01 which was held in Berlin, Germany in conjunction with Formal Methods Europe 2001 (FME'01). It 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.
More recently, we have seen the emergence of hybrid techniques that combine the ease-of-use of model checkers with the power of theorem provers. Tools based on these techniques afford users with full automation, and are less sensitive to the size of the state space (which may be infinite or arbitrarily large). There is a growing body of knowledge in this field which has a very exciting future. The intention of this workshop is to build a forum for exchanging ideas and experiences by bringing together theoreticians, tool builders, as well as practitioners who are interested in this emerging area of research in formal verification.
Center for High Assurance Computing Systems Naval Research Laboratory Washington DC
A great variety of state-based dynamical systems, such as 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 CMCS workshop is to bring together researchers with a common interest in the theory of coalgebras and its applications.
COCV provides a forum for researchers and practitioners working on optimizing and verifying compilation, and on related fields such as translation validation, certifying and credible compilation, programming language design and programming language semantics 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. Submission of papers at the joint of all these fields is solicited.
University of Dortmund
In recent years, multi-agent systems have come to form one of the key technologies for software development. This workshop aims at bringing together researchers from the fields of logic, theoretical computer science and multi-agent systems in order to discuss formal techniques for specifying and verifying multi-agent systems. Suggested, but not exclusive, topics of interest for the workshop are:
Institute of Informatics, Warsaw University
Fifty years into the First Computing Era some of us in the computing arena have come to realize we have made a false start that cannot be fixed, and for us to finally be able to produce lasting, correct, beautiful, usable, scalable, enjoyable software that stands the tests of time and moral human endeavor, we need to start over. Perhaps we will be able to salvage some of what we have learned from the First Era, but we expect almost everything except the most mathematical and philosophical fundamentals to be brushed aside.
This workshop will focus on diverse approaches to programming, both with and without programming languages, and both new and old, while putting an emphasis on the existing diversity in computing which might have become hidden or ignored due to a quest for the one `right', `general-purpose' solution.
University of Bonn
The aim of the workshop is to provide a forum for researchers who study or apply the theory of fixed points. The topics of the workshop concern applications and development of the theory of fixed points in many different frameworks such as: design and implementation of programming languages, program logics, databases.
Previous workshops where held in Brno (1998, MFCS workshop), Paris (2000, LC2000 workshop), Florence (2001, PLI 01 workshop). In 2002, FICS will be organized in Copenhagen as a satellite workshop to LICS 02.
LaBRI, Bordeaux University
The aim of this one day workshop is to bring together researchers from academia and industry interested in the field of formal language definitions and the use of these definitions for the derivation of tools and software applications. The absence of a standard formal method for language descriptions creates opportunities to study the benefits, drawbacks, enhancements and relationship between various formal language definitions. The workshop welcomes contributions on all aspects of formal language definitions, with special emphasis on applications and tools developed for or with these language definitions.
INRIA Sophia Antipolis, France
Rough Set theory has reached a level of high visibility and maturity. In recent years, we have witnessed diverse, as well as, widespread research in rough set theory and its applications worldwide. A considerable number of applications of rough sets in medicine, economics, finance, business, environment, electrical and computer engineering, a number of sciences, software engineering, and information science have been introduced in recent years. In addition, many rough set case studies and more than a dozen commercial, as well as, research rough set tools are currently available. The proposed workshop is intended as a place for researchers from universities, laboratories and industry to present state-of-the-art in rough set theory and its applications. The aim of this workshop is to bring together researchers from diverse fields of expertise to facilitate dialogue and cooperation. Relevant topics include, but are not limited to:
Warsaw University, Institute of Mathematics
The component-based approach to produce software from smaller units has attracted increasing attention of both research and industry. Software composition extends this approach because it does not only reason about component models but investigates into technology to compose components. Hence, this workshop collects new approaches to software composition, e.g., novel composition operators, composition languages, merging techniques, adaptation techniques, verification and validation techniques, view- and aspect composition techniques, dynamic composition techniques, or uniform composition techniques for XML dialects.
Component based systems are increasingly used in software development. The lack of information about internals at different development stages and the need of optimizing verification and validation require new approaches to test and analysis. The complexity of the problems requires the synergy of various analysis, testing and design for testability approaches. Main focus of the workshop is on techniques, tools, and experiences on testing, analysis and design for testability of components, component based systems, and configurable products. Special attention will be given to heterogeneous, modular and configurable embedded systems that share hardware and software resources and are available in several versions. Contributions about techniques, tools and research results, as well as contributions on experiences, problems and failures that can help in focusing discussion and research are welcome.
The aim of this workshop is to bring together people working especially in the following three areas:
Many studies of complex software systems have shown that more than 80% of the total cost of software development is devoted to software maintenance. In particular, evolution in response to unanticipated changes of requirements accounts for most technical problems and related costs. Therefore, support for unanticipated software evolution becomes a key issue for programming languages, component models and related runtime infrastructures.
This one-day workshop will address the issues inherent in unanticipated static and dynamic evolution of software. Topics of interest include, but are not limited to:
University of Bonn
WITS is the official workshop organized by the IFIP WG 1.7 on `Theoretical Foundations of Security Analysis and Design', established to promote the investigation on the theoretical foundations of security, discovering and promoting new areas of application of theoretical techniques in computer security and supporting the systematic use of formal techniques in the development of security related applications.
Suggested submission topics include:
Dipartimento di Scienze dell'Informazione
Object-oriented programming languages have been and still are the source of extensive foundational and applicative research in several fields including semantics, calculi, type theory, and program verification. The new advances in network technology and distributed systems have recently created world-wide revived interest in object-oriented languages and calculi as effective tools for structuring, composing and coordinating concurrent, distributed, and mobile code.
This workshop intends to offer a forum for discussion about theoretical work on models and type systems, as well as presentation of experience reports on, and novel techniques for, program analysis and verification. Submissions are solicited on all the above subjects and areas.
University of Torino