w.ahmad | 11 Sep 14:04 2014
Picon
Picon

CfP: 1st International Workshop on Investigating Dataflow in Embedded computing Architecture

[Please accept our apologies if you receive multiple copies]

 

===== Call for Extended Abstracts - IDEA 2015 =====

1st International Workshop on Investigating Dataflow in Embedded computing Architecture
http://caes.ewi.utwente.nl/idea2015

In conjunction with with HiPEAC 2015
http://www.hipeac.net/2015/amsterdam



===== Important Dates =====
Abstract Submission Deadline: 11 October 2014
Notification of Acceptance: 15 November 2014
Camera-Ready Version Submission Deadline: 6 December 2014
Workshop date: 21 January 2015.
HiPEAC Conference Date: 18 – 21 January 2015

===== General Scope =====

The dataflow model of computation offers a powerful perspective on parallel computations that may be conditioned in terms of data dependencies. It dates back to the sixties and has applications in the design of real-time stream-processing systems, especially in the area of digital signal processing. As a model of computation that fits embedded multi-core system architectures, dataflow is gaining renewed popularity, with an influx of work ranging from using dataflow as a programming paradigm, for performance analysis, or for design optimization.

Dataflow is gaining popularity among researchers around Europe and the world. However, research on dataflow is limited to small pockets in different communities without a common forum for discussion. The goal of this workshop is to provide a platform dedicated to the discussion of emerging ideas in modeling and analysis of present and future high performance computing architectures using dataflow. Furthermore we hope to increase exposure and strengthen communication among different research groups working on dataflow.

We especially invite new PhD students and Post-Docs exploring into dataflow modeling and analysis. The workshop offers an informal setting to discuss and exchange ideas, and to get in touch with experts in the field. Topics of interest include, but are not limited to:

• Dataflow as a programming paradigm for embedded applications.
• Real-time scheduling, analysis, response modeling techniques, for embedded systems.
• Tools for compilation, evaluation, optimization or synthesis of applications for heterogeneous / homogeneous multi-processor systems with respect to shared bus, shared memory, buffer sizing, power consumption, etc.
• New variants of the dataflow model of computation to capture dynamic execution behavior.
• Analysis of data flow graphs using other models of computation.



===== Organizing Committee =====
Waheed Ahmad (University of Twente, Twente)
Robert de Groote (University of Twente, Twente)
Alok Lele (University of Eindhoven, Eindhoven)



===== Technical Program Committee =====
Benny Åkesson (Czech Technical University, Prague)
Marco Bekooij (NXP Research, Eindhoven)
Shuvra S. Bhattacharyya (University of Maryland, College Park)
Pieter J. L. Cuijpers (University of Eindhoven, Eindhoven)
Michael Glaß, (Friedrich-Alexander-Universität, Erlangen-Nürnberg)
Kim Grüttner (OFFIS, Oldenburg)
Alix Munier Kordon (INRIA / LIP6, Paris)
Orlando Moreira (Ericsson, Eindhoven)
Luis Miguel Pinho (CISTER, Porto)
Petro Poplavko (VERIMAG, Grenoble)
Gerard Smit (University of Twente, Twente)
Sander Stuijk (University of Eindhoven, Eindhoven)
Jean-Pierre Talpin (INRIA, Rennes)
Xue-Yang ZHU (SKLCS, Beijing)

===== Submission Guidelines =====
We invite authors to submit 2 – 4 page extended abstracts, in double column format, font no smaller than 10 points. A booklet containing the proceedings will be available at the conference and on the website of the workshop. Templates are available at:
http://www.ieee.org/conferences_events/conferences/publishing/templates.html

Authors may submit their work using the following link:
https://easychair.org/conferences/?conf=idea2015
Accepted submissions will be invited to give either a long 25 minute presentation or a short 15 minute presentation depending on the content of the submission as seen fit by the program committee.

_______________________________________________
Concurrency mailing list
Concurrency@...
http://listserver.tue.nl/mailman/listinfo/concurrency
benoit delahaye | 12 Sep 09:08 2014
Picon

SynCoP 2015: 1st Call for Papers

(apologies for multiple copies)

==================================================
                           Call for papers

                             SynCoP 2015
  2nd International Workshop on the SYNthesis of COmplex Parameters

                       (ETAPS satellite event)

http://lipn.univ-paris13.fr/SynCoP2015/
==================================================

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 workshop will take place on Saturday, April 11, 2015, in London, UK, 
as a
satellite event of ETAPS.

The workshop may be able to (at least partially) support the travel and the
ETAPS workshop registration fees for one or two PhD or Master student(s).

=================
  IMPORTANT DATES
=================
Abstract:               January 12, 2015
Full papers:            January 19, 2015
Informal presentations: February 20, 2015
Notification:           February 27th, 2015
Workshop:               April 11th, 2015
Camera ready:           May 1st, 2015

=================
  TOPICS OF THE WORKSHOP
=================

The scientific subject of the workshop covers (but is not limited to) the
following areas:
   * parameter synthesis
   * parametric model checking
   * regular model checking
   * robustness analysis
   * parametric logics, decidability and complexity issues
   * formalisms such as parametric timed and hybrid automata, parametric
time(d) Petri nets, parametric probabilistic (timed) automata, parametric
Markov Decision Processes, networks of identical processes
   * interactions between discrete and continuous parameters
   * tools and applications to major areas of computer science and control
engineering.

=================
  SUBMISSION AND PUBLICATION
=================

SynCoP seeks both regular papers and tool papers.

The content of papers should be original and not submitted elsewhere. All
papers will be assigned to at least three reviews.

