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 (email@example.com)
This satellite event has been cancelled.
Contact: Ramesh Bharadwaj (firstname.lastname@example.org)
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 (email@example.com)
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 (firstname.lastname@example.org)
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
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'kcl.ac.uk)
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
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 (email@example.com)
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 (firstname.lastname@example.org)
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 (email@example.com)
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 (firstname.lastname@example.org)
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
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 (email@example.com)
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 (firstname.lastname@example.org)
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 (email@example.com)
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 (firstname.lastname@example.org)
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 (email@example.com)
Contact: Judith Bishop (firstname.lastname@example.org)
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 (email@example.com)
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 (firstname.lastname@example.org)
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 (http://www.dsi.unive.it/~focardi/)
ETAPS 2007 Satellite Events Co-chairs