Markus Roggenbach | 14 Apr 12:46 2014

CFP: Model-based design and analysis of cyber-physical systems - SPES_XT Summer School at AVoCS'14

(Apologies if you receive this multiple times).


    Model-based design and analysis of cyber-physical systems
           SPES_XT Summer School at AVoCS'14
                 Twente, The Netherlands
                    Sept. 17-23, 2014

Today's challenges in the development of embedded and cyber-physical
systems are mainly caused by the ever-increasing complexity of the
software. Model-based design and analysis has a high potential to
overcome these challenges. SPES_XT (Software Platform Embedded
Systems) is a large German endeavour to build a consistent, coherent
model-based design methodology for complex embedded and cyber-physical
systems. The aim of AVoCS (International Workshop on Automated
Verification of Critical Systems) is to further research on tools and
techniques for the verification of critical systems. The SPES_XT
Summer School at AVoCS'14 will present results and experiences from
the SPES_XT project, as well as research approaches established at
AVoCS. It will provide a concise introduction to the state-of-the-art,
as well as new approaches and research questions. Attendants will gain
an intimate understanding of a consistent system development process
for complex embedded and cyber-physical systems over different
application domains (e.g. automation, automotive, avionic, rail).

The school addresses young researchers as well as young professionals
from industry. It will be held immediately prior to AVoCS 2014.

(Continue reading)

Yuan-Fang Li | 17 Apr 01:37 2014

Call for papers: The 20th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC 2014)

*** Apologies for cross-posting ***

*** Please not the URL of the conference Web site: ***

Call for Papers: The 20th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC 2014)

Nov 18-21, 2014

PRDC 2014 ( is the twentieth in this series of symposia started in 1989 that are devoted to dependable and fault-tolerant computing. PRDC is recognized as the main event in the Pacific area that covers the many dimensions of dependability and fault tolerance, encompassing fundamental theoretical approaches, practical experimental projects, and commercial components and systems. As applications of computing systems have permeated into all aspects of daily life, the dependability of computing systems has become increasingly critical. This symposium provides a forum for countries around the Pacific Rim and other areas of the world to exchange ideas for improving the dependability of computing systems.

Topics of interest include (but not limited to):
  • Software and hardware reliability, testing, verification, and validation
  • Dependability measurement, modeling, evaluation, and tools
  • Self-healing, self-protecting, and fault-tolerant systems
  • Software aging and rejuvenation
  • Safety-critical systems and software
  • Architecture and system design for dependability
  • Fault-tolerant algorithms and protocols
  • Reliability in cloud computing, Internet, and web systems and applications
  • Cloud and Internet Information security
  • Dependability issues in computer networks and communications
  • Dependability issues in distributed and parallel systems
  • Dependability issues in real-time systems, database, and transaction processing systems
  • Dependability issues in autonomic computing
  • Dependability issues in aerospace and embedded systems

Paper Submissions

Manuscripts should be submitted in the following categories: Regular Papers and Practical Experience Reports. Regular Papers should describe original research (not submitted or published elsewhere) and be not more than 10 pages using IEEE format guidelines or 20 pages double-spaced. Practical Experience Reports (max 6 pages using IEEE format guidelines or 12 pages double-spaced) should describe an experience or a case study, such as the design and deployment of a system or actual failure and recovery field data. The title page should include a 150-word abstract, five keywords, authors' names and affiliations, and a line specifying whether the submission is a Regular Paper or a Practical Experience Report. The full mailing address, phone, fax, and email address of the corresponding author should be specified.

All submissions must be made electronically (in PDF format) on the submission web site . Papers will be reviewed internationally and selected based on their originality, significance, relevance, and clarity of presentation. All accepted papers will be published by IEEE Computer Society Press. One outstanding paper will be selected to receive the Best Paper Award.

Important Dates

Submission deadline: May 2, 2014
Notification: June 25, 2014

Best regards

Concurrency mailing list
Lina Ye | 14 Apr 16:56 2014

Call for Papers: Workshops Colocated with SEFM 2014

Our apologies if you have received multiple copies.



Five Workshops Colocated with SEFM 2014

Grenoble, France
September 1-2, 2014



- 1st Workshop on Human-Oriented Formal Methods: From Readability to Automation

This workshop aims to bring together researchers, engineers and practitioners 
from academia and industry to baseline the state of the art in the increasingly 
important domain: applications of human factors to the analysis and to the 
optimization of formal methods area. It also aims to develop a future vision 
and roadmap of usability and automation, focusing especially on readability 
and ease of use. 

For more details please see

Paper Submission: 10 June, 2014
Notification of Acceptance: 5 July, 2014
Post-proceedings Final version: 15 September 2014
Workshop Date: 1 September, 2014


- 3rd International Symposium on Modelling and Knowledge Management 
applications: Systems and Domains

The aim of the Symposium is to bring together practitioners and
researchers from academia, industry, government and non-government
organisations to present research results and exchange experience,
ideas, and solutions for modelling and analysing complex systems
and using knowledge management strategies, technology and systems
in various domain areas (e.g., ecology, biology, medicine, climate, 
economy, governance, education and social software engineering) 
that address problems of sustainable development.

For more details please see

Paper Submission: 6 June 2014
Notification of Acceptance: 5 July 2014
Pre-proceedings Final version: 31 July 2014
Post-proceedings Final version: 15 September 2014
Symposium Date: 2 September 2014


- 8th International Workshop on Foundations and Techniques for Open 
Source Software Certification

The aim of this workshop is to bring together researchers from Academia 
and Industry who are broadly interested in 1) the quality assessment of 
the open source software projects, and 2) metrics, procedures, and tools 
that could be useful in assessing and qualifying individual participation 
and collaboration patterns in the open source software communities.

