- 9:00am—10:00am, Keynote
Multi‐Agent Networked Systems with Adversarial Elements.
- 10:00am—11:00am, Kronecker and product form methods
A matrix-free structured solution for Markov Regenerative Processes..
Low-rank tensor methods for communicating Markov processes..
- 11:30am—1:00pm, Hybrid systems
A statistical approach for computing reachability of non-linear and stochastic dynamical systems..
Formal Synthesis and Validation of Inhomogeneous Thermostatically Controlled Loads..
Finite Abstractions of Stochastic Max-Plus-Linear Systems..
- 2:30pm—4:00pm, Mean-field/population analysis
Mean field for performance models with generally distributed-timed transitions..
Mean-Field approximation and Quasi-Equilibrium reduction of Markov Population Models..
On performance of Gossip communication in a crowd-sensing scenario..
- 4:30pm—6:00pm, Models and tools
Probabilistic Model Checking of DTMC Models of User Activity Patterns..
Performance Comparison of IEEE 802.11 DCF and EDCA for Beaconing in Vehicular Networks..
A new GreatSPN GUI for GSPN editing and CSLTA model checking (tool paper)..
The Octave queueing Package (tool paper)..
- 6:30pm—11:00pm, Reception at Villa Bardini
- 9:00am—10:00am, Keynote (joint program with FORMATS)
The Modeling and Analysis of Mixed-Criticality Systems.(University of North Carolina at Chapel Hill).
- 10:00am—11:00am, Simulation
A perfect sampling algorithm of random walks with forbidden arcs..
Modelling Replication in NoSQL Datastores..
- 11:30am—1:00pm, Queueing, debugging, and tools
On queues with general service demands and constant service capacity..
Simulation Debugging and Visualization in the Mobius Modeling Framework..
Scalar: A distributed benchmarking framework for systematic scalability analysis (tool paper)..
Non-Intrusive Scalable Memory Access Tracer (tool paper)..
- 2:30pm—4:00pm, Process algebras and equivalencies
Probabilistic Programming Process Algebra..
PALOMA: A Process Algebra for Located Markovian Agents..
On the Discriminating Power of Testing Equivalences for Reactive Probabilistic Systems: Results and Open Problems..
- 4:30pm—6:00pm, Automata and Markov process theory
Continuity Properties of Distances for Markov Processes..
Deciding the value 1 problem for reachability in 1-clock decision stochastic timed automata..
Decidable Problems for Unary PFAs..
- 8:00pm—11:30pm, Social dinner at Castello dell'Acciaiolo
- 9:00am—10:00am, Keynote (joint program with SAFECOMP)
Quantitative safety assessment: experiments and field measurements.(University of Coimbra).
- 10:00am—11:00am, Fault Injection Techniques (SAFECOMP Session)
A Simulated Fault Injection Framework for Time-Triggered Safety-Critical Embedded Systems..
Rapid Fault-Space Exploration by Evolutionary Pruning..
- 11:30am—1:00pm, Applications, theory, and tools
A Scalable Approach to the Assessment of Storm Impact in Distributed Automation Power Grids..
Compositionality Results for Quantitative Information Flow..
CyberSAGE: A Tool for Automatic Security Assessment of Cyber-Physical Systems (tool paper)..
Tool demonstrations (also during lunch).
- 2:30pm—3:30pm, Keynote
Quantitative Evaluation of Service Dependability in Shared Execution Environments.(Universität Würzburg).
- 3:30pm—4:30pm, Probabilistic Model Checking
Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains..
Accelerating Parametric Probabilistic Verification..
- 5:00pm—6:00pm, Verification & Validation Techniques (SAFECOMP Session)
Safety Validation of Sense and Avoid Algorithms using Simulation and Evolutionary Search..
Debugging with Timed Automata Mutations..