Conference program
| |||||||||||
|
Sunday session A | top of the page |
9:00-10:30
| Tutorial | building I, room IB110 |
Simulation + Hypothesis Testing for Model Checking Probabilistic Systems
Axel Legay, IRISA/INRIA Rennes, France and
Mahesh Viswanathan, University of Illinois at Urbana-Champaign, USA
PART 1
Axel Legay, IRISA/INRIA Rennes, France and
Mahesh Viswanathan, University of Illinois at Urbana-Champaign, USA
PART 1
10:30-11:00
| Coffee break | building I, first floor |
11:00-12:30
| Tutorial | building I, room IB110 |
Simulation + Hypothesis Testing for Model Checking Probabilistic Systems
Axel Legay, IRISA/INRIA Rennes, France and
Mahesh Viswanathan, University of Illinois at Urbana-Champaign, USA
PART 2
Axel Legay, IRISA/INRIA Rennes, France and
Mahesh Viswanathan, University of Illinois at Urbana-Champaign, USA
PART 2
12:30-14:00
| Lunch break | building I, first floor |
14:00-15:30
| Tutorial | building I, room IB110 |
Infinite-State Verification: From Transition Systems to Markov Chains
Parosh Aziz Abdulla, Uppsala University
Parosh Aziz Abdulla, Uppsala University
15:30-16:00
| Coffee break | building I, first floor |
16:00-17:30
| Tutorial | building I, room IB110 |
Analyzing Large Sparse Markov Chains of Kronecker Products
Tugrul Dayar, Department of Computer Engineering, Bilkent University
Tugrul Dayar, Department of Computer Engineering, Bilkent University
18:00-19:30
| Welcome reception | building I, first floor |
|
Sunday session B | top of the page |
9:00-10:30
| Tutorial | building I, room IB210 |
An Introduction to Monte Carlo Methods and Rare Event Simulation
Gerardo Rubino and Bruno Tuffin,
IRISA/INRIA Rennes, France
PART 1
Gerardo Rubino and Bruno Tuffin,
IRISA/INRIA Rennes, France
PART 1
10:30-11:00
| Coffee break | building I, first floor |
11:00-12:30
| Tutorial | building I, room IB210 |
An Introduction to Monte Carlo Methods and Rare Event Simulation
Gerardo Rubino and Bruno Tuffin,
IRISA/INRIA Rennes, France
PART 2
Gerardo Rubino and Bruno Tuffin,
IRISA/INRIA Rennes, France
PART 2
12:30-14:00
| Lunch break | building I, first floor |
14:00-15:30
| Tutorial | building I, room IB210 |
Petri net analysis using decision diagrams
Gianfranco Ciardo, Department of Computer Science and Engineering, University of California at Riverside
PART 1
Gianfranco Ciardo, Department of Computer Science and Engineering, University of California at Riverside
PART 1
15:30-16:00
| Coffee break | building I, first floor |
16:00-17:30
| Tutorial | building I, room IB210 |
Petri net analysis using decision diagrams
Gianfranco Ciardo, Department of Computer Science and Engineering, University of California at Riverside
PART 2
Gianfranco Ciardo, Department of Computer Science and Engineering, University of California at Riverside
PART 2
18:00-19:30
| Welcome reception | building I, first floor |
| Monday | top of the page |
9:00-10:00
| Opening and Plenary session | building A, conference room AF |
QEST/FORMATS invited talk
Jan Beutel, ETH Zurich, Switzerland
Jan Beutel, ETH Zurich, Switzerland
10:00-10:30
| Coffee break | building I, room IB018 |
and also walk to building I, the place of the regular talks (see the map of the venue menuitem)
10:30-12:30
| Model checking | building I, room IB017 |
10:30-11:00
|
Pedro R. D'Argenio, Nicolás Wolovick, Pedro Sanchez Terraf and Pablo Celayes. Nondeterministic Labeled Markov Processes: Bisimulations and Logical Characterization
|
best paper
|
11:00-11:30
Jiri Barnat, Ivana Cerna and Jana Tumova. Quantitative Model Checking of Systems with Degradation
11:30-12:00
Joost-Pieter Katoen and Ivan Zapreev. Simulation-Based CTMC Model Checking: An Empirical Evaluation
12:00-12:30
Rena Bakhshi and Ansgar Fehnker. On the impact of modelling choices for distributed information spread
12:30-14:00
| Lunch break | building I, room IB018 |
14:00-15:30
| PH/MAP | building I, room IB017 |
14:00-14:30
Peter Buchholz and Jan Kriege. A Heuristic Approach for Fitting MAPs to Moments and Joint Moments
14:30-15:00
Reza Pulungan and Holger Hermanns. Acyclic Minimality by Construction
15:00-15:30
Hiroyuki Okamura and Tadashi Dohi. Faster Maximum Likelihood Estimation Algorithms for Markovian Arrival Processes
15:30-16:00
| Coffee break | building I, room IB018 |
16:00-18:00
| Hardware, Software models | building I, room IB017 |
16:00-16:30
Michael Kuperberg, Martin Krogmann and Ralf Reussner. TimerMeter: Quantifying Properties of Software Timers for System Analysis
16:30-16:40
Melinda Magyar and István Majzik. Modular Construction of Dependability Models from System Architecture Models: A Tool-supported Approach
16:40-17:10
Abigail Lebrecht, Nicholas Dingle and William Knottenbelt. A Performance Model of Zoned Disk Drives with I/O Request Reordering
17:10-17:20
Philippe Moret, Walter Binder, Alex Villazon, Danilo Ansaloni and Martin Schoeberl. Locating Performance Bottlenecks in Embedded Java Software with Calling-Context Cross-Profiling
17:20-17:50
Martin Schoeberl, Walter Binder, Philippe Moret and Alex Villazon. Design Space Exploration for Java Processors with Cross-Profiling
17:50-18:00
Max Walter, Philipp Limbourg and Sebastian Esch. COBAREA: The COpula-BAsed REliability and Availability modeling environment
| Tuesday | top of the page |
9:00-10:00
| Plenary session | building A, conference room AF |
FORMATS invited talk
Stéphane Gaubert, INRIA Saclay — Île-de-France, France
Stéphane Gaubert, INRIA Saclay — Île-de-France, France
10:00-10:30
| Coffee break | building I, room IB018 |
and also walk to building I, the place of the regular talks (see the map of the venue menuitem)
10:30-12:00
| QBDs | building I, room IB017 |
10:30-11:00
Juan F. Perez and Benny Van Houdt. Exploiting restricted transitions in Quasi-Birth-and-Death processes
11:00-11:30
Daniel Klink, Anne Remke, Boudewijn Haverkort and Joost-Pieter Katoen. Time-Bounded Reachability in Tree-Structured QBDs by Abstraction
11:30-12:00
Qi Zhang, Armin Heindl, Andreas Stathopoulos and Evgenia Smirni. Comparison of two output models for the BMAP/MAP/1 departure process
12:00-12:30
| Stochastic petri nets | building I, room IB017 |
András Horváth and Enrico Vicario. Aggregated stochastic state classes in quantitative evaluation of non-Markovian Stochastic Petri Nets
12:30-14:00
| Lunch break | building I, room IB018 |
14:00-15:30
| Probabilistic model checking | building I, room IB017 |
14:00-14:30
Ivan Zapreev, Joost-Pieter Katoen, Holger Hermanns, E. Moritz Hahn and David N. Jansen. The Ins and Outs of The Probabilistic Model Checker MRMC
14:30-15:00
Serge Haddad and Nihal Pekergin. Using Stochastic Comparison for Efficient Model Checking of Uncertain Markov Chains
15:00-15:30
Arnd Hartmanns and Holger Hermanns. A Modest Approach to Checking Probabilistic Timed Automata
15:30-16:00
| Coffee break | building I, room IB018 |
16:00-16:30
| Model checking | building I, room IB017 |
Husain Aljazzar and Stefan Leue. Generation of Counterexamples for Model Checking of Markov Decision Processes
16:30-17:00
| Tools demonstration | building I, room IB017 |
16:30-16:40
Divey Gulati, Ken Keefe, Quincy Mitchell, Eric W. D. Rozier and William H. Sanders. Remote Job Management in the Mobius Modeling Framework
16:50-16:50
Jonathan Bogdoll, Holger Hermanns and Lijun Zhang. FlowSim Simulation Benchmarking Platform
16:50-17:00
Antonius Erdmann and Dietmar Weber. PerDaCol and PerfAnalysis - A tool set for performance measurement data collection and evaluation of real-time communication systems
17:40-21:00
| Social program and banquet diner | in the city |
| Wednesday | top of the page |
9:00-10:00
| Plenary session | building A, conference room AF |
QEST invited talk
Lucy Cherkasova, Hewlett-Packard Laboratories, USA
Towards Automated Capacity Planning and Anomaly Detection for Enterprise Applications
Lucy Cherkasova, Hewlett-Packard Laboratories, USA
Towards Automated Capacity Planning and Anomaly Detection for Enterprise Applications
10:00-10:30
| Coffee break | building I, room IB018 |
and also walk to building I, the place of the regular talks (see the map of the venue menuitem)
10:30-12:30
| Network models | building I, room IB017 |
10:30-11:00
Jens Schmitt and Ivan Martinovic. Demultiplexing in Network Calculus - A Stochastic Scaling Approach
11:00-11:30
Giuliano Casale. The Multi-Branched Method of Moments for Queueing Networks
11:30-12:00
András Faragó. Quantifying the trade-off between the level of connectivity and local complexity in random wireless network topologies
12:00-12:30
Rena Bakhshi, Lucia Cloth, Wan Fokkink and Boudewijn Haverkort. Mean-Field Analysis for the Evaluation of Gossip Protocols
12:30-14:00
| Lunch break | building I, room IB018 |
14:00-15:00
| QBDs | building I, room IB017 |
14:00-14:30
Ruth Lamprecht and Peter Kemper. On the Detection of Symmetries in Compositional Markov Models
14:30-15:00
Afonso Sales and Brigitte Plateau. Reachable state space generation for structured models which use functional transitions
15:00-15:30
| Tools demonstration | building I, room IB017 |
15:00-15:10
Ricardo Czekster, Paulo Fernandes and Thais Webber. GTA express - A Software Package to Handle Kronecker Descriptors
15:10-15:20
Peter Kemper. Recent Extensions to Traviando
15:20-15:30
Elina Pacini Naumovich and Simona Bernardi. Integrating TPNs and performance bound techniques in DrawNET: a new import functionality
15:30-16:00
| Coffee break | building I, room IB018 |
16:00-17:00
| Probabilistic model checking | building I, room IB017 |
16:00-16:30
Alastair Donaldson, Alice Miller and David Parker. Language-level Symmetry Reduction for Probabilistic Model Checking
16:30-17:00
Husain Aljazzar, Manuel Fischer, Lars Grunske, Matthias Kuntz, Florian Leitner and Stefan Leue. Safety Analysis of an Airbag System using Probabilistic FMEA and Probabilistic Counter Examples
17:00-17:10
| Tools demonstration | building I, room IB017 |
Federica Ciocchetta, Adam Duguid, Stephen Gilmore, Maria Luisa Guerriero and Jane Hillston. The Bio-PEPA Tool Suite
17:10-17:20
| Closing | building I, room IB017 |
17:40-19:10
| Transportation to PMCCS | in front of building I |