For more details please see

Paper Submission: 6 June 2014
Notification of Acceptance: 11 July 2014
Notification of Early Registration: 15 July 2014
Pre-proceedings Final version: 31 July 2014
Post-proceedings Final version: 15 September 2014
Workshop Date: 1 September 2014


- 1st Workshop on Safety and Formal Methods

Formal methods have traditionally been advocated for improving the reliability 
of safety-relevant systems. The SaFoMe workshop aims to provide a forum for 
people from academia and industry to communicate their latest results on 
theoretical advances, industrial case studies, and lessons learned in the 
application of formal methods to safety certification, verification and/or 
validation in (but not limited to) component-based systems.

For more details please see

Abstract Submission: 23 May, 2014
Paper Submission: 30 May, 2014
Notification of Acceptance: 30 June, 2014
Camera-ready Paper Due: 15 July, 2014
Registration deadline: 15 July, 2014
Workshop Date: 1 September, 2014


- 4th Workshop on Formal Methods in the Development of Software

The aim of WS-FMDS is to bring together scientists and practitioners who are 
active in the area of formal methods and interested in exchanging their 
experiences in the industrial usage of these methods. This workshop also 
strives to promote research and development for the improvement of theoretical 
aspects of formal methods and tools focused on practical usability for 
industrial applications.

For more details please see

Paper Submission: 23 May, 2014
Notification of Acceptance: 9 June, 2014
Camera-ready Paper Due: 20 June, 2014
Workshop Date: 1-2 September, 2014



All accepted papers will be published by Springer in a volume of LNCS.
Condition for inclusion in the post-proceedings is that at least one
of the co-authors has presented the paper at the workshop.

Concurrency mailing list
Kirstin Peters | 16 Apr 18:47 2014

[DisCoTec] Call for Contribution

[We apologize for multiple copies] ==================================================================== Call for Participation DisCoTec 2014 Berlin, Germany, June 3-6, 2014 early registration, May 5 ==================================================================== The DisCoTec series of federated conferences is one of the major events sponsored by the International Federation for Information processing (IFIP). The main conferences, taking place on 3-5 June at Technische Universität Berlin, are: * COORDINATION - 16th International Conference on Coordination Models and Languages * DAIS - 14th IFIP International Conference on Distributed Applications and Interoperable Systems * FORTE - 34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems ==================================================================== Invited Speakers Frank Leymann (University of Stuttgart, Germany) Maarten van Steen (VU University Amsterdam, Netherlands) Joachim Parrow (Uppsala University, Sweden) ==================================================================== The DisCoTec 2014 program is available at: ==================================================================== Registration The early registration deadline of DisCoTec is May 5th. The registration page is available on the DisCoTec homepage:

Concurrency mailing list
Franck Cassez | 15 Apr 01:53 2014

ATVA 2014: Last Call for Papers -- Sydney November 3-7

[We apologise for duplicates.]

                   ATVA 2014 Call for Papers

           12th International Symposium on Automated
           Technology for Verification and Analysis

                   Sydney, November 3-7, 2014

. Abstract submission:  NEW         19 April 2014
. Paper submission:     NEW         27 April 2014

The purpose of ATVA is to promote research on theoretical and practical
aspects of automated analysis, verification and synthesis by providing
an international forum for interaction among the researchers in academia
and industry.

