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 (uprange@cs.tu-berlin.de)
URL: http://tfs.cs.tu-berlin.de/workshops/accat2007/
This satellite event has been cancelled.
Contact: Ramesh Bharadwaj (ramesh@itd.nrl.navy.mil)
URL: http://chacs.nrl.navy.mil/AVIS07
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 (fausto.spoto@univr.it)
URL: http://www.sci.univr.it/~spoto/Bytecode07/
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 (glesner@cs.tu-berlin.de)
URL: http://pes.cs.tu-berlin.de/cocv2007/
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'kcl.ac.uk)
URL: http://palab.dcs.kcl.ac.uk/fesca/
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 (finco07@cs.brown.edu)
URL: http://www.cs.brown.edu/sites/finco07/
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 (karsten@mcs.le.ac.uk)
URL: http://www.cs.le.ac.uk/events/GTVMT07/
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 (jjb@microsoft.com)
URL: http://www.cs.tau.ac.il/~msagiv/hav.html
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 (hfl07@hflworkshop.org)
URL: http://hfl07.hflworkshop.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
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 (evw@cs.umn.edu)
URL: http://www.di.uminho.pt/ldta07
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 (finkbeiner@cs.uni-sb.de)
URL: http://react.cs.uni-sb.de/mbt2007/
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 (mompes@di.uminho.pt)
URL: http://www.di.uminho.pt/mompes
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 (opencert07@di.uminho.pt)
URL: http://opencert.iist.unu.edu/
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 (qapl07@cse.yorku.ca)
URL: http://www.cse.yorku.ca/qapl07
Contact: Judith Bishop (jbishop@cs.up.ac.za)
URL: http://ssel.vub.ac.be/sc2007
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 (michael.mendler@wiai.uni-bamberg.de)
URL: http://web.uni-bamberg.de/wiai/gdi/SLAP07/
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 (ian.mackie@kcl.ac.uk)
URL: http://www.termgraph.org.uk
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/)
URL: http://www.dsi.unive.it/IFIPWG1_7/wits/2007
http://www.di.uminho.pt/etaps07
etaps07@di.uminho.pt
Luis Barbosa
Joost Visser
ETAPS 2007 Satellite Events Co-chairs
lsb@di.uminho.pt, joost.visser@di.uminho.pt