QAPL 2018: second call for papers

                       [Apologies for multiple copies]

**************************************************************************
                        2nd Call for Papers
16th Workshop on Quantitative Aspects of Programming Languages and Systems

                                QAPL 2018

                    Oxford UK, Saturday 14 July 2018
               part of FLoC 2018, affiliated with FM 2018
            http://www1.isti.cnr.it/~Massink/EVENTS/QAPL2018/

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

SCOPE:

The scope of the QAPL workshop is to discuss new developments on the
quantitative evaluation of systems, with an emphasis on quantitative
aspects of computation, broadly construed.

We solicit papers on theory, engineering methodologies, tools, case
studies, and experience reports where quantitative properties such as
bandwidth, cost, energy, memory, performance, probability,
reliability, security, locality, and time are first-class citizens.

TOPICS:

Topics of interest include (but are by no means not limited to):

 * The design of probabilistic, deterministic, hybrid, real-time, and
   quantum languages, and the definition of their semantical models.

 * Quantitative analysis techniques such as simulation, numerical
   approximation, symbolic approaches, and optimisation methods.
   
 * Specification of quantitative properties such as probabilistic
   model checking and reward structures, theory and application of
   spatial and statistical model checking, as well as verification
   and/or synthesis of systems in relation to quantitative aspects.
   
 * Methodologies and frameworks as well as software tools for the
   design, construction, and maintenance of systems based on
   quantitative information, such as reliability engineering and
   software performance engineering.
     
 * Case studies and applications, for instance about coordination
   models, cyber-physical systems, security, self-adaptive systems,
   smart grids, systems of systems as well as natural/physical domains
   such as chemistry and systems biology.
 

INVITED SPEAKERS:

  *  Carlo Ghezzi, Politecnico di Milano IT
     Making Cyber-physical Spaces Dependable through Formal Modelling
     and Verification

     We increasingly live in cyber-physical spaces (CPSs), where physical
     and computational entities are inextricably intertwined. Through
     their interactions complex and critical functionalities emerge.
     A CPS must be dependable, because human life depends on it.
     For example, think of smart buildings, smart transport systems,
     or smart cities. How can design of a CPS guarantee the required
     level of dependability? How can the CPS be managed at run-time in
     face of possible changes? The talk explores the research challenges
     posed by these questions. It also presents promising research directions
     that focus on formally modeling both the requirements, using a
     spatio-temporal logic language, and the CPS and its dynamics, using
     a graph based formalism and graph rewriting rules, and uses model
     checking to verify requirements satisfaction both at design time
     and at run time.

  *  Annabelle McIver, Macquarie University AU
     Proving Termination in Probabilistic Programs: New Rules
     for Difficult Scenarios

     Proving termination of probabilistic programs is an interesting -
     and sometimes puzzling topic. Does the program "Flip a coin until
     heads shows." terminate? Or might it go on forever? The
     more-or-less accepted answer to that question is to ask only for
     "termination with probability one", or equivalently that the
     probability of going on forever is zero (and so can be ignored):
     this is called "almost-sure termination". But even then simple
     programs like the random walker, who moves up and down the number
     line with equal probability, and who can be shown with a simple
     mathematical argument almost surely to return to his starting
     point, causes problems for most termination-proof methods that
     apply to computer programs. Program proofs must be absolutely
     rigorous: and rigour for almost-sure termination turns out to be
     surprisingly tricky. Recently however my colleagues and I have
     devised a probabilistic-termination rule that seems to extend
     most of those extant: it puts together "old" ingredients, like
     "definite progress" and "super martingales" but in a new way. And
     it is amazingly simple: not tricky at all. I will explain its
     main features, sketch why it works (and how it avoids subtle
     traps leading to unsoundness), and illustrate it on intriguing
     examples.

SUBMISSIONS:

In order to encourage participation and discussion, this workshop
solicits two types of submissions - regular papers and presentations:

1. Regular paper: Submissions must be original work, and must not have
   been previously published, nor be under consideration for
   publication elsewhere. Regular paper submission must not exceed
   12 pages (excluding the bibliography). Additional technical material,
   proofs, etc. can be provided in a clearly marked appendix which
   will be read by reviewers at their discretion. Regular papers will
   be reviewed by the PC.

2. Presentation report: this concerns recent or ongoing work on
   relevant topics and ideas, for timely discussion and feedback at
   the workshop. There is no restriction as for previous/future
   publication of the contents of this contributions. Typically, a
   presentation is based on a paper which recently appeared (or which
   is going to appear) in the proceedings of another recognized
   conference, or which has not been submitted yet. The (extended)
   abstract of presentation submissions should not exceed 4
   pages. Presentation reports will be selected by the PC Chairs
   (based on the availability of presentation time).

All submissions must be in PDF format and use the EPTCS LaTeX style
(see http://style.eptcs.org/.) Submissions can be made on the
following website:

    http://www.easychair.org/conferences/?conf=qapl2018

The workshop PC will review all regular paper submissions based on
their relevance, merit, originality, and technical content.
Presentation reports will receive a lightweight review to establish
their relevance for the workshop. The authors of accepted submissions
of both types are expected to present and discuss their work at the
workshop. Accepted regular papers will be published electronically in
the pre-proceedings available during the workshop and after the
workshop in the Electronic Proceedings in Theoretical Computer Science
(EPTCS) as post-proceedings (to be confirmed). Short papers will not
be included in the EPTCS post-proceedings. A special issue related to
QAPL 2018 in an international journal is under consideration.

IMPORTANT DATES:

For regular papers:

   Abstract:      10 April 2018 (AoE, optional)
   Submission:    15 April 2018 (AoE)
   Notification:  15 May 2018
   Final version: (FLoC workshop proceedings) 25 May 2017
   Final version: (EPTCS proceedings): TBA

For presentation reports:

   Submission:     7 May 2018 (AoE)
   Notification:  11 May 2018
   Final version: (FLoC workshop proceedings) 25 May 2017

ORGANISATION:
 
  * Mieke Massink, CNR-ISTI Pisa IT
  * Erik de Vink, Eindhoven University of Technology NL

PROGRAMME COMMITTEE

  * Erika Abraham, RWTH Aachen University DE
  * Alessandro Aldini, University of Urbino "Carlo Bo" IT
  * Nathalie Bertrand, INRIA Rennes FR
  * Luca Bortolussi, University of Trieste IT
  * Konstantinos Chatzikokolakis, CNRS and Ecole Polytechnique FR
  * Vincenzo Ciancia, CNR-ISTI Pisa IT
  * Josee Desharnais, Universite Laval CA
  * Pedro D'Argenio, Universidad Nacional de Cordoba AR
  * Alessandra Di Pierro, Università di Verona IT
  * Christoph Haase, University of Oxford UK
  * Jane Hillston, University of Edinburgh UK
  * Jan Kretinsky, TU Munich DE
  * Michele Loreti, Universita  di Camerino IT
  * Mieke Massink (co-chair), CNR-ISTI IT
  * Mohammadreza Mousavi, University of Leicester UK
  * David Safranek, Masaryk University CZ
  * Jeremy Sproston, University of Turin IT
  * Ana Sokolova, University of Salzburg AT
  * Marielle Stoelinga, University of Twente NL
  * Mirco Tribastone, IMT Lucca IT
  * Erik de Vink (co-chair), Eindhoven University of Technology NL
  * Herbert Wiklicky, Imperial College UK
  * Wang Yi, Uppsala University SE