. Abstract submission:  NEW         19 April 2014
. Paper submission:     NEW         27 April 2014
. Notification of acceptance:       30 June 2014
. Final copy for proceedings:       30 July 2014
. Conference:                       3-7 November 2014

ATVA 2014 solicits high quality submissions in areas related to the theory and
practice of automated analysis and verification of hardware and software systems.
Topics of interest include, but are not limited to:
Formalisms for modeling hardware, software and embedded systems
. Specification and verification of finite-state, infinite-state
and parameterized system
. Program analysis and software verification
. Analysis and verification of hardware circuits, systems-on-chip
and embedded systems
. Analysis of real-time, hybrid, timed, priced/weighted and probabilistic systems
. Deductive, algorithmic, compositional, and abstraction/refinement techniques
for analysis and verification
. Analytical techniques for safety, security, and dependability
. Testing and runtime analysis based on verification technology
. Synthesis and Games
. Analysis and verification of parallel and concurrent hardware/software systems
. Verification in industrial practice
. Applications and case studies
Theory papers should preferably be motivated by practical problems, and
applications should be based on sound theory and should solve problems of
practical interest.

ATVA invites research contributions in two categories: Regular research
papers (with 15 pages page limit) and tool papers (with 4 pages page limit).
Contributions must be written in English and in LNCS format, and must
present original research which is unpublished and not submitted elsewhere
(conferences or journals). The proceedings of ATVA 2014 will be
be published by Springer as a volume in the series of Lecture Notes in
Computer Science (LNCS). A special journal issue is also being planned
for selected papers.

General Chair:
   Dr. Ralf Huuck (NICTA and UNSW)

Program co-chairs:
   Dr. Franck Cassez (NICTA and UNSW)
   Pr. Jean-François Raskin (ULB)

Workshop Chair:
   Dr. Peter Höefner (NICTA and UNSW)

Program committee:
   Ahmed Bouajjani (LIAFA, University Paris Diderot, France)
   Supratik Chakraborty (IIT Bombay, India)
   Alessandro Cimatti (FBK-irst, Italy)
   Deepak D'Souza (Indian Institute of Science, Bangalore, India)
   Hung Dang Van (UET, Vietnam National University, Hanoi)
   Giorgio Delzanno (DIBRIS, Università di Genova)
   E. Allen Emerson (The University of Texas at Austin, USA)
   Pierre Ganty (IMDEA Software Institute, Spain)
   Patrice Godefroid (Microsoft Research, USA)
   Kim Guldstrand Larsen (Aalborg University, Denmark)
   Teruo Higashino (Osaka University, Japan)
   Alan Hu (University of British Columbia, Canada)
   Joost-Pieter Katoen (RWTH Aachen University, Germany)
   Moonzoo Kim (KAIST, Korea)
   Gerwin Klein (NICTA and UNSW, Australia)
   Orna Kupferman (Hebrew University, Israel)
   Marta Kwiatkowska (University of Oxford, UK)
   Insup Lee (University of Pennsylvania, USA)
   Oded Maler (CNRS-VERIMAG, France)
   Annabelle McIver (Macquarie University, Australia)
   Madhavan Mukund (Chennai Mathematical Institute, India)
   Mizuhito Ogawa (Japan Advanced Institute of Science and Technology, Japan)
   Sungwoo Park Pohang (University of Science and Technology, Korea)
   Doron Peled (Bar Ilan University, Israel)
   Andreas Podelski (University of Freiburg, Germany)
   Pierre-Alain Reynier (Aix-Marseille University, France)
   Jie-Hong Rolland-Jiang (National Taiwan University Taipei, Taiwan)
   Jing Sun (The University of Auckland, New Zealand)
   P.S. Thiagarajan (National University of Singapore, Singapore)
   Ron Van Der Meyden (UNSW, Australia)
   Rob Van Glabbeek (NICTA and UNSW, Australia)
   Farn Wang (National Taiwan University Taipei, Taiwan)
   Chao Wang (Virginia Tech., USA)
   Bow-Yaw Wang (Academia Sinica, Taipei, Taiwan)
   Karsten Wolf (Rostock University, Germany)
   Hsu-Chun (Yen National Taiwan University, Taiwan)
   Wang Yi (Uppsala University, Sweden)
   Wenhui Zhang (Institute of Software, Chinese Academy of Sciences, China)

