Last modified on October 29, 2011, 2:52 pm

NWPT 2011
 
Invited Speakers
Programme
Call for papers
Paper submission
Important dates
Registration
Accomodation
Venue/Maps
Organization
Local/Travel Info
Event Photographs
 

Supported by:


NWPT 2011 Program

[ Programme as PDF file ]
[ NWPT 2011 PROCEEDINGS as PDF file ]

Wednesday 26/10:

08.30-09.00Registration and Welcome
09.00-10.00Invited talk: Michael Williams
Title: Ensure you are wearing fireproof clothes before trying to introduce disruptive technology
10.00-10.20Coffee
10.20-12.00 Sesssion 1: Model-checking and Compositionality
Chair: Paul Pettersson, Mälardalen University (MDH)
10:20 - 10:45 : Tim Strazny. Accelerating Backward Reachability Analysis
10:45 - 11:10 : Dung Phan Anh and Michael R. Hansen. From functional programming to multicore parallelism: A case study based on Presburger Arithmetic
11:10 - 11:35 : Hallstein Asheim Hansen. GSPeeDI - a reachability checker for planar, polygonal hybrid systems using incomplete acceleration
11:35 - 12:00 : Hardi Hungar. Compositionality with Strong Assumptions
12.00-13.00Lunch
13.00-14.40 Sesssion 2: Service-Oriented and Distributed Systems
Chair: Thomas Hildebrandt, IT University of Copenhagen (ITU)
13:00 - 13:25 : Søren Debois, Thomas Hildebrandt, Raghava Rao Mukkamala and Francesco Zanitti. Towards a Programming Language for Declarative Event-based Context-sensitive Reactive Services
13:25 - 13:50 : Saleem Vighio, Anders Ravn and Zhiming Liu. A Verified Design Pattern for Long-running Nested Transactions
13:50 - 14:15 : Luigia Petre and Petter Sandvik. Formal Modelling of Inter-Peer Relations in Peer-to-Peer Media Distribution Systems
14:15 - 14:40 : Patrick Bahr. A Functional Language for Specifying Business Reports
14.40-15.00Coffee
15.00-17.05 Sesssion 3: Program Analysis
Chair: Cristina Seceleanu, Mälardalen University (MDH)
15:00 - 15:25 : Alastair Donaldson, Leopold Haller, Daniel Kroening and Philipp Ruemmer. Software Verification Using k-Induction
15:25 - 15:50 : Viorel Preoteasa, Ralph-Johan Back and Johannes Eriksson. Verification and Code Generation for Invariant Diagrams in Isabelle
15:50 - 16:15 : Johan Dovland, Einar Broch Johnsen, Olaf Owe and Ingrid Yu. A Proof System for Adaptable Class Hierarchies
16:15 - 16:40 : Marco Carbone, Thomas Hildebrandt and Hugo A. López. Open Mixed Refinement
16:40 - 17:05 : Patrick Bahr. Evaluation à la Carte -- Non-Strict Evaluation via Compositional Data Types
17.15-19.30Reception @ MDH student union pub
Thursday 27/10:

