AVIS'04 - Third International Workshop on Automatic Verification of Infinite-State Systems
AVIS is for researchers, and practitioners interested in the application of formal verification technology for large practical systems. The recent emergence of hybrid techniques that combine the ease-of-use of model checking with the power of theorem proving affords users with full automation and scalability. This workshop is a forum for exchanging ideas in this promising area of research.
Contact: Dr. Ramesh Bharadwaj (email@example.com)
The aim of the workshop is to bring together researchers with a common interest in the theory of coalgebras and its applications. The topics of the workshop include, but are not limited to:
Contact: Jiri Adamek (J.Adamek@tu-bs.de)
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.
Contact: Jens Knoop (Jens.Knoop@FernUni-Hagen.De)
The concept of constraints makes it possible to model and specify problems with uncertain, incomplete information and to solve combinatorial problems. Constraint-based programming languages enjoy elegant theoretical properties, conceptual simplicity, and practical success.
The aim of the workshop is to provide opportunity for interactions with the other ETAPS'04 events and to be a major meeting point in the research area inbetween the Constraint Programming conferences, which are held each autumn.
Taking inspiration from the CP 02 workshop CFV, we will have a special track dedicated to "formal verification", since there has been an increasing interest for the application of constraint programming and constraint solving technology to the formal verification of hardware and software systems.
Contact: Thom Fruehwirth (Thom.Fruehwirth@informatik.uni-ulm.de)
The 2004 DCC workshop will 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 in formally-based hardware verification and provided a venue for debate about how more effective design and verification methods can be developed.
Contact: Mary Sheeran (firstname.lastname@example.org) and Tom Melham (Tom.Melham@comlab.ox.ac.uk)
The Eclipse platform (http://www.eclipse.org) is designed for building integrated development environments (IDEs) for object-oriented application development. The eclipse Technology eXchange workshop seeks original papers that describe the use of the Eclipse code base for teaching or research projects, or for projects that actively promote the growth of Eclipse user communities. Accepted papers will be presented at the workshop. Submitted papers are encouraged to explore potential new uses of Eclipse and improved usability of the core Eclipse technology. Both tool demonstrations and regular research papers are welcomed.
Contact: Brian Barry (email@example.com) or Oege de
The aim of the workshop is to bring together researchers from academia and industry interested in formal modelling approaches as well as associated analysis and reasoning techniques with practical benefits for dependable and/or safety-critical embedded software and component-based software architectures.
Contact: Juliana Küster Filipe (firstname.lastname@example.org)
Many studies of complex software systems have shown that unanticipated changes of requirements account for most technical problems and related costs of software maintenance. Therefore, support for unanticipated software evolution becomes a key issue for software development tools and techniques, programming languages, component models and runtime infrastructures.
This two-day workshop will address formal techniques that help to perform, analyse, measure and manage unanticipated static and dynamic evolution of software. It is a successor of the second workshop on Unanticipated Software Evolution (at ETAPS 2003) and the first workshop on Formal Foundations of Software Evolution (at CSMR 2001).
Contact: Tom Mens, (email@example.com)
Effective applications of visual modelling techniques require tool support at a semantic level, e.g., for model analysis, transformation, and consistency management. Due to the variety of languages and methods used in different domains, an engineering approach is required which allows for the generation of such tools from high-level specifications.
Graph transformations provide means to specify, at a conceptual level, complex operations on diagrams. Complementing this by techniques like meta modelling, compiler technology, logic and algebra, etc., the workshop aims to bring together researchers from different communities to discuss their respective contributions to the above challenges.
The workshop is an event of the European Research Training Network SegraVis.
Contact: Reiko Heckel
Modern software development processes have to deal with a variety of modelling, specification, and description techniques, incorperating also techniques from engineering sciences. These have to be integrated, i.e., methods and techniques have to be provided to compare different specifications, to establish semantic correspondences, to check their consistency, and to define the informal or formal semantics of a collection of specifications.
Contact: Hartmut Ehrig (firstname.lastname@example.org) and Gunnar Schroeter (email@example.com)
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.
Contact: Joao Saraiva (firstname.lastname@example.org)
Model-based testing has recently gained attention with the popularization of models in software/hardware design and development. Test case generation with these models allows one to measure to what degree a product faithfully implements a given model.
The intent of this workshop is to discuss the state of art in theory, application, tools and industrialization of model-based testing.
Contact: Alexander Kossatchev (email@example.com)
Quantitative aspects of computation are important and sometimes essential in characterising the behaviour and determining the properties of systems. They are related to the use of physical quantities (storage space, time, bandwidth, etc.) as well as mathematical quantities (e.g. probability and measures for reliability, risk and trust). 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 this workshop is to discuss the explicit use of quantitative information (e.g. time and probabilities) either directly in the model or as a tool for the analysis of systems.
Contact: Alessandra Di Pierro
The objective is to debate how to monitor and analyze the execution of programs, also phrased as dynamic program analysis. This covers such subjects as specification based program monitoring, where execution traces are verified against formally stated specifications; multi-threading analysis such as for example data race and deadlock analysis; program instrumentation; and program guidance, either for fault-protection, or to expose errors during test.
Contact: Klaus Havelund (firstname.lastname@example.org)
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, software composition is considered to be a new way to overcome the remaining problems still not solved by the object-oriented paradigm.
Contact: Uwe Assmann (email@example.com)
Engineering design languages are at the heart of today's tools employed for developing embedded systems. This workshop provides an opportunity for academic and industrial experts in concurrency theory, tool development, and formal validation to present novel and ongoing research on the semantic foundations of engineering design languages, on case studies and design tools, as well as on semantic issues in simulation, validation and code generation.
Contact: Michael Mendler (firstname.lastname@example.org)
Synchronous languages have been introduced in the 80s to program reactive systems. Such systems are characterised by their continuous reaction to their environment, at a speed determined by the latter. Synchronous languages have recently seen a tremendous interest from leading companies developing automatic control software for critical applications (Schneider Electric, Aerospatiale, Dassault Aviation, Snecma, ST Microelectronics, Texas Instrument, Motorola, Intel...). The key advantage pointed by these companies is that the synchronous approach has a rigorous mathematical semantics which allows the programmers to develop critical software faster and better.
Indeed, the semantics of the languages is used as a formal model upon which all the programming environments are defined. The compilation involves the construction of these formal models, and their analysis for static properties, their optimisation, the synthesis of executable sequential implementations, the automated distribution of programs. It can also build a model of the dynamical behaviours, in the form of a transition system, upon which are based the analysis of dynamical properties, e.g., through model-checking based verification, or discrete controller synthesis.
After SLAP 2002 in Grenoble and SLAP 2003 in Porto, SLAP 2004 will be the third workshop devoted entirely to synchronous languages, applications, and programming. Its purpose is to bring together researchers and practitioners who work in the field of reactive systems. The workshop topics cover the following issues:
Contact: Florence Maraninchi (Florence.Maraninchi@imag.fr)
The SPIN workshop brings together practitionars and researchers interested in the use of model-checking based techniques for the validation of software artifacts. The aimed contributions refer to techniques based on explicit representations of state spaces, as implemented in SPIN and other tools. Topics include theoretical and algorithmic foundations and tools, model derivation from code and code derivation from models, techniques for dealing with large and infinite state spaces, timing and applications.
Contact: Susanne Graf, Verimag/CNRS (email@example.com)
Component based systems are increasingly used in software development. The characteristics of these systems 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.
Contact: Mauro Pezzè (firstname.lastname@example.org)
The algebraic approach to system specification encompasses many aspects of the formal design of software systems. Originally born as a formal method for reasoning about abstract data types, it now covers new specification frameworks and programming paradigms (such as object-oriented, aspect-oriented, agent-oriented, logic and higher-order functional programming) as well as a wide range of application areas (including information systems, concurrent, distributed and mobile systems). The topics of the workshop include, but are not limited to: formal methods for system development, including validation, verification, refinement and redesign; specification languages and methods; systems and techniques for reasoning about specifications; specification development systems (concepts and tools); methods and techniques for concurrent, distributed and mobile systems; algebraic and co-algebraic foundations
Contact: Peter Mosses (email@example.com)
WITS is the offical workshop organised 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.
Contact: Peter Y A Ryan (firstname.lastname@example.org)
Rewriting logic (RL) is a natural model of computation and an expressive semantic framework used to specify a wide range of systems, languages, and logics. Several languages based on RL have been designed and implemented (CafeOBJ, ELAN, Maude). The aim of WRLA 2004 is to give researchers the opportunity to present their recent work on the following topics: foundations and models of RL, languages based on RL, RL as a logical and semantic framework, extensions of RL, and comparisons of RL with other formalisms.
Contact: Narciso Marti-Oliet (email@example.com)