The synergy between Logic and Computational Complexity has gained importance and vigor in recent years, cutting across areas such as Proof Theory, Finite Model Theory, Computation Theory, Applicative Programming, Database Theory, and Philosophical Logic. Several machine-independent approaches to computational complexity have been developed, which characterize complexity classes by conceptual measures borrowed primarily from mathematical logic. Examples are descriptive complexity (finite model theory), bounded arithmetic, set-existence principles, intrinsic theories, linear logics, and algebras of functions. Collectively these approaches might be dubbed Implicit Computational Complexity. Practically, implicit computational complexity provide framework for a streamlined incorporation of computational complexity into areas such as formal methods in software development, programming language theory, and database theory.

The mission of the workshop is to further the development of implicit computational complexity and its applications, in particular in database theory, functional programming languages, and formal methods in hardware and software design. In addition to research reports on advances in implicit computational complexity, the workshop will strive to facilitate the discovery of conceptual bridges and unifying principles.

Symbolic model checking is a formal technique for the verification of finite-state concurrent systems. Symbolic model checkers (e.g. SMV, VIS) have been used to verify industrial systems, ranging from hardware to communication protocols to safety critical plants and procedures. Symbolic model checking is applied in technology transfer projects, and is the core technique for several industrial verification tools.
The aim of the workshop is to bring together active developers and users of symbolic model checkers, compare state of the art model checking techniques (e.g. compositional reasoning, abstraction, partitioning), discuss experimental results and experience reports, and promising directions for future research.

"Run-Time Result Verification" is a novel approach to the verification of digital systems: the idea is to verify formally the correctness of the results of each run of the system rather than the correctness of the system algorithm or code. For instance, rather than proving in advance that (the code implementing) a compiler is correct, each individual run of the compiler is followed by a validation phase which verifies that the target is a correct compilation of the source program on this run. Run-Time Result Verification is robust to implementation changes and can be often used to verify systems which are not available for examination or simply too difficult and expensive to verify with standard practice in formal verification. Moreover, it can detect run-time execution errors which cannot be detected with traditional formal verification techniques. It has been recently applied with success to the certification of industrial compilers, mobile code and safety critical software. The aim of the workshop is to bring together active researchers in this emerging research area to discuss scientific issues and industrial applications.

This workshop will address the use of formal methods in the development and analysis of security protocols. Topics of interest include descriptive techniques (specification languages, models, logics) and analysis techniques (model checking, theorem proving, and their combination), as applied to protocols for authentication, fair exchange, electronic commerce, and electronic auctions. We particularly want to hear about new approaches, new problems, new security properties, and new protocol bugs. The workshop program will likely include tutorials, technical sessions, and a panel discussion. Our overall aim is to address questions such as: What are the opportunities in security for more formal reasoning and analysis? Where should researchers in formal methods be spending their time, and energy?

Intuitionistic and modal logics are of foundational relevance to Computer Science and both have led to successful applications in the formal specification and verification of computer systems. The intuitionistic and the modal frameworks are usually investigated separately. However, a growing body of published work, stimulated by theoretical considerations and fed by various applications in Computer Science, shows that both paradigms may fruitfully be merged. Intuitionistic Modal Logic (IML) and associated theories can exploit both the proof-theoretic strengths of intuitionistic logic and the model-theoretic features of modal logics. The potential and the challenge of IML both lie in finding a satisfactory combination of its intensional and its extensional aspects. We intend the workshop to seed a more concerted organisation of the ongoing research in the area of IML, bringing together the method-oriented and the problem-oriented approaches on the one hand, and the proof-theoretic and model-theoretic ones on the other. This will create fruitful research stimuli through the friction between engineering applications and pure theory, and between intensional and extensional lines of thinking.

Strategies are almost ubiquitous in automated deduction and reasoning systems, yet only recently have they been studied in their own right. The workshop aims at making progress towards a deeper understanding of the nature of theorem proving strategies, their descriptions, their properties, and their usage. It provides a common forum for researchers working on all aspects of strategies, with an emphasis on strategy languages, theory of strategies, and proof planning. The workshop continues and focuses the efforts of two previous workshops held in conjunction with CADE'97 and CADE'98. Information about this and previous workshops is available at the workshop web site (see above).

Both Deduction Systems and Computer Algebra Systems are receiving growing attention from industry and academia. On the one hand, Mathematical Software Systems have been commercially very successful. Their use is now wide-spread in industry, education, and scientific contexts: there are now literally millions of installations of computer algebra programs. On the other hand, the use of formal methods in hardware and software development has made Deduction Systems indispensable not least because of the complexity and sheer size of the reasoning tasks involved. In spite of these successes there is still need for improvement as many application domains still fall outside the scope of existing Deduction Systems and Computer Algebra Systems. The workshop is intended for researchers and developers interested in combining the reasoning capabilities of Deduction Systems and the computational power of CASs. A key issue is whether existing systems and technologies can be integrated as they stand or if a fundamental redesign will be necessary. Contributions addressing this specific problem will be considered of special interest.

