IMPORTANT NOTICE: WORKSHOP HAS BEEN CANCELLED
We are sorry to inform you that on April 18, 2018, due to an insufficient number of submissions, the QAPL 2018 event at FLoC has been cancelled. We apologise for any inconvience this may have caused.
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, and time are first-class citizens.
Topics of interest include (but are by no means 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 solution, symbolic approaches, optimisation methods and their extensions to spatial and spatio-temporal aspects.
- Specification of quantitative properties such as probabilistic model checking and reward structures as well as verification and/or synthesis of systems in relation to quantitative aspects.
- Methodologies and frameworks for the engineering of systems based on quantitative information, such as reliability engineering and software performance engineering.
- Software tools to support the quantitative specification, analysis, verification and programming of systems.
- 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.
Submission
In order to encourage participation and discussion, this workshop solicits two types of submissions - regular papers and presentations:
- 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.
- Presentation reports concern 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 a presentation. Typically, a presentation is based on a paper which recently appeared (or which is going to appear) in the proceedings of another recognised conference, or which has not yet been submitted. 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 style files. Submissions can be made through the EasyChair submission page .
Accepted regular papers will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS). Please use the EPTCS latex style for both your preliminary submission and the camera ready paper.
A special issue in a renowned international journal is planned in case of a sufficient number of high quality submissions.
- Prof. Carlo Ghezzi, Polytechnic University of Milan, Italy
Title: Making Cyber-physical Spaces Dependable through Formal Modelling and Verification
Abstract: 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.
- Prof. Annabelle McIver, Macquarie University, Sydney, Australia
Title: Proving Termination in Probabilistic Programs: New Rules for Difficult Scenarios
Abstract: 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.
Programme Co-Chairs
- Mieke Massink, CNR-ISTI Pisa, IT
- Erik de Vink, Eindhoven University of Technology, NL
- Erika Ábrahám, 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 École Polytechnique FR
- Vincenzo Ciancia, CNR-ISTI Pisa IT
- Josée Desharnais, Université 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, Università di Camerino IT
- Mieke Massink (co-chair), CNR-ISTI IT
- Mohammadreza Mousavi, University of Leicester UK
- David Šafránek, 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