Steering Committee:
    Professor E. Allen Emerson (University of Texas at Austin)
    Professor Teruo Higashino (Osaka University)
    Professor Insup Lee (University of Pennsylvania)
    Professor Doron A. Peled (Bar Ilan Universioty)
    Professor Farn Wang (National Taiwan University)
    Professor Hsu-Chun Yen (National Taiwan University)


The information in this e-mail may be confidential and subject to legal professional privilege and/or
copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Concurrency mailing list

Charles Pecheur | 15 Apr 12:12 2014

FTSCS 2014 call for papers

                      Call for Papers

                         FTSCS 2014

3rd International Workshop on Formal Techniques for Safety-Critical Systems

               Luxembourg, November 6-7, 2014
             (satellite workshop of ICFEM 2014)



*** Science of Computer Programming special issue ***
*** Springer CCIS proceedings ***

Aims and Scope:

There is an increasing demand in industry to use formal methods to
achieve software-independent verification and validation of
safety-critical systems, e.g., in fields such as avionics, automotive,
medical, and other cyber-physical systems. Newer standards, such as
DO-178C (avionics) and ISO 26262 (automotive), emphasize the need for
formal methods and model-based development, speeding up the
adaptation of such methods in industry.

The aim of this workshop is to bring together researchers and engineers
who are interested in the application of formal and semi-formal methods
to improve the quality of safety-critical computer systems. In
particular, FTSCS strives strives to promote research and development of
formal methods and tools for industrial applications, and is particularly
interested in industrial applications of formal methods.

Specific topics include, but are not limited to:

* case studies and experience reports on the use of formal methods for
analyzing safety-critical systems, including avionics, automotive,
medical, and other kinds of safety-critical and QoS-critical systems
* methods, techniques and tools to support automated analysis,
certification, debugging, etc., of complex safety/QoS-critical systems
* analysis methods that address the limitations of formal methods in
industry (usability, scalability, etc.)
* formal analysis support for modeling languages used in industry,
such as AADL, Ptolemy, SysML, SCADE, Modelica, etc.
* code generation from validated models.

The workshop will provide a platform for discussions and the exchange of
innovative ideas, so submissions on work in progress are encouraged.


We solicit submissions reporting on:

A- original research contributions (15 pages max, LNCS format);
B- applications and experiences (15 pages max, LNCS format);
C- surveys, comparisons, and state-of-the-art reports (15 pages max, LNCS);
D- tool papers (5 pages max, LNCS format);
E- position papers and work in progress (5 pages max, LNCS format)

related to the topics mentioned above.

All submissions must be original, unpublished, and not submitted
concurrently for publication elsewhere. Paper submission is done
via EasyChair at
The final version of the paper must be prepared in LaTeX, adhering to
the LNCS format available at


All accepted papers will appear in the pre-proceedings of FTSCS 2014.
Accepted papers in the categories A-D above will appear in the
workshop proceedings that will be published as a volume in
Springer's CCIS series. 

The authors of a selected subset of accepted papers will be invited to
submit extended versions of their papers to appear in a special issue
of the Science of Computer Programming journal.

Important dates:

Submission deadline: September 6, 2014
Notification of acceptance: October 3, 2014
Workshop: November 6/7, 2014



Program chairs:

Cyrille Artho        AIST, Japan
Peter Olveczky       University of Oslo, Norway

Program committee:

Erika Abraham        RWTH Aachen University, Germany
Musab AlTurki        King Fahd Univ. of Petroleum and Minerals, Saudi Arabia
Toshiaki Aoki        JAIST, Japan
Farhad Arbab         Leiden University and CWI, The Netherlands
Cyrille Artho        AIST, Japan
Kyungmin Bae         University of Illinois at Urbana-Champaign, USA
Saddek Bensalem      Verimag, France
Armin Biere          Johannes Kepler University, Austria
Ansgar Fehnker       University of the South Pacific, Fiji
Mamoun Filali        IRIT, France
Bernd Fischer        Stellenbosch University, South Africa
Klaus Havelund       NASA JPL, USA
Marieke Huisman      University of Twente, The Netherlands
Ralf Huuck           NICTA, Australia
Fuyuki Ishikawa      National Institute of Informatics, Japan
Takashi Kitamura     AIST, Japan
Alexander Knapp      Augsburg University, Germany
Yang Liu             Nanyang Technological University, Singapore
Frederic Mallet      INRIA Sophia Antipolis, France
Robi Malik           University of Waikato, New Zealand
Cesar Munoz          NASA Langley, USA
Thomas Noll          RWTH Aachen University, Germany
Peter Olveczky       University of Oslo, Norway
Charles Pecheur      Universite catholique de Louvain, Belgium
Paul Pettersson      Malardalen University, Sweden
Camilo Rocha         Escuela Colombiana de Ingenieria, Colombia
Ralf Sasse           ETH Zurich, Switzerland
Oleg Sokolsky        University of Pennsylvania, USA
Sofiene Tahar        Concordia University, Canada
Carolyn Talcott      SRI International, USA
Tatsuhiro Tsuchiya   Osaka University, Japan
Jackie Wang          McMaster University, Canada
Michael Whalen       University of Minnesota, USA
Huibiao Zhu          East China Normal University, China


