NWPT '09 Home
Call for papers
Organisation
Important Dates
Programme
- Wednesday
- Thursday
- Friday
Background
Scope
Invited Talks
Submission
Publication
Venue
Registration
Accommodation
Travel info
|
Programme
All sessions take place in:
Building 101A, Meeting Room 1
Technical University of Denmark (DTU)
Anker Engelundsvej 1, 2800 Kgs. Lyngby
Building 101 is the main building at DTU, and Meeting Room 1 is upstairs, next to Faculty Club. See monitors at entrance 101A.
Wednesday, October 14, 2009
|
8:30 - 9:00
|
Registration and welcome
|
Probabilistic Systems
Session Chair - Michael R. Hansen
|
9:00 - 9:25
|
Lei Song and J. C. Godskesen
|
|
A probabilistic calculus for mobile and ad hoc networks
|
|
9:25 - 9:50
|
N. Skrypnyuk, F. Nielson and H. Pilegaard
|
|
Pathway Analysis for IMC
|
|
9:50 - 10:15
|
B. Delahaye, B. Caillaud and A. Legay
|
|
Compositional Reasoning for Assume/Guarantee Contracts Combining Stochastic and Nondeterministic Aspects
|
|
10:15 - 10:40
|
E. Yüksel, H. R. Nielson and F. Nielson
|
|
Quantitative Security Analysis of ZigBee Key Updates
|
Coffee Break
Invited Talk
Chair - Michael R. Hansen
|
11:00 - 12:00
|
Joost-Pieter Katoen
|
|
Verifying Large -and Infinite- Markov Chains
|
Lunch in the main canteen, on the ground floor in building 101
Model Checking
Session Chair - Einar Broch Johnsen
|
13:00 - 13:25
|
N. Timm
|
|
A Bounded Model Checker for Partially Known Systems
|
|
13:25 - 13:50
|
G. Sauter, H. Dierks, M. Fränzle and M. R. Hansen
|
|
Light-weight hybrid model checking facilitating online prediction of temporal properties
|
|
13:50 - 14:15
|
H. A. Hansen and G. Schneider
|
|
On the reachability analysis of planar, non-linear autonomous systems using hybrid systems
|
|
14:15 - 14:40
|
W. P. Heise, M. Fränzle, M. R. Hansen
|
|
A prototype model checker for Duration Calculus
|
Coffee Break
Wireless Sensor Networks
Session Chair - Uwe Wolter
|
15:00 - 15:25
|
W. Leister and J. Bjørk
|
|
Modelling Routing Algorithms for Wireless Sensor Networks in Creol
|
|
15:25 - 15:50
|
M. K. Jakobsen, M. R. Hansen and J. Madsen
|
|
Formal verification of energy aware routing algorithm
|
|
15:50 - 16:15
|
M. S. Vighio and A. P. Ravn
|
|
Analysis of collision in wireless sensor networks
|
Get-together
|
16:15 - 17:30
|
Informal gathering w/ refreshments
|
Thursday, October 15, 2009
Static Analysis
Session Chair - Bengt Nordström
|
9:00 - 9:25
|
M. Steffen and T. M. T. Tran
|
|
Safe Commits for Transactional Featherweight Java
|
|
9:25 - 9:50
|
A. Cortesi and R. Halder
|
|
Abstract Interpretation Framework for Structured Query Languages
|
|
9:50 - 10:15
|
I. Grabe, M. Steffen and F. de Boer
|
|
Static Deadlock Detection for Active Objects
|
|
10:15 - 10:40
|
P. Schneider-Kamp, J. Giesl, A. Serebrenik, T. Ströder and R. Thiemann
|
|
Proving Termination for Logic Programs with Cut
|
Coffee Break
Invited talk
Chair - Michael R. Hansen
|
11:00 - 12:00
|
Franz Wotawa
|
|
The current State of Automated Debugging
|
Lunch in the glass room of the main canteen
Testing and Verification
Session Chair - Uwe Wolter
|
13:00 - 13:25
|
M. Veanes, P. Grigorenko, J. de Halleux and N. Tillmann
|
|
Symbolic Query Exploration
|
|
13:25 - 13:50
|
M. Nica, I. Moraru and F. Wotawa
|
|
Representing Program Debugging as Constraint Satisfaction Problem
|
|
13:50 - 14:15
|
A. Torjusen, M. Steffen and O. Owe
|
|
Model Testing Asynchronously Communicating Objects using Modulo AC Rewriting
|
Coffee Break
Logic and Semantics
Session Chair - Einar Broch Johnsen
|
14:35 - 15:00
|
L. Juhl
|
|
Introducing Modal Transition Systems with Weight Sets
|
|
15:00 - 15:25
|
A. Hernandez and F. Nielson
|
|
Enforcing Mandatory Access Control in Distributed Systems using Aspect-Orientation
|
|
15:25 - 15:50
|
C. Prisacariu
|
|
A Decidable Logic for Complex Contracts
|
Robot Swarms
Session Chair - Michael R. Hansen
|
16:00 - 16:25
|
S. Juurik and J. Vain
|
|
Model checking emerging behavior properties of robot swarms
|
|
16:25 - 16:50
|
S. L. T. Tarifa and E. B. Johnsen
|
|
The Cooperative Cleaners Case Study: Modelling and Analysis in Creol
|
Conference Dinner
Friday, October 16, 2009
Computation and Semantics
Session Chair - Bengt Nordström
|
9:00 - 9:25
|
L. Birkedal, K. Støvring and J. Thamsborg.
|
|
Predicates for higher-order store
|
|
9:25 - 9:50
|
J. Schönborn and M. Kyas
|
|
Ready Semantics for UML State Machines
|
|
9:50 - 10:15
|
L. Birkedal, K. Støvring and J. Thamsborg
|
|
One-sided Top-top-closed Relations: The What and Why
|
|
10:15 - 10:40
|
T. Altenkirch, J. Chapman and T. Uustalu
|
|
Machine assisted proofs in the theory of monads
|
Coffee Break
Invited talk
Chair - Michael R. Hansen
|
11:00 - 12:00
|
Dines Bjørner
|
|
Role of Domain Engineering in Software Development - Why Current Requirements Engineering are Flawed?
|
Lunch in the glass room of the main canteen
Model-Driven Engineering
Session Chair - Paul Pettersson
|
13:00 - 13:25
|
A. Rossini, A. Rutle, F. Mancini, D. Hovland, K. A. Mughal, Y. Lamo and U. Wolter
|
|
A Formal Approach to the Specification of Data Validation Constraints in MDE
|
|
13:25 - 13:50:
|
A. Rutle, A. Rossini, Y. Lamo and U. Wolter
|
|
Constraint-Aware Model Transformations
|
|
13:50 - 14:15
|
A. Brekling, M. R. Hansen and J. Madsen
|
|
Analysis of Quantitative Properties of Hardware Specifications
|
Coffee Break
Semantics
Session Chair - Michael R. Hansen
|
14:35 - 15:00
|
J. Okika, O. Owe and C. Prisacariu
|
|
Operational Semantics for BPEL Complex Features in Rewriting Logic
|
|
15:00 - 15:25
|
A. Causevic, C. Seceleanu and P. Pettersson
|
|
Behavioral Modeling and Refinement of Services
|
|
15:25 - 15:50
|
L. Hartmann, N. D. Jones and J. G. Simonsen
|
|
Programming in Biomolecular Computation
|
|