Published: 3rd July 2012
DOI: 10.4204/EPTCS.85
ISSN: 2075-2180

EPTCS 85

Proceedings 10th Workshop on
Quantitative Aspects of Programming Languages and Systems
Tallinn, Estonia, 31 March and 1 April 2012

Edited by: Herbert Wiklicky and Mieke Massink

Preface
Invited Presentation: UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata
Peter Bulychev, Alexandre David, Kim Gulstrand Larsen, Marius Mikučionis, Danny Bøgsted Poulsen, Axel Legay and Zheng Wang
1
Efficient computation of exact solutions for quantitative model checking
Sergio Giro
17
Measuring Progress of Probabilistic LTL Model Checking
Elise Cormie-Bowins and Franck van Breugel
33
Automated Verification of Quantum Protocols using MCMAS
F. Belardinelli, P. Gonzalez and A. Lomuscio
48
A non-local method for robustness analysis of floating point programs
Ivan Gazeau, Dale Miller and Catuscia Palamidessi
63
Quantitative Information Flow as Safety and Liveness Hyperproperties
Hirotoshi Yasuoka and Tachio Terauchi
77
Differential Privacy for Relational Algebra: Improving the Sensitivity Bounds via Constraint Systems
Catuscia Palamidessi and Marco Stronati
92
Hybrid performance modelling of opportunistic networks
Luca Bortolussi, Vashti Galpin and Jane Hillston
106
Weak Markovian Bisimulation Congruences and Exact CTMC-Level Aggregations for Concurrent Processes
Marco Bernardo
122

Preface

This volume contains the proceedings of the Tenth Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2012), held in Tallinn, Estonia, on 31 March and 1 April, 2012. QAPL 2012 was a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2012).

The central theme of the workshop is that of quantitative aspects of computation. These aspects are related to the use of physical quantities (storage space, time, bandwidth, etc.) as well as mathematical quantities (e.g. probability and measures for reliability, security and trust), and play an important (sometimes essential) role in characterising the behaviour and determining the properties of systems. Such quantities are central to the definition of both the model of systems (architecture, language design, semantics) and the methodologies and tools for the analysis and verification of the systems properties. The aim of this workshop is to discuss the explicit use of quantitative information such as time and probabilities either directly in the model or as a tool for the analysis of systems.

In particular, the workshop focuses on:

The history of QAPL starts in 2001, when its first edition was held in Florence, Italy, as a satellite event of the ACM Principles, Logics, and Implementations of high-level programming languages, PLI 2001. The second edition, QAPL 2004, was held in Barcelona, Spain, as a satellite event of ETAPS 2004. Since then, QAPL has become a yearly appointment with ETAPS. In the following years, QAPL was held in Edinburgh, Scotland (QAPL 2005), Vienna, Austria (QAPL 2006), Braga, Portugal (QAPL 2007), Budapest, Hungary (QAPL 2008), York, UK (QAPL 2009), Paphos, Cyprus (QAPL 2010) and Saarbruecken, Germany (QAPL 2011). The proceedings of the workshops upto and including 2009 are published as volumes in Electronic Notes in Theoretical Computer Science (ENTCS). The editions of 2010 and 2011 are published as volume 28 and volume 57, respectively, of Electronic Proceedings in Theoretical Computer Science (EPTCS).

Three special issues of the journal of Theoretical Computer Science are dedicated to the QAPL 2004, QAPL 2006 and QAPL 2010 events, and are published in Volume 346(1), Volume 382(1) and Volume 413(1) respectively. A special issue of the journal of Theoretical Computer Science dedicated to QAPL 2011 and QAPL 2012 is planned.

The workshop programme included three keynote presentations: Kim G. Larsen (Aalborg University, Denmark); Boris Köpf (IMDEA Software Institute, Madrid, Spain) and Jeremy Bradley (Imperial College London, U.K.). Furthermore, the Program Committee of QAPL 2012 which comprised of:

selected 8 regular papers and 4 presentation-only papers. All regular papers were reviewed by at least three reviewers. After the workshop, the authors of regular papers were asked to submit a revised version, incorporating the comments made during the discussion at the workshop, which are included in this volume. The volume also includes an invited paper by one of the keynote speakers (Kim G. Larsen).

We would like to thank the QAPL steering committee for its support, Formal Methods Europe (FME) for their financial support for the speakers, the ETAPS 2012 organisers and furthermore all the authors, the invited speakers, the programme committee and the external referees for their valuable contributions.

June 2012Mieke Massink and Herbert Wiklicky

Program Co-chairs