Workshops



ACCAT

Applied and Computational Category Theory

The originators of the ACCAT workshops are Hartmut Ehrig (Berlin) and Jochen Pfalzgraf (Salzburg) starting with the 1st ACCAT workshop at ETAPS 2006. 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. The workshop will consist of about 12 invited lectures where extended abstracts will be presented.

Contact: Jochen Pfalzgraf, (jochen.pfalzgraf [AT] sbg.ac.at) and Julia Padberg

URL:http://www.cosy.sbg.ac.at/~jpfalz/ETAPS-2010.html

ARSPA-WITS 2010

ARSPA is a series of workshops on Automated Reasoning for Security Protocol Analysis, bringing together researchers and practitioners from both the security and the formal methods communities, from academia and industry, who are working on developing and applying automated reasoning techniques and tools for the formal specification and analysis of security protocols.  WITS is the official annual 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.

In 2010, ARSPA and WITS will again join forces for the joint workshop ARSPA-WITS'10.  The aim of ARSPA-WITS'10 is to provide a forum for continued activity in different areas of computer security, bringing computer security researchers in closer contact with the ETAPS community and giving ETAPS attendees an opportunity to talk to experts in computer security, on the one hand, and contribute to bridging the gap between logical methods and computer security foundations, on the other.

Contact: Gavin Lowe, gavin.lowe [AT] comlab.ox.ac.uk and Alessandro Armando, (armando[AT]dist.unige.it)

URL: http://www.avantssar.eu/arspa-wits10/

Bytecode 2010

5th 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 Internet and mobile devices (smart-cards, phones, etc.) applications, 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 theoretical and practical aspects of semantics, verification, analysis, certification and transformation of bytecode.

Contact: David Pichardie, (david.pichardie [AT] inria.fr)

URL: http://bytecode2010.inria.fr/

CMCS 2010

Coalgebraic Methods in Computer Science

During the last few years, it has become increasingly clear that a great variety of state-based dynamical systems, like transition systems, automata, process calculi and class-based systems, can be captured uniformly as coalgebras. Coalgebra is developing into a field of its own interest presenting a deep mathematical foundation, a growing field of applications, and interactions with various other fields such as reactive and interactive system theory, object oriented and concurrent programming, formal system specification, modal logic, dynamical systems, control systems, category theory, algebra, analysis, etc. The aim of the workshop is to bring together researchers with a common interest in the theory of coalgebras and its applications.

Contact: Prof.dr. Jan Rutten, (cmcs10@cwi.nl)

URL: http://event.cwi.nl/cmcs10/

COCV 2010 (Canceled)

9th 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: Jens Knoop (knoop [AT] complang.tuwien.ac.at) and Wolf Zimmermann

URL:http://www.complang.tuwien.ac.at/cocv2010/

 

DCC 2010

Designing Correct Circuits

