Revision as of 17:42, 27 September 2014

NWPT 2014 Poster.

26th Nordic Workshop on Programming Theory, NWPT '14

October 29-31, 2014 - Halmstad University, Sweden

Introduction

The NWPT series of annual workshops is a forum bringing together programming theorists from the Nordic and Baltic countries (but also elsewhere).

Call for Papers

Scope

Topics of interest include (but are not limited to)

semantics of programming languages
programming language design and programming methodology
programming logics
formal specification of programs
program verification
program construction
tools for program verification and construction
program transformation and refinement
real-time and hybrid systems
models of concurrency and distributed computing
language-based security.

Important Dates

Deadlines:

~~15 September~~ 20 September 2014: Submission of abstracts
28 September 2014: Notification
5 October 2014: Registration deadline

Submission

Authors wishing to give a talk at the workshop are requested to submit abstracts of 2-3 pages (pdf, printable on A4 paper, using easychair.cls from http://www.easychair.org/publications/easychair.zip ) through EasyChair. Work in progress as well as abstracts of manuscripts submitted for formal publication elsewhere are permitted.

Submission website is located at: https://www.easychair.org/conferences/?conf=nwpt2014

Publication

The abstracts of the accepted contributions will be available at the workshop.

We have arranged a special issue of the Journal of Logic and Algebraic Methods in Programming dedicated to the best contributions of the workshop. The contributions will be invited after the workshop and will undergo a rigorous review process according to the stringent rules of JLAMP.

Invited Speakers

Holger Hermanns, Saarland University, Germany

Title: Concurrent Programming Education in the Post-Java Era

Abstract:

Many-core architectures - service orientation - business processes - app technology - pervasive systems - organic computing. All these are en vogue topics in computing practice. At their common core, they all revolve around ways to master and exploit concurrency. Unfortunately, concurrency is a notoriously difficult subject to master. Our students are facing the challenge. Do we educate them properly?

This invited talk asks for concerted efforts to make our foundational concurrency education apt for the concurrency challenges. As a potential nucleus it presents pseuco.com, an open platform for light weight education of the core principles of concurrency theory and practice. This is wrapped in a simple, yet executable pseudocode notation, and features ways to study semantic as well pragmatic aspects of concurrent programming, covering both message-passing and shared-memory paradigms.

Anna Ingolfsdottir, Reykjavik University, Iceland

Title: Graphical versus Logical Specifications

(Inspired by a paper with the same title by Kim G. Larsen and Gerard Boudol)

Abstract:

It has become a standard approach to use graphical formalisms to describe, on an abstract level, the behaviour of systems or processes. Typical formalisms of this kind are Labelled Transition Systems (LTS), Kripke Structures and different types of automata. Although these description are on a relatively abstract level, there has been a need to introduce formalisms that are even more abstract where properties of such systems can be expressed and reasoned about in a systematic way. For this purpose different types of logical formalisms have been introduced and reasoned about. Sometimes these logical formalisms characterize the underlying graphical formalisms, often up to a given equivalence or preorder in the sense that two processes are equivalent if and only if they satisfy exactly the same formulae in the language or, in the case of a preorder, the larger one satisfies all the formulas the smaller one satisfies.

Independent of this correlation with the graphical relations, it makes perfect sense to define logical equivalence and preorders by saying that two process are logically equivalent if they satisfy the same formulae and similarly for the preorder. In the cases described above this logical and the graphical equivalence and preorders coincide.

In this talk I will try to compare, in a very general sense, the logical and the graphical characterization of processes and relationships between them. In particular I will focus on what it means for a formula to be characteristic or prime with respect to the logical equivalence, what the connection is between these two concepts and when we can expect processes to have characteristic formula and when not.

Catuscia Palamidessi, INRIA Saclay and École Polytechnique, France

Title: New Advances in Quantitative Information Flow

Abstract:

Quantitative Information Flow deals with the leakage of secret information by programs and systems due to the (probabilistic) correlation with public observables. In this talk we will report on one of the most recent proposals to formalize the notion of the vulnerability of the secrets. This approach offers a rich operational model of the attacker, based on decision theory, and it turns out that it is characterized by a surprisingly simple set of axioms. Then, we will discuss the relation with the axiomatic systems defining Shannon and Renyi information theory, which have been the foundations of the most popular proposal for (quantitative) language-based security so far, thus providing an axiomatically structured view of the field.

Tentative Program

October 29 (08:30-17:00)

08:30-09:15 Arrival and Registration

09:15-09:30 Welcome, opening remarks (Mohammad Mousavi, Halmstad)

09:30-10:30 Invited Talk: Catuscia Palamidessi, New Advances in Quantitative Information Flow

10:30-11:00 Coffee / Tea Break

11:00-12:30 Session 1: Security and Contracts

Raúl Pardo and Gerardo Schneider. Privacy-Preserving Social Networks

Patrick Bahr, Jost Berthold and Martin Elsman. Towards Certified Management of Financial Contracts

John J. Camilleri and Gerardo Schneider. On the formal analysis of normative texts

12:30-14:00 Lunch

14:00-15:30 Session 2: Process Algebra

Abeer Al-Humaimeedy and Maribel Fernandez. Introducing Mobility into CSP

Bashar Alkhawaldeh. Modelling and Verification of RBC Handover Using CSP

Harsh Beohar. Towards a Precongruence Format for Input-Output Conformance

15:30-16:00 Coffee / Tea Break

16:00-17:00 Session 3: Model Evolution

Fazle Rabbi, Yngve Lamo, Ingrid Yu and Lars Kristensen. Towards a Diagrammatic Rewriting System for Model Completion

Volker Stolz. Safer Refactorings

18:00-19:30 Reception at the City Library

October 30 (9:00-17:00)

09:00-10:00 Invited Talk: Anna Ingolfsdottir, Graphical versus Logical Specifications

10:00-10:30 Coffee / Tea Break

10:30-12:00 Session 4: Semantics

Casper Bach Poulsen and Peter D. Mosses. Divergence as State in Coinductive Big-Step Semantics

Tarmo Uustalu. How to contain monads?

James Chapman and Andreas Abel. Normalization by Evaluation in the Delay Monad: An Extended Case Study for Coinduction via Copatterns and Sized Types

Detlef Plump. From Imperative to Rule-based Graph Programs

12:30-14:00 Lunch

14:00-15:30 Session 5: Analysis

Jesus Mauricio Chimento, Wolfgang Ahrendt, Gerardo Schneider and Gordon Pace. StaRVOOrS: A Framework for Unified Static and Runtime Verification of Object-Oriented Software

Georgiana Caltais and Bertrand Meyer. Coffman deadlocks in SCOOP

Mahsa Varshosaz and Harsh Beohar. Delta-Oriented Testing for Finite State Machines

15:30-16:00 Coffee / Tea Break

16:00-17:00 Session 6: Specification and Refinement

Masoumeh Parsa, Colin Snook, Marta Olszewska and Marina Walden. Parallel development of Event-B systems with agile methods

Muhammad Taimoor Khan, Dimitrios Serpanos and Howard Shrobe. On the Behavioral Formalization of the Cognitive Middleware AWDRAT

18:30- Social Dinner

October 31 (9:00-14:00)

09:00-10:00 Invited Talk: Holger Hermanns, Concurrent Programming Education in the Post-Java Era

10:00-10:30 Coffee / Tea Break

10:30-12:30 Session 7: Embedded and Cyber-Physical Systems

Hang Yin, Rafia Inam, Reinder Bril and Mikael Sjödin. Formalization and verification of mode changes in hierarchical scheduling

Walid Taha, Kevin Atkinson, Paul Brauner, Robert Cartwright, Alexandre Chapoutot, Adam Duracz, Jan Duracz and Yingfu Zeng. The Acumen Language

Suleyman Savas and Essayas Gebrewahid. Development of Architecture and Software Tools for High Performance Embedded Computing

Morteza Mohaqeqi, Mohammadreza Mousavi and Walid Taha. Conformance Testing of Cyber-Physical Systems: A Comparative Study

12:30-14:00 Lunch

Program Committee

Luca Aceto, Reykjavík Univ., Iceland
Lars Birkedal, Aarhus Univ., Denmark
Einar Broch Johnsen, Univ. of Oslo, Norway
Michael R. Hansen, DTU, Denmark
Keijo Heljanko, Aalto Univ., Finland
Fritz Henglein, Univ. of Copenhagen, Denmark
Yngve Lamo, Bergen Univ. Col., Norway
Kim G. Larsen, Aalborg Univ., Denmark
Mohammad Mousavi, Halmstad Univ., Sweden
Bengt Nordström, Univ. of Gothenburg, Sweden
Olaf Owe, Univ. of Oslo, Norway
Paul Pettersson, Mälardalen Univ., Sweden
Gerardo Schneider, Chalmers, Sweden
Walid Taha, Halmstad Univ., Sweden
Tarmo Uustalu, Inst. of Cybernetics, Estonia
Jüri Vain, Tallinn Univ. of Tech., Estonia
Marina Waldén, Åbo Akademi Univ., Finland
Uwe Wolter, Univ. of Bergen, Norway
Wang Yi, Uppsala Univ., Sweden

Venue

The workshop will be held on the campus of Halmstad University in Halmstad, Sweden. Halmstad is a popular holiday destination located on the Swedish west coast. Just a few minutes by bicycle or bus takes you from campus to city centre, sandy beaches or forested Galgberget Hill.

Directions to/in Campus

Directions for getting to campus can be found at http://www.hh.se/english/abouttheuniversity/visitus.307_en.html

The campus map can be found here. The workshop will be located at the Wigforss lecture hall, which is located at the ground floor of the J building (Visionen). Coffee breaks will be held at the ground floor of the same building.

Directions to Halmstad

Trains take you directly to Göteborg in 75 minutes, to the Malmö-Copenhagen area in about 2 hours and to Stockholm in 4.5 hours. There are also daily flights from Halmstad Airport to Stockholm.

If you are flying in internationally it is generally easiest to fly into Copenhagen (CPH) airport (also known as Kastrup). The best thing about flying into CPH is that you just buy a train ticket when you arrive at the airport and simply take a train from the airport directly to Halmstad. The train leaves from the airport itself approximately once an hour on weekdays. We recommend that you check the time-table at the Swedish Railways site and allow one hour from touchdown to getting to the train station (just outside customs). (It seems that you can take an earlier or a later train on the same day regardless of the exact train you booked, but obviously you will lose your seat reservation if you have made one.) To get to your hotel, you can combine a taxi booking with your train ticket at the Swedish Railways site and a driver will wait for you with your name mentioned on a board once you arrive in Halmstad.

In Halmstad, everything is either in walking distance or a short taxi ride away. Usually there are taxis at the station. If there are none there is a phone that connects directly to the local taxi company. For the eventuality that the phone is not working, it is good to have a cell phone handy. The number for the taxi company is written on the phone.

Note that CPH is in Denmark (and not in Sweden). So, if you need visas for European countries, make sure you get one that works for both. If for some reason you cannot or do not want to use CPH, the next best international airport is in Gothenburg (GOT), locally known as Landvetter. The tricky thing about using that airport is that you would first have to take a 45 minute shuttle from the airport to the Gothenburg train station, and then take the train to Halmstad. That is one transfer and one wait.

Accommodation

We have made a pre-booking for a number of rooms at Hotel Continental. The negotiated rate is 995 SEK/night for single rooms and 1218 SEK/night for standard (double) rooms, both including breakfast. If you would like to use this offer, please send an email to the hotel reservation and mention the booking code "NWPT2014". The pre-booking is only valid till October 15, 2014.

Here are some other suggestions for the accommodation, with an indication of their price range, (obtained from booking.com) and their distance to the workshop venue:

Scandic Hallandia (~160-200 EUR / night, 2km)
Hotel Amadeus (~100-120 EUR / night, 2.5km)
First Hotel Martenson (~130-150 EUR / night, 2km)
Quality Hotel Halmstad (~80-100 EUR / night, 3 km)
STF Halmstads Hostel Kaptenshamn (~80-100 EUR / night, 2km)

Registration

To register for the workshop, please visit the registration page. The registration fee for people providing the VAT number of their corresponding university / institute is 1800 SEK and without providing the VAT number is 2250 SEK. It includes attendance, coffee and lunch breaks, proceedings on a USB stick, reception and workshop dinner, but excludes the drinks at the workshop dinner. Payment can be performed preferably using PayPal or by invoicing your university / institute. The registration deadline is 5 October, 2014.

History

The previous editions were held in

Uppsala (1989, 1999 and 2004),
Aalborg (1990),
Göteborg (1991 and 1995),
Bergen (1992, 2000 and 2012),
Åbo (1993, 1998, 2003 and 2010),
Aarhus (1994),
Oslo (1996, 2007),
Tallinn (1997, 2002, 2008 and 2013),
Lyngby (2001 and 2009),
Copenhagen (2005),
Reykjavík (2006), and
Västerås (2011).

Organizers

Veronica Gaspes (Organization Chair, veronica.gaspes@hh.se)
Mohammad Mousavi (Program Co-Chair, m.r.mousavi@hh.se)
Eva Nestius (Local Organization)
Walid Taha (Program Co-Chair, walid.taha@hh.se)

Difference between revisions of "NWPT 2014"

Revision as of 17:42, 27 September 2014

Contents

Introduction

Call for Papers

Scope

Important Dates

Submission

Publication

Invited Speakers

Tentative Program

Program Committee

Venue

Directions to/in Campus

Directions to Halmstad

Accommodation

Registration

History

Organizers

Navigation menu

Views

Personal tools

Search

Tools

@@ Line 92: / Line 92: @@
-=Program=
-To be announced.
+=Tentative Program=
+'''October 29  (08:30-17:00)'''
+:30-09:15 Arrival and Registration
+:15-09:30 Welcome, opening remarks (Mohammad Mousavi, Halmstad)
+:30-10:30 '''Invited Talk:''' Catuscia Palamidessi, New Advances in Quantitative Information Flow
+:30-11:00 Coffee / Tea Break
+:00-12:30 Session 1: Security and Contracts
+Raúl Pardo and Gerardo Schneider. Privacy-Preserving Social Networks
+Patrick Bahr, Jost Berthold and Martin Elsman. Towards Certified Management of Financial Contracts
+John J. Camilleri and Gerardo Schneider. On the formal analysis of normative texts
+:30-14:00  Lunch
+:00-15:30 Session 2: Process Algebra
+Abeer Al-Humaimeedy and Maribel Fernandez. Introducing Mobility into CSP
+Bashar Alkhawaldeh. Modelling and Verification of RBC Handover Using CSP
+Harsh Beohar. Towards a Precongruence Format for Input-Output Conformance
+:30-16:00  Coffee / Tea Break
+:00-17:00 Session 3: Model Evolution
+Fazle Rabbi, Yngve Lamo, Ingrid Yu and Lars Kristensen. Towards a Diagrammatic Rewriting System for Model Completion
+Volker Stolz. Safer Refactorings
+:00-19:30 Reception at the City Library
+'''October 30  (9:00-17:00)'''
+:00-10:00 '''Invited Talk:''' Anna Ingolfsdottir, Graphical versus Logical Specifications
+:00-10:30 Coffee / Tea Break
+:30-12:00 Session 4: Semantics
+Casper Bach Poulsen and Peter D. Mosses. Divergence as State in Coinductive Big-Step Semantics
+Tarmo Uustalu. How to contain monads?
+James Chapman and Andreas Abel. Normalization by Evaluation in the Delay Monad: An Extended Case Study for Coinduction via Copatterns and Sized Types
+Detlef Plump. From Imperative to Rule-based Graph Programs
+:30-14:00  Lunch
+:00-15:30 Session 5: Analysis
+Jesus Mauricio Chimento, Wolfgang Ahrendt, Gerardo Schneider and Gordon Pace. StaRVOOrS: A Framework for Unified Static and Runtime Verification of Object-Oriented
+Software
+Georgiana Caltais and Bertrand Meyer. Coffman deadlocks in SCOOP
+Mahsa Varshosaz and Harsh Beohar. Delta-Oriented Testing for Finite State Machines
+:30-16:00  Coffee / Tea Break
+:00-17:00 Session 6: Specification and Refinement
+Masoumeh Parsa, Colin Snook, Marta Olszewska and Marina Walden. Parallel development of Event-B systems with agile methods
+Muhammad Taimoor Khan, Dimitrios Serpanos and Howard Shrobe. On the Behavioral Formalization of the Cognitive Middleware AWDRAT
+:30- Social Dinner
+'''October 31  (9:00-14:00)'''
+:00-10:00 '''Invited Talk:''' Holger Hermanns, Concurrent Programming Education in the Post-Java Era
+:00-10:30 Coffee / Tea Break
+:30-12:30 Session 7: Embedded and Cyber-Physical Systems
+Hang Yin, Rafia Inam, Reinder Bril and Mikael Sjödin. Formalization and verification of mode changes in hierarchical scheduling
+Walid Taha, Kevin Atkinson, Paul Brauner, Robert Cartwright, Alexandre Chapoutot, Adam Duracz, Jan Duracz and Yingfu Zeng. The Acumen Language
+Suleyman Savas and Essayas Gebrewahid. Development of Architecture and Software Tools for High Performance Embedded Computing
+Morteza Mohaqeqi, Mohammadreza Mousavi and Walid Taha. Conformance Testing of Cyber-Physical Systems: A Comparative Study
+:30-14:00  Lunch