(email)  peterol@...  and  c.artho@...

Concurrency mailing list

Carsten Fuhs | 17 Apr 01:27 2014

2nd CfP: 14th Intl. Workshop on Termination (WST 2014), Vienna (Austria), 17-18 July

           14th International Workshop on Termination (WST)

         Affiliated with CAV, IJCAR and RTA-TLCA at FLoC 2014
                  17 - 18 July 2014, Vienna, Austria



The Workshop on Termination traditionally brings together, in an
informal setting, researchers interested in all aspects of
termination, whether this interest be practical or theoretical,
primary or derived. The workshop also provides a ground for
cross-fertilisation of ideas from term rewriting and from the
different programming language communities. The friendly atmosphere
enables fruitful exchanges leading to joint research and subsequent

The 14th International Workshop on Termination in Vienna continues the
successful workshops held in St. Andrews (1993), La Bresse (1995),
Ede (1997), Dagstuhl (1999), Utrecht (2001), Valencia (2003),
Aachen (2004), Seattle (2006), Paris (2007), Leipzig (2009),
Edinburgh (2010), Obergurgl (2012), and Bertinoro (2013). More
information on earlier WSTs is available on the Termination Portal:


The 14th International Workshop on Termination welcomes contributions
on all aspects of termination and complexity analysis (and their
automation) for various models of computation, ranging from rewrite
systems and state transition systems to programming languages.

Contributions from the imperative, constraint, functional, logic,
and concurrent programming communities, and papers investigating
applications of complexity or termination (for example in program
transformation or theorem proving) are particularly welcome.

Areas of interest include, but are not limited to, the following:

      * Termination of programs
      * Termination of rewriting
      * Termination analysis of transition systems
      * Complexity of programs
      * Complexity of rewriting
      * Implicit computational complexity
      * Implementation of termination and complexity analysis methods
      * SAT and SMT solving for (non-)termination analysis
      * Certification of termination and complexity proofs
      * Termination orders, well-founded orders, and reduction orders
      * Termination methods for theorem provers
      * Strong and weak normalization of lambda calculi
      * Termination analysis for different language paradigms
      * Invariants for termination proving
      * Challenging termination problems
      * Applications to program transformation and compilation
      * Comparison and classification of termination methods
      * Non-termination and loop detection
      * Termination in distributed and concurrent systems
      * Proof methods for liveness and fairness
      * Well-quasi-order theory
      * Ordinal notations and subrecursive hierarchies


Elvira Albert (Complutense University of Madrid)
Amir Ben-Amram (Tel-Aviv Academic College)
Byron Cook (Microsoft Research and University College London)
Carsten Fuhs (University College London) - chair
Jürgen Giesl (RWTH Aachen)
Laure Gonnord (University of Lyon)
Albert Rubio (Universitat Politècnica de Catalunya)
Peter Schneider-Kamp (University of Southern Denmark)
Christian Sternagel (University of Innsbruck)
Thomas Ströder (RWTH Aachen)
Johannes Waldmann (HTWK Leipzig)
Harald Zankl (University of Innsbruck)


The keynote will be given by Jasmin Fisher from
Microsoft Research, Cambridge, United Kingdom:


Submissions are short papers / extended abstracts which should not
exceed 5 pages using the LIPIcs style for LaTeX:

There will be no formal reviewing, but we will provide informal
feedback for each submission. Accepted papers will be made available
electronically, both on the WST 2014 web page and on the FLoC USB
proceedings. The workshop proceedings are informal as well. Thus,
submission to WST 2014 is not in conflict with an earlier, concurrent,
or later publication of the same material at a journal, a conference,
or another workshop. In case of simultaneous submissions to several
FLoC events, please state in the abstract on easychair to which other
FLoC venues you are submitting as well.

Papers should be submitted electronically via the submission page:


Paper submission      23 April 2014
Notification          07 May 2014
Final versions due    21 May 2014
Workshop date         17 - 18 July 2014
Concurrency mailing list