The page limit is 12 pages in OASIcs LaTeX format
(http://www.dagstuhl.de/en/publications/oasics/) for regular papers and 4
pages for tool papers.
All accepted papers will be published in the Dagstuhl's OpenAccess 
Series in
Informatics (OASIcs), using the Creative Commons CC-BY license. Hereby, the
authors retain their copyright. All accepted papers will be referenced 
using
an ISBN and a DOI in all major databases (such as DBLP).

Accepted tool papers will be required to do a demo during the workshop.

Submission will be made in English in PDF format through Easychair:
https://www.easychair.org/conferences/?conf=syncop2015

=================
INVITED SPEAKERS
=================
* Parosh Abdulla, Uppsala, Sweden (tentative)
* TBA

=================
    PC CHAIRS
=================
* Etienne Andre (Universite Paris 13, Sorbonne Paris Cite, France)
* Goran Frehse (Universite Joseph Fourier Grenoble 1 - Verimag, France)

=================
PROGRAM COMMITTEE
=================

* Alessandro Cimatti, Trento, Italy
* Benoit Delahaye, Nantes, France
* Giorgio Delzanno, Genova, Italy
* Alexandre Donze, Berkeley, USA
* Laurent Fribourg, Cachan, France
* Antoine Girard, Grenoble, France
* Claude Jard, Nantes, France
* Vineet Kahlon, Austin, TX, USA
* Sumit Kumar Jha, Orlando, USA
* Kim Larsen, Aalborg, Denmark
* Didier Lime, Nantes, France
* Wojciech Penczek, Warszawa, Poland
* Laure Petrucci, Villetaneuse, France
* Olivier H. Roux, Nantes, France
* Jiri Srba, Aalborg, Denmark
* Jun Sun, Singapore
* Ashish Tiwari, USA
* Tayssir Touili, Villetaneuse, France
* Tomas Vojnar, Brno, Czech Republic

=================
    TOOL DEMONSTRATION CHAIR
=================
* Laure Petrucci, Villetaneuse, France
* TBA

=================
    PUBLICITY CHAIR
=================
* Claude Jard, Nantes, France
* Benoit Delahaye, Nantes, France

=================
SUPPORT
=================
TBA

--

-- 
--------------------------------------------
--------------------------------------------
Benoît Delahaye
Maître de Conférences
Université de Nantes/LINA

_______________________________________________
Concurrency mailing list
Concurrency <at> listserver.tue.nl
http://listserver.tue.nl/mailman/listinfo/concurrency
liyuanfang | 2 Sep 06:22 2014
Picon

CFP: PRDC2014 Call for Participation

PRDC 2014 Call for Participation

School of Computing, National University of Singapore, Singapore 
Nov. 19-21,2014
http://prdc.dependability.org/PRDC2014/index.html

---------------------------------
Call for Participation
http://prdc.dependability.org/PRDC2014/program.html
---------------------------------

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

The program of PRDC 2014 can be found at http://prdc.dependability.org/PRDC2014/program.html.

Registration information can be found at http://prdc.dependability.org/PRDC2014/registration.html.

## National University of Singapore ##

A leading global university centered in Asia, the National University of Singapore (NUS) offers a global
approach to education and research, with a focus on Asian perspectives and expertise. Over 36,000
students from 100 countries further enrich the community with their diverse social and cultural
perspectives, making campus life vibrant and exciting. NUS has a strong and growing reputation for
impactful research with numerous productive collaborations with research organizations and industry
in Singapore and around the world. The Department of Computer Science, with over 80 faculty members, had a
long track record in grooming leaders for the digital economy and IT workforce. The Computer Science
department has more than 350 PH.D students where strong teams of more than 20 students are doi
 ng research in Formal Method area. The departments' internationally recognized faculty members perform
research in various areas.

## Singapore ##

Singapore (also called the Lion City), is a Southeast Asian city-state off the southern tip of the Malay
Peninsula, 137 kilometres (85 mi) north of the equator. An island country made up of 63 islands, it is
separated from Malaysia by the Straits of Johor to its north and from Indonesia's Riau Islands by the
Singapore Strait to its south. Singapore is highly urbanized but almost half of the country is covered by
greenery. More land is being created for development through land reclamation.

The Lion City is a modern metropolis with one of the world's busiest ports and a world-class airport. At the
same time, the small tropical island has retained many elements of its colonial past.
_______________________________________________
Concurrency mailing list
Concurrency@...
http://listserver.tue.nl/mailman/listinfo/concurrency
Linh Thi Xuan Phan | 3 Sep 16:55 2014

Second Call for Papers: DATE'15 - Topic E3: Model-based Design and Verification for Embedded Systems

[Our apologies if you receive multiple copies of this message]

===============================================================
                 CALL FOR PAPERS DATE 2015

       Topic: E3 Model-based Design and Verification for Embedded Systems

          DATE (Design, Automation & Test in Europe) Conference
                Grenoble, France, 9-13 March, 2015
		  
===============================================================

DEADLINES
- Paper Submission:            	Sunday, September 14, 2014
- Notification of Acceptance:  	Friday, November 07, 2014
- Camera-Ready Paper:          	Friday, November 28, 2014

===============================================================

QUICK LINKS
- Conference http://www.date-conference.com
- Call for Papers http://www.date-conference.com/call-for-papers
- Instructions http://www.date-conference.com/submission-instructions

===============================================================

The Design, Automation and Test in Europe conference and
exhibition is the main European event bringing together designers
and design automation users, researchers and vendors, as well as
specialists in the hardware and software design, test and
manufacturing of electronic circuits and systems.

This five-day event consists of a conference with
plenary keynotes, regular papers, interactive presentations,
panels and hot-topic sessions, tutorials, master courses and
workshops. The scientific conference is complemented by a
commercial exhibition showing the state-of-the-art in design and
test tools, methodologies, IP and design services. Both the
conference and the exhibition, together with the many user group
meetings, fringe meetings, university booth and social events
offer a wide variety of opportunities to meet and exchange
information.

You are invited to submit your research contributions to the topic

     E3 Model-based Design and Verification for Embedded Systems

which is devoted to:

- Verification techniques for embedded systems ranging from
simulation, testing, model-checking, SAT and SMT-based reasoning,
compositional analysis and analytical methods. 

- Modeling, analysis and optimization of non-functional and performance 
aspects such as timing, memory usage, QoS and reliability. 

- Model-based design of software architectures and deployment. 

- Theories, languages and tools supporting model-based design flows 
covering software, control and physical components.

------------------------------------------
E3 Topic Program Committee:
------------------------------------------

Saddek Bensalem, Université Joseph Fourier/Verimag, France (Chair)
Linh Thi Xuan Phan, University of Pennsylvania, USA (Co-Chair)
Borzoo Bonakdarpour, McMaster University, Canada
Petru Eles, Linköping University, Sweden
Alain Girault, INRIA, France
Oleg Sokolsky, University of Pennsylvania, USA
Wang Yi, Uppsala University, Sweden
_______________________________________________
Concurrency mailing list
Concurrency@...
http://listserver.tue.nl/mailman/listinfo/concurrency

Wojciech Mostowski | 4 Sep 21:37 2014
Picon
Picon

AVoCS 2014: Final Call for Participation

(Apologies for multiple copies)

**********************************************************************

Call for Participation

14th Automated Verification of Critical Systems (AVoCS) 2014 Workshop

http://www.utwente.nl/avocs2014

24-26th September, 2014

University of Twente, Netherlands

**********************************************************************

Final Call for Participation

The aim of Automated Verification of Critical Systems (AVoCS) 2014 is
to contribute to the interaction and exchange of ideas among members
of the international research community on tools and techniques for
the verification of critical systems. The subject is to be interpreted
broadly and inclusively. It covers all aspects of automated
verification, including model checking, theorem proving, SAT/SMT
constraint solving, abstract interpretation, and refinement pertaining
to various types of critical systems which need to meet stringent
dependability requirements (safety-critical, business-critical,
performance-critical, etc.). Contributions that describe different
techniques, or industrial case studies are encouraged. The technical
programme will consist of invited and contributed talks and also allow
for short presentations of research ideas. The workshop will be
relatively informal, with an emphasis on discussion.

AVoCS topics include (but are not limited to)

     Model Checking
     Automatic and Interactive Theorem Proving
     SAT, SMT or Constraint Solving for Verification
     Abstract Interpretation
     Specification and Refinement
     Requirements Capture and Analysis
     Verification of Software and Hardware
     Specification and Verification of Fault Tolerance and Resilience
     Probabilistic and Real-Time Systems
     Dependable Systems
     Verified System Development
     Industrial Applications

Thanks to Formal Methods Europe (http://www.fmeurope.org/), we offer a
financial support for students registering for AVoCS in the form of a
registration fee waiver (full or partial). Because our financial support
is limited, we ask the students that would like to take the advantage of
this support to submit a short application (deadline August 14th). The
details on how to apply can be found on the AVoCS 2014 webpage
(http://www.utwente.nl/avocs2014).

AVoCS 2014 is coorganised and colocated with SPES_XT Summer School
on Model-based design and analysis of cyber-physical systems:

http://spes2020.informatik.tu-muenchen.de/summerschool2014.html

A registration reduction is offered for participants attending both
events. There are still places free for the prospective summer school
participants.

Important Dates (Early registration expired)

   Early registration: 1st September 2014
   Workshop: 24-26th September 2014 (2.5 days, ends 26th lunchtime)

Registration and Hotel Details

All the details on how to register and pay are to be found at the
workshop page at
http://fmt.cs.utwente.nl/conferences/avocs2014/register.php.
Hotel information is to be found at
http://fmt.cs.utwente.nl/conferences/avocs2014/local.php

Invited Speakers

The workshop will have three invited speakers:

   * Laura Kovács (Chalmers, Sweden) will speak about "Symbol
     Elimination for Automated Generation of Program Properties"
     Abstract: Automatic understanding of the intended meaning of
     computer programs is a very hard problem, requiring intelligence
     and reasoning. In this talk we describe applications of our symbol
     elimination methods in automated proram analysis. Symbol
     elimination uses first-order theorem proving techniques in
     conjunction with symbolic computation methods, and derives
     nontrivial program properties, such as loop invariants and
     loopbounds, in a fully automatic way. Moreover, symbol elimination
     can be used as analternative to interpolation for software
     verification.

   * Alastair Donaldson (Imperial College, U.K.) will speak about "Static
     Verification for GPU Kernels"
     Abstract: Graphics processing units (GPUs) are nowadays commonly
     used to accelerate general purpose computations. Because GPUs are
     massively parallel they can be hard to program correctly, and
     suffer from concurrency-related defects including data races. In
     the GPUVerify project we have been interested in applying static
     verification techniques to GPU kernels (the pieces of code that
     execute on GPU devices) in order to automatically find or prove
     absence of data races. I will describe the method we have designed
     to obtain an analysis method for parallel GPU kernels that scales
     to large numbers of threads, and will demo the GPUVerify tool in
     action on a number of examples. I will then discuss open problems
     for research in the area of reliability of data-parallel software.
     For an introduction to GPUVerify check out this video:
     https://www.youtube.com/watch?v=l8ysBPV8OvA.

     This is joint work with current and previous members of the
     Multicore Programming Group at Imperial College London, and with
     Shaz Qadeer at Microsoft Research.

   * Guy Broadfoot (U.K.) will speak about "The highs and lows of
     deploying Formal Methods in Industry".
     Abstract: I attended my first software conference in 1968; it was
     organised by NATO with the title "The Software Crisis." Many of the
     papers presented then could have been written yesterday; the
     problems of the software industry in producing reliable, correct
     software in the face of increasing complexity and shrinking time to
     market pressures have not fundamentally changed that much.

     In the intervening years as a community we have developed various
     tactics for trying to minimise software errors. Advances in theorem
     proving and model checking are good examples of systematic efforts
     to improve software correctness. Nevertheless, it remains the case
     that such approaches are rarely if ever encountered in the
     industrial workplace, with the possible exception of some safety
     critical domains, such as the software controlling nuclear power
     plants.

     In spite advances in formal methods and supporting tools, the tools
     available to programmers for verifying assertions about program
     execution are complex and require knowledge and skills that most
     practicing programmers do not have. Formal proofs remain difficult
     to construct, especially for anything but the simplest of programs.
     Merely constructing assertions to characterise program correctness
     is a difficult challenge.

     In 1998, I conceived the idea of combing model checking, code
     generation and the specification approach of Sequence-based
     Specification together to form an integrated software design
     platform for developing software components whose design
     (implementation) would be formally verified for correctness with
     respect to its specification. Other general correctness properties
     such as freedom from deadlocks, non-determinism, incomplete cases,
     etc. would also be verified. Verification would be performed by
     automatically translating Sequence-based specifications into
     semantically equivalent CSP process algebra and then applying the
     model-checking engine FDR2. After verification was completed,
     semantically equivalent source code would be generated in one
     of several supported high-level languages.

     These ideas were developed further together with Philippa Hopcroft
     and in 2003 a company was founded to develop a commercial
     implementation of a development platform based on these ideas. In
     this talk, I will present an overview of the development platform
     and the technologies used. I will then discuss the experience
     gained during 10 years of trying to introduce this approach into
     industry and the lessons learned along the way.

Research Presentations

The following is the list of full research papers that will be
presented at AVoCS 2014. The complete program is available at
http://fmt.cs.utwente.nl/conferences/avocs2014/program.php

Jan Friso Groote, Remco Van Der Hofstad and Matthias Raffelsieper.
   On the Random Structure of Behavioural Transition Systems

Paolo Arcaini, Angelo Gargantini and Elvinia Riccobene.
   Using SMT for dealing with nondeterminism in ASM-based runtime
   verification

Jingshu Chen, Marie Duflot and Stephan Merz.
   Analyzing Conflict Freedom for Multithreaded Programs with Time
   Annotations

Morteza Mohaqeqi, Mohammadreza Mousavi and Walid Taha.
   Conformance Testing of Cyber-Physical Systems: A Comparative Study

Petr Ročkai, Jiří Barnat and Luboš Brim.
   Model Checking C++ with Exceptions

Leo Hatvani, Alexandre David, Cristina Seceleanu and Paul Pettersson.
   Adaptive Task Automata with Earliest-Deadline-First Scheduling

Sven Reimer, Matthias Sauer, Paolo Marin and Bernd Becker.
   QBF with Soft Variables

Adisak Intana, Michael Poppleton and Geoff Merrett.
   A Formal Co-Simulation Approach for Wireless Sensor Network
   Development

John Mullins and Béatrice Bérard.
   Verification of Information Flow Properties under Rational Observation

Jeremy Sproston.
   Exact and Approximate Abstraction for Classes of Stochastic Hybrid
   Systems

Ernst Moritz Hahn, Arnd Hartmanns and Holger Hermanns.
   Reachability and Reward Checking for Stochastic Timed Automata

Renaud De Landtsheer, Christophe Ponsard, Nicolas Devos, Bénédicte
Moriau and Guy Anckaerts.
   A Constraint-Solving Approach for Achieving Minimal-Reset Transition
   Coverage of Smartcard Behaviour

Ali Jafari, Ehsan Khamespanah, Marjan Sirjani and Holger Hermanns.
   Performance Analysis of Distributed and Asynchronous Systems using
   Probabilistic Timed Actors

Steering Committee

   Michael Goldsmith, University of Oxford, U.K.
   Stephan Merz, INRIA Nancy & LORIA, France
   Markus Roggenbach, Swansea University, U.K.

Organization Committee

   Marieke Huisman
   Wojciech Mostowski (publicity chair)
   Jaco van de Pol

--

-- 
Wojciech Mostowski
University of Twente
Formal Methods and Tools, EWI
EWI-FMT, P.O. Box 217, 7500AE Enschede, The Netherlands
e-mail: w.mostowski <at> utwente.nl
www: http://wwwhome.ewi.utwente.nl/~mostowskiwi/
tel: +31-53-489 3640
fax: +31-53-489 3247
_______________________________________________
Concurrency mailing list
Concurrency <at> listserver.tue.nl
http://listserver.tue.nl/mailman/listinfo/concurrency
Marco Bernardo | 4 Sep 18:25 2014
Picon

JLAMP special issue on Open Problems in Concurrency Theory

JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

SPECIAL ISSUE ON OPEN PROBLEMS IN CONCURRENCY THEORY

CALL FOR PAPERS

* Aims and Scope

This special issue of the Journal of Logical and Algebraic Methods in Programming is
devoted to the themes of the Research Seminar on Open Problems in Concurrency Theory,
which took place in June 2014 in Bertinoro, Italy, and was co-sponsored by
the IFIP Working Group 1.8 (see http://opct2014.cs.vu.nl/ for more details).

This is an open call for papers, therefore both participants of the research seminar
and other authors are encouraged to submit their contributions. Submissions are invited
in the field of concurrency theory; specific topics include, but are not limited to,
the following:

- Models of concurrency
- Process calculi
- Behavioral relations and metrics
- Expressiveness
- Programming languages and types
- Quantitative and security aspects
- Verification, testing, and synthesis

Papers surveying important open problems in concurrency theory are also welcome.

* Submission Guidelines

We expect original submissions of 20-30 pages, which present high-quality contributions
that have not been previously published in another journal and that are not simultaneously
submitted for publication elsewhere. Longer papers will be considered if there is a clear
justification for why additional pages are necessary; prospective authors should contact
the guest editors to discuss this.

Each paper will undergo a thorough evaluation by at least two reviewers. The authors will
have some time to incorporate the comments of the reviewers and submit a revised version
of their papers, which will be evaluated again by the reviewers to make a final decision.

Submissions will be handled through the Elsevier Editorial System (EES) and can be uploaded
from the JLAMP webpage (http://ees.elsevier.com/jlamp/). Authors must select "SI: OPCT 2014"
when they reach the "Article Type" step in the submission process. Contributions should be
typeset in PDF format and comply with the JLAMP author guidelines. Accepted manuscripts
can be posted to arXiv.

* Important Dates

Submission of papers:    November 15, 2014
First review decision:   February 28, 2015
Revision due:            April 30, 2015
Acceptance notification: May 31, 2015
Final manuscript due:    June 30, 2015
Expected publication:    July 31, 2015

* Guest Editors

Marco Bernardo
University of Urbino, Italy

Daniel Gebler
Free University of Amsterdam, The Netherlands

Michele Loreti
University of Firenze, Italy
_______________________________________________
Concurrency mailing list
Concurrency@...
http://listserver.tue.nl/mailman/listinfo/concurrency

Lars Michael Kristensen | 4 Sep 13:09 2014
Picon

PhD position in model-driven and component-based software engineering at Bergen University College, Norway

Bergen University College, Faculty of Engineering and Business Administration, has an open position for a PhD research fellow in computer science/informatics focusing on model-driven and component-based software engineering. The PhD research fellow will be affiliated with the Department of Computing, Mathematics and Physics, and be part of Bergen University College’s IT-oriented strategic research programme on ICT engineering. The ICT engineering programme currently includes 17 permanent professors and associate professors, and several PhD candidates. The department is responsible for bachelor programmes in software engineering and information technology, as well as a master’s programme in software engineering.

The PhD project will span one or more of the following areas, depending on the qualifications and interests of the successful applicant.

-          Process-aware tools and techniques for model-driven software engineering with UML and domain-specific modelling languages;

-          Multi-domain modelling languages, including integration of behavioral and structural models in domains such as software, robotics, and sensor systems;

-          Foundation of model transformations, including co-evolution of model transformations, bi-directional model transformations, and deep meta-modelling.

Bergen University College has an internationally active research group working on model-based software engineering and software verification, and is conducting research ranging from theoretical foundations to computer tools and technology transfer aimed at the practical application of MDE and software verification addressing the challenges in modern software development. The successful applicant must have earned a master's degree or equivalent in informatics/ computer science or in a closely related field, or have submitted the master's thesis before the application deadline.

 

For further information, see: http://hib.easycruit.com/vacancy/1242879/41311?iso=no

 

Lars Michael Kristensen, Professor, PhD

Department of Computing; Mathematics, and Physics

Faculty of Engineering and Business Administration

Bergen University College, Bergen, Norway

Email: lmkr [ at ] hib.no

Web: home.hib.no/ansatte/lmkr

 

 

_______________________________________________
Concurrency mailing list
Concurrency@...
http://listserver.tue.nl/mailman/listinfo/concurrency
Matthias Weidlich | 27 Aug 22:46 2014
Picon

Call for Participation - WS-FM:FASOCC 2014 - Web Services and Formal Methods

#####################################################################

Call for Participation

WS-FM:FASOCC 2014

11th International Workshop on Web Services and Formal Methods:
Formal Aspects of Service-Oriented and Cloud Computing

11th - 12th September, 2014

NEW LOCATION: Eindhoven, The Netherlands

http://wsfm2014.haifa.ac.il/

#####################################################################

You are kindly invited to participate in the 11th International Workshop
on Web Services and Formal Methods: Formal Aspects of Service-Oriented
and Cloud Computing (WS-FM:FASOCC 2014). The aim of the WS-FM:FASOCC
workshop series is to bring together researchers working on SOC, cloud
computing, and formal methods in order to catalyse fruitful
collaboration. The scope of the workshop is not only limited to
technological aspects. In fact, the workshop series has a strong
tradition of attracting submissions on formal approaches to enterprise
systems modelling in general, and business process modelling in particular.

As in previous years, the workshop is co-located to the International
Conference on Business Process Management (BPM 2014). After it was
decided to relocate BPM 2014 from Haifa, Israel to Eindhoven, The
Netherlands, WS-FM:FASOCC 2014 will also take place in Eindhoven, 11th -
12th September, 2014.

The online registration for WS-FM:FASOCC is available at
http://bpm2014.haifa.ac.il/practical-details/registration

############################
Programme
############################

WS-FM:FASOCC will run from 11th September (afternoon) until 12th
September (noon). The full programme is available at
http://wsfm2014.haifa.ac.il/?page_id=19

Keynotes

 * Verification of Data-Aware Processes
   Giuseppe De Giacomo, Sapienza Univ. Roma, Italy

 * Choreographic Programming
   Fabrizio Montesi, University of Southern Denmark, Denmark

Research paper presentations

 * Paolo Arcaini, Roxana – Maria Holom and Elvinia Riccobene
   Modeling and formal analysis of a client-server application for
   Cloud services

 * Abel Armas, Marlon Dumas, Luciano Garcia-Banuelos and Artem
   Polyvyanyy
   On the Suitability of Generalized Behavioral Profiles for Process
   Model Comparison

 * Cinzia Di Giusto and Jorge A. Perez
   An Event-Based Approach to Runtime Adaptation in Communication
   Centric Systems

 * Marco Montali and Andrey Rivkin
   Formal Verification of Petri Nets with Names

_______________________________________________
Concurrency mailing list
Concurrency@...
http://listserver.tue.nl/mailman/listinfo/concurrency

Wojciech Mostowski | 26 Aug 15:26 2014
Picon
Picon

AVoCS 2014: 2nd Call for Participation (early registration by September 1st)

(Apologies for multiple copies)

**********************************************************************

Call for Participation

14th Automated Verification of Critical Systems (AVoCS) 2014 Workshop

http://www.utwente.nl/avocs2014

24-26th September, 2014

University of Twente, Netherlands

**********************************************************************

Deadlines Approaching

Early registration for AVoCS 2014 closes on 1st of September!

Call for Participation

The aim of Automated Verification of Critical Systems (AVoCS) 2014 is
to contribute to the interaction and exchange of ideas among members
of the international research community on tools and techniques for
the verification of critical systems. The subject is to be interpreted
broadly and inclusively. It covers all aspects of automated
verification, including model checking, theorem proving, SAT/SMT
constraint solving, abstract interpretation, and refinement pertaining
to various types of critical systems which need to meet stringent
dependability requirements (safety-critical, business-critical,
performance-critical, etc.). Contributions that describe different
techniques, or industrial case studies are encouraged. The technical
programme will consist of invited and contributed talks and also allow
for short presentations of research ideas. The workshop will be
relatively informal, with an emphasis on discussion.

AVoCS topics include (but are not limited to)

     Model Checking
     Automatic and Interactive Theorem Proving
     SAT, SMT or Constraint Solving for Verification
     Abstract Interpretation
     Specification and Refinement
     Requirements Capture and Analysis
     Verification of Software and Hardware
     Specification and Verification of Fault Tolerance and Resilience
     Probabilistic and Real-Time Systems
     Dependable Systems
     Verified System Development
     Industrial Applications

Thanks to Formal Methods Europe (http://www.fmeurope.org/), we offer a
financial support for students registering for AVoCS in the form of a
registration fee waiver (full or partial). Because our financial support
is limited, we ask the students that would like to take the advantage of
this support to submit a short application (deadline August 14th). The
details on how to apply can be found on the AVoCS 2014 webpage
(http://www.utwente.nl/avocs2014).

AVoCS 2014 is coorganised and colocated with SPES_XT Summer School
on Model-based design and analysis of cyber-physical systems:

http://spes2020.informatik.tu-muenchen.de/summerschool2014.html

A registration reduction is offered for participants attending both
events.There are still places free for the prospective summer school 
participants.

The workshop will have three invited speakers:

   Laura Kovacs (Chalmers, Sweden) will speak about automated assertion
     generation.
   Alastair Donaldson (Imperial College, U.K.) will speak about
     verification of OpenCL kernels.
   Guy Broadfoot (U.K.) will speak about fighting the battle to get
     industry to adopt formal based tools.

Important Dates

   Student grant application: 14th August 2014
   Early registration: 1st September 2014

   Workshop: 24-26th September 2014 (2.5 days, ends 26th lunchtime)

Registration and Hotel Details

All the details on how to register and pay are to be found at the 
workshop page at
http://fmt.cs.utwente.nl/conferences/avocs2014/register.php.
Hotel information is to be found at
http://fmt.cs.utwente.nl/conferences/avocs2014/local.php
(note that the special price for the last hotel will also expire on
September 1st).

Research Presentations

The following is the list of full research papers that will be presented at
AVoCS 2014:

Jan Friso Groote, Remco Van Der Hofstad and Matthias Raffelsieper.
   On the Random Structure of Behavioural Transition Systems

Paolo Arcaini, Angelo Gargantini and Elvinia Riccobene.
   Using SMT for dealing with nondeterminism in ASM-based runtime
   verification

Jingshu Chen, Marie Duflot and Stephan Merz.
   Analyzing Conflict Freedom for Multithreaded Programs with Time
   Annotations

Morteza Mohaqeqi, Mohammadreza Mousavi and Walid Taha.
   Conformance Testing of Cyber-Physical Systems: A Comparative Study

Petr Ročkai, Jiří Barnat and Luboš Brim.
   Model Checking C++ with Exceptions

Leo Hatvani, Alexandre David, Cristina Seceleanu and Paul Pettersson.
   Adaptive Task Automata with Earliest-Deadline-First Scheduling

Sven Reimer, Matthias Sauer, Paolo Marin and Bernd Becker.
   QBF with Soft Variables

Adisak Intana, Michael Poppleton and Geoff Merrett.
   A Formal Co-Simulation Approach for Wireless Sensor Network
   Development

John Mullins and Béatrice Bérard.
   Verification of Information Flow Properties under Rational Observation

Jeremy Sproston.
   Exact and Approximate Abstraction for Classes of Stochastic Hybrid
   Systems

Ernst Moritz Hahn, Arnd Hartmanns and Holger Hermanns.
   Reachability and Reward Checking for Stochastic Timed Automata

Renaud De Landtsheer, Christophe Ponsard, Nicolas Devos, Bénédicte
Moriau and Guy Anckaerts.
   A Constraint-Solving Approach for Achieving Minimal-Reset Transition
   Coverage of Smartcard Behaviour

Ali Jafari, Ehsan Khamespanah, Marjan Sirjani and Holger Hermanns.
   Performance Analysis of Distributed and Asynchronous Systems using
   Probabilistic Timed Actors

Steering Committee

   Michael Goldsmith, University of Oxford, U.K.
   Stephan Merz, INRIA Nancy & LORIA, France
   Markus Roggenbach, Swansea University, U.K.

Organization Committee

   Marieke Huisman
   Wojciech Mostowski (publicity chair)
   Jaco van de Pol

--

-- 
Wojciech Mostowski
University of Twente
Formal Methods and Tools, EWI
EWI-FMT, P.O. Box 217, 7500AE Enschede, The Netherlands
e-mail: w.mostowski <at> utwente.nl
www: http://wwwhome.ewi.utwente.nl/~mostowskiwi/
tel: +31-53-489 3640
fax: +31-53-489 3247
_______________________________________________
Concurrency mailing list
Concurrency <at> listserver.tue.nl
http://listserver.tue.nl/mailman/listinfo/concurrency
Jiri Srba | 25 Aug 08:22 2014
Picon
Picon

Postdoctoral Researcher Position in Embedded Systems, Aalborg University, Denmark

Postdoctoral Researcher Position in Embedded Systems

at CISS Competence Center on Embedded Software Systems, Aalborg  University, Denmark.

The distributed and embedded systems group of prof. Kim G. Larsen  (Aalborg University, Denmark) 
is seeking qualified applicants for a postdoctoral researcher position connected to the EU project 
CASSTING  (http://www.cassting-project.eu/) on Collective Adaptive Systems Synthesis with 
Non-Zero-Sum Games. The researcher will be involved in adapting abstract games and control 
strategies into an executable code on various platforms provided by the industrial partners of the 
CASSTING project. The principal investigators involved in the project are prof. Kim G. Larsen, 
assoc. prof. Arne Skou and assoc. prof. Jiri Srba. Researchers with the interest in applying formal 
methods into industrial case studies with a PhD in one of the following areas are welcome to apply.

* Formal methods, model checking, verification and control synthesis.

* Game theory, control theory, hybrid and real-time systems.

* Programming languages and program analysis for embedded software.

A successful applicant will get the possibility to work in a creative international environment 
and conduct a highly competitive research on a global scale. Within the research there are numerous 
opportunities to cooperate with highly recognized national and international partners.
There is also the possibility to gain valuable experience in the emerging field of energy optimisation 
of distributed embedded systems, in terms of new theoretical models and methods and in prototype systems.

The candidate must hold a PhD degree with a top performance and have a track record in conducting 
original competitive scientific research and publishing the results in reputable conferences and
scientific 
journals. Maturity, self-motivation and the ability to work both independently and as a team player in
local 
and international research teams are expected. Experience with software development, for example 
verification/analysis tool prototypes, is very welcome. We prefer to hire an individual with a good
balance 
between a solid theoretical background and a practical experience in software development. Good English 
language skills are mandatory.

The position is initially offered for the period of one year, starting as soon as possible and latest in the
first 
quarter of 2015. A competitive salary and social benefits will be offered.

Interested candidates may send further questions and a short statement of research interests, 
including their CV, to the Director of CISS, prof. Kim Guldstrand Larsen (kgl@...).

_______________________________________________
Concurrency mailing list
Concurrency@...
http://listserver.tue.nl/mailman/listinfo/concurrency

Francesco tiezzi | 29 Aug 10:01 2014
Picon

ACM SAC 2015: Track on Coordination Models, Languages and Applications - Final CfP

**************************************************************************************
                  Coordination Models, Languages and Applications
        Special Track of the 30th ACM Symposium on Applied Computing (SAC'15)        
                           http://sac2015.apice.unibo.it/
                                            
                                April 13 - 17, 2015
                                  Salamanca, Spain

**************************************************************************************

Building on the success of the fifteenth previous editions (1998-2014), a special 
track on coordination models, languages and applications will be held at SAC 2015. 
Over the last decade, we have witnessed the emergence of models, formalisms and 
mechanisms to describe concurrent and distributed computations and systems based on 
the concept of coordination. The purpose of a coordination model is to enable the 
integration of a number of possibly heterogeneous components (processes, objects, 
agents, services) in such a way that the resulting ensemble can execute as a whole, 
forming a distributed software system with desired characteristics and functionalities. 
This is done in terms of coordination abstractions, languages, algorithms, mechanisms, 
and middleware specifically focused on the management of component interaction.

The coordination paradigm crosscuts a number of contemporary software engineering 
approaches and fields, which we aim to cross-fertilize and bring contribution to, 
including in particular: multi-agent systems, self-adaptative and self-organising 
systems, service-oriented architectures, component-based systems, and all related 
middleware platforms. 

The Special Track on Coordination Models, Languages and Applications takes a 
deliberately broad view of what constitutes coordination. Accordingly, major topics 
of interest this year will include:

   - Novel models, languages, formalisms, programming and implementation techniques
   - Coordination technologies, systems and infrastructures
   - Applications
   - Middleware platforms
   - Formal aspects (semantics, reasoning, verification)
   - Software architectures and software engineering techniques
   - Coordination of multi-agent systems, including mobile agents, intelligent agents, 
     and agent-based simulations
   - Internet, Web, and pervasive computing systems coordination
   - Languages for service description and composition
   - Models, frameworks and tools for Group Decision Making
   - All aspects related to Cooperative Information Systems (e.g. workflow management, 
     CSCW)
   - Configuration and Architecture Description Languages
   - Self-organising, self-adaptive and nature-inspired coordination approaches
   - Relationship with other computational models such as object oriented, declarative 
     (functional, logic, constraint) programming or their extensions with coordination 
     capabilities
   - Coordination models and specification in Service-Oriented Architectures, Web Service 
     technologies (orchestration, choreography, etc.),Pervasive Computing and Autonomic 
     Computing
   - Policy-based approaches to coordination and self-adaptation

We also welcome papers on practical systems or novel applications that are aimed at 
reaching coordination between components and services, especially if those systems and 
novel applications challenge existing ideas and models.

In previous editions, CM Special Track organisers have been inviting authors of selected 
papers for special issues in high impact journals, such as, ACM Transactions on Autonomous 
and Adaptive Systems (TAAS) and Science of Computer Programming (SCP).  


------------------------
   Important Dates
------------------------

     Sept 12, 2014: Paper submission 
     Nov 17, 2014: Author notification
     Dec 8, 2014: Camera-Ready Copy
     Dec 15 2014: Author Registration


------------------------
   Program Co-Chairs
------------------------

Mirko Viroli
    Alma Mater Studiorum - Universita' di Bologna

Jose Luis Fernandez-Marquez
    University of Geneva
    
Francesco Tiezzi    
    IMT Institute for Advanced Studies Lucca


----------------------------------------
   Program Committee Members
----------------------------------------

Farhad Arbab, CWI Amsterdam and Leiden University, Netherlands
Jacob Beal, BBN Technologies, USA 
Ferruccio Damiani, University of Torino, Italy
Wolfgang De Meuter, Vrije Universiteit Brussel, Belgium
Rocco De Nicola, Institute for Advanced Studies Lucca, Italy 
Simon Dobson, University of St Andrews, Scotland 
eva Kühn, Vienna University of Technology, Austria
Hung La, Rutgers University, USA 
Flemming Nielson, Technical University of Denmark
Michael O'Grady, University College Dublin, Ireland
Andrea Omicini, University of Bologna, Italy
Manuel Oriol, University of York, UK
António Porto, University of Porto, Portugal
Rosario Pugliese, University of Firenze, Italy
Alessandro Ricci, University of Bologna, Italy
Juan Antonio Rodriguez Aguilar, IIIA-CSIC, Spain
Michael Ignaz Schumacher, University of Applied Sciences, Switzerland
Marjan Sirjani, Reykjavik University, Iceland
Yasuyuki Tahara, National Institute of Informatics, Japan
Robert Tolksdorf, Freie Universitaet Berlin, Germany
Giuseppe Valetto, Drexel University, USA 
Eiko Yoneki, University of Cambridge Computer Laboratory, UK
Nobuko Yoshida, Imperial College London, UK
George Wells, Rhodes University, South Africa
Danny Weyns, Linnaeus University, Sweden
Pawel T. Wojciechowski, Poznan University of Technology, Poland



---------------------
   Proceedings
---------------------

Papers accepted for the Special Track on Coordination Models, Languages and 
Applications will be published by ACM both in the SAC 2015 proceedings and in 
the Digital Library.



-------------------------------------
   Paper submission and format
-------------------------------------

All papers should represent original and previously unpublished works that 
currently are not under review in any conference or journal.

The author(s) name(s) and address(es) must NOT appear in the body of the paper,
and self-reference should be in the third person. This is to facilitate blind 
review. Only the title should be shown at the first page without the author's 
information.

Submitted papers must be no longer than 6 pages and in the ACM two-column page
format (doc template, pdf template, latex template). It will be possible to have 
up to 2 extra pages in the proceeding at a charge of $80 per page (total 8 pages 
maximum).

Paper registration is required, allowing the inclusion of the paper/poster in the
conference proceedings. An author or a proxy attending SAC MUST present the paper. 
This is a requirement for the paper/poster to be included in the ACM/IEEE digital 
library. No-show of scheduled papers and posters will result in excluding them 
from the ACM/IEEE digital library.

Submission is entirely automated via the STAR Submission System, which is available 
from the main SAC Web Site: https://www.softconf.com/d/sac2015/.


-------------------------
   Poster Sessions
-------------------------

Papers that received high reviews (that is acceptable by reviewer standards) but 
were not accepted due to space limitation can be invited for the poster session. 
Poster should be not longer than 2 pages plus 1 extra page at $80. The poster 
session procedures and details will be posted on SAC 2015 website as soon as they 
become available.


------------------------------------------------
   Student research abstracts competition
------------------------------------------------

Graduate students are invited to submit research abstracts (minimum of 2-page and 
maximum of 4-page) following the instructions published at SAC 2015 website. 
Submission of the same abstract to multiple tracks is not allowed.
    
_______________________________________________
Concurrency mailing list
Concurrency@...
http://listserver.tue.nl/mailman/listinfo/concurrency

Gmane