21st Nordic Workshop on Programming Theory, NWPT '09
Lyngby, Denmark, 14-16 October 2009
NWPT '09 Home
Call for papers
Important Dates

- Wednesday
- Thursday
- Friday

Invited Talks
Travel info


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

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
19:00 Conference Dinner at Restaurant Fortunen
Ved Fortunen 33, 2800 Kgs. Lyngby

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

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

http://www.imm.dtu.dk/nwpt09 | email: nwpt09(at)imm.dtu.dk | ę DTU Informatics, 2009