Quantitative Aspects of Programming Languages and Systems over the past $2^4$ years and beyond

Abstract

Quantitative aspects of computation are related to the use of both physical and mathematical quantities, including time, performance metrics, probability, and measures for reliability and security. They are essential in characterizing the behaviour of many critical systems and in estimating their properties. Hence, they need to be integrated both at the level of system modeling and within the verification methodologies and tools. Along the last two decades a variety of theoretical achievements and automated techniques have contributed to make quantitative modeling and verification mainstream in the research community. In the same period, they represented the central theme of the series of workshops entitled Quantitative Aspects of Programming Languages and Systems (QAPL) and born in 2001. The aim of this survey is to revisit such achievements and results from the standpoint of QAPL and its community.

arXiv commentIn Proceedings QAPL 2019, arXiv:2001.06163

References in corpus (50)

• UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata
• CARMA: Collective Adaptive Resource-sharing Markovian Agents
• A new tool for the performance analysis of massively parallel computer systems
• Stochastic Calculus of Wrapped Compartments
• Logical Characterization of Bisimulation Metrics
• Probabilistic Model-Based Safety Analysis
• Computing Distances between Probabilistic Automata
• Distances for Weighted Transition Systems: Games and Properties
• Two-Player Reachability-Price Games on Single-Clock Timed Automata
• Hybrid performance modelling of opportunistic networks
• Stochastically timed predicate-based communication primitives for autonomic computing
• Probabilistic Concurrent Kleene Algebra
• Quantitative Security Analysis for Multi-threaded Programs
• An expectation transformer approach to predicate abstraction and data independence for probabilistic programs
• Weak Markovian Bisimulation Congruences and Exact CTMC-Level Aggregations for Concurrent Processes
• Optimal Time-Abstract Schedulers for CTMDPs and Markov Games
• Divide and Conquer: Variable Set Separation in Hybrid Systems Reachability Analysis
• HYPE with stochastic events
• A non-local method for robustness analysis of floating point programs
• Logical Characterization of Trace Metrics
• MELA: Modelling in Ecology with Location Attributes
• Patch-based Hybrid Modelling of Spatially Distributed Systems by Using Stochastic HYPE - ZebraNet as an Example
• Model Checking CSL for Markov Population Models
• Quantitative Information Flow for Scheduler-Dependent Systems
• Performance Evaluation of Components Using a Granularity-based Interface Between Real-Time Calculus and Timed Automata
• The Complexity of Robot Games on the Integer Line
• Analysis of Non-Linear Probabilistic Hybrid Systems
• On-the-fly Uniformization of Time-Inhomogeneous Infinite Markov Population Models
• Extended Differential Aggregations in Process Algebra for Performance and Biology
• Solving Stochastic Büchi Games on Infinite Arenas with a Finite Attractor
• MeGARA: Menu-based Game Abstraction and Abstraction Refinement of Markov Automata
• Testing Reactive Probabilistic Processes
• Time Delays in Membrane Systems and Petri Nets
• The Spectrum of Strong Behavioral Equivalences for Nondeterministic and Probabilistic Processes
• Expected-Delay-Summing Weak Bisimilarity for Markov Automata
• Semiring-based Specification Approaches for Quantitative Security
• Limit Your Consumption! Finding Bounds in Average-energy Games
• A Definition Scheme for Quantitative Bisimulation
• Automated Verification of Quantum Protocols using MCMAS
• Indexed Labels for Loop Iteration Dependent Costs
• Modal Specifications for Probabilistic Timed Systems
• Probabilistic Output Analysis by Program Manipulation
• Efficient Checking of Individual Rewards Properties in Markov Population Models
• Design and Optimisation of the FlyFast Front-end for Attribute-based Coordination
• PAWS: A Tool for the Analysis of Weighted Systems
• Measuring Progress of Probabilistic LTL Model Checking
• Language-based Abstractions for Dynamical Systems
• Rooted branching bisimulation as a congruence for probabilistic transition systems
• A Stochastic Broadcast Pi-Calculus
• Injecting Abstract Interpretations into Linear Cost Models