The In recent years, formal methods have been used increasingly in the verification of large-scale circuit designs, particularly in the microprocessor industry. Great progress has been made in adapting and scaling up methods developed in academia, and in developing new methods to solve real veri cation problems. Various themes emerged in the eld ranging from ways to compose design and veri cation to system level modelling. A variety of useful tools have been developed { theorem provers, model checkers and combinations of the two. Similarly, the use of higher-level hardware design languages, including functional ones, has been explored, and various approaches and solutions have appeared. Yet, more needs to be done. There are indications that we need to incorporate formal veri cation earlier in the design process, and this means thinking hard about our design and speci cation notations, and about how best to guide the veri cation process. We should probably exploit modern programming language technology, and we need to think about how to raise the level of abstraction at which we do veri cation. The aim of the workshop is to present the state of the art in hardware design and veri cation methods (from both an academic and an industrial viewpoint). Then, we hope to start a discussion on the question of what needs to be done next in research if we are to solve the huge problems facing both microprocessor manufacturers and the System on a Chip industry.

Contact: Joe Stoy, (stoy [AT] bluespec.com)

URL: http://www.comlab.ox.ac.uk/dcc2010

DICE 2010

Developments in Implicit Computational Complexity

Area of Implicit Computational Complexity (ICC) grew out from several proposals to use logic and formal methods to provide languages for complexity-bounded computation (e.g. Ptime, Logspace computation). It aims at studying the computational complexity of programs without referring to external measuring conditions or a particular machine model, but only by considering language restrictions or logical/computational principles entailing complexity properties. Several approaches have been explored for that purpose, like restrictions on primitive recursion and rami cation, rewriting systems, linear logic, types and lambda calculus, interpretations of functional and imperative programs. The workshop is intended to be a forum for researchers interested in ICC to present new results and discuss recent developments in this area.

Contact: Patrick Baillot, (patrick.baillot [AT] ens-lyon.fr)

URL: http://www.ens-lyon.fr/LIP/DICE2010/

FBTC

From Biology to Concurrency and back

As in its previous editions, the workshop aims at gathering researchers with special interest at the convergence of life and computer science, with particular focus on the application of techniques and tools from concurrency. We solicit the submission of unpublished results reporting on both modelling, analyzing, and validating biological behaviours using concurrency-inspired methods and platforms, and on bio-inspired models and tools for describing distributed interactions.

Contact: Emanuela Merelli, ( emanuela.merelli [AT] unicam.it ) and Paola Quaglia ( quaglia [AT] disi.unitn.it )

URL: http://www.disi.unitn.it/~fbtc2010/

FESCA 2010

7th International Workshop on Formal Engineering approaches to Software Components and Architectures

Component-based Component-based software design has received considerable attention in industry and academia in the past decade. In recent years, the growing need for trustworthy software systems and the increased relevance of systems reliability, performance, and scalability have stimulated the emergence of formal techniques and architecture modelling approaches for the specification and implementation of component-based software architectures. Both have to deal with an increasing complexity in software systems challenging analytical methods as well as modelling techniques. FESCA aims to address the open question of how formal methods can be applied effectively to these new contexts and challenges. FESCA is interested in both the development and application of formal methods in component-based development and tries to cross-fertilize their research and application.

Contact: Barbora Buhnova and Jens Happe ( fesca2010 [AT] easychair.org)

URL: http://sdq.ipd.uka.de/conferences_and_events/fesca10/

FOSS-AMA

Free and Open Source Software - for Accessible Mainstream Applications

The FOSS-AMA (Free and Open Source Software - for Accessible Mainstream Applications) workshop aims to bring together the most recent achievements and renowned experts in Open Source Community and Accessibility. 3rd generation access techniques and their potential for more accessible mainstream ICT for end-users and relevant toolkits for developers will be explored. Interactive demos will embellish the presentations sessions.

Contact: Karel Van Isacker (info@aegis-project)

URL: http://www.aegis-project.eu/index.php?option=com_content&view=article&id=53:aegis-organises-sattelite-event-at-etaps-2010-march-2728-2010-in-paphos-cyprus&catid=8:news-archive&Itemid=24

GaLoP V

Games for Logics and Programming Languages

GaLoP is an annual international workshop on game-semantic models for logics and programming languages and their applications. It is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tutorials as well as contributed papers.

Contact: Claudia Faggian (Claudia.Faggian@pps.jussieu.fr), Olivier Laurent (olivier.laurent@ens-lyon.fr)

URL: http://perso.ens-lyon.fr/olivier.laurent/galop10/

GT-VMT 2010

9th International Workshop on Graph Transformation and Visual Modeling Techniques

GT-VMT 2010 is the ninth 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. The aim of the workshop is to promote engineering approaches that provide effective sound tool support for visual modeling languages, enhancing formal reasoning at the semantic level (e.g., for model analysis, transformation, and consistency management) in different domains, such as UML, Petri nets, Graph Transformation or Business Process/Workflow Models. This year's workshop will have a special focus on visualisation, simulation, and verification of distributed systems.

Contact: Jochen M Kuester, (JKU [AT] zurich.ibm.com)

URL: http://www.cs.le.ac.uk/events/gtvmt10/

LDTA 2010

Tenth Workshop on Language Descriptions, Tools and Applications

The LDTA workshops bring together researchers interested in the field of formal language definitions and language technologies, with an emphasis on tools developed for or with these language definitions. Several specification formalisms like attribute grammars, action semantics, operational semantics, term rewriting, and algebraic approaches have been developed over the years. Of specific interest are the formal analysis of language specifications, and the automatic generation of language processing tools from such specifications. These tools typically perform some sort of program analysis, transformation, or generation. Also of interest are applications of such tools in domains including, but not limited to, modeling languages, re-engineering and re-factoring, aspect-oriented and domain-specific languages, XML processing, visualization and graph transformation.

Contact: Anthony Sloane, ( Anthony.Sloane [AT] mq.edu.au )

URL: http://www.ldta.info

MBT 2010

6th Workshop on Model-Based Testing

MBT 2010 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. The intent of this workshop is to bring together researchers and users using different kinds of models for testing and to discuss the state of the art in theory, applications, tools, and industrialization of model-based testing.

Contact: Bernd Finkbeiner, (finkbeiner [AT] cs.uni-sb.de)

URL: http://react.cs.uni-sb.de/mbt2010

PLACES 2010

Programming Language Approaches to Concurrency and Communication-cEntric Software

This workshop aims to offer a forum for researchers from different fields to exchange new ideas on one of the central challenges in programming in the near future: the development of programming methodologies and infrastructures where concurrency and communication are the norm rather than a marginal concern, be it for web services, sensor networks, multicore CPUs, business integration or high-performance computing. The development of effective programming methodologies for this new area demands exploration and understanding of a wide range of ideas and methodologies, from language primitives to concurrent data structures to types for linearity and communication to static analysis to runtime architectures. The workshop is dedicated to the focused exchange of new ideas on these topics in the quest for a unifying picture in this new area of programming methodologies.

Contact:Kohei Honda, kohei.honda.kh@googlemail.com

URL: http://places10.di.fc.ul.pt/

QAPL 2010

8th Workshop on Quantitative Aspects of Programming Languages

Quantitative aspects of computation refer to the use of physical quantities (time, bandwidth, etc.) as well as mathematical quantities (e.g. probabilities) for the characterisation of the behaviour and for determining the properties of systems. 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 the QAPL workshop series is to discuss the explicit use of time and probability and general quantities either directly in the model or as a tool for the analysis of systems.

Contact: Alessandra Di Pierro, (alessandra.dipierro [AT] univr.it)

URL: http://qav.comlab.ox.ac.uk/qapl10/

SafeCert (Canceled)

3rd Workshop on the Certification of Safety-Critical Software Controlled Systems

Certification of Safety-Critical Software Controlled Systems In many domains like transportation, power generation, medical technology, manufacturing and space exploration, statutory obligations traditionally require a formalized certification for the development of high assurance products. Formal methods are part of the standard recommendations, in particular for the higher safety integrity levels. However, experience and recent work show that certifiable development of high-assurance software needs a lot more than pure application of formal techniques and tools that are founded on a formal semantics and support in parts automated code generation, formal analysis, verification or error detection. The major question to be addressed in the workshop is how to embed formal methods and tools in a seamless design process which covers several development phases and which includes an efficient construction of a safety case for the product.

Contact: Michaela Huhn, (M.Huhn [AT] tu-bs.de)

URL: http://safecert10.offis.de/

WGT 2010

2nd Workshop on Generative Technologies

Generative programming is a recently emerged programming paradigm assisting the creation of flexible libraries, software development automation, and compile-time code transformation. The programming paradigm consists of numerous styles, including aspect-orientation, template metaprogramming, intentional programming, generic programming, and others. These programming styles are becoming everyday tools for today's programmers designing and implementing software ever growing in size and complexity. The purpose of the workshop is to provide a forum for researchers working in this area to discuss the state-of-the-art generative technologies and tools, and also exchange ideas about the future of the generative paradigm. Papers describing practical applications of generative styles, and new possible directions of the paradigm are expected.

Contact: Norbert Pataki, (patakino [AT] elte.hu)

URL: http://wgt2010.elte.hu/

WRLA 2010

8th International Workshop on Rewriting Logic and its Applications

Rewriting logic (RL) is a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication, and interaction. It can be used for specifying a wide range of systems and languages in various application fields. It also has good properties as a metalogical framework for representing logics. In recent years, several languages based on RL (ASF+SDF, CafeOBJ, ELAN, Maude) have been designed and implemented. The aim of the workshop is to bring together researchers with a common interest in RL and its applications, and to give them the opportunity to present their recent works, discuss future research directions, and exchange ideas.

Contact: Peter Ölveczky, (peterol [AT] ifi.uio.no)

URL: http://wrla10.ifi.uio.no/

Satellite Events Chairs

The satellite organisers can be contacted by sending e-mail to <etaps10_satellite_events@cs.ucy.ac.cy>.