ETAPS 2015: 11-18 April 2015, London, UK
Sunday, 12 April 2015
The area of Implicit Computational Complexity (ICC) has grown from several proposals for using logic and formal methods to provide languages for complexity-bounded computation (e.g. PTIME, LOGSPACE computation). Its aim is to study computational complexity without reference to external measuring conditions or particular machine models, but only in terms of language restrictions or logical/computational principles implying complexity properties.
This workshop focuses on ICC methods related to programs. Traditionally, in this approach one relates complexity classes to restrictions on programming paradigms (functional programs, lambda calculi, rewriting systems), such as ramified recurrence, weak polymorphic types, linear logic and linear types, and interpretative measures. This year we also aim at enlarge the scope of DICE to other research areas loosely related to ICC.
The workshop will be open to contributions on various aspects of ICC including (but not exclusively):
Organiser: Marco Gaboardi (PC chair) (
Authors are invited to submit an extended abstract of up to 5 pages.
Submission: 30 January 2015Notification: 16 February 2015
We will have an open call for paper for a journal special issue after the workshop - joint with DICE'14.
The aim of the FESCA workshop is to bring together junior researchers from formal methods, software engineering, and industry interested in the development and application of formal modelling approaches as well as associated analysis and reasoning techniques with practical benefits for software engineering.
In recent years, the growing importance of functional correctness and the increased relevance of system quality properties (e.g. performance, reliability, security) have stimulated the emergence of analytical and modelling techniques for the design and development of software systems. With the increasing complexity of today's software systems, FESCA aims at addressing two research questions: (1) what role the software architecture can play in systematic addressing of the analytical and modelling challenges, and (2) how formal and semi-formal techniques can be applied effectively to make the issues easier to address automatically, with lower human intervention.
We encourage not only mature research results, submissions presenting innovative ideas and early results of junior researchers are also of a particular interest.
Three kinds of submissions are solicited:
* regular papers (up to 15 pages) presenting original and unpublished work related to the workshop topics,
* position papers (up to 10 pages) presenting ideas and directions of interesting ongoing and yet unpublished research related to the workshop topics, and
* tool demonstration papers (up to 8 pages) presenting and highlighting the distinguishing features of a topic-related tool (co-developed by the authors).
The papers should be written in English, follow the EPTCS style, and respect the page limit. Papers are to be submitted via the EasyChair conference system, and need to be registered before submission (authors, title, abstract, keywords). All accepted papers are required to be presented at the workshop by one of the authors. Tool demonstration and position papers are required to state "Tool demonstration paper/Position paper" as a subtitle of the publication.
Final versions of accepted regular and position papers will be published in a volume of the Electronic Proceedings in Theoretical Computer Science (EPTCS). The tool demonstration papers will not appear in the EPTCS proceedings, but will be included in the electronic pre-proceedings (distributed at the workshop) and made available on the workshop website.
Paper registration: 10 December 2014Submission: 17 December 2014Notification: 26 January 2015Camera-ready: 16 February 2015
Saturday, 11 April 2015
Software product line engineering (SPLE) aims to develop a family of systems through systematic, large-scale reuse in order to reduce time-to-market and costs and to increase product quality. Formal methods and analyses offer promising techniques towards realizing these goals. While some analysis approaches (e.g., for feature modelling and variant management) and formal methods (e.g., BDDs, CSPs, SAT solvers, model checkers and formal semantics of variability models) have been applied to SPLE, a considerable potential remains to be exploited. This workshop brings together researchers and practitioners interested in raising the efficiency and the effectiveness of SPLE by applying innovative analysis approaches and formal methods. Participants will be invited to review the state of the art and practice in their respective fields, identify further promising application areas, report practical requirements and constraints from real-world product lines, discuss drawbacks and complements of various approaches, or present new ideas and results.
Topics of interest include, but are not limited to:
Organisers: Joanne Atlee, U. Waterloo, Canada (Stefania Gnesi, ISTI/CNR, Pisa, Italy (
Submission: 30 January 2015Notification: 27 February 2015Camera-ready version: 13 March 2015
Saturday, 11 April 2014
The FOPARA workshop will serve as a forum for presenting original research results that are rel- evant to the analysis of resource (e.g. time, space, energy) consumption by computer programs. The workshop aims to bring together the researchers that work on foundational issues with the researchers that focus more on practical results. Therefore, both theoretical and practical con- tributions are encouraged. We also encourage papers that combine theory and practice. The following list of topics is non-exhaustive:
Organisers: Marko van Eekelen, Radboud University Nijmegen and Open University of the Netherlands (
FOPARA 2015 is a two-phase workshop. All participants are invited to submit a draft paper describing the work to be presented at the workshop. These submissions will be screened by the program committee chair to make sure they are within the scope of FOPARA and will appear in the informal pre-proceedings at the workshop. Submissions appearing in the draft proceedings are not peer-reviewed publications.
After the workshop, authors will be given the opportunity to incorporate the feedback from discussions at the workshop and will be invited to submit a revised full article for the formal review process. These revised submissions will be reviewed by the program committee using prevailing academic standards to select the best articles that will appear in the formal proceedings. The papers selected after the reviewing process will be published as a volume of the Springer LNCS series. The 2013 FOPARA LNCS proceedings volume is still in preparation. The 2009, 2011, 2013 FOPARA proceeding are published as LNCS Volumes 6324, 7177, 8552 (see e.g. DBLP: http://www.informatik.uni-trier.de/ ley/db/conf/fopara/index.html). LNCS is also the expected publication venue for Fopara 2015.
Paper submission: 23 January 2015 (via Easychair)Notification of acceptance: 16 February 2015Informal pre-proceedings version due: 2 March 2015Submission for formal peer-reviewed post proceedings: 29 May 2015 Notification (Paper): 10 July 2015Camera Ready: 4 September 2015
11-12 April 2015
Game semantics has emerged as a new and successful paradigm in the field of semantics of logics and programming languages. Game semantics made its breakthrough in computer science in the early 90s, providing an innovative set of methods and techniques for the analysis of logical systems. Subsequently, game-semantic techniques led to the development of the first syntax-independent fully-abstract models for a variety of programming languages, ranging from the purely functional to languages with non-functional features such as control, references or concurrency. 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 to semantic analysis, an algorithmic approach to game semantics has recently been developed, with a view to applications in computer assisted verification and program analysis. The workshop provides an opportunity for interaction with other Etaps events and is a major meeting point in the research area of Game Semantics and its applications.
Organiser: Dan Ghica (
Submission: 25 January 2015Notification: 10 February 2015
GaM seeks to attract and stimulate research on the techniques for graph analysis, inspection and transformation, on a general level rather than in any specific domain. Thus, the concept of a graph (in its many guises) is central; contributions should address scenarios for the use of graphs in a modelling context that potentially transcend specific settings and can be applied across domains. Good, well-known examples of such techniques are model checking and graph transformation; but we welcome contributions on any of the following (non-exhaustive) list of topics:
Submission: The workshop seeks submissions of three kinds:
All contributions should be submitted through EasyChair via this link.
Submission: 16 January 2015Notification: 13 February 2015Final manuscript: 13 March 2015
Saturday, 18 April 2015
This workshop is intended to be a less formal counterpart to the Principles of Security and Trust (POST) conference at ETAPS, and with an emphasis on "hot topics", both of security and of its theoretical foundations and analysis.
Like POST, the themes are
Submissions about new and emerging topics (for example, those that have not appeared prominently in conferences and workshops until now) are particularly encouraged. Submissions of preliminary, tentative work are also encouraged. There is no page limit, but the length of your submission should be appropriate to its content. There will be no formal proceedings. Inclusion in informal proceedings is optional.
This workshop is organised by IFIP WG 1.7: Theoretical Foundations of Security Analysis and Design.
Organiser: Luca Vigano (
Submission: 5 January 2015Notification: 6 February 2015Final versions for informal proceedings (optional): 15 February 2015
MBT 2015 is devoted to model-based testing of both software and hardware, and new trends in fusion of testing with other model-based verification technologies.
Model-based testing uses models that describe the behavior of the system under consideration to guide 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: testing with such models allows measuring the degree of the product's conformance with the model. The intent of this workshop is to bring together researchers and practitioners who use different kinds of models for testing to discuss the state of the art in theory, applications, tools, and industrialization of MBT.
Applications today are built using numerous interacting services; soon off-the-shelf CPUs will host thousands of cores, and sensor networks will be composed from a large number of processing units. Many applications need to make effective use of thousands of computing nodes. At some level of granularity, computation in such systems is inherently concurrent and communication-centred.
To exploit and harness the richness of this computing environment, designers and programmers will utilise a rich variety of programming paradigms, depending on the shape of the data and control flow. Plausible candidates for such paradigms include structured imperative concurrent programming, stream-based programming, concurrent functions with asynchronous message passing, higher-order types for events, and the use of types for communications and data structures (such as session types and linear types), to name but a few. Combinations of these abstractions will be used even in a single application, and the runtime environment needs to ensure seamless execution without relying on differences in available resources such as the number of cores.
The development of effective programming methodologies for the coming computing paradigm demands exploration and understanding of a wide variety of ideas and techniques. This workshop aims to offer a forum where researchers from different fields exchange new ideas on one of the central challenges for programming in the near future, the development of programming methodologies and infrastructures where concurrency and distribution are the norm rather than a marginal concern.
Submission: Friday 19th December 2014Notification: Friday 23rd January 2015Publication: post-proceedings in EPTCS, submissions approx. end May 2015
11 - 12 April 2015
Quantitative aspects of computation are important and sometimes essential in characterising the behavior and determining the properties of systems. They are related to the use of physical quantities (storage space, time, bandwidth, etc.) as well as mathematical quantities (e.g. probability and measures for reliability, security and trust). 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 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:
Organisers: Nathalie Bertrand (Mirco Tribastone (
The proceedings will appear in EPTCS.
Submission: 14 December 2014Notification: 9 February 2015
SynCoP aims at bringing together researchers working on verification and parameter synthesis for systems with discrete or continuous parameters, in which the parameters influence the behavior of the system in ways that are complex and difficult to predict. Such problems may arise for real-time, hybrid or probabilistic systems in a large variety of application domains. The parameters can be continuous (e.g., timing, probabilities, costs) or discrete (e.g., number of processes). The goal can be to identify suitable parameters to achieve desired behavior, or to verify the behavior for a given range of parameter values.
The scientific subject of the workshop covers (but is not limited to) the following areas:
Organisers: Étenne André (Goran Frehse (
We welcome submissions of either 12 pages (regular papers) or 4 pages (tool papers). Publication in the OASIcs series (free and open access).
Submission (abstract): 12 January 2015 AoESubmission (paper): 19 January 2015 AoENotification: 27 February 2015
Differential privacy is a promising approach to the privacy-preserving release of data: it offers a strong guaranteed bound on the increase in harm that a user incurs as a result of participating in a differentially private data analysis. Several mechanisms and software tools have been developed to ensure differential privacy for a wide range of data analysis tasks, such as combinatorial optimization, machine learning, answering distributed queries, etc.
Researchers in differential privacy come from several area of computer science as algorithms, programming languages, security, databases, machine learning, as well as from several areas of statistics and data analysis. The workshop is intended to be an occasion for researchers from these different research areas to discuss the recent developments in the theory and practice of differential privacy.
Specific topics of interest for the workshop include (but are not limited to):
Authors are invited to submit a short abstract (4-5 pages maximum) of their work.
Submission: 23 January 2015Notification: 23 February 2015
We will have a journal special issue after the workshop
Recently, tree automata and transducers have been combined and applied to various areas in computer science, including rewrite systems, static analysis of software, program transformation, XML document processing, and computational linguistics. This workshop aims to provide an opportunity for researchers from different areas to exchange ideas on the theory and practice of tree automata and tree transducers. The topics of the workshop include, but are not limited to:
Organiser: Emmanuel Filiot (
Extended abstracts of at most 6 pages are solicited. The work may be in a preliminary stage, or may be a short version of recently published articles or papers submitted elsewhere. Accepted papers will be made available electronically before the workshop. It is planned to publish original papers in formal post-workshop proceedings (TBA soon).
Submission: 9 January 2015Notification: 10 February 2015
VerifyThis is the successor of the program verification competitions held at FoVeOOS2011, FM2012 and the Dagstuhl seminar on Evaluating Software Verification Systems: Benchmarks and Competitions.
Its aims are:
The competition will offer a number of challenges presented in natural language. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification.
There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will focus on the input-output behavior of programs, yet it is at the discretion of participants to treat only aspects of requirements. Solutions will be judged for correctness, completeness, degree of automation, and elegance.
The aim of the workshop is to bring together researchers working in the fields of Program Verification and Program Transformation. There is a great potential for beneficial interactions between these two fields because:
(i) methods and tools developed in the field of Program Transformation such as partial evaluation, fold/unfold transformations, and supercompilation, have all been applied with success in the field of the verification of infinite state systems and parameterized systems, and
(ii) model checking, abstract interpretation, SAT and SMT solving and automated theorem proving have been used to enhance program transformation techniques. Moreover, the formal certification of program transformation tools, such as refactoring tools and compilers, has recently attracted considerable interest and posed major challenges.
The workshop will provide a forum where researchers from the Verification and Transformation fields may exchange ideas and foster new developments.
Abstract submission: 16 January 2015Paper submission: 6 February 2015Notification: 3 March 2015Camera-ready version: 11 March 2015
Sunday 12 April 2015
Modern programming languages provide sophisticated control mechanisms, commonly referred to as control operators which are widely used to realize a variety of applications. Since we cannot escape control features, it becomes a challenge to provide them with sound reasoning principles. There is an active research on understanding, representing, and reasoning about elaborated non-local control structures, in particular in declarative programming languages such as functional and logic languages. Ideas and results from this area have impact in many other fields of computer science, like concurrent systems, proof theory, proof mining, web programming and linguistics. The focus of the workshop is on the interplay between syntax and semantics, the question of what a program using control operators means and how it acts.
The study of control operators is a prominent issue in the theory and practice of functional programming languages with a respectable tradition since the 80's which has been rediscovered along the years in several fields of computer science, fostering applications and rising new challenges. In particular the theme of embedding nonfunctional features in purely functional languages seems a good way to reconcile abstraction and methodologically well understood concepts with expressiveness w.r.t. concurrent systems and communication centered programming which are of major interest at present.
A preliminary list of topics includes (but it is not limited to):
This workshop opens a dialogue between researchers and industry experts in programming languages. Topics include all aspects of developer productivity at scale, from programming language design and implementation to software engineering, including static and dynamic analysis and testing. Industrial impact on software reliability due to modern theorem proving technology is also among the topics.
The goal of this event is to foster collaboration between academia and industry on topics of importance for today's software development practices.
Format: invited talks and a panel.
Sunday 12 and Saturday 18 April
(only for those who registered for the SAT dinner)
The SAT dinners will take place in the function suite of the Dickens Inn. The Dickens Inn is a restyled and reconstructed wooden warehouse building thought to have housed tea or to have been owned by a local brewery. It certainly existed at the turn of the 18th century and may well have been born in the 1700’s.
Address: The Dickens Inn, St Katharine Docks, 2 Marble Quay, London E1W 1UH
Directions: From Queen Mary one should take the District line from Stepney Green Underground Station to Tower Hill Station. From there it is a short 8 minutes walk to the restaurant as shown on the map below:
We have 53 guests and no members online