The goal of this workshop is to emphasize and exploit the connections between Groebner bases and rewrite systems at the levels of theory, implementation and application. Of particular interest are the connections between Groebner bases in noncommutative rings and rewrite systems over strings. Participants from both the Groebner basis and rewriting communities will be invited to discuss current research. The workshop will consist of several sessions begun with presentation of a position paper followed by open discussion of the topic. Position papers, open problems and other participant contributions will be published on the world wide web as a resource for future research.

The aim of this one-day workshop is to bring together researchers working on both the theoretical and applied aspects of explicit substitutions, to present recent work (possibly still in progress), and to discuss new ideas as well as emerging trends in the subject. A special issue of MCSC dedicated to this workshop is planned.

It seems to the organizers that there has been recently a reawaking of interest in many aspects of realizability interpretations -- especially as regards type systems for programming language semantics of for constructive reasoning. But, the details of realizability can be quite technical, and so the aim of the workshop is to have several tutorial lectures on history, basic definitions and results, recent applications, connections to category theory, and then leave room for contributed workshop-style research talks (of 30 minutes each). The workshop will last two days, and we may need one evening session or a poster session.
Aside from the topics mentioned above, we wish to solicit contributions on such topics as: Recursive Definitions of Types, Connections with Synthetic/Axiomatic Domain Theory, Applications to Normalization, Modal Logics, Logical Relations, Uses for Specification, Problems of Automating Deduction, and Extraction of Algorithms. Reports on work in progress are encouraged.
An official call for papers will be distributed early in October along with a listing of the scheduled tutorial lectures. We also expect that there will be a good possibility of reproducing in print after the workshop - perhaps as a special issue of an appropriate journal - the tutorials and the major results presented during the workshop.

The aim of the FMICS workshops is to provide a forum mainly intended for, but not limited to, researchers of ERCIM sites who are interested in the development and application of formal methods in industry. In particular, these workshops should bring together scientists that are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. They also aim at the promotion of research and development for the improvement of formal methods and tools for industrial applications.

The First International Workshop on Formal Methods for Industrial Critical Systems took place in Oxford on March 19, 1996. The second edition was held in Cesena on July 4-5, 1997. The third edition was held in Amsterdam on May 25-26, 1998.

In the recent years, there has been a concerted effort to understand the complexity of various problems which arise in Database Theory, logics for Artificial Intelligence, and Finite Model Theory. Moreover in many cases, there are complexity theory results for both finite and infinite examples. These complexity results are not only interesting in their own right but are important because they can be used to pinpoint the sources of essential complexity inherit in these problems. Thus these theoretical results can help to direct the search for more efficient algorithms for specific problems as well as to find of classes of problems where generally complex problems have simpler solutions.
We intend to bring together researchers from three interconnected areas: Database Theory, Logical Foundations of AI and Finite Model Theory in expectation that their interaction will lead to the better comprehension of the fundamental complexity issues within these areas. In addition, this workshop will alert researchers in each specific discipline about the possible applications of the techniques developed in the other disciplines. Each of these areas provides a language which can often illuminate the problems from the other two. As a result we expect to increase the collaboration between the corresponding communities.

Mathematical induction is required for reasoning about objects or events containing repetition, e.g. computer programs with recursion or iteration, electronic circuits with feedback loops or parameterized components. It is thus a vital ingredient of formal methods techniques for synthesizing, verifying and transforming software and hardware. The automation of induction proof will improve the capability of mechanical assistants for software and hardware designers. This one day workshop will be organized around four sessions. Each session will focus on a distinct theme related to the automation of inductive proofs. The three pre-selected workshop themes are as follows: Application to formal methods, Higher-order inductive theorem proving, and Meeting the challenges - what has to be done in the future.

The interactions between finite model theory and computer science have expanded both in depth and in scope in recent years. Well-established connections, such as those between finite model theory and complexity theory and with relational databases, remain extremely fruitful. In addition, there are newer connections, such as those between finite model theory and verification, between finite model theory and linguistics, and between finite model theory and new database models (e.g. spatial and temporal databases). The goal of this one-day informal workshop is both to allow established researchers in the field of finite model theory to share contributions, and to introduce these new developments to a wide audience. The workshop will aim for invited talks of an expository nature, covering new developments and new applications; these talks will be aimed for a FLOC-wide audience. It will also seek contributions geared for those within the finite model theory community.

We solicit papers that focus on theoretical aspects of SPIN and model checking in general. Topics include, but are not necessarily restricted to: theory (automata, algorithms, reduction methods, logic, real-time, abstraction, modularity, hierarchy, refinement, implementation, fairness, symmetry relation, storage methods, caching methods, etc.); short tutorials or surveys on a topical subject related to SPIN model checking; analyses of shortcomings, possible extensions, benefits of existing tools; and empirical studies, measurements, tool comparisons, etc.