1,720,989 research outputs found
Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems
No full textThis volume contains the proceedings of the Eleventh Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013), held in Rome, Italy, on 23 and 24 March, 2013. QAPL 2013 was a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2013).
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 design of probabilistic, real-time and quantum languages, and the definition of semantical models for such languages;
the discussion of methodologies for the analysis of probabilistic and timing properties (e.g. se- curity, safety, scheduability) and of other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g. worst-case mem- ory/stack/cache requirements);
the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);
applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, and to any other domain involving quantitative issues.
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), Saarbru _cken, Germany (QAPL 2011) and Tallinn, Estonia (QAPL 2012).
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, 2011 and 2012 are published as volume 28, volume 57, and volume 85, respectively, of the 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 in preparation.
The workshop programme included two QAPL keynote presentations: Alessandra Di Pierro (University of Verona, Italy): Probabilistic static analysis and security trade-offs, and Paolo Zuliani (University of Newcastle, UK): Statistical Model Checking for Cyber-Physical Systems as well as two keynotes shared with MLQA: Martin Franzle (University of Oldenburg, Germany): A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems, and Flemming Nielson (Technical University of Denmark): Guarding against Denial of Service Attacks.
Furthermore, the Program Committee of QAPL 2013 which comprised of:
Alessandro Aldini, University of Urbino, Italy
Christel Baier, Technical University of Dresden, Germany
Ezio Bartocci, Technical University of Vienna, Austria
Marco Bernardo, University of Urbino, Italy
Nathalie Bertrand, INRIA Rennes Bretagne Atlantique, France
Luca Bortolussi (Co-chair), University of Trieste, Italy
Tomas Brazdil, Masaryk University, Czech Republic
Kostas Chatzikokolakis, CNRS, France
Pedro D'Argenio, University of Cordoba, Argentina
Alessandra Di Pierro, University of Verona, Italy
Vashti Galpin, University of Edinburgh, UK
Joost-Pieter Katoen, RWTH Aachen, Germany
Richard Hayden, Imperial College, London
Holger Hermanns, Saarland University, Germany
Mieke Massink, Italian National Research Council - ISTI, Pisa, Italy
Annabelle McIver, Macquarie University, Australia
Gethin Norman, University of Glasgow, UK
David Parker, Oxford University, UK
Anne Remke, University of Twente, the Netherlands
Jeremy Sproston, University of Turin, Italy
Mirco Tribastone, LMU Munich, Germany
Franck van Breugel, York University, Canada
Herbert Wiklicky (Co-chair), Imperial College London, UK
Verena Wolf, Saarland University, Germany
selected 9 regular papers and 3 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 here.
We would like to thank the QAPL steering committee for its support, the ETAPS 2013 organisers and furthermore all the authors, the invited speakers, the programme committee and the external referees for their valuable contributions.
May 2013
Luca Bortolussi and Herbert Wiklicky
Program Co-chair
Coordination Models and Languages. Proc. 8th International Conference, COORDINATION 2006
No full textAtti di convegno internazional
Probabilistic Lambda-calculus and Quantitative Program Analysis
No full textWe show how the framework of probabilistic abstract interpretation can be applied to statically analyse a probabilistic version of the {lambda}-calculus. The resulting analysis allows for a more speculative use of its outcomes based on the consideration of statistically defined quantities. After introducing a linear operator based semantics for our probabilistic {lambda}-calculus {Lambda}p, and reviewing the framework of abstract interpretation and strictness analysis, we demonstrate our technique by constructing a probabilistic (first-order) strictness analysis for {Lambda}p
Quantitative Static Analysis of Distributed Systems
No full textWe introduce a quantitative approach to the analysis of distributed systems which relies on a linear operator based network semantics. A typical problem in a distributed setting is how information propagates through a network, and a typical qualitative analysis is concerned with establishing whether some information will eventually be transmitted from one node to another node in the network. The quantitative approach we present allows to obtain additional information such as an estimation of the probability that some data is transmitted within a given interval of time. We formalise situations like this using a probabilistic version of a process calculus which is the core of KLAIM, a language for distributed and mobile computing based on interactions through distributed tuple spaces. The analysis we present exploits techniques based on Probabilistic Abstract Interpretation and is characterised by compositional aspects which greatly simplify the inspection of the nodes interaction and the detection of the information propagation through a computer network
Program Analysis Probably Counts
No full textIn this paper we start by reviewing both classical and probabilistic/quantitative approaches to program analysis. We shall provide a comparison of the two approaches. We shall use a simple information flow analysis to exemplify the classical approach. The existence of covert information flows through timing channels are difficult to detect using classical techniques; we show how such problems can be addressed using probabilistic techniques
Approximate Non-Interference
No full textWe address the problem of characterising the security of a program against unauthorised information flows. Classical approaches are based on non-inter\-ference models which depend ultimately on the notion of process equivalence. In these models confidentiality is an absolute property stating the absence of any illegal information flow. We present a model in which the notion of non-interference is approximated in the sense that it allows for some exactly quantified leakage of information. This is characterised via a notion of process similarity which replaces the indistinguishability of processes by a quantitative measure of their behavioural difference. Such a quantity is related to the number of statistical tests needed to distinguish two behaviours. We also present two semantics-based analyses of approximate non-interference and we show that one is a correct abstraction of the other
A systematic approach to probabilistic pointer analysis
No full textWe present a formal framework for syntax directed probabilistic program analysis. Our focus is on probabilistic pointer analysis. We show how to obtain probabilistic points-to matrices and their relational counterparts in a systematic way via Probabilistic Abstract Interpretation (PAI). The analysis is based on a non-standard semantics for a simple imperative language which corresponds to a Discrete-Time Markov Chain (DTMC). The generator of this DTMC is constructed by composing (via tensor product) the probabilistic control flow of the program and the data updates of the different variables at individual program points. The dimensionality of the concrete semantics is in general prohibitively large but abstraction (via PAI) allows for a drastic (exponential) reduction of size
Approximate Confinement under Uniform Attacks
No full textWe are concerned to give certain guarantees about the security of a system. We identify two kinds of attack: the internally scheduled attack (exemplified by Trojan Horse attacks) and externally scheduled attacks (exemplified by timing attacks). In this paper we focus on the latter. We present a semantic framework for studying such attacks in the context of PCCP, a simple process algebra with a constraint store. We show that a measure of the efficacy of an attacker can be determined by considering its observable behaviour over the "average" store of the system (for some number of steps). We show how to construct an analysis to determine the average store using the technique of probabilistic abstract interpretation
Probabilistic Abstract Interpretation and Statistical Testing
No full textAlthough generally too weak to guarantee correctness, testing is an indispensable technique for the validation of reactive systems. Abstract Interpretation has been used to overcome some of the problems associated with testing such as the termination of a program run within an acceptable interval of time. We propose the use of Probabilistic Abstract Interpretation for measuring the error made in the evaluation of the reliability of systems via Monte-Carlo testing. The problem we consider is to determine the probability that a reactive system's response falls within a certain set of possible outputs, i.e. that it passes a certain test. As Monte-Carlo testing of the concrete system is not always feasible, tests can be performed instead on an abstract system. This abstraction introduces a further approximation which must be taken into account in the estimation of the error made by testing. The problem is to find out how much the expectation value (or average) of the abstract system differs from the one of the concrete system. We show how to measure such difference by lifting the abstraction to a probabilistic abstract interpretation
Measuring the confinement of probabilistic systems
No full textAbstractIn this paper we lay the semantic basis for a quantitative security analysis of probabilistic systems by introducing notions of approximate confinement based on various process equivalences. We re-cast the operational semantics classically expressed via probabilistic transition systems (PTS) in terms of linear operators and we present a technique for defining approximate semantics as probabilistic abstract interpretations of the PTS semantics. An operator norm is then used to quantify this approximation. This provides a quantitative measure ɛ of the indistinguishability of two processes and therefore of their confinement. In this security setting a statistical interpretation is then given of the quantity ɛ which relates it to the number of tests needed to breach the security of the system
- …
