AVIS'05 is a forum for researchers interested in the application of formal methods and tools for the automatic verification of large practical systems. Model checking is limited in scope for practical verification due to state explosion. However, we have recently 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 even be infinite. The intention of the AVIS series of workshops is to build a forum for exchanging ideas and experiences by bringing together theoreticians, tool builders, as well as practitioners interested in this promising area of research.
Contact: Ramesh Bharadwaj, ramesh@itd.nrl.navy.mil
URL: http://chacs.nrl.navy.mil/AVIS05
Model-based development yields the precondition for the efficient construction of reliable embedded systems. To make it constructive in industrial production processes, however, the management of the complex relationships of the models must be supported. Continuous engineering addresses the continuity of any software development and maintenance activities in that models and documents are connected that correspond to different design stages, levels of the system, variants of the same product, or members of the same product family etc. Continuity guarantees that invariants of the design are respected, dependencies can be detected, and the impact of planned changes can be determined. The workshop is a forum for the presentation and discussion of practical experiences, research results and ongoing activities in all areas of the continuous engineering of embedded systems.
Contact: Martin Grosse-Rhode, martin.grosse-rhode@isst.fraunhofer.de
URL: http://www.isst.fhg.de/~mgrosse/cees/index.htm
Game semantics has emerged as an innovative and successful paradigm in the field of semantics of logics and programming languages, leading to the development of the first syntax-independent fully-abstract models for a variety of programming languages. 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, 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'05 events and to become a major meeting point in the research area of Game Semantics and its applications.
Contact: Dan Ghica, Dan.Ghica@comlab.ox.ac.uk
URL: http://users.ox.ac.uk/%7Ecoml0074/galop.html
This workshop is part of a series that brings together international researchers to discuss the Grand Challenge Project on Dependable Systems Evolution. The long-term aim of the project is to produce a coherent software engineering tool-set based on formal principles, to aid in the development, deployment, and evolutio n of dependable systems; and to submit the tools to convincing large-scale evalu ation on a heterogeneous range of challenge codes. The purpose of this particular workshop is to bring together theory and programming language researchers to discuss long-term scientific challenges posed by software verification.
Contact: Jim Woodcock, Jim.Woodcock@cs.york.ac.uk
URL: http://www.dcs.qmul.ac.uk/~ohearn/DSE-Workshop/etaps05.html
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 as well as mathematical quantities. Such quantities play a central role in defining both the model of systems 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 such as time and probabilities either directly in the model or as a tool for the analysis of systems. In particular, the workshop focuses on: the design of probabilistic and real-time languages and the definition of semantical models for such languages; the discussion of methodologies for the analysis of probabilistic and timing properties; the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects; applications to safety-critical systems, communication protocols, asynchronous hardware.
Contact: Herbert Wiklicky, herbert@doc.ic.ac.uk
URL: http://www.doc.ic.ac.uk/~qapl05
This workshop will provide an avenue for work that extends traditional methods that derive from constructive logic for synthesizing complex software. After more than 30 years of research, program synthesis using constructive logic constitutes a mature field with an established theory and set of best practices. Recent years have seen an interest in providing analogous results to other logical systems and programming languages. This workshop will bring together researchers and practitioners to share ideas on the foundations, techniques, tools, and applications of constructive logic and its methods to automated software engineering technology.
Contact: Iman Poernomo, ihp@csse.monash.edu.au
URL: http://www.csse.monash.edu.au/clase
COCV is devoted to advances in theory and practice on the theoretical foundations and applications of approaches, technologies, and tools for compiler optimization and compiler verification and their mutual dependencies. It 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, but also programming language design and programming language semantics to exchange their latest findings. 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@complang.tuwien.ac.at
URL: http://www.complang.tuwien.ac.at/knoop/COCV2005/cocv2005.html
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 language technologies, with a special emphasis on tools developed for or with these language definitions. This active area of research involves the following basic approaches: Program analysis, transformation, and generation; Formal analysis of language properties; Automatic generation of language processing tools. Among others, the following application domains can benefit from advanced language technologies: Software component models and modeling languages; Re-engineering and re-factoring; Aspect-oriented programming; Domain-specific languages; XML processing; Visualization and graph transformation; Programming environments such as Eclipse, Rotor, SUN Java, etc. 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:Thomas Noll, Noll@cs.rwth-aachen.de
URL: http://www-i2.informatik.rwth-aachen.de/Events/LDTA2005/
SLAP is a workshop dedicated to synchronous languages. Such languages have emerged in the 80s as a new method to design real-time embedded critical systems. There exists now a strong interest for them in industry: Lustre, Esterel, and Signal are used with success to program real-time and safety critical applications, from nuclear power plant management layer to Airbus air flight control systems. The purpose of the SLAP workshop is to bring together researchers and practitioners who work in the field of reactive systems. The workshop topics are covering all these issues: synchronous model of computation, synchronous languages and programming formalisms, compiling techniques, formal verification, test and validation of programs, case-studies.
Contact: Florence Maraninchi, Florence.Maraninchi@imag.fr
URL: http://www-sop.inria.fr/cma/slap/slap2005.html
Computing technology has become ubiquitous, from global applications to miniscule embedded devices. Trust in computing is vital to help protect public safety, national security, and economic prosperity. A new area of research, known as global computing, has recently emerged that aims at defining new models of computation based on code and data mobility on networks with highly dynamic topologies, and that aims at providing infrastructures to support coordination and control of components originating from different, possibly untrusted, sources. Trustworthy Global Computing aims at guaranteeing safe and reliable network usage. The conference will analyze foundational aspects of global computing and security and deal with the issues of: resource usage; language-based security; theories, systems of trust, authentication; privacy, reliability, business integrity; access control; models of interaction, dynamic components management; programming language concepts, abstraction mechanisms; verification tools; new software principles to support "debugging".
Contact: Rocco De Nicola, denicola@dsi.unifi.it
URL: http://www.cs.unibo.it/~sangio/TGC05/
Bytecode, such as produced by Java and .NET compilers, is a topic of interest, both for industry and academia. The industrial interest stems from the fact that bytecode is used in critical environments, such as the Internet and smart cards. Moreover, an important characteristic for bytecode is that it is device-independent and allows dynamic loading of classes. For researchers that wish to apply formal methods to bytecode, this dynamic nature provides an extra challenge. In addition, also the unstructuredness of the code and the pervasive presence of the stack provide extra challenges for the analysis. 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: Fausto Spoto, fausto.spoto@univr.it
URL: http://www.sci.univr.it/~spoto/Bytecode05/
While formal verification has become part of the design process of digital circuits, its application to analog and mixed-signal design is only in its infancy. This is mainly due to the fact that the mathematical models for such circuits are very different from the discrete, finite-state transition systems that underly verification of digital systems. Such models are based on continuous dynamical systems governed by differential equations and their verification calls for different techniques, like those developed in the analysis of hybrid systems. This workshop intends to bring together practitioners in circuit design and in EDA tools with researchers in verification of discrete and hybrid systems in order to understand the problems faced by designers of analog circuits and to see what support can be provided by existing and new verification techniques.
Contact: Oded Maler, Oded.Maler@imag.fr
URL: http://www-verimag.imag.fr/~maler/FAC
The aim of this 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 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 growing need for safety-critical embedded software, this trend has been amplified. Formal methods have sometimes not kept up with the increasing complexity of software. For instance, a range of new middleware platforms have been developed in both enterprise and embedded systems industries. Often, engineers use semi-formal notations such as UML2 to model and organise components into architectures. FESCA aims to address the open question of how formal methods can be applied effectively to these new contexts.
Contact: Juliana Kuester-Filipe, jkfilipe@inf.ed.ac.uk
URL: http://www.csse.monash.edu.au/fesca/
The paradigm shift from algorithms to interactive computation is capturing the technology shift from mainframes to networks, number-crunching to embedded systems, and procedure-oriented to object-based computation. The interaction paradigm is at the core of most contemporary approaches to models of computation, artificial intelligence, software engineering, programming languages, information systems, and networking. This workshop provides the first opportunity for researchers in these fields to meet and exchange ideas on interactive computation. We solicit high-quality research papers that analyze the underpinnings of interaction, providing conceptual and formal models, describing domain-specific aspects and fe atures, and comparing different approaches, frameworks, and ontologies. The ultimate goal of the workshop is to promote the introduction of a unified conceptual and formal framework for modeling interaction.
Contact: Mirko Viroli, mviroli@deis.unibo.it
URL: http://www.cse.uconn.edu/cse/finco05/
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 and adapt components. The rational behind this trend is in the promise of reuse and hence to produce software by "plug & play" components which already exist or are produced by different external vendors. Components and software composition are considered to be a new way to overcome the remaining problems (e.g. reusability, complexity) still not solved by the object-oriented paradigm.
Contact: Thomas Gschwind, tom@infosys.tuwien.ac.at
URL: http://www.infosys.tuwien.ac.at/staff/tom/SC2005
The User Interfaces for Theorem Provers workshop series brings together researchers interested in designing, developing and evaluating interfaces for interactive proof systems, such as theorem provers, formal method tools, and other tools for manipulating and presenting mathematical formulas. While the reasoning capabilities of interactive proof systems have increased markedly in recent years, the system interfaces have often not enjoyed the same attention as the proof engines themselves. In many cases, interfaces remain basic and under-designed. This workshop provides a forum for all researchers interested in improving usability and human interaction of proof systems. We welcome participation and contributions from the theorem proving, formal methods and tools, and HCI communities, both to report on experience with existing systems, and to discuss new directions.
Contact: David Aspinall, da@inf.ed.ac.uk
URL: http://uitp05.inf.ed.ac.uk
Molecular biology has traditionally considered biological molecules as isolated entities or as components of simple systems. However these molecules participate in very complex networks in living systems, including: regulatory networks for gene expression; intracellular metabolic networks; and both intra- and intercellular communication networks. Recent progress in biology in high-throughput data-production technologies has given the prospect of a new approach, focussing on how components work together as a system. The CMSB workshop is intended to catalyze the convergence between modellers - theoretical computer scientists from fields such as language design, concurrency theory or program verification, mathematicians and physicists and biologists interested in such a systems-level understanding of cellular processes.
Contact: Gordon Plotkin, gdp@inf.ed.ac.uk
URL: http://homepages.inf.ed.ac.uk/v1bklin/cmsb05