30th Nordic Workshop on Programming Theory
Oslo, Norway

Important dates

  • Submission    September 1st  September 10
  • Notification    September 26
  • Final version  October 1st October 7
  • Registration   October 1st October 7
  • Workshop      October 24-26

Topics

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

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) through EasyChair. Work in progress as well as abstracts of manuscripts submitted for formal publication elsewhere are permitted.

As with earlier NWPT workshops, we have arranged a special issue of the Journal of Logical and Algebraic Methods in Programming (JLAMP) devoted to the best contributions to the workshop. The contributions will be selected by the PC. They will be invited after the workshop and will undergo a rigorous, journal-strength review process according to the standards of JLAMP.

Invited speakers

We are pleased to have three invited speakers for NWPT’18.

Erika Ábrahám   RWTH Aachen University, Germany

Title: Symbolic Computation Techniques in SMT Solving:
Mathematical Beauty meets Efficient Heuristics

Checking the satisfiability of quantifier-free real-arithmetic formulas is a practically highly relevant but computationally hard problem. Some beautiful mathematical decision procedures implemented in computer algebra systems are capable of solving such problems, however, they were developed for more general tasks like quantifier elimination, therefore their applicability to satisfiability checking is often restricted. In computer science, recent advances in satisfiability-modulo-theories (SMT) solving led to elegant embeddings of such decision procedures in SMT solvers in a way that combines the strengths of symbolic computation methods and heuristic-driven search techniques. In this talk we discuss such embeddings and show that they might be quite challenging but can lead to powerful synergies and open new lines of research.

Andrei Sabelfeld   Chalmers University, Sweden

Title: Breaking and Fixing IoT Apps: from Attacks to Formal Methods for Security

IoT apps empower users by connecting a variety of otherwise unconnected services. Unfortunately, the power of IoT apps can be abused by malicious makers, unnoticeably to users. We demonstrate that popular IoT app platforms are susceptible to several classes of attacks that violate user privacy, integrity, and availability. We estimate the impact of these attacks by an empirical study. We suggest short/medium-term countermeasures based on fine-grained access control and long-term countermeasures based on information flow tracking. Finally, we discuss general trends and challenges for the Web of Things and, in particular, the role of formal methods in securing it.

Parts of the talk are based on joint work with Iulia Bastys and Musard Balliu.

Peter Ölveczky   University of Oslo, Norway

Title: Design and Validation of Cloud Storage Systems using Rewriting Logic

To deal with large amounts of data while offering high availability and throughput and low latency, cloud computing systems rely on distributed, partitioned, and replicated data stores. Such cloud storage systems are complex software artifacts that are very hard to design and analyze. We argue that formal specification and model checking should be beneficial during their design and validation. In particular, I propose rewriting logic and its accompanying Maude tools as a suitable framework for formally specifying and analyzing both the correctness and the performance of cloud storage systems. This talk gives an overview of the use of rewriting logic at the University of Illinois’ Assured Cloud Computing center on industrial data stores such as Google’s Megastore and Facebook/Apache’s Cassandra. I also briefly summarize the experiences of the use of a different formal method for similar purposes by engineers at Amazon Web Services.

Program

Here is the program in PDF.

Registration

The workshops registration fee is 250€, and it covers:

  • Lunches and refreshments for Wednesday, Thursday and Friday
  • Welcome reception on Wednesday evening
  • Conference dinner on Thursday evening
  • E-proceedings

Click here to register for the workshop.

Travel information

Oslo is served by the Gardermoen Oslo Airport (OSL). From the airport, you can get to the city center via the Airport express train (Flytoget) or the Norwegian State Rails (NSB). NSB is cheaper than Flytoget, but not as frequent.

For getting around town see Ruter, the transit authority that oversees public transportation via buses, metro (T-banen), trams (trikken), and ferry. Local taxi firms include Oslo Taxi (+47 22 38 8090) and Christiania Taxi (+47 22 57 80 00).

You will need to book your accommodation independently. Most bookings can be made online. See VisitOslo for a selection of options. An inexpensive option is Cochs Pensjonat, near the royal castle. You may also consider booking a small apartment with Frogner House Apartments, Oslo Apartments or Airbnb. We are looking at arranging pre-booked rooms.

Venue

The workshop will be held at room Faros on the 5th floor of the Oslo Science Park (Forskningsparken), next to the University of Oslo Informatics building.

Oslotech AS
Gaustadalleen 21
N-0349 Oslo

Reception

We will have a reception with tapas on the 5th floor of the Ole-Johan Dahl’s building. The building is right across from the conference center. The reception is on Wednesday, October 24, at 17:30.

Dinner

On Thursday, October 25, at 18:30, we will have the workshop dinner at Ekeberg Restaurant.

Kongsveien 15
0193 Oslo

Committee

Program committee

  • Lars Birkedal, Aarhus Univ., Denmark
  • Johannes Borgström, Uppsala Univ., Sweden
  • Daniel S. Fava, Univ. of Oslo, Norway
  • John Gallagher, RUC, Denmark
  • Michael R. Hansen, DTU, Denmark
  • Magne Haveraaen, Univ. of Bergen, Norway
  • Keijo Heljanko, Aalto Univ., Finland
  • Fritz Henglein, Univ. of Copenhagen, Denmark
  • Thomas T. Hildebrandt, ITU, Denmark
  • Anna Ingólfsdóttir, Reykjavík Univ., Iceland
  • Einar Broch Johnsen, Univ. of Oslo, Norway
  • Jaakko Järvi, Univ. of Bergen, Norway
  • Yngve Lamo, Bergen Univ. Col., Norway
  • Kim G. Larsen, Aalborg Univ., Denmark
  • Alberto Lluch Lafuente, DTU, Denmark
  • Fabrizio Montesi, Univ. of Southern Denmark, Denmark
  • Wojciech Mostowski, Halmstad Univ., Sweden
  • Olaf Owe, Univ. of Oslo, Norway
  • Philipp Rümmer, Uppsala Univ., Sweden
  • Gerardo Schneider, University of Gothenburg, Sweden
  • Cristina Seceleanu, Mälardalen Univ., Sweden
  • Jiri Srba, Aalborg Univ., Denmark
  • Tarmo Uustalu, Reykjavík Univ., Iceland
  • Jüri Vain, Tallinn Univ. of Tech., Estonia
  • Antti Valmari, University of Jyväskylä, Finland
  • Marina Waldén, Åbo Akademi Univ., Finland

Recent previous years

  • Turku, Finland, 2017
  • North Jutland, Denmark, 2016
  • Reykjavík, Iceland, 2015
  • Halmstad, Sweden, 2014
  • Tallinn, Estonia, 2013
  • Bergen, Norway, 2012
  • Västerås, Sweden, 2011
  • Turku, Finland, 2010
  • Lyngby, Denmark, 2009
  • Tallinn, Estonia, 2008

Organizers

Contact

Further information at nwpt-18@ifi.uio.no