Lavygina, Anna | 16 Apr 16:32 2014

BPCAS 2014: Business Processes in Collective Adaptive Systems

[ Apologies for multiple copies. Please forward to interested colleagues. ]


Business Processes in Collective Adaptive Systems 
(BPCAS 2014)

September 8, 2014, Haifa, Israel

In conjunction with the 12th International Conference on Business Process Management (BPM 2014)

Submission deadline: 1 June 2014


BPCAS is a new workshop focusing on all topics related to Collective Adaptive Systems (CAS). It aims to provide a high-quality forum for the presentation of developments in CASs and for bringing together researchers and practitioners from diverse disciplines interested in CASs both within the business process community and outside. The latter are particularly welcome to submit to the workshop.

Topics of interest include:

* business process modeling for CAS
* collective configuration of business processes in CAS
* context/knowledge-aware business processes in CAS
* adaptation and evolution in CAS
* formal methods for CAS
* distribution and mobility in CAS
* big data in CAS
* process similarity and emergent properties of CAS
* security and privacy in CAS
* machine learning and data mining techniques for CAS
* optimization of CAS
* frameworks, tools and programming paradigms for CAS
* usability aspects of CAS
* case studies and scenarios

Accepted papers will be published by Springer as a post-workshop proceedings volume in the series Lecture Notes in Business Information Processing (LNBIP). In addition authors of the best papers will be invited to submit a revised and extended version of their paper to a special issue of the IET Software journal.  The workshop is sponsored by the EU’s Fundamentals of Collective Adaptive Systems programme initiative (


Submission deadline: June 1, 2014
Author notification: July 1, 2014
Camera-ready submission: July 23, 2014
Workshop date: September 8, 2014


Manfred Reichert, Universität Ulm, Germany


Antonio Bucchiarone, Fondazione Bruno Kessler, Italy
Naranker Dulay, Imperial College London, UK
Dimka Karastoyanova, University of Stuttgart, Germany
Anna Lavygina, Imperial College London, UK
Adnan Tariq, University of Stuttgart, Germany

Program Committee
Vasilios Andrikopoulos, University of Stuttgart, Germany
Salima Benbernou, L’Universit´e Paris Descartes, France
Marina Bitsaki, University of Crete, Greece
Alexei Lapouchnian, University of Toronto, Canada
Kim Larsen, Aalborg University, Denmark
Lior Limonad, IBM Haifa, Israel
Christos Nikolaou, University of Crete, Greece
Francisco Pereira, SMART-MIT, Singapore
Marco Pistore, Fondazione Bruno Kessler, Italy
Manfred Reichert, Universität Ulm, Germany
Kurt Rothermel, University of Stuttgart, Germany
Alessandra Russo, Imperial College, UK
Nikola Serbedija, Fraunhofer FIRST, Germany
Pnino Soffer, University of Haifa, Israel
Arnon Sturm, Ben-Gurion University of the Negev, Israel
Yury Tsoy, Institut Pasteur Korea, South Korea
Ingo Weber, NICTA, Australia


We invite submissions in two forms: full papers and position papers. Submitted papers must be written in English, should not have been submitted for review or published elsewhere, and should not exceed 12 pages for full papers, and 6 pages for position papers (including figures, bibliography and appendices).

Submissions are only accepted in PDF format via the EasyChair system ( Submissions should be formatted according to the LNBIP format specified by Springer.

At least one author of each accepted paper is required to present the paper at the workshop.


For further information contact Anna Lavygina (a.lavygina-AQ/
Concurrency mailing list
Eric Madelaine | 17 Apr 17:07 2014

PhD position in Sophia-Antipolis + Bologna

We have one PhD position available in Sophia Antipolis, in collaboration with Univ of Bologna.

Localisation :         Sophia Antipolis AND Univ. of Bologna
Start :                     Sept 2014
Ludovic Henrio --

Title: Deadlock analysis for concurrent and distributed programming

Thesis advisors:
Ludovic Henrio (HDR) - CNRS / I3S; Team: SCALE (INRIA/CNRS/I3S/Université de Nice Sophia-Antipolis)
Cosimo Laneve (Professor) - Università di Bologna Team: FOCUS - INRIA

This thesis is in the field of programming languages, especially languages for programming multicore and distributed applications. The overall objective of this thesis is to study and improve the state or the art of programming languages dedicated to these architectures. We aim at improvements both in terms of ease of programming and in terms of efficient and safe execution of programs.

Programming distributed systems is a challenging task, and providing a tool suite for helping the programmer to write correct programs over concurrent and distributed systems is crucial. For this, we believe that the approach advocated by actors and active objects is valuable. Indeed, these models focus on the asynchrony between remote entities and by nature decouple the execution flow in each distributed entity as much as possible. This approach is particularly relevant for programming large scale distributed systems and/or service-oriented applications. An active object is an object associated with a single thread of execution. Unfortunately, active-objects are not as efficient as they could be when it comes to execution on multicore machines. To fully use the computing power of multicore architectures, different threads should share access to the same memory, which is contradictory with the principles of active objects.

The OASIS team is working on the design of programming paradigms, languages, and mid- dleware for distributed systems. Recently, the team proposed a new programming model called ”multi-active objects”. The multi-active objects benefit from the ease of programming provided by the active objects and actors, while overcoming their limitations in terms of expressiveness and efficiency on multicore machines. This model is among the first high-level programming paradigms tackling both distributed and parallel computing and it is extremely promising in terms of ease of programming and efficiency. Multi-active objects offer a new compromise between the model of strict and secure programming proposed by active objects, and classical multi-threaded approach, very tolerant but very prone to errors. However, the programming model for multi-active objects also requires new advances in the fundamental study of distributed programming languages to prove the properties and to formalize this new programming model.

The FOCUS team has also a solid experience in distributed programming languages and their verification. In the past they have prototyped a distributed pi-calculus language with XML datatypes, called PiDuce, and studied its relation with web services. More recently, the FO- CUS team has been involved in the HATS European project, where the distributed actor-based language ABS has been developed. This language has a model similar to the one of active objects. The major contribution of the FOCUS team has been the development of a deadlock analysis framework for ABS programs.

Locks, Impact and Challenges:

The expected impact of this thesis is to contribute to the formal design and the practical implementation of multi-active objects. Mostly, we want to benefit from this thesis to show that our programming model is easy to use, can be formally specified, and is efficient in practice. This thesis will particularly focus on the formal specification and on the support for writing programs that run safely. One of the major source of bugs in concurrent and distributed systems is deadlocks. Deadlocks come from the fact that most programs rely on synchronization points, where one task is waiting for the completion of another task before being able to finish. If the graph of synchronization dependencies form a cycle, then there is a deadlock. Finding deadlocks in distributed programs requires a strong expertise. Alleviating the programmer from the difficult task by providing him/her with automatic tools able to detect automatically those deadlocks will be a valuable contribution. Indeed, despite the ease of programming featured by active objects and the fact that multi-threading allows us to avoid several misbehaviours, this programming model is far from being deadlock free.

We want the relevant information for detecting deadlock to be automatically inferred from the program, namely the information needed to statically build the graph of synchronization dependencies. Such information in our experience takes the form of (behavioral) types, which are the input of a deadlock analyzer. This is a more complex task than a mere adaptation of the tool already developed for ABS, for several reasons. First, even if ABS and multi-active objects have similar concurrency models, the impact of their differences must be fully understood. For instance, ABS provides an explicit blocking operator for retrieving future values, while in the multi-active objects paradigm this is an implicit operation performed at the first access. Second, the multi- active object paradigm provides powerful user-defined annotations and scheduling policies, which should be carefully managed by the inference engine in order to properly recognize dependencies between threads. Third, once the inference system has been developed, then it could represent a basis for inferring other kind of information from the code, such as tracking resource access information. Therefore, the system might be able to verify other properties related to the interplay of concurrent threads – e.g. noninterference of methods (in order to maximize the parallelism).

Objectives and expected results:

This thesis proposal contribute to the formal model of multi-active objects and to their practical implementation. In particular, we will provide tools for the static analysis of deadlocks. As regards this last point, while several works already focus on the safe design of distributed applications, those works are not massively adopted in practice. The main originality of our approach is twofold. First we rely on a programming model that enforces a strong separation between remote entities. This helps us for automatically inferring behavioral types for those entities and will make our analysis more compositional, more scalable, and thus better adapted to real applications. Second, the design of our language will be mainly driven by the efficiency of program execution, by the expressiveness of the model, and by the easiness of writing distributed applications.

The main objectives of this thesis are the following ones:

• Contribution to the programming model. The precise definition of the semantics of multi- active objects, a comparison with existing active-object models, and the analysis of the potential deadlocks. At this points, several variants of the programming language will be studied, some of them might simplify the deadlock analysis or make it more powerful. Being able to study such languages restrictions will guarantee the success of this thesis and will allow us to study different categories of applications.

• Definition of a deadlock analysis algorithm for multi-active objects. This objective should be divided in the following steps:

        • Identify which are the synchronization points in the multi-active objects as opposed to the one already identified for ABS, and define an inference system. A first step in this direction would be the definition of the inference system for a variant of ABS without explicit synchronization (get) operation. This step will bridge the semantic gap between the two languages.

        • Extend the preliminary inference system to the full multi-active object model.

        • Possibly adapt/extend/empower the deadlock analyzer developed for ABS.

The PhD involves teaching duties, and should be mostly located in Sophia Antipolis. The PhD student will spend a significant amount of time in Univ. of Bologna. The PhD should start before September 2014.

The PhD is funded by UNC <at> Sophia Labex (funded by the French Government (National Research Agency, ANR) through the “Investments for the Future” Program  reference #  ANR-11-LABX-0031-01)
Concurrency mailing list
Andreas Lochbihler | 15 Apr 15:52 2014

Two PhD positions in Information Security at ETH Zurich, Switzerland

The Information Security group headed by Prof. David Basin at ETH
Zurich has two open PhD positions in two projects:

(1) Formalizing computational soundness for protocol implementations
(2) Testing access control systems

We are looking for enthusiastic outstanding researchers with a strong
background and interest in one or more of the following areas:

- formal methods or mathematical logic,
- information security or cryptography,
- (project 1) interactive theorem proving
   (project 2) software testing.

Candidates with a strong theoretical background in related areas are
also encouraged to apply. ETH Zurich regulations require PhD
candidates to hold a Masters or equivalent degree (e.g. Diplom). The
preferred starting date for both positions is as soon as possible, at
the latest by the end of 2014.

Description of the projects:

(1) Formalizing computational soundness for protocol implementations,
     funded by the Swiss National Science Foundation

The project aims at a better understanding of, and more confidence in,
the security guarantees offered by symbolic analysis methods for
security protocols, e.g. TLS and IPsec. To this end, symbolic and
computational models of security protocols and security properties
will be formalized in the proof assistant Isabelle/HOL and linked with
computational soundness results. For more information see:

(2) Testing access control systems

The project aims at developing algorithms and tools for generating
security tests from formal access control policies, and assessing
their effectiveness. The position is within the Zurich Information
Security and Privacy Center (ZISC) and the successful candidate will
work closely with our industrial partner.

Applications should include a curriculum vitae, a brief description of
research interests, transcripts of grades, letters of recommendation
from teachers or employers, an indication of the preferred project,
and, if possible, the Master's or Bachelor's thesis and publications.
We will consider applications until the position is filled. Please

Applications and informal inquiries should be sent to Andreas
Lochbihler and Mohammad Torabi Dashti at the following email address:


PhD students are paid employees of ETH. Salary and employment
conditions are attractive. Zurich is a diverse and multicultural city
that is consistently rated among the best cities in the world in which
to live. Further information is available from the following links:

Open Positions at Institute of Information Security:

Institute of Information Security:

ETH Zurich:

City of Zurich:
Concurrency mailing list

jun sun | 16 Apr 09:06 2014

One Postdoc Research Fellow Position on Verification of Cyber-Physical Systems


A Postdoctoral Research Fellow position is available on security and cyber-physical systems, funded by a research project led by Dr. Sun Jun from Singapore University of Technology and Design. The goal of this project is to develop novel automated techniques for analyzing security properties of cyber-physical systems.

To apply you must hold a degree in the areas of Computer Science, or a related discipline, and a PhD in a relevant research area (which includes program analysis, security, cyber-physical system analysis, formal verification, model checking, formal methods, testing, etc.). Candidates are expected to have high-quality publications in peer-reviewed conferences and journals. The postdoc will be supervised by Dr. Sun Jun and will be working closely with his existing research fellows/assistants as well as PhD students.

The Singapore University of Technology and Design’s (SUTD) is set up in collaboration with Massachusetts Institute of Technology (MIT) and represents MIT’s most significant collaboration on education to date. SUTD takes pride in creating a unique system of education that includes cohort based instruction, novel pedagogy, and emphasis on design throughout its multidisciplinary curriculum. This research project is supported by a research center on cyber-physical systems in SUTD. Also of the research center are multiple mock up systems of real-world cyber-physical systems. Researchers supported by the center are encouraged to apply their research approaches/results on these real systems.

This postdoc position is available for up to 4 years. The salary ranges from SGD 60K to 80K per year with attractive package. 

Informal inquiries are encouraged and should be directed to:

Dr Sun Jun (


Concurrency mailing list