Applied and Computational Category Theory

Category Theory is a well-known powerful mathematical modeling language with a wide area of applications in mathematics and computer science, including especially the semantical foundations of topics in software science and development. Since about 30 years there have been workshops including these topics. More recently, the ACCAT group established by Jochen Pfalzgraf at Linz and Salzburg has begun to study interesting applications of category theory in Geometry, Neurobiology, Cognitive Sciences, and Artificial Intelligence. It is the intention of this ACCAT workshop to bring together leading researchers in these areas with those in Software Science and Development in order to transfer categorical concepts and theories in both directions.

Contact: Ulrike Prange (


AVIS (cancelled)

Sixth International Workshop on Automated Verification of Infinite-State Systems

This satellite event has been cancelled.

AVIS is a forum for researchers interested in the application of formal methods for the automatic verification of large practical systems. Model checking, which has found wide application on hardware descriptions, does not scale to practical software systems due to state explosion. For such systems, theorem proving -- a process requiring manual effort and mathematical sophistication to use -- has so far been the only viable alternative.
More recently, hybrid techniques have been developed that combine the ease-of-use of model checkers with the power of theorem provers, yielding tools that are less sensitive to the size of the state space (which may be infinite.) AVIS provides a forum for those who are interested in this emerging area of research that has a bright future.

Contact: Ramesh Bharadwaj (



Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation

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: Fausto Spoto (



Sixth International Workshop on Compiler Optimization Meets Compiler Verification

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: Sabine Glesner (



Formal Foundations of Embedded Software and Component-Based Software Architectures

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.
Recent years has seen the emergence of formal and informal techniques and technologies for the specification and implementation of component-based software architectures. 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. 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 symbol'



Foundations of Interactive Computation

Since the 1960's, computation has become increasingly interactive. Concurrent, distributed, reactive, embedded, component-oriented, agent-oriented and service-oriented systems all fundamentally depend on interaction. However, a satisfactory formal foundation of interactive computation, analogous to one that recursive functions, Turing Machines, and lambda-calculus provide for algorithms, is still lacking. Furthermore, the implications of treating interaction as a first-class concept in the process of software design and construction remain to be fully understood.
Following the success of FInCo 2005, our goals are to work towards developing a unified conceptual and formal framework for understanding the principles of interaction, establishing language- and domain-independent models for it, and improving the development of software applications and systems through the application of interactive principles and models.

Contact: Dina Goldin (



Sixth International Workshop on Graph Transformation and Visual Modeling Techniques

GT-VMT 2007 is the sixth workshop of a series that serves as a forum for all researchers and practitioners interested in the use of graph-based notation, techniques and tools for the specification, modeling, validation, manipulation and verification of complex systems. Due to the variety of languages and methods used in different domains, the aim of the workshop 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, hence providing effective tool support at the semantic level (e.g., for model analysis, transformation, and consistency management). This year's workshop will have an additional focus on application of graph transformation and visual modeling techniques in engineering, biology, and medicine.

Contact: Karsten Ehrig (



Heap Analysis and Verification

Accurate and efficient expression, discovery, and verification of the structure of program heap memory is an active research area. Many problems remain open, and therefore many programs remain unverified. We are seeing advances however: Among these are exciting new techniques for analysis and verification of concurrently accessed heap memory, new techniques for interprocedural and modular analysis and verification, and great strides increasing the range of practically applicable analysis and verification techniques. The aim of this workshop is to bring together researchers to exchange and develop new ideas in all aspects of formal analysis and verification for heaps. Submissions are invited from across the full spectrum of basic theoretical work through to applied practical work.

Contact: Josh Berdine (



Hardware design using Functional Languages

More abstract representations and verification techniques are needed to keep up with the ever-increasing complexity of modern hardware designs. We face challenging research problems, many of them related to language design and to ways of modelling circuits at various levels of abstraction.
This workshop will bring together researchers in modern functional languages, hardware description languages, high-level modelling and validation, and formal design environments. It aims to present the state of the art, and to spark debate about how to proceed.
To achieve the necessary breakthroughs, we must ensure that academics and industrial researchers continue to work together to solve the real challenge of hardware design and verification. A major aim of this workshop is to open the necessary communication channels.

Contact: Andy Martin (



Seventh Workshop on Language Descriptions, Tools and Applications

The LDTA workshops bring together academic and industrial researchers interested in the field of formal language definitions and language technologies, with an emphasis on tools developed for or with these language definitions. This active research area includes basic approaches such as the analysis, transformation, and generation of programs, the formal analysis of language properties, and the automatic generation of language processing tools.
Several specification formalisms like attribute grammars, action semantics, operational semantics, and algebraic approaches have been developed over the years. A goal of LDTA is to increase the use of such formalisms through demonstrations of their practical utility in, among others, the following application domains: component models and modeling languages, re-engineering and re-factoring, aspect-oriented and domain-specific languages, XML processing, visualization and graph transformation, and programming environments, such as Eclipse.

Contact: Eric Van Wyk (



3rd Workshop on Model Based Testing

The workshop is devoted to model-based testing of both software and hardware. Model-based testing uses models that describe the behavior 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 (



4th International Workshop on Model-based Methodologies for Pervasive and Embedded Software

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 computer-based systems, and more specifically, pervasive and embedded software.

Contact: Joćo M. Fernandes (



Foundations and Techniques for Open Source Software Certification

The aim of this workshop is to bring together researchers from academia and industry who are interested in developing techniques for the quality assessment of Open Source Software (OSS), leading to the definition of a complete certification process.
The workshop will focus on formal methods and model-based techniques, emphasising on those aspects which are specific to OSS, such as unconventional development, rapid evolution of the code, and huge amount of legacy code.
Contributions to the workshop are expected to present foundations, methods, tools and case studies that integrate techniques from different areas such as certification, security, reverse engineering, and formal modeling and verification, in order to overcome the challenges in the quality assessment of OSS.

Contact: Luis Barbosa (



5th Workshop on Quantitative Aspects of Programming Languages

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 (e.g. time, bandwidth) as well as mathematical quantities (e.g. probabilities) which play a central role in defining models (architectures, protocols, languages, etc.) and methodologies for analysis and verification.
The aim of this workshop is to discuss the explicit role of real-time aspects, probabilities, resource consumption, performance parameters, etc. in the design as well the analysis of such systems. The topics covered are transversal to all areas of Computer Science including Languages, Protocols, Architectures, Security, Semantics, Analysis, etc. Particular relevance will be given to the emerging areas of Quantum Computation and Bioinformatics.

Contact: Alessandro Aldini and Franck van Breugel (



Workshop on Software Composition

The goal of SC 2007 is to develop a better understanding of how we build and maintain large software systems, and thereby to build the body of knowledge and experience in software composition. The sixth SC symposium will bring together the research and industrial communities to address the challenges of the component-based approach to software development. Suggested topics of interess related to component systems include:

Contact: Judith Bishop (



Model-driven High-level Programming of Embedded Systems

SLA++P is dedicated to synchronous languages and the model-driven high-level programming of reactive and embedded systems. Firmly grounded in clean mathematical semantics, synchronous languages are receiving increasing attention in industry ever since they emerged in the 80s. Lustre, Esterel, Signal are now widely and successfully used to program real-time and safety critical applications of commercial scale. At the same time, model-based programming is making its way in other fields of software engineering, often involving cycle-based synchronous paradigms. SLA++P extends the former SLAP workshop series on Synchronous Languages, Applications, and Programming but is not limited to synchronous approaches. It is open to other engineering design techniques with strong semantical foundations to go from high-level description to provable executable code.

Contact: Michael Mendler (



4th International Workshop on Computing with Terms and Graphs

The advantage of computing with graphs rather than terms is that common subexpressions can be shared, improving the efficiency of computations in space and time. Sharing is ubiquitous in implementations of programming languages: many functional, logic, object-oriented and concurrent calculi are implemented using term graphs. Research in term and graph rewriting ranges from theoretical questions to practical implementation issues. Different research areas include: the modelling of first- and higher-order term rewriting by (acyclic or cyclic) graph rewriting, the use of graphical frameworks such as interaction nets and sharing graphs (optimal reduction), rewrite calculi for the semantics and analysis of functional programs, graph reduction implementations of programming languages, graphical calculi modelling concurrent and mobile computations, object-oriented systems, graphs as a model of biological or chemical abstract machines, and automated reasoning and symbolic computation systems working on shared structures.

Contact: Ian Mackie (



7th International Workshop on Issues in the Theory of Security

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. The members of WG hold their annual workshop as an open event to which all researchers working on the theory of computer security are invited. This is the seventh meeting of the series, and is organized in cooperation with ACM SIGPLAN (to be confirmed) and the working group FoMSESS of the German Computer Society (GI). There will be proceedings published as ``Issues in the Theory of Security““.

Contact: Riccardo Focardi (


Luis Barbosa
Joost Visser
ETAPS 2007 Satellite Events Co-chairs,

Valid HTML 4.01!