09.00-10.00Invited talk: Werner Damm
Title: Does it pay to extend the parameter of the world model?
10.00-10.20Coffee
10.20-12.00 Sesssion 4: Behavioral Specification and Analysis
Chair: Marina Waldén, Åbo Akademi
10:20 - 10:45 : Muhammad Taimoor Khan and Wolfgang Schreiner. Towards a Behavioral Analysis of Computer Algebra Programs
10:45 - 11:10 : Einar Broch Johnsen, Rudolf Schlatte and Silvia Lizeth Tapia Tarifa. Integrating Resource-Restricted Execution Contexts with Abstract Behavioral Specifications
11:10 - 11:35 : Ka I Pun, Martin Steffen and Volker Stolz. Polymorphic behavioural lock effects for deadlock checking
11:35 - 12:00 : Sofia Cassel, Falk Howar, Bengt Jonsson, Maik Merten and Bernhard Steffen. A Succinct Canonical Register Automaton Model
12.00-13.00Lunch
13.00-14.00 Invited talk: Glynn Winskel
Title: The winning ways of concurrent games
14.00-14.10Break
14.10-15.00 Sesssion 5: Probabilistic Systems
Chair: TBA
14:10 - 14:35 : Benoit Delahaye, Kim Guldstrand Larsen, Axel Legay and Mikkel L. Pedersen. Stuttering in Abstract Probabilistic Automata
14:35 - 15:00 : Luke Herbert and Robin Sharp. Towards quantitative evaluation of stochastic pharmacy workflows
15.00-15.20Coffee
15.20-17.00 Sesssion 6: Model-Driven Engineering
Chair: Alessandro Rossini, University of Bergen
15:20 - 15:45 : Xiaoliang Wang and Yngve Lamo. Correctness of Constraint-aware Model Transformations
15:45 - 16:10 : Andreas Johnsen, Paul Pettersson and Kristina Lundqvist. An Architecture-based Verification Technique for AADL-specifications
16:10 - 16:35 : Jose Quaresma, Christian W. Probst and Flemming Nielson. The Guided System Development Framework
16:35 - 17:00 : Florian Mantz, Alessandro Rossini, Gabriele Taentzer, Yngve Lamo and Uwe Wolter. Formalising Metamodel Evolution based on Category Theory
18.30 -Recreation and Workshop Dinner @ STRIKE bowling/Restaurant
Friday 28/10:

09.00-10.00 Invited talk: Björn Lisper
Title: Parametric WCET Analysis
10.00-10.20Coffee
10.20-12.00 Sesssion 7: Static Analysis
Chair: Kai Lampka, ETH Zurich
10:20 - 10:45 : Thi Mai Thuong Tran, Martin Steffen and Hoang Truong. Estimating Resource Bounds for Software Transactions
10:45 - 11:10 : Bart Van Delft. Value sensitivity in information flow analysis
11:10 - 11:35 : Stefan Bygde, Björn Lisper and Niklas Holsti. Static Analyis of Bounded Polyhedra
11:35 - 12:00 : Kasper Søe Luckow, Bent Thomsen and Stephan Erbs Korsholm. Towards a Real-Time, WCET Analysable JVM Running in 256 kB of Flash Memory
12.00-13.00Lunch
13.00-14.40 Session 8: Real- time Systems
Chair: TBA
13:00 - 13:25 : Pontus Ekberg, Nan Guan, Martin Stigge and Wang Yi. An Optimal Resource Sharing Protocol for Generalized Multiframe Tasks
13:25 - 13:50 : Leo Hatvani, Paul Pettersson and Cristina Seceleanu. Adaptive Task Automata: A Framework for Verifying Adaptive Embedded Systems
13:50 - 14:15 : Kai Lampka and Lothar Thiele. Towards Integrated Modeling: Analytic Real-time Interfaces for Timed Automata based Component Models
14:15 - 14:40 : Hang Yin and Hans Hansson. A Mode Switch Logic for component-based multi-mode systems
14.40-15.00Coffee
15.00-17.05 Session 9 Semantics
Chair: Björn Lisper, MDH
15:00 - 15:25 : Elena Oshevskaya, Irina Virbitskaite and Eike Best. A Categorical View of Bisimulation for Higher Dimensional Automata
15:25 - 15:50 : Filippo Del Tedesco, Sebastian Hunt and David Sands. A Semantic Hierarchy for Erasure Policies
15:50 - 16:15 : Michael Mendler, Joaquin Aguado and Marc Pouzet. Unifying synchronous data and control flow in the lazy lambda-calculus
16:15 - 16:40 : Erika Abraham, Thi Mai Thuong Tran and Martin Steffen. Inheritance and Observability
16:40 - 17:05 : Härmel Nestra. Compositional Transfinite Semantics of While
Web page hosted at School of Innovation, Design and Engineering,
Mälardalen University, Sweden. Webmaster: Jagadish Suryadevara